Passes simple tests and doesn't break existing functionality.
Still need some work merged in for models.
This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV). Tonight's nightly regression run should tell us if/how that hurts performance.
(this commit was certified error- and warning-free by the test-and-commit script.)
}
}
-/* class CheckSatCommand */
-
-CheckSatCommand::CheckSatCommand() throw() :
- d_expr() {
-}
-
Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
return new PopCommand();
}
/* class CheckSatCommand */
+CheckSatCommand::CheckSatCommand() throw() :
+ d_expr() {
+}
+
CheckSatCommand::CheckSatCommand(const Expr& expr) throw() :
d_expr(expr) {
}
// CVC4::Datatype class, but this actually needs to be checked.
AlwaysAssert(!SelectorType(selectorType).getRangeType().d_typeNode->isFunctionLike(),
"cannot put function-like things in datatypes");
- // currently don't play well with Boolean terms
- if(SelectorType(selectorType).getRangeType().d_typeNode->isBoolean()) {
- WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created a datatype containing a Boolean)" << std::endl;
- }
}
}
}
for (unsigned i = 0; i < sorts.size(); ++ i) {
CheckArgument(!sorts[i].isFunctionLike(), sorts,
"cannot create higher-order function types");
- if(i + 1 < sorts.size() && sorts[i].isBoolean()) {
- WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created a function type with a Boolean argument)" << std::endl;
- }
sortNodes.push_back(sorts[i]);
}
return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
for (unsigned i = 0; i < sorts.size(); ++ i) {
CheckArgument(!sorts[i].isFunctionLike(), sorts,
"cannot create higher-order function types");
- if(i + 1 < sorts.size() && sorts[i].isBoolean()) {
- WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created a predicate type with a Boolean argument)" << std::endl;
- }
sortNodes.push_back(sorts[i]);
}
sortNodes.push_back(booleanType());
for (unsigned i = 0; i < types.size(); ++ i) {
CheckArgument(!types[i].isFunctionLike(), types,
"cannot put function-like types in tuples");
- if(types[i].isBoolean()) {
- WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created a tuple type with a Boolean argument)" << std::endl;
- }
typeNodes.push_back(types[i]);
}
return mkTypeNode(kind::TUPLE_TYPE, typeNodes);
"cannot index arrays by a function-like type");
CheckArgument(!constituentType.isFunctionLike(), constituentType,
"cannot store function-like types in arrays");
- if(indexType.isBoolean() || constituentType.isBoolean()) {
- WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created an array type with a Boolean index or constituent type)" << std::endl;
- }
Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl;
return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
}
std::vector<DatatypeType>
Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
- std::vector<DatatypeType> types =
- d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
-
- assert(datatypes.size() == types.size());
-
- for(unsigned i = 0; i < datatypes.size(); ++i) {
- DatatypeType t = types[i];
- const Datatype& dt = t.getDatatype();
- const std::string& name = dt.getName();
- Debug("parser-idt") << "define " << name << " as " << t << std::endl;
- if(isDeclared(name, SYM_SORT)) {
- throw ParserException(name + " already declared");
- }
- if( t.isParametric() ) {
- std::vector< Type > paramTypes = t.getParamTypes();
- defineType(name, paramTypes, t );
- } else {
- defineType(name, t);
- }
- for(Datatype::const_iterator j = dt.begin(),
- j_end = dt.end();
- j != j_end;
- ++j) {
- const DatatypeConstructor& ctor = *j;
- Expr::printtypes::Scope pts(Debug("parser-idt"), true);
- Expr constructor = ctor.getConstructor();
- Debug("parser-idt") << "+ define " << constructor << std::endl;
- string constructorName = ctor.getName();
- if(isDeclared(constructorName, SYM_VARIABLE)) {
- throw ParserException(constructorName + " already declared");
+ try {
+ std::vector<DatatypeType> types =
+ d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
+
+ assert(datatypes.size() == types.size());
+
+ for(unsigned i = 0; i < datatypes.size(); ++i) {
+ DatatypeType t = types[i];
+ const Datatype& dt = t.getDatatype();
+ const std::string& name = dt.getName();
+ Debug("parser-idt") << "define " << name << " as " << t << std::endl;
+ if(isDeclared(name, SYM_SORT)) {
+ throw ParserException(name + " already declared");
}
- defineVar(constructorName, constructor);
- Expr tester = ctor.getTester();
- Debug("parser-idt") << "+ define " << tester << std::endl;
- string testerName = ctor.getTesterName();
- if(isDeclared(testerName, SYM_VARIABLE)) {
- throw ParserException(testerName + " already declared");
+ if( t.isParametric() ) {
+ std::vector< Type > paramTypes = t.getParamTypes();
+ defineType(name, paramTypes, t );
+ } else {
+ defineType(name, t);
}
- defineVar(testerName, tester);
- for(DatatypeConstructor::const_iterator k = ctor.begin(),
- k_end = ctor.end();
- k != k_end;
- ++k) {
- Expr selector = (*k).getSelector();
- Debug("parser-idt") << "+++ define " << selector << std::endl;
- string selectorName = (*k).getName();
- if(isDeclared(selectorName, SYM_VARIABLE)) {
- throw ParserException(selectorName + " already declared");
+ for(Datatype::const_iterator j = dt.begin(),
+ j_end = dt.end();
+ j != j_end;
+ ++j) {
+ const DatatypeConstructor& ctor = *j;
+ Expr::printtypes::Scope pts(Debug("parser-idt"), true);
+ Expr constructor = ctor.getConstructor();
+ Debug("parser-idt") << "+ define " << constructor << std::endl;
+ string constructorName = ctor.getName();
+ if(isDeclared(constructorName, SYM_VARIABLE)) {
+ throw ParserException(constructorName + " already declared");
+ }
+ defineVar(constructorName, constructor);
+ Expr tester = ctor.getTester();
+ Debug("parser-idt") << "+ define " << tester << std::endl;
+ string testerName = ctor.getTesterName();
+ if(isDeclared(testerName, SYM_VARIABLE)) {
+ throw ParserException(testerName + " already declared");
+ }
+ defineVar(testerName, tester);
+ for(DatatypeConstructor::const_iterator k = ctor.begin(),
+ k_end = ctor.end();
+ k != k_end;
+ ++k) {
+ Expr selector = (*k).getSelector();
+ Debug("parser-idt") << "+++ define " << selector << std::endl;
+ string selectorName = (*k).getName();
+ if(isDeclared(selectorName, SYM_VARIABLE)) {
+ throw ParserException(selectorName + " already declared");
+ }
+ defineVar(selectorName, selector);
}
- defineVar(selectorName, selector);
}
}
- }
- // These are no longer used, and the ExprManager would have
- // complained of a bad substitution if anything is left unresolved.
- // Clear out the set.
- d_unresolved.clear();
+ // These are no longer used, and the ExprManager would have
+ // complained of a bad substitution if anything is left unresolved.
+ // Clear out the set.
+ d_unresolved.clear();
- return types;
+ return types;
+ } catch(IllegalArgumentException& ie) {
+ throw ParserException(ie.getMessage());
+ }
}
bool Parser::isDeclared(const std::string& name, SymbolType type) {
#include "expr/node_manager.h" // for VarNameAttr
#include "expr/command.h"
#include "theory/substitutions.h"
-
+#include "smt/boolean_terms.h"
#include "theory/model.h"
#include <iostream>
break;
case kind::CONSTRUCTOR_TYPE:
case kind::SELECTOR_TYPE:
- if (n.getNumChildren() > 1) {
- if (n.getNumChildren() > 2) {
+ if(n.getNumChildren() > 1) {
+ if(n.getNumChildren() > 2) {
out << '(';
}
- for (unsigned i = 0; i < n.getNumChildren(); ++ i) {
- if (i > 0) {
+ for(unsigned i = 0; i < n.getNumChildren() - 1; ++i) {
+ if(i > 0) {
out << ", ";
}
toStream(out, n[i], depth, types, false);
}
- if (n.getNumChildren() > 2) {
+ if(n.getNumChildren() > 2) {
out << ')';
}
+ out << " -> ";
}
- out << " -> ";
- toStream(out, n[n.getNumChildren()-1], depth, types, false);
+ toStream(out, n[n.getNumChildren() - 1], depth, types, false);
return;
- break;
case kind::TESTER_TYPE:
toStream(out, n[0], depth, types, false);
out << " -> BOOLEAN";
Node n = Node::fromExpr( ((const DeclareFunctionCommand*)c)->getFunction() );
TypeNode tn = n.getType();
out << n << " : ";
+ /* Boolean terms functionality needs to be merged in
+ if(n.hasAttribute(smt::BooleanTermAttr())) {
+ out << "*** ";
+ }
+ */
if( tn.isFunction() || tn.isPredicate() ){
out << "(";
for( size_t i=0; i<tn.getNumChildren()-1; i++ ){
}
static void toStream(std::ostream& out, const GetModelCommand* c) throw() {
- out << "% (get-model)";
+ out << "COUNTERMODEL;";
}
static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() {
}
static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() {
- out << "% (get-assertions)";
+ out << "WHERE;";
}
static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() {
}
static void toStream(std::ostream& out, const SetOptionCommand* c) throw() {
- out << "% (set-option " << c->getFlag() << " ";
+ out << "OPTION \"" << c->getFlag() << "\" ";
toStream(out, c->getSExpr());
- out << ")";
+ out << ";";
}
static void toStream(std::ostream& out, const GetOptionCommand* c) throw() {
command_list.cpp \
command_list.h \
modal_exception.h \
+ boolean_terms.h \
+ boolean_terms.cpp \
logic_exception.h \
simplification_mode.h \
simplification_mode.cpp
--- /dev/null
+/********************* */
+/*! \file boolean_terms.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-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "smt/boolean_terms.h"
+#include "smt/smt_engine.h"
+#include "theory/theory_engine.h"
+#include "theory/model.h"
+#include "expr/kind.h"
+#include <string>
+#include <algorithm>
+
+using namespace std;
+using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace smt {
+
+const Datatype& BooleanTermConverter::booleanTermsConvertDatatype(const Datatype& dt) throw() {
+ return dt;
+ // boolean terms not supported in datatypes, yet
+
+ Debug("boolean-terms") << "booleanTermsConvertDatatype: considering " << dt.getName() << endl;
+ for(Datatype::const_iterator c = dt.begin(); c != dt.end(); ++c) {
+ TypeNode t = TypeNode::fromType((*c).getConstructor().getType());
+ for(TypeNode::const_iterator a = t.begin(); a != t.end(); ++a) {
+ if((*a).isBoolean()) {
+ Datatype newDt(dt.getName() + "'");
+ Debug("boolean-terms") << "found a Boolean arg in constructor " << (*c).getName() << endl;
+ for(c = dt.begin(); c != dt.end(); ++c) {
+ DatatypeConstructor ctor((*c).getName() + "'", (*c).getTesterName() + "'");
+ t = TypeNode::fromType((*c).getConstructor().getType());
+ for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) {
+ if((*a).getType().getRangeType().isBoolean()) {
+ ctor.addArg((*a).getName() + "'", NodeManager::currentNM()->mkBitVectorType(1).toType());
+ } else {
+ Type argType = (*a).getType().getRangeType();
+ if(argType.isDatatype() && DatatypeType(argType).getDatatype() == dt) {
+ ctor.addArg((*a).getName() + "'", DatatypeSelfType());
+ } else {
+ ctor.addArg((*a).getName() + "'", argType);
+ }
+ }
+ }
+ newDt.addConstructor(ctor);
+ }
+ DatatypeType newDtt = NodeManager::currentNM()->toExprManager()->mkDatatypeType(newDt);
+ const Datatype& newD = newDtt.getDatatype();
+ for(c = dt.begin(); c != dt.end(); ++c) {
+ Debug("boolean-terms") << "constructor " << (*c).getConstructor() << ":" << (*c).getConstructor().getType() << " made into " << newD[(*c).getName() + "'"].getConstructor() << ":" << newD[(*c).getName() + "'"].getConstructor().getType() << endl;
+ d_booleanTermCache[make_pair(Node::fromExpr((*c).getConstructor()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor());
+ d_booleanTermCache[make_pair(Node::fromExpr((*c).getTester()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getTester());
+ for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) {
+ d_booleanTermCache[make_pair(Node::fromExpr((*a).getSelector()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'"));
+ }
+ }
+ return newD;
+ }
+ }
+ }
+ return dt;
+}/* BooleanTermConverter::booleanTermsConvertDatatype() */
+
+Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw() {
+ Debug("boolean-terms") << "rewriteBooleanTerms: " << top << " - boolParent=" << boolParent << endl;
+
+ BooleanTermCache::iterator i = d_booleanTermCache.find(make_pair<Node, bool>(top, boolParent));
+ if(i != d_booleanTermCache.end()) {
+ return (*i).second.isNull() ? Node(top) : (*i).second;
+ }
+
+ Kind k = top.getKind();
+ kind::MetaKind mk = top.getMetaKind();
+
+ NodeManager* nm = NodeManager::currentNM();
+
+ if(!boolParent && top.getType().isBoolean()) {
+ Node one = nm->mkConst(BitVector(1u, 1u));
+ Node zero = nm->mkConst(BitVector(1u, 0u));
+ // still need to rewrite e.g. function applications over boolean
+ Node topRewritten = rewriteBooleanTerms(top, true);
+ Node n = nm->mkNode(kind::ITE, topRewritten, one, zero);
+ Debug("boolean-terms") << "constructed ITE: " << n << endl;
+ return n;
+ }
+
+ if(mk == kind::metakind::CONSTANT) {
+ Assert(k != kind::STORE_ALL, "array store-all not yet supported by Boolean-term conversion");
+ return top;
+ } else if(mk == kind::metakind::VARIABLE) {
+ TypeNode t = top.getType();
+ if(t.isFunction()) {
+ for(unsigned i = 0; i < t.getNumChildren() - 1; ++i) {
+ if(t[i].isBoolean()) {
+ vector<TypeNode> argTypes = t.getArgTypes();
+ replace(argTypes.begin(), argTypes.end(), t[i], nm->mkBitVectorType(1));
+ TypeNode newType = nm->mkFunctionType(argTypes, t.getRangeType());
+ Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "_bt",
+ newType, "a function introduced by Boolean-term conversion",
+ NodeManager::SKOLEM_EXACT_NAME);
+ Debug("boolean-terms") << "constructed func: " << n << " of type " << newType << endl;
+ top.setAttribute(BooleanTermAttr(), n);
+ d_booleanTermCache[make_pair(top, boolParent)] = n;
+ return n;
+ }
+ }
+ } else if(t.isArray()) {
+ TypeNode indexType = t.getArrayIndexType();
+ TypeNode constituentType = t.getArrayConstituentType();
+ bool rewrite = false;
+ if(indexType.isBoolean()) {
+ indexType = nm->mkBitVectorType(1);
+ rewrite = true;
+ }
+ if(constituentType.isBoolean()) {
+ constituentType = nm->mkBitVectorType(1);
+ rewrite = true;
+ }
+ if(rewrite) {
+ TypeNode newType = nm->mkArrayType(indexType, constituentType);
+ Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
+ newType, "an array variable introduced by Boolean-term conversion",
+ NodeManager::SKOLEM_EXACT_NAME);
+ top.setAttribute(BooleanTermAttr(), n);
+ Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
+ d_booleanTermCache[make_pair(top, boolParent)] = n;
+ return n;
+ }
+ d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
+ return top;
+ } else if(t.isTuple()) {
+ return top;
+ } else if(t.isRecord()) {
+ return top;
+ } else if(t.isDatatype()) {
+ const Datatype& dt = t.getConst<Datatype>();
+ const Datatype& dt2 = booleanTermsConvertDatatype(dt);
+ if(dt != dt2) {
+ Assert(d_booleanTermCache.find(make_pair(top, boolParent)) == d_booleanTermCache.end(),
+ "Node `%s' already in cache ?!", top.toString().c_str());
+ Assert(top.isVar());
+ TypeNode newType = TypeNode::fromType(dt2.getDatatypeType());
+ Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
+ newType, "an array variable introduced by Boolean-term conversion",
+ NodeManager::SKOLEM_EXACT_NAME);
+ top.setAttribute(BooleanTermAttr(), n);
+ Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
+ d_booleanTermCache[make_pair(top, boolParent)] = n;
+ return n;
+ } else {
+ d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
+ return top;
+ }
+ } else if(t.isConstructor()) {
+ Assert(!boolParent);
+ const Datatype& dt = t[t.getNumChildren() - 1].getConst<Datatype>();
+ const Datatype& dt2 = booleanTermsConvertDatatype(dt);
+ if(dt != dt2) {
+ Assert(d_booleanTermCache.find(make_pair(top, boolParent)) != d_booleanTermCache.end(),
+ "constructor `%s' not in cache", top.toString().c_str());
+ return d_booleanTermCache[make_pair(top, boolParent)];
+ } else {
+ d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
+ return top;
+ }
+ } else if(t.isTester() || t.isSelector()) {
+ Assert(!boolParent);
+ const Datatype& dt = t[0].getConst<Datatype>();
+ const Datatype& dt2 = booleanTermsConvertDatatype(dt);
+ if(dt != dt2) {
+ Assert(d_booleanTermCache.find(make_pair(top, boolParent)) != d_booleanTermCache.end(),
+ "tester or selector `%s' not in cache", top.toString().c_str());
+ return d_booleanTermCache[make_pair(top, boolParent)];
+ } else {
+ d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
+ return top;
+ }
+ } else if(t.getNumChildren() > 0) {
+ for(TypeNode::iterator i = t.begin(); i != t.end(); ++i) {
+ if((*i).isBoolean()) {
+ vector<TypeNode> argTypes(t.begin(), t.end());
+ replace(argTypes.begin(), argTypes.end(), *i, nm->mkBitVectorType(1));
+ TypeNode newType = nm->mkTypeNode(t.getKind(), argTypes);
+ Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
+ newType, "a variable introduced by Boolean-term conversion",
+ NodeManager::SKOLEM_EXACT_NAME);
+ Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
+ top.setAttribute(BooleanTermAttr(), n);
+ d_booleanTermCache[make_pair(top, boolParent)] = n;
+ return n;
+ }
+ }
+ }/* else if(t.isRecord()) {
+ Unimplemented();
+ }*/
+ return top;
+ }
+ switch(k) {
+ case kind::LAMBDA:
+ case kind::FORALL:
+ case kind::EXISTS:
+ case kind::REWRITE_RULE:
+ case kind::RR_REWRITE:
+ case kind::RR_REDUCTION:
+ case kind::RR_DEDUCTION:
+ //Assert(false, "not yet supported");
+ return top;
+
+ default:
+ NodeBuilder<> b(k);
+ Debug("bt") << "looking at: " << top << std::endl;
+ if(mk == kind::metakind::PARAMETERIZED) {
+ if(kindToTheoryId(k) != THEORY_BV &&
+ k != kind::TUPLE_SELECT &&
+ k != kind::TUPLE_UPDATE &&
+ k != kind::RECORD_SELECT &&
+ k != kind::RECORD_UPDATE &&
+ k != kind::RECORD) {
+ Debug("bt") << "rewriting: " << top.getOperator() << std::endl;
+ b << rewriteBooleanTerms(top.getOperator(), kindToTheoryId(k) == THEORY_BOOL);
+ Debug("bt") << "got: " << b.getOperator() << std::endl;
+ } else {
+ b << top.getOperator();
+ }
+ }
+ for(TNode::const_iterator i = top.begin(); i != top.end(); ++i) {
+ Debug("bt") << "rewriting: " << *i << std::endl;
+ b << rewriteBooleanTerms(*i, kindToTheoryId(k) == THEORY_BOOL);
+ Debug("bt") << "got: " << b[b.getNumChildren() - 1] << std::endl;
+ }
+ Node n = b;
+ Debug("boolean-terms") << "constructed: " << n << endl;
+ d_booleanTermCache[make_pair(top, boolParent)] = n;
+ return n;
+ }
+}/* BooleanTermConverter::rewriteBooleanTerms() */
+
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file boolean_terms.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-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "expr/attribute.h"
+#include "expr/node.h"
+#include "util/hash.h"
+#include <utility>
+
+namespace CVC4 {
+namespace smt {
+
+namespace attr {
+ struct BooleanTermAttrTag { };
+}/* CVC4::smt::attr namespace */
+
+typedef expr::Attribute<attr::BooleanTermAttrTag, Node> BooleanTermAttr;
+
+class BooleanTermConverter {
+ /** The type of the Boolean term conversion cache */
+ typedef std::hash_map< std::pair<Node, bool>, Node,
+ PairHashFunction< Node, bool,
+ NodeHashFunction, std::hash<int> > > BooleanTermCache;
+
+ /** The cache used during Boolean term conversion */
+ BooleanTermCache d_booleanTermCache;
+
+ /**
+ * Scan a datatype for and convert as necessary.
+ */
+ const Datatype& booleanTermsConvertDatatype(const Datatype& dt) throw();
+
+public:
+
+ /**
+ * We rewrite Boolean terms in assertions as bitvectors of length 1.
+ */
+ Node rewriteBooleanTerms(TNode n, bool boolParent = true) throw();
+
+};/* class BooleanTermConverter */
+
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
+ Output the assertions after preprocessing and before clausification.\n\
Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
where PASS is one of the preprocessing passes: definition-expansion\n\
- constrain-subtypes substitution skolem-quant simplify\n\
+ boolean-terms constrain-subtypes substitution skolem-quant simplify\n\
static-learning ite-removal repeat-simplify theory-preprocessing.\n\
PASS can also be the special value \"everything\", in which case the\n\
assertions are printed before any preprocessing (with\n\
}
if(!strcmp(p, "everything")) {
} else if(!strcmp(p, "definition-expansion")) {
+ } else if(!strcmp(p, "boolean-terms")) {
} else if(!strcmp(p, "constrain-subtypes")) {
} else if(!strcmp(p, "substitution")) {
} else if(!strcmp(p, "skolem-quant")) {
#include "util/configuration.h"
#include "util/exception.h"
#include "smt/command_list.h"
+#include "smt/boolean_terms.h"
#include "smt/options.h"
#include "options/option_exception.h"
#include "util/output.h"
struct SmtEngineStatistics {
/** time spent in definition-expansion */
TimerStat d_definitionExpansionTime;
+ /** time spent in Boolean term rewriting */
+ TimerStat d_rewriteBooleanTermsTime;
/** time spent in non-clausal simplification */
TimerStat d_nonclausalSimplificationTime;
/** Num of constant propagations found during nonclausal simp */
SmtEngineStatistics() :
d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
+ d_rewriteBooleanTermsTime("smt::SmtEngine::rewriteBooleanTermsTime"),
d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
d_staticLearningTime("smt::SmtEngine::staticLearningTime"),
d_checkModelTime("smt::SmtEngine::checkModelTime") {
StatisticsRegistry::registerStat(&d_definitionExpansionTime);
+ StatisticsRegistry::registerStat(&d_rewriteBooleanTermsTime);
StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime);
StatisticsRegistry::registerStat(&d_numConstantProps);
StatisticsRegistry::registerStat(&d_staticLearningTime);
~SmtEngineStatistics() {
StatisticsRegistry::unregisterStat(&d_definitionExpansionTime);
+ StatisticsRegistry::unregisterStat(&d_rewriteBooleanTermsTime);
StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime);
StatisticsRegistry::unregisterStat(&d_numConstantProps);
StatisticsRegistry::unregisterStat(&d_staticLearningTime);
/** Size of assertions array when preprocessing starts */
unsigned d_realAssertionsEnd;
+ /** The converter for Boolean terms -> BITVECTOR(1). */
+ BooleanTermConverter d_booleanTermConverter;
+
/** A circuit propagator for non-clausal propositional deduction */
booleans::CircuitPropagator d_propagator;
d_assertionsToPreprocess(),
d_nonClausalLearnedLiterals(),
d_realAssertionsEnd(0),
+ d_booleanTermConverter(),
d_propagator(d_nonClausalLearnedLiterals, true, true),
d_assertionsToCheck(),
d_fakeContext(),
setOption("check-models", SExpr("false"));
}
}
+
+ // may need to force BV on to handle Boolean terms
+ if(!d_logic.isPure(theory::THEORY_ARITH)) {
+ d_logic = d_logic.getUnlockedCopy();
+ d_logic.enableTheory(theory::THEORY_BV);
+ d_logic.lock();
+ }
}
void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+ dumpAssertions("pre-boolean-terms", d_assertionsToPreprocess);
+ {
+ Chat() << "rewriting Boolean terms..." << endl;
+ TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime);
+ for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) {
+ d_assertionsToPreprocess[i] =
+ d_booleanTermConverter.rewriteBooleanTerms(d_assertionsToPreprocess[i]);
+ }
+ }
+ dumpAssertions("post-boolean-terms", d_assertionsToPreprocess);
+
+ Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
+ Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
+
dumpAssertions("pre-constrain-subtypes", d_assertionsToPreprocess);
{
// Any variables of subtype types need to be constrained properly.
stringstream ss;
ss << "The logic was specified as " << d_logicInfo.getLogicString()
<< ", which doesn't include " << Theory::theoryOf(atom)
- << ", but got an asserted fact to that theory";
+ << ", but got a preprocessing-time fact for that theory." << endl
+ << "The fact:" << endl
+ << literal;
throw LogicException(ss.str());
}
stringstream ss;
ss << "The logic was specified as " << d_logicInfo.getLogicString()
<< ", which doesn't include " << Theory::theoryOf(current)
- << ", but got an asserted fact to that theory";
+ << ", but got a preprocesing-time fact for that theory." << endl
+ << "The fact:" << endl
+ << current;
throw LogicException(ss.str());
}
stringstream ss;
ss << "The logic was specified as " << d_logicInfo.getLogicString()
<< ", which doesn't include " << toTheoryId
- << ", but got an asserted fact to that theory";
+ << ", but got an asserted fact to that theory." << endl
+ << "The fact:" << endl
+ << assertion;
throw LogicException(ss.str());
}
return false;
}
- if(d_name != other.d_name ||
- getNumConstructors() != other.getNumConstructors()) {
+ if( d_name != other.d_name ||
+ getNumConstructors() != other.getNumConstructors() ) {
return false;
}
for(const_iterator i = begin(), j = other.begin(); i != end(); ++i, ++j) {
return d_constructor;
}
-Type DatatypeConstructorArg::getType() const {
+SelectorType DatatypeConstructorArg::getType() const {
return getSelector().getType();
}
* Get the type of the selector for this constructor argument;
* this call is only permitted after resolution.
*/
- Type getType() const;
+ SelectorType getType() const;
/**
* Get the name of the type of this constructor argument
#include <cstdio>
#include <cstdlib>
#include <cstdarg>
+#include "util/cvc4_assert.h"
using namespace std;
using namespace CVC4;
setMessage(string(buf));
+#ifdef CVC4_DEBUG
+ if(s_debugLastException == NULL) {
+ // we leak buf[] but only in debug mode with assertions failing
+ s_debugLastException = buf;
+ }
+#else /* CVC4_DEBUG */
delete [] buf;
+#endif /* CVC4_DEBUG */
}
void IllegalArgumentException::construct(const char* header, const char* extra,
setMessage(string(buf));
+#ifdef CVC4_DEBUG
+ if(s_debugLastException == NULL) {
+ // we leak buf[] but only in debug mode with assertions failing
+ s_debugLastException = buf;
+ }
+#else /* CVC4_DEBUG */
delete [] buf;
+#endif /* CVC4_DEBUG */
}
simple-uf.smt2 \
simplification_bug4.smt2 \
parallel-let.smt2 \
- get-value-incremental.smt2
+ get-value-incremental.smt2 \
+ hung13sdk_output1.smt2 \
+ hung10_itesdk_output2.smt2 \
+ hung10_itesdk_output1.smt2 \
+ hung13sdk_output2.smt2
# Regression tests for PL inputs
CVC_TESTS = \
bug168.smt \
bug187.smt2 \
bug216.smt2 \
+ bug217.smt2 \
bug220.smt2 \
bug239.smt \
bug274.cvc \
--- /dev/null
+; EXPECT: unsat
+; EXIT: 20
+(set-logic QF_UF)
+(set-info :status sat)
+(set-option :produce-models true)
+(declare-fun f (Bool) Bool)
+(declare-fun x () Bool)
+(declare-fun y () Bool)
+(declare-fun z () Bool)
+(assert (or (f x) (f y) (f z)))
+(assert (not (f false)))
+(assert (not (f true)))
+(check-sat)
+;(get-value ((f true) (f false) (f x) (f y) (f z) x y z))
--- /dev/null
+( set-logic QF_ALL_SUPPORTED)
+( set-info :source | SMT-COMP'06 organizers |)
+( set-info :smt-lib-version 2.0)
+( set-info :category "check")
+( set-info :status sat)
+( declare-fun x1 () Bool)
+( declare-fun x2 () Real)
+( declare-fun x3 () Real)
+( declare-fun x4 () Bool)
+( declare-fun x5 () Real)
+( declare-fun x6 () Real)
+( declare-fun x7 () Real)
+( declare-fun x8 () Real)
+( declare-fun bo1 () Bool)
+( declare-fun bo2 () Bool)
+( declare-fun bo3 () Bool)
+( declare-fun r1 () Real)
+( declare-fun r2 () Real)
+( declare-fun r3 () Real)
+( define-fun myBoolIte ( ( a Real) ( b Bool) ( c Bool)) Bool
+ ( ite ( > a 0.0) b c))
+( define-fun myRealIte ( ( a1 Bool) ( b1 Real) ( c1 Real)) Real
+ ( ite a1 b1 c1))
+( declare-fun f ( Real Bool) Real)
+( declare-fun fRealRealReal ( Real Real) Real)
+( declare-fun fRealReal ( Real) Real)
+( declare-fun fReal () Real)
+( assert ( = 4.0 ( + fReal ( myRealIte x1 x2 x3))))
+(check-sat)
+(exit)
--- /dev/null
+( set-logic QF_ALL_SUPPORTED)
+( set-info :source | SMT-COMP'06 organizers |)
+( set-info :smt-lib-version 2.0)
+( set-info :category "check")
+( set-info :status sat)
+( declare-fun x1 () Bool)
+( declare-fun x2 () Real)
+( declare-fun x3 () Real)
+( declare-fun x4 () Bool)
+( declare-fun x5 () Real)
+( declare-fun x6 () Real)
+( declare-fun x7 () Real)
+( declare-fun x8 () Real)
+( declare-fun bo1 () Bool)
+( declare-fun bo2 () Bool)
+( declare-fun bo3 () Bool)
+( declare-fun r1 () Real)
+( declare-fun r2 () Real)
+( declare-fun r3 () Real)
+( define-fun myBoolIte ( ( a Real) ( b Bool) ( c Bool)) Bool
+ ( ite ( > a 0.0) b c))
+( define-fun myRealIte ( ( a1 Bool) ( b1 Real) ( c1 Real)) Real
+ ( ite a1 b1 c1))
+( declare-fun f ( Real Bool) Real)
+( declare-fun fRealRealReal ( Real Real) Real)
+( declare-fun fRealReal ( Real) Real)
+( declare-fun fReal () Real)
+( assert ( = 4.0 ( + fReal ( myRealIte x1 x2 x3))))
+(check-sat)
+(exit)
--- /dev/null
+( set-logic QF_ALL_SUPPORTED)
+( set-info :source | SMT-COMP'06 organizers |)
+( set-info :smt-lib-version 2.0)
+( set-info :category "check")
+( set-info :status sat)
+( declare-fun x1 () Bool)
+( declare-fun x2 () Real)
+( declare-fun x3 () Real)
+( define-fun myRealIte ( ( a1 Bool) ( b1 Real) ( c1 Real)) Real
+ ( ite a1 b1 c1))
+( declare-fun fReal () Real)
+( assert ( = 4.0 ( + fReal ( myRealIte x1 x2 x3))))
+(check-sat)
+(exit)
--- /dev/null
+( set-logic QF_ALL_SUPPORTED)
+( set-info :source | SMT-COMP'06 organizers |)
+( set-info :smt-lib-version 2.0)
+( set-info :category "check")
+( set-info :status sat)
+( declare-fun x1 () Bool)
+( declare-fun x2 () Real)
+( declare-fun x3 () Real)
+( define-fun myRealIte ( ( a1 Bool) ( b1 Real) ( c1 Real)) Real
+ ( ite a1 b1 c1))
+( declare-fun fReal () Real)
+( assert ( = 4.0 ( + fReal ( myRealIte x1 x2 x3))))
+(check-sat)
+(exit)
+++ /dev/null
-(set-logic QF_UF)
-(set-info :status unsat)
-(declare-fun f (Bool) Bool)
-(declare-fun x () Bool)
-(declare-fun y () Bool)
-(declare-fun z () Bool)
-;(assert (and x (or (f x) (f y))))
-(assert (or (f x) (f y) (f z)))
-(assert (not (f false)))
-(assert (not (f true)))
-(check-sat)
-;(get-value ((f true) (f false) (f x) (f y) (f z) x y z))
error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
fi
benchmark=$tmpbenchmark
- elif grep '^ *(set-info *:status *sat' "$benchmark" &>/dev/null; then
+ elif grep '^ *( *set-info *:status *sat' "$benchmark" &>/dev/null; then
expected_proof=
expected_output=sat
expected_exit_status=10
command_line=
- elif grep '^ *(set-info *:status *unsat' "$benchmark" &>/dev/null; then
+ elif grep '^ *( *set-info *:status *unsat' "$benchmark" &>/dev/null; then
expected_proof=
expected_output=unsat
expected_exit_status=20
projects / cvc5.git / commitdiff