From 428572ea18afa8fdcaaedfa0c293182cf5a00a3d Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 3 Apr 2014 19:16:39 -0400 Subject: [PATCH] Some incremental bugs for Boolean terms, fixed. Thanks to Pantazis Deligiannis and Jeroen Ketema for discovering this issue. --- src/smt/boolean_terms.cpp | 8 ++++---- src/smt/boolean_terms.h | 8 ++++---- src/smt/smt_engine.cpp | 3 +-- test/regress/regress0/Makefile.am | 2 ++ .../regress0/boolean-terms-kernel1.smt2 | 13 +++++++++++++ .../regress0/boolean-terms-kernel2.smt2 | 19 +++++++++++++++++++ 6 files changed, 43 insertions(+), 10 deletions(-) create mode 100644 test/regress/regress0/boolean-terms-kernel1.smt2 create mode 100644 test/regress/regress0/boolean-terms-kernel2.smt2 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 BooleanTermAttr; class BooleanTermConverter { /** The type of the Boolean term conversion variable cache */ - typedef std::hash_map BooleanTermVarCache; + typedef context::CDHashMap BooleanTermVarCache; /** The type of the Boolean term conversion cache */ - typedef std::hash_map< std::pair, Node, - PairHashFunction< Node, bool, - NodeHashFunction, std::hash > > BooleanTermCache; + typedef context::CDHashMap< std::pair, Node, + PairHashFunction< Node, bool, + NodeHashFunction, std::hash > > BooleanTermCache; /** The type of the Boolean term conversion type cache */ typedef std::hash_map< std::pair, 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) -- 2.30.2