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.

10 files changed, 59 insertions, 10 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 2b47570ed..b62468cdd 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1992,9 +1992,17 @@ header = "options/quantifiers_options.h"
   category   = "regular"
   long       = "print-inst-full"
   type       = "bool"
-  default    = "true"
+  default    = "false"
   help       = "print instantiations for formulas that do not have given identifiers"
 
+[[option]]
+  name       = "debugInst"
+  category   = "regular"
+  long       = "debug-inst"
+  type       = "bool"
+  default    = "false"
+  help       = "print instantiations during solving (for debugging)"
+
 ### SyGuS instantiation options
 
 [[option]]
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 62ea4e4fa..b88dc70b6 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1901,7 +1901,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
   | tok=( ATTRIBUTE_QUANTIFIER_ID_TOK ) symbolicExpr[sexpr]
     {
       api::Sort boolType = SOLVER->getBooleanSort();
-      api::Term avar = SOLVER->mkVar(boolType, sexpr.toString());
+      api::Term avar = SOLVER->mkConst(boolType, sexpr.toString());
       attr = std::string(":qid");
       retExpr = MK_TERM(api::INST_ATTRIBUTE, avar);
       Command* c = new SetUserAttributeCommand("qid", avar.getExpr());
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index deed76fc9..c9048fc95 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -783,7 +783,7 @@ Node Instantiate::getInstantiatedConjunction(Node q)
   return ret;
 }
 
-void Instantiate::debugPrint()
+void Instantiate::debugPrint(std::ostream& out)
 {
   // debug information
   if (Trace.isOn("inst-per-quant-round"))
@@ -795,6 +795,20 @@ void Instantiate::debugPrint()
       d_temp_inst_debug[i.first] = 0;
     }
   }
+  if (options::debugInst())
+  {
+    bool isFull = options::printInstFull();
+    for (std::pair<const Node, uint32_t>& i : d_temp_inst_debug)
+    {
+      std::stringstream ss;
+      if (!printQuant(i.first, ss, isFull))
+      {
+        continue;
+      }
+      out << "(num-instantiations " << ss.str() << " " << i.second << ")"
+          << std::endl;
+    }
+  }
 }
 
 void Instantiate::debugPrintModel()
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index 630efe72c..16ff1f2c3 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -202,8 +202,12 @@ class Instantiate : public QuantifiersUtil
   Node getTermForType(TypeNode tn);
   //--------------------------------------end general utilities
 
-  /** debug print, called once per instantiation round. */
-  void debugPrint();
+  /**
+   * Debug print, called once per instantiation round. This prints
+   * instantiations added this round to trace inst-per-quant-round, if
+   * applicable, and prints to out if the option debug-inst is enabled.
+   */
+  void debugPrint(std::ostream& out);
   /** debug print model, called once, before we terminate with sat/unknown. */
   void debugPrintModel();
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 534d92c92..6dcf1a980 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -16,6 +16,7 @@
 
 #include "options/quantifiers_options.h"
 #include "options/uf_options.h"
+#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/alpha_equivalence.h"
 #include "theory/quantifiers/anti_skolem.h"
@@ -803,8 +804,16 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
     d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
     Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
-    if( d_hasAddedLemma ){
-      d_instantiate->debugPrint();
+    // debug print
+    if (d_hasAddedLemma)
+    {
+      bool debugInstTrace = Trace.isOn("inst-per-quant-round");
+      if (options::debugInst() || debugInstTrace)
+      {
+        Options& sopts = smt::currentSmtEngine()->getOptions();
+        std::ostream& out = *sopts.getOut();
+        d_instantiate->debugPrint(out);
+      }
     }
     if( Trace.isOn("quant-engine") ){
       double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
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)