cvc4-1.4
|
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 |
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-2014 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.
#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 468 of file cvc3_compat.h.
#define PRESENTATION_LANG |
Definition at line 464 of file cvc3_compat.h.
#define SMTLIB_LANG |
Definition at line 465 of file cvc3_compat.h.
#define SMTLIB_V2_LANG |
Definition at line 466 of file cvc3_compat.h.
#define TPTP_LANG |
Definition at line 467 of file cvc3_compat.h.