diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-28 01:10:16 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-28 01:10:16 +0000 |
commit | cf287f593931a1c4fc141e18845b4c5d36879889 (patch) | |
tree | 4dad0f555b7db01fbeedcd9eace394cd8f7a0fb4 /src | |
parent | b7b1c1d99ffa333704af2c8ecd60b1af8833a28b (diff) |
Improved compatibility layer, now supports quantifiers. Also incorporates
numerous bugfixes, and the cvc3 system test is enabled.
Diffstat (limited to 'src')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 285 | ||||
-rw-r--r-- | src/compat/cvc3_compat.h | 8 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 39 | ||||
-rw-r--r-- | src/expr/expr_template.h | 9 | ||||
-rw-r--r-- | src/expr/type.cpp | 2 | ||||
-rw-r--r-- | src/expr/type.h | 2 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 7 | ||||
-rw-r--r-- | src/options/Makefile.am | 4 | ||||
-rw-r--r-- | src/options/base_options | 6 | ||||
-rw-r--r-- | src/options/base_options_handlers.h | 26 | ||||
-rw-r--r-- | src/options/option_exception.h | 2 | ||||
-rw-r--r-- | src/smt/options | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 34 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 10 | ||||
-rw-r--r-- | src/smt/smt_options_template.cpp | 4 | ||||
-rw-r--r-- | src/theory/arrays/kinds | 7 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_type_rules.h | 23 | ||||
-rw-r--r-- | src/theory/bv/kinds | 5 | ||||
-rw-r--r-- | src/util/Makefile.am | 54 | ||||
-rw-r--r-- | src/util/rational_cln_imp.h | 4 | ||||
-rw-r--r-- | src/util/rational_gmp_imp.h | 2 |
21 files changed, 348 insertions, 187 deletions
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<CVC4::ExprManager*, ValidityChecker*> s_validityCheckers; + static std::hash_map<Type, Expr, CVC4::TypeHashFunction> s_typeToExpr; static std::hash_map<Expr, Type, CVC4::ExprHashFunction> 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> > Expr::getTriggers() const { - return vector< vector<Expr> >(); + CheckArgument(isClosure(), *this, __PRETTY_FUNCTION__, "getTriggers() called on non-closure expr"); + if(getNumChildren() < 3) { + // no triggers for this quantifier + return vector< vector<Expr> >(); + } else { + // get the triggers from the third child + Expr triggers = (*this)[2]; + vector< vector<Expr> > v; + for(const_iterator i = triggers.begin(); i != triggers.end(); ++i) { + v.push_back(vector<Expr>()); + 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<ExprManager*>(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, "<internal>").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<ExprManager*>(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, "<internal>").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build(); } ValidityChecker::~ValidityChecker() { + for(vector<Expr>::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<ValidityChecker*>::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<std::string>& selectors, const std::vector<Expr>& types) { - AlwaysAssert(selectors.size() == types.size()); + CheckArgument(selectors.size() == types.size(), types, "expected selectors and types vectors to be of equal length"); vector<string> cv; vector< vector<string> > sv; vector< vector<Expr> > tv; @@ -1081,8 +1135,8 @@ Type ValidityChecker::dataType(const std::string& name, const std::vector<std::string>& constructors, const std::vector<std::vector<std::string> >& selectors, const std::vector<std::vector<Expr> >& 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<string> nv; vector< vector<string> > cv; vector< vector< vector<string> > > sv; @@ -1103,19 +1157,19 @@ void ValidityChecker::dataType(const std::vector<std::string>& names, const std::vector<std::vector<std::vector<Expr> > >& types, std::vector<Type>& 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<CVC4::Datatype> 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<string>())); @@ -1137,12 +1191,17 @@ void ValidityChecker::dataType(const std::vector<std::string>& names, for(vector<CVC4::DatatypeType>::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<Expr>& children) { - const vector<CVC4::Expr>& v = - *reinterpret_cast<const vector<CVC4::Expr>*>(&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<const vector<CVC4::Expr>*>(&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<Expr>& children) { - const vector<CVC4::Expr>& v = - *reinterpret_cast<const vector<CVC4::Expr>*>(&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<const vector<CVC4::Expr>*>(&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<Expr>& children) { + CheckArgument(children.size() > 1, children, "it makes no sense to create a `distinct' expression with only one child"); const vector<CVC4::Expr>& v = *reinterpret_cast<const vector<CVC4::Expr>*>(&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<Expr>& children) { - const vector<CVC4::Expr>& v = - *reinterpret_cast<const vector<CVC4::Expr>*>(&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<const vector<CVC4::Expr>*>(&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<Expr>& 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<Expr>::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<Expr>& 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<Expr>::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<Expr>& 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<Expr>::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<Expr>& 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<Expr>::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<Expr>& 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<Expr>& kids) { + // BITVECTOR_PLUS is not N-ary in CVC4 + CheckArgument(kids.size() > 1, kids, "BITVECTOR_PLUS must have at least 2 children"); + std::vector<Expr>::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<Expr>& vars, const Expr& body) { - Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); + Expr boundVarList = d_em->mkExpr(CVC4::kind::BOUND_VAR_LIST, *reinterpret_cast<const std::vector<CVC4::Expr>*>(&vars)); + return d_em->mkExpr(CVC4::kind::FORALL, boundVarList, body); } Expr ValidityChecker::forallExpr(const std::vector<Expr>& 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<const std::vector<CVC4::Expr>*>(&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<Expr>& vars, const Expr& body, const std::vector<Expr>& triggers) { - Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); + // set of triggers + Expr boundVarList = d_em->mkExpr(CVC4::kind::BOUND_VAR_LIST, *reinterpret_cast<const std::vector<CVC4::Expr>*>(&vars)); + std::vector<CVC4::Expr> pats; + for(std::vector<Expr>::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<Expr>& vars, const Expr& body, const std::vector<std::vector<Expr> >& 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<const std::vector<CVC4::Expr>*>(&vars)); + std::vector<CVC4::Expr> pats; + for(std::vector< std::vector<Expr> >::const_iterator i = triggers.begin(); i != triggers.end(); ++i) { + pats.push_back(d_em->mkExpr(CVC4::kind::INST_PATTERN, *reinterpret_cast<const std::vector<CVC4::Expr>*>(&*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<std::vector<Expr> > & 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<Expr>& 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<Expr>& multiTrigger) { - Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); } Expr ValidityChecker::existsExpr(const std::vector<Expr>& vars, const Expr& body) { - Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); + Expr boundVarList = d_em->mkExpr(CVC4::kind::BOUND_VAR_LIST, *reinterpret_cast<const std::vector<CVC4::Expr>*>(&vars)); + return d_em->mkExpr(CVC4::kind::EXISTS, boundVarList, body); } Op ValidityChecker::lambdaExpr(const std::vector<Expr>& 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<Expr>& 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<std::vector<CVC4::Expr>*>(&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<CVC4::ExprManager*, CVC4::ExprManagerMapCollection> d_emmc; + std::set<ValidityChecker*> d_reverseEmmc; CVC4::SmtEngine* d_smt; CVC4::parser::Parser* d_parserContext; + std::vector<Expr> d_exprTypeMapRemove; + + friend class Type; // to reach in to d_exprTypeMapRemove typedef std::hash_map<std::string, const CVC4::Datatype*, CVC4::StringHashFunction> ConstructorMap; typedef std::hash_map<std::string, std::pair<const CVC4::Datatype*, std::string>, 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<Node> 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<Iterator> mkNodeIteratorAdaptor(Iterator i) { Expr Expr::substitute(const std::vector<Expr> exes, const std::vector<Expr>& 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<Iterator> mkNodePairIteratorAdaptor(Iterat } Expr Expr::substitute(const std::hash_map<Expr, Expr, ExprHashFunction> 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<Node::iterator*>(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<Node::iterator*>(d_iterator); } + d_exprManager = it.d_exprManager; + ExprManagerScope ems(*d_exprManager); d_iterator = new Node::iterator(*reinterpret_cast<Node::iterator*>(it.d_iterator)); return *this; } Expr::const_iterator::~const_iterator() { if(d_iterator != NULL) { + ExprManagerScope ems(*d_exprManager); delete reinterpret_cast<Node::iterator*>(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<Node::iterator*>(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<Node::iterator*>(d_iterator); return it; } Expr Expr::const_iterator::operator*() const { Assert(d_iterator != NULL); + ExprManagerScope ems(*d_exprManager); return (**reinterpret_cast<Node::iterator*>(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<std::input_iterator_tag, Expr> { + 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 <iostream> option out std::ostream* :default &std::cout :include <iostream> option err std::ostream* :default &std::cerr :include <iostream> -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<Expr> SmtEngine::getAssertions() throw ModalException(msg); } Assert(d_assertionList != NULL); + // copy the result out return vector<Expr>(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) { |