summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/command.cpp10
-rw-r--r--src/expr/expr_manager_template.cpp4
-rw-r--r--src/expr/node_manager.h12
-rw-r--r--src/parser/parser.cpp110
-rw-r--r--src/printer/cvc/cvc_printer.cpp30
-rw-r--r--src/smt/Makefile.am2
-rw-r--r--src/smt/boolean_terms.cpp254
-rw-r--r--src/smt/boolean_terms.h62
-rw-r--r--src/smt/options_handlers.h3
-rw-r--r--src/smt/smt_engine.cpp31
-rw-r--r--src/theory/theory_engine.cpp12
-rw-r--r--src/util/datatype.cpp6
-rw-r--r--src/util/datatype.h2
-rw-r--r--src/util/exception.cpp15
-rw-r--r--test/regress/regress0/Makefile.am7
-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.smt230
-rw-r--r--test/regress/regress0/hung10_itesdk_output2.smt230
-rw-r--r--test/regress/regress0/hung13sdk_output1.smt214
-rw-r--r--test/regress/regress0/hung13sdk_output2.smt214
-rwxr-xr-xtest/regress/run_regression4
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback