d_tt(),
d_ffDt(),
d_ttDt(),
+ d_varCache(),
d_termCache(),
- d_typeCache() {
+ d_typeCache(),
+ d_datatypeCache() {
// set up our "false" and "true" conversions based on command-line option
if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS ||
Debug("boolean-terms") << "constructor " << (*c).getConstructor() << ":" << (*c).getConstructor().getType() << " made into " << newD[(*c).getName() + "'"].getConstructor() << ":" << newD[(*c).getName() + "'"].getConstructor().getType() << endl;
Node::fromExpr(newD[(*c).getName() + "'"].getConstructor()).setAttribute(BooleanTermAttr(), Node::fromExpr((*c).getConstructor()));// other attr?
Debug("boolean-terms") << "mapped " << newD[(*c).getName() + "'"].getConstructor() << " to " << (*c).getConstructor() << endl;
- d_termCache[make_pair(Node::fromExpr((*c).getConstructor()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor());
- d_termCache[make_pair(Node::fromExpr((*c).getTester()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getTester());
+ d_varCache[Node::fromExpr((*c).getConstructor())] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor());
+ d_varCache[Node::fromExpr((*c).getTester())] = Node::fromExpr(newD[(*c).getName() + "'"].getTester());
for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) {
- d_termCache[make_pair(Node::fromExpr((*a).getSelector()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'"));
+ d_varCache[Node::fromExpr((*a).getSelector())] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'"));
}
}
out = &newD;
if(!childrenPushed) {
Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - parentTheory=" << parentTheory << endl;
- BooleanTermCache::iterator i = d_termCache.find(pair<Node, theory::TheoryId>(top, parentTheory));
- if(i != d_termCache.end()) {
+ BooleanTermVarCache::iterator i = d_varCache.find(top);
+ if(i != d_varCache.end()) {
result.top() << ((*i).second.isNull() ? Node(top) : (*i).second);
worklist.pop();
goto next_worklist;
}
+ BooleanTermCache::iterator j = d_termCache.find(pair<Node, theory::TheoryId>(top, parentTheory));
+ if(j != d_termCache.end()) {
+ result.top() << ((*j).second.isNull() ? Node(top) : (*j).second);
+ worklist.pop();
+ goto next_worklist;
+ }
if(quantBoolVars.find(top) != quantBoolVars.end()) {
// this Bool variable is quantified over and we're changing it to a BitVector var
Node lam = nm->mkNode(kind::LAMBDA, boundVars, body);
Debug("boolean-terms") << "substituting " << top << " ==> " << lam << endl;
d_smt.d_theoryEngine->getModel()->addSubstitution(top, lam);
- d_termCache[make_pair(top, parentTheory)] = n;
+ d_varCache[top] = n;
result.top() << n;
worklist.pop();
goto next_worklist;
nm->mkConst(false), n_ff);
Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl;
d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl);
- d_termCache[make_pair(top, parentTheory)] = n;
+ d_varCache[top] = n;
result.top() << n;
worklist.pop();
goto next_worklist;
top.setAttribute(BooleanTermAttr(), n);
Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
- d_termCache[make_pair(top, parentTheory)] = n;
+ d_varCache[top] = n;
result.top() << n;
worklist.pop();
goto next_worklist;
nm->mkNode(kind::EQUAL, n_tt, d_tt));
Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl;
d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl);
- d_termCache[make_pair(top, parentTheory)] = n;
+ d_varCache[top] = n;
result.top() << n;
worklist.pop();
goto next_worklist;
}
- d_termCache[make_pair(top, parentTheory)] = Node::null();
+ d_varCache[top] = Node::null();
result.top() << top;
worklist.pop();
goto next_worklist;
Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl;
d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
- d_termCache[make_pair(top, parentTheory)] = n;
+ d_varCache[top] = n;
result.top() << n;
worklist.pop();
goto next_worklist;
}
- d_termCache[make_pair(top, parentTheory)] = Node::null();
+ d_varCache[top] = Node::null();
result.top() << top;
worklist.pop();
goto next_worklist;
Debug("boolean-terms") << "found a var of datatype type" << endl;
TypeNode newT = convertType(t, parentTheory == theory::THEORY_DATATYPES);
if(t != newT) {
- Assert(d_termCache.find(make_pair(top, parentTheory)) == d_termCache.end(),
+ Assert(d_varCache.find(top) == d_varCache.end(),
"Node `%s' already in cache ?!", top.toString().c_str());
Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
newT, "a datatype variable introduced by Boolean-term conversion",
top.setAttribute(BooleanTermAttr(), n);
d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
Debug("boolean-terms") << "constructed: " << n << " of type " << newT << endl;
- d_termCache[make_pair(top, parentTheory)] = n;
+ d_varCache[top] = n;
result.top() << n;
worklist.pop();
goto next_worklist;
} else {
- d_termCache[make_pair(top, parentTheory)] = Node::null();
+ d_varCache[top] = Node::null();
result.top() << top;
worklist.pop();
goto next_worklist;
TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>();
if(dt != dt2) {
- Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(),
+ Assert(d_varCache.find(top) != d_varCache.end(),
"constructor `%s' not in cache", top.toString().c_str());
- result.top() << d_termCache[make_pair(top, parentTheory)];
+ result.top() << d_varCache[top];
worklist.pop();
goto next_worklist;
}
- d_termCache[make_pair(top, parentTheory)] = Node::null();
+ d_varCache[top] = Node::null();
result.top() << top;
worklist.pop();
goto next_worklist;
TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>();
if(dt != dt2) {
- Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(),
+ Assert(d_varCache.find(top) != d_varCache.end(),
"tester or selector `%s' not in cache", top.toString().c_str());
- result.top() << d_termCache[make_pair(top, parentTheory)];
+ result.top() << d_varCache[top];
worklist.pop();
goto next_worklist;
} else {
- d_termCache[make_pair(top, parentTheory)] = Node::null();
+ d_varCache[top] = Node::null();
result.top() << top;
worklist.pop();
goto next_worklist;
NodeManager::SKOLEM_EXACT_NAME);
Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
top.setAttribute(BooleanTermAttr(), n);
- d_termCache[make_pair(top, parentTheory)] = n;
+ d_varCache[top] = n;
result.top() << n;
worklist.pop();
goto next_worklist;
typedef expr::Attribute<attr::BooleanTermAttrTag, Node> BooleanTermAttr;
class BooleanTermConverter {
+ /** The type of the Boolean term conversion variable cache */
+ typedef std::hash_map<Node, Node, NodeHashFunction> BooleanTermVarCache;
+
/** The type of the Boolean term conversion cache */
typedef std::hash_map< std::pair<Node, theory::TheoryId>, Node,
PairHashFunction< Node, bool,
/** The conversion for "true" when in datatypes contexts. */
Node d_ttDt;
+ /** The cache used during Boolean term variable conversion */
+ BooleanTermVarCache d_varCache;
/** The cache used during Boolean term conversion */
BooleanTermCache d_termCache;
/** The cache used during Boolean term type conversion */
hash_map<unsigned, Node> d_BVDivByZero;
hash_map<unsigned, Node> d_BVRemByZero;
-
/**
* Function symbol used to implement uninterpreted
* int-division-by-zero semantics. Needed to deal with partial
Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache)
throw(TypeCheckingException, LogicException);
+ /**
+ * Rewrite Boolean terms in a Node.
+ */
+ Node rewriteBooleanTerms(TNode n);
+
/**
* Simplify node "in" by expanding definitions and applying any
* substitutions learned from preprocessing.
return false;
}
+Node SmtEnginePrivate::rewriteBooleanTerms(TNode n) {
+ TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime);
+ if(d_booleanTermConverter == NULL) {
+ // This needs to be initialized _after_ the whole SMT framework is in place, subscribed
+ // to ExprManager notifications, etc. Otherwise we might miss the "BooleanTerm" datatype
+ // definition, and not dump it properly.
+ d_booleanTermConverter = new BooleanTermConverter(d_smt);
+ }
+ Node retval = d_booleanTermConverter->rewriteBooleanTerms(n);
+ if(retval != n) {
+ switch(booleans::BooleanTermConversionMode mode = options::booleanTermConversionMode()) {
+ case booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS:
+ case booleans::BOOLEAN_TERM_CONVERT_NATIVE:
+ if(!d_smt.d_logic.isTheoryEnabled(THEORY_BV)) {
+ d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+ d_smt.d_logic.enableTheory(THEORY_BV);
+ d_smt.d_logic.lock();
+ }
+ break;
+ case booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES:
+ if(!d_smt.d_logic.isTheoryEnabled(THEORY_DATATYPES)) {
+ d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+ d_smt.d_logic.enableTheory(THEORY_DATATYPES);
+ d_smt.d_logic.lock();
+ }
+ break;
+ default:
+ Unhandled(mode);
+ }
+ }
+ return retval;
+}
+
void SmtEnginePrivate::processAssertions() {
TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime);
dumpAssertions("pre-boolean-terms", d_assertionsToPreprocess);
{
Chat() << "rewriting Boolean terms..." << endl;
- TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime);
- if(d_booleanTermConverter == NULL) {
- // This needs to be initialized _after_ the whole SMT framework is in place, subscribed
- // to ExprManager notifications, etc. Otherwise we might miss the "BooleanTerm" datatype
- // definition, and not dump it properly.
- d_booleanTermConverter = new BooleanTermConverter(d_smt);
- }
for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) {
- Node n = d_booleanTermConverter->rewriteBooleanTerms(d_assertionsToPreprocess[i]);
- if(n != d_assertionsToPreprocess[i]) {
- switch(booleans::BooleanTermConversionMode mode = options::booleanTermConversionMode()) {
- case booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS:
- case booleans::BOOLEAN_TERM_CONVERT_NATIVE:
- if(!d_smt.d_logic.isTheoryEnabled(THEORY_BV)) {
- d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
- d_smt.d_logic.enableTheory(THEORY_BV);
- d_smt.d_logic.lock();
- }
- break;
- case booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES:
- if(!d_smt.d_logic.isTheoryEnabled(THEORY_DATATYPES)) {
- d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
- d_smt.d_logic.enableTheory(THEORY_DATATYPES);
- d_smt.d_logic.lock();
- }
- break;
- default:
- Unhandled(mode);
- }
- }
- d_assertionsToPreprocess[i] = n;
+ d_assertionsToPreprocess[i] = rewriteBooleanTerms(d_assertionsToPreprocess[i]);
}
}
dumpAssertions("post-boolean-terms", d_assertionsToPreprocess);
// do not need to apply preprocessing substitutions (should be recorded
// in model already)
+ Node n = Node::fromExpr(e);
+ Trace("smt") << "--- getting value of " << n << endl;
+ TypeNode expectedType = n.getType();
+
// Expand, then normalize
hash_map<Node, Node, NodeHashFunction> cache;
- Node n = d_private->expandDefinitions(Node::fromExpr(e), cache);
+ n = d_private->expandDefinitions(n, cache);
+ n = d_private->rewriteBooleanTerms(n);
n = Rewriter::rewrite(n);
Trace("smt") << "--- getting value of " << n << endl;
resultNode = m->getValue(n);
}
Trace("smt") << "--- got value " << n << " = " << resultNode << endl;
- resultNode = postprocess(resultNode, n.getType());
+ resultNode = postprocess(resultNode, expectedType);
Trace("smt") << "--- model-post returned " << resultNode << endl;
Trace("smt") << "--- model-post returned " << resultNode.getType() << endl;
- Trace("smt") << "--- model-post expected " << n.getType() << endl;
+ Trace("smt") << "--- model-post expected " << expectedType << endl;
// type-check the result we got
- Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(n.getType()));
+ Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(expectedType));
// ensure it's a constant
Assert(resultNode.getKind() == kind::LAMBDA || resultNode.isConst());
++i) {
Assert((*i).getType() == boolType);
+ Trace("smt") << "--- getting value of " << *i << endl;
+
// Expand, then normalize
hash_map<Node, Node, NodeHashFunction> cache;
Node n = d_private->expandDefinitions(*i, cache);
+ n = d_private->rewriteBooleanTerms(n);
n = Rewriter::rewrite(n);
Trace("smt") << "--- getting value of " << n << endl;
// type-check the result we got
Assert(resultNode.isNull() || resultNode.getType() == boolType);
+ // ensure it's a constant
+ Assert(resultNode.isConst());
+
vector<SExpr> v;
if((*i).getKind() == kind::APPLY) {
Assert((*i).getNumChildren() == 0);
bug521.minimized.smt2 \
bug522.smt2 \
bug528a.smt2 \
- bug541.smt2
+ bug541.smt2 \
+ bug544.smt2
TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
--- /dev/null
+; EXPECT: sat
+; EXPECT: (((not (select a x)) false))
+(set-option :produce-models true)
+(set-logic QF_AUFLIA)
+(declare-sort U 0)
+(declare-fun x () U)
+(declare-fun a () (Array U Bool))
+(assert (select a x))
+(check-sat)
+(get-value ((not (select a x))))
projects / cvc5.git / commitdiff