From: Morgan Deters Date: Thu, 1 Mar 2012 14:48:04 +0000 (+0000) Subject: Partial merge from kind-backend branch, including Minisat and CNF work to X-Git-Tag: cvc5-1.0.0~8291 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=45a138c326da72890bf889a3670aad503ef4aa1e;p=cvc5.git 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! --- 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() == "_NEGINF"; + bool noUpperBound = r.getType().isString() && r.getConst() == "_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()); + CVC4::SubrangeBound br = noUpperBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(r.getConst()); + 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& 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(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& 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(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) { diff --git a/src/context/context.cpp b/src/context/context.cpp index 2b220d5b4..abb1575d4 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -62,7 +62,7 @@ Context::~Context() throw(AssertionException) { void Context::push() { Trace("pushpop") << std::string(2 * getLevel(), ' ') << "Push [to " - << getLevel() + 1 << "] {" << std::endl; + << getLevel() + 1 << "] { " << this << std::endl; // Create a new memory region d_pCMM->push(); @@ -106,7 +106,7 @@ void Context::pop() { } Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop [to " - << getLevel() << "]" << std::endl; + << getLevel() << "] " << this << std::endl; } diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 8d089901b..3dac28e11 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -494,10 +494,14 @@ Expr DefineFunctionCommand::getFormula() const throw() { void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() { //Dump("declarations") << *this << endl; -- done by SmtEngine - if(!d_func.isNull()) { - smtEngine->defineFunction(d_func, d_formals, d_formula); + try { + if(!d_func.isNull()) { + smtEngine->defineFunction(d_func, d_formals, d_formula); + } + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); } - d_commandStatus = CommandSuccess::instance(); } Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 46a7bb82c..533a4dd7f 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -97,24 +97,33 @@ ExprManager::ExprManager(const Options& options) : #endif } -ExprManager::~ExprManager() { -#ifdef CVC4_STATISTICS_ON +ExprManager::~ExprManager() throw() { NodeManagerScope nms(d_nodeManager); - for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { - if (d_exprStatistics[i] != NULL) { - StatisticsRegistry::unregisterStat(d_exprStatistics[i]); - delete d_exprStatistics[i]; + + try { + +#ifdef CVC4_STATISTICS_ON + for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { + if (d_exprStatistics[i] != NULL) { + StatisticsRegistry::unregisterStat(d_exprStatistics[i]); + delete d_exprStatistics[i]; + } } - } - for (unsigned i = 0; i <= LAST_TYPE; ++ i) { - if (d_exprStatisticsVars[i] != NULL) { - StatisticsRegistry::unregisterStat(d_exprStatisticsVars[i]); - delete d_exprStatisticsVars[i]; + for (unsigned i = 0; i <= LAST_TYPE; ++ i) { + if (d_exprStatisticsVars[i] != NULL) { + StatisticsRegistry::unregisterStat(d_exprStatisticsVars[i]); + delete d_exprStatisticsVars[i]; + } } - } #endif - delete d_nodeManager; - delete d_ctxt; + + delete d_nodeManager; + delete d_ctxt; + + } catch(Exception& e) { + Warning() << "CVC4 threw an exception during cleanup." << std::endl + << e << std::endl; + } } const Options* ExprManager::getOptions() const { @@ -697,6 +706,39 @@ SortConstructorType ExprManager::mkSortConstructor(const std::string& name, new TypeNode(d_nodeManager->mkSortConstructor(name, arity)))); } +Type ExprManager::mkPredicateSubtype(Expr lambda) + throw(TypeCheckingException) { + NodeManagerScope nms(d_nodeManager); + try { + return PredicateSubtype(Type(d_nodeManager, + new TypeNode(d_nodeManager->mkPredicateSubtype(lambda)))); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Type ExprManager::mkPredicateSubtype(Expr lambda, Expr witness) + throw(TypeCheckingException) { + NodeManagerScope nms(d_nodeManager); + try { + return PredicateSubtype(Type(d_nodeManager, + new TypeNode(d_nodeManager->mkPredicateSubtype(lambda, witness)))); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Type ExprManager::mkSubrangeType(const SubrangeBounds& bounds) + throw(TypeCheckingException) { + NodeManagerScope nms(d_nodeManager); + try { + return SubrangeType(Type(d_nodeManager, + new TypeNode(d_nodeManager->mkSubrangeType(bounds)))); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + /** * Get the type for the given Expr and optionally do type checking. * diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 2abd05821..bf9bfbb38 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -26,6 +26,7 @@ #include "expr/kind.h" #include "expr/type.h" #include "expr/expr.h" +#include "util/subrange_bound.h" ${includes} @@ -33,7 +34,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 37 "${template}" +#line 38 "${template}" namespace CVC4 { @@ -119,7 +120,7 @@ public: * any expression references that used to be managed by this expression * manager and are left-over are bad. */ - ~ExprManager(); + ~ExprManager() throw(); /** Get this node manager's options */ const Options* getOptions() const; @@ -403,9 +404,34 @@ public: SortConstructorType mkSortConstructor(const std::string& name, size_t arity) const; + /** + * Make a predicate subtype type defined by the given LAMBDA + * expression. A TypeCheckingException can be thrown if lambda is + * not a LAMBDA, or is ill-typed, or if CVC4 fails at proving that + * the resulting predicate subtype is inhabited. + */ + Type mkPredicateSubtype(Expr lambda) + throw(TypeCheckingException); + + /** + * Make a predicate subtype type defined by the given LAMBDA + * expression and whose non-emptiness is witnessed by the given + * witness. A TypeCheckingException can be thrown if lambda is not + * a LAMBDA, or is ill-typed, or if the witness is not a witness or + * ill-typed. + */ + Type mkPredicateSubtype(Expr lambda, Expr witness) + throw(TypeCheckingException); + + /** + * Make an integer subrange type as defined by the argument. + */ + Type mkSubrangeType(const SubrangeBounds& bounds) + throw(TypeCheckingException); + /** Get the type of an expression */ Type getType(Expr e, bool check = false) - throw (TypeCheckingException); + throw(TypeCheckingException); // variables are special, because duplicates are permitted Expr mkVar(const std::string& name, Type type); @@ -421,6 +447,7 @@ public: /** Returns the maximum arity of the given kind. */ static unsigned maxArity(Kind kind); + };/* class ExprManager */ ${mkConst_instantiations} diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index c510ce381..d0f5fde9e 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -76,7 +76,8 @@ TypeCheckingException::~TypeCheckingException() throw() { } void TypeCheckingException::toStream(std::ostream& os) const throw() { - os << "Error type-checking " << d_expr << ": " << d_msg << endl << *d_expr; + os << "Error during type checking: " << d_msg << endl + << "The ill-typed expression: " << *d_expr; } Expr TypeCheckingException::getExpression() const throw() { diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 695e572ab..e303a9e58 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -36,7 +36,7 @@ TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () { } void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const throw() { - os << "Error type-checking " << d_node << ": " << d_msg << std::endl << *d_node; + os << "Error during type checking: " << d_msg << std::endl << *d_node << endl << "The ill-typed expression: " << *d_node; } NodeTemplate TypeCheckingExceptionPrivate::getNode() const throw() { diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index c647e128c..a2fddadfc 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -29,6 +29,7 @@ #include #include +#include #include using namespace std; @@ -235,14 +236,15 @@ void NodeManager::reclaimZombies() { }/* NodeManager::reclaimZombies() */ TypeNode NodeManager::getType(TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - // Many theories' type checkers call Node::getType() directly. - // This is incorrect, since "this" might not be the caller's - // curent node manager. Rather than force the individual typecheckers - // not to do this (by policy, which would be imperfect and lead - // to hard-to-find bugs, which it has in the past), we just - // set this node manager to be current for the duration of this - // check. + throw(TypeCheckingExceptionPrivate, AssertionException) { + + // Many theories' type checkers call Node::getType() directly. This + // is incorrect, since "this" might not be the caller's curent node + // manager. Rather than force the individual typecheckers not to do + // this (by policy, which would be imperfect and lead to + // hard-to-find bugs, which it has in the past), we just set this + // node manager to be current for the duration of this check. + // NodeManagerScope nms(this); TypeNode typeNode; @@ -321,4 +323,51 @@ TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor, return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts); } +TypeNode NodeManager::mkPredicateSubtype(Expr lambda) + throw(TypeCheckingExceptionPrivate) { + + Node lambdan = Node::fromExpr(lambda); + + if(lambda.isNull()) { + throw TypeCheckingExceptionPrivate(lambdan, "cannot make a predicate subtype based on null expression"); + } + + TypeNode tn = lambdan.getType(); + if(! tn.isPredicateLike() || + tn.getArgTypes().size() != 1) { + std::stringstream ss; + ss << Expr::setlanguage(Options::current()->outputLanguage) + << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'"; + throw TypeCheckingExceptionPrivate(lambdan, ss.str()); + } + + return TypeNode(mkTypeConst(Predicate(lambda))); +} + +TypeNode NodeManager::mkPredicateSubtype(Expr lambda, Expr witness) + throw(TypeCheckingExceptionPrivate) { + + Node lambdan = Node::fromExpr(lambda); + + if(lambda.isNull()) { + throw TypeCheckingExceptionPrivate(lambdan, "cannot make a predicate subtype based on null expression"); + } + + TypeNode tn = lambdan.getType(); + if(! tn.isPredicateLike() || + tn.getArgTypes().size() != 1) { + std::stringstream ss; + ss << Expr::setlanguage(Options::current()->outputLanguage) + << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'"; + throw TypeCheckingExceptionPrivate(lambdan, ss.str()); + } + + return TypeNode(mkTypeConst(Predicate(lambda, witness))); +} + +TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds) + throw(TypeCheckingExceptionPrivate) { + return TypeNode(mkTypeConst(bounds)); +} + }/* CVC4 namespace */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 704e930b5..da999cc82 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -38,6 +38,7 @@ #include "expr/metakind.h" #include "expr/node_value.h" #include "context/context.h" +#include "util/subrange_bound.h" #include "util/configuration_private.h" #include "util/tls.h" #include "util/options.h" @@ -661,6 +662,31 @@ public: /** Make a new sort with the given name and arity. */ inline TypeNode mkSortConstructor(const std::string& name, size_t arity); + /** + * Make a predicate subtype type defined by the given LAMBDA + * expression. A TypeCheckingExceptionPrivate can be thrown if + * lambda is not a LAMBDA, or is ill-typed, or if CVC4 fails at + * proving that the resulting predicate subtype is inhabited. + */ + TypeNode mkPredicateSubtype(Expr lambda) + throw(TypeCheckingExceptionPrivate); + + /** + * Make a predicate subtype type defined by the given LAMBDA + * expression and whose non-emptiness is witnessed by the given + * witness. A TypeCheckingExceptionPrivate can be thrown if lambda + * is not a LAMBDA, or is ill-typed, or if the witness is not a + * witness or ill-typed. + */ + TypeNode mkPredicateSubtype(Expr lambda, Expr witness) + throw(TypeCheckingExceptionPrivate); + + /** + * Make an integer subrange type as defined by the argument. + */ + TypeNode mkSubrangeType(const SubrangeBounds& bounds) + throw(TypeCheckingExceptionPrivate); + /** * Get the type for the given node and optionally do type checking. * @@ -687,7 +713,7 @@ public: * (default: false) */ TypeNode getType(TNode n, bool check = false) - throw (TypeCheckingExceptionPrivate, AssertionException); + throw(TypeCheckingExceptionPrivate, AssertionException); /** * Convert a node to an expression. Uses the ExprManager @@ -944,10 +970,15 @@ inline TypeNode NodeManager::mkBitVectorType(unsigned size) { inline TypeNode NodeManager::mkArrayType(TypeNode indexType, TypeNode constituentType) { - CheckArgument(!indexType.isFunctionLike(), domain, + CheckArgument(!indexType.isNull(), indexType, + "unexpected NULL index type"); + CheckArgument(!constituentType.isNull(), constituentType, + "unexpected NULL constituent type"); + CheckArgument(!indexType.isFunctionLike(), indexType, "cannot index arrays by a function-like type"); - CheckArgument(!constituentType.isFunctionLike(), domain, + CheckArgument(!constituentType.isFunctionLike(), constituentType, "cannot store function-like types in arrays"); +Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl; return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType); } diff --git a/src/expr/type.cpp b/src/expr/type.cpp index a901af73a..eaf10ba20 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -103,26 +103,32 @@ Type& Type::operator=(const Type& t) { } bool Type::operator==(const Type& t) const { + NodeManagerScope nms(d_nodeManager); return *d_typeNode == *t.d_typeNode; } bool Type::operator!=(const Type& t) const { + NodeManagerScope nms(d_nodeManager); return *d_typeNode != *t.d_typeNode; } bool Type::operator<(const Type& t) const { + NodeManagerScope nms(d_nodeManager); return *d_typeNode < *t.d_typeNode; } bool Type::operator<=(const Type& t) const { + NodeManagerScope nms(d_nodeManager); return *d_typeNode <= *t.d_typeNode; } bool Type::operator>(const Type& t) const { + NodeManagerScope nms(d_nodeManager); return *d_typeNode > *t.d_typeNode; } bool Type::operator>=(const Type& t) const { + NodeManagerScope nms(d_nodeManager); return *d_typeNode >= *t.d_typeNode; } @@ -375,13 +381,39 @@ bool Type::isSortConstructor() const { return d_typeNode->isSortConstructor(); } -/** Cast to a sort type */ +/** Cast to a sort constructor type */ Type::operator SortConstructorType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isNull() || isSortConstructor()); return SortConstructorType(*this); } +/** Is this a predicate subtype */ +bool Type::isPredicateSubtype() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isPredicateSubtype(); +} + +/** Cast to a predicate subtype */ +Type::operator PredicateSubtype() const throw(AssertionException) { + NodeManagerScope nms(d_nodeManager); + Assert(isNull() || isPredicateSubtype()); + return PredicateSubtype(*this); +} + +/** Is this an integer subrange */ +bool Type::isSubrange() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isSubrange(); +} + +/** Cast to a predicate subtype */ +Type::operator SubrangeType() const throw(AssertionException) { + NodeManagerScope nms(d_nodeManager); + Assert(isNull() || isSubrange()); + return SubrangeType(*this); +} + /** Is this a kind type (i.e., the type of a type)? */ bool Type::isKind() const { NodeManagerScope nms(d_nodeManager); @@ -543,6 +575,18 @@ SortConstructorType::SortConstructorType(const Type& t) Assert(isNull() || isSortConstructor()); } +PredicateSubtype::PredicateSubtype(const Type& t) + throw(AssertionException) : + Type(t) { + Assert(isNull() || isPredicateSubtype()); +} + +SubrangeType::SubrangeType(const Type& t) + throw(AssertionException) : + Type(t) { + Assert(isNull() || isSubrange()); +} + unsigned BitVectorType::getSize() const { return d_typeNode->getBitVectorSize(); } @@ -648,6 +692,21 @@ BooleanType TesterType::getRangeType() const { return BooleanType(makeType(d_nodeManager->booleanType())); } +Expr PredicateSubtype::getPredicate() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getSubtypePredicate().toExpr(); +} + +Type PredicateSubtype::getBaseType() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getSubtypeBaseType().toType(); +} + +SubrangeBounds SubrangeType::getSubrangeBounds() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getSubrangeBounds(); +} + size_t TypeHashFunction::operator()(const Type& t) const { return TypeNodeHashFunction()(NodeManager::fromType(t)); } diff --git a/src/expr/type.h b/src/expr/type.h index 34cc925f6..76fccb37b 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -28,6 +28,7 @@ #include "util/Assert.h" #include "util/cardinality.h" +#include "util/subrange_bound.h" namespace CVC4 { @@ -60,6 +61,8 @@ class TupleType; class KindType; class SortType; class SortConstructorType; +class PredicateSubtype; +class SubrangeType; class Type; /** Strategy for hashing Types */ @@ -404,6 +407,30 @@ public: */ operator SortConstructorType() const throw(AssertionException); + /** + * Is this a predicate subtype? + * @return true if this is a predicate subtype + */ + bool isPredicateSubtype() const; + + /** + * Cast this type to a predicate subtype + * @return the predicate subtype + */ + operator PredicateSubtype() const throw(AssertionException); + + /** + * Is this an integer subrange type? + * @return true if this is an integer subrange type + */ + bool isSubrange() const; + + /** + * Cast this type to an integer subrange type + * @return the integer subrange type + */ + operator SubrangeType() const throw(AssertionException); + /** * Is this a kind type (i.e., the type of a type)? * @return true if this is a kind type @@ -573,6 +600,39 @@ public: };/* class SortConstructorType */ +/** + * Class encapsulating a predicate subtype. + */ +class CVC4_PUBLIC PredicateSubtype : public Type { + +public: + + /** Construct from the base type */ + PredicateSubtype(const Type& type = Type()) throw(AssertionException); + + /** Get the LAMBDA defining this predicate subtype */ + Expr getPredicate() const; + + /** Get the base type of this predicate subtype */ + Type getBaseType() const; + +};/* class PredicateSubtype */ + +/** + * Class encapsulating an integer subrange type. + */ +class CVC4_PUBLIC SubrangeType : public Type { + +public: + + /** Construct from the base type */ + SubrangeType(const Type& type = Type()) throw(AssertionException); + + /** Get the bounds defining this integer subrange */ + SubrangeBounds getSubrangeBounds() const; + +};/* class SubrangeType */ + /** * Class encapsulating the kind type (the type of types). */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 77203bbb5..8cfb6387a 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -71,68 +71,45 @@ Node TypeNode::mkGroundTerm() const { return kind::mkGroundTerm(*this); } -bool TypeNode::isBoolean() const { - return getKind() == kind::TYPE_CONSTANT && - ( getConst() == BOOLEAN_TYPE || - getConst() == PSEUDOBOOLEAN_TYPE ); -} - -bool TypeNode::isInteger() const { - return getKind() == kind::TYPE_CONSTANT && - ( getConst() == INTEGER_TYPE || - getConst() == PSEUDOBOOLEAN_TYPE ); -} - -bool TypeNode::isReal() const { - return getKind() == kind::TYPE_CONSTANT && - ( getConst() == REAL_TYPE || - getConst() == INTEGER_TYPE || - getConst() == PSEUDOBOOLEAN_TYPE ); -} - -bool TypeNode::isPseudoboolean() const { - return getKind() == kind::TYPE_CONSTANT && - getConst() == PSEUDOBOOLEAN_TYPE; -} - -bool TypeNode::isString() const { - return getKind() == kind::TYPE_CONSTANT && - getConst() == STRING_TYPE; -} - -bool TypeNode::isArray() const { - return getKind() == kind::ARRAY_TYPE; -} - -TypeNode TypeNode::getArrayIndexType() const { - Assert(isArray()); - return (*this)[0]; -} - -TypeNode TypeNode::getArrayConstituentType() const { - Assert(isArray()); - return (*this)[1]; -} - -TypeNode TypeNode::getConstructorRangeType() const { - Assert(isConstructor()); - return (*this)[getNumChildren()-1]; -} - -bool TypeNode::isFunction() const { - return getKind() == kind::FUNCTION_TYPE; +bool TypeNode::isSubtypeOf(TypeNode t) const { + if(*this == t) { + return true; + } + if(getKind() == kind::TYPE_CONSTANT) { + switch(getConst()) { + case PSEUDOBOOLEAN_TYPE: + return t.getKind() == kind::TYPE_CONSTANT && + ( t.getConst() == BOOLEAN_TYPE || + t.getConst() == INTEGER_TYPE ); + case INTEGER_TYPE: + return t.getKind() == kind::TYPE_CONSTANT && t.getConst() == REAL_TYPE; + default: + return false; + } + } + if(isSubrange()) { + if(t.isSubrange()) { + return t.getSubrangeBounds() <= getSubrangeBounds(); + } else { + return t.getKind() == kind::TYPE_CONSTANT && + ( t.getConst() == INTEGER_TYPE || + t.getConst() == REAL_TYPE ); + } + } + if(isPredicateSubtype()) { + return getSubtypeBaseType().isSubtypeOf(t); + } + return false; } -bool TypeNode::isFunctionLike() const { - return - getKind() == kind::FUNCTION_TYPE || - getKind() == kind::CONSTRUCTOR_TYPE || - getKind() == kind::SELECTOR_TYPE || - getKind() == kind::TESTER_TYPE; +Node TypeNode::getSubtypePredicate() const { + Assert(isPredicateSubtype()); + return Node::fromExpr(getConst()); } -bool TypeNode::isPredicate() const { - return isFunction() && getRangeType().isBoolean(); +TypeNode TypeNode::getSubtypeBaseType() const { + Assert(isPredicateSubtype()); + return getSubtypePredicate().getType().getArgTypes()[0]; } std::vector TypeNode::getArgTypes() const { @@ -158,19 +135,6 @@ std::vector TypeNode::getParamTypes() const { return params; } -TypeNode TypeNode::getRangeType() const { - if(isTester()) { - return NodeManager::currentNM()->booleanType(); - } - Assert(isFunction() || isConstructor() || isSelector()); - return (*this)[getNumChildren()-1]; -} - -/** Is this a tuple type? */ -bool TypeNode::isTuple() const { - return getKind() == kind::TUPLE_TYPE; -} - /** Is this a tuple type? */ vector TypeNode::getTupleTypes() const { Assert(isTuple()); @@ -181,37 +145,6 @@ vector TypeNode::getTupleTypes() const { return types; } -/** Is this a sort kind */ -bool TypeNode::isSort() const { - return getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()); -} - -/** Is this a sort constructor kind */ -bool TypeNode::isSortConstructor() const { - return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr()); -} - -/** Is this a kind type (i.e., the type of a type)? */ -bool TypeNode::isKind() const { - return getKind() == kind::TYPE_CONSTANT && - getConst() == KIND_TYPE; -} - -/** Is this a bit-vector type */ -bool TypeNode::isBitVector() const { - return getKind() == kind::BITVECTOR_TYPE; -} - -/** Is this a datatype type */ -bool TypeNode::isDatatype() const { - return getKind() == kind::DATATYPE_TYPE; -} - -/** Is this a parametric datatype type */ -bool TypeNode::isParametricDatatype() const { - return getKind() == kind::PARAMETRIC_DATATYPE; -} - /** Is this an instantiated datatype type */ bool TypeNode::isInstantiatedDatatype() const { if(getKind() == kind::DATATYPE_TYPE) { @@ -239,31 +172,4 @@ bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const { return TypeNode::fromType(dt.getParameter(n)) != (*this)[n + 1]; } -/** Is this a constructor type */ -bool TypeNode::isConstructor() const { - return getKind() == kind::CONSTRUCTOR_TYPE; -} - -/** Is this a selector type */ -bool TypeNode::isSelector() const { - return getKind() == kind::SELECTOR_TYPE; -} - -/** Is this a tester type */ -bool TypeNode::isTester() const { - return getKind() == kind::TESTER_TYPE; -} - -/** Is this a bit-vector type of size size */ -bool TypeNode::isBitVector(unsigned size) const { - return getKind() == kind::BITVECTOR_TYPE && - getConst() == size; -} - -/** Get the size of this bit-vector type */ -unsigned TypeNode::getBitVectorSize() const { - Assert(isBitVector()); - return getConst(); -} - }/* CVC4 namespace */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index c7da5ceb7..f59ce2dfe 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -447,6 +447,9 @@ public: */ Node mkGroundTerm() const; + /** Is this type a subtype of the given type? */ + bool isSubtypeOf(TypeNode t) const; + /** Is this the Boolean type? */ bool isBoolean() const; @@ -519,6 +522,16 @@ public: */ bool isPredicate() const; + /** + * Is this a predicate-LIKE type? Predicate-like things + * (e.g. datatype testers) that aren't actually predicates ARE + * considered predicates, here. + * + * Arrays are explicitly *not* predicate-like for the purposes of + * this test. + */ + bool isPredicateLike() const; + /** Is this a tuple type? */ bool isTuple() const; @@ -561,6 +574,21 @@ public: /** Is this a sort constructor kind */ bool isSortConstructor() const; + /** Is this a subtype predicate */ + bool isPredicateSubtype() const; + + /** Get the predicate defining this subtype */ + Node getSubtypePredicate() const; + + /** Get the base type of this subtype */ + TypeNode getSubtypeBaseType() const; + + /** Is this a subrange */ + bool isSubrange() const; + + /** Get the bounds defining this subrange */ + const SubrangeBounds& getSubrangeBounds() const; + /** Is this a kind type (i.e., the type of a type)? */ bool isKind() const; @@ -755,6 +783,172 @@ inline void TypeNode::printAst(std::ostream& out, int indent) const { d_nv->printAst(out, indent); } +inline bool TypeNode::isBoolean() const { + return + ( getKind() == kind::TYPE_CONSTANT && getConst() == BOOLEAN_TYPE ) || + isPseudoboolean() || + ( isPredicateSubtype() && getSubtypeBaseType().isBoolean() ); +} + +inline bool TypeNode::isInteger() const { + return + ( getKind() == kind::TYPE_CONSTANT && getConst() == INTEGER_TYPE ) || + isSubrange() || + isPseudoboolean() || + ( isPredicateSubtype() && getSubtypeBaseType().isInteger() ); +} + +inline bool TypeNode::isReal() const { + return + ( getKind() == kind::TYPE_CONSTANT && getConst() == REAL_TYPE ) || + isInteger() || + ( isPredicateSubtype() && getSubtypeBaseType().isReal() ); +} + +inline bool TypeNode::isPseudoboolean() const { + return + ( getKind() == kind::TYPE_CONSTANT && getConst() == PSEUDOBOOLEAN_TYPE ) || + ( isPredicateSubtype() && getSubtypeBaseType().isPseudoboolean() ); +} + +inline bool TypeNode::isString() const { + return getKind() == kind::TYPE_CONSTANT && + getConst() == STRING_TYPE; +} + +inline bool TypeNode::isArray() const { + return getKind() == kind::ARRAY_TYPE || + ( isPredicateSubtype() && getSubtypeBaseType().isPseudoboolean() ); +} + +inline TypeNode TypeNode::getArrayIndexType() const { + Assert(isArray()); + return (*this)[0]; +} + +inline TypeNode TypeNode::getArrayConstituentType() const { + Assert(isArray()); + return (*this)[1]; +} + +inline TypeNode TypeNode::getConstructorRangeType() const { + Assert(isConstructor()); + return (*this)[getNumChildren()-1]; +} + +inline bool TypeNode::isFunction() const { + return getKind() == kind::FUNCTION_TYPE; +} + +inline bool TypeNode::isFunctionLike() const { + return + getKind() == kind::FUNCTION_TYPE || + getKind() == kind::CONSTRUCTOR_TYPE || + getKind() == kind::SELECTOR_TYPE || + getKind() == kind::TESTER_TYPE; +} + +inline bool TypeNode::isPredicate() const { + return isFunction() && getRangeType().isBoolean(); +} + +inline bool TypeNode::isPredicateLike() const { + return isFunctionLike() && getRangeType().isBoolean(); +} + +inline TypeNode TypeNode::getRangeType() const { + if(isTester()) { + return NodeManager::currentNM()->booleanType(); + } + Assert(isFunction() || isConstructor() || isSelector()); + return (*this)[getNumChildren() - 1]; +} + +/** Is this a tuple type? */ +inline bool TypeNode::isTuple() const { + return getKind() == kind::TUPLE_TYPE || + ( isPredicateSubtype() && getSubtypeBaseType().isTuple() ); +} + +/** Is this a sort kind */ +inline bool TypeNode::isSort() const { + return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ) || + ( isPredicateSubtype() && getSubtypeBaseType().isSort() ); +} + +/** Is this a sort constructor kind */ +inline bool TypeNode::isSortConstructor() const { + return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr()); +} + +/** Is this a predicate subtype */ +inline bool TypeNode::isPredicateSubtype() const { + return getKind() == kind::SUBTYPE_TYPE; +} + +/** Is this a subrange type */ +inline bool TypeNode::isSubrange() const { + return getKind() == kind::SUBRANGE_TYPE || + ( isPredicateSubtype() && getSubtypeBaseType().isSubrange() ); +} + +/** Is this a kind type (i.e., the type of a type)? */ +inline bool TypeNode::isKind() const { + return getKind() == kind::TYPE_CONSTANT && + getConst() == KIND_TYPE; +} + +/** Is this a bit-vector type */ +inline bool TypeNode::isBitVector() const { + return getKind() == kind::BITVECTOR_TYPE || + ( isPredicateSubtype() && getSubtypeBaseType().isBitVector() ); +} + +/** Is this a datatype type */ +inline bool TypeNode::isDatatype() const { + return getKind() == kind::DATATYPE_TYPE || + ( isPredicateSubtype() && getSubtypeBaseType().isDatatype() ); +} + +/** Is this a parametric datatype type */ +inline bool TypeNode::isParametricDatatype() const { + return getKind() == kind::PARAMETRIC_DATATYPE || + ( isPredicateSubtype() && getSubtypeBaseType().isParametricDatatype() ); +} + +/** Is this a constructor type */ +inline bool TypeNode::isConstructor() const { + return getKind() == kind::CONSTRUCTOR_TYPE; +} + +/** Is this a selector type */ +inline bool TypeNode::isSelector() const { + return getKind() == kind::SELECTOR_TYPE; +} + +/** Is this a tester type */ +inline bool TypeNode::isTester() const { + return getKind() == kind::TESTER_TYPE; +} + +/** Is this a bit-vector type of size size */ +inline bool TypeNode::isBitVector(unsigned size) const { + return + ( getKind() == kind::BITVECTOR_TYPE && getConst() == size ) || + ( isPredicateSubtype() && getSubtypeBaseType().isBitVector(size) ); +} + +/** Get the size of this bit-vector type */ +inline unsigned TypeNode::getBitVectorSize() const { + Assert(isBitVector()); + return getConst(); +} + +inline const SubrangeBounds& TypeNode::getSubrangeBounds() const { + Assert(isSubrange()); + return getConst(); +} + #ifdef CVC4_DEBUG /** * Pretty printer for use within gdb. This is not intended to be used diff --git a/src/main/driver.cpp b/src/main/driver.cpp index fa42e0b28..eb70f5c93 100644 --- a/src/main/driver.cpp +++ b/src/main/driver.cpp @@ -259,7 +259,7 @@ int runCvc4(int argc, char* argv[], Options& options) { ParserBuilder parserBuilder(&exprMgr, filename, options); if( inputFromStdin ) { - parserBuilder.withStreamInput(cin); + parserBuilder.withLineBufferedStreamInput(cin); } Parser *parser = parserBuilder.build(); diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp index d17d00c5d..363901c1d 100644 --- a/src/main/driver_portfolio.cpp +++ b/src/main/driver_portfolio.cpp @@ -428,7 +428,7 @@ int runCvc4(int argc, char *argv[], Options& options) { withOptions(options); if( inputFromStdin ) { - parserBuilder.withStreamInput(cin); + parserBuilder.withLineBufferedStreamInput(cin); } Parser *parser = parserBuilder.build(); diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index a63d6c67b..d8e7df2f2 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -83,7 +83,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, const Options& options) : d_in(*options.in), d_out(*options.out), - d_language(options.inputLanguage), + d_options(options), d_quit(false) { ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, options); /* Create parser with bogus input. */ @@ -95,7 +95,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, ::rl_completion_entry_function = commandGenerator; ::using_history(); - switch(OutputLanguage lang = toOutputLanguage(d_language)) { + switch(OutputLanguage lang = toOutputLanguage(d_options.inputLanguage)) { case output::LANG_CVC4: d_historyFilename = string(getenv("HOME")) + "/.cvc4_history"; commandsBegin = cvc_commands; @@ -166,7 +166,7 @@ Command* InteractiveShell::readCommand() { /* Prompt the user for input. */ if(d_usingReadline) { #if HAVE_LIBREADLINE - lineBuf = ::readline("CVC4> "); + lineBuf = ::readline(d_options.verbosity >= 0 ? "CVC4> " : ""); if(lineBuf != NULL && lineBuf[0] != '\0') { ::add_history(lineBuf); } @@ -174,7 +174,9 @@ Command* InteractiveShell::readCommand() { free(lineBuf); #endif /* HAVE_LIBREADLINE */ } else { - d_out << "CVC4> " << flush; + if(d_options.verbosity >= 0) { + d_out << "CVC4> " << flush; + } /* Read a line */ d_in.get(sb,'\n'); @@ -229,7 +231,7 @@ Command* InteractiveShell::readCommand() { input[n] = '\n'; if(d_usingReadline) { #if HAVE_LIBREADLINE - lineBuf = ::readline("... > "); + lineBuf = ::readline(d_options.verbosity >= 0 ? "... > " : ""); if(lineBuf != NULL && lineBuf[0] != '\0') { ::add_history(lineBuf); } @@ -237,7 +239,9 @@ Command* InteractiveShell::readCommand() { free(lineBuf); #endif /* HAVE_LIBREADLINE */ } else { - d_out << "... > " << flush; + if(d_options.verbosity >= 0) { + d_out << "... > " << flush; + } /* Read a line */ d_in.get(sb,'\n'); @@ -250,7 +254,7 @@ Command* InteractiveShell::readCommand() { } } - d_parser->setInput(Input::newStringInput(d_language,input,INPUT_FILENAME)); + d_parser->setInput(Input::newStringInput(d_options.inputLanguage, input, INPUT_FILENAME)); /* There may be more than one command in the input. Build up a sequence. */ diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index 65fea8494..7f17b88d7 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -36,7 +36,7 @@ class CVC4_PUBLIC InteractiveShell { std::istream& d_in; std::ostream& d_out; parser::Parser* d_parser; - const InputLanguage d_language; + const Options& d_options; bool d_quit; bool d_usingReadline; diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 4f00cfb3d..f14941d01 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -45,6 +45,8 @@ libcvc4parser_la_SOURCES = \ antlr_input.h \ antlr_input.cpp \ antlr_input_imports.cpp \ + antlr_line_buffered_input.h \ + antlr_line_buffered_input.cpp \ bounded_token_buffer.h \ bounded_token_buffer.cpp \ bounded_token_factory.h \ @@ -64,6 +66,8 @@ libcvc4parser_noinst_la_SOURCES = \ antlr_input.h \ antlr_input.cpp \ antlr_input_imports.cpp \ + antlr_line_buffered_input.h \ + antlr_line_buffered_input.cpp \ bounded_token_buffer.h \ bounded_token_buffer.cpp \ bounded_token_factory.h \ diff --git a/src/parser/Makefile.antlr_tracing b/src/parser/Makefile.antlr_tracing index 087554c52..fa79337b4 100644 --- a/src/parser/Makefile.antlr_tracing +++ b/src/parser/Makefile.antlr_tracing @@ -3,7 +3,8 @@ # This makefile is included from parser directories in order to # do antlr tracing. THIS IS VERY MUCH A HACK, and is only enabled # if CVC4_TRACE_ANTLR is defined (and not 0). In ANTLR 3.2, we -# have to #define +# have to #define "println" and "System," etc., because the +# generator erroneously puts Java in C output! # ifeq ($(CVC4_TRACE_ANTLR),) diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index e52145d4e..67d873a48 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -24,6 +24,7 @@ #include "parser/input.h" #include "parser/bounded_token_buffer.h" #include "parser/bounded_token_factory.h" +#include "parser/antlr_line_buffered_input.h" #include "parser/memory_mapped_input_buffer.h" #include "parser/parser_exception.h" #include "parser/parser.h" @@ -60,8 +61,8 @@ pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const { return d_input; } -AntlrInputStream* -AntlrInputStream::newFileInputStream(const std::string& name, +AntlrInputStream* +AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap) throw (InputStreamException, AssertionException) { pANTLR3_INPUT_STREAM input = NULL; @@ -81,63 +82,84 @@ AntlrInputStream::newFileInputStream(const std::string& name, return new AntlrInputStream( name, input ); } -AntlrInputStream* -AntlrInputStream::newStreamInputStream(std::istream& input, - const std::string& name) +AntlrInputStream* +AntlrInputStream::newStreamInputStream(std::istream& input, + const std::string& name, + bool lineBuffered) throw (InputStreamException, AssertionException) { - // Since these are all NULL on entry, realloc will be called - char *basep = NULL, *boundp = NULL, *cp = NULL; - /* 64KB seems like a reasonable default size. */ - size_t bufSize = 0x10000; + pANTLR3_INPUT_STREAM inputStream = NULL; - /* Keep going until we can't go no more. */ - while( !input.eof() && !input.fail() ) { + if(lineBuffered) { +#ifdef CVC4_ANTLR3_OLD_INPUT_STREAM + inputStream = + antlr3LineBufferedStreamNew(input, + 0, + (pANTLR3_UINT8) strdup(name.c_str())); +#else /* CVC4_ANTLR3_OLD_INPUT_STREAM */ + inputStream = + antlr3LineBufferedStreamNew(input, + ANTLR3_ENC_8BIT, + (pANTLR3_UINT8) strdup(name.c_str())); +#endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */ + } else { - if( cp == boundp ) { - /* We ran out of room in the buffer. Realloc at double the size. */ - ptrdiff_t offset = cp - basep; - basep = (char *) realloc(basep, bufSize); - if( basep == NULL ) { - throw InputStreamException("Failed buffering input stream: " + name); + // Since these are all NULL on entry, realloc will be called + char *basep = NULL, *boundp = NULL, *cp = NULL; + /* 64KB seems like a reasonable default size. */ + size_t bufSize = 0x10000; + + /* Keep going until we can't go no more. */ + while( !input.eof() && !input.fail() ) { + + if( cp == boundp ) { + /* We ran out of room in the buffer. Realloc at double the size. */ + ptrdiff_t offset = cp - basep; + basep = (char *) realloc(basep, bufSize); + if( basep == NULL ) { + throw InputStreamException("Failed buffering input stream: " + name); + } + cp = basep + offset; + boundp = basep + bufSize; + bufSize *= 2; } - cp = basep + offset; - boundp = basep + bufSize; - bufSize *= 2; - } - /* Read as much as we have room for. */ - input.read( cp, boundp - cp ); - cp += input.gcount(); - } + /* Read as much as we have room for. */ + input.read( cp, boundp - cp ); + cp += input.gcount(); + } - /* Make sure the fail bit didn't get set. */ - if( !input.eof() ) { - throw InputStreamException("Stream input failed: " + name); - } + /* Make sure the fail bit didn't get set. */ + if( !input.eof() ) { + throw InputStreamException("Stream input failed: " + name); + } - /* Create an ANTLR input backed by the buffer. */ + /* Create an ANTLR input backed by the buffer. */ #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM - pANTLR3_INPUT_STREAM inputStream = + inputStream = antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8) basep, cp - basep, (pANTLR3_UINT8) strdup(name.c_str())); #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */ - pANTLR3_INPUT_STREAM inputStream = + inputStream = antlr3StringStreamNew((pANTLR3_UINT8) basep, ANTLR3_ENC_8BIT, cp - basep, (pANTLR3_UINT8) strdup(name.c_str())); #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */ - if( inputStream==NULL ) { + + } + + if( inputStream == NULL ) { throw InputStreamException("Couldn't initialize input: " + name); } + return new AntlrInputStream( name, inputStream ); } -AntlrInputStream* -AntlrInputStream::newStringInputStream(const std::string& input, +AntlrInputStream* +AntlrInputStream::newStringInputStream(const std::string& input, const std::string& name) throw (InputStreamException, AssertionException) { char* inputStr = strdup(input.c_str()); @@ -309,6 +331,5 @@ void AntlrInput::setAntlr3Parser(pANTLR3_PARSER pParser) { d_parser->rec->mismatch; } - }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index dca26ab75..a39defd14 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -77,7 +77,8 @@ public: /** Create an input from an istream. */ static AntlrInputStream* newStreamInputStream(std::istream& input, - const std::string& name) + const std::string& name, + bool lineBuffered = false) throw (InputStreamException, AssertionException); /** Create a string input. @@ -88,7 +89,7 @@ public: static AntlrInputStream* newStringInputStream(const std::string& input, const std::string& name) throw (InputStreamException, AssertionException); -}; +};/* class AntlrInputStream */ class Parser; @@ -209,7 +210,7 @@ protected: /** Set the Parser object for this input. */ virtual void setParser(Parser& parser); -}; +};/* class AntlrInput */ inline std::string AntlrInput::getUnparsedText() { const char *base = (const char *)d_antlr3InputStream->data; diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp new file mode 100644 index 000000000..b42562f72 --- /dev/null +++ b/src/parser/antlr_line_buffered_input.cpp @@ -0,0 +1,379 @@ +/********************* */ +/*! \file antlr_line_buffered_input.cpp + ** \verbatim + ** Original author: mdeters + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include +#include +#include + +#include "util/output.h" +#include "util/Assert.h" + +namespace CVC4 { +namespace parser { + +typedef struct ANTLR3_LINE_BUFFERED_INPUT_STREAM { + ANTLR3_INPUT_STREAM antlr; + std::istream* in; +} *pANTLR3_LINE_BUFFERED_INPUT_STREAM; + +static pANTLR3_INPUT_STREAM antlr3CreateLineBufferedStream(std::istream& in); + +static void +setupInputStream(pANTLR3_INPUT_STREAM input) +{ +#if 0 + ANTLR3_BOOLEAN isBigEndian; + + // Used to determine the endianness of the machine we are currently + // running on. + // + ANTLR3_UINT16 bomTest = 0xFEFF; + + // What endianess is the machine we are running on? If the incoming + // encoding endianess is the same as this machine's natural byte order + // then we can use more efficient API calls. + // + if (*((pANTLR3_UINT8)(&bomTest)) == 0xFE) + { + isBigEndian = ANTLR3_TRUE; + } + else + { + isBigEndian = ANTLR3_FALSE; + } + + // What encoding did the user tell us {s}he thought it was? I am going + // to get sick of the questions on antlr-interest, I know I am. + // + switch (input->encoding) + { + case ANTLR3_ENC_UTF8: + + // See if there is a BOM at the start of this UTF-8 sequence + // and just eat it if there is. Windows .TXT files have this for instance + // as it identifies UTF-8 even though it is of no consequence for byte order + // as UTF-8 does not have a byte order. + // + if ( (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar)) == 0xEF + && (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1)) == 0xBB + && (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+2)) == 0xBF + ) + { + // The UTF8 BOM is present so skip it + // + input->nextChar = (void *)((pANTLR3_UINT8)input->nextChar + 3); + } + + // Install the UTF8 input routines + // + antlr3UTF8SetupStream(input); + break; + + case ANTLR3_ENC_UTF16: + + // See if there is a BOM at the start of the input. If not then + // we assume that the byte order is the natural order of this + // machine (or it is really UCS2). If there is a BOM we determine if the encoding + // is the same as the natural order of this machine. + // + if ( (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar)) == 0xFE + && (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1)) == 0xFF + ) + { + // BOM Present, indicates Big Endian + // + input->nextChar = (void *)((pANTLR3_UINT8)input->nextChar + 2); + + antlr3UTF16SetupStream(input, isBigEndian, ANTLR3_TRUE); + } + else if ( (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar)) == 0xFF + && (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1)) == 0xFE + ) + { + // BOM present, indicates Little Endian + // + input->nextChar = (void *)((pANTLR3_UINT8)input->nextChar + 2); + + antlr3UTF16SetupStream(input, isBigEndian, ANTLR3_FALSE); + } + else + { + // No BOM present, assume local computer byte order + // + antlr3UTF16SetupStream(input, isBigEndian, isBigEndian); + } + break; + + case ANTLR3_ENC_UTF32: + + // See if there is a BOM at the start of the input. If not then + // we assume that the byte order is the natural order of this + // machine. If there is we determine if the encoding + // is the same as the natural order of this machine. + // + if ( (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar)) == 0x00 + && (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1)) == 0x00 + && (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+2)) == 0xFE + && (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+3)) == 0xFF + ) + { + // BOM Present, indicates Big Endian + // + input->nextChar = (void *)((pANTLR3_UINT8)input->nextChar + 4); + + antlr3UTF32SetupStream(input, isBigEndian, ANTLR3_TRUE); + } + else if ( (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar)) == 0xFF + && (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1)) == 0xFE + && (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1)) == 0x00 + && (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1)) == 0x00 + ) + { + // BOM present, indicates Little Endian + // + input->nextChar = (void *)((pANTLR3_UINT8)input->nextChar + 4); + + antlr3UTF32SetupStream(input, isBigEndian, ANTLR3_FALSE); + } + else + { + // No BOM present, assume local computer byte order + // + antlr3UTF32SetupStream(input, isBigEndian, isBigEndian); + } + break; + + case ANTLR3_ENC_UTF16BE: + + // Encoding is definately Big Endian with no BOM + // + antlr3UTF16SetupStream(input, isBigEndian, ANTLR3_TRUE); + break; + + case ANTLR3_ENC_UTF16LE: + + // Encoding is definately Little Endian with no BOM + // + antlr3UTF16SetupStream(input, isBigEndian, ANTLR3_FALSE); + break; + + case ANTLR3_ENC_UTF32BE: + + // Encoding is definately Big Endian with no BOM + // + antlr3UTF32SetupStream(input, isBigEndian, ANTLR3_TRUE); + break; + + case ANTLR3_ENC_UTF32LE: + + // Encoding is definately Little Endian with no BOM + // + antlr3UTF32SetupStream(input, isBigEndian, ANTLR3_FALSE); + break; + + case ANTLR3_ENC_EBCDIC: + + // EBCDIC is basically the same as ASCII but with an on the + // fly translation to ASCII + // + antlr3EBCDICSetupStream(input); + break; + + case ANTLR3_ENC_8BIT: + default: + + // Standard 8bit/ASCII + // + antlr38BitSetupStream(input); + break; + } +#endif /* 0 */ +} + +static ANTLR3_UCHAR +myLA(pANTLR3_INT_STREAM is, ANTLR3_INT32 la) { + pANTLR3_INPUT_STREAM input; + + input = ((pANTLR3_INPUT_STREAM) (is->super)); + + Debug("pipe") << "LA" << std::endl; + if (( ((pANTLR3_UINT8)input->nextChar) + la - 1) >= (((pANTLR3_UINT8)input->data) + input->sizeBuf)) + { + std::istream& in = *((pANTLR3_LINE_BUFFERED_INPUT_STREAM)input)->in; + if(!in) { + Debug("pipe") << "EOF" << std::endl; + return ANTLR3_CHARSTREAM_EOF; + } + Debug("pipe") << "READ" << std::endl; + if(input->data == NULL) { + Debug("pipe") << "ALLOC" << std::endl; + input->data = malloc(1024); + input->nextChar = input->data; + } else { + Debug("pipe") << "REALLOC" << std::endl; + size_t pos = (char*)input->nextChar - (char*)input->data; + input->data = realloc(input->data, input->sizeBuf + 1024); + input->nextChar = (char*)input->data + pos; + } + in.getline((((char*)input->data) + input->sizeBuf), 1024); + while(in.fail() && !in.eof()) { + Debug("pipe") << "input string too long, reallocating" << std::endl; + input->sizeBuf += strlen(((char*)input->data) + input->sizeBuf); + size_t pos = (char*)input->nextChar - (char*)input->data; + input->data = realloc(input->data, input->sizeBuf + 1024); + input->nextChar = (char*)input->data + pos; + in.clear(); + in.getline((((char*)input->data) + input->sizeBuf), 1024); + } + input->sizeBuf += strlen(((char*)input->data) + input->sizeBuf); + Assert(*(((char*)input->data) + input->sizeBuf) == '\0'); + Debug("pipe") << "SIZEBUF now " << input->sizeBuf << std::endl; + *(((char*)input->data) + input->sizeBuf) = '\n'; + ++input->sizeBuf; + } + + Debug("pipe") << "READ POINTER[" << la << "] AT: >>" << std::string(((char*)input->nextChar), input->sizeBuf - (((char*)input->nextChar) - (char*)input->data) + 1) << "<< returning '" << (char)(*((pANTLR3_UINT8)input->nextChar + la - 1)) << "' (" << (unsigned)(*((pANTLR3_UINT8)input->nextChar + la - 1)) << ")" << std::endl; + return (ANTLR3_UCHAR)(*((pANTLR3_UINT8)input->nextChar + la - 1)); +} + + +static void +myConsume(pANTLR3_INT_STREAM is) +{ + pANTLR3_INPUT_STREAM input; + + input = ((pANTLR3_INPUT_STREAM) (is->super)); + + Debug("pipe") << "consume! '" << *(char*)input->nextChar << "' (" << (unsigned)*(char*)input->nextChar << ")" << std::endl; + if ((pANTLR3_UINT8)(input->nextChar) < (((pANTLR3_UINT8)input->data) + input->sizeBuf)) + { + /* Indicate one more character in this line + */ + input->charPositionInLine++; + + if ((ANTLR3_UCHAR)(*((pANTLR3_UINT8)input->nextChar)) == input->newlineChar) + { + /* Reset for start of a new line of input + */ + input->line++; + input->charPositionInLine = 0; + input->currentLine = (void *)(((pANTLR3_UINT8)input->nextChar) + 1); + Debug("pipe") << "-- newline!" << std::endl; + } + + /* Increment to next character position + */ + input->nextChar = (void *)(((pANTLR3_UINT8)input->nextChar) + 1); + Debug("pipe") << "-- advance nextChar! looking at '" << *(char*)input->nextChar << "' (" << (unsigned)*(char*)input->nextChar << ")" << std::endl; + } else Debug("pipe") << "-- nothing!" << std::endl; +} + +pANTLR3_INPUT_STREAM +antlr3LineBufferedStreamNew(std::istream& in, ANTLR3_UINT32 encoding, pANTLR3_UINT8 name) +{ + pANTLR3_INPUT_STREAM input; + + if(!in) { + return NULL; + } + + // First order of business is to set up the stream and install the data pointer. + // Then we will work out the encoding and byte order and adjust the API functions that are installed for the + // default 8Bit stream accordingly. + // + input = antlr3CreateLineBufferedStream(in); + if (input == NULL) + { + return NULL; + } + + // Size (in bytes) of the given 'string' + // + input->sizeBuf = 0; + + input->istream->_LA = myLA; + input->istream->consume = myConsume; + +#ifndef CVC4_ANTLR3_OLD_INPUT_STREAM + // We have the data in memory now so we can deal with it according to + // the encoding scheme we were given by the user. + // + input->encoding = encoding; +#endif /* ! CVC4_ANTLR3_OLD_INPUT_STREAM */ + + // Now we need to work out the endian type and install any + // API functions that differ from 8Bit + // + setupInputStream(input); + + // Now we can set up the file name + // + input->istream->streamName = input->strFactory->newStr8(input->strFactory, name); + input->fileName = input->istream->streamName; + + return input; +} + +static pANTLR3_INPUT_STREAM +antlr3CreateLineBufferedStream(std::istream& in) +{ + // Pointer to the input stream we are going to create + // + pANTLR3_INPUT_STREAM input; + + if (!in) + { + return NULL; + } + + // Allocate memory for the input stream structure + // + input = (pANTLR3_INPUT_STREAM) + ANTLR3_CALLOC(1, sizeof(ANTLR3_LINE_BUFFERED_INPUT_STREAM)); + + if (input == NULL) + { + return NULL; + } + + // Structure was allocated correctly, now we can install the pointer + // + input->data = malloc(1024); + input->isAllocated = ANTLR3_FALSE; + + ((pANTLR3_LINE_BUFFERED_INPUT_STREAM)input)->in = ∈ + + // Call the common 8 bit input stream handler + // initialization. + // +#ifdef CVC4_ANTLR3_OLD_INPUT_STREAM + antlr3AsciiSetupStream(input, ANTLR3_CHARSTREAM); +#else /* CVC4_ANTLR3_OLD_INPUT_STREAM */ + antlr38BitSetupStream(input); + // In some libantlr3c 3.4-beta versions, this call is not included in the above. + // This is probably an erroneously-deleted line in the libantlr3c source since 3.2. + antlr3GenericSetupStream(input); +#endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */ + + return input; +} + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ + diff --git a/src/parser/antlr_line_buffered_input.h b/src/parser/antlr_line_buffered_input.h new file mode 100644 index 000000000..b59645dd7 --- /dev/null +++ b/src/parser/antlr_line_buffered_input.h @@ -0,0 +1,36 @@ +/********************* */ +/*! \file antlr_line_buffered_input.h + ** \verbatim + ** Original author: mdeters + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4parser_private.h" + +#ifndef __CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H +#define __CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H + +#include + +namespace CVC4 { +namespace parser { + +pANTLR3_INPUT_STREAM +antlr3LineBufferedStreamNew(std::istream& in, ANTLR3_UINT32 encoding, pANTLR3_UINT8 name); + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H */ diff --git a/src/parser/antlr_tracing.h b/src/parser/antlr_tracing.h index 2c3e66c12..95f6100f4 100644 --- a/src/parser/antlr_tracing.h +++ b/src/parser/antlr_tracing.h @@ -54,7 +54,7 @@ static struct __Cvc4System { struct JavaPrinter { template JavaPrinter operator+(const T& t) const { - ::CVC4::Message() << t; + Message() << t; return JavaPrinter(); } };/* struct JavaPrinter */ @@ -67,7 +67,7 @@ static struct __Cvc4System { * to the call-by-value semantics of C. All that's left to * do is print the newline. */ - void println(JavaPrinter) { ::CVC4::Message() << std::endl; } + void println(JavaPrinter) { Message() << std::endl; } } out; } System; diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp index d77f72bfa..d63d3afe0 100644 --- a/src/parser/bounded_token_buffer.cpp +++ b/src/parser/bounded_token_buffer.cpp @@ -308,19 +308,19 @@ setTokenSource ( pANTLR3_TOKEN_STREAM ts, static pANTLR3_STRING toString (pANTLR3_TOKEN_STREAM ts) { - Unreachable(); + Unimplemented("toString(ts)"); } static pANTLR3_STRING toStringSS(pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 start, ANTLR3_UINT32 stop) { - Unreachable(); + Unimplemented("toStringSS(ts, %u, %u)", start, stop); } static pANTLR3_STRING toStringTT (pANTLR3_TOKEN_STREAM ts, pANTLR3_COMMON_TOKEN start, pANTLR3_COMMON_TOKEN stop) { - Unreachable(); + Unimplemented("toStringTT(ts, %u, %u)", start, stop); } /** Move the input pointer to the next incoming token. The stream diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 9f0c2cddb..657a2fe2c 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -132,9 +132,6 @@ tokens { PARENHASH = '(#'; HASHPAREN = '#)'; - //DOT = '.'; - DOTDOT = '..'; - // Operators ARROW_TOK = '->'; @@ -198,6 +195,12 @@ tokens { BVSGT_TOK = 'BVSGT'; BVSLE_TOK = 'BVSLE'; BVSGE_TOK = 'BVSGE'; + + // these are parsed by special NUMBER_OR_RANGEOP rule, below + DECIMAL_LITERAL; + INTEGER_LITERAL; + DOT; + DOTDOT; }/* tokens */ @parser::members { @@ -312,7 +315,8 @@ Kind getOperatorKind(int type, bool& negate) { case PLUS_TOK: return kind::PLUS; case MINUS_TOK: return kind::MINUS; case STAR_TOK: return kind::MULT; - case INTDIV_TOK: Unhandled(CvcParserTokenNames[type]); + case INTDIV_TOK: return kind::INTS_DIVISION; + case MOD_TOK: return kind::INTS_MODULUS; case DIV_TOK: return kind::DIVISION; case EXP_TOK: Unhandled(CvcParserTokenNames[type]); @@ -363,9 +367,14 @@ Expr createPrecedenceTree(ExprManager* em, unsigned pivot = findPivot(operators, startIndex, stopIndex - 1); //Debug("prec") << "pivot[" << startIndex << "," << stopIndex - 1 << "] at " << pivot << std::endl; bool negate; - Expr e = em->mkExpr(getOperatorKind(operators[pivot], negate), - createPrecedenceTree(em, expressions, operators, startIndex, pivot), - createPrecedenceTree(em, expressions, operators, pivot + 1, stopIndex)); + Kind k = getOperatorKind(operators[pivot], negate); + Expr lhs = createPrecedenceTree(em, expressions, operators, startIndex, pivot); + Expr rhs = createPrecedenceTree(em, expressions, operators, pivot + 1, stopIndex); + if(k == kind::EQUAL && lhs.getType().isBoolean()) { + WarningOnce() << "Warning: converting BOOL = BOOL to BOOL <=> BOOL" << std::endl; + k = kind::IFF; + } + Expr e = em->mkExpr(k, lhs, rhs); return negate ? em->mkExpr(kind::NOT, e) : e; }/* createPrecedenceTree() recursive variant */ @@ -497,6 +506,8 @@ namespace CVC4 { #include "util/output.h" #include +#include +#include #define REPEAT_COMMAND(k, CommandCtor) \ ({ \ @@ -691,8 +702,8 @@ mainCommand[CVC4::Command*& cmd] { UNSUPPORTED("CALL command"); } | ECHO_TOK - ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) - { Message() << s << std::endl; } + ( simpleSymbolicExpr[sexpr] + { Message() << sexpr << std::endl; } | { Message() << std::endl; } ) @@ -732,17 +743,30 @@ mainCommand[CVC4::Command*& cmd] | toplevelDeclaration[cmd] ; -symbolicExpr[CVC4::SExpr& sexpr] +simpleSymbolicExpr[CVC4::SExpr& sexpr] @declarations { - std::vector children; std::string s; + CVC4::Rational r; } - : INTEGER_LITERAL ('.' DIGIT+)? - { sexpr = SExpr((const char*)$symbolicExpr.text->chars); } + : INTEGER_LITERAL + { sexpr = SExpr(AntlrInput::tokenText($INTEGER_LITERAL)); } + | DECIMAL_LITERAL + { sexpr = SExpr(AntlrInput::tokenText($DECIMAL_LITERAL)); } + | HEX_LITERAL + { sexpr = SExpr(AntlrInput::tokenText($HEX_LITERAL)); } + | BINARY_LITERAL + { sexpr = SExpr(AntlrInput::tokenText($BINARY_LITERAL)); } | str[s] { sexpr = SExpr(s); } | IDENTIFIER { sexpr = SExpr(AntlrInput::tokenText($IDENTIFIER)); } + ; + +symbolicExpr[CVC4::SExpr& sexpr] +@declarations { + std::vector children; +} + : simpleSymbolicExpr[sexpr] | LPAREN (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN { sexpr = SExpr(children); } ; @@ -1020,9 +1044,12 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, bool& lhs] @init { Type t2; - Expr f; + Expr f, f2; std::string id; std::vector types; + std::vector< std::pair > typeIds; + DeclarationScope* declScope; + Parser* parser; lhs = false; } /* named types */ @@ -1056,24 +1083,33 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, { t = EXPR_MANAGER->mkArrayType(t, t2); } /* subtypes */ - | SUBTYPE_TOK LPAREN formula[f] ( COMMA formula[f] )? RPAREN - { UNSUPPORTED("subtypes not supported yet"); - t = Type(); } + | SUBTYPE_TOK LPAREN + /* A bit tricky: this LAMBDA expression cannot refer to constants + * declared in the outer context. What follows isn't quite right, + * though, since type aliases and function definitions should be + * retained in the set of current declarations. */ + { /*declScope = PARSER_STATE->getDeclarationScope(); + PARSER_STATE->useDeclarationsFrom(new DeclarationScope());*/ } + formula[f] ( COMMA formula[f2] )? RPAREN + { /*DeclarationScope* old = PARSER_STATE->getDeclarationScope(); + PARSER_STATE->useDeclarationsFrom(declScope); + delete old;*/ + t = f2.isNull() ? + EXPR_MANAGER->mkPredicateSubtype(f) : + EXPR_MANAGER->mkPredicateSubtype(f, f2); + } /* subrange types */ | LBRACKET k1=bound DOTDOT k2=bound RBRACKET - { std::stringstream ss; - ss << "subranges not supported yet: [" << k1 << ":" << k2 << ']'; - UNSUPPORTED(ss.str()); - if(k1.hasBound() && k2.hasBound() && + { if(k1.hasBound() && k2.hasBound() && k1.getBound() > k2.getBound()) { - ss.str(""); + std::stringstream ss; ss << "Subrange [" << k1.getBound() << ".." << k2.getBound() << "] inappropriate: range must be nonempty!"; PARSER_STATE->parseError(ss.str()); } - Debug("subranges") << ss.str() << std::endl; - t = Type(); } + t = EXPR_MANAGER->mkSubrangeType(SubrangeBounds(k1, k2)); + } /* tuple types / old-style function types */ | LBRACKET type[t,check] { types.push_back(t); } @@ -1087,15 +1123,14 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, } } else { // tuple type [ T, U, V... ] - t = EXPR_MANAGER->mkTupleType(types); + t = PARSER_STATE->mkTupleType(types); } } /* record types */ - | SQHASH identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] - ( COMMA identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] )* HASHSQ - { UNSUPPORTED("records not supported yet"); - t = Type(); } + | SQHASH identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); } + ( COMMA identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); } )* HASHSQ + { t = PARSER_STATE->mkRecordType(typeIds); } /* bitvector types */ | BITVECTOR_TOK LPAREN k=numeral RPAREN @@ -1321,14 +1356,20 @@ arithmeticBinop[unsigned& op] | MINUS_TOK | STAR_TOK | INTDIV_TOK + | MOD_TOK | DIV_TOK | EXP_TOK ; -/** Parses an array assignment term. */ +/** Parses an array/tuple/record assignment term. */ storeTerm[CVC4::Expr& f] : uminusTerm[f] - ( WITH_TOK arrayStore[f] ( COMMA arrayStore[f] )* )* + ( WITH_TOK + ( arrayStore[f] ( COMMA arrayStore[f] )* + | DOT ( tupleStore[f] ( COMMA DOT tupleStore[f] )* + | recordStore[f] ( COMMA DOT recordStore[f] )* ) ) + | /* nothing */ + ) ; /** @@ -1361,6 +1402,84 @@ arrayStore[CVC4::Expr& f] } ; +/** + * Parses just part of the tuple assignment (and constructs + * the store terms). + */ +tupleStore[CVC4::Expr& f] +@init { + Expr f2; +} + : k=numeral ASSIGN_TOK uminusTerm[f2] + { + Type t = f.getType(); + if(! t.isDatatype()) { + PARSER_STATE->parseError("tuple-update applied to non-tuple"); + } + Datatype tuple = DatatypeType(f.getType()).getDatatype(); + if(tuple.getName() != "__cvc4_tuple") { + PARSER_STATE->parseError("tuple-update applied to non-tuple"); + } + if(k < tuple[0].getNumArgs()) { + std::vector args; + for(unsigned i = 0; i < tuple[0].getNumArgs(); ++i) { + if(i == k) { + args.push_back(f2); + } else { + Expr selectorOp = tuple[0][i].getSelector(); + Expr select = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f); + args.push_back(select); + } + } + f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, tuple[0].getConstructor(), args); + } else { + std::stringstream ss; + ss << "tuple is of length " << tuple[0].getNumArgs() << "; cannot update index " << k; + PARSER_STATE->parseError(ss.str()); + } + } + ; + +/** + * Parses just part of the record assignment (and constructs + * the store terms). + */ +recordStore[CVC4::Expr& f] +@init { + std::string id; + Expr f2; +} + : identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK uminusTerm[f2] + { + Type t = f.getType(); + if(! t.isDatatype()) { + PARSER_STATE->parseError("record-update applied to non-record"); + } + Datatype record = DatatypeType(f.getType()).getDatatype(); + if(record.getName() != "__cvc4_record") { + PARSER_STATE->parseError("record-update applied to non-record"); + } + const DatatypeConstructorArg* updateArg; + try { + updateArg = &record[0][id]; + } catch(IllegalArgumentException& e) { + PARSER_STATE->parseError(std::string("no such field `") + id + "' in record"); + } + std::vector args; + for(unsigned i = 0; i < record[0].getNumArgs(); ++i) { + const DatatypeConstructorArg* thisArg = &record[0][i]; + if(thisArg == updateArg) { + args.push_back(f2); + } else { + Expr selectorOp = record[0][i].getSelector(); + Expr select = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f); + args.push_back(select); + } + } + f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, record[0].getConstructor(), args); + } + ; + /** Parses a unary minus term. */ uminusTerm[CVC4::Expr& f] @init { @@ -1469,20 +1588,42 @@ postfixTerm[CVC4::Expr& f] } /* record / tuple select */ - // FIXME - clash in lexer between tuple-select and real; can - // resolve with syntactic predicate in ANTLR 3.3, but broken in - // 3.2 ? - /*| DOT + | DOT ( identifier[id,CHECK_NONE,SYM_VARIABLE] - { UNSUPPORTED("record select not implemented yet"); - f = Expr(); } + { Type t = f.getType(); + if(! t.isDatatype()) { + PARSER_STATE->parseError("record-select applied to non-record"); + } + Datatype record = DatatypeType(f.getType()).getDatatype(); + if(record.getName() != "__cvc4_record") { + PARSER_STATE->parseError("record-select applied to non-record"); + } + try { + Expr selectorOp = record[0][id].getSelector(); + f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f); + } catch(IllegalArgumentException& e) { + PARSER_STATE->parseError(std::string("no such field `") + id + "' in record"); + } + } | k=numeral - { UNSUPPORTED("tuple select not implemented yet"); - // This will assert-fail if k too big or f not a tuple - // that's ok for now, once a TUPLE_SELECT operator exists, - // that will do any necessary type checking - f = EXPR_MANAGER->mkVar(TupleType(f.getType()).getTypes()[k]); } - )*/ + { Type t = f.getType(); + if(! t.isDatatype()) { + PARSER_STATE->parseError("tuple-select applied to non-tuple"); + } + Datatype tuple = DatatypeType(f.getType()).getDatatype(); + if(tuple.getName() != "__cvc4_tuple") { + PARSER_STATE->parseError("tuple-select applied to non-tuple"); + } + try { + Expr selectorOp = tuple[0][k].getSelector(); + f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f); + } catch(IllegalArgumentException& e) { + std::stringstream ss; + ss << "tuple is of length " << tuple[0].getNumArgs() << "; cannot access index " << k; + PARSER_STATE->parseError(ss.str()); + } + } + ) )* ( typeAscription[f, t] { if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && t.isDatatype()) { @@ -1641,6 +1782,8 @@ simpleTerm[CVC4::Expr& f] @init { std::string name; std::vector args; + std::vector names; + Expr e; Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; Type t; } @@ -1654,7 +1797,12 @@ simpleTerm[CVC4::Expr& f] /* If args has elements, we must be a tuple literal. * Otherwise, f is already the sub-formula, and * there's nothing to do */ - f = EXPR_MANAGER->mkExpr(kind::TUPLE, args); + std::vector types; + for(std::vector::const_iterator i = args.begin(); i != args.end(); ++i) { + types.push_back((*i).getType()); + } + DatatypeType t = PARSER_STATE->mkTupleType(types); + f = EXPR_MANAGER->mkExpr(kind::APPLY_CONSTRUCTOR, t.getDatatype()[0].getConstructor(), args); } } @@ -1677,9 +1825,16 @@ simpleTerm[CVC4::Expr& f] std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4); f = MK_CONST( BitVector(binString, 2) ); } /* record literals */ - | PARENHASH recordEntry (COMMA recordEntry)+ HASHPAREN - { UNSUPPORTED("records not implemented yet"); - f = Expr(); } + | PARENHASH recordEntry[name,e] { names.push_back(name); args.push_back(e); } + ( COMMA recordEntry[name,e] { names.push_back(name); args.push_back(e); } )* HASHPAREN + { std::vector< std::pair > typeIds; + Assert(names.size() == args.size()); + for(unsigned i = 0; i < names.size(); ++i) { + typeIds.push_back(std::make_pair(names[i], args[i].getType())); + } + DatatypeType t = PARSER_STATE->mkRecordType(typeIds); + f = EXPR_MANAGER->mkExpr(kind::APPLY_CONSTRUCTOR, t.getDatatype()[0].getConstructor(), args); + } /* variable / zero-ary constructor application */ | identifier[name,CHECK_DECLARED,SYM_VARIABLE] @@ -1707,12 +1862,8 @@ typeAscription[const CVC4::Expr& f, CVC4::Type& t] /** * Matches an entry in a record literal. */ -recordEntry -@init { - std::string id; - Expr f; -} - : identifier[id,CHECK_DECLARED,SYM_VARIABLE] ASSIGN_TOK formula[f] +recordEntry[std::string& name, CVC4::Expr& ex] + : identifier[name,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK formula[ex] ; /** @@ -1823,22 +1974,6 @@ selector[CVC4::DatatypeConstructor& ctor] */ IDENTIFIER : (ALPHA | '_') (ALPHA | DIGIT | '_' | '\'' | '\\' | '?' | '$' | '~')*; -/** - * Matches an integer literal. - */ -INTEGER_LITERAL - : ( '0' - | '1'..'9' DIGIT* - ) - ; - -/** - * Matches a decimal literal. - */ -DECIMAL_LITERAL - : INTEGER_LITERAL '.' DIGIT+ - ; - /** * Same as an integer literal converted to an unsigned int, but * slightly more convenient AND works around a strange ANTLR bug (?) @@ -1901,6 +2036,32 @@ fragment ALPHA : 'a'..'z' | 'A'..'Z'; */ fragment DIGIT : '0'..'9'; +// This rule adapted from http://www.antlr.org/wiki/pages/viewpage.action?pageId=13828121 +// which reportedly comes from Tapestry (http://tapestry.apache.org/tapestry5/) +// +// Special rule that uses parsing tricks to identify numbers and ranges; it's all about +// the dot ('.'). +// Recognizes: +// '.' as DOT +// '..' as DOTDOT +// INTEGER_LITERAL (digit+) +// DECIMAL_LITERAL (digit* . digit+) +// Has to watch out for embedded rangeop (i.e. "1..10" is not "1." and ".10"). +// +// This doesn't ever generate the NUMBER_OR_RANGEOP token, it +// manipulates the $type inside to return the right token. +NUMBER_OR_RANGEOP + : DIGIT+ + ( + { LA(2) != '.' }? => '.' DIGIT* { $type = DECIMAL_LITERAL; } + | { $type = INTEGER_LITERAL; } + ) + | '.' + ( '.' {$type = DOTDOT; } + | {$type = DOT; } + ) + ; + /** * Matches the hexidecimal digits (0-9, a-f, A-F) */ diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 70c887371..76aa47812 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -59,25 +59,26 @@ Input* Input::newFileInput(InputLanguage lang, bool useMmap) throw (InputStreamException, AssertionException) { AntlrInputStream *inputStream = - AntlrInputStream::newFileInputStream(filename,useMmap); - return AntlrInput::newInput(lang,*inputStream); + AntlrInputStream::newFileInputStream(filename, useMmap); + return AntlrInput::newInput(lang, *inputStream); } Input* Input::newStreamInput(InputLanguage lang, std::istream& input, - const std::string& name) + const std::string& name, + bool lineBuffered) throw (InputStreamException, AssertionException) { AntlrInputStream *inputStream = - AntlrInputStream::newStreamInputStream(input,name); - return AntlrInput::newInput(lang,*inputStream); + AntlrInputStream::newStreamInputStream(input, name, lineBuffered); + return AntlrInput::newInput(lang, *inputStream); } Input* Input::newStringInput(InputLanguage lang, const std::string& str, const std::string& name) throw (InputStreamException, AssertionException) { - AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str,name); - return AntlrInput::newInput(lang,*inputStream); + AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str, name); + return AntlrInput::newInput(lang, *inputStream); } }/* CVC4::parser namespace */ diff --git a/src/parser/input.h b/src/parser/input.h index 25023e1a8..8fa51a095 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -110,7 +110,7 @@ public: */ static Input* newFileInput(InputLanguage lang, const std::string& filename, - bool useMmap=false) + bool useMmap = false) throw (InputStreamException, AssertionException); /** Create an input for the given stream. @@ -121,7 +121,8 @@ public: */ static Input* newStreamInput(InputLanguage lang, std::istream& input, - const std::string& name) + const std::string& name, + bool lineBuffered = false) throw (InputStreamException, AssertionException); /** Create an input for the given string @@ -182,6 +183,7 @@ protected: /** Set the Parser object for this input. */ virtual void setParser(Parser& parser) = 0; + };/* class Input */ }/* CVC4::parser namespace */ diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 4418ea18f..3efc315cc 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -54,6 +54,7 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool par } Expr Parser::getSymbol(const std::string& name, SymbolType type) { + checkDeclaration(name, CHECK_DECLARED, type); Assert( isDeclared(name, type) ); switch( type ) { @@ -77,12 +78,14 @@ Expr Parser::getFunction(const std::string& name) { Type Parser::getType(const std::string& var_name, SymbolType type) { + checkDeclaration(var_name, CHECK_DECLARED, type); Assert( isDeclared(var_name, type) ); Type t = getSymbol(var_name, type).getType(); return t; } Type Parser::getSort(const std::string& name) { + checkDeclaration(name, CHECK_DECLARED, SYM_SORT); Assert( isDeclared(name, SYM_SORT) ); Type t = d_declScope->lookupType(name); return t; @@ -90,12 +93,14 @@ Type Parser::getSort(const std::string& name) { Type Parser::getSort(const std::string& name, const std::vector& params) { + checkDeclaration(name, CHECK_DECLARED, SYM_SORT); Assert( isDeclared(name, SYM_SORT) ); Type t = d_declScope->lookupType(name, params); return t; } size_t Parser::getArity(const std::string& sort_name){ + checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT); Assert( isDeclared(sort_name, SYM_SORT) ); return d_declScope->lookupArity(sort_name); } @@ -236,7 +241,7 @@ SortType Parser::mkUnresolvedType(const std::string& name) { SortConstructorType Parser::mkUnresolvedTypeConstructor(const std::string& name, size_t arity) { - SortConstructorType unresolved = mkSortConstructor(name,arity); + SortConstructorType unresolved = mkSortConstructor(name, arity); d_unresolved.insert(unresolved); return unresolved; } @@ -325,6 +330,37 @@ Parser::mkMutualDatatypeTypes(const std::vector& datatypes) { return types; } +DatatypeType Parser::mkRecordType(const std::vector< std::pair >& typeIds) { + DatatypeType& dtt = d_recordTypes[typeIds]; + if(dtt.isNull()) { + Datatype dt("__cvc4_record"); +Debug("datatypes") << "make new record_ctor" << std::endl; + DatatypeConstructor c("__cvc4_record_ctor"); + for(std::vector< std::pair >::const_iterator i = typeIds.begin(); i != typeIds.end(); ++i) { + c.addArg((*i).first, (*i).second); + } + dt.addConstructor(c); + dtt = d_exprManager->mkDatatypeType(dt); + } else { +Debug("datatypes") << "use old record_ctor" << std::endl; +} + return dtt; +} + +DatatypeType Parser::mkTupleType(const std::vector& types) { + DatatypeType& dtt = d_tupleTypes[types]; + if(dtt.isNull()) { + Datatype dt("__cvc4_tuple"); + DatatypeConstructor c("__cvc4_tuple_ctor"); + for(std::vector::const_iterator i = types.begin(); i != types.end(); ++i) { + c.addArg("__cvc4_tuple_stor", *i); + } + dt.addConstructor(c); + dtt = d_exprManager->mkDatatypeType(dt); + } + return dtt; +} + bool Parser::isDeclared(const std::string& name, SymbolType type) { switch(type) { case SYM_VARIABLE: diff --git a/src/parser/parser.h b/src/parser/parser.h index 70bd45c31..405e397b8 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -142,6 +142,20 @@ class CVC4_PUBLIC Parser { /** Are we only parsing? */ bool d_parseOnly; + /** + * We might see the same record type multiple times; we have + * to match always to the same Type. This map contains all the + * record types we have. + */ + std::map >, DatatypeType> d_recordTypes; + + /** + * We might see the same tuple type multiple times; we have + * to match always to the same Type. This map contains all the + * tuple types we have. + */ + std::map, DatatypeType> d_tupleTypes; + /** The set of operators available in the current logic. */ std::set d_logicOperators; @@ -398,6 +412,16 @@ public: std::vector mkMutualDatatypeTypes(const std::vector& datatypes); + /** + * Create a record type, or if there's already a matching one, return that one. + */ + DatatypeType mkRecordType(const std::vector< std::pair >& typeIds); + + /** + * Create a tuple type, or if there's already a matching one, return that one. + */ + DatatypeType mkTupleType(const std::vector& types); + /** * Add an operator to the current legal set. * @@ -494,6 +518,14 @@ public: } } + inline void useDeclarationsFrom(DeclarationScope* scope) { + d_declScope = scope; + } + + inline DeclarationScope* getDeclarationScope() const { + return d_declScope; + } + /** * Gets the current declaration level. */ diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index c17956e62..dff5b93ac 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -66,6 +66,11 @@ Parser* ParserBuilder::build() case FILE_INPUT: input = Input::newFileInput(d_lang, d_filename, d_mmap); break; + case LINE_BUFFERED_STREAM_INPUT: + AlwaysAssert( d_streamInput != NULL, + "Uninitialized stream input in ParserBuilder::build()" ); + input = Input::newStreamInput(d_lang, *d_streamInput, d_filename, true); + break; case STREAM_INPUT: AlwaysAssert( d_streamInput != NULL, "Uninitialized stream input in ParserBuilder::build()" ); @@ -155,6 +160,12 @@ ParserBuilder& ParserBuilder::withStreamInput(std::istream& input) { return *this; } +ParserBuilder& ParserBuilder::withLineBufferedStreamInput(std::istream& input) { + d_inputType = LINE_BUFFERED_STREAM_INPUT; + d_streamInput = &input; + return *this; +} + ParserBuilder& ParserBuilder::withStringInput(const std::string& input) { d_inputType = STRING_INPUT; d_stringInput = input; diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index ce01d3c53..095769ab5 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -44,6 +44,7 @@ class Parser; class CVC4_PUBLIC ParserBuilder { enum InputType { FILE_INPUT, + LINE_BUFFERED_STREAM_INPUT, STREAM_INPUT, STRING_INPUT }; @@ -90,7 +91,7 @@ public: const Options& options); /** Build the parser, using the current settings. */ - Parser *build() throw (InputStreamException,AssertionException); + Parser *build() throw (InputStreamException, AssertionException); /** Should semantic checks be enabled in the parser? (Default: yes) */ ParserBuilder& withChecks(bool flag = true); @@ -150,6 +151,9 @@ public: /** Set the parser to use the given stream for its input. */ ParserBuilder& withStreamInput(std::istream& input); + /** Set the parser to use the given stream for its input. */ + ParserBuilder& withLineBufferedStreamInput(std::istream& input); + /** Set the parser to use the given string for its input. */ ParserBuilder& withStringInput(const std::string& input); };/* class ParserBuilder */ diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index 0ee6944d4..508bfe352 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -41,6 +41,9 @@ std::hash_map Smt::newL logicMap["QF_UFIDL"] = QF_UFIDL; logicMap["QF_UFLRA"] = QF_UFLRA; logicMap["QF_UFLIA"] = QF_UFLIA; + logicMap["QF_UFLIRA"] = QF_UFLIRA; + logicMap["QF_UFNIA"] = QF_UFNIA; + logicMap["QF_UFNIRA"] = QF_UFNIRA; logicMap["QF_AUFLIA"] = QF_AUFLIA; logicMap["QF_AUFLIRA"] = QF_AUFLIRA; return logicMap; @@ -159,6 +162,7 @@ void Smt::setLogic(const std::string& name) { case QF_UFIDL: case QF_UFLIA: + case QF_UFNIA:// nonstandard logic addTheory(THEORY_INTS); addUf(); break; @@ -169,6 +173,13 @@ void Smt::setLogic(const std::string& name) { addUf(); break; + case QF_UFLIRA:// nonstandard logic + case QF_UFNIRA:// nonstandard logic + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + addUf(); + break; + case QF_UF: addUf(); break; diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h index a99f81998..62bb24336 100644 --- a/src/parser/smt/smt.h +++ b/src/parser/smt/smt.h @@ -54,7 +54,10 @@ public: QF_UF, QF_UFIDL, QF_UFLIA, + QF_UFNIA, // nonstandard QF_UFLRA, + QF_UFLIRA, // nonstandard + QF_UFNIRA, // nonstandard QF_UFNRA, UFNIA }; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 791e550b9..926ce1718 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -67,7 +67,6 @@ options { #include "parser/smt2/smt2.h" #include "parser/antlr_input.h" -#include "parser/antlr_tracing.h" using namespace CVC4; using namespace CVC4::parser; @@ -79,6 +78,7 @@ using namespace CVC4::parser; @parser::includes { #include "expr/command.h" #include "parser/parser.h" +#include "parser/antlr_tracing.h" namespace CVC4 { class Expr; @@ -358,7 +358,12 @@ command returns [CVC4::Command* cmd = NULL] extendedCommand[CVC4::Command*& cmd] @declarations { std::vector dts; + Type t; Expr e; + SExpr sexpr; + std::string name; + std::vector names; + std::vector sorts; } /* Z3's extended SMT-LIBv2 set of commands syntax */ : DECLARE_DATATYPES_TOK @@ -368,33 +373,43 @@ extendedCommand[CVC4::Command*& cmd] { PARSER_STATE->popScope(); cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } - | DECLARE_SORTS_TOK | DECLARE_FUNS_TOK + LPAREN_TOK + ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] nonemptySortList[sorts] RPAREN_TOK )+ + RPAREN_TOK | DECLARE_PREDS_TOK - | DEFINE_TOK + LPAREN_TOK + ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] sortList[sorts] RPAREN_TOK )+ + RPAREN_TOK + | DEFINE_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] term[e] | DEFINE_SORTS_TOK - | DECLARE_CONST_TOK - + LPAREN_TOK + ( LPAREN_TOK ( symbol[name,CHECK_UNDECLARED,SYM_SORT] LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK | + symbol[name,CHECK_UNDECLARED,SYM_SORT] symbol[name,CHECK_NONE,SYM_SORT] ) RPAREN_TOK RPAREN_TOK )+ + RPAREN_TOK + | DECLARE_CONST_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] sortSymbol[t,CHECK_DECLARED] + | SIMPLIFY_TOK term[e] { cmd = new SimplifyCommand(e); } | ECHO_TOK - ( STRING_LITERAL - { Message() << AntlrInput::tokenText($STRING_LITERAL) << std::endl; } + ( simpleSymbolicExpr[sexpr] + { Message() << sexpr << std::endl; } | { Message() << std::endl; } ) + { cmd = new EmptyCommand; } ; -symbolicExpr[CVC4::SExpr& sexpr] +simpleSymbolicExpr[CVC4::SExpr& sexpr] @declarations { - std::vector children; CVC4::Kind k; + std::string s; } : INTEGER_LITERAL { sexpr = SExpr(AntlrInput::tokenText($INTEGER_LITERAL)); } | DECIMAL_LITERAL { sexpr = SExpr(AntlrInput::tokenText($DECIMAL_LITERAL)); } - | STRING_LITERAL - { sexpr = SExpr(AntlrInput::tokenText($STRING_LITERAL)); } + | str[s] + { sexpr = SExpr(s); } | SYMBOL { sexpr = SExpr(AntlrInput::tokenText($SYMBOL)); } | builtinOp[k] @@ -404,6 +419,13 @@ symbolicExpr[CVC4::SExpr& sexpr] } | KEYWORD { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); } + ; + +symbolicExpr[CVC4::SExpr& sexpr] +@declarations { + std::vector children; +} + : simpleSymbolicExpr[sexpr] | LPAREN_TOK (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN_TOK @@ -610,6 +632,17 @@ termList[std::vector& formulas, CVC4::Expr& expr] : ( term[expr] { formulas.push_back(expr); } )+ ; +/** + * Matches a string, and strips off the quotes. + */ +str[std::string& s] + : STRING_LITERAL + { s = AntlrInput::tokenText($STRING_LITERAL); + /* strip off the quotes */ + s = s.substr(1, s.size() - 2); + } + ; + /** * Matches a builtin operator symbol and sets kind to its associated Expr kind. */ @@ -637,6 +670,8 @@ builtinOp[CVC4::Kind& kind] | MINUS_TOK { $kind = CVC4::kind::MINUS; } | STAR_TOK { $kind = CVC4::kind::MULT; } | DIV_TOK { $kind = CVC4::kind::DIVISION; } + | INTS_DIV_TOK { $kind = CVC4::kind::INTS_DIVISION; } + | INTS_MOD_TOK { $kind = CVC4::kind::INTS_MODULUS; } | SELECT_TOK { $kind = CVC4::kind::SELECT; } | STORE_TOK { $kind = CVC4::kind::STORE; } @@ -705,6 +740,13 @@ sortList[std::vector& sorts] : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )* ; +nonemptySortList[std::vector& sorts] +@declarations { + Type t; +} + : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )+ + ; + /** * Matches a sequence of (variable,sort) symbol pairs and fills them * into the given vector. @@ -937,6 +979,9 @@ STORE_TOK : 'store'; // TILDE_TOK : '~'; XOR_TOK : 'xor'; +INTS_DIV_TOK : 'div'; +INTS_MOD_TOK : 'mod'; + CONCAT_TOK : 'concat'; BVNOT_TOK : 'bvnot'; BVAND_TOK : 'bvand'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 7d6f27aa5..39eaf5b95 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -127,6 +127,7 @@ void Smt2::setLogic(const std::string& name) { case Smt::QF_UFIDL: case Smt::QF_UFLIA: + case Smt::QF_UFNIA:// nonstandard logic addTheory(THEORY_INTS); addOperator(kind::APPLY_UF); break; @@ -137,6 +138,13 @@ void Smt2::setLogic(const std::string& name) { addOperator(kind::APPLY_UF); break; + case Smt::QF_UFLIRA:// nonstandard logic + case Smt::QF_UFNIRA:// nonstandard logic + addOperator(kind::APPLY_UF); + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + break; + case Smt::QF_BV: addTheory(THEORY_BITVECTORS); break; diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 283cdd725..04690f500 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -94,7 +94,11 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo break; case kind::CONST_RATIONAL: { const Rational& rat = n.getConst(); - out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')'; + if(rat.getDenominator() == 1) { + out << rat.getNumerator(); + } else { + out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')'; + } break; } case kind::CONST_INTEGER: { @@ -107,6 +111,12 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo out << num; break; } + case kind::SUBRANGE_TYPE: + out << '[' << n.getConst() << ']'; + break; + case kind::SUBTYPE_TYPE: + out << "SUBTYPE(" << n.getConst() << ")"; + break; case kind::TYPE_CONSTANT: switch(TypeConstant tc = n.getConst()) { case REAL_TYPE: @@ -129,6 +139,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo break; } break; + default: Warning() << "Constant printing not implemented for the case of " << n.getKind() << endl; out << n.getKind(); @@ -340,6 +351,14 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo op << '/'; opType = INFIX; break; + case kind::INTS_DIVISION: + op << "DIV"; + opType = INFIX; + break; + case kind::INTS_MODULUS: + op << "MOD"; + opType = INFIX; + break; case kind::LT: op << '<'; opType = INFIX; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 393ad664b..691e96ed7 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -127,6 +127,19 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, break; } + case kind::SUBRANGE_TYPE: { + const SubrangeBounds& bounds = n.getConst(); + // No way to represent subranges in SMT-LIBv2; this is inspired + // by yices format (but isn't identical to it). + out << "(subrange " << bounds.lower << ' ' << bounds.upper << ')'; + break; + } + case kind::SUBTYPE_TYPE: + // No way to represent predicate subtypes in SMT-LIBv2; this is + // inspired by yices format (but isn't identical to it). + out << "(subtype " << n.getConst() << ')'; + break; + default: // fall back on whatever operator<< does on underlying type; we // might luck out and be SMT-LIB v2 compliant diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 9f49d81a2..396454fac 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -50,9 +50,19 @@ CnfStream::CnfStream(SatSolverInterface *satSolver, Registrar* registrar, bool f d_registrar(registrar) { } -void CnfStream::recordTranslation(TNode node) { +void CnfStream::recordTranslation(TNode node, bool alwaysRecord) { + Debug("cnf") << "recordTranslation(" << alwaysRecord << "," << d_removable << "): " << node << std::endl; if (!d_removable) { - d_translationTrail.push_back(stripNot(node)); + node = stripNot(node); + if(d_translationCache.find(node)->second.recorded) { + Debug("cnf") << "--> Already recorded, not recording again." << std::endl; + } else { + Debug("cnf") << "--> Recorded at position " << d_translationTrail.size() << ". (level " << d_translationCache.find(node)->second.level << ")" << std::endl; + Assert(d_translationTrail.empty() || d_translationCache.find(node)->second.level >= d_translationCache.find(d_translationTrail.back())->second.level, "levels on the translation trail should be monotonically increasing ?!"); + d_translationTrail.push_back(node); + d_translationCache.find(node)->second.recorded = true; + d_translationCache.find(node.notNode())->second.recorded = true; + } } } @@ -112,7 +122,8 @@ bool CnfStream::hasLiteral(TNode n) const { void TseitinCnfStream::ensureLiteral(TNode n) { if(hasLiteral(n)) { // Already a literal! - SatLiteral lit = getLiteral(n); + // newLiteral() may be necessary to renew a previously-extant literal + SatLiteral lit = isTranslated(n) ? getLiteral(n) : newLiteral(n, true); NodeCache::iterator i = d_nodeCache.find(lit); if(i == d_nodeCache.end()) { // Store backward-mappings @@ -158,11 +169,12 @@ void TseitinCnfStream::ensureLiteral(TNode n) { SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { Debug("cnf") << "newLiteral(" << node << ", " << theoryLiteral << ")" << endl; + Assert(node.getKind() != kind::NOT); // Get the literal for this node SatLiteral lit; if (!hasLiteral(node)) { - // If no literal, well make one + // If no literal, we'll make one lit = SatLiteral(d_satSolver->newVar(theoryLiteral)); d_translationCache[node].literal = lit; d_translationCache[node.notNode()].literal = ~lit; @@ -174,13 +186,15 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { // We will translate clauses, so remember the level int level = d_satSolver->getAssertionLevel(); + d_translationCache[node].recorded = false; + d_translationCache[node.notNode()].recorded = false; d_translationCache[node].level = level; d_translationCache[node.notNode()].level = level; // If it's a theory literal, need to store it for back queries if ( theoryLiteral || d_fullLitToNodeMap || ( CVC4_USE_REPLAY && Options::current()->replayLog != NULL ) || - Dump.isOn("clauses") ) { + (Dump.isOn("clauses")) ) { d_nodeCache[lit] = node; d_nodeCache[~lit] = node.notNode(); } @@ -223,6 +237,11 @@ SatLiteral CnfStream::convertAtom(TNode node) { } } + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(node, true); + return lit; } @@ -250,6 +269,11 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) { assertClause(xorNode, a, ~b, xorLit); assertClause(xorNode, ~a, b, xorLit); + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(xorNode, true); + return xorLit; } @@ -285,6 +309,11 @@ SatLiteral TseitinCnfStream::handleOr(TNode orNode) { // This needs to go last, as the clause might get modified by the SAT solver assertClause(orNode, clause); + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(orNode, true); + // Return the literal return orLit; } @@ -321,6 +350,12 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) { clause[n_children] = andLit; // This needs to go last, as the clause might get modified by the SAT solver assertClause(andNode, clause); + + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(andNode, true); + return andLit; } @@ -345,6 +380,11 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) { assertClause(impliesNode, a, impliesLit); assertClause(impliesNode, ~b, impliesLit); + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(impliesNode, true); + return impliesLit; } @@ -377,6 +417,11 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) { assertClause(iffNode, ~a, ~b, iffLit); assertClause(iffNode, a, b, iffLit); + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(iffNode, true); + return iffLit; } @@ -423,6 +468,11 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) { assertClause(iteNode, iteLit, ~condLit, ~thenLit); assertClause(iteNode, iteLit, condLit, ~elseLit); + // We have a literal, so it has to be recorded. The definitional clauses + // go away on user-pop, so this literal will have to be re-vivified if it's + // used subsequently. + recordTranslation(iteNode, true); + return iteLit; } @@ -435,6 +485,7 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { // If the non-negated node has already been translated, get the translation if(isTranslated(node)) { + Debug("cnf") << "toCNF(): already translated" << endl; nodeLit = getLiteral(node); } else { // Handle each Boolean operator case @@ -690,15 +741,19 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { void CnfStream::removeClausesAboveLevel(int level) { while (d_translationTrail.size() > 0) { + Debug("cnf") << "Considering translation trail position " << d_translationTrail.size() << std::endl; TNode node = d_translationTrail.back(); + // Get the translation information + TranslationInfo& infoPos = d_translationCache.find(node)->second; + // If the level of the node is less or equal to given we are done + if (infoPos.level >= 0 && infoPos.level <= level) { + Debug("cnf") << "Node is " << node << " level " << infoPos.level << ", we're done." << std::endl; + break; + } Debug("cnf") << "Removing node " << node << " from CNF translation" << endl; d_translationTrail.pop_back(); - // Get the translation informations - TranslationInfo& infoPos = d_translationCache.find(node)->second; // If already untranslated, we're done if (infoPos.level == -1) continue; - // If the level of the node is less or equal to given we are done - if (infoPos.level <= level) break; // Otherwise we have to undo the translation undoTranslate(node, level); } @@ -734,6 +789,7 @@ void CnfStream::undoTranslate(TNode node, int level) { // Untranslate infoPos.level = -1; + infoPos.recorded = false; // Untranslate the negation node // If not a not node, unregister it from sat and untranslate the negation @@ -747,6 +803,7 @@ void CnfStream::undoTranslate(TNode node, int level) { Assert(it != d_translationCache.end()); TranslationInfo& infoNeg = (*it).second; infoNeg.level = -1; + infoNeg.recorded = false; } // undoTranslate the children diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index c9306952b..4812c6a21 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -52,6 +52,7 @@ public: /** Per node translation information */ struct TranslationInfo { + bool recorded; /** The level at which this node was translated (negative if not translated) */ int level; /** The literal of this node */ @@ -109,7 +110,7 @@ protected: } /** Record this translation */ - void recordTranslation(TNode node); + void recordTranslation(TNode node, bool alwaysRecord = false); /** * Moves the node and all of it's parents to level 0. diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 3fe9db10c..678fe28dc 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -714,10 +714,11 @@ CRef Solver::propagate(TheoryCheckType type) } void Solver::propagateTheory() { - - SatClause propagatedLiteralsClause; + SatClause propagatedLiteralsClause; + // Doesn't actually call propagate(); that's done in theoryCheck() now that combination + // is online. This just incorporates those propagations previously discovered. proxy->theoryPropagate(propagatedLiteralsClause); - + vec propagatedLiterals; DPLLMinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals); @@ -885,10 +886,22 @@ void Solver::removeClausesAboveLevel(vec& cs, int level) for (i = j = 0; i < cs.size(); i++){ Clause& c = ca[cs[i]]; if (c.level() > level) { - Debug("minisat") << "removeClausesAboveLevel(" << level << "): removing level-" << c.level() << " clause: " << c << std::endl; + if(Debug.isOn("minisat")) { + Debug("minisat") << "removeClausesAboveLevel(" << level << "): removing level-" << c.level() << " clause: " << c << ":"; + for(int i = 0; i < c.size(); ++i) { + Debug("minisat") << " " << c[i]; + } + Debug("minisat") << std::endl; + } removeClause(cs[i]); } else { - Debug("minisat") << "removeClausesAboveLevel(" << level << "): leaving level-" << c.level() << " clause: " << c << std::endl; + if(Debug.isOn("minisat")) { + Debug("minisat") << "removeClausesAboveLevel(" << level << "): leaving level-" << c.level() << " clause: " << c << ":"; + for(int i = 0; i < c.size(); ++i) { + Debug("minisat") << " " << c[i]; + } + Debug("minisat") << std::endl; + } cs[j++] = cs[i]; } } @@ -1328,16 +1341,25 @@ void Solver::push() Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl; trail_user.push(lit_Undef); trail_ok.push(ok); + trail_user_lim.push(trail.size()); + assert(trail_user_lim.size() == assertionLevel); + Debug("minisat") << "MINISAT PUSH assertionLevel is " << assertionLevel << ", trail.size is " << trail.size() << std::endl; } void Solver::pop() { assert(enable_incremental); + Debug("minisat") << "MINISAT POP at level " << decisionLevel() << " (context " << context->getLevel() << "), popping trail..." << std::endl; popTrail(); + Debug("minisat") << "MINISAT POP now at " << decisionLevel() << " (context " << context->getLevel() << ")" << std::endl; + + assert(decisionLevel() == 0); + assert(trail_user_lim.size() == assertionLevel); --assertionLevel; + Debug("minisat") << "MINISAT POP assertionLevel is now down to " << assertionLevel << ", trail.size is " << trail.size() << ", need to get down to " << trail_user_lim.last() << std::endl; Debug("minisat") << "in user pop, reducing assertion level to " << assertionLevel << " and removing clauses above this from db" << std::endl; // Remove all the clauses asserted (and implied) above the new base level @@ -1346,6 +1368,23 @@ void Solver::pop() Debug("minisat") << "in user pop, at " << trail_lim.size() << " : " << assertionLevel << std::endl; + int downto = trail_user_lim.last(); + while(downto < trail.size()) { + Debug("minisat") << "== unassigning " << trail.last() << std::endl; + Var x = var(trail.last()); + if(intro_level(x) != -1) {// might be unregistered + assigns [x] = l_Undef; + vardata[x].trail_index = -1; + polarity[x] = sign(trail.last()); + insertVarOrder(x); + } + trail.pop(); + } + qhead = trail.size(); + Debug("minisat") << "MINISAT POP assertionLevel is now down to " << assertionLevel << ", trail.size is " << trail.size() << ", should be at " << trail_user_lim.last() << std::endl; + assert(trail_user_lim.last() == qhead); + trail_user_lim.pop(); + // Unset any units learned or added at this level Debug("minisat") << "in user pop, unsetting level units for level " << assertionLevel << std::endl; while(trail_user.last() != lit_Undef) { diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 426268b4b..c0dd00166 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -191,6 +191,10 @@ public: int nVars () const; // The current number of variables. int nFreeVars () const; + // Debugging SMT explanations + // + bool properExplanation(Lit l, Lit expl) const; // returns true if expl can be used to explain l---i.e., both assigned and trail_index(expl) < trail_index(l) + // Resource contraints: // void setConfBudget(int64_t x); @@ -282,6 +286,7 @@ protected: vec trail; // Assignment stack; stores all assigments made in the order they were made. vec trail_lim; // Separator indices for different decision levels in 'trail'. vec trail_user; // Stack of assignments to UNdo on user pop. + vec trail_user_lim; // Separator indices for different user levels in 'trail'. vec trail_ok; // Stack of "whether we're in conflict" flags. vec vardata; // Stores reason and level for each variable. int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat). @@ -462,6 +467,7 @@ inline int Solver::nClauses () const { return clauses_persisten inline int Solver::nLearnts () const { return clauses_removable.size(); } inline int Solver::nVars () const { return vardata.size(); } inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); } +inline bool Solver::properExplanation(Lit l, Lit expl) const { return value(l) == l_True && value(expl) == l_True && trail_index(var(expl)) < trail_index(var(l)); } inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; } inline void Solver::setDecisionVar(Var v, bool b) { diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 7d0353122..2538e6d0c 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -232,6 +232,10 @@ void PropEngine::pop() { Debug("prop") << "pop()" << endl; } +bool PropEngine::isRunning() const { + return d_inCheckSat; +} + void PropEngine::interrupt() throw(ModalException) { if(! d_inCheckSat) { throw ModalException("SAT solver is not currently solving anything; " @@ -247,5 +251,49 @@ void PropEngine::spendResource() throw() { // TODO implement me } +bool PropEngine::properExplanation(TNode node, TNode expl) const { + if(! d_cnfStream->hasLiteral(node)) { + Trace("properExplanation") << "properExplanation(): Failing because node " + << "being explained doesn't have a SAT literal ?!" << std::endl + << "properExplanation(): The node is: " << node << std::endl; + return false; + } + + SatLiteral nodeLit = d_cnfStream->getLiteral(node); + + for(TNode::kinded_iterator i = expl.begin(kind::AND), + i_end = expl.end(kind::AND); + i != i_end; + ++i) { + if(! d_cnfStream->hasLiteral(*i)) { + Trace("properExplanation") << "properExplanation(): Failing because one of explanation " + << "nodes doesn't have a SAT literal" << std::endl + << "properExplanation(): The explanation node is: " << *i << std::endl; + return false; + } + + SatLiteral iLit = d_cnfStream->getLiteral(*i); + + if(iLit == nodeLit) { + Trace("properExplanation") << "properExplanation(): Failing because the node" << std::endl + << "properExplanation(): " << node << std::endl + << "properExplanation(): cannot be made to explain itself!" << std::endl; + return false; + } + + if(! d_satSolver->properExplanation(nodeLit, iLit)) { + Trace("properExplanation") << "properExplanation(): SAT solver told us that node" << std::endl + << "properExplanation(): " << *i << std::endl + << "properExplanation(): is not part of a proper explanation node for" << std::endl + << "properExplanation(): " << node << std::endl + << "properExplanation(): Perhaps it one of the two isn't assigned or the explanation" << std::endl + << "properExplanation(): node wasn't propagated before the node being explained" << std::endl; + return false; + } + } + + return true; +} + }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 4f83888fc..91b9a61e6 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -241,6 +241,12 @@ public: */ void pop(); + /** + * Return true if we are currently searching (either in this or + * another thread). + */ + bool isRunning() const; + /** * Check the current time budget. */ @@ -258,11 +264,23 @@ public: */ void spendResource() throw(); + /** + * For debugging. Return true if "expl" is a well-formed + * explanation for "node," meaning: + * + * 1. expl is either a SAT literal or an AND of SAT literals + * currently assigned true; + * 2. node is assigned true; + * 3. node does not appear in expl; and + * 4. node was assigned after all of the literals in expl + */ + bool properExplanation(TNode node, TNode expl) const; + };/* class PropEngine */ inline void SatTimer::check() { - if(expired()) { + if(d_propEngine.isRunning() && expired()) { Trace("limit") << "SatTimer::check(): interrupt!" << std::endl; d_propEngine.interrupt(); } diff --git a/src/prop/sat.h b/src/prop/sat.h index a6bdcb309..14b42e445 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -49,6 +49,30 @@ class PropEngine; class CnfStream; /* Definitions of abstract types and conversion functions for SAT interface */ +/* +inline SatLiteral variableToLiteral(SatVariable var) { + return Minisat::mkLit(var); +} + +inline bool literalSign(SatLiteral lit) { + return Minisat::sign(lit); +} + +static inline size_t +hashSatLiteral(const SatLiteral& literal) { + return (size_t) Minisat::toInt(literal); +} + +inline std::string stringOfLiteralValue(SatLiteralValue val) { + if( val == l_False ) { + return "0"; + } else if (val == l_True ) { + return "1"; + } else { // unknown + return "_"; + } +} +*/ /** * The proxy class that allows the SatSolver to communicate with the theories diff --git a/src/prop/sat_module.cpp b/src/prop/sat_module.cpp index 9391acbe5..db911f488 100644 --- a/src/prop/sat_module.cpp +++ b/src/prop/sat_module.cpp @@ -383,6 +383,9 @@ SatLiteralValue DPLLMinisatSatSolver::modelValue(SatLiteral l){ return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l))); } +bool DPLLMinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const { + return true; +} /** Incremental interface */ diff --git a/src/prop/sat_module.h b/src/prop/sat_module.h index 320dfe09b..9c49c7d67 100644 --- a/src/prop/sat_module.h +++ b/src/prop/sat_module.h @@ -152,6 +152,8 @@ public: virtual void pop() = 0; + virtual bool properExplanation(SatLiteral lit, SatLiteral expl) const = 0; + }; // toodo add ifdef @@ -179,11 +181,11 @@ public: SatLiteralValue value(SatLiteral l); SatLiteralValue modelValue(SatLiteral l); - void unregisterVar(SatLiteral lit); void renewVar(SatLiteral lit, int level = -1); int getAssertionLevel() const; + // helper methods for converting from the internal Minisat representation static SatVariable toSatVariable(BVMinisat::Var var); @@ -254,6 +256,8 @@ public: SatLiteralValue modelValue(SatLiteral l); + bool properExplanation(SatLiteral lit, SatLiteral expl) const; + /** Incremental interface */ int getAssertionLevel() const; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7bf22c2c0..3c320b814 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -18,8 +18,10 @@ #include #include +#include #include #include +#include #include #include "context/cdlist.h" @@ -27,6 +29,8 @@ #include "context/context.h" #include "expr/command.h" #include "expr/expr.h" +#include "expr/kind.h" +#include "expr/metakind.h" #include "expr/node_builder.h" #include "prop/prop_engine.h" #include "smt/bad_option_exception.h" @@ -119,6 +123,17 @@ class SmtEnginePrivate { /** The top level substitutions */ theory::SubstitutionMap d_topLevelSubstitutions; + /** + * The last substition that the SAT layer was told about. + * In incremental settings, substitutions cannot be performed + * "backward," only forward. So SAT needs to be told of all + * substitutions that are going to be done. This iterator + * holds the last substitution from d_topLevelSubstitutions + * that was pushed out to SAT. + * If d_lastSubstitutionPos == d_topLevelSubstitutions.end(), + * then nothing has been pushed out yet. */ + context::CDO d_lastSubstitutionPos; + /** * Runs the nonclausal solver and tries to solve all the assigned * theory literals. @@ -135,6 +150,14 @@ class SmtEnginePrivate { */ void removeITEs(); + /** + * Any variable in a assertion that is declared as a subtype type + * (predicate subtype or integer subrange type) must be constrained + * to be in that type. + */ + void constrainSubtypes(TNode n, std::vector& assertions) + throw(AssertionException); + /** * Perform non-clausal simplification of a Node. This involves * Theory implementations, but does NOT involve the SAT solver in @@ -148,7 +171,8 @@ public: d_smt(smt), d_nonClausalLearnedLiterals(), d_propagator(smt.d_userContext, d_nonClausalLearnedLiterals, true, true), - d_topLevelSubstitutions(smt.d_userContext) { + d_topLevelSubstitutions(smt.d_userContext), + d_lastSubstitutionPos(smt.d_userContext, d_topLevelSubstitutions.end()) { } Node applySubstitutions(TNode node) const { @@ -160,6 +184,17 @@ public: */ void processAssertions(); + /** + * Process a user pop. Clears out the non-context-dependent stuff in this + * SmtEnginePrivate. Necessary to clear out our assertion vectors in case + * someone does a push-assert-pop without a check-sat. + */ + void notifyPop() { + d_assertionsToPreprocess.clear(); + d_nonClausalLearnedLiterals.clear(); + d_assertionsToCheck.clear(); + } + /** * Adds a formula to the current context. Action here depends on * the SimplificationMode (in the current Options scope); the @@ -175,6 +210,7 @@ public: */ Node expandDefinitions(TNode n, hash_map& cache) throw(NoSuchFunctionException, AssertionException); + };/* class SmtEnginePrivate */ }/* namespace CVC4::smt */ @@ -231,7 +267,14 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_definedFunctions = new(true) DefinedFunctionMap(d_userContext); - if(Options::current()->interactive) { + // [MGD 10/20/2011] keep around in incremental mode, due to a + // cleanup ordering issue and Nodes/TNodes. If SAT is popped + // first, some user-context-dependent TNodes might still exist + // with rc == 0. + if(Options::current()->interactive || + Options::current()->incrementalSolving) { + // In the case of incremental solving, we appear to need these to + // ensure the relevant Nodes remain live. d_assertionList = new(true) AssertionList(d_userContext); } @@ -265,31 +308,39 @@ void SmtEngine::shutdown() { d_theoryEngine->shutdown(); } -SmtEngine::~SmtEngine() { +SmtEngine::~SmtEngine() throw() { NodeManagerScope nms(d_nodeManager); - shutdown(); + try { + while(Options::current()->incrementalSolving && d_userContext->getLevel() > 0) { + internalPop(); + } + + shutdown(); - if(d_assignments != NULL) { - d_assignments->deleteSelf(); - } + if(d_assignments != NULL) { + d_assignments->deleteSelf(); + } - if(d_assertionList != NULL) { - d_assertionList->deleteSelf(); - } + if(d_assertionList != NULL) { + d_assertionList->deleteSelf(); + } - d_definedFunctions->deleteSelf(); + d_definedFunctions->deleteSelf(); - StatisticsRegistry::unregisterStat(&d_definitionExpansionTime); - StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime); - StatisticsRegistry::unregisterStat(&d_staticLearningTime); + StatisticsRegistry::unregisterStat(&d_definitionExpansionTime); + StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime); + StatisticsRegistry::unregisterStat(&d_staticLearningTime); - // Deletion order error: circuit propagator has some unsafe TNodes ?! - // delete d_private; - delete d_userContext; + delete d_private; + delete d_userContext; - delete d_theoryEngine; - delete d_propEngine; + delete d_theoryEngine; + delete d_propEngine; + } catch(Exception& e) { + Warning() << "CVC4 threw an exception during cleanup." << endl + << e << endl; + } } void SmtEngine::setLogic(const std::string& s) throw(ModalException) { @@ -415,7 +466,11 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value) } if(key == ":print-success") { - throw BadOptionException(); + if(value.isAtom() && value.getValue() == "false") { + // fine; don't need to do anything + } else { + throw BadOptionException(); + } } else if(key == ":expand-definitions") { throw BadOptionException(); } else if(key == ":interactive-mode") { @@ -641,17 +696,17 @@ void SmtEnginePrivate::nonClausalSimplify() { Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "applying substitutions" << endl; for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { - Trace("simplify") << "applying to " << d_assertionsToPreprocess[i] << std::endl; + Trace("simplify") << "applying to " << d_assertionsToPreprocess[i] << endl; d_assertionsToPreprocess[i] = theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i])); - Trace("simplify") << " got " << d_assertionsToPreprocess[i] << std::endl; + Trace("simplify") << " got " << d_assertionsToPreprocess[i] << endl; } // Assert all the assertions to the propagator Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "asserting to propagator" << endl; for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { - Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertionsToPreprocess[i] << std::endl; + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertionsToPreprocess[i] << endl; d_propagator.assert(d_assertionsToPreprocess[i]); } @@ -691,6 +746,7 @@ void SmtEnginePrivate::nonClausalSimplify() { << "solving " << learnedLiteral << endl; Theory::PPAssertStatus solveStatus = d_smt.d_theoryEngine->solve(learnedLiteral, d_topLevelSubstitutions); + switch (solveStatus) { case Theory::PP_ASSERT_STATUS_CONFLICT: // If in conflict, we return false @@ -711,6 +767,27 @@ void SmtEnginePrivate::nonClausalSimplify() { d_nonClausalLearnedLiterals[j++] = d_nonClausalLearnedLiterals[i]; break; } + + if( Options::current()->incrementalSolving || + Options::current()->simplificationMode == Options::SIMPLIFICATION_MODE_INCREMENTAL ) { + // Tell PropEngine about new substitutions + SubstitutionMap::iterator pos = d_lastSubstitutionPos; + if(pos == d_topLevelSubstitutions.end()) { + pos = d_topLevelSubstitutions.begin(); + } else { + ++pos; + } + + while(pos != d_topLevelSubstitutions.end()) { + // Push out this substitution + TNode lhs = (*pos).first, rhs = (*pos).second; + Node n = NodeManager::currentNM()->mkNode(lhs.getType().isBoolean() ? kind::IFF : kind::EQUAL, lhs, rhs); + d_assertionsToCheck.push_back(n); + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n << endl; + d_lastSubstitutionPos = pos; + ++pos; + } + } } // Resize the learnt d_nonClausalLearnedLiterals.resize(j); @@ -733,6 +810,63 @@ void SmtEnginePrivate::nonClausalSimplify() { d_assertionsToPreprocess.clear(); } +void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector& assertions) + throw(AssertionException) { + + Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top << endl; + + set done; + stack worklist; + worklist.push(top); + done.insert(top); + + do { + TNode n = worklist.top(); + worklist.pop(); + + TypeNode t = n.getType(); + if(t.isPredicateSubtype()) { + WarningOnce() << "Warning: CVC4 doesn't yet do checking that predicate subtypes are nonempty domains" << endl; + Node pred = t.getSubtypePredicate(); + Kind k; + // pred can be a LAMBDA, a function constant, or a datatype tester + Trace("constrainSubtypes") << "constrainSubtypes(): pred.getType() == " << pred.getType() << endl; + if(d_smt.d_definedFunctions->find(pred) != d_smt.d_definedFunctions->end()) { + k = kind::APPLY; + } else if(pred.getType().isTester()) { + k = kind::APPLY_TESTER; + } else { + k = kind::APPLY_UF; + } + Node app = NodeManager::currentNM()->mkNode(k, pred, n); + Trace("constrainSubtypes") << "constrainSubtypes(): assert(" << k << ") " << app << endl; + assertions.push_back(app); + } else if(t.isSubrange()) { + SubrangeBounds bounds = t.getSubrangeBounds(); + Trace("constrainSubtypes") << "constrainSubtypes(): got bounds " << bounds << endl; + if(bounds.lower.hasBound()) { + Node c = NodeManager::currentNM()->mkConst(bounds.lower.getBound()); + Node lb = NodeManager::currentNM()->mkNode(kind::LEQ, c, n); + Trace("constrainSubtypes") << "constrainSubtypes(): assert " << lb << endl; + assertions.push_back(lb); + } + if(bounds.upper.hasBound()) { + Node c = NodeManager::currentNM()->mkConst(bounds.upper.getBound()); + Node ub = NodeManager::currentNM()->mkNode(kind::LEQ, n, c); + Trace("constrainSubtypes") << "constrainSubtypes(): assert " << ub << endl; + assertions.push_back(ub); + } + } + + for(TNode::iterator i = n.begin(); i != n.end(); ++i) { + if(done.find(*i) == done.end()) { + worklist.push(*i); + done.insert(*i); + } + } + } while(! worklist.empty()); +} + void SmtEnginePrivate::simplifyAssertions() throw(NoSuchFunctionException, AssertionException) { try { @@ -821,7 +955,7 @@ Result SmtEngine::check() { d_cumulativeResourceUsed += resource; Trace("limit") << "SmtEngine::check(): cumulative millis " << d_cumulativeTimeUsed - << ", conflicts " << d_cumulativeResourceUsed << std::endl; + << ", conflicts " << d_cumulativeResourceUsed << endl; return result; } @@ -835,9 +969,28 @@ void SmtEnginePrivate::processAssertions() { Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl; + Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; + Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + + // Any variables of subtype types need to be constrained properly. + // Careful, here: constrainSubtypes() adds to the back of + // d_assertionsToPreprocess, but we don't need to reprocess those. + // We also can't use an iterator, because the vector may be moved in + // memory during this loop. + for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) { + constrainSubtypes(d_assertionsToPreprocess[i], d_assertionsToPreprocess); + } + + Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; + Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + // Simplify the assertions simplifyAssertions(); + Trace("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl; + Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; + Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + if(Dump.isOn("assertions")) { // Push the simplified assertions to the dump output stream for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { @@ -1201,6 +1354,7 @@ size_t SmtEngine::getStackLevel() const { void SmtEngine::push() { NodeManagerScope nms(d_nodeManager); Trace("smt") << "SMT push()" << endl; + d_private->processAssertions(); if(Dump.isOn("benchmark")) { Dump("benchmark") << PushCommand() << endl; } @@ -1245,6 +1399,9 @@ void SmtEngine::pop() { } d_userLevels.pop_back(); + // Clear out assertion queues etc., in case anything is still in there + d_private->notifyPop(); + Trace("userpushpop") << "SmtEngine: popped to level " << d_userContext->getLevel() << endl; // FIXME: should we reset d_status here? @@ -1258,6 +1415,7 @@ void SmtEngine::internalPush() { if(Options::current()->incrementalSolving) { d_private->processAssertions(); d_userContext->push(); + d_context->push(); d_propEngine->push(); } } @@ -1266,6 +1424,7 @@ void SmtEngine::internalPop() { Trace("smt") << "SmtEngine::internalPop()" << endl; if(Options::current()->incrementalSolving) { d_propEngine->pop(); + d_context->pop(); d_userContext->pop(); } } @@ -1276,20 +1435,20 @@ void SmtEngine::interrupt() throw(ModalException) { void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) { if(cumulative) { - Trace("limit") << "SmtEngine: setting cumulative resource limit to " << units << std::endl; + Trace("limit") << "SmtEngine: setting cumulative resource limit to " << units << endl; d_resourceBudgetCumulative = (units == 0) ? 0 : (d_cumulativeResourceUsed + units); } else { - Trace("limit") << "SmtEngine: setting per-call resource limit to " << units << std::endl; + Trace("limit") << "SmtEngine: setting per-call resource limit to " << units << endl; d_resourceBudgetPerCall = units; } } void SmtEngine::setTimeLimit(unsigned long millis, bool cumulative) { if(cumulative) { - Trace("limit") << "SmtEngine: setting cumulative time limit to " << millis << " ms" << std::endl; + Trace("limit") << "SmtEngine: setting cumulative time limit to " << millis << " ms" << endl; d_timeBudgetCumulative = (millis == 0) ? 0 : (d_cumulativeTimeUsed + millis); } else { - Trace("limit") << "SmtEngine: setting per-call time limit to " << millis << " ms" << std::endl; + Trace("limit") << "SmtEngine: setting per-call time limit to " << millis << " ms" << endl; d_timeBudgetPerCall = millis; } } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 17717e440..84d6d1a73 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -231,7 +231,7 @@ public: /** * Destruct the SMT engine. */ - ~SmtEngine(); + ~SmtEngine() throw(); /** * Set the logic of the script. diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index a309b9403..c0ef02ec4 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -93,6 +93,21 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ return preRewritePlus(t); }else if(t.getKind() == kind::MULT){ return preRewriteMult(t); + }else if(t.getKind() == kind::INTS_DIVISION){ + Integer intOne(1); + if(t[1].getKind()== kind::CONST_INTEGER && t[1].getConst() == intOne){ + return RewriteResponse(REWRITE_AGAIN, t[0]); + }else{ + return RewriteResponse(REWRITE_DONE, t); + } + }else if(t.getKind() == kind::INTS_MODULUS){ + Integer intOne(1); + if(t[1].getKind()== kind::CONST_INTEGER && t[1].getConst() == intOne){ + Integer intZero(0); + return RewriteResponse(REWRITE_AGAIN, mkIntegerNode(intZero)); + }else{ + return RewriteResponse(REWRITE_DONE, t); + } }else{ Unreachable(); } @@ -112,6 +127,10 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ return postRewritePlus(t); }else if(t.getKind() == kind::MULT){ return postRewriteMult(t); + }else if(t.getKind() == kind::INTS_DIVISION){ + return RewriteResponse(REWRITE_DONE, t); + }else if(t.getKind() == kind::INTS_MODULUS){ + return RewriteResponse(REWRITE_DONE, t); }else{ Unreachable(); } diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index bf5ea24c1..95d7d6ed1 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -17,7 +17,9 @@ operator PLUS 2: "arithmetic addition" operator MULT 2: "arithmetic multiplication" operator MINUS 2 "arithmetic binary subtraction operator" operator UMINUS 1 "arithmetic unary negation" -operator DIVISION 2 "arithmetic division" +operator DIVISION 2 "real division" +operator INTS_DIVISION 2 "ints division" +operator INTS_MODULUS 2 "ints modulus" operator POW 2 "arithmetic power" sort REAL_TYPE \ @@ -39,6 +41,19 @@ sort PSEUDOBOOLEAN_TYPE \ "expr/node_manager.h" \ "Pseudoboolean type" +constant SUBRANGE_TYPE \ + ::CVC4::SubrangeBounds \ + ::CVC4::SubrangeBoundsHashStrategy \ + "util/subrange_bound.h" \ + "the type of an integer subrange" +cardinality SUBRANGE_TYPE \ + "::CVC4::theory::arith::SubrangeProperties::computeCardinality(%TYPE%)" \ + "theory/arith/theory_arith_type_rules.h" +well-founded SUBRANGE_TYPE \ + true \ + "::CVC4::theory::arith::SubrangeProperties::mkGroundTerm(%TYPE%)" \ + "theory/arith/theory_arith_type_rules.h" + constant CONST_RATIONAL \ ::CVC4::Rational \ ::CVC4::RationalHashStrategy \ @@ -75,4 +90,7 @@ typerule LEQ ::CVC4::theory::arith::ArithPredicateTypeRule typerule GT ::CVC4::theory::arith::ArithPredicateTypeRule typerule GEQ ::CVC4::theory::arith::ArithPredicateTypeRule +typerule INTS_DIVISION ::CVC4::theory::arith::ArithOperatorTypeRule +typerule INTS_MODULUS ::CVC4::theory::arith::ArithOperatorTypeRule + endtheory diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 511982d48..8d0d79f0a 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -21,6 +21,8 @@ #ifndef __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H #define __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H +#include "util/subrange_bound.h" + namespace CVC4 { namespace theory { namespace arith { @@ -33,7 +35,7 @@ public: if (n.getKind() == kind::CONST_RATIONAL) return nodeManager->realType(); return nodeManager->integerType(); } -}; +};/* class ArithConstantTypeRule */ class ArithOperatorTypeRule { public: @@ -60,7 +62,7 @@ public: } return (isInteger ? integerType : realType); } -}; +};/* class ArithOperatorTypeRule */ class ArithPredicateTypeRule { public: @@ -80,7 +82,33 @@ public: } return nodeManager->booleanType(); } -}; +};/* class ArithPredicateTypeRule */ + +class SubrangeProperties { +public: + inline static Cardinality computeCardinality(TypeNode type) { + Assert(type.getKind() == kind::SUBRANGE_TYPE); + + const SubrangeBounds& bounds = type.getConst(); + if(!bounds.lower.hasBound() || !bounds.upper.hasBound()) { + return Cardinality::INTEGERS; + } + return Cardinality(bounds.upper.getBound() - bounds.lower.getBound()); + } + + inline static Node mkGroundTerm(TypeNode type) { + Assert(type.getKind() == kind::SUBRANGE_TYPE); + + const SubrangeBounds& bounds = type.getConst(); + if(bounds.lower.hasBound()) { + return NodeManager::currentNM()->mkConst(bounds.lower.getBound()); + } + if(bounds.upper.hasBound()) { + return NodeManager::currentNM()->mkConst(bounds.upper.getBound()); + } + return NodeManager::currentNM()->mkConst(Integer(0)); + } +};/* class SubrangeProperties */ }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 61abfbfaf..519536c81 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -325,4 +325,17 @@ typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule +constant SUBTYPE_TYPE \ + ::CVC4::Predicate \ + ::CVC4::PredicateHashStrategy \ + "util/predicate.h" \ + "predicate subtype" +cardinality SUBTYPE_TYPE \ + "::CVC4::theory::builtin::SubtypeProperties::computeCardinality(%TYPE%)" \ + "theory/builtin/theory_builtin_type_rules.h" +well-founded SUBTYPE_TYPE \ + "::CVC4::theory::builtin::SubtypeProperties::isWellFounded(%TYPE%)" \ + "::CVC4::theory::builtin::SubtypeProperties::mkGroundTerm(%TYPE%)" \ + "theory/builtin/theory_builtin_type_rules.h" + endtheory diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index cd3e1437f..706196f8b 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -227,6 +227,26 @@ public: } };/* class TupleProperties */ +class SubtypeProperties { +public: + + inline static Cardinality computeCardinality(TypeNode type) { + Assert(type.getKind() == kind::SUBTYPE_TYPE); + Unimplemented("Computing the cardinality for predicate subtype not yet supported."); + } + + inline static bool isWellFounded(TypeNode type) { + Assert(type.getKind() == kind::SUBTYPE_TYPE); + Unimplemented("Computing the well-foundedness for predicate subtype not yet supported."); + } + + inline static Node mkGroundTerm(TypeNode type) { + Assert(type.getKind() == kind::SUBTYPE_TYPE); + Unimplemented("Constructing a ground term for predicate subtype not yet supported."); + } + +};/* class SubtypeProperties */ + }/* CVC4::theory::builtin namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index 301cb8d60..caf7566b9 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -173,4 +173,9 @@ void SubstitutionMap::print(ostream& out) const { } }/* CVC4::theory namespace */ + +std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i) { + return out << "[CDMap-iterator]"; +} + }/* CVC4 namespace */ diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index c03baa1ac..1ade4815d 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -48,6 +48,9 @@ public: typedef context::CDMap NodeMap; + typedef NodeMap::iterator iterator; + typedef NodeMap::const_iterator const_iterator; + private: typedef std::hash_map NodeCache; @@ -115,6 +118,22 @@ public: return const_cast(this)->apply(t); } + iterator begin() { + return d_substitutions.begin(); + } + + iterator end() { + return d_substitutions.end(); + } + + const_iterator begin() const { + return d_substitutions.begin(); + } + + const_iterator end() const { + return d_substitutions.end(); + } + // NOTE [MGD]: removed clear() and swap() from the interface // when this data structure became context-dependent // because they weren't used---and it's not clear how they @@ -134,6 +153,9 @@ inline std::ostream& operator << (std::ostream& out, const SubstitutionMap& subs } }/* CVC4::theory namespace */ + +std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i); + }/* CVC4 namespace */ #endif /* __CVC4__THEORY__SUBSTITUTIONS_H */ diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 1998498f5..76aabeb1f 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -76,5 +76,14 @@ void Theory::computeCareGraph(CareGraph& careGraph) { } } +void Theory::printFacts(std::ostream& os) const { + unsigned i, n = d_facts.size(); + for(i = 0; i < n; i++){ + const Assertion& a_i = d_facts[i]; + Node assertion = a_i; + os << d_id << '[' << i << ']' << " " << assertion << endl; + } +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory.h b/src/theory/theory.h index b0f5e4e53..35c81239f 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -142,7 +142,7 @@ private: protected: - /** + /** * A list of shared terms that the theory has. */ context::CDList d_sharedTerms; @@ -210,6 +210,9 @@ protected: */ static TheoryId s_uninterpretedSortOwner; + void printFacts(std::ostream& os) const; + + public: /** @@ -218,6 +221,9 @@ public: static inline TheoryId theoryOf(TypeNode typeNode) { Trace("theory") << "theoryOf(" << typeNode << ")" << std::endl; TheoryId id; + while (typeNode.isPredicateSubtype()) { + typeNode = typeNode.getSubtypeBaseType(); + } if (typeNode.getKind() == kind::TYPE_CONSTANT) { id = typeConstantToTheoryId(typeNode.getConst()); } else { diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 91d6beead..2950ad413 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -575,8 +575,10 @@ void TheoryEngine::assertFact(TNode node) // Get the atom TNode atom = node.getKind() == kind::NOT ? node[0] : node; - // Assert the fact to the apropriate theory - theoryOf(atom)->assertFact(node, true); + // Assert the fact to the appropriate theory and mark it active + Theory* theory = theoryOf(atom); + theory->assertFact(node, true); + markActive(Theory::setInsert(theory->getId())); // If any shared terms, notify the theories if (d_sharedTerms.hasSharedTerms(atom)) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index ceefa88e8..72244a573 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -91,7 +91,7 @@ class TheoryEngine { /** * A bitmap of theories that are "active" for the current run. We - * mark a theory active when we firt see a term or type belonging to + * mark a theory active when we first see a term or type belonging to * it. This is important because we can optimize for single-theory * runs (no sharing), can reduce the cost of walking the DAG on * registration, etc. diff --git a/src/util/Makefile.am b/src/util/Makefile.am index e24184ad2..e8d33fbd4 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -57,6 +57,8 @@ libutil_la_SOURCES = \ ntuple.h \ recursion_breaker.h \ subrange_bound.h \ + predicate.h \ + predicate.cpp \ cardinality.h \ cardinality.cpp \ cache.h \ diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 211a1127b..8942c049b 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -190,7 +190,7 @@ string Configuration::getSubversionId() { return ss.str(); } -string Configuration::getCompiler() { +std::string Configuration::getCompiler() { stringstream ss; #ifdef __GNUC__ ss << "GCC"; @@ -205,4 +205,8 @@ string Configuration::getCompiler() { return ss.str(); } +std::string Configuration::getCompiledDateTime() { + return __DATE__ " " __TIME__; +} + }/* CVC4 namespace */ diff --git a/src/util/configuration.h b/src/util/configuration.h index 1a57af62b..1bd48999e 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -102,6 +102,7 @@ public: static std::string getSubversionId(); static std::string getCompiler(); + static std::string getCompiledDateTime(); };/* class Configuration */ diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h index fc0915f28..b93a6dd5e 100644 --- a/src/util/configuration_private.h +++ b/src/util/configuration_private.h @@ -121,7 +121,8 @@ This is CVC4 version " CVC4_RELEASE_STRING ) + \ ? ( ::std::string(" [") + ::CVC4::Configuration::getSubversionId() + "]" ) \ : ::std::string("") \ ) + "\n\ -compiled with " + ::CVC4::Configuration::getCompiler() + "\n\n\ +compiled with " + ::CVC4::Configuration::getCompiler() + "\n\ +on " + ::CVC4::Configuration::getCompiledDateTime() + "\n\n\ Copyright (C) 2009, 2010, 2011, 2012\n\ The ACSys Group\n\ Courant Institute of Mathematical Sciences\n\ diff --git a/src/util/datatype.i b/src/util/datatype.i index 056c15004..2b2a96030 100644 --- a/src/util/datatype.i +++ b/src/util/datatype.i @@ -11,6 +11,8 @@ %ignore to_array();// ocaml %ignore vector(size_type);// java/python %ignore resize(size_type);// java/python + %ignore set(int i, const CVC4::Datatype& x); + %ignore to_array(); }; %template(vectorDatatype) std::vector< CVC4::Datatype >; @@ -23,6 +25,8 @@ %ignore to_array();// ocaml %ignore vector(size_type);// java/python %ignore resize(size_type);// java/python + %ignore set(int i, const CVC4::Datatype::Constructor& x); + %ignore to_array(); }; %template(vectorDatatypeConstructor) std::vector< CVC4::DatatypeConstructor >; diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 161666df5..a02f5d2c1 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -268,14 +268,14 @@ public: long si = d_value.get_si(); // ensure there wasn't overflow AlwaysAssert(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, - "Overflow detected in Integer::getLong()"); + "Overflow when extracting long from multiprecision integer"); return si; } unsigned long getUnsignedLong() const { unsigned long ui = d_value.get_ui(); // ensure there wasn't overflow AlwaysAssert(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, - "Overflow detected in Integer::getUnsignedLong()"); + "Overflow when extracting unsigned long from multiprecision integer"); return ui; } diff --git a/src/util/options.cpp b/src/util/options.cpp index e33fbc263..d21df27ac 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -23,6 +23,7 @@ #include #include #include +#include #include @@ -274,10 +275,10 @@ Dump modes can be combined with multiple uses of --dump. Generally you want\n\ one from the assertions category (either asertions, learned, or clauses), and\n\ perhaps one or more stateful or non-stateful modes for checking correctness\n\ and completeness of decision procedure implementations. Stateful modes dump\n\ -the contextual assertions made by the core solver (all decisions and propagations\n\ -as assertions; that affects the validity of the resulting correctness and\n\ -completeness queries, so of course stateful and non-stateful modes cannot\n\ -be mixed in the same run.\n\ +the contextual assertions made by the core solver (all decisions and\n\ +propagations as assertions; that affects the validity of the resulting\n\ +correctness and completeness queries, so of course stateful and non-stateful\n\ +modes cannot be mixed in the same run.\n\ \n\ The --output-language option controls the language used for dumping, and\n\ this allows you to connect CVC4 to another solver implementation via a UNIX\n\ @@ -983,7 +984,12 @@ throw(OptionException) { break; case ':': - throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument"); + // This can be a long or short option, and the way to get at the name of it is different. + if(optopt == 0) { // was a long option + throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument"); + } else { // was a short option + throw OptionException(string("option `-") + char(optopt) + "' missing its required argument"); + } case '?': default: @@ -1004,7 +1010,13 @@ throw(OptionException) { } break; } - throw OptionException(string("can't understand option `") + argv[optind - 1] + "'"); + + // This can be a long or short option, and the way to get at the name of it is different. + if(optopt == 0) { // was a long option + throw OptionException(string("can't understand option `") + argv[optind - 1] + "'"); + } else { // was a short option + throw OptionException(string("can't understand option `-") + char(optopt) + "'"); + } } } diff --git a/src/util/output.h b/src/util/output.h index 8a90ef136..8afb4e05a 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -28,6 +28,7 @@ #include #include #include +#include namespace CVC4 { @@ -167,6 +168,20 @@ CVC4ostream& CVC4ostream::operator<<(T const& t) { return *this; } +/** + * Does nothing; designed for compilation of non-debug/non-trace + * builds. None of these should ever be called in such builds, but we + * offer this to the compiler so it doesn't complain. + */ +class CVC4_PUBLIC NullC { +public: + operator bool() { return false; } + operator CVC4ostream() { return CVC4ostream(); } + operator std::ostream&() { return null_os; } +};/* class NullC */ + +extern NullC nullCvc4Stream CVC4_PUBLIC; + /** The debug output class */ class CVC4_PUBLIC DebugC { std::set d_tags; @@ -208,6 +223,7 @@ public: /** The warning output class */ class CVC4_PUBLIC WarningC { + std::set< std::pair > d_alreadyWarned; std::ostream* d_os; public: @@ -221,6 +237,22 @@ public: std::ostream& getStream() { return *d_os; } bool isOn() const { return d_os != &null_os; } + + // This function supports the WarningOnce() macro, which allows you + // to easily indicate that a warning should be emitted, but only + // once for a given run of CVC4. + bool warnOnce(const char* file, size_t line) { + std::pair pr = std::make_pair(file, line); + if(d_alreadyWarned.find(pr) != d_alreadyWarned.end()) { + // signal caller not to warn again + return false; + } + + // okay warn this time, but don't do it again + d_alreadyWarned.insert(pr); + return true; + } + };/* class WarningC */ /** The message output class */ @@ -378,6 +410,7 @@ extern DumpC DumpChannel CVC4_PUBLIC; # define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel # define Warning ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel +# define WarningOnce ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel # define Message ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel # define Notice ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel # define Chat ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel @@ -405,6 +438,7 @@ inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; } inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; } # endif /* CVC4_DEBUG */ # define Warning (! ::CVC4::WarningChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel +# define WarningOnce (! ::CVC4::WarningChannel.isOn() || ! ::CVC4::WarningChannel.warnOnce(__FILE__,__LINE__)) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel # define Message (! ::CVC4::MessageChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel # define Notice (! ::CVC4::NoticeChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel # define Chat (! ::CVC4::ChatChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel @@ -532,20 +566,6 @@ public: #endif /* CVC4_TRACING */ -/** - * Does nothing; designed for compilation of non-debug/non-trace - * builds. None of these should ever be called in such builds, but we - * offer this to the compiler so it doesn't complain. - */ -class CVC4_PUBLIC NullC { -public: - operator bool() { return false; } - operator CVC4ostream() { return CVC4ostream(); } - operator std::ostream&() { return null_os; } -};/* class NullC */ - -extern NullC nullCvc4Stream CVC4_PUBLIC; - /** * Pushes an indentation level on construction, pop on destruction. * Useful for tracing recursive functions especially, but also can be diff --git a/src/util/predicate.cpp b/src/util/predicate.cpp new file mode 100644 index 000000000..1868f557d --- /dev/null +++ b/src/util/predicate.cpp @@ -0,0 +1,57 @@ +/********************* */ +/*! \file predicate.cpp + ** \verbatim + ** Original author: mdeters + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Representation of predicates for predicate subtyping + ** + ** Simple class to represent predicates for predicate subtyping. + ** Instances of this class are carried as the payload of + ** the CONSTANT-metakinded SUBTYPE_TYPE types. + **/ + +#include "expr/expr.h" +#include "util/predicate.h" +#include "util/Assert.h" + +using namespace std; + +namespace CVC4 { + +Predicate::Predicate(Expr e, Expr w) throw(IllegalArgumentException) : d_predicate(e), d_witness(w) { + CheckArgument(! e.isNull(), e, "Predicate cannot be null"); + CheckArgument(e.getType().isPredicate(), e, "Expression given is not predicate"); + CheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e, "Expression given is not predicate of a single argument"); +} + +Predicate::operator Expr() const { + return d_predicate; +} + +bool Predicate::operator==(const Predicate& p) const { + return d_predicate == p.d_predicate && d_witness == p.d_witness; +} + +std::ostream& +operator<<(std::ostream& out, const Predicate& p) { + out << p.d_predicate; + if(! p.d_witness.isNull()) { + out << " : " << p.d_witness; + } + return out; +} + +size_t PredicateHashStrategy::hash(const Predicate& p) { + ExprHashFunction h; + return h(p.d_witness) * 5039 + h(p.d_predicate); +} + +}/* CVC4 namespace */ diff --git a/src/util/predicate.h b/src/util/predicate.h new file mode 100644 index 000000000..94a685177 --- /dev/null +++ b/src/util/predicate.h @@ -0,0 +1,64 @@ +/********************* */ +/*! \file predicate.h + ** \verbatim + ** Original author: mdeters + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Representation of predicates for predicate subtyping + ** + ** Simple class to represent predicates for predicate subtyping. + ** Instances of this class are carried as the payload of + ** the CONSTANT-metakinded SUBTYPE_TYPE types. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__PREDICATE_H +#define __CVC4__PREDICATE_H + +#include "util/Assert.h" + +namespace CVC4 { + +class Predicate; + +std::ostream& operator<<(std::ostream& out, const Predicate& p) CVC4_PUBLIC; + +struct CVC4_PUBLIC PredicateHashStrategy { + static size_t hash(const Predicate& p); +};/* class PredicateHashStrategy */ + +}/* CVC4 namespace */ + +#include "expr/expr.h" + +namespace CVC4 { + +class CVC4_PUBLIC Predicate { + + Expr d_predicate; + Expr d_witness; + +public: + + Predicate(Expr e, Expr w = Expr()) throw(IllegalArgumentException); + + operator Expr() const; + + bool operator==(const Predicate& p) const; + + friend std::ostream& operator<<(std::ostream& out, const Predicate& p); + friend size_t PredicateHashStrategy::hash(const Predicate& p); + +};/* class Predicate */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__PREDICATE_H */ diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h index 0c84b214e..9d4d446bd 100644 --- a/src/util/subrange_bound.h +++ b/src/util/subrange_bound.h @@ -25,6 +25,8 @@ #include "util/integer.h" #include "util/Assert.h" +#include + namespace CVC4 { /** @@ -76,8 +78,132 @@ public: return !(*this == b); } + /** + * Is this SubrangeBound "less than" another? For two + * SubrangeBounds that "have bounds," this is defined as expected. + * For a finite SubrangeBound b1 and a SubrangeBounds b2 without a + * bound, b1 < b2 (but note also that b1 > b2). This strange + * behavior is due to the fact that a SubrangeBound without a bound + * is the representation for both +infinity and -infinity. + */ + bool operator<(const SubrangeBound& b) const throw() { + return (!hasBound() && b.hasBound()) || (hasBound() && !b.hasBound()) || + ( hasBound() && b.hasBound() && getBound() < b.getBound() ); + } + + /** + * Is this SubrangeBound "less than or equal to" another? For two + * SubrangeBounds that "have bounds," this is defined as expected. + * For a finite SubrangeBound b1 and a SubrangeBounds b2 without a + * bound, b1 < b2 (but note also that b1 > b2). This strange + * behavior is due to the fact that a SubrangeBound without a bound + * is the representation for both +infinity and -infinity. + */ + bool operator<=(const SubrangeBound& b) const throw() { + return !hasBound() || !b.hasBound() || + ( hasBound() && b.hasBound() && getBound() <= b.getBound() ); + } + + /** + * Is this SubrangeBound "greater than" another? For two + * SubrangeBounds that "have bounds," this is defined as expected. + * For a finite SubrangeBound b1 and a SubrangeBounds b2 without a + * bound, b1 > b2 (but note also that b1 < b2). This strange + * behavior is due to the fact that a SubrangeBound without a bound + * is the representation for both +infinity and -infinity. + */ + bool operator>(const SubrangeBound& b) const throw() { + return (!hasBound() && b.hasBound()) || (hasBound() && !b.hasBound()) || + ( hasBound() && b.hasBound() && getBound() < b.getBound() ); + } + + /** + * Is this SubrangeBound "greater than or equal to" another? For + * two SubrangeBounds that "have bounds," this is defined as + * expected. For a finite SubrangeBound b1 and a SubrangeBounds b2 + * without a bound, b1 > b2 (but note also that b1 < b2). This + * strange behavior is due to the fact that a SubrangeBound without + * a bound is the representation for both +infinity and -infinity. + */ + bool operator>=(const SubrangeBound& b) const throw() { + return !hasBound() || !b.hasBound() || + ( hasBound() && b.hasBound() && getBound() <= b.getBound() ); + } + };/* class SubrangeBound */ +class CVC4_PUBLIC SubrangeBounds { +public: + + SubrangeBound lower; + SubrangeBound upper; + + SubrangeBounds(const SubrangeBound& l, const SubrangeBound& u) : + lower(l), + upper(u) { + CheckArgument(!l.hasBound() || !u.hasBound() || + l.getBound() <= u.getBound(), + l, "Bad subrange bounds specified"); + } + + bool operator==(const SubrangeBounds& bounds) const { + return lower == bounds.lower && upper == bounds.upper; + } + + bool operator!=(const SubrangeBounds& bounds) const { + return !(*this == bounds); + } + + /** + * Is this pair of SubrangeBounds "less than" (contained inside) the + * given pair of SubrangeBounds? Think of this as a subtype + * relation, e.g., [0,2] < [0,3] + */ + bool operator<(const SubrangeBounds& bounds) const { + return (lower > bounds.lower && upper <= bounds.upper) || + (lower >= bounds.lower && upper < bounds.upper); + } + + /** + * Is this pair of SubrangeBounds "less than or equal" (contained + * inside) the given pair of SubrangeBounds? Think of this as a + * subtype relation, e.g., [0,2] < [0,3] + */ + bool operator<=(const SubrangeBounds& bounds) const { + return lower >= bounds.lower && upper <= bounds.upper; + } + + /** + * Is this pair of SubrangeBounds "greater than" (does it contain) + * the given pair of SubrangeBounds? Think of this as a supertype + * relation, e.g., [0,3] > [0,2] + */ + bool operator>(const SubrangeBounds& bounds) const { + return (lower < bounds.lower && upper >= bounds.upper) || + (lower <= bounds.lower && upper > bounds.upper); + } + + /** + * Is this pair of SubrangeBounds "greater than" (does it contain) + * the given pair of SubrangeBounds? Think of this as a supertype + * relation, e.g., [0,3] > [0,2] + */ + bool operator>=(const SubrangeBounds& bounds) const { + return lower <= bounds.lower && upper >= bounds.upper; + } + +};/* class SubrangeBounds */ + +struct CVC4_PUBLIC SubrangeBoundsHashStrategy { + static inline size_t hash(const SubrangeBounds& bounds) { + // We use Integer::hash() rather than Integer::getUnsignedLong() + // because the latter might overflow and throw an exception + size_t l = bounds.lower.hasBound() ? bounds.lower.getBound().hash() : std::numeric_limits::max(); + size_t u = bounds.upper.hasBound() ? bounds.upper.getBound().hash() : std::numeric_limits::max(); + return l + 0x9e3779b9 + (u << 6) + (u >> 2); + } +};/* struct SubrangeBoundsHashStrategy */ + inline std::ostream& operator<<(std::ostream& out, const SubrangeBound& bound) throw() CVC4_PUBLIC; @@ -92,6 +218,16 @@ operator<<(std::ostream& out, const SubrangeBound& bound) throw() { return out; } +inline std::ostream& +operator<<(std::ostream& out, const SubrangeBounds& bounds) throw() CVC4_PUBLIC; + +inline std::ostream& +operator<<(std::ostream& out, const SubrangeBounds& bounds) throw() { + out << bounds.lower << ".." << bounds.upper; + + return out; +} + }/* CVC4 namespace */ #endif /* __CVC4__SUBRANGE_BOUND_H */ diff --git a/test/Makefile.am b/test/Makefile.am index 4f7818ade..2bcb283d7 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -35,6 +35,7 @@ subdirs_to_check = \ regress/regress0/arith/integers \ regress/regress0/uf \ regress/regress0/uflra \ + regress/regress0/uflia \ regress/regress0/bv \ regress/regress0/bv/core \ regress/regress0/arrays \ @@ -43,6 +44,7 @@ subdirs_to_check = \ regress/regress0/push-pop \ regress/regress0/precedence \ regress/regress0/preprocess \ + regress/regress0/subtypes \ regress/regress1 \ regress/regress2 \ regress/regress3 diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 1c4071c00..016bf6e2a 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -41,7 +41,8 @@ SMT2_TESTS = \ ite4.smt2 \ simple-lra.smt2 \ simple-rdl.smt2 \ - simple-uf.smt2 + simple-uf.smt2 \ + simplification_bug4.smt2 # Regression tests for PL inputs CVC_TESTS = \ @@ -105,7 +106,8 @@ EXTRA_DIST = $(TESTS) \ bug216.smt2.expect \ bug288b.smt \ bug288c.smt \ - bug288.smt + bug288.smt \ + simplification_bug4.smt2.expect if CVC4_BUILD_PROFILE_COMPETITION else diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index c4a4e2fdd..581897535 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -12,6 +12,10 @@ MAKEFLAGS = -k # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ + tuple.cvc \ + rec1.cvc \ + rec2.cvc \ + rec5.cvc \ datatype.cvc \ datatype0.cvc \ datatype1.cvc \ @@ -45,7 +49,8 @@ endif # and make sure to distribute it EXTRA_DIST += \ - error.cvc + error.cvc \ + rec4.cvc # synonyms for "check" .PHONY: regress regress0 test diff --git a/test/regress/regress0/datatypes/rec1.cvc b/test/regress/regress0/datatypes/rec1.cvc new file mode 100644 index 000000000..25e14eac0 --- /dev/null +++ b/test/regress/regress0/datatypes/rec1.cvc @@ -0,0 +1,8 @@ +% EXPECT: valid +% EXIT: 20 +c : BOOLEAN; +a17 : BOOLEAN = ((# _a := 2, _b := 2 #) = ( + IF c THEN (# _a := 3, _b := 2 #) + ELSE (# _a := 1, _b := 2 #) + ENDIF WITH ._a := 2)); +QUERY a17; diff --git a/test/regress/regress0/datatypes/rec2.cvc b/test/regress/regress0/datatypes/rec2.cvc new file mode 100644 index 000000000..80aecfe25 --- /dev/null +++ b/test/regress/regress0/datatypes/rec2.cvc @@ -0,0 +1,12 @@ +% EXPECT: valid +% EXIT: 20 +c : BOOLEAN; +a16 : [# _a : REAL, _b : REAL #] = ( + IF c THEN (# _a := 3, _b := 2 #) + ELSE (# _a := 1, _b := 5 #) + ENDIF WITH ._a := 2); +a21 : BOOLEAN = + IF c THEN ((# _a := 2, _b := 2 #) = a16) + ELSE ((# _a := 2, _b := 5 #) = a16) + ENDIF; +QUERY a21; diff --git a/test/regress/regress0/datatypes/rec4.cvc b/test/regress/regress0/datatypes/rec4.cvc new file mode 100644 index 000000000..c474502d5 --- /dev/null +++ b/test/regress/regress0/datatypes/rec4.cvc @@ -0,0 +1,11 @@ +% EXPECT: valid +% EXIT: 20 +a : BOOLEAN; +a49 : BOOLEAN = ( + IF a THEN (# _a := 1 #) + ELSE (# _a := 2 #) + ENDIF = (# _a := + IF a THEN 1 + ELSE 2 + ENDIF #)); +QUERY a49; diff --git a/test/regress/regress0/datatypes/rec5.cvc b/test/regress/regress0/datatypes/rec5.cvc new file mode 100644 index 000000000..d52174b8e --- /dev/null +++ b/test/regress/regress0/datatypes/rec5.cvc @@ -0,0 +1,205 @@ +% EXPECT: invalid +% EXIT: 10 +bit__ty: TYPE = [0..1]; +bc1553__lru_name: TYPE = [0..11]; +bus__inputs__type: TYPE; +bus__word_index: TYPE = INT; +cartesian__position: TYPE = [# x: INT, y: INT, z: INT #]; +ibit__phase: TYPE = [0..6]; +measuretypes__meter: TYPE = INT; +bc1553__asi: [0..11]; +bc1553__barometer: [0..11]; +bc1553__compass: [0..11]; +bc1553__destruct: [0..11]; +bc1553__fins: [0..11]; +bc1553__fuel: [0..11]; +bc1553__fuze: [0..11]; +bc1553__infrared: [0..11]; +bc1553__ins: [0..11]; +bc1553__lru_name__base__first: [0..11]; +bc1553__lru_name__base__last: [0..11]; +bc1553__lru_name__first: [0..11]; +bc1553__lru_name__last: [0..11]; +bc1553__lru_name__size: INT; +bc1553__motor: [0..11]; +bc1553__radar: [0..11]; +bc1553__warhead: [0..11]; +bus__all_msg_index__base__first: INT; +bus__all_msg_index__base__last: INT; +bus__all_msg_index__first: INT; +bus__all_msg_index__last: INT; +bus__all_msg_index__size: INT; +bus__lru_subaddress_index__base__first: INT; +bus__lru_subaddress_index__base__last: INT; +bus__lru_subaddress_index__first: INT; +bus__lru_subaddress_index__last: INT; +bus__lru_subaddress_index__size: INT; +bus__word__base__first: INT; +bus__word__base__last: INT; +bus__word__first: INT; +bus__word__last: INT; +bus__word__size: INT; +bus__word_index__base__first: INT; +bus__word_index__base__last: INT; +bus__word_index__first: INT; +bus__word_index__last: INT; +bus__word_index__size: INT; +bus_id: [0..11]; +ibit__fail: [0..6]; +ibit__in_progress: [0..6]; +ibit__off: [0..6]; +ibit__pass: [0..6]; +ibit__phase__base__first: [0..6]; +ibit__phase__base__last: [0..6]; +ibit__phase__first: [0..6]; +ibit__phase__last: [0..6]; +ibit__phase__size: INT; +ibit__request_start: [0..6]; +ibit__request_stop: [0..6]; +ibit__timeout: [0..6]; +integer__base__first: INT; +integer__base__last: INT; +integer__first: INT; +integer__last: INT; +integer__size: INT; +measuretypes__meter__base__first: INT; +measuretypes__meter__base__last: INT; +measuretypes__meter__first: INT; +measuretypes__meter__last: INT; +measuretypes__meter__size: INT; +systemtypes__unsigned16__base__first: INT; +systemtypes__unsigned16__base__last: INT; +systemtypes__unsigned16__first: INT; +systemtypes__unsigned16__last: INT; +systemtypes__unsigned16__size: INT; +bus__inputs: bus__inputs__type; +bus__inputs__tilde: bus__inputs__type; +ibit_request: [0..6]; +ibit_request__5: [0..6]; +ibit_request__5__tilde: [0..6]; +ibit_request__tilde: [0..6]; +last_position: [# x: INT, y: INT, z: INT #]; +last_position__1: [# x: INT, y: INT, z: INT #]; +last_position__1__tilde: [# x: INT, y: INT, z: INT #]; +last_position__2: [# x: INT, y: INT, z: INT #]; +last_position__2__tilde: [# x: INT, y: INT, z: INT #]; +last_position__3: [# x: INT, y: INT, z: INT #]; +last_position__3__tilde: [# x: INT, y: INT, z: INT #]; +last_position__tilde: [# x: INT, y: INT, z: INT #]; +word: INT; +word__4: INT; +word__4__tilde: INT; +word__tilde: INT; +bc1553__is_fresh: ([0..11], INT, bus__inputs__type) -> BOOLEAN; +bc1553__is_valid: ([0..11], INT, bus__inputs__type) -> BOOLEAN; +bc1553__lru_name__LE: ([0..11], [0..11]) -> BOOLEAN; +bc1553__lru_name__pos: [0..11] -> INT; +bc1553__lru_name__pred: [0..11] -> [0..11]; +bc1553__lru_name__succ: [0..11] -> [0..11]; +bc1553__lru_name__val: INT -> [0..11]; +character__pos: INT -> INT; +character__val: INT -> INT; +ibit__phase__LE: ([0..6], [0..6]) -> BOOLEAN; +ibit__phase__pos: [0..6] -> INT; +ibit__phase__pred: [0..6] -> [0..6]; +ibit__phase__succ: [0..6] -> [0..6]; +ibit__phase__val: INT -> [0..6]; +integer__pred: INT -> INT; +integer__succ: INT -> INT; +round__: REAL -> INT; +int__div: (INT, INT) -> INT; +int__mod: (INT, INT) -> INT; +ASSERT (bus_id = bc1553__ins); +ASSERT (0 <= integer__size); +ASSERT (integer__first = -(2147483647)); +ASSERT (integer__last = 2147483647); +ASSERT (integer__base__first = -(2147483647)); +ASSERT (integer__base__last = 2147483647); +ASSERT (0 <= systemtypes__unsigned16__size); +ASSERT (systemtypes__unsigned16__first = 0); +ASSERT (systemtypes__unsigned16__last = 65535); +ASSERT (systemtypes__unsigned16__base__first = -(2147483647)); +ASSERT (systemtypes__unsigned16__base__last = 2147483647); +ASSERT (0 <= measuretypes__meter__size); +ASSERT (measuretypes__meter__first = -(200000)); +ASSERT (measuretypes__meter__last = 200000); +ASSERT (measuretypes__meter__base__first = -(2147483647)); +ASSERT (measuretypes__meter__base__last = 2147483647); +ASSERT (0 <= bus__word_index__size); +ASSERT (bus__word_index__first = 1); +ASSERT (bus__word_index__last = 31); +ASSERT (bus__word_index__base__first <= bus__word_index__base__last); +ASSERT (bus__word_index__base__first <= bus__word_index__first); +ASSERT (bus__word_index__last <= bus__word_index__base__last); +ASSERT (0 <= bus__word__size); +ASSERT (bus__word__first = 0); +ASSERT (bus__word__last = 65535); +ASSERT (bus__word__base__first = -(2147483647)); +ASSERT (bus__word__base__last = 2147483647); +ASSERT (0 <= bus__all_msg_index__size); +ASSERT (bus__all_msg_index__first = 0); +ASSERT (bus__all_msg_index__last = 63); +ASSERT (bus__all_msg_index__base__first = -(32768)); +ASSERT (bus__all_msg_index__base__last = 32767); +ASSERT (0 <= bus__lru_subaddress_index__size); +ASSERT (bus__lru_subaddress_index__first = 1); +ASSERT (bus__lru_subaddress_index__last = 8); +ASSERT (bus__lru_subaddress_index__base__first = -(32768)); +ASSERT (bus__lru_subaddress_index__base__last = 32767); +ASSERT (0 <= bc1553__lru_name__size); +ASSERT (bc1553__lru_name__first = bc1553__barometer); +ASSERT (bc1553__lru_name__last = bc1553__warhead); +ASSERT (bc1553__lru_name__base__first = bc1553__barometer); +ASSERT (bc1553__lru_name__base__last = bc1553__warhead); +ASSERT (0 <= ibit__phase__size); +ASSERT (ibit__phase__first = ibit__off); +ASSERT (ibit__phase__last = ibit__timeout); +ASSERT (ibit__phase__base__first = ibit__off); +ASSERT (ibit__phase__base__last = ibit__timeout); +ASSERT (bc1553__barometer = 0); +ASSERT (bc1553__asi = 1); +ASSERT (bc1553__ins = 2); +ASSERT (bc1553__compass = 3); +ASSERT (bc1553__fuel = 4); +ASSERT (bc1553__fuze = 5); +ASSERT (bc1553__radar = 6); +ASSERT (bc1553__infrared = 7); +ASSERT (bc1553__fins = 8); +ASSERT (bc1553__motor = 9); +ASSERT (bc1553__destruct = 10); +ASSERT (bc1553__warhead = 11); +ASSERT (ibit__off = 0); +ASSERT (ibit__request_start = 1); +ASSERT (ibit__in_progress = 2); +ASSERT (ibit__request_stop = 3); +ASSERT (ibit__pass = 4); +ASSERT (ibit__fail = 5); +ASSERT (ibit__timeout = 6); +ASSERT TRUE; +ASSERT (measuretypes__meter__first <= (last_position).z); +ASSERT ((last_position).z <= measuretypes__meter__last); +ASSERT (measuretypes__meter__first <= (last_position).y); +ASSERT ((last_position).y <= measuretypes__meter__last); +ASSERT (measuretypes__meter__first <= (last_position).x); +ASSERT ((last_position).x <= measuretypes__meter__last); +ASSERT TRUE; +ASSERT (ibit__phase__first <= ibit_request); +ASSERT (ibit_request <= ibit__phase__last); +ASSERT (bus__lru_subaddress_index__first <= 1); +ASSERT (1 <= bus__lru_subaddress_index__last); +ASSERT (bc1553__lru_name__first <= bus_id); +ASSERT (bus_id <= bc1553__lru_name__last); +ASSERT TRUE; +ASSERT (bc1553__is_valid(bus_id, 1, bus__inputs) => ((bus__lru_subaddress_index__first <= 1) AND (1 <= bus__lru_subaddress_index__last))); +ASSERT (bc1553__is_valid(bus_id, 1, bus__inputs) => ((bc1553__lru_name__first <= bus_id) AND (bus_id <= bc1553__lru_name__last))); +ASSERT (bc1553__is_valid(bus_id, 1, bus__inputs) => TRUE); +ASSERT bc1553__is_valid(bus_id, 1, bus__inputs); +ASSERT bc1553__is_fresh(bus_id, 1, bus__inputs); +ASSERT (bus__word_index__first <= 2); +ASSERT (2 <= bus__word_index__last); +ASSERT (bus__word_index__first <= 1); +ASSERT (1 <= bus__word_index__last); +ASSERT (measuretypes__meter__first <= (last_position__1).x); +ASSERT ((last_position__1).x <= measuretypes__meter__last); +ASSERT ((last_position__1).y = (last_position).y); +QUERY (last_position = last_position__1); diff --git a/test/regress/regress0/datatypes/tuple.cvc b/test/regress/regress0/datatypes/tuple.cvc new file mode 100644 index 000000000..1def5d14e --- /dev/null +++ b/test/regress/regress0/datatypes/tuple.cvc @@ -0,0 +1,11 @@ +% EXPECT: valid +% EXIT: 20 +x: [REAL,INT,REAL] = ( 4/5, 9, 11/9 ); +first_elem: REAL = x.0; +third_elem: REAL = x.2; + +Tup: TYPE = [REAL,INT,REAL]; +y: Tup = ( 4/5, 9, 11/9 ); +y1: Tup = y WITH .1 := 3; + +QUERY x=y AND first_elem = y1.0 AND third_elem = y1.2 AND y1.1 = 3; diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index aedf03470..f43a4d183 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -20,6 +20,9 @@ CVC_TESTS = \ units.cvc \ incremental-subst-bug.cvc +SMT2_TESTS = \ + tiny_bug.smt2 + TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/push-pop/tiny_bug.smt2 b/test/regress/regress0/push-pop/tiny_bug.smt2 new file mode 100644 index 000000000..83ccca49e --- /dev/null +++ b/test/regress/regress0/push-pop/tiny_bug.smt2 @@ -0,0 +1,28 @@ +; COMMAND-LINE: --incremental --simplification=none +; EXPECT: sat +; EXPECT: unsat +; EXIT: 20 +(set-logic QF_UFLIA) +(declare-fun base () Int) +(declare-fun n () Int) + +(declare-fun g (Int) Bool) +(declare-fun f (Int) Bool) + +(push 1) +(assert (<= 0 n)) +(assert (f n)) +(assert (= (f n) (or (= (- n base) 1) (g n)))) +(check-sat) +(pop 1) + +(push 1) +(assert (<= 0 n)) + +(assert (or (= (- n base) 1) (g n))) +(assert (not (g n))) +(assert (= base (- 2))) + +(check-sat) +(pop 1) + diff --git a/test/regress/regress0/simplification_bug4.smt2 b/test/regress/regress0/simplification_bug4.smt2 new file mode 100644 index 000000000..0d62d6921 --- /dev/null +++ b/test/regress/regress0/simplification_bug4.smt2 @@ -0,0 +1,295 @@ +(set-logic QF_LIA) +;; Simplified benchmark, derived from NuSMV output durationThm_1.bmc_k100.smt2 +;; +;; Original version generated by Alberto Griggio +;; on Fri Feb 4 15:56:12 2011 +(declare-fun sb_0__AT0 () Bool) +(declare-fun si_0__AT0 () Int) +(declare-fun si_1__AT0 () Int) +(declare-fun sb_1__AT0 () Bool) +(declare-fun si_2__AT0 () Int) +(declare-fun si_3__AT0 () Int) +(declare-fun sb_2__AT0 () Bool) +(declare-fun si_4__AT0 () Int) +(declare-fun si_5__AT0 () Int) +(declare-fun sb_3__AT0 () Bool) +(declare-fun sb_4__AT0 () Bool) +(declare-fun sb_5__AT0 () Bool) +(declare-fun si_6__AT0 () Int) +(declare-fun si_7__AT0 () Int) +(declare-fun si_8__AT0 () Int) +(declare-fun si_9__AT0 () Int) +(declare-fun si_10__AT0 () Int) +(declare-fun si_11__AT0 () Int) +(declare-fun sb_6__AT0 () Bool) +(declare-fun sb_7__AT0 () Bool) +(declare-fun si_12__AT0 () Int) +(declare-fun si_13__AT0 () Int) +(declare-fun si_14__AT0 () Int) +(assert (let ((.def_61 (= si_2__AT0 si_4__AT0))) +(let ((.def_60 (= si_3__AT0 si_5__AT0))) +(let ((.def_62 (and .def_60 .def_61))) +(let ((.def_63 (and sb_2__AT0 .def_62))) +(let ((.def_59 (= si_8__AT0 0))) +(let ((.def_64 (and .def_59 .def_63))) +(let ((.def_58 (= si_11__AT0 0))) +(let ((.def_65 (and .def_58 .def_64))) +(let ((.def_53 (<= 1 si_0__AT0))) +(let ((.def_52 (<= 1 si_1__AT0))) +(let ((.def_54 (and .def_52 .def_53))) +(let ((.def_48 (<= si_0__AT0 si_6__AT0))) +(let ((.def_49 (not .def_48))) +(let ((.def_50 (or sb_4__AT0 .def_49))) +(let ((.def_55 (and .def_50 .def_54))) +(let ((.def_45 (<= si_1__AT0 si_9__AT0))) +(let ((.def_46 (not .def_45))) +(let ((.def_47 (or sb_5__AT0 .def_46))) +(let ((.def_56 (and .def_47 .def_55))) +(let ((.def_57 (= sb_7__AT0 .def_56))) +(let ((.def_66 (and .def_57 .def_65))) +(let ((.def_44 (= si_14__AT0 0))) +(let ((.def_67 (and .def_44 .def_66))) +(let ((.def_33 (not sb_1__AT0))) +(let ((.def_34 (or sb_2__AT0 .def_33))) +(let ((.def_35 (= sb_0__AT0 .def_34))) +(let ((.def_32 (= si_0__AT0 si_2__AT0))) +(let ((.def_36 (and .def_32 .def_35))) +(let ((.def_31 (= si_1__AT0 si_3__AT0))) +(let ((.def_37 (and .def_31 .def_36))) +(let ((.def_30 (= sb_1__AT0 sb_6__AT0))) +(let ((.def_38 (and .def_30 .def_37))) +(let ((.def_29 (= si_6__AT0 si_8__AT0))) +(let ((.def_39 (and .def_29 .def_38))) +(let ((.def_28 (= si_9__AT0 si_11__AT0))) +(let ((.def_40 (and .def_28 .def_39))) +(let ((.def_27 (= sb_6__AT0 sb_7__AT0))) +(let ((.def_41 (and .def_27 .def_40))) +(let ((.def_26 (= si_12__AT0 si_14__AT0))) +(let ((.def_42 (and .def_26 .def_41))) +(let ((.def_68 (and .def_42 .def_67))) +.def_68 +)))))))))))))))))))))))))))))))))))))))))) + +; (push 1) +; (assert (let ((.def_69 (not sb_0__AT0))) +; .def_69 +; )) +; (check-sat) +; (pop 1) + +(declare-fun sb_0__AT1 () Bool) +(declare-fun si_0__AT1 () Int) +(declare-fun si_1__AT1 () Int) +(declare-fun sb_1__AT1 () Bool) +(declare-fun si_2__AT1 () Int) +(declare-fun si_3__AT1 () Int) +(declare-fun sb_2__AT1 () Bool) +(declare-fun si_4__AT1 () Int) +(declare-fun si_5__AT1 () Int) +(declare-fun sb_3__AT1 () Bool) +(declare-fun sb_4__AT1 () Bool) +(declare-fun sb_5__AT1 () Bool) +(declare-fun si_6__AT1 () Int) +(declare-fun si_7__AT1 () Int) +(declare-fun si_8__AT1 () Int) +(declare-fun si_9__AT1 () Int) +(declare-fun si_10__AT1 () Int) +(declare-fun si_11__AT1 () Int) +(declare-fun sb_6__AT1 () Bool) +(declare-fun sb_7__AT1 () Bool) +(declare-fun si_12__AT1 () Int) +(declare-fun si_13__AT1 () Int) +(declare-fun si_14__AT1 () Int) +(assert (let ((.def_163 (= si_0__AT0 si_2__AT1))) +(let ((.def_162 (= si_1__AT0 si_3__AT1))) +(let ((.def_164 (and .def_162 .def_163))) +(let ((.def_155 (* (- 1) si_12__AT1))) +(let ((.def_156 (+ si_1__AT1 .def_155))) +(let ((.def_157 (+ si_0__AT1 .def_156))) +(let ((.def_158 (<= .def_157 0))) +(let ((.def_159 (not .def_158))) +(let ((.def_160 (or sb_5__AT1 .def_159))) +(let ((.def_161 (= sb_2__AT1 .def_160))) +(let ((.def_165 (and .def_161 .def_164))) +(let ((.def_147 (* (- 1) si_7__AT1))) +(let ((.def_148 (+ si_6__AT0 .def_147))) +(let ((.def_149 (= .def_148 (- 1)))) +(let ((.def_142 (not sb_3__AT0))) +(let ((.def_150 (or .def_142 .def_149))) +(let ((.def_144 (= si_7__AT1 0))) +(let ((.def_145 (or sb_3__AT0 .def_144))) +(let ((.def_151 (and .def_145 .def_150))) +(let ((.def_139 (* (- 1) si_13__AT1))) +(let ((.def_140 (+ si_12__AT0 .def_139))) +(let ((.def_141 (= .def_140 (- 1)))) +(let ((.def_143 (or .def_141 .def_142))) +(let ((.def_152 (and .def_143 .def_151))) +(let ((.def_136 (= si_13__AT1 0))) +(let ((.def_137 (or sb_3__AT0 .def_136))) +(let ((.def_153 (and .def_137 .def_152))) +(let ((.def_166 (and .def_153 .def_165))) +(let ((.def_133 (not sb_4__AT0))) +(let ((.def_130 (* (- 1) si_10__AT1))) +(let ((.def_131 (+ si_9__AT0 .def_130))) +(let ((.def_132 (= .def_131 (- 1)))) +(let ((.def_134 (or .def_132 .def_133))) +(let ((.def_126 (= si_10__AT1 0))) +(let ((.def_127 (or sb_4__AT0 .def_126))) +(let ((.def_135 (and .def_127 .def_134))) +(let ((.def_167 (and .def_135 .def_166))) +(let ((.def_125 (= si_7__AT1 si_8__AT1))) +(let ((.def_168 (and .def_125 .def_167))) +(let ((.def_124 (= si_10__AT1 si_11__AT1))) +(let ((.def_169 (and .def_124 .def_168))) +(let ((.def_118 (<= 1 si_0__AT1))) +(let ((.def_117 (<= 1 si_1__AT1))) +(let ((.def_119 (and .def_117 .def_118))) +(let ((.def_114 (<= si_0__AT1 si_6__AT1))) +(let ((.def_115 (not .def_114))) +(let ((.def_116 (or sb_4__AT1 .def_115))) +(let ((.def_120 (and .def_116 .def_119))) +(let ((.def_111 (<= si_1__AT1 si_9__AT1))) +(let ((.def_112 (not .def_111))) +(let ((.def_113 (or sb_5__AT1 .def_112))) +(let ((.def_121 (and .def_113 .def_120))) +(let ((.def_122 (and sb_6__AT0 .def_121))) +(let ((.def_123 (= sb_7__AT1 .def_122))) +(let ((.def_170 (and .def_123 .def_169))) +(let ((.def_110 (= si_13__AT1 si_14__AT1))) +(let ((.def_171 (and .def_110 .def_170))) +(let ((.def_100 (not sb_1__AT1))) +(let ((.def_101 (or sb_2__AT1 .def_100))) +(let ((.def_102 (= sb_0__AT1 .def_101))) +(let ((.def_99 (= si_0__AT1 si_2__AT1))) +(let ((.def_103 (and .def_99 .def_102))) +(let ((.def_98 (= si_1__AT1 si_3__AT1))) +(let ((.def_104 (and .def_98 .def_103))) +(let ((.def_97 (= sb_1__AT1 sb_6__AT1))) +(let ((.def_105 (and .def_97 .def_104))) +(let ((.def_96 (= si_6__AT1 si_8__AT1))) +(let ((.def_106 (and .def_96 .def_105))) +(let ((.def_95 (= si_9__AT1 si_11__AT1))) +(let ((.def_107 (and .def_95 .def_106))) +(let ((.def_94 (= sb_6__AT1 sb_7__AT1))) +(let ((.def_108 (and .def_94 .def_107))) +(let ((.def_93 (= si_12__AT1 si_14__AT1))) +(let ((.def_109 (and .def_93 .def_108))) +(let ((.def_172 (and .def_109 .def_171))) +(let ((.def_173 (and sb_0__AT0 .def_172))) +.def_173 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + +; (push 1) +; (assert (let ((.def_174 (not sb_0__AT1))) +; .def_174 +; )) +; (check-sat) +; (pop 1) + +(declare-fun sb_0__AT2 () Bool) +(declare-fun si_0__AT2 () Int) +(declare-fun si_1__AT2 () Int) +(declare-fun sb_1__AT2 () Bool) +(declare-fun si_2__AT2 () Int) +(declare-fun si_3__AT2 () Int) +(declare-fun sb_2__AT2 () Bool) +(declare-fun si_4__AT2 () Int) +(declare-fun si_5__AT2 () Int) +(declare-fun sb_3__AT2 () Bool) +(declare-fun sb_4__AT2 () Bool) +(declare-fun sb_5__AT2 () Bool) +(declare-fun si_6__AT2 () Int) +(declare-fun si_7__AT2 () Int) +(declare-fun si_8__AT2 () Int) +(declare-fun si_9__AT2 () Int) +(declare-fun si_10__AT2 () Int) +(declare-fun si_11__AT2 () Int) +(declare-fun sb_6__AT2 () Bool) +(declare-fun sb_7__AT2 () Bool) +(declare-fun si_12__AT2 () Int) +(declare-fun si_13__AT2 () Int) +(declare-fun si_14__AT2 () Int) +(assert (let ((.def_267 (= si_0__AT1 si_2__AT2))) +(let ((.def_266 (= si_1__AT1 si_3__AT2))) +(let ((.def_268 (and .def_266 .def_267))) +(let ((.def_259 (* (- 1) si_12__AT2))) +(let ((.def_260 (+ si_1__AT2 .def_259))) +(let ((.def_261 (+ si_0__AT2 .def_260))) +(let ((.def_262 (<= .def_261 0))) +(let ((.def_263 (not .def_262))) +(let ((.def_264 (or sb_5__AT2 .def_263))) +(let ((.def_265 (= sb_2__AT2 .def_264))) +(let ((.def_269 (and .def_265 .def_268))) +(let ((.def_251 (* (- 1) si_7__AT2))) +(let ((.def_252 (+ si_6__AT1 .def_251))) +(let ((.def_253 (= .def_252 (- 1)))) +(let ((.def_246 (not sb_3__AT1))) +(let ((.def_254 (or .def_246 .def_253))) +(let ((.def_248 (= si_7__AT2 0))) +(let ((.def_249 (or sb_3__AT1 .def_248))) +(let ((.def_255 (and .def_249 .def_254))) +(let ((.def_243 (* (- 1) si_13__AT2))) +(let ((.def_244 (+ si_12__AT1 .def_243))) +(let ((.def_245 (= .def_244 (- 1)))) +(let ((.def_247 (or .def_245 .def_246))) +(let ((.def_256 (and .def_247 .def_255))) +(let ((.def_240 (= si_13__AT2 0))) +(let ((.def_241 (or sb_3__AT1 .def_240))) +(let ((.def_257 (and .def_241 .def_256))) +(let ((.def_270 (and .def_257 .def_269))) +(let ((.def_237 (not sb_4__AT1))) +(let ((.def_234 (* (- 1) si_10__AT2))) +(let ((.def_235 (+ si_9__AT1 .def_234))) +(let ((.def_236 (= .def_235 (- 1)))) +(let ((.def_238 (or .def_236 .def_237))) +(let ((.def_231 (= si_10__AT2 0))) +(let ((.def_232 (or sb_4__AT1 .def_231))) +(let ((.def_239 (and .def_232 .def_238))) +(let ((.def_271 (and .def_239 .def_270))) +(let ((.def_230 (= si_7__AT2 si_8__AT2))) +(let ((.def_272 (and .def_230 .def_271))) +(let ((.def_229 (= si_10__AT2 si_11__AT2))) +(let ((.def_273 (and .def_229 .def_272))) +(let ((.def_223 (<= 1 si_0__AT2))) +(let ((.def_222 (<= 1 si_1__AT2))) +(let ((.def_224 (and .def_222 .def_223))) +(let ((.def_219 (<= si_0__AT2 si_6__AT2))) +(let ((.def_220 (not .def_219))) +(let ((.def_221 (or sb_4__AT2 .def_220))) +(let ((.def_225 (and .def_221 .def_224))) +(let ((.def_216 (<= si_1__AT2 si_9__AT2))) +(let ((.def_217 (not .def_216))) +(let ((.def_218 (or sb_5__AT2 .def_217))) +(let ((.def_226 (and .def_218 .def_225))) +(let ((.def_227 (and sb_6__AT1 .def_226))) +(let ((.def_228 (= sb_7__AT2 .def_227))) +(let ((.def_274 (and .def_228 .def_273))) +(let ((.def_215 (= si_13__AT2 si_14__AT2))) +(let ((.def_275 (and .def_215 .def_274))) +(let ((.def_205 (not sb_1__AT2))) +(let ((.def_206 (or sb_2__AT2 .def_205))) +(let ((.def_207 (= sb_0__AT2 .def_206))) +(let ((.def_204 (= si_0__AT2 si_2__AT2))) +(let ((.def_208 (and .def_204 .def_207))) +(let ((.def_203 (= si_1__AT2 si_3__AT2))) +(let ((.def_209 (and .def_203 .def_208))) +(let ((.def_202 (= sb_1__AT2 sb_6__AT2))) +(let ((.def_210 (and .def_202 .def_209))) +(let ((.def_201 (= si_6__AT2 si_8__AT2))) +(let ((.def_211 (and .def_201 .def_210))) +(let ((.def_200 (= si_9__AT2 si_11__AT2))) +(let ((.def_212 (and .def_200 .def_211))) +(let ((.def_199 (= sb_6__AT2 sb_7__AT2))) +(let ((.def_213 (and .def_199 .def_212))) +(let ((.def_198 (= si_12__AT2 si_14__AT2))) +(let ((.def_214 (and .def_198 .def_213))) +(let ((.def_276 (and .def_214 .def_275))) +(let ((.def_277 (and sb_0__AT1 .def_276))) +.def_277 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + +(push 1) +(assert (not sb_0__AT2)) +(check-sat) +(pop 1) + diff --git a/test/regress/regress0/simplification_bug4.smt2.expect b/test/regress/regress0/simplification_bug4.smt2.expect new file mode 100644 index 000000000..ef44f9b74 --- /dev/null +++ b/test/regress/regress0/simplification_bug4.smt2.expect @@ -0,0 +1,3 @@ +% COMMAND-LINE: --incremental +% EXPECT: unsat +% EXIT: 20 diff --git a/test/regress/run_regression b/test/regress/run_regression index 6c06175d2..75d81b938 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -102,12 +102,12 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then if [ -z "$expected_exit_status" ]; then error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" fi - elif grep -q '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then - expected_proof=`grep -q '^% PROOF' "$benchmark" && echo yes` - expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'` - expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` - expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'` - command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'` + elif grep -q '^\(%\|;\) \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then + expected_proof=`grep -q '^[%;] PROOF' "$benchmark" && echo yes` + expected_output=`grep '^[%;] EXPECT: ' "$benchmark" | sed 's,^[%;] EXPECT: ,,'` + expected_error=`grep '^[%;] EXPECT-ERROR: ' "$benchmark" | sed 's,^[%;] EXPECT-ERROR: ,,'` + expected_exit_status=`grep -m 1 '^[%;] EXIT: ' "$benchmark" | perl -pe 's,^[%;] EXIT: ,,;s,\r,,'` + command_line=`grep '^[%;] COMMAND-LINE: ' "$benchmark" | sed 's,^[%;] COMMAND-LINE: ,,'` # old mktemp from coreutils 7.x is broken, can't do XXXX in the middle # this frustrates our auto-language-detection gettemp tmpbenchmark cvc4_benchmark.smt2.$$.XXXXXXXXXX diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index 99e8b087c..e9cba5f9c 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -100,7 +100,11 @@ public: return SatValUnknown; } -}; + bool properExplanation(SatLiteral lit, SatLiteral expl) const { + return true; + } + +};/* class FakeSatSolver */ class CnfStreamBlack : public CxxTest::TestSuite { /** The SAT solver proxy */