cvc4-1.3
cvc3_compat.h File Reference

CVC3 compatibility layer for CVC4. More...

#include "cvc4_public.h"
#include "expr/expr_manager.h"
#include "expr/expr.h"
#include "expr/type.h"
#include "smt/smt_engine.h"
#include "util/rational.h"
#include "util/integer.h"
#include "util/exception.h"
#include "util/hash.h"
#include "parser/parser.h"
#include <stdlib.h>
#include <map>
#include <utility>

Go to the source code of this file.

Data Structures

class  CVC3::CLFlag
 
class  CVC3::CLFlags
 
class  CVC3::Proof
 
class  CVC3::Theorem
 
class  CVC3::ExprMap< T >
 
class  CVC3::ExprHashMap< T >
 
class  CVC3::Type
 
class  CVC3::Expr
 Expr class for CVC3 compatibility layer. More...
 
class  CVC3::ExprManager
 
class  CVC3::ValidityChecker
 CVC3 API (compatibility layer for CVC4) More...
 

Namespaces

 CVC3
 

Macros

#define __CVC4__CVC3_COMPAT_H
 
#define _cvc3__expr_h_
 
#define _cvc3__include__vc_h_
 
#define _cvc3__command_line_flags_h_
 
#define _cvc3__include__queryresult_h_
 
#define _cvc3__include__formula_value_h_
 
#define PRESENTATION_LANG
 
#define SMTLIB_LANG
 
#define SMTLIB_V2_LANG
 
#define TPTP_LANG
 
#define AST_LANG
 

Typedefs

typedef size_t CVC3::ExprIndex
 
typedef CVC4::TypeCheckingException CVC3::TypecheckException
 
typedef size_t CVC3::Unsigned
 
typedef Expr CVC3::Op
 
typedef CVC4::Statistics CVC3::Statistics
 
typedef enum CVC3::QueryResult CVC3::QueryResult
 
typedef enum CVC3::FormulaValue CVC3::FormulaValue
 

Enumerations

enum  CVC3::CLFlagType {
  CVC3::CLFLAG_NULL, CVC3::CLFLAG_BOOL, CVC3::CLFLAG_INT, CVC3::CLFLAG_STRING,
  CVC3::CLFLAG_STRVEC
}
 Different types of command line flags. More...
 
enum  CVC3::CVC3CardinalityKind { CVC3::CARD_FINITE, CVC3::CARD_INFINITE, CVC3::CARD_UNKNOWN }
 
enum  CVC3::QueryResult {
  CVC3::SATISFIABLE, CVC3::INVALID, CVC3::VALID, CVC3::UNSATISFIABLE,
  CVC3::ABORT, CVC3::UNKNOWN
}
 
enum  CVC3::FormulaValue { CVC3::TRUE_VAL, CVC3::FALSE_VAL, CVC3::UNKNOWN_VAL }
 

Functions

std::string CVC3::int2string (int n)
 
std::ostream & CVC3::operator<< (std::ostream &out, CLFlagType clft)
 
std::ostream & CVC3::operator<< (std::ostream &out, CVC3CardinalityKind c)
 
bool CVC3::operator== (const Cardinality &c, CVC3CardinalityKind d)
 
bool CVC3::operator== (CVC3CardinalityKind d, const Cardinality &c)
 
bool CVC3::operator!= (const Cardinality &c, CVC3CardinalityKind d)
 
bool CVC3::operator!= (CVC3CardinalityKind d, const Cardinality &c)
 
bool CVC3::isArrayLiteral (const Expr &)
 
std::ostream & CVC3::operator<< (std::ostream &out, QueryResult qr)
 
std::string CVC3::QueryResultToString (QueryResult query_result)
 
std::ostream & CVC3::operator<< (std::ostream &out, FormulaValue fv)
 
int CVC3::compare (const Expr &e1, const Expr &e2)
 

Variables

const CVC4::Kind CVC3::EQ
 
const CVC4::Kind CVC3::LE
 
const CVC4::Kind CVC3::GE
 
const CVC4::Kind CVC3::DIVIDE
 
const CVC4::Kind CVC3::BVLT
 
const CVC4::Kind CVC3::BVLE
 
const CVC4::Kind CVC3::BVGT
 
const CVC4::Kind CVC3::BVGE
 
const CVC4::Kind CVC3::BVPLUS
 
const CVC4::Kind CVC3::BVSUB
 
const CVC4::Kind CVC3::BVCONST
 
const CVC4::Kind CVC3::EXTRACT
 
const CVC4::Kind CVC3::CONCAT
 

Detailed Description

CVC3 compatibility layer for CVC4.

** Original author: Morgan Deters
** Major contributors: none
** Minor contributors (to current version): Francois Bobot
** This file is part of the CVC4 project.
** Copyright (c) 2009-2013  New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.

CVC3 compatibility layer for CVC4. This version was derived from the following CVS revisions of the following files in CVC3. If those files have a later revision, then this file might be out of date. Note that this compatibility layer is not safe for use in multithreaded contexts where multiple threads are accessing this compatibility layer functionality.

src/include/vc.h 1.36 src/include/expr.h 1.39 src/include/command_line_flags.h 1.3 src/include/queryresult.h 1.2 src/include/formula_value.h 1.1

Definition in file cvc3_compat.h.

Macro Definition Documentation

#define __CVC4__CVC3_COMPAT_H

Definition at line 31 of file cvc3_compat.h.

#define _cvc3__command_line_flags_h_

Definition at line 47 of file cvc3_compat.h.

#define _cvc3__expr_h_

Definition at line 45 of file cvc3_compat.h.

#define _cvc3__include__formula_value_h_

Definition at line 49 of file cvc3_compat.h.

#define _cvc3__include__queryresult_h_

Definition at line 48 of file cvc3_compat.h.

#define _cvc3__include__vc_h_

Definition at line 46 of file cvc3_compat.h.

#define AST_LANG

Definition at line 466 of file cvc3_compat.h.

#define PRESENTATION_LANG

Definition at line 462 of file cvc3_compat.h.

#define SMTLIB_LANG

Definition at line 463 of file cvc3_compat.h.

#define SMTLIB_V2_LANG

Definition at line 464 of file cvc3_compat.h.

#define TPTP_LANG

Definition at line 465 of file cvc3_compat.h.