From: Andrew Reynolds Date: Tue, 14 Jul 2020 06:41:24 +0000 (-0500) Subject: Debug instantiations output (#4739) X-Git-Tag: cvc5-1.0.0~3113 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1cd3c3c5dad84093aa6b2db164798c8fff473fec;p=cvc5.git 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 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& 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)