diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-03-01 14:48:04 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-03-01 14:48:04 +0000 |
commit | 45a138c326da72890bf889a3670aad503ef4aa1e (patch) | |
tree | fa0c9a8497d0b33f78a9f19212152a61392825cc /src/compat | |
parent | 8c0b2d6db32103268f84d89c0d0545c7eb504069 (diff) |
Partial merge from kind-backend branch, including Minisat and CNF work to
support incrementality.
Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.
Expected performance change negligible; slightly better on memory:
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!
Diffstat (limited to 'src/compat')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 73 |
1 files changed, 57 insertions, 16 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index a30ccb27d..83c33c7ab 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -25,6 +25,8 @@ #include "util/integer.h" #include "util/bitvector.h" #include "util/hash.h" +#include "util/subrange_bound.h" +#include "util/predicate.h" #include "parser/parser.h" #include "parser/parser_builder.h" @@ -184,7 +186,7 @@ bool Type::isBool() const { } bool Type::isSubtype() const { - return false; + return isPredicateSubtype(); } Cardinality Type::card() const { @@ -980,11 +982,21 @@ Type ValidityChecker::intType() { } Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) { - Unimplemented("Subranges not supported by CVC4 yet (sorry!)"); + bool noLowerBound = l.getType().isString() && l.getConst<string>() == "_NEGINF"; + bool noUpperBound = r.getType().isString() && r.getConst<string>() == "_POSINF"; + CheckArgument(noLowerBound || l.getKind() == CVC4::kind::CONST_INTEGER, l); + CheckArgument(noUpperBound || r.getKind() == CVC4::kind::CONST_INTEGER, r); + CVC4::SubrangeBound bl = noLowerBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(l.getConst<Integer>()); + CVC4::SubrangeBound br = noUpperBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(r.getConst<Integer>()); + return d_em->mkSubrangeType(CVC4::SubrangeBounds(bl, br)); } Type ValidityChecker::subtypeType(const Expr& pred, const Expr& witness) { - Unimplemented("Predicate subtyping not supported by CVC4 yet (sorry!)"); + if(witness.isNull()) { + return d_em->mkPredicateSubtype(pred); + } else { + return d_em->mkPredicateSubtype(pred, witness); + } } Type ValidityChecker::tupleType(const Type& type0, const Type& type1) { @@ -1172,15 +1184,29 @@ Type ValidityChecker::getType(const Expr& e) { } Type ValidityChecker::getBaseType(const Expr& e) { - Type t = d_em->getType(e); - return t.isInteger() ? Type(d_em->realType()) : t; + return getBaseType(e.getType()); } Type ValidityChecker::getBaseType(const Type& t) { - return t.isInteger() ? Type(d_em->realType()) : t; + Type type = t; + while(type.isPredicateSubtype()) { + type = CVC4::PredicateSubtype(type).getBaseType(); + } + // We might still be a (primitive) subtype. Check the types that can + // form the base of such a type. + if(type.isReal()) { + return d_em->realType(); + } + Assert(!type.isInteger());// should be handled by Real + if(type.isBoolean()) { + return d_em->booleanType(); + } + return type; } Expr ValidityChecker::getTypePred(const Type&t, const Expr& e) { + // This function appears to be TCC-related---it doesn't just get the pred of a + // subtype predicate, but returns a predicate describing the type. Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); } @@ -1189,42 +1215,52 @@ Expr ValidityChecker::stringExpr(const std::string& str) { } Expr ValidityChecker::idExpr(const std::string& name) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + // represent as a string expr, CVC4 doesn't have id exprs + return d_em->mkConst(name); } Expr ValidityChecker::listExpr(const std::vector<Expr>& kids) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + // list exprs aren't supported by CVC4; make a tuple if two or more + CheckArgument(kids.size() > 0, kids); + return (kids.size() == 1) ? kids[0] : Expr(d_em->mkExpr(CVC4::kind::TUPLE, vector<CVC4::Expr>(kids.begin(), kids.end()))); } Expr ValidityChecker::listExpr(const Expr& e1) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + // list exprs aren't supported by CVC4; just return e1 + return e1; } Expr ValidityChecker::listExpr(const Expr& e1, const Expr& e2) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + // list exprs aren't supported by CVC4; just return a tuple + return d_em->mkExpr(CVC4::kind::TUPLE, e1, e2); } Expr ValidityChecker::listExpr(const Expr& e1, const Expr& e2, const Expr& e3) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + // list exprs aren't supported by CVC4; just return a tuple + return d_em->mkExpr(CVC4::kind::TUPLE, e1, e2, e3); } Expr ValidityChecker::listExpr(const std::string& op, const std::vector<Expr>& kids) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + // list exprs aren't supported by CVC4; just return a tuple + return d_em->mkExpr(CVC4::kind::TUPLE, d_em->mkConst(op), vector<CVC4::Expr>(kids.begin(), kids.end())); } Expr ValidityChecker::listExpr(const std::string& op, const Expr& e1) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + // list exprs aren't supported by CVC4; just return a tuple + return d_em->mkExpr(CVC4::kind::TUPLE, d_em->mkConst(op), e1); } Expr ValidityChecker::listExpr(const std::string& op, const Expr& e1, const Expr& e2) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + // list exprs aren't supported by CVC4; just return a tuple + return d_em->mkExpr(CVC4::kind::TUPLE, d_em->mkConst(op), e1, e2); } Expr ValidityChecker::listExpr(const std::string& op, const Expr& e1, const Expr& e2, const Expr& e3) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + // list exprs aren't supported by CVC4; just return a tuple + return d_em->mkExpr(CVC4::kind::TUPLE, d_em->mkConst(op), e1, e2, e3); } void ValidityChecker::printExpr(const Expr& e) { @@ -1340,7 +1376,12 @@ Op ValidityChecker::createOp(const std::string& name, const Type& type) { Op ValidityChecker::createOp(const std::string& name, const Type& type, const Expr& def) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + CheckArgument(def.getType() == type, type, + "Type mismatch in ValidityChecker::createOp(): `%s' defined to an " + "expression of type %s but ascribed as type %s", name.c_str(), + def.getType().toString().c_str(), type.toString().c_str()); + d_parserContext->defineFunction(name, def); + return def; } Op ValidityChecker::lookupOp(const std::string& name, Type* type) { |