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.

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 2b47570eda230371bd8b7481fde7775d6e038d4e..b62468cddea12ac2a8413f15421286a1a885c723 100644 (file)
--- 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 62ea4e4fa2a8516733972a64c67896c401b577e7..b88dc70b62cf93e0ca3a98a99534331452fbe721 100644 (file)
--- 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 deed76fc95be72ae755bb602d91d14d3664ccfeb..c9048fc951c9ee5cbf2a71426f61b878121a6c70 100644 (file)
--- 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 630efe72ca11d534c05bf5ee7f7794d0a69947ca..16ff1f2c3db7187fbfa47ad7ec3b65abb5f29975 100644 (file)
--- 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 534d92c92393a13aeb9f19bc42e3db16b4cb1dd0..6dcf1a980051d8310b340ef0b4df9b36e51d00f0 100644 (file)
--- 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 5072e5a176eaeab3bc9e4c83757c3e861e61d3ab..4e79b5dbec02f97fcadb97b386a7c190cb79f91a 100644 (file)
--- 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 94dbe9f88fa98c7a0a0a16e411873a93440435c0..8a9f10ea7a49832cffd4cfb059e1d799aea7cbe7 100644 (file)
--- 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 2995f768249fc01f3c9f90e4d6cc70da5ad880b6..9edc4df2b2c206f4dbda4e2d8e1c6ffef597a0b0 100644 (file)
--- 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 3a8bc4b9c77c214b18ac7c34d85657516edf4037..d150259006f0798b88b29109bd8b7966569e2146 100644 (file)
--- 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 (file)
index 0000000..6b987a3
--- /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)