diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-14 11:38:04 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-14 11:38:04 -0600 |
| commit | af7c14503f4600559a104cd97181448a07837dd0 (patch) | |
| tree | 5b43bfa56f58dd56a8dbf33bdfc9a81935297e35 /test/regress | |
| parent | c51920039f10864f813ae1a4b4e765264a322256 (diff) | |
Properly implement datatype selector triggers (#5624)
This ensures that datatype selectors are properly handled as triggers in E-matching.
This is challenging since selectors in quantified formulas are of kind APPLY_SELECTOR but are theory-preprocessed to APPLY_SELECTOR_TOTAL/APPLY_UF. Hence, we must match on 2 possible operators, and ones that do not match the operator of the trigger. This adds a custom candidate generator for this case.
It also removes a deprecated option that is no longer used (in part due to our use of shared selectors).
This is in preparation for further work on optimizing cvc4 on benchmarks from Facebook.
Note that there is not a convienient way to call expandDefinitions currently (which is required to get the proper operators to match). This PR calls smt::getCurrentSmtEngine() to do this, although we should find a better solution soon, e.g. adding expandDefinitions to the rewriter.
FYI @barrettcw
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/selector-trigger.smt2 | 14 |
2 files changed, 15 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a5adf4d9c..b32e0799d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -870,6 +870,7 @@ set(regress_0_tests regress0/quantifiers/qcf-rel-dom-opt.smt2 regress0/quantifiers/quant-model-simplification.smt2 regress0/quantifiers/rew-to-scala.smt2 + regress0/quantifiers/selector-trigger.smt2 regress0/quantifiers/simp-len.smt2 regress0/quantifiers/simp-typ-test.smt2 regress0/quantifiers/sygus-inst-nia-psyco-060.smt2 diff --git a/test/regress/regress0/quantifiers/selector-trigger.smt2 b/test/regress/regress0/quantifiers/selector-trigger.smt2 new file mode 100644 index 000000000..4e5cf0ecf --- /dev/null +++ b/test/regress/regress0/quantifiers/selector-trigger.smt2 @@ -0,0 +1,14 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-datatypes ((T 0)) ( + ((Z) (Y (y Int))))) + +(declare-fun b () T) +(declare-fun a () Int) + +(declare-fun P (Int) Bool) +(assert (P (y b))) + +(assert (forall ((x T)) (not (P (y x))))) + +(check-sat) |