diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
commit | 1f4b954a2cc7667a56a3007fa75c125fba93ed23 (patch) | |
tree | ea8734e89aa5fba170781c7148d3fd886c597d4e /test | |
parent | 21b0cedd7dadd96e5d256885e3b65a926a7e4a81 (diff) |
Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
Diffstat (limited to 'test')
22 files changed, 361 insertions, 18 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 20de7a97c..1e533cc61 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -177,7 +177,9 @@ BUG_TESTS = \ bug595.cvc \ bug596.cvc \ bug596b.cvc \ - bug605.cvc + bug605.cvc \ + bt-test-00.smt2 \ + bt-test-01.smt2 #bug590.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am index b974bc95e..17cfa3fd4 100644 --- a/test/regress/regress0/arrays/Makefile.am +++ b/test/regress/regress0/arrays/Makefile.am @@ -49,7 +49,8 @@ TESTS = \ constarr2.cvc \ constarr3.cvc \ parsing_ringer.cvc \ - bug637.delta.smt2 + bug637.delta.smt2 \ + bool-array.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/arrays/bool-array.smt2 b/test/regress/regress0/arrays/bool-array.smt2 new file mode 100644 index 000000000..f05d0266b --- /dev/null +++ b/test/regress/regress0/arrays/bool-array.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores +; EXPECT: unsat +(set-logic QF_AX) +(set-info :status unsat) + +(declare-fun a () (Array Bool Bool)) +(declare-fun b () (Array Bool Bool)) + +(assert (not (= (select a (= a b)) (select a (not (= a b)))))) +(assert (= (select a true) (select a false))) + +(check-sat) + diff --git a/test/regress/regress0/bt-test-00.smt2 b/test/regress/regress0/bt-test-00.smt2 new file mode 100644 index 000000000..cd3e1137e --- /dev/null +++ b/test/regress/regress0/bt-test-00.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --no-check-proofs +; EXPECT: unsat +(set-logic QF_UF) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) + +(declare-fun f (Bool) Bool) +(declare-fun g (Bool) Bool) +(declare-fun h (Bool) Bool) + +(declare-fun x () Bool) +(declare-fun y () Bool) +(declare-fun z () Bool) + +(assert (not (= (f x) (f y)))) +(assert (not (= (g y) (g z)))) +(assert (not (= (h z) (h x)))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/bt-test-01.smt2 b/test/regress/regress0/bt-test-01.smt2 new file mode 100644 index 000000000..918dcf9ec --- /dev/null +++ b/test/regress/regress0/bt-test-01.smt2 @@ -0,0 +1,27 @@ +; COMMAND-LINE: --no-check-proofs +; EXPECT: unsat +(set-logic QF_UF) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) + +(declare-fun x0 () Bool) +(declare-fun y0 () Bool) +(declare-fun z0 () Bool) + +(assert (or x0 y0)) +(assert (or (not y0) z0)) + +(declare-fun x1 () Bool) +(declare-fun y1 () Bool) + +(assert x1) +(assert y1) + +(declare-fun f (Bool) Bool) + +(assert (not (= (f (or x0 z0)) (f (and x1 y1))))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/bug217.smt2 b/test/regress/regress0/bug217.smt2 index a1e29f63e..34cfcad33 100644 --- a/test/regress/regress0/bug217.smt2 +++ b/test/regress/regress0/bug217.smt2 @@ -1,6 +1,7 @@ +; COMMAND-LINE: --no-check-proofs ; EXPECT: unsat (set-logic QF_UF) -(set-info :status sat) +(set-info :status unsat) (set-option :produce-models true) (declare-fun f (Bool) Bool) (declare-fun x () Bool) diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index a8a637377..fed65924b 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -71,7 +71,10 @@ TESTS = \ coda_simp_model.smt2 \ Test1-tup-mp.cvc \ dt-param-card4-unsat.smt2 \ - dt-param-card4-bool-sat.smt2 + dt-param-card4-bool-sat.smt2 \ + bug604.smt2 \ + bug597-rbt.smt2 \ + example-dailler-min.smt2 FAILING_TESTS = \ datatype-dump.cvc diff --git a/test/regress/regress0/datatypes/bug597-rbt.smt2 b/test/regress/regress0/datatypes/bug597-rbt.smt2 new file mode 100644 index 000000000..45d82a522 --- /dev/null +++ b/test/regress/regress0/datatypes/bug597-rbt.smt2 @@ -0,0 +1,12 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +; Tree type +(declare-datatypes () ((Tree (node (data Int) (color Bool) (left Tree) (right Tree)) (nil)))) + +; content function +(declare-fun size (Tree) Int) +(assert (= (size nil) 0)) + + +(check-sat) diff --git a/test/regress/regress0/datatypes/bug604.smt2 b/test/regress/regress0/datatypes/bug604.smt2 new file mode 100644 index 000000000..15a60c3e3 --- /dev/null +++ b/test/regress/regress0/datatypes/bug604.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-datatypes () ( (PairIntInt (pair (firstPairIntInt Int) +(secondPairIntInt Int)) ) )) +(declare-fun /ArrayIntOfPair () (Array Int PairIntInt)) +(declare-datatypes () ( (SequenceABC (sequenceABC (a Int) (b Bool) (c Int)) ) +)) +(declare-fun /ArrayIntOfSequenceABC () (Array Int SequenceABC)) +(check-sat) diff --git a/test/regress/regress0/datatypes/example-dailler-min.smt2 b/test/regress/regress0/datatypes/example-dailler-min.smt2 new file mode 100644 index 000000000..1698fc3b0 --- /dev/null +++ b/test/regress/regress0/datatypes/example-dailler-min.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(set-info :status sat) +(declare-datatypes () ((D (C (R Bool))))) +(declare-fun a () (Array Int D)) +(declare-fun P ((Array Int D)) Bool) +(assert (P a)) +(check-sat) diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index af8776ace..79cff2947 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -65,7 +65,9 @@ TESTS = \ memory_model-R_cpp-dd.cvc \ bug764.smt2 \ ko-bound-set.cvc \ - cons-sets-bounds.smt2 + cons-sets-bounds.smt2 \ + bug651.smt2 \ + bug652.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/bug651.smt2 b/test/regress/regress0/fmf/bug651.smt2 new file mode 100644 index 000000000..9afc47972 --- /dev/null +++ b/test/regress/regress0/fmf/bug651.smt2 @@ -0,0 +1,43 @@ +; COMMAND-LINE: --fmf-fun --no-check-models +; EXPECT: sat +(set-logic UFDTSLIA) +(set-info :smt-lib-version 2.5) +(set-option :produce-models true) + +(declare-datatypes () ( + (Conditional_Int (Conditional_Int$CAbsent_Int) (Conditional_Int$CPresent_Int (Conditional_Int$CPresent_Int$value Int))) + (Conditional_T_titleType (Conditional_T_titleType$CAbsent_T_titleType) (Conditional_T_titleType$CPresent_T_titleType (Conditional_T_titleType$CPresent_T_titleType$value T_titleType))) + (Conditional_boolean (Conditional_boolean$CAbsent_boolean) (Conditional_boolean$CPresent_boolean (Conditional_boolean$CPresent_boolean$value Bool))) + (Conditional_string (Conditional_string$CAbsent_string) (Conditional_string$CPresent_string (Conditional_string$CPresent_string$value String))) + (Double (Double$CINF) (Double$CNINF) (Double$CNaN) (Double$CValue (Double$CValue$value Int))) + (List_T_titleType (List_T_titleType$CNil_T_titleType) (List_T_titleType$Cstr_T_titleType (List_T_titleType$Cstr_T_titleType$head T_titleType) (List_T_titleType$Cstr_T_titleType$tail List_T_titleType))) + (List_boolean (List_boolean$CNil_boolean) (List_boolean$Cstr_boolean (List_boolean$Cstr_boolean$head Bool) (List_boolean$Cstr_boolean$tail List_boolean))) + (List_string (List_string$CNil_string) (List_string$Cstr_string (List_string$Cstr_string$head String) (List_string$Cstr_string$tail List_string))) + (T_titleType (T_titleType$C_T_titleType (T_titleType$C_T_titleType$base String))) +) ) + +(define-fun f1361$isValid_string((x String)) Bool true) +(define-fun f5131$isValid_T_titleType((x T_titleType)) Bool (and (f1361$isValid_string (T_titleType$C_T_titleType$base x)) (<= (str.len (T_titleType$C_T_titleType$base x)) 80))) +(define-funs-rec + ( + (f5242$isValidElementsList_T_titleType((x List_T_titleType)) Bool) + ) + ( + (=> (is-List_T_titleType$Cstr_T_titleType x) (and (f5131$isValid_T_titleType (List_T_titleType$Cstr_T_titleType$head x)) (f5242$isValidElementsList_T_titleType (List_T_titleType$Cstr_T_titleType$tail x)))) + ) +) +(define-fun f1348$isValid_boolean((x Bool)) Bool true) +(define-funs-rec + ( + (f4169$isValidElementsList_boolean((x List_boolean)) Bool) + ) + ( + (=> (is-List_boolean$Cstr_boolean x) (and (f1348$isValid_boolean (List_boolean$Cstr_boolean$head x)) (f4169$isValidElementsList_boolean (List_boolean$Cstr_boolean$tail x)))) + ) +) + + +(declare-const title T_titleType) +(check-sat) + + diff --git a/test/regress/regress0/fmf/bug652.smt2 b/test/regress/regress0/fmf/bug652.smt2 new file mode 100644 index 000000000..13748eeea --- /dev/null +++ b/test/regress/regress0/fmf/bug652.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --fmf-fun --no-check-models +; EXPECT: sat +(set-logic UFDTSLIA) +(set-info :smt-lib-version 2.5) +(set-option :produce-models true) + +(declare-datatypes () ( + (List_boolean (List_boolean$CNil_boolean) (List_boolean$Cstr_boolean (List_boolean$Cstr_boolean$head Bool) (List_boolean$Cstr_boolean$tail List_boolean))) +) ) + +(define-funs-rec + ( + (f4208$lengthList_boolean((x List_boolean)) Int) + ) + ( + (ite (is-List_boolean$CNil_boolean x) 0 (+ 1 (f4208$lengthList_boolean (List_boolean$Cstr_boolean$tail x)))) + ) +) + + +(declare-const boolean Bool) +(check-sat) diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index 99619a6aa..262132779 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -46,7 +46,9 @@ BUG_TESTS = \ inc-double-u.smt2 \ fmf-fun-dbu.smt2 \ inc-define.smt2 \ - bug765.smt2 + bug765.smt2 \ + bug691.smt2 \ + bug694-Unapply1.scala-0.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/push-pop/bug691.smt2 b/test/regress/regress0/push-pop/bug691.smt2 new file mode 100644 index 000000000..df8964658 --- /dev/null +++ b/test/regress/regress0/push-pop/bug691.smt2 @@ -0,0 +1,21 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +(set-logic UFDTSLIA) +(set-info :smt-lib-version 2.5) + +(declare-datatypes () ( + (Response (Response$Response (Response$Response$success Bool))) + ) ) + + +(push 1) +(declare-fun $BLout$3248$0$1$() Response) +(assert (= $BLout$3248$0$1$ (Response$Response true))) +(check-sat) +(pop 1) + +(push 1) +(declare-fun $BLout$3248$2$1$() Response) +(assert (= $BLout$3248$2$1$ (Response$Response true))) +(check-sat) diff --git a/test/regress/regress0/push-pop/bug694-Unapply1.scala-0.smt2 b/test/regress/regress0/push-pop/bug694-Unapply1.scala-0.smt2 new file mode 100644 index 000000000..8fdee6f43 --- /dev/null +++ b/test/regress/regress0/push-pop/bug694-Unapply1.scala-0.smt2 @@ -0,0 +1,147 @@ +; COMMAND-LINE: --incremental +; EXPECT: unsat +; EXPECT: sat +; EXPECT: sat +(set-logic ALL) +(declare-fun start!1 () Bool) + +(assert start!1) + +(declare-fun b!15 () Bool) + +(declare-fun e!22 () Bool) + +(declare-fun error_value!0 () Bool) + +(assert (=> b!15 (= e!22 error_value!0))) + +(declare-fun b!16 () Bool) + +(declare-fun e!20 () Bool) + +(assert (=> b!16 (= e!20 e!22))) + +(declare-fun b!20 () Bool) + +(declare-datatypes () ( (Option!3 (None!1) (Some!1 (v!71 tuple2!0))) (tuple2!0 (tuple2!1 (_1!0 Unit!0) (_2!0 Bool))) (Unit!0 (Unit!1)) )) + +(declare-fun lt!7 () Option!3) + +(declare-fun Unit!2 () Unit!0) + +(assert (=> b!16 (= b!20 (ite (is-Some!1 lt!7) (= (_1!0 (v!71 lt!7)) Unit!2) false)))) + +(assert (=> b!16 (or (not b!20) (not b!15)))) + +(assert (=> b!16 (or b!20 b!15))) + +(declare-datatypes () ( (tuple3!0 (tuple3!1 (_1!1 (_ BitVec 32)) (_2!1 Bool) (_3!0 Unit!0))) )) + +(declare-fun unapply!2 (tuple3!0) Option!3) + +(declare-fun Unit!3 () Unit!0) + +(assert (=> b!16 (= lt!7 (unapply!2 (tuple3!1 #x0000002A false Unit!3))))) + +(declare-fun b!17 () Bool) + +(declare-fun e!21 () Bool) + +(assert (=> b!17 e!21)) + +(declare-fun b!18 () Bool) + +(declare-fun Unit!4 () Unit!0) + +(assert (=> b!18 (= e!20 (_2!0 (v!71 (unapply!2 (tuple3!1 #x0000002A false Unit!4))))))) + +(declare-fun lt!6 () Bool) + +(assert (=> start!1 (not lt!6))) + +(assert (=> start!1 (= lt!6 e!20))) + +(assert (=> start!1 (= b!18 e!21))) + +(assert (=> start!1 (or (not b!18) (not b!16)))) + +(assert (=> start!1 (or b!18 b!16))) + +(declare-fun b!19 () Bool) + +(assert (=> (and start!1 (not b!19)) (not e!21))) + +(declare-fun lt!8 () Option!3) + +(assert (=> start!1 (= b!19 (ite (is-Some!1 lt!8) true false)))) + +(declare-fun Unit!5 () Unit!0) + +(assert (=> start!1 (= lt!8 (unapply!2 (tuple3!1 #x0000002A false Unit!5))))) + +(assert (=> (and b!19 (not b!17)) (not e!21))) + +(declare-fun Unit!6 () Unit!0) + +(assert (=> b!19 (= b!17 (_2!0 (v!71 (unapply!2 (tuple3!1 #x0000002A false Unit!6))))))) + +(declare-fun Unit!7 () Unit!0) + +(assert (=> b!20 (= e!22 (_2!0 (v!71 (unapply!2 (tuple3!1 #x0000002A false Unit!7))))))) + +(push 1) + +(assert (and (and (and (and (not b!19) (not start!1)) (not b!20)) (not b!18)) (not b!16))) + +(check-sat) + +(pop 1) + +(push 1) + +(assert true) + +(check-sat) + +(pop 1) + +(declare-fun d!1 () Bool) + +(declare-fun e!25 () Bool) + +(assert (=> d!1 e!25)) + +(declare-fun b!23 () Bool) + +(assert (=> (and d!1 (not b!23)) (not e!25))) + +(declare-fun Unit!8 () Unit!0) + +(declare-fun Unit!9 () Unit!0) + +(declare-fun Unit!10 () Unit!0) + +(declare-fun Unit!11 () Unit!0) + +(assert (=> d!1 (= b!23 (= (unapply!2 (tuple3!1 #x0000002A false Unit!8)) (ite (= (_1!1 (tuple3!1 #x0000002A false Unit!9)) #x00000000) None!1 (Some!1 (tuple2!1 (_3!0 (tuple3!1 #x0000002A false Unit!10)) (_2!1 (tuple3!1 #x0000002A false Unit!11))))))))) + +(assert (=> b!23 (= e!25 true))) + +(assert (=> b!18 d!1)) + +(assert (=> start!1 d!1)) + +(assert (=> b!16 d!1)) + +(assert (=> b!20 d!1)) + +(assert (=> b!19 d!1)) + +(push 1) + +(assert true) + +(check-sat) + +(pop 1) + diff --git a/test/regress/regress0/quantifiers/small-bug1-fixpoint-3.smt2 b/test/regress/regress0/quantifiers/small-bug1-fixpoint-3.smt2 index da48f5e68..c26cde173 100644 --- a/test/regress/regress0/quantifiers/small-bug1-fixpoint-3.smt2 +++ b/test/regress/regress0/quantifiers/small-bug1-fixpoint-3.smt2 @@ -1,5 +1,6 @@ ; COMMAND-LINE: --cbqi-all --no-check-models ; EXPECT: sat +;AJR:BROKEN (set-logic UFBV) (set-info :status sat) (declare-fun Verilog__main.impl_PC_valid_64_1_39_!3 (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool) diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index 91b276889..8a4ce33b7 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -50,7 +50,8 @@ TESTS = \ cnf-iff-base.smt2 \ cnf-ite.smt2 \ cnf-and-neg.smt2 \ - cnf_abc.smt2 + cnf_abc.smt2 \ + bool-pred-nested.smt2 EXTRA_DIST = $(TESTS) \ mkpidgeon diff --git a/test/regress/regress0/uf/bool-pred-nested.smt2 b/test/regress/regress0/uf/bool-pred-nested.smt2 new file mode 100644 index 000000000..66275423e --- /dev/null +++ b/test/regress/regress0/uf/bool-pred-nested.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_UF) +(set-info :status sat) +(declare-fun P (Bool Bool) Bool) + +(assert (P (P true (P false false)) (P false true))) + +(check-sat) diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index eb0ff3ad3..bd00b770f 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -346,14 +346,14 @@ public: } void testIffNode() { - /* Node iffNode(const Node& right) const; */ + /* Node eqNode(const Node& right) const; */ Node left = d_nodeManager->mkConst(true); Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); - Node eq = left.iffNode(right); + Node eq = left.eqNode(right); - TS_ASSERT(IFF == eq.getKind()); + TS_ASSERT(EQUAL == eq.getKind()); TS_ASSERT(2 == eq.getNumChildren()); TS_ASSERT(*(eq.begin()) == left); @@ -398,8 +398,8 @@ public: Node n = d_nodeManager->mkNode(NOT, a); TS_ASSERT(NOT == n.getKind()); - n = d_nodeManager->mkNode(IFF, a, b); - TS_ASSERT(IFF == n.getKind()); + n = d_nodeManager->mkNode(EQUAL, a, b); + TS_ASSERT(EQUAL == n.getKind()); Node x = d_nodeManager->mkSkolem("x", *d_realType); Node y = d_nodeManager->mkSkolem("y", *d_realType); diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index c93accd33..7a6281e5b 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -178,7 +178,7 @@ class CnfStreamWhite : public CxxTest::TestSuite { d_nodeManager->mkNode( kind::IMPLIES, d_nodeManager->mkNode(kind::AND, a, b), d_nodeManager->mkNode( - kind::IFF, d_nodeManager->mkNode(kind::OR, c, d), + kind::EQUAL, d_nodeManager->mkNode(kind::OR, c, d), d_nodeManager->mkNode(kind::NOT, d_nodeManager->mkNode(kind::XOR, e, f)))), false, false, RULE_INVALID, Node::null()); @@ -203,7 +203,7 @@ class CnfStreamWhite : public CxxTest::TestSuite { NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::IFF, a, b), false, + d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::EQUAL, a, b), false, false, RULE_INVALID, Node::null()); TS_ASSERT(d_satSolver->addClauseCalled()); } diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h index cb5e20db9..e5c18ff83 100644 --- a/test/unit/util/boolean_simplification_black.h +++ b/test/unit/util/boolean_simplification_black.h @@ -94,10 +94,10 @@ public: hfc = d_nm->mkNode(kind::APPLY_UF, h, fc); gfb = d_nm->mkNode(kind::APPLY_UF, g, fb); - ac = d_nm->mkNode(kind::IFF, a, c); - ffbd = d_nm->mkNode(kind::IFF, ffb, d); - efhc = d_nm->mkNode(kind::IFF, e, fhc); - dfa = d_nm->mkNode(kind::IFF, d, fa); + ac = d_nm->mkNode(kind::EQUAL, a, c); + ffbd = d_nm->mkNode(kind::EQUAL, ffb, d); + efhc = d_nm->mkNode(kind::EQUAL, e, fhc); + dfa = d_nm->mkNode(kind::EQUAL, d, fa); // this test is designed for >= 10 removal threshold TS_ASSERT_LESS_THAN_EQUALS(10u, |