diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-14 01:41:24 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-13 23:41:24 -0700 |
| commit | 1cd3c3c5dad84093aa6b2db164798c8fff473fec (patch) | |
| tree | 2cb4fe22f3ca9c97cf93c77aa50c5d08b30dc7d0 /test | |
| parent | 34043bdcd93860969cfd9e87c683340175c640b9 (diff) | |
Debug instantiations output (#4739)
This prints # instantiations per round (during solving) for each quantified formula with `--debug-inst`, giving output like this:
```
(num-instantiations myQuant1 1)
(num-instantiations myQuant2 1)
unsat
```
It also changes the default value of print-inst-full to match the behavior of unsat-cores vs unsat-cores-full (by default, nameless quantifiers are ignored).
It fixes an issue with qid, where mkVar was accidentally used instead of mkConst, leading to assertion failures in debug. Marking major since this fixes debug regress1.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/dump-inst-i.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/dump-inst-proof.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/dump-inst.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/qid-debug-inst.smt2 | 13 |
5 files changed, 17 insertions, 3 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5072e5a17..4e79b5dbe 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1605,6 +1605,7 @@ set(regress_1_tests regress1/quantifiers/qe-partial.smt2 regress1/quantifiers/qe.smt2 regress1/quantifiers/qid.smt2 + regress1/quantifiers/qid-debug-inst.smt2 regress1/quantifiers/quant-wf-int-ind.smt2 regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 regress1/quantifiers/recfact.cvc diff --git a/test/regress/regress1/quantifiers/dump-inst-i.smt2 b/test/regress/regress1/quantifiers/dump-inst-i.smt2 index 94dbe9f88..8a9f10ea7 100644 --- a/test/regress/regress1/quantifiers/dump-inst-i.smt2 +++ b/test/regress/regress1/quantifiers/dump-inst-i.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --dump-instantiations --incremental +; COMMAND-LINE: --dump-instantiations --incremental --print-inst-full ; SCRUBBER: sed -e 's/skv_.* )$/skv_TERM )/' ; EXPECT: unsat ; EXPECT: (skolem (forall ((x Int)) (or (P x) (Q x)) ) diff --git a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 b/test/regress/regress1/quantifiers/dump-inst-proof.smt2 index 2995f7682..9edc4df2b 100644 --- a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 +++ b/test/regress/regress1/quantifiers/dump-inst-proof.smt2 @@ -1,5 +1,5 @@ ; REQUIRES: proof -; COMMAND-LINE: --dump-instantiations --proof +; COMMAND-LINE: --dump-instantiations --proof --print-inst-full ; EXPECT: unsat ; EXPECT: (instantiations (forall ((x Int)) (or (P x) (Q x)) ) ; EXPECT: ( 2 ) diff --git a/test/regress/regress1/quantifiers/dump-inst.smt2 b/test/regress/regress1/quantifiers/dump-inst.smt2 index 3a8bc4b9c..d15025900 100644 --- a/test/regress/regress1/quantifiers/dump-inst.smt2 +++ b/test/regress/regress1/quantifiers/dump-inst.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --dump-instantiations +; COMMAND-LINE: --dump-instantiations --print-inst-full ; SCRUBBER: sed -e 's/skv_.* )$/skv_TERM )/' ; EXPECT: unsat ; EXPECT: (skolem (forall ((x Int)) (or (P x) (Q x)) ) diff --git a/test/regress/regress1/quantifiers/qid-debug-inst.smt2 b/test/regress/regress1/quantifiers/qid-debug-inst.smt2 new file mode 100644 index 000000000..6b987a3a3 --- /dev/null +++ b/test/regress/regress1/quantifiers/qid-debug-inst.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --debug-inst +; EXPECT: (num-instantiations myQuant1 1) +; EXPECT: (num-instantiations myQuant2 1) +; EXPECT: unsat + +(set-logic UFLIA) +(declare-fun P (Int) Bool) +(declare-fun Q (Int) Bool) +(assert (forall ((x Int)) (! (P x) :qid |myQuant1|))) +(assert (forall ((x Int)) (! (=> (P x) (Q x)) :qid |myQuant2|))) +(assert (P 5)) +(assert (not (Q 5))) +(check-sat) |