From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 3 Apr 2014 23:16:39 +0000 (-0400)
Subject: Some incremental bugs for Boolean terms, fixed.  Thanks to Pantazis Deligiannis and... 
X-Git-Tag: cvc5-1.0.0~6986
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=428572ea18afa8fdcaaedfa0c293182cf5a00a3d;p=cvc5.git

Some incremental bugs for Boolean terms, fixed.  Thanks to Pantazis Deligiannis and Jeroen Ketema for discovering this issue.
---

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) {
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 664958e5a..5df8577af 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -47,6 +47,8 @@ SMT_TESTS = \
 # Regression tests for SMT2 inputs
 SMT2_TESTS = \
 	arrayinuf_declare.smt2 \
+	boolean-terms-kernel1.smt2 \
+	boolean-terms-kernel2.smt2 \
 	chained-equality.smt2 \
 	ite2.smt2 \
 	ite3.smt2 \
diff --git a/test/regress/regress0/boolean-terms-kernel1.smt2 b/test/regress/regress0/boolean-terms-kernel1.smt2
new file mode 100644
index 000000000..a999a6a76
--- /dev/null
+++ b/test/regress/regress0/boolean-terms-kernel1.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: sat
+(set-logic QF_ABV)
+(declare-fun b () (_ BitVec 32))
+(declare-fun hk () (Array Bool (_ BitVec 32)))
+(push 1)
+(assert (not (= b (select hk true))))
+(check-sat)
+(pop 1)
+(assert (not (= b (_ bv0 32))))
+(assert (= b (select hk true)))
+(check-sat)
diff --git a/test/regress/regress0/boolean-terms-kernel2.smt2 b/test/regress/regress0/boolean-terms-kernel2.smt2
new file mode 100644
index 000000000..a4e49dd90
--- /dev/null
+++ b/test/regress/regress0/boolean-terms-kernel2.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: --incremental
+; EXPECT: unsat
+; EXPECT: sat
+(set-logic QF_ABV)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(declare-fun a () (Array Bool (Array (_ BitVec 32) (_ BitVec 32))))
+(declare-fun v2 () (_ BitVec 32))
+(declare-fun r0 () (_ BitVec 32))
+(declare-fun r1 () (_ BitVec 32))
+(declare-fun l () (_ BitVec 32))
+(declare-fun i () (_ BitVec 32))
+(assert c)
+(push 1)
+(assert (not (=> false (not (= i (select (select a true) (bvsub (bvmul (bvsdiv v2 (_ bv2 32)) (bvadd (bvmul (_ bv2 32) l) (_ bv1 32))) (_ bv1 32))))))))
+(check-sat)
+(pop 1)
+(assert (not (=> (= i (select (select a true) (bvsub (bvmul (bvsdiv v2 (_ bv2 32)) (bvadd (bvmul (_ bv2 32) l) (_ bv1 32))) (_ bv1 32)))) (not (= r1 (ite b i r0))))))
+(check-sat)