diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-03-07 21:38:04 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-03-07 21:38:04 +0000 |
commit | a9288938b0244551b713bd3687a62a6aa0762b56 (patch) | |
tree | 3730f4c67351e66a37d5750db8217fc2b4e0c949 /src/compat | |
parent | c409b60e8c507997a24ba9ea1c611da9132d1e10 (diff) |
fix some Java compatibility-layer interface problems; also fix some Mac OS X build issues
Diffstat (limited to 'src/compat')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 26 | ||||
-rw-r--r-- | src/compat/cvc3_compat.h | 66 |
2 files changed, 86 insertions, 6 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 83c33c7ab..16169c10a 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -225,6 +225,10 @@ Expr::Expr(const Expr& e) : CVC4::Expr(e) { Expr::Expr(const CVC4::Expr& e) : CVC4::Expr(e) { } +Expr::Expr(const CVC4::Kind k) : CVC4::Expr() { + *this = getEM()->operatorOf(k); +} + Expr Expr::eqExpr(const Expr& right) const { return getEM()->mkExpr(CVC4::kind::EQUAL, *this, right); } @@ -321,6 +325,22 @@ bool Expr::isString() const { return false; } +bool Expr::isBoundVar() const { + Unimplemented(); +} + +bool Expr::isLambda() const { + Unimplemented(); +} + +bool Expr::isClosure() const { + Unimplemented(); +} + +bool Expr::isQuantifier() const { + Unimplemented(); +} + bool Expr::isApply() const { return hasOperator(); } @@ -404,7 +424,7 @@ std::vector< std::vector<Expr> > Expr::getTriggers() const { } ExprManager* Expr::getEM() const { - return getExprManager(); + return reinterpret_cast<ExprManager*>(getExprManager()); } std::vector<Expr> Expr::getKids() const { @@ -709,7 +729,7 @@ ValidityChecker::ValidityChecker() : d_clflags(new CLFlags()), d_options() { setUpOptions(d_options, *d_clflags); - d_em = new CVC4::ExprManager(d_options); + d_em = reinterpret_cast<ExprManager*>(new CVC4::ExprManager(d_options)); d_smt = new CVC4::SmtEngine(d_em); d_parserContext = CVC4::parser::ParserBuilder(d_em, "<internal>").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build(); } @@ -718,7 +738,7 @@ ValidityChecker::ValidityChecker(const CLFlags& clflags) : d_clflags(new CLFlags(clflags)), d_options() { setUpOptions(d_options, *d_clflags); - d_em = new CVC4::ExprManager(d_options); + d_em = reinterpret_cast<ExprManager*>(new CVC4::ExprManager(d_options)); d_smt = new CVC4::SmtEngine(d_em); d_parserContext = CVC4::parser::ParserBuilder(d_em, "<internal>").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build(); } diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h index beef53006..eae8412cf 100644 --- a/src/compat/cvc3_compat.h +++ b/src/compat/cvc3_compat.h @@ -82,6 +82,20 @@ namespace CVC3 { +const CVC4::Kind EQ = CVC4::kind::EQUAL; +const CVC4::Kind LE = CVC4::kind::LEQ; +const CVC4::Kind GE = CVC4::kind::GEQ; +const CVC4::Kind DIVIDE = CVC4::kind::DIVISION; +const CVC4::Kind BVLT = CVC4::kind::BITVECTOR_ULT; +const CVC4::Kind BVLE = CVC4::kind::BITVECTOR_ULE; +const CVC4::Kind BVGT = CVC4::kind::BITVECTOR_UGT; +const CVC4::Kind BVGE = CVC4::kind::BITVECTOR_UGE; +const CVC4::Kind BVPLUS = CVC4::kind::BITVECTOR_PLUS; +const CVC4::Kind BVSUB = CVC4::kind::BITVECTOR_SUB; +const CVC4::Kind BVCONST = CVC4::kind::CONST_BITVECTOR; +const CVC4::Kind EXTRACT = CVC4::kind::BITVECTOR_EXTRACT; +const CVC4::Kind CONCAT = CVC4::kind::BITVECTOR_CONCAT; + std::string int2string(int n); //! Different types of command line flags @@ -227,10 +241,11 @@ public: };/* class CLFlags */ +class ExprManager; class Context; class Proof {}; +class Theorem {}; -using CVC4::ExprManager; using CVC4::InputLanguage; using CVC4::Integer; using CVC4::Rational; @@ -318,6 +333,7 @@ public: Expr(); Expr(const Expr& e); Expr(const CVC4::Expr& e); + Expr(CVC4::Kind k); // Compound expression constructors Expr eqExpr(const Expr& right) const; @@ -348,12 +364,40 @@ public: bool isTrue() const; bool isBoolConst() const; bool isVar() const; + bool isBoundVar() const; bool isString() const; + bool isSymbol() const; + bool isTerm() const; + bool isType() const; + bool isClosure() const; + bool isQuantifier() const; + bool isForall() const; + bool isExists() const; + bool isLambda() const; bool isApply() const; bool isTheorem() const; bool isConstant() const; bool isRawList() const; + bool isAtomic() const; + bool isAtomicFormula() const; + bool isAbsAtomicFormula() const; + bool isLiteral() const; + bool isAbsLiteral() const; + bool isBoolConnective() const; + bool isPropLiteral() const; + bool isPropAtom() const; + + const std::string& getName() const; + const std::string& getUid() const; + + const std::string& getString() const; + const std::vector<Expr>& getVars() const; + const Expr& getExistential() const; + int getBoundIndex() const; + const Expr& getBody() const; + const Theorem& getTheorem() const; + bool isEq() const; bool isNot() const; bool isAnd() const; @@ -366,7 +410,7 @@ public: bool isRational() const; bool isSkolem() const; - Rational getRational() const; + const Rational& getRational() const; Op mkOp() const; Op getOp() const; @@ -407,8 +451,24 @@ public: //! Look up the current type. Do not recursively compute (i.e. may be NULL) Type lookupType() const; + //! Pretty-print the expression + void pprint() const; + //! Pretty-print without dagifying + void pprintnodag() const; + };/* class CVC3::Expr */ +bool isArrayLiteral(const Expr&); + +class ExprManager : public CVC4::ExprManager { +public: + const std::string& getKindName(int kind); + //! Get the input language for printing + InputLanguage getInputLang() const; + //! Get the output language for printing + InputLanguage getOutputLang() const; +};/* class CVC3::ExprManager */ + typedef CVC4::StatisticsRegistry Statistics; #define PRESENTATION_LANG ::CVC4::language::input::LANG_CVC4 @@ -464,7 +524,7 @@ class CVC4_PUBLIC ValidityChecker { CLFlags* d_clflags; CVC4::Options d_options; - CVC4::ExprManager* d_em; + CVC3::ExprManager* d_em; CVC4::SmtEngine* d_smt; CVC4::parser::Parser* d_parserContext; |