From a97944b850f201fd692aa870e830b8fa0369c541 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 9 Sep 2016 14:14:09 -0500 Subject: Support for separation logic + EPR. Refactor preprocessing of sep.nil, only allow sep disequal card constants when type is monotonic. Update logics on sep regressions. --- test/regress/regress0/sep/Makefile.am | 3 ++- test/regress/regress0/sep/chain-int.smt2 | 2 +- test/regress/regress0/sep/crash1220.smt2 | 2 +- test/regress/regress0/sep/dispose-list-4-init.smt2 | 2 +- test/regress/regress0/sep/dup-nemp.smt2 | 2 +- test/regress/regress0/sep/emp2-quant-unsat.smt2 | 12 ++++++++++++ test/regress/regress0/sep/loop-1220.smt2 | 2 +- test/regress/regress0/sep/nemp.smt2 | 2 +- test/regress/regress0/sep/nspatial-simp.smt2 | 2 +- test/regress/regress0/sep/pto-01.smt2 | 2 +- test/regress/regress0/sep/pto-02.smt2 | 2 +- test/regress/regress0/sep/pto-04.smt2 | 2 +- test/regress/regress0/sep/sep-01.smt2 | 2 +- test/regress/regress0/sep/sep-02.smt2 | 2 +- test/regress/regress0/sep/sep-03.smt2 | 2 +- test/regress/regress0/sep/sep-find2.smt2 | 2 +- test/regress/regress0/sep/sep-neg-1refine.smt2 | 2 +- test/regress/regress0/sep/sep-neg-nstrict.smt2 | 2 +- test/regress/regress0/sep/sep-neg-nstrict2.smt2 | 2 +- test/regress/regress0/sep/sep-neg-simple.smt2 | 2 +- test/regress/regress0/sep/sep-neg-swap.smt2 | 2 +- test/regress/regress0/sep/sep-nterm-again.smt2 | 2 +- test/regress/regress0/sep/sep-nterm-val-model.smt2 | 2 +- test/regress/regress0/sep/sep-plus1.smt2 | 2 +- test/regress/regress0/sep/sep-simp-unc.smt2 | 2 +- test/regress/regress0/sep/sep-simp-unsat-emp.smt2 | 2 +- test/regress/regress0/sep/simple-neg-sat.smt2 | 2 +- test/regress/regress0/sep/split-find-unsat-w-emp.smt2 | 2 +- test/regress/regress0/sep/split-find-unsat.smt2 | 2 +- test/regress/regress0/sep/wand-0526-sat.smt2 | 2 +- test/regress/regress0/sep/wand-crash.smt2 | 2 +- test/regress/regress0/sep/wand-false.smt2 | 2 +- test/regress/regress0/sep/wand-nterm-simp.smt2 | 2 +- test/regress/regress0/sep/wand-nterm-simp2.smt2 | 2 +- test/regress/regress0/sep/wand-simp-sat.smt2 | 2 +- test/regress/regress0/sep/wand-simp-sat2.smt2 | 2 +- test/regress/regress0/sep/wand-simp-unsat.smt2 | 2 +- 37 files changed, 49 insertions(+), 36 deletions(-) create mode 100644 test/regress/regress0/sep/emp2-quant-unsat.smt2 (limited to 'test') diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am index 6078bfa19..7bcd700bd 100644 --- a/test/regress/regress0/sep/Makefile.am +++ b/test/regress/regress0/sep/Makefile.am @@ -56,7 +56,8 @@ TESTS = \ fmf-nemp-2.smt2 \ trees-1.smt2 \ wand-false.smt2 \ - dup-nemp.smt2 + dup-nemp.smt2 \ + emp2-quant-unsat.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/sep/chain-int.smt2 b/test/regress/regress0/sep/chain-int.smt2 index d3245e33f..ebe52fa46 100644 --- a/test/regress/regress0/sep/chain-int.smt2 +++ b/test/regress/regress0/sep/chain-int.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/crash1220.smt2 b/test/regress/regress0/sep/crash1220.smt2 index a0fc5a187..f68434f33 100755 --- a/test/regress/regress0/sep/crash1220.smt2 +++ b/test/regress/regress0/sep/crash1220.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/dispose-list-4-init.smt2 b/test/regress/regress0/sep/dispose-list-4-init.smt2 index 766354cd9..b3e2088b1 100644 --- a/test/regress/regress0/sep/dispose-list-4-init.smt2 +++ b/test/regress/regress0/sep/dispose-list-4-init.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (declare-sort Loc 0) diff --git a/test/regress/regress0/sep/dup-nemp.smt2 b/test/regress/regress0/sep/dup-nemp.smt2 index 009561128..98348f617 100644 --- a/test/regress/regress0/sep/dup-nemp.smt2 +++ b/test/regress/regress0/sep/dup-nemp.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-sort Loc 0) (declare-const l Loc) diff --git a/test/regress/regress0/sep/emp2-quant-unsat.smt2 b/test/regress/regress0/sep/emp2-quant-unsat.smt2 new file mode 100644 index 000000000..52d99d8c0 --- /dev/null +++ b/test/regress/regress0/sep/emp2-quant-unsat.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --quant-epr +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-sort U 0) +(declare-fun u () U) + +(assert (sep (not (emp u)) (not (emp u)))) + +(assert (forall ((x U) (y U)) (= x y))) + +(check-sat) diff --git a/test/regress/regress0/sep/loop-1220.smt2 b/test/regress/regress0/sep/loop-1220.smt2 index 2981606d8..b857aec2a 100644 --- a/test/regress/regress0/sep/loop-1220.smt2 +++ b/test/regress/regress0/sep/loop-1220.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2 index e1e21dd10..a0766a7e0 100644 --- a/test/regress/regress0/sep/nemp.smt2 +++ b/test/regress/regress0/sep/nemp.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (assert (not (emp 0))) (check-sat) diff --git a/test/regress/regress0/sep/nspatial-simp.smt2 b/test/regress/regress0/sep/nspatial-simp.smt2 index 0c93719c9..c807757d1 100755 --- a/test/regress/regress0/sep/nspatial-simp.smt2 +++ b/test/regress/regress0/sep/nspatial-simp.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-fun x () Int) diff --git a/test/regress/regress0/sep/pto-01.smt2 b/test/regress/regress0/sep/pto-01.smt2 index b0dece248..28ed5c47b 100644 --- a/test/regress/regress0/sep/pto-01.smt2 +++ b/test/regress/regress0/sep/pto-01.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/pto-02.smt2 b/test/regress/regress0/sep/pto-02.smt2 index f0b6d2dee..ab1cea0c8 100644 --- a/test/regress/regress0/sep/pto-02.smt2 +++ b/test/regress/regress0/sep/pto-02.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) diff --git a/test/regress/regress0/sep/pto-04.smt2 b/test/regress/regress0/sep/pto-04.smt2 index 1734c93bb..9b0afda7a 100644 --- a/test/regress/regress0/sep/pto-04.smt2 +++ b/test/regress/regress0/sep/pto-04.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x1 Int) diff --git a/test/regress/regress0/sep/sep-01.smt2 b/test/regress/regress0/sep/sep-01.smt2 index c3330f036..a93fc4db8 100644 --- a/test/regress/regress0/sep/sep-01.smt2 +++ b/test/regress/regress0/sep/sep-01.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-02.smt2 b/test/regress/regress0/sep/sep-02.smt2 index 403bcf077..6f190d964 100644 --- a/test/regress/regress0/sep/sep-02.smt2 +++ b/test/regress/regress0/sep/sep-02.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-03.smt2 b/test/regress/regress0/sep/sep-03.smt2 index 427c44b50..8dce5acc7 100644 --- a/test/regress/regress0/sep/sep-03.smt2 +++ b/test/regress/regress0/sep/sep-03.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-find2.smt2 b/test/regress/regress0/sep/sep-find2.smt2 index 26a27eb22..356f866c1 100644 --- a/test/regress/regress0/sep/sep-find2.smt2 +++ b/test/regress/regress0/sep/sep-find2.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x1 Int) diff --git a/test/regress/regress0/sep/sep-neg-1refine.smt2 b/test/regress/regress0/sep/sep-neg-1refine.smt2 index 8ddbdd05f..ab12c6461 100644 --- a/test/regress/regress0/sep/sep-neg-1refine.smt2 +++ b/test/regress/regress0/sep/sep-neg-1refine.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-neg-nstrict.smt2 b/test/regress/regress0/sep/sep-neg-nstrict.smt2 index 1a69336a8..425e5ce3c 100644 --- a/test/regress/regress0/sep/sep-neg-nstrict.smt2 +++ b/test/regress/regress0/sep/sep-neg-nstrict.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-neg-nstrict2.smt2 b/test/regress/regress0/sep/sep-neg-nstrict2.smt2 index e71e6a51a..7ada6ff06 100644 --- a/test/regress/regress0/sep/sep-neg-nstrict2.smt2 +++ b/test/regress/regress0/sep/sep-neg-nstrict2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-neg-simple.smt2 b/test/regress/regress0/sep/sep-neg-simple.smt2 index 191e7527f..7b6fc69e9 100644 --- a/test/regress/regress0/sep/sep-neg-simple.smt2 +++ b/test/regress/regress0/sep/sep-neg-simple.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-neg-swap.smt2 b/test/regress/regress0/sep/sep-neg-swap.smt2 index f89a9c0ac..53f890b0d 100644 --- a/test/regress/regress0/sep/sep-neg-swap.smt2 +++ b/test/regress/regress0/sep/sep-neg-swap.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-nterm-again.smt2 b/test/regress/regress0/sep/sep-nterm-again.smt2 index 9b4afe36a..3e595b5e9 100644 --- a/test/regress/regress0/sep/sep-nterm-again.smt2 +++ b/test/regress/regress0/sep/sep-nterm-again.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-nterm-val-model.smt2 b/test/regress/regress0/sep/sep-nterm-val-model.smt2 index 0178134cb..d4fb0fd52 100644 --- a/test/regress/regress0/sep/sep-nterm-val-model.smt2 +++ b/test/regress/regress0/sep/sep-nterm-val-model.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-plus1.smt2 b/test/regress/regress0/sep/sep-plus1.smt2 index 772acd981..9522e2420 100644 --- a/test/regress/regress0/sep/sep-plus1.smt2 +++ b/test/regress/regress0/sep/sep-plus1.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/sep-simp-unc.smt2 b/test/regress/regress0/sep/sep-simp-unc.smt2 index 6cdf51294..cedbb53eb 100755 --- a/test/regress/regress0/sep/sep-simp-unc.smt2 +++ b/test/regress/regress0/sep/sep-simp-unc.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-sort U 0) (declare-fun x () U) diff --git a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 index fb58b9d10..9239fb770 100644 --- a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 +++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-sort U 0) diff --git a/test/regress/regress0/sep/simple-neg-sat.smt2 b/test/regress/regress0/sep/simple-neg-sat.smt2 index 0c0b6a9a3..70927ad82 100644 --- a/test/regress/regress0/sep/simple-neg-sat.smt2 +++ b/test/regress/regress0/sep/simple-neg-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) diff --git a/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 index ed3187a96..10e509e05 100644 --- a/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 +++ b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/split-find-unsat.smt2 b/test/regress/regress0/sep/split-find-unsat.smt2 index 1731174fa..1a9e76a8a 100644 --- a/test/regress/regress0/sep/split-find-unsat.smt2 +++ b/test/regress/regress0/sep/split-find-unsat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/regress0/sep/wand-0526-sat.smt2 b/test/regress/regress0/sep/wand-0526-sat.smt2 index 0c0ee72ad..fa0aab591 100644 --- a/test/regress/regress0/sep/wand-0526-sat.smt2 +++ b/test/regress/regress0/sep/wand-0526-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) (declare-fun y () Int) (declare-fun u () Int) diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2 index 9b4871323..1d799c8c9 100644 --- a/test/regress/regress0/sep/wand-crash.smt2 +++ b/test/regress/regress0/sep/wand-crash.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (assert (wand (emp 0) (emp 0))) (check-sat) diff --git a/test/regress/regress0/sep/wand-false.smt2 b/test/regress/regress0/sep/wand-false.smt2 index 642c0a8aa..65500f775 100644 --- a/test/regress/regress0/sep/wand-false.smt2 +++ b/test/regress/regress0/sep/wand-false.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-fun x () Int) (assert (wand (pto x x) false)) diff --git a/test/regress/regress0/sep/wand-nterm-simp.smt2 b/test/regress/regress0/sep/wand-nterm-simp.smt2 index e8ee4252c..0db7330d1 100644 --- a/test/regress/regress0/sep/wand-nterm-simp.smt2 +++ b/test/regress/regress0/sep/wand-nterm-simp.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) (assert (wand (emp x) (pto x 3))) (check-sat) diff --git a/test/regress/regress0/sep/wand-nterm-simp2.smt2 b/test/regress/regress0/sep/wand-nterm-simp2.smt2 index c317e8736..cce0f79e3 100644 --- a/test/regress/regress0/sep/wand-nterm-simp2.smt2 +++ b/test/regress/regress0/sep/wand-nterm-simp2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-fun x () Int) (assert (wand (pto x 1) (emp x))) diff --git a/test/regress/regress0/sep/wand-simp-sat.smt2 b/test/regress/regress0/sep/wand-simp-sat.smt2 index df4bfa6d8..120683f74 100755 --- a/test/regress/regress0/sep/wand-simp-sat.smt2 +++ b/test/regress/regress0/sep/wand-simp-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) (assert (wand (pto x 1) (pto x 1))) (check-sat) diff --git a/test/regress/regress0/sep/wand-simp-sat2.smt2 b/test/regress/regress0/sep/wand-simp-sat2.smt2 index 059e91317..c684d16ad 100755 --- a/test/regress/regress0/sep/wand-simp-sat2.smt2 +++ b/test/regress/regress0/sep/wand-simp-sat2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-fun x () Int) (assert (wand (pto x 1) (pto x 3))) diff --git a/test/regress/regress0/sep/wand-simp-unsat.smt2 b/test/regress/regress0/sep/wand-simp-unsat.smt2 index 95bc85537..c9851661a 100755 --- a/test/regress/regress0/sep/wand-simp-unsat.smt2 +++ b/test/regress/regress0/sep/wand-simp-unsat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (declare-fun x () Int) (assert (wand (pto x 1) (pto x 3))) (assert (emp x)) -- cgit v1.2.3 From 14fb8fac59e368a36e936a2d0497745eda72c637 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 9 Sep 2016 15:01:20 -0500 Subject: Fix bug in unconstrained simplifier related to sep.nil/distinguished variables. --- src/theory/unconstrained_simplifier.cpp | 2 +- test/regress/regress0/sep/trees-1.smt2 | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'test') diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index 6a33adc56..393a7c559 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -79,7 +79,7 @@ void UnconstrainedSimplifier::visitAll(TNode assertion) d_visitedOnce[current] = parent; if (current.getNumChildren() == 0) { - if (current.isVar()) { + if (current.getKind()==kind::VARIABLE || current.getKind()==kind::SKOLEM) { d_unconstrained.insert(current); } } diff --git a/test/regress/regress0/sep/trees-1.smt2 b/test/regress/regress0/sep/trees-1.smt2 index 88e875f70..8a46d9fdd 100644 --- a/test/regress/regress0/sep/trees-1.smt2 +++ b/test/regress/regress0/sep/trees-1.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-sort Loc 0) -- cgit v1.2.3 From 442c809911bcc45ae45dc97650146c459a841ea3 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 12 Sep 2016 13:43:02 -0500 Subject: Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry breaking in theory sep. --- src/expr/expr_manager_template.cpp | 4 ++- src/expr/node_manager.cpp | 23 ++++++++-------- src/expr/node_manager.h | 6 ++-- src/theory/sep/theory_sep.cpp | 47 ++++++++++++++------------------ src/theory/sep/theory_sep.h | 2 -- test/regress/regress0/sep/Makefile.am | 3 +- test/regress/regress0/sep/dispose-1.smt2 | 17 ++++++++++++ 7 files changed, 59 insertions(+), 43 deletions(-) create mode 100644 test/regress/regress0/sep/dispose-1.smt2 (limited to 'test') diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 2dc3aebe5..aa5634e7a 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -943,7 +943,9 @@ Expr ExprManager::mkBoundVar(Type type) { Expr ExprManager::mkSepNil(Type type) { NodeManagerScope nms(d_nodeManager); - return Expr(this, d_nodeManager->mkSepNilPtr(*type.d_typeNode)); + Node n = d_nodeManager->mkSepNil(*type.d_typeNode); + return n.toExpr(); + //return Expr(this, d_nodeManager->mkSepNilPtr(*type.d_typeNode)); } Expr ExprManager::mkAssociative(Kind kind, diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index d2ac7e2a1..94b136c46 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -169,6 +169,8 @@ NodeManager::~NodeManager() { for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) { d_operators[i] = Node::null(); } + + d_sep_nils.clear(); //d_tupleAndRecordTypes.clear(); d_tt_cache.d_children.clear(); @@ -682,17 +684,16 @@ Node NodeManager::mkInstConstant(const TypeNode& type) { } Node NodeManager::mkSepNil(const TypeNode& type) { - Node n = NodeBuilder<0>(this, kind::SEP_NIL); - n.setAttribute(TypeAttr(), type); - n.setAttribute(TypeCheckedAttr(), true); - return n; -} - -Node* NodeManager::mkSepNilPtr(const TypeNode& type) { - Node* n = NodeBuilder<0>(this, kind::SEP_NIL).constructNodePtr(); - setAttribute(*n, TypeAttr(), type); - setAttribute(*n, TypeCheckedAttr(), true); - return n; + std::map< TypeNode, Node >::iterator it = d_sep_nils.find( type ); + if( it==d_sep_nils.end() ){ + Node n = NodeBuilder<0>(this, kind::SEP_NIL); + n.setAttribute(TypeAttr(), type); + n.setAttribute(TypeCheckedAttr(), true); + d_sep_nils[type] = n; + return n; + }else{ + return it->second; + } } Node NodeManager::mkAbstractValue(const TypeNode& type) { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index dcd7005f8..79c7320f7 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -157,6 +157,9 @@ class NodeManager { * plusOperator->getConst(), you get kind::PLUS back. */ Node d_operators[kind::LAST_KIND]; + + /** sep nil per type */ + std::map< TypeNode, Node > d_sep_nils; /** * A list of subscribers for NodeManager events. @@ -487,9 +490,8 @@ public: /** Create a instantiation constant with the given type. */ Node mkInstConstant(const TypeNode& type); - /** Create nil reference for separation logic with the given type. */ + /** Create nil reference for separation logic with the given type (unique per type). */ Node mkSepNil(const TypeNode& type); - Node* mkSepNilPtr(const TypeNode& type); /** Make a new abstract value with the given type. */ Node mkAbstractValue(const TypeNode& type); diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index eefc0e779..fcf5ec88d 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -267,20 +267,6 @@ void TheorySep::postProcessModel( TheoryModel* m ){ void TheorySep::presolve() { Trace("sep-pp") << "Presolving" << std::endl; //TODO: cleanup if incremental? - - for( std::map< TypeNode, std::vector< Node > >::iterator it = d_pp_nils.begin(); it != d_pp_nils.end(); ++it ){ - Trace("sep-pp") << it->second.size() << " nil references of type " << it->first << std::endl; - if( !it->second.empty() ){ - setNilRef( it->first, it->second[0] ); - //ensure all instances of sep.nil are made equal - for( unsigned i=1; isecond.size(); i++ ){ - Node lem = NodeManager::currentNM()->mkNode( it->first.isBoolean() ? kind::IFF : kind::EQUAL, it->second[i], it->second[0] ); - Trace("sep-lemma") << "Sep::Lemma: nil ref eq : " << lem << std::endl; - d_out->lemma( lem ); - } - } - } - d_pp_nils.clear(); } @@ -784,7 +770,6 @@ TypeNode TheorySep::getDataType( Node n ) { //must process assertions at preprocess so that quantified assertions are processed properly void TheorySep::ppNotifyAssertions( std::vector< Node >& assertions ) { - d_pp_nils.clear(); std::map< Node, bool > visited; for( unsigned i=0; i& assertions ) { void TheorySep::processAssertion( Node n, std::map< Node, bool >& visited ) { if( visited.find( n )==visited.end() ){ visited[n] = true; - if( n.getKind()==kind::SEP_NIL ){ - TypeNode tn = n.getType(); - if( std::find( d_pp_nils[tn].begin(), d_pp_nils[tn].end(), n )==d_pp_nils[tn].end() ){ - d_pp_nils[tn].push_back( n ); - } - }else if( n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_EMP ){ + Trace("sep-pp-debug") << "process assertion : " << n << std::endl; + if( n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_EMP ){ //get the reference type (will compute d_type_references) int card = 0; TypeNode tn = computeReferenceType( n, card ); @@ -822,7 +803,7 @@ void TheorySep::processAssertion( Node n, std::map< Node, bool >& visited ) { } TypeNode TheorySep::computeReferenceType( Node atom, int& card, int index ) { - Trace("sep-type") << "getReference type " << atom << " " << index << std::endl; + Trace("sep-pp-debug") << "getReference type " << atom << " " << index << std::endl; Assert( atom.getKind()==kind::SEP_PTO || atom.getKind()==kind::SEP_STAR || atom.getKind()==kind::SEP_WAND || atom.getKind()==kind::SEP_EMP || index!=-1 ); std::map< int, TypeNode >::iterator it = d_reference_type[atom].find( index ); if( it==d_reference_type[atom].end() ){ @@ -878,7 +859,7 @@ TypeNode TheorySep::computeReferenceType( Node atom, int& card, int index ) { TypeNode TheorySep::computeReferenceType2( Node atom, int& card, int index, Node n, std::map< Node, int >& visited ) { if( visited.find( n )==visited.end() ){ - Trace("sep-type-debug") << "visit : " << n << " : " << atom << " " << index << std::endl; + Trace("sep-pp-debug") << "visit : " << n << " : " << atom << " " << index << std::endl; visited[n] = -1; if( n.getKind()==kind::SEP_PTO ){ //TODO: when THEORY_SETS supports mixed Int/Real sets @@ -926,9 +907,6 @@ TypeNode TheorySep::computeReferenceType2( Node atom, int& card, int index, Node TypeNode tn = n.getType(); TypeNode tnd; registerRefDataTypes( tn, tnd, n ); - if( std::find( d_pp_nils[tn].begin(), d_pp_nils[tn].end(), n )==d_pp_nils[tn].end() ){ - d_pp_nils[tn].push_back( n ); - } return tn; }else{ card = 0; @@ -1095,6 +1073,23 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { //slem = NodeManager::currentNM()->mkNode( kind::SUBSET, d_base_label[tn], d_reference_bound_max[tn] ); //Trace("sep-lemma") << "Sep::Lemma: base reference bound for " << tn << " : " << slem << std::endl; //d_out->lemma( slem ); + + //symmetry breaking + std::map< unsigned, Node > lit_mem_map; + for( unsigned i=0; imkNode( kind::MEMBER, d_type_references_card[tn][i], d_reference_bound[tn]); + } + for( unsigned i=0; i<(d_type_references_card[tn].size()-1); i++ ){ + std::vector< Node > children; + for( unsigned j=(i+1); jmkNode( kind::AND, children ); + sym_lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, lit_mem_map[i].negate(), sym_lem ); + Trace("sep-lemma") << "Sep::Lemma: symmetry breaking lemma : " << sym_lem << std::endl; + d_out->lemma( sym_lem ); + } } //assert that nil ref is not in base label diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 4f60c5781..a7ca3aff3 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -53,8 +53,6 @@ class TheorySep : public Theory { //whether bounds have been initialized bool d_bounds_init; - - std::map< TypeNode, std::vector< Node > > d_pp_nils; Node mkAnd( std::vector< TNode >& assumptions ); diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am index 7bcd700bd..b43a9a570 100644 --- a/test/regress/regress0/sep/Makefile.am +++ b/test/regress/regress0/sep/Makefile.am @@ -57,7 +57,8 @@ TESTS = \ trees-1.smt2 \ wand-false.smt2 \ dup-nemp.smt2 \ - emp2-quant-unsat.smt2 + emp2-quant-unsat.smt2 \ + dispose-1.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/sep/dispose-1.smt2 b/test/regress/regress0/sep/dispose-1.smt2 new file mode 100644 index 000000000..3c0e7df32 --- /dev/null +++ b/test/regress/regress0/sep/dispose-1.smt2 @@ -0,0 +1,17 @@ +(set-logic QF_ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const w Int) +(declare-const w1 Int) +(declare-const w2 Int) + +;------- f ------- +(assert (= w1 (as sep.nil Int))) +(assert (= w2 (as sep.nil Int))) +;----------------- + +(assert (pto w (as sep.nil Int))) +(assert (not (and (sep (and (emp 0) (= w2 (as sep.nil Int))) (pto w w1)) (sep (pto w w2) true)))) + +(check-sat) +;(get-model) -- cgit v1.2.3 From 374fc2396a4f4338ade7ea0fb958e26c9e3bb982 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 20 Sep 2016 16:02:14 -0500 Subject: More refactoring of cbqi. Add a few regressions. Add option for qcf. --- src/options/quantifiers_options | 5 +- src/theory/quantifiers/ceg_instantiator.cpp | 1093 ++++++++++---------- src/theory/quantifiers/ceg_instantiator.h | 45 +- src/theory/quantifiers/quant_conflict_find.cpp | 2 +- src/theory/quantifiers/quantifiers_rewriter.cpp | 9 +- test/regress/regress0/quantifiers/Makefile.am | 4 +- .../regress0/quantifiers/RNDPRE_4_1-dd-nqe.smt2 | 18 + .../regress0/quantifiers/mix-complete-strat.smt2 | 18 + 8 files changed, 620 insertions(+), 574 deletions(-) create mode 100644 test/regress/regress0/quantifiers/RNDPRE_4_1-dd-nqe.smt2 create mode 100644 test/regress/regress0/quantifiers/mix-complete-strat.smt2 (limited to 'test') diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 3fc589b5c..3269b7574 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -182,8 +182,6 @@ option qcfNestedConflict --qcf-nested-conflict bool :default false consider conflicts for nested quantifiers option qcfVoExp --qcf-vo-exp bool :default false qcf experimental variable ordering - - option instNoEntail --inst-no-entail bool :read-write :default true do not consider instances of quantified formulas that are currently entailed @@ -193,8 +191,11 @@ option instPropagate --inst-prop bool :read-write :default false option qcfEagerTest --qcf-eager-test bool :default true optimization, test qcf instances eagerly +option qcfEagerCheckRd --qcf-eager-check-rd bool :default true + optimization, eagerly check relevant domain of matched position option qcfSkipRd --qcf-skip-rd bool :default false optimization, skip instances based on possibly irrelevant portions of quantified formulas + ### rewrite rules options option quantRewriteRules --rewrite-rules bool :default false diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 987b69522..36eb66dfd 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -28,8 +28,6 @@ #include "theory/bv/theory_bv_utils.h" #include "util/bitvector.h" -//#define MBP_STRICT_ASSERTIONS - using namespace std; using namespace CVC4; using namespace CVC4::kind; @@ -83,6 +81,12 @@ bool CegInstantiator::isEligible( Node n ) { return d_inelig.find( n )==d_inelig.end(); } +bool CegInstantiator::hasVariable( Node n, Node pv ) { + computeProgVars( n ); + return d_prog_var[n].find( pv )!=d_prog_var[n].end(); +} + + void CegInstantiator::registerInstantiationVariable( Node v, unsigned index ) { if( d_instantiator.find( v )==d_instantiator.end() ){ TypeNode tn = v.getType(); @@ -154,7 +158,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e } Assert( vinst!=NULL ); d_active_instantiators[vinst] = true; - vinst->reset( pv, effort ); + vinst->reset( this, sf, pv, effort ); TypeNode pvtn = pv.getType(); TypeNode pvtnb = pvtn.getBaseType(); @@ -202,10 +206,6 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e if( vinst->processEqualTerm( this, sf, pv, pv_coeff, ns, effort ) ){ return true; } - //try the substitution - //if( doAddInstantiationInc( pv, ns, pv_coeff, 0, sf, effort ) ){ - // return true; - //} } } } @@ -219,87 +219,60 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e //[3] : we can solve an equality for pv ///iterate over equivalence classes to find cases where we can solve for the variable - Trace("cbqi-inst-debug") << "[3] try based on solving equalities." << std::endl; - for( unsigned k=0; k >::iterator it_reqc = d_curr_eqc.find( r ); - std::vector< Node > lhs; - std::vector< bool > lhs_v; - std::vector< Node > lhs_coeff; - Assert( it_reqc!=d_curr_eqc.end() ); - for( unsigned kk=0; kksecond.size(); kk++ ){ - Node n = it_reqc->second[kk]; - Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl; - //must be an eligible term - if( isEligible( n ) ){ - Node ns; - Node pv_coeff; - if( !d_prog_var[n].empty() ){ - ns = applySubstitution( pvtn, n, sf, pv_coeff ); - if( !ns.isNull() ){ - computeProgVars( ns ); + if( vinst->hasProcessEquality( this, sf, pv, effort ) ){ + Trace("cbqi-inst-debug") << "[3] try based on solving equalities." << std::endl; + for( unsigned k=0; k >::iterator it_reqc = d_curr_eqc.find( r ); + std::vector< Node > lhs; + std::vector< bool > lhs_v; + std::vector< Node > lhs_coeff; + Assert( it_reqc!=d_curr_eqc.end() ); + for( unsigned kk=0; kksecond.size(); kk++ ){ + Node n = it_reqc->second[kk]; + Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl; + //must be an eligible term + if( isEligible( n ) ){ + Node ns; + Node pv_coeff; + if( !d_prog_var[n].empty() ){ + ns = applySubstitution( pvtn, n, sf, pv_coeff ); + if( !ns.isNull() ){ + computeProgVars( ns ); + } + }else{ + ns = n; } - }else{ - ns = n; - } - if( !ns.isNull() ){ - bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end(); - Trace("cbqi-inst-debug2") << "... " << ns << " has var " << pv << " : " << hasVar << std::endl; - //std::vector< Node > term_coeffs; - //std::vector< Node > terms; - //term_coeffs.push_back( pv_coeff ); - //terms.push_back( ns ); - for( unsigned j=0; jmkNode( MULT, pv_coeff, eq_lhs ); - eq_lhs = Rewriter::rewrite( eq_lhs ); - } - if( !lhs_coeff[j].isNull() ){ - Trace("cbqi-inst-debug") << "...mult rhs by " << lhs_coeff[j] << std::endl; - eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff[j], eq_rhs ); - eq_rhs = Rewriter::rewrite( eq_rhs ); - } - } - Node eq = eq_lhs.eqNode( eq_rhs ); - eq = Rewriter::rewrite( eq ); - Node vts_coeff_inf; - Node vts_coeff_delta; - //isolate pv in the equality - int ires = solve_arith( pv, eq, veq_c, val, vts_coeff_inf, vts_coeff_delta ); - if( ires!=0 ){ - if( doAddInstantiationInc( pv, val, veq_c, 0, sf, effort ) ){ - return true; - } - } - }else if( pvtnb.isDatatype() ){ - val = solve_dt( pv, lhs[j], ns, lhs[j], ns ); - if( !val.isNull() ){ - if( doAddInstantiationInc( pv, val, veq_c, 0, sf, effort ) ){ - return true; - } + if( !ns.isNull() ){ + bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end(); + Trace("cbqi-inst-debug2") << "... " << ns << " has var " << pv << " : " << hasVar << std::endl; + std::vector< Node > term_coeffs; + std::vector< Node > terms; + term_coeffs.push_back( pv_coeff ); + terms.push_back( ns ); + for( unsigned j=0; jhasProcessAssertion( this, sf, pv, effort ) ){ Trace("cbqi-inst-debug") << "[4] try based on assertions." << std::endl; - d_vts_sym[0] = d_qe->getTermDatabase()->getVtsInfinity( pvtn, false, false ); - d_vts_sym[1] = d_qe->getTermDatabase()->getVtsDelta( false, false ); - std::vector< Node > mbp_bounds[2]; - std::vector< Node > mbp_coeff[2]; - std::vector< Node > mbp_vts_coeff[2][2]; - std::vector< Node > mbp_lit[2]; std::vector< Node > lits; //unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2; for( unsigned r=0; r<2; r++ ){ @@ -327,150 +294,6 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e if( vinst->processAssertion( this, sf, pv, lit, effort ) ){ return true; } - - - Trace("cbqi-inst-debug2") << " look at " << lit << std::endl; - Node atom = lit.getKind()==NOT ? lit[0] : lit; - bool pol = lit.getKind()!=NOT; - if( pvtn.isReal() ){ - //arithmetic inequalities and disequalities - if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ){ - Assert( atom.getKind()!=GEQ || atom[1].isConst() ); - Node atom_lhs; - Node atom_rhs; - if( atom.getKind()==GEQ ){ - atom_lhs = atom[0]; - atom_rhs = atom[1]; - }else{ - atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] ); - atom_lhs = Rewriter::rewrite( atom_lhs ); - atom_rhs = d_zero; - } - //must be an eligible term - if( isEligible( atom_lhs ) ){ - //apply substitution to LHS of atom - if( !d_prog_var[atom_lhs].empty() ){ - Node atom_lhs_coeff; - atom_lhs = applySubstitution( pvtn, atom_lhs, sf, atom_lhs_coeff ); - if( !atom_lhs.isNull() ){ - computeProgVars( atom_lhs ); - if( !atom_lhs_coeff.isNull() ){ - atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) ); - } - } - } - //if it contains pv, not infinity - if( !atom_lhs.isNull() && d_prog_var[atom_lhs].find( pv )!=d_prog_var[atom_lhs].end() ){ - Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs ); - //cannot contain infinity? - //if( !d_qe->getTermDatabase()->containsVtsInfinity( atom_lhs ) ){ - Trace("cbqi-inst-debug") << "..[3] From assertion : " << atom << ", pol = " << pol << std::endl; - Trace("cbqi-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl; - Node vts_coeff_inf; - Node vts_coeff_delta; - Node val; - Node veq_c; - //isolate pv in the inequality - int ires = solve_arith( pv, satom, veq_c, val, vts_coeff_inf, vts_coeff_delta ); - if( ires!=0 ){ - //disequalities are either strict upper or lower bounds - unsigned rmax = ( atom.getKind()==GEQ || options::cbqiModel() ) ? 1 : 2; - for( unsigned r=0; rmkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); - uval = Rewriter::rewrite( uval ); - }else{ - Assert( pvtn.isReal() ); - //now is strict inequality - uires = uires*2; - } - } - }else{ - bool is_upper; - if( options::cbqiModel() ){ - // disequality is a disjunction : only consider the bound in the direction of the model - //first check if there is an infinity... - if( !vts_coeff_inf.isNull() ){ - //coefficient or val won't make a difference, just compare with zero - Trace("cbqi-inst-debug") << "Disequality : check infinity polarity " << vts_coeff_inf << std::endl; - Assert( vts_coeff_inf.isConst() ); - is_upper = ( vts_coeff_inf.getConst().sgn()==1 ); - }else{ - Node rhs_value = getModelValue( val ); - Node lhs_value = pv_value; - if( !veq_c.isNull() ){ - lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, veq_c ); - lhs_value = Rewriter::rewrite( lhs_value ); - } - Trace("cbqi-inst-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl; - Assert( lhs_value!=rhs_value ); - Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value ); - cmp = Rewriter::rewrite( cmp ); - Assert( cmp.isConst() ); - is_upper = ( cmp!=d_true ); - } - }else{ - is_upper = (r==0); - } - Assert( atom.getKind()==EQUAL && !pol ); - if( pvtn.isInteger() ){ - uires = is_upper ? -1 : 1; - uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); - uval = Rewriter::rewrite( uval ); - }else{ - Assert( pvtn.isReal() ); - uires = is_upper ? -2 : 2; - } - } - Trace("cbqi-bound-inf") << "From " << lit << ", got : "; - if( !veq_c.isNull() ){ - Trace("cbqi-bound-inf") << veq_c << " * "; - } - Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl; - //take into account delta - if( d_use_vts_delta && ( uires==2 || uires==-2 ) ){ - if( options::cbqiModel() ){ - Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) ); - if( vts_coeff_delta.isNull() ){ - vts_coeff_delta = delta_coeff; - }else{ - vts_coeff_delta = NodeManager::currentNM()->mkNode( PLUS, vts_coeff_delta, delta_coeff ); - vts_coeff_delta = Rewriter::rewrite( vts_coeff_delta ); - } - }else{ - Node delta = d_qe->getTermDatabase()->getVtsDelta(); - uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta ); - uval = Rewriter::rewrite( uval ); - } - } - if( options::cbqiModel() ){ - //just store bounds, will choose based on tighest bound - unsigned index = uires>0 ? 0 : 1; - mbp_bounds[index].push_back( uval ); - mbp_coeff[index].push_back( veq_c ); - Trace("cbqi-inst-debug") << "Store bound " << index << " " << uval << " " << veq_c << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit << std::endl; - for( unsigned t=0; t<2; t++ ){ - mbp_vts_coeff[index][t].push_back( t==0 ? vts_coeff_inf : vts_coeff_delta ); - } - mbp_lit[index].push_back( lit ); - }else{ - //try this bound - if( doAddInstantiationInc( pv, uval, veq_c, uires>0 ? 1 : -1, sf, effort ) ){ - return true; - } - } - } - } - } - } - } - } } } } @@ -478,206 +301,6 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e if( vinst->processAssertions( this, sf, pv, lits, effort ) ){ return true; } - if( options::cbqiModel() ){ - if( pvtn.isInteger() || pvtn.isReal() ){ - bool use_inf = d_use_vts_inf && ( pvtn.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() ); - bool upper_first = false; - if( options::cbqiMinBounds() ){ - upper_first = mbp_bounds[1].size() t_values[3]; - //try optimal bounds - for( unsigned r=0; r<2; r++ ){ - int rr = upper_first ? (1-r) : r; - best_used[rr] = -1; - if( mbp_bounds[rr].empty() ){ - if( use_inf ){ - Trace("cbqi-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << pvtn << ")" << std::endl; - //no bounds, we do +- infinity - Node val = d_qe->getTermDatabase()->getVtsInfinity( pvtn ); - //TODO : rho value for infinity? - if( rr==0 ){ - val = NodeManager::currentNM()->mkNode( UMINUS, val ); - val = Rewriter::rewrite( val ); - } - if( doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){ - return true; - } - } - }else{ - Trace("cbqi-bound") << ( rr==0 ? "Lower" : "Upper" ) << " bounds for " << pv << " (type=" << pvtn << ") : " << std::endl; - int best = -1; - Node best_bound_value[3]; - for( unsigned j=0; jmkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / mbp_coeff[rr][j].getConst() ), value[t] ); - value[t] = Rewriter::rewrite( value[t] ); - } - //check if new best - if( best!=-1 ){ - Assert( !value[t].isNull() && !best_bound_value[t].isNull() ); - if( value[t]!=best_bound_value[t] ){ - Kind k = rr==0 ? GEQ : LEQ; - Node cmp_bound = NodeManager::currentNM()->mkNode( k, value[t], best_bound_value[t] ); - cmp_bound = Rewriter::rewrite( cmp_bound ); - if( cmp_bound!=d_true ){ - new_best = false; - break; - } - } - } - } - Trace("cbqi-bound") << std::endl; - if( new_best ){ - for( unsigned t=0; t<3; t++ ){ - best_bound_value[t] = value[t]; - } - best = j; - } - } - if( best!=-1 ){ - Trace("cbqi-bound") << "...best bound is " << best << " : "; - if( best_bound_value[0]!=d_zero ){ - Trace("cbqi-bound") << "( " << best_bound_value[0] << " * INF ) + "; - } - Trace("cbqi-bound") << best_bound_value[1]; - if( best_bound_value[2]!=d_zero ){ - Trace("cbqi-bound") << " + ( " << best_bound_value[2] << " * DELTA )"; - } - Trace("cbqi-bound") << std::endl; - best_used[rr] = best; - //if using cbqiMidpoint, only add the instance based on one bound if the bound is non-strict - if( !options::cbqiMidpoint() || pvtn.isInteger() || mbp_vts_coeff[rr][1][best].isNull() ){ - Node val = mbp_bounds[rr][best]; - val = getModelBasedProjectionValue( pv, val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], sf.d_theta, - mbp_vts_coeff[rr][0][best], mbp_vts_coeff[rr][1][best] ); - if( !val.isNull() ){ - if( doAddInstantiationInc( pv, val, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, effort ) ){ - return true; - } - } - } - } - } - } - //if not using infinity, use model value of zero - if( !use_inf && mbp_bounds[0].empty() && mbp_bounds[1].empty() ){ - Node val = d_zero; - Node c; //null (one) coefficient - val = getModelBasedProjectionValue( pv, val, true, c, pv_value, d_zero, sf.d_theta, Node::null(), Node::null() ); - if( !val.isNull() ){ - if( doAddInstantiationInc( pv, val, c, 0, sf, effort ) ){ - return true; - } - } - } - if( options::cbqiMidpoint() && !pvtn.isInteger() ){ - Node vals[2]; - bool bothBounds = true; - Trace("cbqi-bound") << "Try midpoint of bounds..." << std::endl; - for( unsigned rr=0; rr<2; rr++ ){ - int best = best_used[rr]; - if( best==-1 ){ - bothBounds = false; - }else{ - vals[rr] = mbp_bounds[rr][best]; - vals[rr] = getModelBasedProjectionValue( pv, vals[rr], rr==0, Node::null(), pv_value, t_values[rr][best], sf.d_theta, - mbp_vts_coeff[rr][0][best], Node::null() ); - } - Trace("cbqi-bound") << "Bound : " << vals[rr] << std::endl; - } - Node val; - if( bothBounds ){ - Assert( !vals[0].isNull() && !vals[1].isNull() ); - if( vals[0]==vals[1] ){ - val = vals[0]; - }else{ - val = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkNode( PLUS, vals[0], vals[1] ), - NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ) ); - val = Rewriter::rewrite( val ); - } - }else{ - if( !vals[0].isNull() ){ - val = NodeManager::currentNM()->mkNode( PLUS, vals[0], d_one ); - val = Rewriter::rewrite( val ); - }else if( !vals[1].isNull() ){ - val = NodeManager::currentNM()->mkNode( MINUS, vals[1], d_one ); - val = Rewriter::rewrite( val ); - } - } - Trace("cbqi-bound") << "Midpoint value : " << val << std::endl; - if( !val.isNull() ){ - if( doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){ - return true; - } - } - } - #ifdef MBP_STRICT_ASSERTIONS - Assert( false ); - #endif - if( options::cbqiNopt() ){ - //try non-optimal bounds (heuristic, may help when nested quantification) ? - Trace("cbqi-bound") << "Try non-optimal bounds..." << std::endl; - for( unsigned r=0; r<2; r++ ){ - int rr = upper_first ? (1-r) : r; - for( unsigned j=0; juseModelValue( this, sf, pv, effort ); if( ( effort>0 || use_model_value || is_cv ) && vinst->allowModelValue( this, sf, pv, effort ) ){ - #ifdef CVC4_ASSERTIONS if( pvtn.isReal() && options::cbqiNestedQE() && !options::cbqiAll() ){ Trace("cbqi-warn") << "Had to resort to model value." << std::endl; @@ -696,10 +318,6 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e Node pv_coeff_m; Trace("cbqi-inst-debug") << "[5] " << i << "...try model value " << mv << std::endl; int new_effort = use_model_value ? effort : 1; -#ifdef MBP_STRICT_ASSERTIONS - //we only resort to values in the case of booleans - Assert( ( pvtn.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() ); -#endif if( doAddInstantiationInc( pv, mv, pv_coeff_m, 0, sf, new_effort ) ){ return true; } @@ -920,9 +538,6 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector } } bool ret = d_out->doAddInstantiation( subs ); -#ifdef MBP_STRICT_ASSERTIONS - Assert( ret ); -#endif return ret; } @@ -1030,66 +645,6 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node } } -Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) { - Node val = t; - Trace("cbqi-bound2") << "Value : " << val << std::endl; - Assert( !e.getType().isInteger() || t.getType().isInteger() ); - Assert( !e.getType().isInteger() || mt.getType().isInteger() ); - //add rho value - //get the value of c*e - Node ceValue = me; - Node new_theta = theta; - if( !c.isNull() ){ - Assert( c.getType().isInteger() ); - ceValue = NodeManager::currentNM()->mkNode( MULT, ceValue, c ); - ceValue = Rewriter::rewrite( ceValue ); - if( new_theta.isNull() ){ - new_theta = c; - }else{ - new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, c ); - new_theta = Rewriter::rewrite( new_theta ); - } - Trace("cbqi-bound2") << "...c*e = " << ceValue << std::endl; - Trace("cbqi-bound2") << "...theta = " << new_theta << std::endl; - } - if( !new_theta.isNull() && e.getType().isInteger() ){ - Node rho; - //if( !mt.getType().isInteger() ){ - //round up/down - //mt = NodeManager::currentNM()->mkNode( - //} - if( isLower ){ - rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt ); - }else{ - rho = NodeManager::currentNM()->mkNode( MINUS, mt, ceValue ); - } - rho = Rewriter::rewrite( rho ); - Trace("cbqi-bound2") << "...rho = " << me << " - " << mt << " = " << rho << std::endl; - Trace("cbqi-bound2") << "..." << rho << " mod " << new_theta << " = "; - rho = NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, rho, new_theta ); - rho = Rewriter::rewrite( rho ); - Trace("cbqi-bound2") << rho << std::endl; - Kind rk = isLower ? PLUS : MINUS; - val = NodeManager::currentNM()->mkNode( rk, val, rho ); - val = Rewriter::rewrite( val ); - Trace("cbqi-bound2") << "(after rho) : " << val << std::endl; - } - if( !inf_coeff.isNull() ){ - Assert( !d_vts_sym[0].isNull() ); - val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, d_vts_sym[0] ) ); - val = Rewriter::rewrite( val ); - } - if( !delta_coeff.isNull() ){ - //create delta here if necessary - if( d_vts_sym[1].isNull() ){ - d_vts_sym[1] = d_qe->getTermDatabase()->getVtsDelta(); - } - val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, d_vts_sym[1] ) ); - val = Rewriter::rewrite( val ); - } - return val; -} - bool CegInstantiator::check() { if( d_qe->getTheoryEngine()->needCheck() ){ Trace("cbqi-engine") << " CEGQI instantiator : wait until all ground theories are finished." << std::endl; @@ -1292,9 +847,7 @@ void CegInstantiator::processAssertions() { addToAuxVarSubstitution( subs_lhs, subs_rhs, r, it->second ); }else{ Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << r << "!!!" << std::endl; -#ifdef MBP_STRICT_ASSERTIONS Assert( false ); -#endif } } @@ -1474,10 +1027,79 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st } } + +Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn ){ + d_closed_enum_type = qe->getTermDatabase()->isClosedEnumerableType( tn ); +} + + +bool Instantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ) { + return ci->doAddInstantiationInc( pv, n, pv_coeff, 0, sf, effort ); +} + + + +Node ArithInstantiator::getModelBasedProjectionValue( CegInstantiator * ci, Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) { + Node val = t; + Trace("cbqi-bound2") << "Value : " << val << std::endl; + Assert( !e.getType().isInteger() || t.getType().isInteger() ); + Assert( !e.getType().isInteger() || mt.getType().isInteger() ); + //add rho value + //get the value of c*e + Node ceValue = me; + Node new_theta = theta; + if( !c.isNull() ){ + Assert( c.getType().isInteger() ); + ceValue = NodeManager::currentNM()->mkNode( MULT, ceValue, c ); + ceValue = Rewriter::rewrite( ceValue ); + if( new_theta.isNull() ){ + new_theta = c; + }else{ + new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, c ); + new_theta = Rewriter::rewrite( new_theta ); + } + Trace("cbqi-bound2") << "...c*e = " << ceValue << std::endl; + Trace("cbqi-bound2") << "...theta = " << new_theta << std::endl; + } + if( !new_theta.isNull() && e.getType().isInteger() ){ + Node rho; + //if( !mt.getType().isInteger() ){ + //round up/down + //mt = NodeManager::currentNM()->mkNode( + //} + if( isLower ){ + rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt ); + }else{ + rho = NodeManager::currentNM()->mkNode( MINUS, mt, ceValue ); + } + rho = Rewriter::rewrite( rho ); + Trace("cbqi-bound2") << "...rho = " << me << " - " << mt << " = " << rho << std::endl; + Trace("cbqi-bound2") << "..." << rho << " mod " << new_theta << " = "; + rho = NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, rho, new_theta ); + rho = Rewriter::rewrite( rho ); + Trace("cbqi-bound2") << rho << std::endl; + Kind rk = isLower ? PLUS : MINUS; + val = NodeManager::currentNM()->mkNode( rk, val, rho ); + val = Rewriter::rewrite( val ); + Trace("cbqi-bound2") << "(after rho) : " << val << std::endl; + } + if( !inf_coeff.isNull() ){ + Assert( !d_vts_sym[0].isNull() ); + val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, d_vts_sym[0] ) ); + val = Rewriter::rewrite( val ); + } + if( !delta_coeff.isNull() ){ + //create delta here if necessary + val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, ci->getQuantifiersEngine()->getTermDatabase()->getVtsDelta() ) ); + val = Rewriter::rewrite( val ); + } + return val; +} + //this isolates the atom into solved form // veq_c * pv <> val + vts_coeff_delta * delta + vts_coeff_inf * inf // ensures val is Int if pv is Int, and val does not contain vts symbols -int CegInstantiator::solve_arith( Node pv, Node atom, Node& veq_c, Node& val, Node& vts_coeff_inf, Node& vts_coeff_delta ) { +int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, Node& veq_c, Node& val, Node& vts_coeff_inf, Node& vts_coeff_delta ) { int ires = 0; Trace("cbqi-inst-debug") << "isolate for " << pv << " in " << atom << std::endl; std::map< Node, Node > msum; @@ -1538,7 +1160,7 @@ int CegInstantiator::solve_arith( Node pv, Node atom, Node& veq_c, Node& val, No if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){ //redo, split integer/non-integer parts bool useCoeff = false; - Integer coeff = d_one.getConst().getNumerator(); + Integer coeff = ci->getQuantifiersEngine()->getTermDatabase()->d_one.getConst().getNumerator(); for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ if( it->first.isNull() || it->first.getType().isInteger() ){ if( !it->second.isNull() ){ @@ -1568,8 +1190,8 @@ int CegInstantiator::solve_arith( Node pv, Node atom, Node& veq_c, Node& val, No if( !vts_coeff[0].isNull() ){ vts_coeff[0] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, rcoeff, vts_coeff[0] ) ); } - realPart = real_part.empty() ? d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) ); - Assert( d_out->isEligibleForInstantiation( realPart ) ); + realPart = real_part.empty() ? ci->getQuantifiersEngine()->getTermDatabase()->d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) ); + Assert( ci->getOutput()->isEligibleForInstantiation( realPart ) ); //re-isolate Trace("cbqi-inst-debug") << "Re-isolate..." << std::endl; ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() ); @@ -1594,7 +1216,415 @@ int CegInstantiator::solve_arith( Node pv, Node atom, Node& veq_c, Node& val, No return ires; } -Node CegInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) { +void ArithInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { + d_vts_sym[0] = ci->getQuantifiersEngine()->getTermDatabase()->getVtsInfinity( d_type, false, false ); + d_vts_sym[1] = ci->getQuantifiersEngine()->getTermDatabase()->getVtsDelta( false, false ); + for( unsigned i=0; i<2; i++ ){ + d_mbp_bounds[i].clear(); + d_mbp_coeff[i].clear(); + for( unsigned j=0; j<2; j++ ){ + d_mbp_vts_coeff[i][j].clear(); + } + d_mbp_lit[i].clear(); + } +} + +bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { + Node eq_lhs = terms[0]; + Node eq_rhs = terms[1]; + Node lhs_coeff = term_coeffs[0]; + Node rhs_coeff = term_coeffs[1]; + //make the same coefficient + if( rhs_coeff!=lhs_coeff ){ + if( !rhs_coeff.isNull() ){ + Trace("cbqi-inst-debug") << "...mult lhs by " << rhs_coeff << std::endl; + eq_lhs = NodeManager::currentNM()->mkNode( MULT, rhs_coeff, eq_lhs ); + eq_lhs = Rewriter::rewrite( eq_lhs ); + } + if( !lhs_coeff.isNull() ){ + Trace("cbqi-inst-debug") << "...mult rhs by " << lhs_coeff << std::endl; + eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff, eq_rhs ); + eq_rhs = Rewriter::rewrite( eq_rhs ); + } + } + Node eq = eq_lhs.eqNode( eq_rhs ); + eq = Rewriter::rewrite( eq ); + Node val; + Node veq_c; + Node vts_coeff_inf; + Node vts_coeff_delta; + //isolate pv in the equality + int ires = solve_arith( ci, pv, eq, veq_c, val, vts_coeff_inf, vts_coeff_delta ); + if( ires!=0 ){ + if( ci->doAddInstantiationInc( pv, val, veq_c, 0, sf, effort ) ){ + return true; + } + } + + return false; +} + +bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { + Trace("cbqi-inst-debug2") << " look at " << lit << std::endl; + Node atom = lit.getKind()==NOT ? lit[0] : lit; + bool pol = lit.getKind()!=NOT; + //arithmetic inequalities and disequalities + if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ){ + Assert( atom.getKind()!=GEQ || atom[1].isConst() ); + Node atom_lhs; + Node atom_rhs; + if( atom.getKind()==GEQ ){ + atom_lhs = atom[0]; + atom_rhs = atom[1]; + }else{ + atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] ); + atom_lhs = Rewriter::rewrite( atom_lhs ); + atom_rhs = ci->getQuantifiersEngine()->getTermDatabase()->d_zero; + } + //must be an eligible term + if( ci->isEligible( atom_lhs ) ){ + //apply substitution to LHS of atom + Node atom_lhs_coeff; + atom_lhs = ci->applySubstitution( d_type, atom_lhs, sf, atom_lhs_coeff ); + if( !atom_lhs.isNull() ){ + if( !atom_lhs_coeff.isNull() ){ + atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) ); + } + } + //if it contains pv, not infinity + if( !atom_lhs.isNull() && ci->hasVariable( atom_lhs, pv ) ){ + Node pv_value = ci->getModelValue( pv ); + Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs ); + //cannot contain infinity? + Trace("cbqi-inst-debug") << "..[3] From assertion : " << atom << ", pol = " << pol << std::endl; + Trace("cbqi-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl; + Node vts_coeff_inf; + Node vts_coeff_delta; + Node val; + Node veq_c; + //isolate pv in the inequality + int ires = solve_arith( ci, pv, satom, veq_c, val, vts_coeff_inf, vts_coeff_delta ); + if( ires!=0 ){ + //disequalities are either strict upper or lower bounds + unsigned rmax = ( atom.getKind()==GEQ || options::cbqiModel() ) ? 1 : 2; + for( unsigned r=0; rmkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); + uval = Rewriter::rewrite( uval ); + }else{ + Assert( d_type.isReal() ); + //now is strict inequality + uires = uires*2; + } + } + }else{ + bool is_upper; + if( options::cbqiModel() ){ + // disequality is a disjunction : only consider the bound in the direction of the model + //first check if there is an infinity... + if( !vts_coeff_inf.isNull() ){ + //coefficient or val won't make a difference, just compare with zero + Trace("cbqi-inst-debug") << "Disequality : check infinity polarity " << vts_coeff_inf << std::endl; + Assert( vts_coeff_inf.isConst() ); + is_upper = ( vts_coeff_inf.getConst().sgn()==1 ); + }else{ + Node rhs_value = ci->getModelValue( val ); + Node lhs_value = pv_value; + if( !veq_c.isNull() ){ + lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, veq_c ); + lhs_value = Rewriter::rewrite( lhs_value ); + } + Trace("cbqi-inst-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl; + Assert( lhs_value!=rhs_value ); + Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value ); + cmp = Rewriter::rewrite( cmp ); + Assert( cmp.isConst() ); + is_upper = ( cmp!=ci->getQuantifiersEngine()->getTermDatabase()->d_true ); + } + }else{ + is_upper = (r==0); + } + Assert( atom.getKind()==EQUAL && !pol ); + if( d_type.isInteger() ){ + uires = is_upper ? -1 : 1; + uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); + uval = Rewriter::rewrite( uval ); + }else{ + Assert( d_type.isReal() ); + uires = is_upper ? -2 : 2; + } + } + Trace("cbqi-bound-inf") << "From " << lit << ", got : "; + if( !veq_c.isNull() ){ + Trace("cbqi-bound-inf") << veq_c << " * "; + } + Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl; + //take into account delta + if( ci->useVtsDelta() && ( uires==2 || uires==-2 ) ){ + if( options::cbqiModel() ){ + Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) ); + if( vts_coeff_delta.isNull() ){ + vts_coeff_delta = delta_coeff; + }else{ + vts_coeff_delta = NodeManager::currentNM()->mkNode( PLUS, vts_coeff_delta, delta_coeff ); + vts_coeff_delta = Rewriter::rewrite( vts_coeff_delta ); + } + }else{ + Node delta = ci->getQuantifiersEngine()->getTermDatabase()->getVtsDelta(); + uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta ); + uval = Rewriter::rewrite( uval ); + } + } + if( options::cbqiModel() ){ + //just store bounds, will choose based on tighest bound + unsigned index = uires>0 ? 0 : 1; + d_mbp_bounds[index].push_back( uval ); + d_mbp_coeff[index].push_back( veq_c ); + Trace("cbqi-inst-debug") << "Store bound " << index << " " << uval << " " << veq_c << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit << std::endl; + for( unsigned t=0; t<2; t++ ){ + d_mbp_vts_coeff[index][t].push_back( t==0 ? vts_coeff_inf : vts_coeff_delta ); + } + d_mbp_lit[index].push_back( lit ); + }else{ + //try this bound + if( ci->doAddInstantiationInc( pv, uval, veq_c, uires>0 ? 1 : -1, sf, effort ) ){ + return true; + } + } + } + } + } + } + } + + + return false; +} + +bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) { + if( options::cbqiModel() ){ + bool use_inf = ci->useVtsInfinity() && ( d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() ); + bool upper_first = false; + if( options::cbqiMinBounds() ){ + upper_first = d_mbp_bounds[1].size() t_values[3]; + Node zero = ci->getQuantifiersEngine()->getTermDatabase()->d_zero; + Node one = ci->getQuantifiersEngine()->getTermDatabase()->d_one; + Node pv_value = ci->getModelValue( pv ); + //try optimal bounds + for( unsigned r=0; r<2; r++ ){ + int rr = upper_first ? (1-r) : r; + best_used[rr] = -1; + if( d_mbp_bounds[rr].empty() ){ + if( use_inf ){ + Trace("cbqi-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << d_type << ")" << std::endl; + //no bounds, we do +- infinity + Node val = ci->getQuantifiersEngine()->getTermDatabase()->getVtsInfinity( d_type ); + //TODO : rho value for infinity? + if( rr==0 ){ + val = NodeManager::currentNM()->mkNode( UMINUS, val ); + val = Rewriter::rewrite( val ); + } + if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){ + return true; + } + } + }else{ + Trace("cbqi-bound") << ( rr==0 ? "Lower" : "Upper" ) << " bounds for " << pv << " (type=" << d_type << ") : " << std::endl; + int best = -1; + Node best_bound_value[3]; + for( unsigned j=0; jgetModelValue( d_mbp_bounds[rr][j] ); + t_values[rr][j] = t_value; + value[1] = t_value; + Trace("cbqi-bound") << value[1]; + }else{ + value[2] = d_mbp_vts_coeff[rr][1][j]; + if( !value[2].isNull() ){ + Trace("cbqi-bound") << " + ( " << value[2] << " * DELTA )"; + }else{ + value[2] = zero; + } + } + //multiply by coefficient + if( value[t]!=zero && !d_mbp_coeff[rr][j].isNull() ){ + Assert( d_mbp_coeff[rr][j].isConst() ); + value[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / d_mbp_coeff[rr][j].getConst() ), value[t] ); + value[t] = Rewriter::rewrite( value[t] ); + } + //check if new best + if( best!=-1 ){ + Assert( !value[t].isNull() && !best_bound_value[t].isNull() ); + if( value[t]!=best_bound_value[t] ){ + Kind k = rr==0 ? GEQ : LEQ; + Node cmp_bound = NodeManager::currentNM()->mkNode( k, value[t], best_bound_value[t] ); + cmp_bound = Rewriter::rewrite( cmp_bound ); + if( cmp_bound!=ci->getQuantifiersEngine()->getTermDatabase()->d_true ){ + new_best = false; + break; + } + } + } + } + Trace("cbqi-bound") << std::endl; + if( new_best ){ + for( unsigned t=0; t<3; t++ ){ + best_bound_value[t] = value[t]; + } + best = j; + } + } + if( best!=-1 ){ + Trace("cbqi-bound") << "...best bound is " << best << " : "; + if( best_bound_value[0]!=zero ){ + Trace("cbqi-bound") << "( " << best_bound_value[0] << " * INF ) + "; + } + Trace("cbqi-bound") << best_bound_value[1]; + if( best_bound_value[2]!=zero ){ + Trace("cbqi-bound") << " + ( " << best_bound_value[2] << " * DELTA )"; + } + Trace("cbqi-bound") << std::endl; + best_used[rr] = best; + //if using cbqiMidpoint, only add the instance based on one bound if the bound is non-strict + if( !options::cbqiMidpoint() || d_type.isInteger() || d_mbp_vts_coeff[rr][1][best].isNull() ){ + Node val = d_mbp_bounds[rr][best]; + val = getModelBasedProjectionValue( ci, pv, val, rr==0, d_mbp_coeff[rr][best], pv_value, t_values[rr][best], sf.d_theta, + d_mbp_vts_coeff[rr][0][best], d_mbp_vts_coeff[rr][1][best] ); + if( !val.isNull() ){ + if( ci->doAddInstantiationInc( pv, val, d_mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, effort ) ){ + return true; + } + } + } + } + } + } + //if not using infinity, use model value of zero + if( !use_inf && d_mbp_bounds[0].empty() && d_mbp_bounds[1].empty() ){ + Node val = zero; + Node c; //null (one) coefficient + val = getModelBasedProjectionValue( ci, pv, val, true, c, pv_value, zero, sf.d_theta, Node::null(), Node::null() ); + if( !val.isNull() ){ + if( ci->doAddInstantiationInc( pv, val, c, 0, sf, effort ) ){ + return true; + } + } + } + if( options::cbqiMidpoint() && !d_type.isInteger() ){ + Node vals[2]; + bool bothBounds = true; + Trace("cbqi-bound") << "Try midpoint of bounds..." << std::endl; + for( unsigned rr=0; rr<2; rr++ ){ + int best = best_used[rr]; + if( best==-1 ){ + bothBounds = false; + }else{ + vals[rr] = d_mbp_bounds[rr][best]; + vals[rr] = getModelBasedProjectionValue( ci, pv, vals[rr], rr==0, Node::null(), pv_value, t_values[rr][best], sf.d_theta, + d_mbp_vts_coeff[rr][0][best], Node::null() ); + } + Trace("cbqi-bound") << "Bound : " << vals[rr] << std::endl; + } + Node val; + if( bothBounds ){ + Assert( !vals[0].isNull() && !vals[1].isNull() ); + if( vals[0]==vals[1] ){ + val = vals[0]; + }else{ + val = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkNode( PLUS, vals[0], vals[1] ), + NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ) ); + val = Rewriter::rewrite( val ); + } + }else{ + if( !vals[0].isNull() ){ + val = NodeManager::currentNM()->mkNode( PLUS, vals[0], one ); + val = Rewriter::rewrite( val ); + }else if( !vals[1].isNull() ){ + val = NodeManager::currentNM()->mkNode( MINUS, vals[1], one ); + val = Rewriter::rewrite( val ); + } + } + Trace("cbqi-bound") << "Midpoint value : " << val << std::endl; + if( !val.isNull() ){ + if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){ + return true; + } + } + } + //generally should not make it to this point FIXME: write proper assertion + //Assert( ( ci->hasNestedQuantification() && !options::cbqiNestedQE() ) || options::cbqiAll() ); + + if( options::cbqiNopt() ){ + //try non-optimal bounds (heuristic, may help when nested quantification) ? + Trace("cbqi-bound") << "Try non-optimal bounds..." << std::endl; + for( unsigned r=0; r<2; r++ ){ + int rr = upper_first ? (1-r) : r; + for( unsigned j=0; jdoAddInstantiationInc( pv, val, d_mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, effort ) ){ + return true; + } + } + } + } + } + } + } + return false; +} + +bool ArithInstantiator::needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, unsigned effort ) { + return !sf.d_has_coeff.empty(); +} + +bool ArithInstantiator::postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, unsigned effort ) { + return true; +} + +void DtInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { + +} + +Node DtInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) { Trace("cbqi-inst-debug2") << "Solve dt : " << v << " " << a << " " << b << " " << sa << " " << sb << std::endl; Node ret; if( !a.isNull() && a==v ){ @@ -1635,47 +1665,6 @@ Node CegInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) { return ret; } - - - -Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn ){ - d_closed_enum_type = qe->getTermDatabase()->isClosedEnumerableType( tn ); -} - - -bool Instantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ) { - return ci->doAddInstantiationInc( pv, n, pv_coeff, 0, sf, effort ); -} - - -void ArithInstantiator::reset( Node pv, unsigned effort ) { - -} - -bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { - return false; -} - -bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { - return false; -} - -bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) { - return false; -} - -bool ArithInstantiator::needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, unsigned effort ) { - return !sf.d_has_coeff.empty(); -} - -bool ArithInstantiator::postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, unsigned effort ) { - return true; -} - -void DtInstantiator::reset( Node pv, unsigned effort ) { - -} - bool DtInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { Trace("cbqi-inst-debug") << "[2] try based on constructors in equivalence class." << std::endl; //[2] look in equivalence class for a constructor @@ -1709,10 +1698,17 @@ bool DtInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, No } bool DtInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { + Node val = solve_dt( pv, terms[0], terms[1], terms[0], terms[1] ); + if( !val.isNull() ){ + Node veq_c; + if( ci->doAddInstantiationInc( pv, val, veq_c, 0, sf, effort ) ){ + return true; + } + } return false; } -void EprInstantiator::reset( Node pv, unsigned effort ) { +void EprInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { d_equal_terms.clear(); } @@ -1827,3 +1823,4 @@ bool BvInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Nod return false; } + diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 259c604dc..088aceeda 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -88,7 +88,6 @@ private: Node d_true; bool d_use_vts_delta; bool d_use_vts_inf; - Node d_vts_sym[2]; //program variable contains cache std::map< Node, std::map< Node, bool > > d_prog_var; std::map< Node, bool > d_inelig; @@ -125,24 +124,13 @@ private: void collectCeAtoms( Node n, std::map< Node, bool >& visited ); //for adding instantiations during check void computeProgVars( Node n ); - // is eligible - bool isEligible( Node n ); // effort=0 : do not use model value, 1: use model value, 2: one must use model value bool doAddInstantiation( SolvedForm& sf, unsigned i, unsigned effort ); bool processInstantiationCoeff( SolvedForm& sf ); bool doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars ); - Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, Node& pv_coeff, bool try_coeff = true ) { - return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, sf.d_vars, pv_coeff, try_coeff ); - } - Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff, - std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ); - Node getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ); void processAssertions(); void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ); -private: - int solve_arith( Node v, Node atom, Node & veq_c, Node & val, Node& vts_coeff_inf, Node& vts_coeff_delta ); - Node solve_dt( Node v, Node a, Node b, Node sa, Node sb ); public: CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true ); virtual ~CegInstantiator(); @@ -152,7 +140,8 @@ public: void presolve( Node q ); //register the counterexample lemma (stored in lems), modify vector void registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ); - + //output + CegqiOutput * getOutput() { return d_out; } //interface for instantiators public: //get quantifiers engine @@ -163,6 +152,18 @@ public: Node getModelValue( Node n ); unsigned getNumCEAtoms() { return d_ce_atoms.size(); } Node getCEAtom( unsigned i ) { return d_ce_atoms[i]; } + // is eligible + bool isEligible( Node n ); + // has variable + bool hasVariable( Node n, Node pv ); + Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, Node& pv_coeff, bool try_coeff = true ) { + return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, sf.d_vars, pv_coeff, try_coeff ); + } + Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff, + std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ); + bool useVtsDelta() { return d_use_vts_delta; } + bool useVtsInfinity() { return d_use_vts_inf; } + bool hasNestedQuantification() { return d_is_nested_quant; } }; @@ -176,7 +177,7 @@ protected: public: Instantiator( QuantifiersEngine * qe, TypeNode tn ); virtual ~Instantiator(){} - virtual void reset( Node pv, unsigned effort ) {} + virtual void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {} //called when pv_coeff * pv = n, and n is eligible for instantiation virtual bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ); @@ -214,11 +215,17 @@ public: class ArithInstantiator : public Instantiator { private: - + Node d_vts_sym[2]; + std::vector< Node > d_mbp_bounds[2]; + std::vector< Node > d_mbp_coeff[2]; + std::vector< Node > d_mbp_vts_coeff[2][2]; + std::vector< Node > d_mbp_lit[2]; + int solve_arith( CegInstantiator * ci, Node v, Node atom, Node & veq_c, Node & val, Node& vts_coeff_inf, Node& vts_coeff_delta ); + Node getModelBasedProjectionValue( CegInstantiator * ci, Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ); public: ArithInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} virtual ~ArithInstantiator(){} - void reset( Node pv, unsigned effort ); + void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ); bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } @@ -230,10 +237,12 @@ public: }; class DtInstantiator : public Instantiator { +private: + Node solve_dt( Node v, Node a, Node b, Node sa, Node sb ); public: DtInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} virtual ~DtInstantiator(){} - void reset( Node pv, unsigned effort ); + void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ); bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ); @@ -250,7 +259,7 @@ private: public: EprInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} virtual ~EprInstantiator(){} - void reset( Node pv, unsigned effort ); + void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ); bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ); std::string identify() const { return "Epr"; } diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 522f4dfce..31831d73b 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -108,7 +108,7 @@ void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) { } Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl; - if( d_mg->isValid() ){ + if( d_mg->isValid() && options::qcfEagerCheckRd() ){ //optimization : record variable argument positions for terms that must be matched std::vector< TNode > vars; //TODO: revisit this, makes QCF faster, but misses conflicts due to caring about paths that may not be relevant (starExec jobs 14136/14137) diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 3bf7749a4..917402106 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1138,12 +1138,13 @@ Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){ if( containsQuantifiers( n ) ){ if( topLevel && options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL && ( n.getKind()==AND || ( n.getKind()==NOT && n[0].getKind()==OR ) ) ){ std::vector< Node > children; - for( unsigned i=0; imkNode( AND, children ); }else if( n.getKind()==NOT ){ diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 6608ae22d..43c77973f 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -86,7 +86,9 @@ TESTS = \ z3.620661-no-fv-trigger.smt2 \ bug_743.smt2 \ quaternion_ds1_symm_0428.fof.smt2 \ - bug749-rounding.smt2 + bug749-rounding.smt2 \ + RNDPRE_4_1-dd-nqe.smt2 \ + mix-complete-strat.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/RNDPRE_4_1-dd-nqe.smt2 b/test/regress/regress0/quantifiers/RNDPRE_4_1-dd-nqe.smt2 new file mode 100644 index 000000000..6379d6cec --- /dev/null +++ b/test/regress/regress0/quantifiers/RNDPRE_4_1-dd-nqe.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --cbqi-nested-qe +; EXPECT: unsat +(set-logic LRA) + +(declare-fun c () Real) + +(assert +(forall ((?x2 Real)) +(exists ((?x3 Real)) +(and +(forall ((?x4 Real)) (or +(not (>= ?x4 4)) +(and (> c (+ ?x2 ?x3)) (> (+ c ?x3 ?x4) 0))) ) +(not (> (+ c ?x2 ?x3) 0)) ) +)) ) + +(check-sat) +(exit) diff --git a/test/regress/regress0/quantifiers/mix-complete-strat.smt2 b/test/regress/regress0/quantifiers/mix-complete-strat.smt2 new file mode 100644 index 000000000..c2209f697 --- /dev/null +++ b/test/regress/regress0/quantifiers/mix-complete-strat.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-logic UFLIA) +(set-info :status sat) + +(declare-sort U 0) +(declare-fun P (U) Bool) + +(assert (forall ((x U)) (P x))) + +(declare-fun u () U) +(assert (P u)) + +(declare-const a Int) +(declare-const b Int) +(assert (forall ((x Int)) (or (> x a) (< x b)))) + +(check-sat) -- cgit v1.2.3 From fe72120c20dc211c7fdf02af7ff1a89527366a47 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Wed, 28 Sep 2016 12:03:08 -0400 Subject: Fix the merge of kbansal/card branch (2039eab). A bug was introduced in the cleanup process as preparation for the merge (theory_sets_private.cpp, lines 2502-2508 in this commit). --- src/theory/sets/theory_sets_private.cpp | 49 +++++++++++++++++++--- src/theory/sets/theory_sets_private.h | 2 +- test/regress/regress0/sets/Makefile.am | 3 +- test/regress/regress0/sets/card-vc6-minimized.smt2 | 15 +++++++ 4 files changed, 62 insertions(+), 7 deletions(-) create mode 100644 test/regress/regress0/sets/card-vc6-minimized.smt2 (limited to 'test') diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index ec6bb7fcd..6fb90fea3 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -853,6 +853,7 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) //processCard2 begin if(Debug.isOn("sets-card")) { + print_graph(true); for(CDNodeSet::const_iterator it = d_V.begin(); it != d_V.end(); ++it) { Node n = nm->mkNode(kind::CARD, *it); Debug("sets-card") << "[sets-card] " << n << " = "; @@ -1040,7 +1041,7 @@ Node mkAnd(const std::vector& conjunctions) { if (t.getKind() == kind::AND) { for(TNode::iterator child_it = t.begin(); child_it != t.end(); ++child_it) { - Assert((*child_it).getKind() != kind::AND); + // Assert((*child_it).getKind() != kind::AND); all.insert(*child_it); } } @@ -1436,7 +1437,11 @@ Node TheorySetsPrivate::explain(TNode literal) Unhandled(); } - return mkAnd(assumptions); + if(assumptions.size()) { + return mkAnd(assumptions); + } else { + return d_trueNode; + } } bool TheorySetsPrivate::lemma(Node n, SetsLemmaTag t) @@ -2333,7 +2338,8 @@ void TheorySetsPrivate::merge_nodes(std::set leaves1, std::set lea } -void TheorySetsPrivate::print_graph() { +void TheorySetsPrivate::print_graph(bool printmodel) { + NodeManager* nm = NodeManager::currentNM(); std::string tag = "sets-graph"; if(Trace.isOn("sets-graph")) { Trace(tag) << "[sets-graph] Graph : " << std::endl; @@ -2358,13 +2364,38 @@ void TheorySetsPrivate::print_graph() { oss << "digraph G { "; for(CDNodeSet::const_iterator it = d_V.begin(); it != d_V.end(); ++it) { TNode v = *it; + + std::ostringstream v_oss; + v_oss << v; + if(printmodel) + { + Node n = nm->mkNode(kind::CARD, v); + if((Rewriter::rewrite(n)).isConst()) { + v_oss << " " << (Rewriter::rewrite(n)); + } else { + v_oss << " " << d_external.d_valuation.getModelValue(n); + } + } + if(d_E.find(v) != d_E.end()) { BOOST_FOREACH(TNode w, d_E[v].get()) { + + std::ostringstream w_oss; + w_oss << w; + if(printmodel) { + Node n = nm->mkNode(kind::CARD, w); + if((Rewriter::rewrite(n)).isConst()) { + w_oss << " " << (Rewriter::rewrite(n)); + } else { + w_oss << " " << d_external.d_valuation.getModelValue(n); + } + } + //oss << v.getId() << " -> " << w.getId() << "; "; - oss << "\"" << v << "\" -> \"" << w << "\"; "; + oss << "\"" << v_oss.str() << "\" -> \"" << w_oss.str() << "\"; "; } } else { - oss << "\"" << v << "\";"; + oss << "\"" << v_oss.str() << "\";"; } } oss << "}"; @@ -2468,6 +2499,14 @@ void TheorySetsPrivate::processCard2(Theory::Effort level) { NodeManager* nm = NodeManager::currentNM(); + if(options::setsGuessEmpty() == 0) { + Trace("sets-guess-empty") << "[sets-guess-empty] Generating lemmas before introduce." << std::endl; + guessLeavesEmptyLemmas(); + if(d_newLemmaGenerated) { + return; + } + } + // Introduce for(CDNodeSet::const_iterator it = d_cardTerms.begin(); it != d_cardTerms.end(); ++it) { diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 71a6d9b2d..049e95786 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -280,7 +280,7 @@ private: std::set get_leaves(Node vertex1, Node vertex2); std::set get_leaves(Node vertex1, Node vertex2, Node vertex3); std::set non_empty(std::set vertices); - void print_graph(); + void print_graph(bool printmodel=false); context::CDQueue < std::pair > d_graphMergesPending; context::CDList d_allSetEqualitiesSoFar; Node eqSoFar(); diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index 558d170d7..2f36cc188 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -64,7 +64,8 @@ TESTS = \ union-1b.smt2 \ union-2.smt2 \ dt-simp-mem.smt2 \ - card3-ground.smt2 + card3-ground.smt2 \ + card-vc6-minimized.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/sets/card-vc6-minimized.smt2 b/test/regress/regress0/sets/card-vc6-minimized.smt2 new file mode 100644 index 000000000..d7f4bdf1e --- /dev/null +++ b/test/regress/regress0/sets/card-vc6-minimized.smt2 @@ -0,0 +1,15 @@ +; EXPECT: unsat +(set-logic QF_UFLIAFS) +(declare-fun x () Int) +(declare-fun c () (Set Int)) +(declare-fun alloc0 () (Set Int)) +(declare-fun alloc1 () (Set Int)) +(declare-fun alloc2 () (Set Int)) +(assert +(and (member x c) + (<= (card (setminus alloc1 alloc0)) 1) + (<= (card (setminus alloc2 alloc1)) + (card (setminus c (singleton x)))) + (> (card (setminus alloc2 alloc0)) (card c)) +)) +(check-sat) -- cgit v1.2.3