diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-03 19:16:39 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-03 19:38:21 -0400 |
commit | 428572ea18afa8fdcaaedfa0c293182cf5a00a3d (patch) | |
tree | 34c0fe0547e3aea8c5ef67f0ba3afc8d55df2500 /src/smt | |
parent | e99ed158fb2c5e030f38d048d2b2f2be6b11c7fb (diff) |
Some incremental bugs for Boolean terms, fixed. Thanks to Pantazis Deligiannis and Jeroen Ketema for discovering this issue.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/boolean_terms.cpp | 8 | ||||
-rw-r--r-- | src/smt/boolean_terms.h | 8 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 3 |
3 files changed, 9 insertions, 10 deletions
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index c1596dddc..4555aac51 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -43,8 +43,8 @@ BooleanTermConverter::BooleanTermConverter(SmtEngine& smt) : d_tt(), d_ffDt(), d_ttDt(), - d_varCache(), - d_termCache(), + d_varCache(smt.d_userContext), + d_termCache(smt.d_userContext), d_typeCache(), d_datatypeCache() { @@ -640,7 +640,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa if(dt != dt2) { Assert(d_varCache.find(top) != d_varCache.end(), "constructor `%s' not in cache", top.toString().c_str()); - result.top() << d_varCache[top]; + result.top() << d_varCache[top].get(); worklist.pop(); goto next_worklist; } @@ -658,7 +658,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa if(dt != dt2) { Assert(d_varCache.find(top) != d_varCache.end(), "tester or selector `%s' not in cache", top.toString().c_str()); - result.top() << d_varCache[top]; + result.top() << d_varCache[top].get(); worklist.pop(); goto next_worklist; } else { diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h index 89611f5ea..b289e3469 100644 --- a/src/smt/boolean_terms.h +++ b/src/smt/boolean_terms.h @@ -36,12 +36,12 @@ 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; + typedef context::CDHashMap<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, - NodeHashFunction, std::hash<size_t> > > BooleanTermCache; + typedef context::CDHashMap< std::pair<Node, theory::TheoryId>, Node, + PairHashFunction< Node, bool, + NodeHashFunction, std::hash<size_t> > > BooleanTermCache; /** The type of the Boolean term conversion type cache */ typedef std::hash_map< std::pair<TypeNode, bool>, TypeNode, PairHashFunction< TypeNode, bool, diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 328a20c28..7aebb60f6 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1877,8 +1877,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { d_assertionsToCheck[d_substitutionsIndex] = Rewriter::rewrite(Node(substitutionsBuilder)); } - } - else { + } else { // If not in incremental mode, must add substitutions to model TheoryModel* m = d_smt.d_theoryEngine->getModel(); if(m != NULL) { |