From: Morgan Deters Date: Tue, 28 Aug 2012 01:10:16 +0000 (+0000) Subject: Improved compatibility layer, now supports quantifiers. Also incorporates X-Git-Tag: cvc5-1.0.0~7838 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cf287f593931a1c4fc141e18845b4c5d36879889;p=cvc5.git Improved compatibility layer, now supports quantifiers. Also incorporates numerous bugfixes, and the cvc3 system test is enabled. --- diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 62885f55f..96cef406f 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -45,6 +45,11 @@ using namespace std; namespace CVC3 { +// Connects ExprManagers to ValidityCheckers. Needed to clean up the +// emmcs on ValidityChecker destruction (which are used for +// ExprManager-to-ExprManager import). +static std::map s_validityCheckers; + static std::hash_map s_typeToExpr; static std::hash_map s_exprToType; @@ -174,6 +179,7 @@ Expr Type::getExpr() const { Expr e = getExprManager()->mkVar("compatibility-layer-expr-type", *this); s_typeToExpr[*this] = e; s_exprToType[e] = *this; + s_validityCheckers[e.getExprManager()]->d_exprTypeMapRemove.push_back(e); return e; } @@ -198,7 +204,7 @@ Cardinality Type::card() const { } Expr Type::enumerateFinite(Unsigned n) const { - Unimplemented(); + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); } Unsigned Type::sizeFinite() const { @@ -326,7 +332,7 @@ bool Expr::isVar() const { } bool Expr::isString() const { - return false; + return getType().isString(); } bool Expr::isBoundVar() const { @@ -334,15 +340,16 @@ bool Expr::isBoundVar() const { } bool Expr::isLambda() const { - Unimplemented(); + // when implemented, also fix isClosure() below + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); } bool Expr::isClosure() const { - Unimplemented(); + return isQuantifier(); } bool Expr::isQuantifier() const { - Unimplemented(); + return getKind() == CVC4::kind::FORALL || getKind() == CVC4::kind::EXISTS; } bool Expr::isApply() const { @@ -424,7 +431,22 @@ Expr Expr::getExpr() const { } std::vector< std::vector > Expr::getTriggers() const { - return vector< vector >(); + CheckArgument(isClosure(), *this, __PRETTY_FUNCTION__, "getTriggers() called on non-closure expr"); + if(getNumChildren() < 3) { + // no triggers for this quantifier + return vector< vector >(); + } else { + // get the triggers from the third child + Expr triggers = (*this)[2]; + vector< vector > v; + for(const_iterator i = triggers.begin(); i != triggers.end(); ++i) { + v.push_back(vector()); + for(const_iterator j = (*i).begin(); j != (*i).end(); ++j) { + v.back().push_back(*j); + } + } + return v; + } } ExprManager* Expr::getEM() const { @@ -711,12 +733,14 @@ void CLFlags::setFlag(const std::string& name, void ValidityChecker::setUpOptions(CVC4::Options& options, const CLFlags& clflags) { // always incremental and model-producing in CVC3 compatibility mode + // also incrementally-simplifying and interactive d_smt->setOption("incremental", string("true")); d_smt->setOption("produce-models", string("true")); + d_smt->setOption("simplification-mode", string("incremental")); + d_smt->setOption("interactive-mode", string("true"));// support SmtEngine::getAssertions() d_smt->setOption("statistics", string(clflags["stats"].getBool() ? "true" : "false")); d_smt->setOption("random-seed", int2string(clflags["seed"].getInt())); - d_smt->setOption("interactive-mode", string(clflags["interactive"].getBool() ? "true" : "false")); d_smt->setOption("parse-only", string(clflags["parse-only"].getBool() ? "true" : "false")); d_smt->setOption("input-language", clflags["lang"].getString()); if(clflags["output-lang"].getString() == "") { @@ -730,24 +754,54 @@ void ValidityChecker::setUpOptions(CVC4::Options& options, const CLFlags& clflag ValidityChecker::ValidityChecker() : d_clflags(new CLFlags()), - d_options() { - setUpOptions(d_options, *d_clflags); + d_options(), + d_em(NULL), + d_emmc(), + d_reverseEmmc(), + d_smt(NULL), + d_parserContext(NULL), + d_exprTypeMapRemove(), + d_constructors(), + d_selectors() { d_em = reinterpret_cast(new CVC4::ExprManager(d_options)); + s_validityCheckers[d_em] = this; d_smt = new CVC4::SmtEngine(d_em); + setUpOptions(d_options, *d_clflags); d_parserContext = CVC4::parser::ParserBuilder(d_em, "").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build(); } ValidityChecker::ValidityChecker(const CLFlags& clflags) : d_clflags(new CLFlags(clflags)), - d_options() { - setUpOptions(d_options, *d_clflags); + d_options(), + d_em(NULL), + d_emmc(), + d_reverseEmmc(), + d_smt(NULL), + d_parserContext(NULL), + d_exprTypeMapRemove(), + d_constructors(), + d_selectors() { d_em = reinterpret_cast(new CVC4::ExprManager(d_options)); + s_validityCheckers[d_em] = this; d_smt = new CVC4::SmtEngine(d_em); + setUpOptions(d_options, *d_clflags); d_parserContext = CVC4::parser::ParserBuilder(d_em, "").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build(); } ValidityChecker::~ValidityChecker() { + for(vector::iterator i = d_exprTypeMapRemove.begin(); i != d_exprTypeMapRemove.end(); ++i) { + s_typeToExpr.erase(s_exprToType[*i]); + s_exprToType.erase(*i); + } delete d_parserContext; + delete d_smt; + d_emmc.clear(); + for(set::iterator i = d_reverseEmmc.begin(); i != d_reverseEmmc.end(); ++i) { + (*i)->d_emmc.erase(d_em); + } + d_reverseEmmc.clear(); + s_validityCheckers.erase(d_em); + delete d_em; delete d_clflags; } @@ -1067,7 +1121,7 @@ Type ValidityChecker::dataType(const std::string& name, const std::string& constructor, const std::vector& selectors, const std::vector& types) { - AlwaysAssert(selectors.size() == types.size()); + CheckArgument(selectors.size() == types.size(), types, "expected selectors and types vectors to be of equal length"); vector cv; vector< vector > sv; vector< vector > tv; @@ -1081,8 +1135,8 @@ Type ValidityChecker::dataType(const std::string& name, const std::vector& constructors, const std::vector >& selectors, const std::vector >& types) { - AlwaysAssert(constructors.size() == selectors.size()); - AlwaysAssert(constructors.size() == types.size()); + CheckArgument(constructors.size() == selectors.size(), selectors, "expected constructors and selectors vectors to be of equal length"); + CheckArgument(constructors.size() == types.size(), types, "expected constructors and types vectors to be of equal length"); vector nv; vector< vector > cv; vector< vector< vector > > sv; @@ -1103,19 +1157,19 @@ void ValidityChecker::dataType(const std::vector& names, const std::vector > >& types, std::vector& returnTypes) { - AlwaysAssert(names.size() == constructors.size()); - AlwaysAssert(names.size() == selectors.size()); - AlwaysAssert(names.size() == types.size()); + CheckArgument(names.size() == constructors.size(), constructors, "expected names and constructors vectors to be of equal length"); + CheckArgument(names.size() == selectors.size(), selectors, "expected names and selectors vectors to be of equal length"); + CheckArgument(names.size() == types.size(), types, "expected names and types vectors to be of equal length"); vector dv; // Set up the datatype specifications. for(unsigned i = 0; i < names.size(); ++i) { CVC4::Datatype dt(names[i]); - AlwaysAssert(constructors[i].size() == selectors[i].size()); - AlwaysAssert(constructors[i].size() == types[i].size()); + CheckArgument(constructors[i].size() == selectors[i].size(), "expected sub-vectors in constructors and selectors vectors to match in size"); + CheckArgument(constructors[i].size() == types[i].size(), "expected sub-vectors in constructors and types vectors to match in size"); for(unsigned j = 0; j < constructors[i].size(); ++j) { CVC4::DatatypeConstructor ctor(constructors[i][j]); - AlwaysAssert(selectors[i][j].size() == types[i][j].size()); + CheckArgument(selectors[i][j].size() == types[i][j].size(), types, "expected sub-vectors in selectors and types vectors to match in size"); for(unsigned k = 0; k < selectors[i][j].size(); ++k) { if(types[i][j][k].getType().isString()) { ctor.addArg(selectors[i][j][k], CVC4::DatatypeUnresolvedType(types[i][j][k].getConst())); @@ -1137,12 +1191,17 @@ void ValidityChecker::dataType(const std::vector& names, for(vector::iterator i = dtts.begin(); i != dtts.end(); ++i) { // For each datatype... const CVC4::Datatype& dt = (*i).getDatatype(); + // ensure it's well-founded (the check is done here because + // that's how it is in CVC3) + if(!dt.isWellFounded()) { + throw TypecheckException(d_em->mkConst(dt), "datatype is not well-founded"); + } for(CVC4::Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) { // For each constructor, register its name and its selectors names. - AlwaysAssert(d_constructors.find((*j).getName()) == d_constructors.end(), "cannot have two constructors with the same name in a ValidityChecker"); + CheckArgument(d_constructors.find((*j).getName()) == d_constructors.end(), constructors, "cannot have two constructors with the same name in a ValidityChecker"); d_constructors[(*j).getName()] = &dt; for(CVC4::DatatypeConstructor::const_iterator k = (*j).begin(); k != (*j).end(); ++k) { - AlwaysAssert(d_selectors.find((*k).getName()) == d_selectors.end(), "cannot have two selectors with the same name in a ValidityChecker"); + CheckArgument(d_selectors.find((*k).getName()) == d_selectors.end(), selectors, "cannot have two selectors with the same name in a ValidityChecker"); d_selectors[(*k).getName()] = make_pair(&dt, (*j).getName()); } } @@ -1306,11 +1365,21 @@ Type ValidityChecker::parseType(const Expr& e) { } Expr ValidityChecker::importExpr(const Expr& e) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + if(e.getExprManager() == d_em) { + return e; + } + + s_validityCheckers[e.getExprManager()]->d_reverseEmmc.insert(this); + return e.exportTo(d_em, d_emmc[e.getExprManager()]); } Type ValidityChecker::importType(const Type& t) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + if(t.getExprManager() == d_em) { + return t; + } + + s_validityCheckers[t.getExprManager()]->d_reverseEmmc.insert(this); + return t.exportTo(d_em, d_emmc[t.getExprManager()]); } void ValidityChecker::cmdsFromString(const std::string& s, InputLanguage lang) { @@ -1355,9 +1424,9 @@ Expr ValidityChecker::andExpr(const Expr& left, const Expr& right) { } Expr ValidityChecker::andExpr(const std::vector& children) { - const vector& v = - *reinterpret_cast*>(&children); - return d_em->mkExpr(CVC4::kind::AND, v); + // AND must have at least 2 children + CheckArgument(children.size() > 0, children); + return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::AND, *reinterpret_cast*>(&children))); } Expr ValidityChecker::orExpr(const Expr& left, const Expr& right) { @@ -1365,9 +1434,9 @@ Expr ValidityChecker::orExpr(const Expr& left, const Expr& right) { } Expr ValidityChecker::orExpr(const std::vector& children) { - const vector& v = - *reinterpret_cast*>(&children); - return d_em->mkExpr(CVC4::kind::OR, v); + // OR must have at least 2 children + CheckArgument(children.size() > 0, children); + return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::OR, *reinterpret_cast*>(&children))); } Expr ValidityChecker::impliesExpr(const Expr& hyp, const Expr& conc) { @@ -1388,6 +1457,7 @@ Expr ValidityChecker::iteExpr(const Expr& ifpart, const Expr& thenpart, } Expr ValidityChecker::distinctExpr(const std::vector& children) { + CheckArgument(children.size() > 1, children, "it makes no sense to create a `distinct' expression with only one child"); const vector& v = *reinterpret_cast*>(&children); return d_em->mkExpr(CVC4::kind::DISTINCT, v); @@ -1446,7 +1516,12 @@ Expr ValidityChecker::ratExpr(const std::string& n, const std::string& d, int ba } Expr ValidityChecker::ratExpr(const std::string& n, int base) { - return d_em->mkConst(Rational(n, base)); + if(n.find(".") == string::npos) { + return d_em->mkConst(Rational(n, base)); + } else { + CheckArgument(base == 10, base, "unsupported base for decimal parsing"); + return d_em->mkConst(Rational::fromDecimal(n)); + } } Expr ValidityChecker::uminusExpr(const Expr& child) { @@ -1458,9 +1533,9 @@ Expr ValidityChecker::plusExpr(const Expr& left, const Expr& right) { } Expr ValidityChecker::plusExpr(const std::vector& children) { - const vector& v = - *reinterpret_cast*>(&children); - return d_em->mkExpr(CVC4::kind::PLUS, v); + // PLUS must have at least 2 children + CheckArgument(children.size() > 0, children); + return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::PLUS, *reinterpret_cast*>(&children))); } Expr ValidityChecker::minusExpr(const Expr& left, const Expr& right) { @@ -1608,8 +1683,14 @@ Expr ValidityChecker::newBVAndExpr(const Expr& t1, const Expr& t2) { } Expr ValidityChecker::newBVAndExpr(const std::vector& kids) { - // BVAND is not N-ary - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + // BITVECTOR_AND is not N-ary in CVC4 + CheckArgument(kids.size() > 1, kids, "BITVECTOR_AND must have at least 2 children"); + std::vector::const_reverse_iterator i = kids.rbegin(); + Expr e = *i++; + while(i != kids.rend()) { + e = d_em->mkExpr(CVC4::kind::BITVECTOR_AND, *i++, e); + } + return e; } Expr ValidityChecker::newBVOrExpr(const Expr& t1, const Expr& t2) { @@ -1619,8 +1700,14 @@ Expr ValidityChecker::newBVOrExpr(const Expr& t1, const Expr& t2) { } Expr ValidityChecker::newBVOrExpr(const std::vector& kids) { - // BVOR is not N-ary - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + // BITVECTOR_OR is not N-ary in CVC4 + CheckArgument(kids.size() > 1, kids, "BITVECTOR_OR must have at least 2 children"); + std::vector::const_reverse_iterator i = kids.rbegin(); + Expr e = *i++; + while(i != kids.rend()) { + e = d_em->mkExpr(CVC4::kind::BITVECTOR_OR, *i++, e); + } + return e; } Expr ValidityChecker::newBVXorExpr(const Expr& t1, const Expr& t2) { @@ -1630,8 +1717,14 @@ Expr ValidityChecker::newBVXorExpr(const Expr& t1, const Expr& t2) { } Expr ValidityChecker::newBVXorExpr(const std::vector& kids) { - // BVXOR is not N-ary - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + // BITVECTOR_XOR is not N-ary in CVC4 + CheckArgument(kids.size() > 1, kids, "BITVECTOR_XOR must have at least 2 children"); + std::vector::const_reverse_iterator i = kids.rbegin(); + Expr e = *i++; + while(i != kids.rend()) { + e = d_em->mkExpr(CVC4::kind::BITVECTOR_XOR, *i++, e); + } + return e; } Expr ValidityChecker::newBVXnorExpr(const Expr& t1, const Expr& t2) { @@ -1641,8 +1734,14 @@ Expr ValidityChecker::newBVXnorExpr(const Expr& t1, const Expr& t2) { } Expr ValidityChecker::newBVXnorExpr(const std::vector& kids) { - // BVXNOR is not N-ary - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + // BITVECTOR_XNOR is not N-ary in CVC4 + CheckArgument(kids.size() > 1, kids, "BITVECTOR_XNOR must have at least 2 children"); + std::vector::const_reverse_iterator i = kids.rbegin(); + Expr e = *i++; + while(i != kids.rend()) { + e = d_em->mkExpr(CVC4::kind::BITVECTOR_XNOR, *i++, e); + } + return e; } Expr ValidityChecker::newBVNandExpr(const Expr& t1, const Expr& t2) { @@ -1707,18 +1806,48 @@ Expr ValidityChecker::newBVSubExpr(const Expr& t1, const Expr& t2) { return d_em->mkExpr(CVC4::kind::BITVECTOR_SUB, t1, t2); } -Expr ValidityChecker::newBVPlusExpr(int numbits, const std::vector& k) { - // BVPLUS is not N-ary - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); +// Copied from CVC3's bitvector theory: makes bitvector expression "e" +// into "len" bits, by zero-padding, or extracting least-significant bits. +Expr ValidityChecker::bvpad(int len, const Expr& e) { + CheckArgument(len >= 0, len, + "padding length must be a non-negative integer, not %d", len); + CheckArgument(e.getType().isBitVector(), e, + "input to bitvector operation must be a bitvector"); + + unsigned size = CVC4::BitVectorType(e.getType()).getSize(); + Expr res; + if(size == len) { + res = e; + } else if(len < size) { + res = d_em->mkExpr(d_em->mkConst(CVC4::BitVectorExtract(len - 1, 0)), e); + } else { + // size < len + Expr zero = d_em->mkConst(CVC4::BitVector(len - size, 0u)); + res = d_em->mkExpr(CVC4::kind::BITVECTOR_CONCAT, zero, e); + } + return res; +} + +Expr ValidityChecker::newBVPlusExpr(int numbits, const std::vector& kids) { + // BITVECTOR_PLUS is not N-ary in CVC4 + CheckArgument(kids.size() > 1, kids, "BITVECTOR_PLUS must have at least 2 children"); + std::vector::const_reverse_iterator i = kids.rbegin(); + Expr e = *i++; + while(i != kids.rend()) { + e = d_em->mkExpr(CVC4::kind::BITVECTOR_PLUS, bvpad(numbits, *i++), e); + } + unsigned size = CVC4::BitVectorType(e.getType()).getSize(); + CheckArgument(unsigned(numbits) == size, numbits, + "argument must match computed size of bitvector sum: " + "passed size == %u, computed size == %u", numbits, size); + return e; } 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, bvpad(numbits, t1), bvpad(numbits, t2)); unsigned size = CVC4::BitVectorType(e.getType()).getSize(); - CheckArgument(numbits > 0, numbits, - "argument must be positive integer, not %u", numbits); CheckArgument(unsigned(numbits) == size, numbits, "argument must match computed size of bitvector sum: " "passed size == %u, computed size == %u", numbits, size); @@ -1728,10 +1857,8 @@ 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, bvpad(numbits, t1), bvpad(numbits, t2)); unsigned size = CVC4::BitVectorType(e.getType()).getSize(); - CheckArgument(numbits > 0, numbits, - "argument must be positive integer, not %u", numbits); CheckArgument(unsigned(numbits) == size, numbits, "argument must match computed size of bitvector product: " "passed size == %u, computed size == %u", numbits, size); @@ -1861,42 +1988,61 @@ Expr ValidityChecker::boundVarExpr(const std::string& name, const std::string& u } Expr ValidityChecker::forallExpr(const std::vector& vars, const Expr& body) { - Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); + Expr boundVarList = d_em->mkExpr(CVC4::kind::BOUND_VAR_LIST, *reinterpret_cast*>(&vars)); + return d_em->mkExpr(CVC4::kind::FORALL, boundVarList, body); } Expr ValidityChecker::forallExpr(const std::vector& vars, const Expr& body, const Expr& trigger) { - Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); + // trigger + Expr boundVarList = d_em->mkExpr(CVC4::kind::BOUND_VAR_LIST, *reinterpret_cast*>(&vars)); + Expr triggerList = d_em->mkExpr(CVC4::kind::INST_PATTERN_LIST, d_em->mkExpr(CVC4::kind::INST_PATTERN, trigger)); + return d_em->mkExpr(CVC4::kind::FORALL, boundVarList, body, triggerList); } Expr ValidityChecker::forallExpr(const std::vector& vars, const Expr& body, const std::vector& triggers) { - Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); + // set of triggers + Expr boundVarList = d_em->mkExpr(CVC4::kind::BOUND_VAR_LIST, *reinterpret_cast*>(&vars)); + std::vector pats; + for(std::vector::const_iterator i = triggers.begin(); i != triggers.end(); ++i) { + pats.push_back(d_em->mkExpr(CVC4::kind::INST_PATTERN, *i)); + } + Expr triggerList = d_em->mkExpr(CVC4::kind::INST_PATTERN_LIST, pats); + return d_em->mkExpr(CVC4::kind::FORALL, boundVarList, body, triggerList); } Expr ValidityChecker::forallExpr(const std::vector& vars, const Expr& body, const std::vector >& triggers) { - Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); + // set of multi-triggers + Expr boundVarList = d_em->mkExpr(CVC4::kind::BOUND_VAR_LIST, *reinterpret_cast*>(&vars)); + std::vector pats; + for(std::vector< std::vector >::const_iterator i = triggers.begin(); i != triggers.end(); ++i) { + pats.push_back(d_em->mkExpr(CVC4::kind::INST_PATTERN, *reinterpret_cast*>(&*i))); + } + Expr triggerList = d_em->mkExpr(CVC4::kind::INST_PATTERN_LIST, pats); + return d_em->mkExpr(CVC4::kind::FORALL, boundVarList, body, triggerList); } void ValidityChecker::setTriggers(const Expr& e, const std::vector > & triggers) { - Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); } void ValidityChecker::setTriggers(const Expr& e, const std::vector& triggers) { - Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); } void ValidityChecker::setTrigger(const Expr& e, const Expr& trigger) { - Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); } void ValidityChecker::setMultiTrigger(const Expr& e, const std::vector& multiTrigger) { - Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); } Expr ValidityChecker::existsExpr(const std::vector& vars, const Expr& body) { - Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); + Expr boundVarList = d_em->mkExpr(CVC4::kind::BOUND_VAR_LIST, *reinterpret_cast*>(&vars)); + return d_em->mkExpr(CVC4::kind::EXISTS, boundVarList, body); } Op ValidityChecker::lambdaExpr(const std::vector& vars, const Expr& body) { @@ -1914,11 +2060,16 @@ Expr ValidityChecker::simulateExpr(const Expr& f, const Expr& s0, } void ValidityChecker::setResourceLimit(unsigned limit) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + // Set a resource limit for CVC4, cumulative (rather than + // per-query), starting from now. + d_smt->setResourceLimit(limit, true); } void ValidityChecker::setTimeLimit(unsigned limit) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + // Set a time limit for CVC4, cumulative (rather than per-query), + // starting from now. Note that CVC3 uses tenths of a second, + // while CVC4 uses milliseconds. + d_smt->setTimeLimit(limit * 100, true); } void ValidityChecker::assertFormula(const Expr& e) { @@ -2031,11 +2182,17 @@ Expr ValidityChecker::getValue(const Expr& e) { } bool ValidityChecker::inconsistent(std::vector& assumptions) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + CheckArgument(assumptions.empty(), assumptions, "assumptions vector should be empty on entry"); + if(d_smt->checkSat() == CVC4::Result::UNSAT) { + // supposed to be a minimal set, but CVC4 doesn't support that + d_smt->getAssertions().swap(*reinterpret_cast*>(&assumptions)); + return true; + } + return false; } bool ValidityChecker::inconsistent() { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + return d_smt->checkSat() == CVC4::Result::UNSAT; } bool ValidityChecker::incomplete() { diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h index 3ef40636a..83465775b 100644 --- a/src/compat/cvc3_compat.h +++ b/src/compat/cvc3_compat.h @@ -526,8 +526,13 @@ class CVC4_PUBLIC ValidityChecker { CLFlags* d_clflags; CVC4::Options d_options; CVC3::ExprManager* d_em; + std::map d_emmc; + std::set d_reverseEmmc; CVC4::SmtEngine* d_smt; CVC4::parser::Parser* d_parserContext; + std::vector d_exprTypeMapRemove; + + friend class Type; // to reach in to d_exprTypeMapRemove typedef std::hash_map ConstructorMap; typedef std::hash_map, CVC4::StringHashFunction> SelectorMap; @@ -539,6 +544,9 @@ class CVC4_PUBLIC ValidityChecker { void setUpOptions(CVC4::Options& options, const CLFlags& clflags); + // helper function for bitvectors + Expr bvpad(int len, const Expr& e); + public: //! Constructor ValidityChecker(); diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index b0364348c..365dc050f 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -120,7 +120,7 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC Expr from_e(from, new Node(n)); Expr& to_e = vmap.d_typeMap[from_e]; if(! to_e.isNull()) { -Debug("export") << "+ mapped `" << from_e << "' to `" << to_e << "'" << std::endl; + Debug("export") << "+ mapped `" << from_e << "' to `" << to_e << "'" << std::endl; return to_e.getNode(); } else { // construct new variable in other manager: @@ -128,11 +128,17 @@ Debug("export") << "+ mapped `" << from_e << "' to `" << to_e << "'" << std::end std::string name; Type type = from->exportType(from_e.getType(), to, vmap); if(Node::fromExpr(from_e).getAttribute(VarNameAttr(), name)) { + // temporarily set the node manager to NULL; this gets around + // a check that mkVar isn't called internally + NodeManagerScope nullScope(NULL); to_e = to->mkVar(name, type);// FIXME thread safety -Debug("export") << "+ exported var `" << from_e << "'[" << from_e.getId() << "] with name `" << name << "' and type `" << from_e.getType() << "' to `" << to_e << "'[" << to_e.getId() << "] with type `" << type << "'" << std::endl; + Debug("export") << "+ exported var `" << from_e << "'[" << from_e.getId() << "] with name `" << name << "' and type `" << from_e.getType() << "' to `" << to_e << "'[" << to_e.getId() << "] with type `" << type << "'" << std::endl; } else { + // temporarily set the node manager to NULL; this gets around + // a check that mkVar isn't called internally + NodeManagerScope nullScope(NULL); to_e = to->mkVar(type);// FIXME thread safety -Debug("export") << "+ exported unnamed var `" << from_e << "' with type `" << from_e.getType() << "' to `" << to_e << "' with type `" << type << "'" << std::endl; + Debug("export") << "+ exported unnamed var `" << from_e << "' with type `" << from_e.getType() << "' to `" << to_e << "' with type `" << type << "'" << std::endl; } uint64_t to_int = (uint64_t)(to_e.getNode().d_nv); uint64_t from_int = (uint64_t)(from_e.getNode().d_nv); @@ -143,16 +149,16 @@ Debug("export") << "+ exported unnamed var `" << from_e << "' with type `" << fr } } else { std::vector children; -Debug("export") << "n: " << n << std::endl; + Debug("export") << "n: " << n << std::endl; if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { -Debug("export") << "+ parameterized, op is " << n.getOperator() << std::endl; + Debug("export") << "+ parameterized, op is " << n.getOperator() << std::endl; children.reserve(n.getNumChildren() + 1); children.push_back(exportInternal(n.getOperator(), from, to, vmap)); } else { children.reserve(n.getNumChildren()); } for(TNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) { -Debug("export") << "+ child: " << *i << std::endl; + Debug("export") << "+ child: " << *i << std::endl; children.push_back(exportInternal(*i, from, to, vmap)); } if(Debug.isOn("export")) { @@ -281,6 +287,7 @@ Type Expr::getType(bool check) const throw (TypeCheckingException) { } Expr Expr::substitute(Expr e, Expr replacement) const { + ExprManagerScope ems(*this); return Expr(d_exprManager, new Node(d_node->substitute(TNode(*e.d_node), TNode(*replacement.d_node)))); } @@ -304,6 +311,7 @@ static inline NodeIteratorAdaptor mkNodeIteratorAdaptor(Iterator i) { Expr Expr::substitute(const std::vector exes, const std::vector& replacements) const { + ExprManagerScope ems(*this); return Expr(d_exprManager, new Node(d_node->substitute(mkNodeIteratorAdaptor(exes.begin()), mkNodeIteratorAdaptor(exes.end()), @@ -330,31 +338,39 @@ static inline NodePairIteratorAdaptor mkNodePairIteratorAdaptor(Iterat } Expr Expr::substitute(const std::hash_map map) const { + ExprManagerScope ems(*this); return Expr(d_exprManager, new Node(d_node->substitute(mkNodePairIteratorAdaptor(map.begin()), mkNodePairIteratorAdaptor(map.end())))); } Expr::const_iterator::const_iterator() : d_iterator(NULL) { } -Expr::const_iterator::const_iterator(void* v) : +Expr::const_iterator::const_iterator(ExprManager* em, void* v) : + d_exprManager(em), d_iterator(v) { } Expr::const_iterator::const_iterator(const const_iterator& it) { if(it.d_iterator == NULL) { d_iterator = NULL; } else { + d_exprManager = it.d_exprManager; + ExprManagerScope ems(*d_exprManager); d_iterator = new Node::iterator(*reinterpret_cast(it.d_iterator)); } } Expr::const_iterator& Expr::const_iterator::operator=(const const_iterator& it) { if(d_iterator != NULL) { + ExprManagerScope ems(*d_exprManager); delete reinterpret_cast(d_iterator); } + d_exprManager = it.d_exprManager; + ExprManagerScope ems(*d_exprManager); d_iterator = new Node::iterator(*reinterpret_cast(it.d_iterator)); return *this; } Expr::const_iterator::~const_iterator() { if(d_iterator != NULL) { + ExprManagerScope ems(*d_exprManager); delete reinterpret_cast(d_iterator); } } @@ -367,26 +383,31 @@ bool Expr::const_iterator::operator==(const const_iterator& it) const { } Expr::const_iterator& Expr::const_iterator::operator++() { Assert(d_iterator != NULL); + ExprManagerScope ems(*d_exprManager); ++*reinterpret_cast(d_iterator); return *this; } Expr::const_iterator Expr::const_iterator::operator++(int) { Assert(d_iterator != NULL); + ExprManagerScope ems(*d_exprManager); const_iterator it = *this; ++*reinterpret_cast(d_iterator); return it; } Expr Expr::const_iterator::operator*() const { Assert(d_iterator != NULL); + ExprManagerScope ems(*d_exprManager); return (**reinterpret_cast(d_iterator)).toExpr(); } Expr::const_iterator Expr::begin() const { - return Expr::const_iterator(new Node::iterator(d_node->begin())); + ExprManagerScope ems(*d_exprManager); + return Expr::const_iterator(d_exprManager, new Node::iterator(d_node->begin())); } Expr::const_iterator Expr::end() const { - return Expr::const_iterator(new Node::iterator(d_node->end())); + ExprManagerScope ems(*d_exprManager); + return Expr::const_iterator(d_exprManager, new Node::iterator(d_node->end())); } std::string Expr::toString() const { diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index e1b5cc4e6..395bdff3a 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -102,12 +102,13 @@ private: protected: TypeCheckingException() throw() : Exception() {} - TypeCheckingException(const Expr& expr, std::string message) throw(); TypeCheckingException(ExprManager* em, const TypeCheckingExceptionPrivate* exc) throw(); public: + TypeCheckingException(const Expr& expr, std::string message) throw(); + /** Copy constructor */ TypeCheckingException(const TypeCheckingException& t) throw(); @@ -299,8 +300,10 @@ public: * Iterator type for the children of an Expr. */ class const_iterator : public std::iterator { + ExprManager* d_exprManager; void* d_iterator; - explicit const_iterator(void*); + + explicit const_iterator(ExprManager*, void*); friend class Expr;// to access void* constructor @@ -957,7 +960,7 @@ public: ${getConst_instantiations} -#line 961 "${template}" +#line 964 "${template}" namespace expr { diff --git a/src/expr/type.cpp b/src/expr/type.cpp index bd8e29a44..d67aa1fe3 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -178,7 +178,7 @@ ExprManager* Type::getExprManager() const { return d_nodeManager->toExprManager(); } -Type Type::exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap) { +Type Type::exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap) const { return ExprManager::exportType(*this, exprManager, vmap); } diff --git a/src/expr/type.h b/src/expr/type.h index bd6a6a298..29b0ac128 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -185,7 +185,7 @@ public: /** * Exports this type into a different ExprManager. */ - Type exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap); + Type exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap) const; /** * Assignment operator. diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 7b093d11a..e35d55e28 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -239,7 +239,7 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ case kind::FUNCTION_TYPE: return TypeNode(); // Not sure if this is right case kind::TUPLE_TYPE: - Unimplemented(); + Unimplemented("haven't implemented leastCommonType for tuples yet"); return TypeNode(); // Not sure if this is right case kind::SUBTYPE_TYPE: if(t1.isPredicateSubtype()){ @@ -278,8 +278,11 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ Assert(t1.isInteger()); return TypeNode(); } + case kind::DATATYPE_TYPE: + // two datatypes that aren't == have no common ancestors + return TypeNode(); default: - Unimplemented(); + Unimplemented("don't have a leastCommonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str()); return TypeNode(); } } diff --git a/src/options/Makefile.am b/src/options/Makefile.am index 088c972b3..eb1a2c498 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -156,9 +156,9 @@ endif # expression (no |, no \<, ...). Debug_tags.tmp Trace_tags.tmp: $(AM_V_GEN)\ - grep '\<$(@:_tags.tmp=) *( *\".*\" *)' \ + grep '\<$(@:_tags.tmp=)\(\.isOn\)* *( *\".*\" *)' \ `find @srcdir@/../ -name "*.cpp" -or -name "*.h" -or -name "*.cc" -or -name "*.g"` | \ - sed 's/^$(@:_tags.tmp=) *( *\"\([^"]*\)\".*/\1/;s/.*[^a-zA-Z0-9_]$(@:_tags.tmp=) *( *\"\([^"]*\)\".*/\1/' | sort | uniq >"$@" + sed 's/^$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/;s/.*[^a-zA-Z0-9_]$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/' | LC_ALL=C sort | uniq >"$@" MOSTLYCLEANFILES = \ Debug_tags \ diff --git a/src/options/base_options b/src/options/base_options index 10ad564e6..59fadf40b 100644 --- a/src/options/base_options +++ b/src/options/base_options @@ -71,9 +71,9 @@ option in std::istream* :default &std::cin :include option out std::ostream* :default &std::cout :include option err std::ostream* :default &std::cerr :include -common-option inputLanguage -L --lang=LANG InputLanguage :handler CVC4::options::stringToInputLanguage :include "util/language.h" :default language::input::LANG_AUTO :read-write +common-option inputLanguage input-language -L --lang=LANG InputLanguage :handler CVC4::options::stringToInputLanguage :include "util/language.h" :default language::input::LANG_AUTO :read-write force input language (default is "auto"; see --lang help) -common-option outputLanguage --output-lang=LANG OutputLanguage :handler CVC4::options::stringToOutputLanguage :include "util/language.h" :default language::output::LANG_AUTO :read-write +common-option outputLanguage output-language --output-lang=LANG OutputLanguage :handler CVC4::options::stringToOutputLanguage :include "util/language.h" :default language::output::LANG_AUTO :read-write force input language (default is "auto"; see --lang help) option languageHelp bool @@ -84,7 +84,7 @@ common-option - -v --verbose void :handler CVC4::options::increaseVerbosity common-option - -q --quiet void :handler CVC4::options::decreaseVerbosity decrease verbosity (may be repeated) -common-option statistics stats --stats bool +common-option statistics statistics --stats bool give statistics on exit common-option parseOnly parse-only --parse-only bool :read-write diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h index 5f82280da..6cb74c637 100644 --- a/src/options/base_options_handlers.h +++ b/src/options/base_options_handlers.h @@ -38,22 +38,22 @@ inline void decreaseVerbosity(std::string option, SmtEngine* smt) { } inline OutputLanguage stringToOutputLanguage(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "cvc4" || optarg == "pl") { + if(optarg == "cvc4" || optarg == "pl" || optarg == "presentation" || optarg == "LANG_CVC4") { return language::output::LANG_CVC4; - } else if(optarg == "smtlib" || optarg == "smt") { + } else if(optarg == "smtlib" || optarg == "smt" || optarg == "LANG_SMTLIB") { return language::output::LANG_SMTLIB; - } else if(optarg == "smtlib2" || optarg == "smt2") { + } else if(optarg == "smtlib2" || optarg == "smt2" || optarg == "LANG_SMTLIB_V2") { return language::output::LANG_SMTLIB_V2; - } else if(optarg == "tptp") { + } else if(optarg == "tptp" || optarg == "LANG_TPTP") { return language::output::LANG_TPTP; - } else if(optarg == "ast") { + } else if(optarg == "ast" || optarg == "LANG_AST") { return language::output::LANG_AST; - } else if(optarg == "auto") { + } else if(optarg == "auto" || optarg == "LANG_AUTO") { return language::output::LANG_AUTO; } if(optarg != "help") { - throw OptionException(std::string("unknown language for --output-lang: `") + + throw OptionException(std::string("unknown language for ") + option + ": `" + optarg + "'. Try --output-lang help."); } @@ -62,20 +62,20 @@ inline OutputLanguage stringToOutputLanguage(std::string option, std::string opt } inline InputLanguage stringToInputLanguage(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "cvc4" || optarg == "pl" || optarg == "presentation") { + if(optarg == "cvc4" || optarg == "pl" || optarg == "presentation" || optarg == "LANG_CVC4") { return language::input::LANG_CVC4; - } else if(optarg == "smtlib" || optarg == "smt") { + } else if(optarg == "smtlib" || optarg == "smt" || optarg == "LANG_SMTLIB") { return language::input::LANG_SMTLIB; - } else if(optarg == "smtlib2" || optarg == "smt2") { + } else if(optarg == "smtlib2" || optarg == "smt2" || optarg == "LANG_SMTLIB_V2") { return language::input::LANG_SMTLIB_V2; - } else if(optarg == "tptp") { + } else if(optarg == "tptp" || optarg == "LANG_TPTP") { return language::input::LANG_TPTP; - } else if(optarg == "auto") { + } else if(optarg == "auto" || optarg == "LANG_AUTO") { return language::input::LANG_AUTO; } if(optarg != "help") { - throw OptionException(std::string("unknown language for --lang: `") + + throw OptionException(std::string("unknown language for ") + option + ": `" + optarg + "'. Try --lang help."); } diff --git a/src/options/option_exception.h b/src/options/option_exception.h index 657bc7568..6aaa7d7e2 100644 --- a/src/options/option_exception.h +++ b/src/options/option_exception.h @@ -49,7 +49,7 @@ public: } UnrecognizedOptionException(const std::string& msg) : - CVC4::OptionException(msg) { + CVC4::OptionException("Unrecognized informational or option key or setting: " + msg) { } };/* class UnrecognizedOptionException */ diff --git a/src/smt/options b/src/smt/options index 13b3b51f3..fea609bb5 100644 --- a/src/smt/options +++ b/src/smt/options @@ -21,7 +21,7 @@ common-option - --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler- expert-option lazyDefinitionExpansion --lazy-definition-expansion bool expand define-funs/LAMBDAs lazily -option simplificationMode --simplification=MODE SimplificationMode :handler CVC4::smt::stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "smt/simplification_mode.h" :handler-include "smt/options_handlers.h" +option simplificationMode simplification-mode --simplification=MODE SimplificationMode :handler CVC4::smt::stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "smt/simplification_mode.h" :handler-include "smt/options_handlers.h" choose simplification mode, see --simplification=help alias --no-simplification = --simplification=none turn off all simplification (same as --simplification=none) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bcd7cc6d2..d450319b1 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -310,6 +310,16 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_context->push(); d_definedFunctions = new(true) DefinedFunctionMap(d_userContext); +} + +void SmtEngine::finishInit() { + d_decisionEngine = new DecisionEngine(d_context, d_userContext); + d_decisionEngine->init(); // enable appropriate strategies + + d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context); + + d_theoryEngine->setPropEngine(d_propEngine); + d_theoryEngine->setDecisionEngine(d_decisionEngine); // [MGD 10/20/2011] keep around in incremental mode, due to a // cleanup ordering issue and Nodes/TNodes. If SAT is popped @@ -336,16 +346,6 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : } } -void SmtEngine::finishInit() { - d_decisionEngine = new DecisionEngine(d_context, d_userContext); - d_decisionEngine->init(); // enable appropriate strategies - - d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context); - - d_theoryEngine->setPropEngine(d_propEngine); - d_theoryEngine->setDecisionEngine(d_decisionEngine); -} - void SmtEngine::finalOptionsAreSet() { if(d_fullyInited) { return; @@ -1534,7 +1534,7 @@ void SmtEnginePrivate::addFormula(TNode n) } } -void SmtEngine::ensureBoolean(const BoolExpr& e) { +void SmtEngine::ensureBoolean(const BoolExpr& e) throw(TypeCheckingException) { Type type = e.getType(options::typeChecking()); Type boolType = d_exprManager->booleanType(); if(type != boolType) { @@ -1546,7 +1546,7 @@ void SmtEngine::ensureBoolean(const BoolExpr& e) { } } -Result SmtEngine::checkSat(const BoolExpr& e) { +Result SmtEngine::checkSat(const BoolExpr& e) throw(TypeCheckingException) { Assert(e.isNull() || e.getExprManager() == d_exprManager); @@ -1608,7 +1608,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) { return r; } -Result SmtEngine::query(const BoolExpr& e) { +Result SmtEngine::query(const BoolExpr& e) throw(TypeCheckingException) { Assert(!e.isNull()); Assert(e.getExprManager() == d_exprManager); @@ -1667,7 +1667,7 @@ Result SmtEngine::query(const BoolExpr& e) { return r; } -Result SmtEngine::assertFormula(const BoolExpr& e) { +Result SmtEngine::assertFormula(const BoolExpr& e) throw(TypeCheckingException) { Assert(e.getExprManager() == d_exprManager); SmtScope smts(this); finalOptionsAreSet(); @@ -1680,7 +1680,7 @@ Result SmtEngine::assertFormula(const BoolExpr& e) { return quickCheck().asValidityResult(); } -Expr SmtEngine::simplify(const Expr& e) { +Expr SmtEngine::simplify(const Expr& e) throw(TypeCheckingException) { Assert(e.getExprManager() == d_exprManager); SmtScope smts(this); finalOptionsAreSet(); @@ -1691,6 +1691,9 @@ Expr SmtEngine::simplify(const Expr& e) { if(Dump.isOn("benchmark")) { Dump("benchmark") << SimplifyCommand(e); } + // Make sure we've done simple preprocessing, unit detection, etc. + Trace("smt") << "SmtEngine::check(): processing assertions" << endl; + d_private->processAssertions(); return d_private->applySubstitutions(e).toExpr(); } @@ -1912,6 +1915,7 @@ vector SmtEngine::getAssertions() throw ModalException(msg); } Assert(d_assertionList != NULL); + // copy the result out return vector(d_assertionList->begin(), d_assertionList->end()); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 43a7ee58d..25800f5b3 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -234,7 +234,7 @@ class CVC4_PUBLIC SmtEngine { * Fully type-check the argument, and also type-check that it's * actually Boolean. */ - void ensureBoolean(const BoolExpr& e); + void ensureBoolean(const BoolExpr& e) throw(TypeCheckingException); void internalPush(); @@ -337,20 +337,20 @@ public: * literals and conjunction of literals. Returns false iff * inconsistent. */ - Result assertFormula(const BoolExpr& e); + Result assertFormula(const BoolExpr& e) throw(TypeCheckingException); /** * Check validity of an expression with respect to the current set * of assertions by asserting the query expression's negation and * calling check(). Returns valid, invalid, or unknown result. */ - Result query(const BoolExpr& e); + Result query(const BoolExpr& e) throw(TypeCheckingException); /** * Assert a formula (if provided) to the current context and call * check(). Returns sat, unsat, or unknown result. */ - Result checkSat(const BoolExpr& e = BoolExpr()); + Result checkSat(const BoolExpr& e = BoolExpr()) throw(TypeCheckingException); /** * Simplify a formula without doing "much" work. Does not involve @@ -361,7 +361,7 @@ public: * @todo (design) is this meant to give an equivalent or an * equisatisfiable formula? */ - Expr simplify(const Expr& e); + Expr simplify(const Expr& e) throw(TypeCheckingException); /** * Get the assigned value of an expr (only if immediately preceded diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp index b254a3b30..1af029f17 100644 --- a/src/smt/smt_options_template.cpp +++ b/src/smt/smt_options_template.cpp @@ -52,7 +52,7 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) #line 54 "${template}" - throw UnrecognizedOptionException(); + throw UnrecognizedOptionException(key); } CVC4::SExpr SmtEngine::getOption(const std::string& key) const @@ -69,7 +69,7 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const #line 71 "${template}" - throw UnrecognizedOptionException(); + throw UnrecognizedOptionException(key); } }/* CVC4 namespace */ diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 986654cd3..3850fab98 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -15,9 +15,12 @@ rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arra operator ARRAY_TYPE 2 "array type" cardinality ARRAY_TYPE \ - "::CVC4::theory::arrays::CardinalityComputer::computeCardinality(%TYPE%)" \ + "::CVC4::theory::arrays::ArraysProperties::computeCardinality(%TYPE%)" \ + "theory/arrays/theory_arrays_type_rules.h" +well-founded ARRAY_TYPE \ + "::CVC4::theory::arrays::ArraysProperties::isWellFounded(%TYPE%)" \ + "::CVC4::theory::arrays::ArraysProperties::mkGroundTerm(%TYPE%)" \ "theory/arrays/theory_arrays_type_rules.h" -well-founded ARRAY_TYPE false enumerator ARRAY_TYPE \ "::CVC4::theory::arrays::ArrayEnumerator" \ diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index 8b31a31f9..854b5449f 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -22,6 +22,7 @@ #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H #include "theory/arrays/theory_arrays_rewriter.h" // for array-constant attributes +#include "theory/type_enumerator.h" namespace CVC4 { namespace theory { @@ -37,7 +38,7 @@ struct ArraySelectTypeRule { throw TypeCheckingExceptionPrivate(n, "array select operating on non-array"); } TypeNode indexType = n[1].getType(check); - if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ + if(!indexType.isComparableTo(arrayType.getArrayIndexType())){ throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array"); } } @@ -56,10 +57,10 @@ struct ArrayStoreTypeRule { } TypeNode indexType = n[1].getType(check); TypeNode valueType = n[2].getType(check); - if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ + if(!indexType.isComparableTo(arrayType.getArrayIndexType())){ throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array"); } - if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){ + if(!valueType.isComparableTo(arrayType.getArrayConstituentType())){ Debug("array-types") << "array type: "<< arrayType.getArrayConstituentType() << std::endl; Debug("array-types") << "value types: " << valueType << std::endl; throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array"); @@ -167,11 +168,11 @@ struct ArrayTableFunTypeRule { throw TypeCheckingExceptionPrivate(n, "array table fun arg 1 is non-array"); } TypeNode indexType = n[2].getType(check); - if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ + if(!indexType.isComparableTo(arrayType.getArrayIndexType())){ throw TypeCheckingExceptionPrivate(n, "array table fun arg 2 does not match type of array"); } indexType = n[3].getType(check); - if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ + if(!indexType.isComparableTo(arrayType.getArrayIndexType())){ throw TypeCheckingExceptionPrivate(n, "array table fun arg 3 does not match type of array"); } } @@ -179,7 +180,7 @@ struct ArrayTableFunTypeRule { } };/* struct ArrayTableFunTypeRule */ -struct CardinalityComputer { +struct ArraysProperties { inline static Cardinality computeCardinality(TypeNode type) { Assert(type.getKind() == kind::ARRAY_TYPE); @@ -188,7 +189,15 @@ struct CardinalityComputer { return valueCard ^ indexCard; } -};/* struct CardinalityComputer */ + + inline static bool isWellFounded(TypeNode type) { + return type[0].isWellFounded() && type[1].isWellFounded(); + } + + inline static Node mkGroundTerm(TypeNode type) { + return *TypeEnumerator(type); + } +};/* struct ArraysProperties */ }/* CVC4::theory::arrays namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 765f6bc59..65500fe91 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -31,6 +31,11 @@ enumerator BITVECTOR_TYPE \ "::CVC4::theory::bv::BitVectorEnumerator" \ "theory/bv/type_enumerator.h" +well-founded BITVECTOR_TYPE \ + true \ + "(*CVC4::theory::TypeEnumerator(%TYPE%))" \ + "theory/type_enumerator.h" + operator BITVECTOR_CONCAT 2: "bit-vector concatenation" operator BITVECTOR_AND 2: "bitwise and" operator BITVECTOR_OR 2: "bitwise or" diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 432e6ef26..7d3664d47 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -89,52 +89,6 @@ BUILT_SOURCES = \ rational.h \ integer.h \ tls.h -if CVC4_DEBUG -if CVC4_TRACING -# listing Debug_tags too ensures that make doesn't auto-remove it -# after building (if it does, we don't get the "cached" effect with -# the .tmp files below, and we have to re-compile and re-link each -# time, even when there are no changes). -BUILT_SOURCES += \ - Debug_tags.h \ - Debug_tags -endif -endif -if CVC4_TRACING -# listing Trace_tags too ensures that make doesn't auto-remove it -# after building (if it does, we don't get the "cached" effect with -# the .tmp files below, and we have to re-compile and re-link each -# time, even when there are no changes). -BUILT_SOURCES += \ - Trace_tags.h \ - Trace_tags -endif - -%_tags.h: %_tags - $(AM_V_GEN)( \ - echo 'static char const* const $^[] = {'; \ - for tag in `cat $^`; do \ - echo "\"$$tag\","; \ - done; \ - echo 'NULL'; \ - echo '};' \ - ) >"$@" - -# This .tmp business is to keep from having to re-compile options.cpp -# (and then re-link the libraries) if nothing has changed. -%_tags: %_tags.tmp - $(AM_V_GEN)\ - diff -q "$^" "$@" &>/dev/null || mv "$^" "$@" || true -# .PHONY ensures the .tmp version is always rebuilt (to check for any changes) -.PHONY: Debug_tags.tmp Trace_tags.tmp -# The "sed" invocation below is particularly obnoxious, but it works around -# inconsistencies in REs on different platforms, using only a basic regular -# expression (no |, no \<, ...). -Debug_tags.tmp Trace_tags.tmp: - $(AM_V_GEN)\ - grep '\<$(@:_tags.tmp=)\(\.isOn\)* *( *\".*\" *)' \ - `find @srcdir@/../ -name "*.cpp" -or -name "*.h" -or -name "*.cc" -or -name "*.g"` | \ - sed 's/^$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/;s/.*[^a-zA-Z0-9_]$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/' | LC_ALL=C sort | uniq >"$@" if CVC4_CLN_IMP libutil_la_SOURCES += \ @@ -181,10 +135,4 @@ DISTCLEANFILES = \ tls.h.tmp \ integer.h \ rational.h \ - tls.h \ - Debug_tags.tmp \ - Debug_tags.h \ - Debug_tags \ - Trace_tags.tmp \ - Trace_tags.h \ - Trace_tags + tls.h diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index 258060e02..969a8b5eb 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -87,7 +87,7 @@ public: * For more information about what is a valid rational string, * see GMP's documentation for mpq_set_str(). */ - explicit Rational(const char * s, int base = 10) throw (std::invalid_argument){ + explicit Rational(const char* s, unsigned base = 10) throw (std::invalid_argument){ cln::cl_read_flags flags; flags.syntax = cln::syntax_rational; @@ -101,7 +101,7 @@ public: throw std::invalid_argument(ss.str()); } } - Rational(const std::string& s, int base = 10) throw (std::invalid_argument){ + Rational(const std::string& s, unsigned base = 10) throw (std::invalid_argument){ cln::cl_read_flags flags; flags.syntax = cln::syntax_rational; diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index 22f1e91b2..0c8a46f33 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -81,7 +81,7 @@ public: * For more information about what is a valid rational string, * see GMP's documentation for mpq_set_str(). */ - explicit Rational(const char * s, int base = 10): d_value(s,base) { + explicit Rational(const char* s, unsigned base = 10): d_value(s, base) { d_value.canonicalize(); } Rational(const std::string& s, unsigned base = 10) : d_value(s, base) { diff --git a/test/system/Makefile.am b/test/system/Makefile.am index 5fcc8833a..836189991 100644 --- a/test/system/Makefile.am +++ b/test/system/Makefile.am @@ -5,7 +5,11 @@ CPLUSPLUS_TESTS = \ ouroborous \ two_smt_engines \ smt2_compliance -# cvc3_main + +if CVC4_BUILD_LIBCOMPAT +CPLUSPLUS_TESTS += \ + cvc3_main +endif TESTS = $(CPLUSPLUS_TESTS) @@ -32,9 +36,13 @@ TEST_DEPS_DIST = \ # changes made in the header files. TEST_DEPS_NODIST = \ $(abs_top_builddir)/src/libcvc4.la \ - $(abs_top_builddir)/src/parser/libcvc4parser.la \ + $(abs_top_builddir)/src/parser/libcvc4parser.la + +if CVC4_BUILD_LIBCOMPAT +TEST_DEPS_NODIST += \ $(abs_top_builddir)/src/compat/libcvc4compat.la \ cvc3_george.lo +endif TEST_DEPS = \ $(TEST_DEPS_DIST) \ @@ -63,8 +71,13 @@ AM_CPPFLAGS = \ -D __STDC_FORMAT_MACROS \ -D __BUILDING_CVC4_SYSTEM_TEST \ $(TEST_CPPFLAGS) -LIBADD = \ - @abs_top_builddir@/src/compat/libcvc4compat.la \ + +LIBADD = +if CVC4_BUILD_LIBCOMPAT +LIBADD += \ + @abs_top_builddir@/src/compat/libcvc4compat.la +endif +LIBADD += \ @abs_top_builddir@/src/parser/libcvc4parser.la \ @abs_top_builddir@/src/libcvc4.la diff --git a/test/system/cvc3_main.cpp b/test/system/cvc3_main.cpp index 76ff9e974..a428f605d 100644 --- a/test/system/cvc3_main.cpp +++ b/test/system/cvc3_main.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -47,12 +47,25 @@ using namespace std; using namespace CVC3; - int exitStatus; +inline void __expect__(const std::string& file, + int line, + bool cond, + const std::string& cond_s, + const std::string& msg) { + if(!cond) { + std::cerr << file << ":" << line + << ": Expected: (" << cond_s << "). " + << msg << std::endl; + exitStatus = 1; + } +} + +#define EXPECT(cond, msg) __expect__(__FILE__, __LINE__, (cond), #cond, (msg)) // Check whether e is valid -bool check(ValidityChecker* vc, Expr e, bool verbose=false) +bool check(ValidityChecker* vc, Expr e, bool verbose=true) { if(verbose) { cout << "Query: "; @@ -124,7 +137,7 @@ void test () Expr f2 = vc->funExpr(f, e); Expr f3 = vc->funExpr(f, f2); - FatalAssert(e != f2 && e != f3, "Refcount problems"); + EXPECT(e != f2 && e != f3, "Refcount problems"); Expr x (vc->boundVarExpr ("x", "0", it));//x0:int vector xs; @@ -159,12 +172,12 @@ void test1() // even in those exceptional cases. try { - IF_DEBUG(bool b =) check(vc, vc->trueExpr()); - FatalAssert(b, "Should be valid"); + bool b = check(vc, vc->trueExpr()); + EXPECT(b, "Should be valid"); vc->push(); - IF_DEBUG(b =) check(vc, vc->falseExpr()); - FatalAssert(!b, "Should be invalid"); + b = check(vc, vc->falseExpr()); + EXPECT(!b, "Should be invalid"); vc->pop(); // Check p OR ~p @@ -172,8 +185,8 @@ void test1() Expr p = vc->varExpr("p", vc->boolType()); Expr e = vc->orExpr(p, vc->notExpr(p)); - IF_DEBUG(b =) check(vc, e); - FatalAssert(b, "Should be valid"); + b = check(vc, e); + EXPECT(b, "Should be valid"); // Check x = y -> f(x) = f(y) @@ -186,16 +199,16 @@ void test1() Expr fy = vc->funExpr(f, y); e = vc->impliesExpr(vc->eqExpr(x,y),vc->eqExpr(fx, fy)); - IF_DEBUG(b =) check(vc, e); - FatalAssert(b, "Should be valid"); + b = check(vc, e); + EXPECT(b, "Should be valid"); // Check f(x) = f(y) -> x = y e = vc->impliesExpr(vc->eqExpr(fx,fy),vc->eqExpr(x, y)); - IF_DEBUG(int scopeLevel = vc->scopeLevel();) + int scopeLevel = vc->scopeLevel(); vc->push(); - IF_DEBUG(b =) check(vc, e); - FatalAssert(!b, "Should be invalid"); + b = check(vc, e); + EXPECT(!b, "Should be invalid"); // Get counter-example @@ -211,7 +224,7 @@ void test1() // Reset to initial scope cout << "Resetting" << endl; vc->pop(); - FatalAssert(scopeLevel == vc->scopeLevel(), "scope error"); + EXPECT(scopeLevel == vc->scopeLevel(), "scope error"); cout << "Scope level: " << vc->scopeLevel() << endl << endl; // Check w = x & x = y & y = z & f(x) = f(y) & x = 1 & z = 2 @@ -231,7 +244,7 @@ void test1() cout << endl << "simplify(w) = "; vc->printExpr(vc->simplify(w)); cout << endl; - FatalAssert(vc->simplify(w)==vc->ratExpr(1), "Expected simplify(w) = 1"); + EXPECT(vc->simplify(w)==vc->ratExpr(1), "Expected simplify(w) = 1"); newAssertion(vc, vc->eqExpr(z, vc->ratExpr(2))); assertions.clear(); @@ -247,7 +260,7 @@ void test1() cout << "simplify(w) = "; vc->printExpr(vc->simplify(w)); - FatalAssert(vc->simplify(w)==w, "Expected simplify(w) = w"); + EXPECT(vc->simplify(w)==w, "Expected simplify(w) = w"); cout << endl; assertions.clear(); @@ -274,11 +287,11 @@ void test2() Expr c = vc->varExpr("c", vc->intType()); vc->assertFormula(c.eqExpr(vc->ratExpr(0)) || c.eqExpr(vc->ratExpr(1))); - IF_DEBUG(bool b =) check(vc, vc->leExpr(bexpr, vc->ratExpr(10))); - FatalAssert(b, "Should be valid"); + bool b = check(vc, vc->leExpr(bexpr, vc->ratExpr(10))); + EXPECT(b, "Should be valid"); - IF_DEBUG(b =) check(vc, vc->falseExpr()); - FatalAssert(!b, "Should be invalid"); + b = check(vc, vc->falseExpr()); + EXPECT(!b, "Should be invalid"); vc->returnFromCheck(); // Check x = y -> g(x,y) = g(y,x) @@ -298,8 +311,8 @@ void test2() Expr gyx = vc->funExpr(g, y, x); Expr e = vc->impliesExpr(vc->eqExpr(x,y),vc->eqExpr(gxy, gyx)); - IF_DEBUG(b =) check(vc, e); - FatalAssert(b, "Should be valid"); + b = check(vc, e); + EXPECT(b, "Should be valid"); Op h = vc->createOp("h", realxreal2real); @@ -307,8 +320,8 @@ void test2() Expr hyx = vc->funExpr(h, y, x); e = vc->impliesExpr(vc->eqExpr(x,y),vc->eqExpr(hxy, hyx)); - IF_DEBUG(b =) check(vc, e); - FatalAssert(b, "Should be valid"); + b = check(vc, e); + EXPECT(b, "Should be valid"); } catch(const Exception& e) { exitStatus = 1; @@ -539,8 +552,7 @@ void test5() // hyp.push_back(vc->orExpr(vc->geExpr(qmp, N), vc->leExpr(qmp, zero))); // hyp.push_back(vc->orExpr(vc->geExpr(qmr, N), vc->leExpr(qmr, zero))); - //Expr test = vc->impliesExpr(vc->andExpr(hyp), e); - Expr test = vc->impliesExpr(hyp[0], e); + Expr test = vc->impliesExpr(vc->andExpr(hyp), e); Expr query; cout << "Checking verification condition:" << endl; @@ -800,11 +812,11 @@ void test8() { try { vector vec; vec.push_back(vc->boundVarExpr("x", "x", vc->realType())); - Expr lambda = vc->lambdaExpr(vec, vc->falseExpr());//.getExpr(); + Expr lambda = vc->lambdaExpr(vec, vc->falseExpr()).getExpr(); Expr witness; try { Type t = vc->subtypeType(lambda, witness); - FatalAssert(false, "Typechecking exception expected"); + EXPECT(false, "Typechecking exception expected"); } catch(const TypecheckException&) { // fall through } @@ -1064,14 +1076,14 @@ void test11() cout << "Assert x = y" << endl; vc->assertFormula(xeqy); c = printImpliedLiterals(vc); - FatalAssert(c==3,"Implied literal error 0"); + EXPECT(c==3,"Implied literal error 0"); cout << "Push" << endl; vc->push(); cout << "Assert x /= z" << endl; vc->assertFormula(!xeqz); c = printImpliedLiterals(vc); - FatalAssert(c==4,"Implied literal error 1"); + EXPECT(c==4,"Implied literal error 1"); cout << "Pop" << endl; vc->pop(); @@ -1080,7 +1092,7 @@ void test11() cout << "Assert y /= z" << endl; vc->assertFormula(!yeqz); c = printImpliedLiterals(vc); - FatalAssert(c==4,"Implied literal error 2"); + EXPECT(c==4,"Implied literal error 2"); cout << "Pop" << endl; vc->pop(); @@ -1089,7 +1101,7 @@ void test11() cout << "Assert p(x)" << endl; vc->assertFormula(px); c = printImpliedLiterals(vc); - FatalAssert(c==2,"Implied literal error 3"); + EXPECT(c==2,"Implied literal error 3"); cout << "Pop" << endl; vc->pop(); @@ -1098,7 +1110,7 @@ void test11() cout << "Assert p(y)" << endl; vc->assertFormula(py); c = printImpliedLiterals(vc); - FatalAssert(c==2,"Implied literal error 4"); + EXPECT(c==2,"Implied literal error 4"); cout << "Pop" << endl; vc->pop(); @@ -1110,7 +1122,7 @@ void test11() cout << "Assert y = x" << endl; vc->assertFormula(yeqx); c = printImpliedLiterals(vc); - FatalAssert(c==3,"Implied literal error 5"); + EXPECT(c==3,"Implied literal error 5"); cout << "Pop" << endl; vc->pop(); @@ -1119,11 +1131,11 @@ void test11() cout << "Assert p(x)" << endl; vc->assertFormula(px); c = printImpliedLiterals(vc); - FatalAssert(c==1,"Implied literal error 6"); + EXPECT(c==1,"Implied literal error 6"); cout << "Assert x = y" << endl; vc->assertFormula(xeqy); c = printImpliedLiterals(vc); - FatalAssert(c==4,"Implied literal error 7"); + EXPECT(c==4,"Implied literal error 7"); cout << "Pop" << endl; vc->pop(); @@ -1132,11 +1144,11 @@ void test11() cout << "Assert NOT p(x)" << endl; vc->assertFormula(!px); c = printImpliedLiterals(vc); - FatalAssert(c==1,"Implied literal error 8"); + EXPECT(c==1,"Implied literal error 8"); cout << "Assert x = y" << endl; vc->assertFormula(xeqy); c = printImpliedLiterals(vc); - FatalAssert(c==4,"Implied literal error 9"); + EXPECT(c==4,"Implied literal error 9"); cout << "Pop" << endl; vc->pop(); @@ -1157,12 +1169,12 @@ void test12() Type boolType = vc->boolType(); vc -> push(); int initial_layer = vc->stackLevel(); - IF_DEBUG(int initial_scope =) vc->scopeLevel(); + int initial_scope = vc->scopeLevel(); Expr exprObj_trueID = vc->trueExpr(); Expr exprObj_falseID = vc->notExpr(vc->trueExpr()); vc->popto(initial_layer); - FatalAssert(vc->scopeLevel() == initial_scope, "Expected no change"); - FatalAssert(vc->stackLevel() == initial_layer, "Expected no change"); + EXPECT(vc->scopeLevel() == initial_scope, "Expected no change"); + EXPECT(vc->stackLevel() == initial_layer, "Expected no change"); // TODO: what happens if we push and then popscope? } catch(const Exception& e) { exitStatus = 1; @@ -1269,7 +1281,7 @@ void test15() { vector assertions; cout << "Scope level: " << vc->scopeLevel() << endl; cout << "Counter-example:" << endl; - vc->getCounterExample(assertions); + //vc->getCounterExample(assertions); for (unsigned i = 0; i < assertions.size(); ++i) { vc->printExpr(assertions[i]); } @@ -1346,7 +1358,7 @@ void test15() { cout << " -- no, with counter examples as " << endl; vector assert2; - vc->getCounterExample(assert2); + //vc->getCounterExample(assert2); for (unsigned int i = 0; i < assert2.size(); i ++) vc->printExpr(assert2[i]); } @@ -1381,7 +1393,7 @@ void test16() { cout << "Scope level: " << vc->scopeLevel() << endl; cout << "Counter-example:" << endl; vc->getCounterExample(assertions); - FatalAssert(assertions.size() > 0, "Expected non-empty counter-example"); + EXPECT(assertions.size() > 0, "Expected non-empty counter-example"); for (unsigned i = 0; i < assertions.size(); ++i) { vc->printExpr(assertions[i]); } @@ -1397,7 +1409,7 @@ void test16() { for(; it!= end; it++) { Expr eq; if(it->first.getType().isBool()) { - FatalAssert((it->second).isBoolConst(), + EXPECT((it->second).isBoolConst(), "Bad variable assignement: e = "+(it->first).toString() +"\n\n val = "+(it->second).toString()); if((it->second).isTrue()) @@ -1432,7 +1444,7 @@ void test17() { types.push_back(vc->stringExpr("list")); Type badList = vc->dataType("list", "cons", selectors, types); - FatalAssert(false, "Typechecking exception expected"); + EXPECT(false, "Typechecking exception expected"); } catch(const TypecheckException&) { // fall through } @@ -1461,8 +1473,8 @@ void test17() { Expr cons = vc->datatypeConsExpr("cons", args); Expr sel = vc->datatypeSelExpr("car", cons); - IF_DEBUG(bool b =) check(vc, vc->eqExpr(sel, x)); - FatalAssert(b, "Should be valid"); + bool b = check(vc, vc->eqExpr(sel, x)); + EXPECT(b, "Should be valid"); } delete vc; @@ -1495,7 +1507,7 @@ void test17() { types[0][0].push_back(vc->stringExpr("list1")); vc->dataType(names, constructors, selectors, types, returnTypes); - FatalAssert(false, "Typechecking exception expected"); + EXPECT(false, "Typechecking exception expected"); } catch(const TypecheckException&) { // fall through } @@ -1553,8 +1565,8 @@ void test17() { args.push_back(null); Expr cons1_2 = vc->datatypeConsExpr("cons1", args); - IF_DEBUG(bool b =) check(vc, vc->impliesExpr(hyp, vc->eqExpr(z, cons1_2))); - FatalAssert(b, "Should be valid"); + bool b = check(vc, vc->impliesExpr(hyp, vc->eqExpr(z, cons1_2))); + EXPECT(b, "Should be valid"); } delete vc; @@ -1578,8 +1590,8 @@ void test17() { args.push_back(!vc->eqExpr(y,z)); args.push_back(!vc->eqExpr(x,z)); - IF_DEBUG(bool b =) check(vc, !vc->andExpr(args)); - FatalAssert(b, "Should be valid"); + bool b = check(vc, !vc->andExpr(args)); + EXPECT(b, "Should be valid"); } } catch(const Exception& e) { @@ -1649,7 +1661,8 @@ void test18() vc->push(); try { check(vc, vc->notExpr(vc->eqExpr(zero, null))); - FatalAssert(false, "Should have caught tcc exception"); + // TCCs not supported by CVC4 yet + //EXPECT(false, "Should have caught tcc exception"); } catch(const TypecheckException&) { } vc->pop(); @@ -1659,16 +1672,17 @@ void test18() vc->push(); try { check(vc, spxeqx); - FatalAssert(false, "Should have caught tcc exception"); + // TCCs not supported by CVC4 yet + //EXPECT(false, "Should have caught tcc exception"); } catch(const TypecheckException&) { } vc->pop(); bool b = check(vc, vc->impliesExpr(vc->datatypeTestExpr("succ", x), spxeqx)); - FatalAssert(b, "Should be valid"); + EXPECT(b, "Should be valid"); b = check(vc, vc->orExpr(vc->datatypeTestExpr("zero", x), vc->datatypeTestExpr("succ", x))); - FatalAssert(b, "Should be valid"); + EXPECT(b, "Should be valid"); Expr y = vc->varExpr("y", nat); Expr xeqy = vc->eqExpr(x, y); @@ -1680,16 +1694,16 @@ void test18() Expr sy = vc->datatypeConsExpr("succ", args); Expr sxeqsy = vc->eqExpr(sx,sy); b = check(vc, vc->impliesExpr(xeqy, sxeqsy)); - FatalAssert(b, "Should be valid"); + EXPECT(b, "Should be valid"); b = check(vc, vc->notExpr(vc->eqExpr(sx, zero))); - FatalAssert(b, "Should be valid"); + EXPECT(b, "Should be valid"); b = check(vc, vc->impliesExpr(sxeqsy, xeqy)); - FatalAssert(b, "Should be valid"); + EXPECT(b, "Should be valid"); b = check(vc, vc->notExpr(vc->eqExpr(sx, x))); - FatalAssert(b, "Should be valid"); + EXPECT(b, "Should be valid"); } catch(const Exception& e) { exitStatus = 1; @@ -1736,9 +1750,9 @@ void test19() cout<<"Checking formula "<query(Q); + bool Succ = vc->query(Q); - FatalAssert(Succ, "Expected valid formula"); + EXPECT(Succ, "Expected valid formula"); } catch(const Exception& e) { exitStatus = 1; @@ -1789,7 +1803,7 @@ void test20() { vc->dataType(names, constructors, selectors, types, returnTypes); - FatalAssert(returnTypes[0].card() == CARD_FINITE, "Expected finite"); + EXPECT(returnTypes[0].card() == CARD_FINITE, "Expected finite"); Unsigned size = returnTypes[0].sizeFinite(); Unsigned i = 0; for (; i < size; ++i) { @@ -1815,32 +1829,51 @@ void test21() { Expr x2 = vc->exprFromString("x"); cout << "x1: " << x1; cout << "\nx2: " << x2; - FatalAssert(x1 == x2, "Expected x1 == x2"); + EXPECT(x1 == x2, "Expected x1 == x2"); + + Expr x3 = vc->exprFromString("x", SMTLIB_V2_LANG); + cout << "\nx3: " << x3; + EXPECT(x1 == x3, "Expected x1 == x3"); Expr y1 = vc->varExpr("y",t); Expr y2 = vc->exprFromString("y"); cout << "\ny1: " << y1; cout << "\ny2: " << y2; - FatalAssert(y1 == y2, "Expected y1 == y2"); + EXPECT(y1 == y2, "Expected y1 == y2"); + + Expr y3 = vc->exprFromString("y", SMTLIB_V2_LANG); + cout << "\ny3: " << y3; + EXPECT(y1 == y3, "Expected y1 == y3"); Expr a1 = vc->gtExpr(x1,vc->ratExpr(0,1)); Expr a2 = vc->exprFromString("x > 0"); cout << "\na1: " << a1; cout << "\na2: " << a2; - FatalAssert(a1 == a2, "Expected a1 == a2"); + EXPECT(a1 == a2, "Expected a1 == a2"); + + Expr a3 = vc->exprFromString("(> x 0)", SMTLIB_V2_LANG); + cout << "\na3: " << a3; + EXPECT(a1 == a3, "Expected a1 == a3"); Expr b1 = vc->ltExpr(x1,y1); Expr b2 = vc->exprFromString ("x < y"); cout << "\nb1: " << b1; cout << "\nb2: " << b2; - FatalAssert(b1 == b2, "Expected b1 == b2"); + EXPECT(b1 == b2, "Expected b1 == b2"); + + Expr b3 = vc->exprFromString ("(< x y)", SMTLIB_V2_LANG); + cout << "\nb3: " << b3; + EXPECT(b1 == b3, "Expected b1 == b3"); Expr e1 = a1 && b1; Expr e2 = vc->exprFromString("x > 0 AND x < y"); - cout << "\ne1: " << e1; cout << "\ne2: " << e2; - FatalAssert(e1 == e2, "Expected e1 == e2"); + EXPECT(e1 == e2, "Expected e1 == e2"); + + Expr e3 = vc->exprFromString("(and (> x 0) (< x y))", SMTLIB_V2_LANG); + cout << "\ne3: " << e3; + EXPECT(e1 == e3, "Expected e1 == e3"); } catch(const Exception& e) { exitStatus = 1; cout << "*** Exception caught in test21(): \n" << e << endl; @@ -1868,56 +1901,56 @@ void test22() { patternvv.push_back(patternv); vc->setTriggers(p,patternv); - FatalAssert( eqExprVecVecs(p.getTriggers(), patternvv), + EXPECT( eqExprVecVecs(p.getTriggers(), patternvv), "Expected p.getTriggers() == patternvv: " + p.toString() ); vc->setTriggers(p,patternvv); - FatalAssert( eqExprVecVecs(p.getTriggers(), patternvv), + EXPECT( eqExprVecVecs(p.getTriggers(), patternvv), "Expected p.getTriggers() == patternvv: " + p.toString() ); // [chris 10/4/2009] Not sure why, but this fails // Expr q(vc->exprFromString("FORALL (x:INT) : PATTERN (f(x)) : x < f(x)")); - // FatalAssert( eqExprVecVecs(q.getTriggers(), patternvv), + // EXPECT( eqExprVecVecs(q.getTriggers(), patternvv), // "Expected q.getTriggers() == patternvv" + q.toString()); vector vars; vars.push_back(x); Expr r(vc->forallExpr( vars, vc->ltExpr(x,fx), patternvv )); - FatalAssert( eqExprVecVecs(r.getTriggers(), patternvv), + EXPECT( eqExprVecVecs(r.getTriggers(), patternvv), "Expected r.getTriggers() == patternvv: " + r.toString() ); Expr s(vc->exprFromString("FORALL (x:INT) : x > f(x)")); vc->setTrigger(s,fx); std::vector > trigsvv = s.getTriggers(); - FatalAssert( trigsvv.size() == 1, + EXPECT( trigsvv.size() == 1, "Expected s.getTriggers().size() == 1: " + trigsvv.size() ); std::vector trigsv = trigsvv[0]; - FatalAssert( trigsv.size() == 1, + EXPECT( trigsv.size() == 1, "Expected s.getTriggers()[0].size() == 1: " + trigsv.size() ); - FatalAssert( trigsv[0] == fx, + EXPECT( trigsv[0] == fx, "Expected s.getTriggers()[0][0] == fx: " + (trigsv[0].toString()) ); Expr t(vc->exprFromString("FORALL (x:INT) : x > f(x)")); vc->setMultiTrigger(t,patternv); trigsvv = t.getTriggers(); - FatalAssert( trigsvv.size() == 1, + EXPECT( trigsvv.size() == 1, "Expected t.getTriggers().size() == 1: " + trigsvv.size() ); trigsv = trigsvv[0]; - FatalAssert( trigsv.size() == 1, + EXPECT( trigsv.size() == 1, "Expected t.getTriggers()[0].size() == 1: " + trigsv.size() ); - FatalAssert( trigsv[0] == fx, + EXPECT( trigsv[0] == fx, "Expected t.getTriggers()[0][0] == fx: " + (trigsv[0].toString()) ); } catch(const Exception& e) { @@ -1954,7 +1987,7 @@ void test23() { Expr u(s.substExpr(oldExprs,newExprs)); cout << "u=" << u << "\n"; - FatalAssert( t == u, "Expected t==u" ); + EXPECT( t == u, "Expected t==u" ); } catch(const Exception& e) { exitStatus = 1; cout << "*** Exception caught in test23(): \n" << e << endl; @@ -1979,21 +2012,17 @@ void test24() { cout << p << "\n"; vector > pTriggers(p.getTriggers()); - FatalAssert( pTriggers.size() == 1, - "Expected one trigger set. Found: " + - int2string(pTriggers.size())); - FatalAssert( pTriggers[0].size() == 1, - "Expected one trigger. Found: " + - int2string( pTriggers[0].size())); + EXPECT( pTriggers.size() == 1, + "Actual: " + int2string(pTriggers.size())); + EXPECT( pTriggers[0].size() == 1, + "Actual: " + int2string( pTriggers[0].size())); /* We can't check that the trigger == ax, because x will have * been replaced with a bvar */ - FatalAssert( pTriggers[0][0].getKind() == READ, - "Expected READ expression. Found: " + - pTriggers[0][0].getKind()); - FatalAssert( pTriggers[0][0][0] == a, - "Expected read on array: " + a.toString() + - "\nFound: " + pTriggers[0][0][0].toString() ); + EXPECT( pTriggers[0][0].getKind() == READ, + "Actual: " + int2string(pTriggers[0][0].getKind())); + EXPECT( pTriggers[0][0][0] == a, + "Actual: " + pTriggers[0][0][0].toString() ); Expr aPrime(vc->varExpr("a'",aType)); Expr axPrime(vc->exprFromString("a'[x]")); @@ -2006,18 +2035,17 @@ void test24() { cout << q << "\n"; vector > qTriggers(q.getTriggers()); - FatalAssert( qTriggers.size() == 1, - "Expected one trigger set. Found: " + - int2string(qTriggers.size())); - FatalAssert( qTriggers[0].size() == 1, - "Expected one trigger. Found: " + - int2string( qTriggers[0].size())); - FatalAssert( qTriggers[0][0].getKind() == READ, - "Expected READ expression. Found: " + - qTriggers[0][0].getKind()); - FatalAssert( qTriggers[0][0][0] == aPrime, - "Expected read on array: " + aPrime.toString() + - "\nFound: " + qTriggers[0][0][0].toString() ); + EXPECT( qTriggers.size() == 1, + "Actual: " + + int2string(qTriggers.size())); + EXPECT( qTriggers[0].size() == 1, + "Actual: " + + int2string(qTriggers[0].size())); + EXPECT( qTriggers[0][0].getKind() == READ, + "Actual: " + + int2string(qTriggers[0][0].getKind())); + EXPECT( qTriggers[0][0][0] == aPrime, + "Actual: " + qTriggers[0][0][0].toString() ); } catch(const Exception& e) { exitStatus = 1; cout << "*** Exception caught in test24(): \n" << e << endl; @@ -2042,7 +2070,7 @@ void test25() { Expr w = vc->ratExpr(-1,10); cout << "-1 over 10 (ints): " << w << endl; - FatalAssert(x == y && y == z && z == w, "Error in rational constants"); + EXPECT(x == y && y == z && z == w, "Error in rational constants"); } catch(const Exception& e) { exitStatus = 1; @@ -2064,17 +2092,17 @@ void test26() { Expr e2 = vc->newBVSHL(x, vc->newBVConstExpr(16, 32)); bool b = check(vc, vc->eqExpr(e1, e2)); - FatalAssert(b, "Should be valid"); + EXPECT(b, "Should be valid"); e1 = vc->newFixedRightShiftExpr(x, 16); e2 = vc->newBVLSHR(x, vc->newBVConstExpr(16, 32)); b = check(vc, vc->eqExpr(e1, e2)); - FatalAssert(b, "Should be valid"); + EXPECT(b, "Should be valid"); e2 = vc->newBVASHR(x, vc->newBVConstExpr(16, 32)); b = check(vc, vc->eqExpr(e1, e2)); - FatalAssert(!b, "Should be invalid"); + EXPECT(!b, "Should be invalid"); } catch(const Exception& e) { exitStatus = 1; @@ -2090,6 +2118,7 @@ int main(int argc, char** argv) if (argc > 1) regressLevel = atoi(argv[1]); cout << "Running API test, regress level = " << regressLevel << endl; exitStatus = 0; + try { // [MGD for CVC4] This is a CVC3 test, and many tests had to be commented // out for CVC4 since the functionality is either unsupported or @@ -2099,22 +2128,22 @@ int main(int argc, char** argv) // not clear how to implement Type::getExpr(), and Exprs and Ops are // indistinguishable, so getOp() and getOpExpr() have the same result. - //cout << "\n}\ntest26(): {" << endl; - //test26(); + cout << "\n}\ntest26(): {" << endl; + test26(); //cout << "\ntest(): {" << endl; //test(); - //cout << "\n}\ntest1(): {" << endl; - //test1(); + cout << "\n}\ntest1(): {" << endl; + test1(); cout << "\n}\n\ntest2(): {" << endl; test2(); cout << "\n}\n\ntest3(): {" << endl; test3(); cout << "\n}\n\ntest4(): {" << endl; test4(); - if (regressLevel > 0) { - cout << "\n}\n\ntest5(): {" << endl; - test5(); - } + //if (regressLevel > 0) { + // cout << "\n}\n\ntest5(): {" << endl; + // test5(); + //} //cout << "\n}\n\ntest6(): {" << endl; //test6(); cout << "\n}\n\ntest7(): {" << endl; @@ -2134,8 +2163,8 @@ int main(int argc, char** argv) test10(); } - cout << "\ntest11(): {" << endl; - test11(); + //cout << "\ntest11(): {" << endl; + //test11(); cout << "\n}\ntest12(): {" << endl; test12(); cout << "\n}\ntest13(): {" << endl; @@ -2150,10 +2179,10 @@ int main(int argc, char** argv) test17(); cout << "\n}\ntest18(): {" << endl; test18(); - //cout << "\n}\ntest19(): {" << endl; - //test19(); - //cout << "\ntest20(): {" << endl; - //test20(); + cout << "\n}\ntest19(): {" << endl; + test19(); + cout << "\ntest20(): {" << endl; + test20(); cout << "\n}\ntest21(): {" << endl; test21(); //cout << "\n}\ntest22(): {" << endl; @@ -2165,6 +2194,7 @@ int main(int argc, char** argv) cout << "\n}\ntest25(): {" << endl; test25(); + /* if (regressLevel > 1) { cout << "\n}\ntestgeorge1(): {" << endl; testgeorge1(); @@ -2177,6 +2207,7 @@ int main(int argc, char** argv) cout << "\n}\ntestgeorge5(): {" << endl; testgeorge5(); } + */ cout << "\n}" << endl; } catch(const Exception& e) {