diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-23 14:04:32 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-23 14:04:32 -0500 |
| commit | df7333de4436d846da70857e61cda411d22d02ba (patch) | |
| tree | b3fe8a20bd3bf89936827eaea0341e049b4116f6 /test | |
| parent | dd515b59583cba1afed8fbb583f8012a214feaad (diff) | |
Simplify auxiliary variable handling in CEGQI (#4141)
Fixes #3849 and fixes #4062.
Overall, the effect of this PR is that CEGQI will generate better instantiations more frequently for quantified formulas that involve the introduction of auxiliary variables.
In CEGQI, auxiliary variables introduced in CEX lemmas must be given special treatment (since the instantiations should not involve them, thus they must be solved for as well). Previously, auxiliary variables that are introduced as parts of CEX lemmas were currently assumed to be:
(1) Only occurring from ITE removal, e.g. s[(ite C t1 t2]) ---> s[k] ^ ite( C, k = t1, k = t2 )
(2) Always trivially solvable by looking at which literal was asserted (k = t1 or k = t2).
Both of these assumption do not hold in general (aux variables can come from other kinds of terms e.g. choice functions, and the user can force options that rewrite arithmetic equalities to inequalities).
This makes auxiliary variable handling in CEGQI more robust by treating auxiliary variables as standard variables. Effectively, this means that the entire procedure for determining instantiations is run for auxiliary variables. This PR removes the specific hacks that were used previously that were based on the assumptions above.
Additionally, #3849 triggered a second issue: SyGuS solution reconstruction that involves auxiliary variables that are introduced as part of instantiation lemmas should not be considered valid solutions. Previously, only a warning was given.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2 | 9 |
2 files changed, 10 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index cd83ef3d1..4cd3c70d2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1502,6 +1502,7 @@ set(regress_1_tests regress1/quantifiers/issue3765.smt2 regress1/quantifiers/issue3765-quant-dd.smt2 regress1/quantifiers/issue4021-ind-opts.smt2 + regress1/quantifiers/issue4062-cegqi-aux.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lra-vts-inf.smt2 diff --git a/test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2 b/test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2 new file mode 100644 index 000000000..0296c978c --- /dev/null +++ b/test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --arith-rewrite-equalities --global-negate --no-check-models +; EXPECT: sat +(set-logic NIA) +(set-option :arith-rewrite-equalities true) +(set-option :global-negate true) +(set-info :status sat) +(declare-const i5 Int) +(assert (= 562 (abs i5))) +(check-sat) |