From c229389dbf99fa7a747a1bb713e41a3081b6d5fa Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 16 Sep 2011 21:30:27 +0000 Subject: [PATCH] some minor fixes to the cvc3 compatibility library and test case --- src/compat/cvc3_compat.cpp | 244 +++++++++++++++++++------------------ src/compat/cvc3_compat.h | 9 +- test/system/Makefile.am | 2 +- test/system/cvc3_main.cpp | 18 +-- 4 files changed, 140 insertions(+), 133 deletions(-) diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 99cf4e84b..766cc300d 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -381,7 +381,7 @@ CLFlag::CLFlag(const char* s, const std::string& help, bool display) : d_data.s = new string(s); } -CLFlag::CLFlag(const std::vector >& sv, +CLFlag::CLFlag(const std::vector >& sv, const std::string& help, bool display) : d_tp(CLFLAG_STRVEC) { d_data.sv = new vector >(sv); @@ -487,13 +487,13 @@ CLFlag& CLFlag::operator=(const char* s) { return *this; } -CLFlag& CLFlag::operator=(const std::pair& p) { +CLFlag& CLFlag::operator=(const std::pair& p) { CheckArgument(d_tp == CLFLAG_STRVEC, this); d_data.sv->push_back(p); return *this; } -CLFlag& CLFlag::operator=(const std::vector >& sv) { +CLFlag& CLFlag::operator=(const std::vector >& sv) { CheckArgument(d_tp == CLFLAG_STRVEC, this); *d_data.sv = sv; return *this; @@ -526,7 +526,7 @@ const std::string& CLFlag::getString() const { return *d_data.s; } -const std::vector >& CLFlag::getStrVec() const { +const std::vector >& CLFlag::getStrVec() const { CheckArgument(d_tp == CLFLAG_STRVEC, this); return *d_data.sv; } @@ -593,14 +593,14 @@ void CLFlags::setFlag(const std::string& name, const char* s) { (*i).second = s; } -void CLFlags::setFlag(const std::string& name, const std::pair& p) { +void CLFlags::setFlag(const std::string& name, const std::pair& p) { FlagMap::iterator i = d_map.find(name); CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); (*i).second = p; } void CLFlags::setFlag(const std::string& name, - const std::vector >& sv) { + const std::vector >& sv) { FlagMap::iterator i = d_map.find(name); CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); (*i).second = sv; @@ -608,14 +608,20 @@ void CLFlags::setFlag(const std::string& name, ValidityChecker::ValidityChecker() : d_clflags(new CLFlags()), - d_em(), - d_smt(&d_em) { + d_options() { + d_options.incrementalSolving = true; +#warning fixme other options from clflags ?? + d_em = new CVC4::ExprManager(d_options); + d_smt = new CVC4::SmtEngine(d_em); } ValidityChecker::ValidityChecker(const CLFlags& clflags) : d_clflags(new CLFlags(clflags)), - d_em(), - d_smt(&d_em) { + d_options() { + d_options.incrementalSolving = true; +#warning fixme other options from clflags ?? + d_em = new CVC4::ExprManager(d_options); + d_smt = new CVC4::SmtEngine(d_em); } ValidityChecker::~ValidityChecker() { @@ -864,15 +870,15 @@ ValidityChecker* ValidityChecker::create() { } Type ValidityChecker::boolType() { - return d_em.booleanType(); + return d_em->booleanType(); } Type ValidityChecker::realType() { - return d_em.realType(); + return d_em->realType(); } Type ValidityChecker::intType() { - return d_em.integerType(); + return d_em->integerType(); } Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) { @@ -887,7 +893,7 @@ Type ValidityChecker::tupleType(const Type& type0, const Type& type1) { vector types; types.push_back(type0); types.push_back(type1); - return d_em.mkTupleType(types); + return d_em->mkTupleType(types); } Type ValidityChecker::tupleType(const Type& type0, const Type& type1, const Type& type2) { @@ -895,13 +901,13 @@ Type ValidityChecker::tupleType(const Type& type0, const Type& type1, const Type types.push_back(type0); types.push_back(type1); types.push_back(type2); - return d_em.mkTupleType(types); + return d_em->mkTupleType(types); } Type ValidityChecker::tupleType(const std::vector& types) { const vector& v = *reinterpret_cast*>(&types); - return Type(d_em.mkTupleType(v)); + return Type(d_em->mkTupleType(v)); } Type ValidityChecker::recordType(const std::string& field, const Type& type) { @@ -947,26 +953,26 @@ void ValidityChecker::dataType(const std::vector& names, } Type ValidityChecker::arrayType(const Type& typeIndex, const Type& typeData) { - return d_em.mkArrayType(typeIndex, typeData); + return d_em->mkArrayType(typeIndex, typeData); } Type ValidityChecker::bitvecType(int n) { CheckArgument(n >= 0, n, "cannot construct a bitvector type of negative size"); - return d_em.mkBitVectorType(n); + return d_em->mkBitVectorType(n); } Type ValidityChecker::funType(const Type& typeDom, const Type& typeRan) { - return d_em.mkFunctionType(typeDom, typeRan); + return d_em->mkFunctionType(typeDom, typeRan); } Type ValidityChecker::funType(const std::vector& typeDom, const Type& typeRan) { const vector& dom = *reinterpret_cast*>(&typeDom); - return Type(d_em.mkFunctionType(dom, typeRan)); + return Type(d_em->mkFunctionType(dom, typeRan)); } Type ValidityChecker::createType(const std::string& typeName) { - return d_em.mkSort(typeName); + return d_em->mkSort(typeName); } Type ValidityChecker::createType(const std::string& typeName, const Type& def) { @@ -978,11 +984,11 @@ Type ValidityChecker::lookupType(const std::string& typeName) { } ExprManager* ValidityChecker::getEM() { - return &d_em; + return d_em; } Expr ValidityChecker::varExpr(const std::string& name, const Type& type) { - return d_em.mkVar(name, type); + return d_em->mkVar(name, type); } Expr ValidityChecker::varExpr(const std::string& name, const Type& type, @@ -995,16 +1001,16 @@ Expr ValidityChecker::lookupVar(const std::string& name, Type* type) { } Type ValidityChecker::getType(const Expr& e) { - return d_em.getType(e); + return d_em->getType(e); } Type ValidityChecker::getBaseType(const Expr& e) { - Type t = d_em.getType(e); - return t.isInteger() ? Type(d_em.realType()) : t; + Type t = d_em->getType(e); + return t.isInteger() ? Type(d_em->realType()) : t; } Type ValidityChecker::getBaseType(const Type& t) { - return t.isInteger() ? Type(d_em.realType()) : t; + return t.isInteger() ? Type(d_em->realType()) : t; } Expr ValidityChecker::getTypePred(const Type&t, const Expr& e) { @@ -1061,7 +1067,7 @@ void ValidityChecker::printExpr(const Expr& e) { void ValidityChecker::printExpr(const Expr& e, std::ostream& os) { Expr::setdepth::Scope sd(os, -1); Expr::printtypes::Scope pt(os, false); - Expr::setlanguage::Scope sl(os, d_em.getOptions()->outputLanguage); + Expr::setlanguage::Scope sl(os, d_em->getOptions()->outputLanguage); os << e; } @@ -1090,62 +1096,62 @@ Expr ValidityChecker::exprFromString(const std::string& e) { } Expr ValidityChecker::trueExpr() { - return d_em.mkConst(true); + return d_em->mkConst(true); } Expr ValidityChecker::falseExpr() { - return d_em.mkConst(false); + return d_em->mkConst(false); } Expr ValidityChecker::notExpr(const Expr& child) { - return d_em.mkExpr(CVC4::kind::NOT, child); + return d_em->mkExpr(CVC4::kind::NOT, child); } Expr ValidityChecker::andExpr(const Expr& left, const Expr& right) { - return d_em.mkExpr(CVC4::kind::AND, left, right); + return d_em->mkExpr(CVC4::kind::AND, left, right); } Expr ValidityChecker::andExpr(const std::vector& children) { const vector& v = *reinterpret_cast*>(&children); - return d_em.mkExpr(CVC4::kind::AND, v); + return d_em->mkExpr(CVC4::kind::AND, v); } Expr ValidityChecker::orExpr(const Expr& left, const Expr& right) { - return d_em.mkExpr(CVC4::kind::OR, left, right); + return d_em->mkExpr(CVC4::kind::OR, left, right); } Expr ValidityChecker::orExpr(const std::vector& children) { const vector& v = *reinterpret_cast*>(&children); - return d_em.mkExpr(CVC4::kind::OR, v); + return d_em->mkExpr(CVC4::kind::OR, v); } Expr ValidityChecker::impliesExpr(const Expr& hyp, const Expr& conc) { - return d_em.mkExpr(CVC4::kind::IMPLIES, hyp, conc); + return d_em->mkExpr(CVC4::kind::IMPLIES, hyp, conc); } Expr ValidityChecker::iffExpr(const Expr& left, const Expr& right) { - return d_em.mkExpr(CVC4::kind::IFF, left, right); + return d_em->mkExpr(CVC4::kind::IFF, left, right); } Expr ValidityChecker::eqExpr(const Expr& child0, const Expr& child1) { - return d_em.mkExpr(CVC4::kind::EQUAL, child0, child1); + return d_em->mkExpr(CVC4::kind::EQUAL, child0, child1); } Expr ValidityChecker::iteExpr(const Expr& ifpart, const Expr& thenpart, const Expr& elsepart) { - return d_em.mkExpr(CVC4::kind::ITE, ifpart, thenpart, elsepart); + return d_em->mkExpr(CVC4::kind::ITE, ifpart, thenpart, elsepart); } Expr ValidityChecker::distinctExpr(const std::vector& children) { const vector& v = *reinterpret_cast*>(&children); - return d_em.mkExpr(CVC4::kind::DISTINCT, v); + return d_em->mkExpr(CVC4::kind::DISTINCT, v); } Op ValidityChecker::createOp(const std::string& name, const Type& type) { - return d_em.mkVar(name, type); + return d_em->mkVar(name, type); } Op ValidityChecker::createOp(const std::string& name, const Type& type, @@ -1158,23 +1164,23 @@ Op ValidityChecker::lookupOp(const std::string& name, Type* type) { } Expr ValidityChecker::funExpr(const Op& op, const Expr& child) { - return d_em.mkExpr(CVC4::kind::APPLY_UF, op, child); + return d_em->mkExpr(CVC4::kind::APPLY_UF, op, child); } Expr ValidityChecker::funExpr(const Op& op, const Expr& left, const Expr& right) { - return d_em.mkExpr(CVC4::kind::APPLY_UF, op, left, right); + return d_em->mkExpr(CVC4::kind::APPLY_UF, op, left, right); } Expr ValidityChecker::funExpr(const Op& op, const Expr& child0, const Expr& child1, const Expr& child2) { - return d_em.mkExpr(CVC4::kind::APPLY_UF, op, child0, child1, child2); + return d_em->mkExpr(CVC4::kind::APPLY_UF, op, child0, child1, child2); } Expr ValidityChecker::funExpr(const Op& op, const std::vector& children) { vector opkids; opkids.push_back(op); opkids.insert(opkids.end(), children.begin(), children.end()); - return d_em.mkExpr(CVC4::kind::APPLY_UF, opkids); + return d_em->mkExpr(CVC4::kind::APPLY_UF, opkids); } bool ValidityChecker::addPairToArithOrder(const Expr& smaller, const Expr& bigger) { @@ -1182,62 +1188,62 @@ bool ValidityChecker::addPairToArithOrder(const Expr& smaller, const Expr& bigge } Expr ValidityChecker::ratExpr(int n, int d) { - return d_em.mkConst(Rational(n, d)); + return d_em->mkConst(Rational(n, d)); } Expr ValidityChecker::ratExpr(const std::string& n, const std::string& d, int base) { - return d_em.mkConst(Rational(n + '/' + d, base)); + return d_em->mkConst(Rational(n + '/' + d, base)); } Expr ValidityChecker::ratExpr(const std::string& n, int base) { - return d_em.mkConst(Rational(n, base)); + return d_em->mkConst(Rational(n, base)); } Expr ValidityChecker::uminusExpr(const Expr& child) { - return d_em.mkExpr(CVC4::kind::UMINUS, child); + return d_em->mkExpr(CVC4::kind::UMINUS, child); } Expr ValidityChecker::plusExpr(const Expr& left, const Expr& right) { - return d_em.mkExpr(CVC4::kind::PLUS, left, right); + return d_em->mkExpr(CVC4::kind::PLUS, left, right); } Expr ValidityChecker::plusExpr(const std::vector& children) { const vector& v = *reinterpret_cast*>(&children); - return d_em.mkExpr(CVC4::kind::PLUS, v); + return d_em->mkExpr(CVC4::kind::PLUS, v); } Expr ValidityChecker::minusExpr(const Expr& left, const Expr& right) { - return d_em.mkExpr(CVC4::kind::MINUS, left, right); + return d_em->mkExpr(CVC4::kind::MINUS, left, right); } Expr ValidityChecker::multExpr(const Expr& left, const Expr& right) { - return d_em.mkExpr(CVC4::kind::MULT, left, right); + return d_em->mkExpr(CVC4::kind::MULT, left, right); } Expr ValidityChecker::powExpr(const Expr& x, const Expr& n) { - return d_em.mkExpr(CVC4::kind::POW, x, n); + return d_em->mkExpr(CVC4::kind::POW, x, n); } Expr ValidityChecker::divideExpr(const Expr& numerator, const Expr& denominator) { - return d_em.mkExpr(CVC4::kind::DIVISION, numerator, denominator); + return d_em->mkExpr(CVC4::kind::DIVISION, numerator, denominator); } Expr ValidityChecker::ltExpr(const Expr& left, const Expr& right) { - return d_em.mkExpr(CVC4::kind::LT, left, right); + return d_em->mkExpr(CVC4::kind::LT, left, right); } Expr ValidityChecker::leExpr(const Expr& left, const Expr& right) { - return d_em.mkExpr(CVC4::kind::LEQ, left, right); + return d_em->mkExpr(CVC4::kind::LEQ, left, right); } Expr ValidityChecker::gtExpr(const Expr& left, const Expr& right) { - return d_em.mkExpr(CVC4::kind::GT, left, right); + return d_em->mkExpr(CVC4::kind::GT, left, right); } Expr ValidityChecker::geExpr(const Expr& left, const Expr& right) { - return d_em.mkExpr(CVC4::kind::GEQ, left, right); + return d_em->mkExpr(CVC4::kind::GEQ, left, right); } Expr ValidityChecker::recordExpr(const std::string& field, const Expr& expr) { @@ -1270,16 +1276,16 @@ Expr ValidityChecker::recUpdateExpr(const Expr& record, const std::string& field } Expr ValidityChecker::readExpr(const Expr& array, const Expr& index) { - return d_em.mkExpr(CVC4::kind::SELECT, array, index); + return d_em->mkExpr(CVC4::kind::SELECT, array, index); } Expr ValidityChecker::writeExpr(const Expr& array, const Expr& index, const Expr& newValue) { - return d_em.mkExpr(CVC4::kind::STORE, array, index, newValue); + return d_em->mkExpr(CVC4::kind::STORE, array, index, newValue); } Expr ValidityChecker::newBVConstExpr(const std::string& s, int base) { - return d_em.mkConst(CVC4::BitVector(s, base)); + return d_em->mkConst(CVC4::BitVector(s, base)); } Expr ValidityChecker::newBVConstExpr(const std::vector& bits) { @@ -1288,7 +1294,7 @@ Expr ValidityChecker::newBVConstExpr(const std::vector& bits) { value *= 2; value += *i ? 1 : 0; } - return d_em.mkConst(CVC4::BitVector(bits.size(), value)); + return d_em->mkConst(CVC4::BitVector(bits.size(), value)); } Expr ValidityChecker::newBVConstExpr(const Rational& r, int len) { @@ -1321,13 +1327,13 @@ Expr ValidityChecker::newBVConstExpr(const Rational& r, int len) { Expr ValidityChecker::newConcatExpr(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only concat a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only concat a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_CONCAT, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_CONCAT, t1, t2); } Expr ValidityChecker::newConcatExpr(const std::vector& kids) { const vector& v = *reinterpret_cast*>(&kids); - return d_em.mkExpr(CVC4::kind::BITVECTOR_CONCAT, v); + return d_em->mkExpr(CVC4::kind::BITVECTOR_CONCAT, v); } Expr ValidityChecker::newBVExtractExpr(const Expr& e, int hi, int low) { @@ -1335,20 +1341,20 @@ Expr ValidityChecker::newBVExtractExpr(const Expr& e, int hi, int low) { CheckArgument(hi >= low, hi, "extraction [%d:%d] is bad; possibly inverted?", hi, low); CheckArgument(low >= 0, low, "extraction [%d:%d] is bad (negative)", hi, low); CheckArgument(CVC4::BitVectorType(e.getType()).getSize() > unsigned(hi), hi, "bitvector is of size %u, extraction [%d:%d] is off-the-end", CVC4::BitVectorType(e.getType()).getSize(), hi, low); - return d_em.mkExpr(CVC4::kind::BITVECTOR_EXTRACT, - d_em.mkConst(CVC4::BitVectorExtract(hi, low)), e); + return d_em->mkExpr(CVC4::kind::BITVECTOR_EXTRACT, + d_em->mkConst(CVC4::BitVectorExtract(hi, low)), e); } Expr ValidityChecker::newBVNegExpr(const Expr& t1) { // CVC3's BVNEG => SMT-LIBv2 bvnot CheckArgument(t1.getType().isBitVector(), t1, "can only bvneg a bitvector, not a `%s'", t1.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_NOT, t1); + return d_em->mkExpr(CVC4::kind::BITVECTOR_NOT, t1); } Expr ValidityChecker::newBVAndExpr(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only bvand a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only bvand a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_AND, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_AND, t1, t2); } Expr ValidityChecker::newBVAndExpr(const std::vector& kids) { @@ -1359,7 +1365,7 @@ Expr ValidityChecker::newBVAndExpr(const std::vector& kids) { Expr ValidityChecker::newBVOrExpr(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only bvor a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only bvor a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_OR, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_OR, t1, t2); } Expr ValidityChecker::newBVOrExpr(const std::vector& kids) { @@ -1370,7 +1376,7 @@ Expr ValidityChecker::newBVOrExpr(const std::vector& kids) { Expr ValidityChecker::newBVXorExpr(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only bvxor a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only bvxor a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_XOR, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_XOR, t1, t2); } Expr ValidityChecker::newBVXorExpr(const std::vector& kids) { @@ -1381,7 +1387,7 @@ Expr ValidityChecker::newBVXorExpr(const std::vector& kids) { Expr ValidityChecker::newBVXnorExpr(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only bvxnor a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only bvxnor a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_XNOR, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_XNOR, t1, t2); } Expr ValidityChecker::newBVXnorExpr(const std::vector& kids) { @@ -1392,63 +1398,63 @@ Expr ValidityChecker::newBVXnorExpr(const std::vector& kids) { Expr ValidityChecker::newBVNandExpr(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only bvnand a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only bvnand a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_NAND, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_NAND, t1, t2); } Expr ValidityChecker::newBVNorExpr(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only bvnor a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only bvnor a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_NOR, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_NOR, t1, t2); } Expr ValidityChecker::newBVCompExpr(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only bvcomp a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only bvcomp a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_COMP, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_COMP, t1, t2); } Expr ValidityChecker::newBVLTExpr(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only bvlt a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only bvlt a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_ULT, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_ULT, t1, t2); } Expr ValidityChecker::newBVLEExpr(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only bvle a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only bvle a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_ULE, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_ULE, t1, t2); } Expr ValidityChecker::newBVSLTExpr(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only bvslt a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only bvslt a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_SLT, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_SLT, t1, t2); } Expr ValidityChecker::newBVSLEExpr(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only bvsle a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only bvsle a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_SLE, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_SLE, t1, t2); } Expr ValidityChecker::newSXExpr(const Expr& t1, int len) { CheckArgument(t1.getType().isBitVector(), t1, "can only sx a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(len >= 0, len, "must sx by a positive integer"); CheckArgument(unsigned(len) >= CVC4::BitVectorType(t1.getType()).getSize(), len, "cannot sx by something smaller than the bitvector (%d < %u)", len, CVC4::BitVectorType(t1.getType()).getSize()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_SIGN_EXTEND, - d_em.mkConst(CVC4::BitVectorSignExtend(len)), t1); + return d_em->mkExpr(CVC4::kind::BITVECTOR_SIGN_EXTEND, + d_em->mkConst(CVC4::BitVectorSignExtend(len)), t1); } Expr ValidityChecker::newBVUminusExpr(const Expr& t1) { // CVC3's BVUMINUS => SMT-LIBv2 bvneg CheckArgument(t1.getType().isBitVector(), t1, "can only bvuminus a bitvector, not a `%s'", t1.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_NEG, t1); + return d_em->mkExpr(CVC4::kind::BITVECTOR_NEG, t1); } Expr ValidityChecker::newBVSubExpr(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only bvsub a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only bvsub by a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_SUB, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_SUB, t1, t2); } Expr ValidityChecker::newBVPlusExpr(int numbits, const std::vector& k) { @@ -1459,7 +1465,7 @@ Expr ValidityChecker::newBVPlusExpr(int numbits, const std::vector& k) { Expr ValidityChecker::newBVPlusExpr(int numbits, const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only bvplus a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only bvplus a bitvector, not a `%s'", t2.getType().toString().c_str()); - Expr e = d_em.mkExpr(CVC4::kind::BITVECTOR_PLUS, t1, t2); + Expr e = d_em->mkExpr(CVC4::kind::BITVECTOR_PLUS, t1, t2); unsigned size = CVC4::BitVectorType(e.getType()).getSize(); CheckArgument(numbits > 0, numbits, "argument must be positive integer, not %u", numbits); @@ -1472,7 +1478,7 @@ Expr ValidityChecker::newBVPlusExpr(int numbits, const Expr& t1, const Expr& t2) Expr ValidityChecker::newBVMultExpr(int numbits, const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only bvmult a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only bvmult by a bitvector, not a `%s'", t2.getType().toString().c_str()); - Expr e = d_em.mkExpr(CVC4::kind::BITVECTOR_MULT, t1, t2); + Expr e = d_em->mkExpr(CVC4::kind::BITVECTOR_MULT, t1, t2); unsigned size = CVC4::BitVectorType(e.getType()).getSize(); CheckArgument(numbits > 0, numbits, "argument must be positive integer, not %u", numbits); @@ -1485,31 +1491,31 @@ Expr ValidityChecker::newBVMultExpr(int numbits, const Expr& t1, const Expr& t2) Expr ValidityChecker::newBVUDivExpr(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only bvudiv a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only bvudiv by a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_UDIV, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_UDIV, t1, t2); } Expr ValidityChecker::newBVURemExpr(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only bvurem a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only bvurem by a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_UREM, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_UREM, t1, t2); } Expr ValidityChecker::newBVSDivExpr(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only bvsdiv a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only bvsdiv by a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_SDIV, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_SDIV, t1, t2); } Expr ValidityChecker::newBVSRemExpr(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only bvsrem a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only bvsrem by a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_SREM, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_SREM, t1, t2); } Expr ValidityChecker::newBVSModExpr(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only bvsmod a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only bvsmod by a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_SMOD, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_SMOD, t1, t2); } Expr ValidityChecker::newFixedLeftShiftExpr(const Expr& t1, int r) { @@ -1517,14 +1523,14 @@ Expr ValidityChecker::newFixedLeftShiftExpr(const Expr& t1, int r) { CheckArgument(r >= 0, r, "left shift amount must be >= 0 (you passed %d)", r); // Defined in: // http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit - return d_em.mkExpr(CVC4::kind::BITVECTOR_CONCAT, t1, d_em.mkConst(CVC4::BitVector(r))); + return d_em->mkExpr(CVC4::kind::BITVECTOR_CONCAT, t1, d_em->mkConst(CVC4::BitVector(r))); } Expr ValidityChecker::newFixedConstWidthLeftShiftExpr(const Expr& t1, int r) { CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(r >= 0, r, "const-width left shift amount must be >= 0 (you passed %d)", r); // just turn it into a BVSHL - return d_em.mkExpr(CVC4::kind::BITVECTOR_SHL, t1, d_em.mkConst(CVC4::BitVector(CVC4::BitVectorType(t1.getType()).getSize(), unsigned(r)))); + return d_em->mkExpr(CVC4::kind::BITVECTOR_SHL, t1, d_em->mkConst(CVC4::BitVector(CVC4::BitVectorType(t1.getType()).getSize(), unsigned(r)))); } Expr ValidityChecker::newFixedRightShiftExpr(const Expr& t1, int r) { @@ -1533,25 +1539,25 @@ Expr ValidityChecker::newFixedRightShiftExpr(const Expr& t1, int r) { // Defined in: // http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit // Should be equivalent to a BVLSHR; just turn it into that. - return d_em.mkExpr(CVC4::kind::BITVECTOR_LSHR, t1, d_em.mkConst(CVC4::BitVector(CVC4::BitVectorType(t1.getType()).getSize(), unsigned(r)))); + return d_em->mkExpr(CVC4::kind::BITVECTOR_LSHR, t1, d_em->mkConst(CVC4::BitVector(CVC4::BitVectorType(t1.getType()).getSize(), unsigned(r)))); } Expr ValidityChecker::newBVSHL(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_SHL, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_SHL, t1, t2); } Expr ValidityChecker::newBVLSHR(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_LSHR, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_LSHR, t1, t2); } Expr ValidityChecker::newBVASHR(const Expr& t1, const Expr& t2) { CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); - return d_em.mkExpr(CVC4::kind::BITVECTOR_ASHR, t1, t2); + return d_em->mkExpr(CVC4::kind::BITVECTOR_ASHR, t1, t2); } Rational ValidityChecker::computeBVConst(const Expr& e) { @@ -1561,7 +1567,7 @@ Rational ValidityChecker::computeBVConst(const Expr& e) { Expr ValidityChecker::tupleExpr(const std::vector& exprs) { const vector& v = *reinterpret_cast*>(&exprs); - return d_em.mkExpr(CVC4::kind::TUPLE, v); + return d_em->mkExpr(CVC4::kind::TUPLE, v); } Expr ValidityChecker::tupleSelectExpr(const Expr& tuple, int index) { @@ -1652,7 +1658,7 @@ void ValidityChecker::setTimeLimit(unsigned limit) { } void ValidityChecker::assertFormula(const Expr& e) { - d_smt.assertFormula(CVC4::BoolExpr(e)); + d_smt->assertFormula(CVC4::BoolExpr(e)); } void ValidityChecker::registerAtom(const Expr& e) { @@ -1664,7 +1670,7 @@ Expr ValidityChecker::getImpliedLiteral() { } Expr ValidityChecker::simplify(const Expr& e) { - return d_smt.simplify(e); + return d_smt->simplify(e); } static QueryResult cvc4resultToCvc3result(CVC4::Result r) { @@ -1688,11 +1694,11 @@ static QueryResult cvc4resultToCvc3result(CVC4::Result r) { } QueryResult ValidityChecker::query(const Expr& e) { - return cvc4resultToCvc3result(d_smt.query(CVC4::BoolExpr(e))); + return cvc4resultToCvc3result(d_smt->query(CVC4::BoolExpr(e))); } QueryResult ValidityChecker::checkUnsat(const Expr& e) { - return cvc4resultToCvc3result(d_smt.checkSat(CVC4::BoolExpr(e))); + return cvc4resultToCvc3result(d_smt->checkSat(CVC4::BoolExpr(e))); } QueryResult ValidityChecker::checkContinue() { @@ -1709,7 +1715,7 @@ void ValidityChecker::returnFromCheck() { void ValidityChecker::getUserAssumptions(std::vector& assumptions) { CheckArgument(assumptions.empty(), assumptions, "assumptions arg must be empty"); - vector v = d_smt.getAssertions(); + vector v = d_smt->getAssertions(); assumptions.swap(*reinterpret_cast*>(&v)); } @@ -1743,8 +1749,8 @@ QueryResult ValidityChecker::tryModelGeneration() { } FormulaValue ValidityChecker::value(const Expr& e) { - CheckArgument(e.getType() == d_em.booleanType(), e, "argument must be a formula"); - return d_smt.getValue(e).getConst() ? TRUE_VAL : FALSE_VAL; + CheckArgument(e.getType() == d_em->booleanType(), e, "argument must be a formula"); + return d_smt->getValue(e).getConst() ? TRUE_VAL : FALSE_VAL; } bool ValidityChecker::inconsistent(std::vector& assumptions) { @@ -1788,25 +1794,25 @@ Proof ValidityChecker::getProofClosure() { } int ValidityChecker::stackLevel() { - return d_smt.getStackLevel(); + return d_smt->getStackLevel(); } void ValidityChecker::push() { - d_smt.push(); + d_smt->push(); } void ValidityChecker::pop() { - d_smt.pop(); + d_smt->pop(); } void ValidityChecker::popto(int stackLevel) { CheckArgument(stackLevel >= 0, stackLevel, "Cannot pop to a negative stack level %u", stackLevel); - CheckArgument(unsigned(stackLevel) <= d_smt.getStackLevel(), stackLevel, + CheckArgument(unsigned(stackLevel) <= d_smt->getStackLevel(), stackLevel, "Cannot pop to a level higher than the current one! " "At level %u, user requested level %d", - d_smt.getStackLevel(), stackLevel); - while(unsigned(stackLevel) < d_smt.getStackLevel()) { + d_smt->getStackLevel(), stackLevel); + while(unsigned(stackLevel) < d_smt->getStackLevel()) { pop(); } } @@ -1839,12 +1845,12 @@ void ValidityChecker::logAnnotation(const Expr& annot) { Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); } -static void doCommands(CVC4::parser::Parser* parser, CVC4::SmtEngine& smt, CVC4::Options& opts) { +static void doCommands(CVC4::parser::Parser* parser, CVC4::SmtEngine* smt, CVC4::Options& opts) { while(CVC4::Command* cmd = parser->nextCommand()) { if(opts.verbosity >= 0) { - cmd->invoke(&smt, *opts.out); + cmd->invoke(smt, *opts.out); } else { - cmd->invoke(&smt); + cmd->invoke(smt); } delete cmd; } @@ -1854,10 +1860,10 @@ void ValidityChecker::loadFile(const std::string& fileName, InputLanguage lang, bool interactive, bool calledFromParser) { - CVC4::Options opts = *d_em.getOptions(); + CVC4::Options opts = *d_em->getOptions(); opts.inputLanguage = lang; opts.interactive = interactive; - CVC4::parser::ParserBuilder parserBuilder(&d_em, fileName, opts); + CVC4::parser::ParserBuilder parserBuilder(d_em, fileName, opts); CVC4::parser::Parser* parser = parserBuilder.build(); doCommands(parser, d_smt, opts); delete parser; @@ -1866,21 +1872,21 @@ void ValidityChecker::loadFile(const std::string& fileName, void ValidityChecker::loadFile(std::istream& is, InputLanguage lang, bool interactive) { - CVC4::Options opts = *d_em.getOptions(); + CVC4::Options opts = *d_em->getOptions(); opts.inputLanguage = lang; opts.interactive = interactive; - CVC4::parser::ParserBuilder parserBuilder(&d_em, "[stream]", opts); + CVC4::parser::ParserBuilder parserBuilder(d_em, "[stream]", opts); CVC4::parser::Parser* parser = parserBuilder.withStreamInput(is).build(); doCommands(parser, d_smt, opts); delete parser; } Statistics& ValidityChecker::getStatistics() { - return *d_smt.getStatisticsRegistry(); + return *d_smt->getStatisticsRegistry(); } void ValidityChecker::printStatistics() { - Message() << d_smt.getStatisticsRegistry(); + Message() << d_smt->getStatisticsRegistry(); } }/* CVC3 namespace */ diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h index 36c5c0f6a..fbb54a46c 100644 --- a/src/compat/cvc3_compat.h +++ b/src/compat/cvc3_compat.h @@ -66,13 +66,13 @@ // some #defines that CVC3 exported to userspace :( #ifdef CVC4_DEBUG -# define DebugAssert(cond, ...) Assert(cond, "CVC3-style assertion failed"); +# define DebugAssert(cond, str) Assert((cond), "CVC3-style assertion failed: %s", std::string(str).c_str()); # define IF_DEBUG(x) x #else # define DebugAssert(...) # define IF_DEBUG(x) #endif -#define FatalAssert(cond, ...) AlwaysAssert(cond, "CVC3-style assertion failed"); +#define FatalAssert(cond, str) AlwaysAssert((cond), "CVC3-style assertion failed: %s", std::string(str).c_str()); //class CInterface; @@ -443,8 +443,9 @@ std::ostream& operator<<(std::ostream& out, FormulaValue fv); class CVC4_PUBLIC ValidityChecker { CLFlags* d_clflags; - CVC4::ExprManager d_em; - CVC4::SmtEngine d_smt; + CVC4::Options d_options; + CVC4::ExprManager* d_em; + CVC4::SmtEngine* d_smt; ValidityChecker(const CLFlags& clflags); diff --git a/test/system/Makefile.am b/test/system/Makefile.am index 66e2bd251..4f0fcea14 100644 --- a/test/system/Makefile.am +++ b/test/system/Makefile.am @@ -2,7 +2,7 @@ TESTS_ENVIRONMENT = TESTS = \ boilerplate \ ouroborous -# cvc3_main.cpp +# cvc3_main # Things that aren't tests but that tests rely on and need to # go into the distribution diff --git a/test/system/cvc3_main.cpp b/test/system/cvc3_main.cpp index f72472acc..ecf664923 100644 --- a/test/system/cvc3_main.cpp +++ b/test/system/cvc3_main.cpp @@ -52,7 +52,7 @@ int exitStatus; // Check whether e is valid -bool check(ValidityChecker* vc, Expr e, bool verbose=true) +bool check(ValidityChecker* vc, Expr e, bool verbose=false) { if(verbose) { cout << "Query: "; @@ -2090,12 +2090,12 @@ int main(int argc, char** argv) cout << "Running API test, regress level = " << regressLevel << endl; exitStatus = 0; try { - cout << "\n}\ntest26(): {" << endl; - test26(); - cout << "\ntest(): {" << endl; - test(); - cout << "\n}\ntest1(): {" << endl; - test1(); + //cout << "\n}\ntest26(): {" << endl; + //test26(); + //cout << "\ntest(): {" << endl; + //test(); + //cout << "\n}\ntest1(): {" << endl; + //test1(); cout << "\n}\n\ntest2(): {" << endl; test2(); cout << "\n}\n\ntest3(): {" << endl; @@ -2106,8 +2106,8 @@ int main(int argc, char** argv) cout << "\n}\n\ntest5(): {" << endl; test5(); } - cout << "\n}\n\ntest6(): {" << endl; - test6(); + //cout << "\n}\n\ntest6(): {" << endl; + //test6(); cout << "\n}\n\ntest7(): {" << endl; test7(); cout << "\n}\n\ntest8(): {" << endl; -- 2.30.2