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!
#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"
}
bool Type::isSubtype() const {
- return false;
+ return isPredicateSubtype();
}
Cardinality Type::card() const {
}
Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) {
- Unimplemented("Subranges not supported by CVC4 yet (sorry!)");
+ bool noLowerBound = l.getType().isString() && l.getConst<string>() == "_NEGINF";
+ bool noUpperBound = r.getType().isString() && r.getConst<string>() == "_POSINF";
+ CheckArgument(noLowerBound || l.getKind() == CVC4::kind::CONST_INTEGER, l);
+ CheckArgument(noUpperBound || r.getKind() == CVC4::kind::CONST_INTEGER, r);
+ CVC4::SubrangeBound bl = noLowerBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(l.getConst<Integer>());
+ CVC4::SubrangeBound br = noUpperBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(r.getConst<Integer>());
+ return d_em->mkSubrangeType(CVC4::SubrangeBounds(bl, br));
}
Type ValidityChecker::subtypeType(const Expr& pred, const Expr& witness) {
- Unimplemented("Predicate subtyping not supported by CVC4 yet (sorry!)");
+ if(witness.isNull()) {
+ return d_em->mkPredicateSubtype(pred);
+ } else {
+ return d_em->mkPredicateSubtype(pred, witness);
+ }
}
Type ValidityChecker::tupleType(const Type& type0, const Type& type1) {
}
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!)");
}
}
Expr ValidityChecker::idExpr(const std::string& name) {
- Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+ // represent as a string expr, CVC4 doesn't have id exprs
+ return d_em->mkConst(name);
}
Expr ValidityChecker::listExpr(const std::vector<Expr>& kids) {
- Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+ // list exprs aren't supported by CVC4; make a tuple if two or more
+ CheckArgument(kids.size() > 0, kids);
+ return (kids.size() == 1) ? kids[0] : Expr(d_em->mkExpr(CVC4::kind::TUPLE, vector<CVC4::Expr>(kids.begin(), kids.end())));
}
Expr ValidityChecker::listExpr(const Expr& e1) {
- Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+ // list exprs aren't supported by CVC4; just return e1
+ return e1;
}
Expr ValidityChecker::listExpr(const Expr& e1, const Expr& e2) {
- Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+ // list exprs aren't supported by CVC4; just return a tuple
+ return d_em->mkExpr(CVC4::kind::TUPLE, e1, e2);
}
Expr ValidityChecker::listExpr(const Expr& e1, const Expr& e2, const Expr& e3) {
- Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+ // list exprs aren't supported by CVC4; just return a tuple
+ return d_em->mkExpr(CVC4::kind::TUPLE, e1, e2, e3);
}
Expr ValidityChecker::listExpr(const std::string& op,
const std::vector<Expr>& kids) {
- Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+ // list exprs aren't supported by CVC4; just return a tuple
+ return d_em->mkExpr(CVC4::kind::TUPLE, d_em->mkConst(op), vector<CVC4::Expr>(kids.begin(), kids.end()));
}
Expr ValidityChecker::listExpr(const std::string& op, const Expr& e1) {
- Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+ // list exprs aren't supported by CVC4; just return a tuple
+ return d_em->mkExpr(CVC4::kind::TUPLE, d_em->mkConst(op), e1);
}
Expr ValidityChecker::listExpr(const std::string& op, const Expr& e1,
const Expr& e2) {
- Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+ // list exprs aren't supported by CVC4; just return a tuple
+ return d_em->mkExpr(CVC4::kind::TUPLE, d_em->mkConst(op), e1, e2);
}
Expr ValidityChecker::listExpr(const std::string& op, const Expr& e1,
const Expr& e2, const Expr& e3) {
- Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+ // list exprs aren't supported by CVC4; just return a tuple
+ return d_em->mkExpr(CVC4::kind::TUPLE, d_em->mkConst(op), e1, e2, e3);
}
void ValidityChecker::printExpr(const Expr& e) {
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) {
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();
}
Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop [to "
- << getLevel() << "]" << std::endl;
+ << getLevel() << "] " << this << std::endl;
}
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) {
#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 {
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.
*
#include "expr/kind.h"
#include "expr/type.h"
#include "expr/expr.h"
+#include "util/subrange_bound.h"
${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 {
* 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;
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);
/** Returns the maximum arity of the given kind. */
static unsigned maxArity(Kind kind);
+
};/* class ExprManager */
${mkConst_instantiations}
}
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() {
}
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<true> TypeCheckingExceptionPrivate::getNode() const throw() {
#include <algorithm>
#include <stack>
+#include <utility>
#include <ext/hash_set>
using namespace std;
}/* 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;
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 */
#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"
/** 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.
*
* (default: false)
*/
TypeNode getType(TNode n, bool check = false)
- throw (TypeCheckingExceptionPrivate, AssertionException);
+ throw(TypeCheckingExceptionPrivate, AssertionException);
/**
* Convert a node to an expression. Uses the ExprManager
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);
}
}
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;
}
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);
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();
}
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));
}
#include "util/Assert.h"
#include "util/cardinality.h"
+#include "util/subrange_bound.h"
namespace CVC4 {
class KindType;
class SortType;
class SortConstructorType;
+class PredicateSubtype;
+class SubrangeType;
class Type;
/** Strategy for hashing Types */
*/
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
};/* 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).
*/
return kind::mkGroundTerm(*this);
}
-bool TypeNode::isBoolean() const {
- return getKind() == kind::TYPE_CONSTANT &&
- ( getConst<TypeConstant>() == BOOLEAN_TYPE ||
- getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE );
-}
-
-bool TypeNode::isInteger() const {
- return getKind() == kind::TYPE_CONSTANT &&
- ( getConst<TypeConstant>() == INTEGER_TYPE ||
- getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE );
-}
-
-bool TypeNode::isReal() const {
- return getKind() == kind::TYPE_CONSTANT &&
- ( getConst<TypeConstant>() == REAL_TYPE ||
- getConst<TypeConstant>() == INTEGER_TYPE ||
- getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE );
-}
-
-bool TypeNode::isPseudoboolean() const {
- return getKind() == kind::TYPE_CONSTANT &&
- getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE;
-}
-
-bool TypeNode::isString() const {
- return getKind() == kind::TYPE_CONSTANT &&
- getConst<TypeConstant>() == 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<TypeConstant>()) {
+ case PSEUDOBOOLEAN_TYPE:
+ return t.getKind() == kind::TYPE_CONSTANT &&
+ ( t.getConst<TypeConstant>() == BOOLEAN_TYPE ||
+ t.getConst<TypeConstant>() == INTEGER_TYPE );
+ case INTEGER_TYPE:
+ return t.getKind() == kind::TYPE_CONSTANT && t.getConst<TypeConstant>() == REAL_TYPE;
+ default:
+ return false;
+ }
+ }
+ if(isSubrange()) {
+ if(t.isSubrange()) {
+ return t.getSubrangeBounds() <= getSubrangeBounds();
+ } else {
+ return t.getKind() == kind::TYPE_CONSTANT &&
+ ( t.getConst<TypeConstant>() == INTEGER_TYPE ||
+ t.getConst<TypeConstant>() == 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<Predicate>());
}
-bool TypeNode::isPredicate() const {
- return isFunction() && getRangeType().isBoolean();
+TypeNode TypeNode::getSubtypeBaseType() const {
+ Assert(isPredicateSubtype());
+ return getSubtypePredicate().getType().getArgTypes()[0];
}
std::vector<TypeNode> TypeNode::getArgTypes() 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> TypeNode::getTupleTypes() const {
Assert(isTuple());
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<TypeConstant>() == 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) {
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 <code>size</code> */
-bool TypeNode::isBitVector(unsigned size) const {
- return getKind() == kind::BITVECTOR_TYPE &&
- getConst<BitVectorSize>() == size;
-}
-
-/** Get the size of this bit-vector type */
-unsigned TypeNode::getBitVectorSize() const {
- Assert(isBitVector());
- return getConst<BitVectorSize>();
-}
-
}/* CVC4 namespace */
*/
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;
*/
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;
/** 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;
d_nv->printAst(out, indent);
}
+inline bool TypeNode::isBoolean() const {
+ return
+ ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE ) ||
+ isPseudoboolean() ||
+ ( isPredicateSubtype() && getSubtypeBaseType().isBoolean() );
+}
+
+inline bool TypeNode::isInteger() const {
+ return
+ ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE ) ||
+ isSubrange() ||
+ isPseudoboolean() ||
+ ( isPredicateSubtype() && getSubtypeBaseType().isInteger() );
+}
+
+inline bool TypeNode::isReal() const {
+ return
+ ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == REAL_TYPE ) ||
+ isInteger() ||
+ ( isPredicateSubtype() && getSubtypeBaseType().isReal() );
+}
+
+inline bool TypeNode::isPseudoboolean() const {
+ return
+ ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE ) ||
+ ( isPredicateSubtype() && getSubtypeBaseType().isPseudoboolean() );
+}
+
+inline bool TypeNode::isString() const {
+ return getKind() == kind::TYPE_CONSTANT &&
+ getConst<TypeConstant>() == 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<TypeConstant>() == 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 <code>size</code> */
+inline bool TypeNode::isBitVector(unsigned size) const {
+ return
+ ( getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size ) ||
+ ( isPredicateSubtype() && getSubtypeBaseType().isBitVector(size) );
+}
+
+/** Get the size of this bit-vector type */
+inline unsigned TypeNode::getBitVectorSize() const {
+ Assert(isBitVector());
+ return getConst<BitVectorSize>();
+}
+
+inline const SubrangeBounds& TypeNode::getSubrangeBounds() const {
+ Assert(isSubrange());
+ return getConst<SubrangeBounds>();
+}
+
#ifdef CVC4_DEBUG
/**
* Pretty printer for use within gdb. This is not intended to be used
ParserBuilder parserBuilder(&exprMgr, filename, options);
if( inputFromStdin ) {
- parserBuilder.withStreamInput(cin);
+ parserBuilder.withLineBufferedStreamInput(cin);
}
Parser *parser = parserBuilder.build();
withOptions(options);
if( inputFromStdin ) {
- parserBuilder.withStreamInput(cin);
+ parserBuilder.withLineBufferedStreamInput(cin);
}
Parser *parser = parserBuilder.build();
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. */
::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;
/* 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);
}
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');
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);
}
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');
}
}
- 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. */
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;
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 \
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 \
# 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),)
#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"
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;
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());
d_parser->rec->mismatch;
}
-
}/* CVC4::parser namespace */
}/* CVC4 namespace */
/** 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.
static AntlrInputStream* newStringInputStream(const std::string& input,
const std::string& name)
throw (InputStreamException, AssertionException);
-};
+};/* class AntlrInputStream */
class Parser;
/** 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;
--- /dev/null
+/********************* */
+/*! \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 <antlr3.h>
+#include <iostream>
+#include <string>
+
+#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 */
+
--- /dev/null
+/********************* */
+/*! \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 <antlr3.h>
+
+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 */
struct JavaPrinter {
template <class T>
JavaPrinter operator+(const T& t) const {
- ::CVC4::Message() << t;
+ Message() << t;
return JavaPrinter();
}
};/* struct JavaPrinter */
* 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;
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
PARENHASH = '(#';
HASHPAREN = '#)';
- //DOT = '.';
- DOTDOT = '..';
-
// Operators
ARROW_TOK = '->';
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 {
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]);
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 */
#include "util/output.h"
#include <vector>
+#include <string>
+#include <sstream>
#define REPEAT_COMMAND(k, CommandCtor) \
({ \
{ 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; }
)
| toplevelDeclaration[cmd]
;
-symbolicExpr[CVC4::SExpr& sexpr]
+simpleSymbolicExpr[CVC4::SExpr& sexpr]
@declarations {
- std::vector<SExpr> 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<SExpr> children;
+}
+ : simpleSymbolicExpr[sexpr]
| LPAREN (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN
{ sexpr = SExpr(children); }
;
bool& lhs]
@init {
Type t2;
- Expr f;
+ Expr f, f2;
std::string id;
std::vector<Type> types;
+ std::vector< std::pair<std::string, Type> > typeIds;
+ DeclarationScope* declScope;
+ Parser* parser;
lhs = false;
}
/* named types */
{ 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); }
}
} 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
| 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 */
+ )
;
/**
}
;
+/**
+ * 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<Expr> 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<Expr> 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 {
}
/* 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()) {
@init {
std::string name;
std::vector<Expr> args;
+ std::vector<std::string> names;
+ Expr e;
Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
Type t;
}
/* 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<Type> types;
+ for(std::vector<Expr>::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);
}
}
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<std::string, Type> > 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]
/**
* 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]
;
/**
*/
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 (?)
*/
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)
*/
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 */
*/
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.
*/
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
/** Set the Parser object for this input. */
virtual void setParser(Parser& parser) = 0;
+
};/* class Input */
}/* CVC4::parser namespace */
}
Expr Parser::getSymbol(const std::string& name, SymbolType type) {
+ checkDeclaration(name, CHECK_DECLARED, type);
Assert( isDeclared(name, type) );
switch( type ) {
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;
Type Parser::getSort(const std::string& name,
const std::vector<Type>& 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);
}
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;
}
return types;
}
+DatatypeType Parser::mkRecordType(const std::vector< std::pair<std::string, Type> >& 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<std::string, Type> >::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<Type>& types) {
+ DatatypeType& dtt = d_tupleTypes[types];
+ if(dtt.isNull()) {
+ Datatype dt("__cvc4_tuple");
+ DatatypeConstructor c("__cvc4_tuple_ctor");
+ for(std::vector<Type>::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:
/** 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<std::vector< std::pair<std::string, Type> >, 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<std::vector<Type>, DatatypeType> d_tupleTypes;
+
/** The set of operators available in the current logic. */
std::set<Kind> d_logicOperators;
std::vector<DatatypeType>
mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
+ /**
+ * Create a record type, or if there's already a matching one, return that one.
+ */
+ DatatypeType mkRecordType(const std::vector< std::pair<std::string, Type> >& typeIds);
+
+ /**
+ * Create a tuple type, or if there's already a matching one, return that one.
+ */
+ DatatypeType mkTupleType(const std::vector<Type>& types);
+
/**
* Add an operator to the current legal set.
*
}
}
+ inline void useDeclarationsFrom(DeclarationScope* scope) {
+ d_declScope = scope;
+ }
+
+ inline DeclarationScope* getDeclarationScope() const {
+ return d_declScope;
+ }
+
/**
* Gets the current declaration level.
*/
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()" );
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;
class CVC4_PUBLIC ParserBuilder {
enum InputType {
FILE_INPUT,
+ LINE_BUFFERED_STREAM_INPUT,
STREAM_INPUT,
STRING_INPUT
};
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);
/** 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 */
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;
case QF_UFIDL:
case QF_UFLIA:
+ case QF_UFNIA:// nonstandard logic
addTheory(THEORY_INTS);
addUf();
break;
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;
QF_UF,
QF_UFIDL,
QF_UFLIA,
+ QF_UFNIA, // nonstandard
QF_UFLRA,
+ QF_UFLIRA, // nonstandard
+ QF_UFNIRA, // nonstandard
QF_UFNRA,
UFNIA
};
#include "parser/smt2/smt2.h"
#include "parser/antlr_input.h"
-#include "parser/antlr_tracing.h"
using namespace CVC4;
using namespace CVC4::parser;
@parser::includes {
#include "expr/command.h"
#include "parser/parser.h"
+#include "parser/antlr_tracing.h"
namespace CVC4 {
class Expr;
extendedCommand[CVC4::Command*& cmd]
@declarations {
std::vector<CVC4::Datatype> dts;
+ Type t;
Expr e;
+ SExpr sexpr;
+ std::string name;
+ std::vector<std::string> names;
+ std::vector<Type> sorts;
}
/* Z3's extended SMT-LIBv2 set of commands syntax */
: DECLARE_DATATYPES_TOK
{ 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<SExpr> 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]
}
| KEYWORD
{ sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); }
+ ;
+
+symbolicExpr[CVC4::SExpr& sexpr]
+@declarations {
+ std::vector<SExpr> children;
+}
+ : simpleSymbolicExpr[sexpr]
| LPAREN_TOK
(symbolicExpr[sexpr] { children.push_back(sexpr); } )*
RPAREN_TOK
: ( 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.
*/
| 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; }
: ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )*
;
+nonemptySortList[std::vector<CVC4::Type>& 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.
// TILDE_TOK : '~';
XOR_TOK : 'xor';
+INTS_DIV_TOK : 'div';
+INTS_MOD_TOK : 'mod';
+
CONCAT_TOK : 'concat';
BVNOT_TOK : 'bvnot';
BVAND_TOK : 'bvand';
case Smt::QF_UFIDL:
case Smt::QF_UFLIA:
+ case Smt::QF_UFNIA:// nonstandard logic
addTheory(THEORY_INTS);
addOperator(kind::APPLY_UF);
break;
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;
break;
case kind::CONST_RATIONAL: {
const Rational& rat = n.getConst<Rational>();
- out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')';
+ if(rat.getDenominator() == 1) {
+ out << rat.getNumerator();
+ } else {
+ out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')';
+ }
break;
}
case kind::CONST_INTEGER: {
out << num;
break;
}
+ case kind::SUBRANGE_TYPE:
+ out << '[' << n.getConst<SubrangeBounds>() << ']';
+ break;
+ case kind::SUBTYPE_TYPE:
+ out << "SUBTYPE(" << n.getConst<Predicate>() << ")";
+ break;
case kind::TYPE_CONSTANT:
switch(TypeConstant tc = n.getConst<TypeConstant>()) {
case REAL_TYPE:
break;
}
break;
+
default:
Warning() << "Constant printing not implemented for the case of " << n.getKind() << endl;
out << n.getKind();
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;
break;
}
+ case kind::SUBRANGE_TYPE: {
+ const SubrangeBounds& bounds = n.getConst<SubrangeBounds>();
+ // 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<Predicate>() << ')';
+ break;
+
default:
// fall back on whatever operator<< does on underlying type; we
// might luck out and be SMT-LIB v2 compliant
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;
+ }
}
}
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
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;
// 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();
}
}
}
+ // 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;
}
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;
}
// 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;
}
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;
}
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;
}
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;
}
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;
}
// 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
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);
}
// Untranslate
infoPos.level = -1;
+ infoPos.recorded = false;
// Untranslate the negation node
// If not a not node, unregister it from sat and untranslate the negation
Assert(it != d_translationCache.end());
TranslationInfo& infoNeg = (*it).second;
infoNeg.level = -1;
+ infoNeg.recorded = false;
}
// undoTranslate the children
/** 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 */
}
/** 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.
}
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<Lit> propagatedLiterals;
DPLLMinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals);
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];
}
}
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
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) {
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);
vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made.
vec<int> trail_lim; // Separator indices for different decision levels in 'trail'.
vec<Lit> trail_user; // Stack of assignments to UNdo on user pop.
+ vec<int> trail_user_lim; // Separator indices for different user levels in 'trail'.
vec<bool> trail_ok; // Stack of "whether we're in conflict" flags.
vec<VarData> 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).
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)
{
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; "
// 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 */
*/
void pop();
+ /**
+ * Return true if we are currently searching (either in this or
+ * another thread).
+ */
+ bool isRunning() const;
+
/**
* Check the current time budget.
*/
*/
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();
}
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
return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
}
+bool DPLLMinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const {
+ return true;
+}
/** Incremental interface */
virtual void pop() = 0;
+ virtual bool properExplanation(SatLiteral lit, SatLiteral expl) const = 0;
+
};
// toodo add ifdef
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);
SatLiteralValue modelValue(SatLiteral l);
+ bool properExplanation(SatLiteral lit, SatLiteral expl) const;
+
/** Incremental interface */
int getAssertionLevel() const;
#include <vector>
#include <string>
+#include <iterator>
#include <utility>
#include <sstream>
+#include <stack>
#include <ext/hash_map>
#include "context/cdlist.h"
#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"
/** 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<theory::SubstitutionMap::iterator> d_lastSubstitutionPos;
+
/**
* Runs the nonclausal solver and tries to solve all the assigned
* theory literals.
*/
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<Node>& assertions)
+ throw(AssertionException);
+
/**
* Perform non-clausal simplification of a Node. This involves
* Theory implementations, but does NOT involve the SAT solver in
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 {
*/
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
*/
Node expandDefinitions(TNode n, hash_map<TNode, Node, TNodeHashFunction>& cache)
throw(NoSuchFunctionException, AssertionException);
+
};/* class SmtEnginePrivate */
}/* namespace CVC4::smt */
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);
}
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) {
}
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") {
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]);
}
<< "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
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);
d_assertionsToPreprocess.clear();
}
+void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertions)
+ throw(AssertionException) {
+
+ Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top << endl;
+
+ set<TNode> done;
+ stack<TNode> 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 {
d_cumulativeResourceUsed += resource;
Trace("limit") << "SmtEngine::check(): cumulative millis " << d_cumulativeTimeUsed
- << ", conflicts " << d_cumulativeResourceUsed << std::endl;
+ << ", conflicts " << d_cumulativeResourceUsed << endl;
return result;
}
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) {
void SmtEngine::push() {
NodeManagerScope nms(d_nodeManager);
Trace("smt") << "SMT push()" << endl;
+ d_private->processAssertions();
if(Dump.isOn("benchmark")) {
Dump("benchmark") << PushCommand() << endl;
}
}
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?
if(Options::current()->incrementalSolving) {
d_private->processAssertions();
d_userContext->push();
+ d_context->push();
d_propEngine->push();
}
}
Trace("smt") << "SmtEngine::internalPop()" << endl;
if(Options::current()->incrementalSolving) {
d_propEngine->pop();
+ d_context->pop();
d_userContext->pop();
}
}
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;
}
}
/**
* Destruct the SMT engine.
*/
- ~SmtEngine();
+ ~SmtEngine() throw();
/**
* Set the logic of the script.
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<Integer>() == 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<Integer>() == intOne){
+ Integer intZero(0);
+ return RewriteResponse(REWRITE_AGAIN, mkIntegerNode(intZero));
+ }else{
+ return RewriteResponse(REWRITE_DONE, t);
+ }
}else{
Unreachable();
}
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();
}
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 \
"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 \
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
#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 {
if (n.getKind() == kind::CONST_RATIONAL) return nodeManager->realType();
return nodeManager->integerType();
}
-};
+};/* class ArithConstantTypeRule */
class ArithOperatorTypeRule {
public:
}
return (isInteger ? integerType : realType);
}
-};
+};/* class ArithOperatorTypeRule */
class ArithPredicateTypeRule {
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<SubrangeBounds>();
+ 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<SubrangeBounds>();
+ 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 */
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
}
};/* 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 */
}
}/* CVC4::theory namespace */
+
+std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i) {
+ return out << "[CDMap-iterator]";
+}
+
}/* CVC4 namespace */
typedef context::CDMap<Node, Node, NodeHashFunction> NodeMap;
+ typedef NodeMap::iterator iterator;
+ typedef NodeMap::const_iterator const_iterator;
+
private:
typedef std::hash_map<Node, Node, NodeHashFunction> NodeCache;
return const_cast<SubstitutionMap*>(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
}
}/* CVC4::theory namespace */
+
+std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i);
+
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__SUBSTITUTIONS_H */
}
}
+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 */
protected:
- /**
+ /**
* A list of shared terms that the theory has.
*/
context::CDList<TNode> d_sharedTerms;
*/
static TheoryId s_uninterpretedSortOwner;
+ void printFacts(std::ostream& os) const;
+
+
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<TypeConstant>());
} else {
// 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)) {
/**
* 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.
ntuple.h \
recursion_breaker.h \
subrange_bound.h \
+ predicate.h \
+ predicate.cpp \
cardinality.h \
cardinality.cpp \
cache.h \
return ss.str();
}
-string Configuration::getCompiler() {
+std::string Configuration::getCompiler() {
stringstream ss;
#ifdef __GNUC__
ss << "GCC";
return ss.str();
}
+std::string Configuration::getCompiledDateTime() {
+ return __DATE__ " " __TIME__;
+}
+
}/* CVC4 namespace */
static std::string getSubversionId();
static std::string getCompiler();
+ static std::string getCompiledDateTime();
};/* class Configuration */
? ( ::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\
%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 >;
%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 >;
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;
}
#include <string.h>
#include <stdint.h>
#include <time.h>
+#include <sstream>
#include <getopt.h>
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\
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:
}
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) + "'");
+ }
}
}
#include <cstdio>
#include <cstdarg>
#include <set>
+#include <utility>
namespace CVC4 {
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<std::string> d_tags;
/** The warning output class */
class CVC4_PUBLIC WarningC {
+ std::set< std::pair<const char*, size_t> > d_alreadyWarned;
std::ostream* d_os;
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<const char*, size_t> 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 */
# 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
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
#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
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
#include "util/integer.h"
#include "util/Assert.h"
+#include <limits>
+
namespace CVC4 {
/**
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<size_t>::max();
+ size_t u = bounds.upper.hasBound() ? bounds.upper.getBound().hash() : std::numeric_limits<size_t>::max();
+ return l + 0x9e3779b9 + (u << 6) + (u >> 2);
+ }
+};/* struct SubrangeBoundsHashStrategy */
+
inline std::ostream&
operator<<(std::ostream& out, const SubrangeBound& bound) throw() CVC4_PUBLIC;
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 */
regress/regress0/arith/integers \
regress/regress0/uf \
regress/regress0/uflra \
+ regress/regress0/uflia \
regress/regress0/bv \
regress/regress0/bv/core \
regress/regress0/arrays \
regress/regress0/push-pop \
regress/regress0/precedence \
regress/regress0/preprocess \
+ regress/regress0/subtypes \
regress/regress1 \
regress/regress2 \
regress/regress3
ite4.smt2 \
simple-lra.smt2 \
simple-rdl.smt2 \
- simple-uf.smt2
+ simple-uf.smt2 \
+ simplification_bug4.smt2
# Regression tests for PL inputs
CVC_TESTS = \
bug216.smt2.expect \
bug288b.smt \
bug288c.smt \
- bug288.smt
+ bug288.smt \
+ simplification_bug4.smt2.expect
if CVC4_BUILD_PROFILE_COMPETITION
else
# 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 \
# and make sure to distribute it
EXTRA_DIST += \
- error.cvc
+ error.cvc \
+ rec4.cvc
# synonyms for "check"
.PHONY: regress regress0 test
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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);
--- /dev/null
+% 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;
units.cvc \
incremental-subst-bug.cvc
+SMT2_TESTS = \
+ tiny_bug.smt2
+
TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
EXTRA_DIST = $(TESTS)
--- /dev/null
+; 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)
+
--- /dev/null
+(set-logic QF_LIA)
+;; Simplified benchmark, derived from NuSMV output durationThm_1.bmc_k100.smt2
+;;
+;; Original version generated by Alberto Griggio <griggio@fbk.eu>
+;; 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)
+
--- /dev/null
+% COMMAND-LINE: --incremental
+% EXPECT: unsat
+% EXIT: 20
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
return SatValUnknown;
}
-};
+ bool properExplanation(SatLiteral lit, SatLiteral expl) const {
+ return true;
+ }
+
+};/* class FakeSatSolver */
class CnfStreamBlack : public CxxTest::TestSuite {
/** The SAT solver proxy */
projects / cvc5.git / commitdiff