summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/quantifiers_options.toml10
-rw-r--r--src/parser/smt2/Smt2.g2
-rw-r--r--src/theory/quantifiers/instantiate.cpp16
-rw-r--r--src/theory/quantifiers/instantiate.h8
-rw-r--r--src/theory/quantifiers_engine.cpp13
-rw-r--r--test/regress/CMakeLists.txt1
-rw-r--r--test/regress/regress1/quantifiers/dump-inst-i.smt22
-rw-r--r--test/regress/regress1/quantifiers/dump-inst-proof.smt22
-rw-r--r--test/regress/regress1/quantifiers/dump-inst.smt22
-rw-r--r--test/regress/regress1/quantifiers/qid-debug-inst.smt213
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback