diff options
-rw-r--r-- | src/expr/command.cpp | 10 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 4 | ||||
-rw-r--r-- | src/expr/node_manager.h | 12 | ||||
-rw-r--r-- | src/parser/parser.cpp | 110 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 30 | ||||
-rw-r--r-- | src/smt/Makefile.am | 2 | ||||
-rw-r--r-- | src/smt/boolean_terms.cpp | 254 | ||||
-rw-r--r-- | src/smt/boolean_terms.h | 62 | ||||
-rw-r--r-- | src/smt/options_handlers.h | 3 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 31 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 12 | ||||
-rw-r--r-- | src/util/datatype.cpp | 6 | ||||
-rw-r--r-- | src/util/datatype.h | 2 | ||||
-rw-r--r-- | src/util/exception.cpp | 15 | ||||
-rw-r--r-- | test/regress/regress0/Makefile.am | 7 | ||||
-rw-r--r-- | test/regress/regress0/bug217.smt2 (renamed from test/regress/regress0/uf/bug217.smt2) | 6 | ||||
-rw-r--r-- | test/regress/regress0/hung10_itesdk_output1.smt2 | 30 | ||||
-rw-r--r-- | test/regress/regress0/hung10_itesdk_output2.smt2 | 30 | ||||
-rw-r--r-- | test/regress/regress0/hung13sdk_output1.smt2 | 14 | ||||
-rw-r--r-- | test/regress/regress0/hung13sdk_output2.smt2 | 14 | ||||
-rwxr-xr-x | test/regress/run_regression | 4 |
21 files changed, 557 insertions, 101 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 5be612b20..8ded902b7 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -231,12 +231,6 @@ void PopCommand::invoke(SmtEngine* smtEngine) throw() { } } -/* class CheckSatCommand */ - -CheckSatCommand::CheckSatCommand() throw() : - d_expr() { -} - Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { return new PopCommand(); } @@ -247,6 +241,10 @@ Command* PopCommand::clone() const { /* class CheckSatCommand */ +CheckSatCommand::CheckSatCommand() throw() : + d_expr() { +} + CheckSatCommand::CheckSatCommand(const Expr& expr) throw() : d_expr(expr) { } diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 7cb5eb459..5159f6b5a 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -700,10 +700,6 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const { // 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; - } } } } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 6e08a9bc2..5cf591f9d 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1055,9 +1055,6 @@ NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) { 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); @@ -1070,9 +1067,6 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) { 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()); @@ -1085,9 +1079,6 @@ inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { 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); @@ -1119,9 +1110,6 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType, "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); } diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 10ca16001..57589ec9c 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -277,66 +277,70 @@ bool Parser::isUnresolvedType(const std::string& name) { 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) { diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index b3e16b38e..a61d2d4c0 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -20,7 +20,7 @@ #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> @@ -305,24 +305,23 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo 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"; @@ -823,6 +822,11 @@ void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const t 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++ ){ @@ -977,7 +981,7 @@ static void toStream(std::ostream& out, const GetValueCommand* c) throw() { } 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() { @@ -985,7 +989,7 @@ 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() { @@ -1007,9 +1011,9 @@ static void toStream(std::ostream& out, const GetInfoCommand* 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() { diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am index 82601e3c3..75f17326d 100644 --- a/src/smt/Makefile.am +++ b/src/smt/Makefile.am @@ -15,6 +15,8 @@ libsmt_la_SOURCES = \ command_list.cpp \ command_list.h \ modal_exception.h \ + boolean_terms.h \ + boolean_terms.cpp \ logic_exception.h \ simplification_mode.h \ simplification_mode.cpp diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp new file mode 100644 index 000000000..c332642f1 --- /dev/null +++ b/src/smt/boolean_terms.cpp @@ -0,0 +1,254 @@ +/********************* */ +/*! \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 */ diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h new file mode 100644 index 000000000..dea9adcf7 --- /dev/null +++ b/src/smt/boolean_terms.h @@ -0,0 +1,62 @@ +/********************* */ +/*! \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 */ diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h index 68b7222d7..a3065f29b 100644 --- a/src/smt/options_handlers.h +++ b/src/smt/options_handlers.h @@ -82,7 +82,7 @@ assertions\n\ + 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\ @@ -176,6 +176,7 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) { } 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")) { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 07e3439fc..8e6fcccb8 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -50,6 +50,7 @@ #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" @@ -105,6 +106,8 @@ public: 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 */ @@ -130,6 +133,7 @@ struct SmtEngineStatistics { 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"), @@ -143,6 +147,7 @@ struct SmtEngineStatistics { 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); @@ -158,6 +163,7 @@ struct SmtEngineStatistics { ~SmtEngineStatistics() { StatisticsRegistry::unregisterStat(&d_definitionExpansionTime); + StatisticsRegistry::unregisterStat(&d_rewriteBooleanTermsTime); StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime); StatisticsRegistry::unregisterStat(&d_numConstantProps); StatisticsRegistry::unregisterStat(&d_staticLearningTime); @@ -198,6 +204,9 @@ class SmtEnginePrivate : public NodeManagerListener { /** 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; @@ -334,6 +343,7 @@ public: d_assertionsToPreprocess(), d_nonClausalLearnedLiterals(), d_realAssertionsEnd(0), + d_booleanTermConverter(), d_propagator(d_nonClausalLearnedLiterals, true, true), d_assertionsToCheck(), d_fakeContext(), @@ -951,6 +961,13 @@ void SmtEngine::setLogicInternal() throw() { 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) @@ -2063,6 +2080,20 @@ void SmtEnginePrivate::processAssertions() { 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. diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 60d79e90e..42fe10cb9 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -694,7 +694,9 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa 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()); } @@ -792,7 +794,9 @@ Node TheoryEngine::preprocess(TNode assertion) { 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()); } @@ -882,7 +886,9 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, 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()); } diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index be98e40e1..18ecbc316 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -296,8 +296,8 @@ bool Datatype::operator==(const Datatype& other) const throw() { 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) { @@ -765,7 +765,7 @@ Expr DatatypeConstructorArg::getConstructor() const { return d_constructor; } -Type DatatypeConstructorArg::getType() const { +SelectorType DatatypeConstructorArg::getType() const { return getSelector().getType(); } diff --git a/src/util/datatype.h b/src/util/datatype.h index 4006702c5..de38d8835 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -111,7 +111,7 @@ public: * 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 diff --git a/src/util/exception.cpp b/src/util/exception.cpp index 95d307744..92f5c1840 100644 --- a/src/util/exception.cpp +++ b/src/util/exception.cpp @@ -19,6 +19,7 @@ #include <cstdio> #include <cstdlib> #include <cstdarg> +#include "util/cvc4_assert.h" using namespace std; using namespace CVC4; @@ -63,7 +64,14 @@ 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 */ } void IllegalArgumentException::construct(const char* header, const char* extra, @@ -96,5 +104,12 @@ 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 */ } diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 4789b0a55..6af6fbf70 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -49,7 +49,11 @@ SMT2_TESTS = \ 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 = \ @@ -116,6 +120,7 @@ BUG_TESTS = \ bug168.smt \ bug187.smt2 \ bug216.smt2 \ + bug217.smt2 \ bug220.smt2 \ bug239.smt \ bug274.cvc \ diff --git a/test/regress/regress0/uf/bug217.smt2 b/test/regress/regress0/bug217.smt2 index 45f0f3c0c..92b72c87d 100644 --- a/test/regress/regress0/uf/bug217.smt2 +++ b/test/regress/regress0/bug217.smt2 @@ -1,10 +1,12 @@ +; EXPECT: unsat +; EXIT: 20 (set-logic QF_UF) -(set-info :status unsat) +(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 (and x (or (f x) (f y)))) (assert (or (f x) (f y) (f z))) (assert (not (f false))) (assert (not (f true))) diff --git a/test/regress/regress0/hung10_itesdk_output1.smt2 b/test/regress/regress0/hung10_itesdk_output1.smt2 new file mode 100644 index 000000000..8bcdfdfbc --- /dev/null +++ b/test/regress/regress0/hung10_itesdk_output1.smt2 @@ -0,0 +1,30 @@ +( 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) diff --git a/test/regress/regress0/hung10_itesdk_output2.smt2 b/test/regress/regress0/hung10_itesdk_output2.smt2 new file mode 100644 index 000000000..8bcdfdfbc --- /dev/null +++ b/test/regress/regress0/hung10_itesdk_output2.smt2 @@ -0,0 +1,30 @@ +( 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) diff --git a/test/regress/regress0/hung13sdk_output1.smt2 b/test/regress/regress0/hung13sdk_output1.smt2 new file mode 100644 index 000000000..bf3ab9a26 --- /dev/null +++ b/test/regress/regress0/hung13sdk_output1.smt2 @@ -0,0 +1,14 @@ +( 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) diff --git a/test/regress/regress0/hung13sdk_output2.smt2 b/test/regress/regress0/hung13sdk_output2.smt2 new file mode 100644 index 000000000..bf3ab9a26 --- /dev/null +++ b/test/regress/regress0/hung13sdk_output2.smt2 @@ -0,0 +1,14 @@ +( 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) diff --git a/test/regress/run_regression b/test/regress/run_regression index 9333cdb8c..68c1e0677 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -121,12 +121,12 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then 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 |