Statistics on instantiations per quantified formula. (#4719)

This adds a new print format for instantiations --print-instantiations=num, which prints the total number of instantations of quantified formulas. This count is user-context-dependent, which is in sync with the existing print-instantiation format (list).

It also simplifies and improves printing of Instantiation Tries.

5 files changed, 19 insertions, 5 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c5048ae63..0449107af 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1603,6 +1603,7 @@ set(regress_1_tests
   regress1/quantifiers/qcft-smtlib3dbc51.smt2
   regress1/quantifiers/qe-partial.smt2
   regress1/quantifiers/qe.smt2
+  regress1/quantifiers/qid.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 9221a2abc..94dbe9f88 100644
--- a/test/regress/regress1/quantifiers/dump-inst-i.smt2
+++ b/test/regress/regress1/quantifiers/dump-inst-i.smt2
@@ -4,14 +4,14 @@
 ; EXPECT: (skolem (forall ((x Int)) (or (P x) (Q x)) )
 ; EXPECT:   ( skv_TERM )
 ; EXPECT: )
-; EXPECT: (instantiation (forall ((x Int)) (P x) )
+; EXPECT: (instantiations (forall ((x Int)) (P x) )
 ; EXPECT:   ( skv_TERM )
 ; EXPECT: )
 ; EXPECT: unsat
 ; EXPECT: (skolem (forall ((x Int)) (or (P x) (R x)) )
 ; EXPECT:   ( skv_TERM )
 ; EXPECT: )
-; EXPECT: (instantiation (forall ((x Int)) (P x) )
+; EXPECT: (instantiations (forall ((x Int)) (P x) )
 ; EXPECT:   ( skv_TERM )
 ; EXPECT: )
 (set-logic UFLIA)
diff --git a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 b/test/regress/regress1/quantifiers/dump-inst-proof.smt2
index 674950c34..2995f7682 100644
--- a/test/regress/regress1/quantifiers/dump-inst-proof.smt2
+++ b/test/regress/regress1/quantifiers/dump-inst-proof.smt2
@@ -1,10 +1,10 @@
 ; REQUIRES: proof
 ; COMMAND-LINE: --dump-instantiations --proof
 ; EXPECT: unsat
-; EXPECT: (instantiation (forall ((x Int)) (or (P x) (Q x)) )
+; EXPECT: (instantiations (forall ((x Int)) (or (P x) (Q x)) )
 ; EXPECT:   ( 2 )
 ; EXPECT: )
-; EXPECT: (instantiation (forall ((x Int)) (or (not (S x)) (not (Q x))) )
+; EXPECT: (instantiations (forall ((x Int)) (or (not (S x)) (not (Q x))) )
 ; EXPECT:   ( 2 )
 ; EXPECT: )
 (set-logic UFLIA)
diff --git a/test/regress/regress1/quantifiers/dump-inst.smt2 b/test/regress/regress1/quantifiers/dump-inst.smt2
index 38e60d4db..3a8bc4b9c 100644
--- a/test/regress/regress1/quantifiers/dump-inst.smt2
+++ b/test/regress/regress1/quantifiers/dump-inst.smt2
@@ -4,7 +4,7 @@
 ; EXPECT: (skolem (forall ((x Int)) (or (P x) (Q x)) )
 ; EXPECT:   ( skv_TERM )
 ; EXPECT: )
-; EXPECT: (instantiation (forall ((x Int)) (P x) )
+; EXPECT: (instantiations (forall ((x Int)) (P x) )
 ; EXPECT:   ( skv_TERM )
 ; EXPECT: )
 (set-logic UFLIA)
diff --git a/test/regress/regress1/quantifiers/qid.smt2 b/test/regress/regress1/quantifiers/qid.smt2
new file mode 100644
index 000000000..05639337d
--- /dev/null
+++ b/test/regress/regress1/quantifiers/qid.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --dump-instantiations --print-inst=num --no-print-inst-full
+; EXPECT: unsat
+; EXPECT: (num-instantiations myQuantP 1)
+; EXPECT: (num-instantiations myQuantQ 7)
+
+(set-logic UFLIA)
+(declare-fun P (Int) Bool)
+(declare-fun Q (Int) Bool)
+(assert (forall ((x Int)) (! (P x) :qid |myQuantP|)))
+(assert (forall ((x Int)) (! (=> (Q x) (Q (+ x 1))) :qid |myQuantQ|)))
+(assert (Q 0))
+(assert (or (not (P 5)) (not (Q 7))))
+(check-sat)