diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-23 15:53:48 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-01-23 15:53:48 -0600 |
| commit | dd29958ff0c78c099f540f080e455d843caf1c6b (patch) | |
| tree | 4f3d6edfdb60463eff7c22001220adddebd30b81 | |
| parent | fd88b18c0db55eb63d0cd0454b19810a8abee789 (diff) | |
Fix trivial solve method for single invocation (#3650)
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 2 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/issue3654.sy | 24 |
3 files changed, 26 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index e36047e67..b6750c5da 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -676,7 +676,7 @@ bool CegSingleInv::solveTrivial(Node q) } } // if we solved all arguments - if (args.empty()) + if (args.empty() && body.isConst() && !body.getConst<bool>()) { Trace("cegqi-si-trivial-solve") << q << " is trivially solvable by substitution " << vars << " -> " diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 65d7f2b31..518e3a889 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1787,6 +1787,7 @@ set(regress_1_tests regress1/sygus/issue3580.sy regress1/sygus/issue3634.smt2 regress1/sygus/issue3635.smt2 + regress1/sygus/issue3654.sy regress1/sygus/large-const-simp.sy regress1/sygus/let-bug-simp.sy regress1/sygus/list-head-x.sy diff --git a/test/regress/regress1/sygus/issue3654.sy b/test/regress/regress1/sygus/issue3654.sy new file mode 100644 index 000000000..12949c55a --- /dev/null +++ b/test/regress/regress1/sygus/issue3654.sy @@ -0,0 +1,24 @@ +; EXPECT: unknown +; COMMAND-LINE: --sygus-out=status +(set-logic ALL) +(synth-fun inv-fn ((i Int) (x (Array Int Int)) (c Int)) Bool) + +(define-fun init-fn ((i Int) (x (Array Int Int)) (c Int)) Bool + (and (= i 0) + (= (select x 10) c))) + +(define-fun post-fn ((i Int) (x (Array Int Int))(c Int)) Bool + (exists ((index Int)) (and (= (select x index) c) + (forall ((index2 Int)) (=> (< index2 index) (not (= (select x index) c)))) + ))) + +(declare-var x (Array Int Int)) +(declare-var x! (Array Int Int)) +(declare-var i Int) +(declare-var i! Int) +(declare-var c Int) + + +(constraint (=> (init-fn i x c) (inv-fn i x c))) +(constraint (=> (inv-fn i x c) (post-fn i x c))) +(check-synth) |