From 4b86268a71d0d6fd179134889f7d15304623b130 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 13 Jul 2020 14:21:47 -0500 Subject: [PATCH] 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. --- src/options/quantifiers_options.toml | 24 +++++ src/parser/smt2/Smt2.g | 11 +++ src/theory/quantifiers/inst_match_trie.cpp | 16 +--- src/theory/quantifiers/inst_match_trie.h | 8 +- src/theory/quantifiers/instantiate.cpp | 95 ++++++++++++++++--- src/theory/quantifiers/instantiate.h | 21 +++- .../quantifiers/quantifiers_attributes.cpp | 13 ++- .../quantifiers/quantifiers_attributes.h | 10 +- src/theory/quantifiers/theory_quantifiers.cpp | 2 +- src/theory/quantifiers_engine.cpp | 7 +- test/regress/CMakeLists.txt | 1 + .../regress1/quantifiers/dump-inst-i.smt2 | 4 +- .../regress1/quantifiers/dump-inst-proof.smt2 | 4 +- .../regress1/quantifiers/dump-inst.smt2 | 2 +- test/regress/regress1/quantifiers/qid.smt2 | 13 +++ 15 files changed, 178 insertions(+), 53 deletions(-) create mode 100644 test/regress/regress1/quantifiers/qid.smt2 diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 2fb5dd0ba..227f43c46 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1962,6 +1962,30 @@ header = "options/quantifiers_options.h" default = "false" help = "track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization)" +### Output options + +[[option]] + name = "printInstMode" + category = "regular" + long = "print-inst=MODE" + type = "PrintInstMode" + default = "LIST" + help = "print format for printing instantiations" + help_mode = "Print format for printing instantiations." +[[option.mode.LIST]] + name = "list" + help = "Print the list of instantiations per quantified formula, when non-empty." +[[option.mode.NUM]] + name = "num" + help = "Print the total number of instantiations per quantified formula, when non-zero." + +[[option]] + name = "printInstFull" + category = "regular" + long = "print-inst-full" + type = "bool" + default = "true" + help = "print instantiations for formulas that do not have given identifiers" ### SyGuS instantiation options diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index cc87306e3..62ea4e4fa 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1898,6 +1898,16 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] c->setMuted(true); PARSER_STATE->preemptCommand(c); } + | tok=( ATTRIBUTE_QUANTIFIER_ID_TOK ) symbolicExpr[sexpr] + { + api::Sort boolType = SOLVER->getBooleanSort(); + api::Term avar = SOLVER->mkVar(boolType, sexpr.toString()); + attr = std::string(":qid"); + retExpr = MK_TERM(api::INST_ATTRIBUTE, avar); + Command* c = new SetUserAttributeCommand("qid", avar.getExpr()); + c->setMuted(true); + PARSER_STATE->preemptCommand(c); + } | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr] { attr = std::string(":named"); @@ -2351,6 +2361,7 @@ ATTRIBUTE_PATTERN_TOK : ':pattern'; ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern'; ATTRIBUTE_NAMED_TOK : ':named'; ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level'; +ATTRIBUTE_QUANTIFIER_ID_TOK : ':qid'; // operators (NOTE: theory symbols go here) EXISTS_TOK : 'exists'; diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp index 0993edbae..e5ab44032 100644 --- a/src/theory/quantifiers/inst_match_trie.cpp +++ b/src/theory/quantifiers/inst_match_trie.cpp @@ -131,7 +131,6 @@ bool InstMatchTrie::recordInstLemma(Node q, void InstMatchTrie::print(std::ostream& out, Node q, std::vector& terms, - bool& firstTime, bool useActive, std::vector& active) const { @@ -156,11 +155,6 @@ void InstMatchTrie::print(std::ostream& out, } if (print) { - if (firstTime) - { - out << "(instantiation " << q << std::endl; - firstTime = false; - } out << " ( "; for (unsigned i = 0, size = terms.size(); i < size; i++) { @@ -178,7 +172,7 @@ void InstMatchTrie::print(std::ostream& out, for (const std::pair& d : d_data) { terms.push_back(d.first); - d.second.print(out, q, terms, firstTime, useActive, active); + d.second.print(out, q, terms, useActive, active); terms.pop_back(); } } @@ -392,7 +386,6 @@ bool CDInstMatchTrie::recordInstLemma(Node q, void CDInstMatchTrie::print(std::ostream& out, Node q, std::vector& terms, - bool& firstTime, bool useActive, std::vector& active) const { @@ -419,11 +412,6 @@ void CDInstMatchTrie::print(std::ostream& out, } if (print) { - if (firstTime) - { - out << "(instantiation " << q << std::endl; - firstTime = false; - } out << " ( "; for (unsigned i = 0; i < terms.size(); i++) { @@ -438,7 +426,7 @@ void CDInstMatchTrie::print(std::ostream& out, for (const std::pair& d : d_data) { terms.push_back(d.first); - d.second->print(out, q, terms, firstTime, useActive, active); + d.second->print(out, q, terms, useActive, active); terms.pop_back(); } } diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h index a827ff697..961d1608c 100644 --- a/src/theory/quantifiers/inst_match_trie.h +++ b/src/theory/quantifiers/inst_match_trie.h @@ -164,12 +164,11 @@ class InstMatchTrie /** print this class */ void print(std::ostream& out, Node q, - bool& firstTime, bool useActive, std::vector& active) const { std::vector terms; - print(out, q, terms, firstTime, useActive, active); + print(out, q, terms, useActive, active); } /** the data */ std::map d_data; @@ -181,7 +180,6 @@ class InstMatchTrie void print(std::ostream& out, Node q, std::vector& terms, - bool& firstTime, bool useActive, std::vector& active) const; /** helper for get instantiations @@ -332,12 +330,11 @@ class CDInstMatchTrie /** print this class */ void print(std::ostream& out, Node q, - bool& firstTime, bool useActive, std::vector& active) const { std::vector terms; - print(out, q, terms, firstTime, useActive, active); + print(out, q, terms, useActive, active); } private: @@ -351,7 +348,6 @@ class CDInstMatchTrie void print(std::ostream& out, Node q, std::vector& terms, - bool& firstTime, bool useActive, std::vector& active) const; /** helper for get instantiations diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 53e9c6832..d40a2c13d 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -37,7 +37,7 @@ Instantiate::Instantiate(QuantifiersEngine* qe, context::UserContext* u) : d_qe(qe), d_term_db(nullptr), d_term_util(nullptr), - d_total_inst_count_debug(0), + d_total_inst_debug(u), d_c_inst_match_trie_dom(u) { } @@ -264,9 +264,8 @@ bool Instantiate::addInstantiation( return false; } - d_total_inst_debug[q]++; + d_total_inst_debug[q] = d_total_inst_debug[q] + 1; d_temp_inst_debug[q]++; - d_total_inst_count_debug++; if (Trace.isOn("inst")) { Trace("inst") << "*** Instantiate " << q << " with " << std::endl; @@ -465,6 +464,16 @@ Node Instantiate::getTermForType(TypeNode tn) } bool Instantiate::printInstantiations(std::ostream& out) +{ + if (options::printInstMode() == options::PrintInstMode::NUM) + { + return printInstantiationsNum(out); + } + Assert(options::printInstMode() == options::PrintInstMode::LIST); + return printInstantiationsList(out); +} + +bool Instantiate::printInstantiationsList(std::ostream& out) { bool useUnsatCore = false; std::vector active_lemmas; @@ -473,35 +482,89 @@ bool Instantiate::printInstantiations(std::ostream& out) useUnsatCore = true; } bool printed = false; + bool isFull = options::printInstFull(); if (options::incrementalSolving()) { for (std::pair& t : d_c_inst_match_trie) { - bool firstTime = true; - t.second->print(out, t.first, firstTime, useUnsatCore, active_lemmas); - if (!firstTime) + std::stringstream qout; + if (!printQuant(t.first, qout, isFull)) + { + continue; + } + std::stringstream sout; + t.second->print(sout, t.first, useUnsatCore, active_lemmas); + if (!sout.str().empty()) { + out << "(instantiations " << qout.str() << std::endl; + out << sout.str(); out << ")" << std::endl; + printed = true; } - printed = printed || !firstTime; } } else { for (std::pair& t : d_inst_match_trie) { - bool firstTime = true; - t.second.print(out, t.first, firstTime, useUnsatCore, active_lemmas); - if (!firstTime) + std::stringstream qout; + if (!printQuant(t.first, qout, isFull)) + { + continue; + } + std::stringstream sout; + t.second.print(sout, t.first, useUnsatCore, active_lemmas); + if (!sout.str().empty()) { + out << "(instantiations " << qout.str() << std::endl; + out << sout.str(); out << ")" << std::endl; + printed = true; } - printed = printed || !firstTime; } } + out << std::endl; return printed; } +bool Instantiate::printInstantiationsNum(std::ostream& out) +{ + if (d_total_inst_debug.empty()) + { + return false; + } + bool isFull = options::printInstFull(); + for (NodeUIntMap::iterator it = d_total_inst_debug.begin(); + it != d_total_inst_debug.end(); + ++it) + { + std::stringstream ss; + if (printQuant((*it).first, ss, isFull)) + { + out << "(num-instantiations " << ss.str() << " " << (*it).second << ")" + << std::endl; + } + } + return true; +} + +bool Instantiate::printQuant(Node q, std::ostream& out, bool isFull) +{ + if (isFull) + { + out << q; + return true; + } + quantifiers::QuantAttributes* qa = d_qe->getQuantAttributes(); + Node name = qa->getQuantName(q); + if (name.isNull()) + { + return false; + } + out << name; + return true; +} + void Instantiate::getInstantiatedQuantifiedFormulas(std::vector& qs) { if (options::incrementalSolving()) @@ -726,7 +789,7 @@ void Instantiate::debugPrint() // debug information if (Trace.isOn("inst-per-quant-round")) { - for (std::pair& i : d_temp_inst_debug) + for (std::pair& i : d_temp_inst_debug) { Trace("inst-per-quant-round") << " * " << i.second << " for " << i.first << std::endl; @@ -739,10 +802,12 @@ void Instantiate::debugPrintModel() { if (Trace.isOn("inst-per-quant")) { - for (std::pair& i : d_total_inst_debug) + for (NodeUIntMap::iterator it = d_total_inst_debug.begin(); + it != d_total_inst_debug.end(); + ++it) { - Trace("inst-per-quant") << " * " << i.second << " for " << i.first - << std::endl; + Trace("inst-per-quant") + << " * " << (*it).second << " for " << (*it).first << std::endl; } } } diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index aa4f85cdc..630efe72c 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -81,6 +81,8 @@ class InstantiationRewriter */ class Instantiate : public QuantifiersUtil { + typedef context::CDHashMap NodeUIntMap; + public: Instantiate(QuantifiersEngine* qe, context::UserContext* u); ~Instantiate(); @@ -209,7 +211,8 @@ class Instantiate : public QuantifiersUtil /** print instantiations * * Print all instantiations for all quantified formulas on out, - * returns true if at least one instantiation was printed. + * returns true if at least one instantiation was printed. The type of output + * (list, num, etc.) is determined by printInstMode. */ bool printInstantiations(std::ostream& out); /** get instantiated quantified formulas @@ -323,6 +326,16 @@ class Instantiate : public QuantifiersUtil * if possible. */ static Node ensureType(Node n, TypeNode tn); + /** print instantiations in list format */ + bool printInstantiationsList(std::ostream& out); + /** print instantiations in num format */ + bool printInstantiationsNum(std::ostream& out); + /** + * Print quantified formula q on output out. If isFull is false, then we print + * the identifier of the quantified formula if it has one, or print + * nothing and return false otherwise. + */ + bool printQuant(Node q, std::ostream& out, bool isFull); /** pointer to the quantifiers engine */ QuantifiersEngine* d_qe; @@ -333,12 +346,10 @@ class Instantiate : public QuantifiersUtil /** instantiation rewriter classes */ std::vector d_instRewrite; - /** statistics for debugging total instantiation */ - int d_total_inst_count_debug; /** statistics for debugging total instantiations per quantifier */ - std::map d_total_inst_debug; + NodeUIntMap d_total_inst_debug; /** statistics for debugging total instantiations per quantifier per round */ - std::map d_temp_inst_debug; + std::map d_temp_inst_debug; /** list of all instantiations produced for each quantifier * diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 17c625652..c00d3c579 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -50,8 +50,9 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve SygusAttribute ca; n.setAttribute( ca, true ); } - else if (attr == "quant-name") + else if (attr == "qid") { + // using z3 syntax "qid" Trace("quant-attr-debug") << "Set quant-name " << n << std::endl; QuantNameAttribute qna; n.setAttribute(qna, true); @@ -303,6 +304,16 @@ bool QuantAttributes::isQuantElimPartial( Node q ) { } } +Node QuantAttributes::getQuantName(Node q) const +{ + std::map::const_iterator it = d_qattr.find(q); + if (it != d_qattr.end()) + { + return it->second.d_name; + } + return Node::null(); +} + int QuantAttributes::getQuantIdNum( Node q ) { std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); if( it!=d_qattr.end() ){ diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 189c79470..cadf0b0d6 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -126,9 +126,9 @@ struct QAttributes /** the instantiation pattern list for this quantified formula (its 3rd child) */ Node d_ipl; - /** the name of this quantified formula */ + /** The name of this quantified formula, used for :qid */ Node d_name; - /** the quantifier id associated with this formula */ + /** The (internal) quantifier id associated with this formula */ Node d_qid_num; /** is this quantified formula a function definition? */ bool isFunDef() const { return !d_fundef_f.isNull(); } @@ -198,9 +198,11 @@ public: bool isQuantElim( Node q ); /** is quant elim partial */ bool isQuantElimPartial( Node q ); - /** get quant id num */ + /** get quant name, which is used for :qid */ + Node getQuantName(Node q) const; + /** get (internal) quant id num */ int getQuantIdNum( Node q ); - /** get quant id num */ + /** get (internal)quant id num */ Node getQuantIdNumNode( Node q ); /** set instantiation level attr */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index e7d5d36a3..7365960e9 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -46,7 +46,7 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, { out.handleUserAttribute( "fun-def", this ); out.handleUserAttribute( "sygus", this ); - out.handleUserAttribute("quant-name", this); + out.handleUserAttribute("qid", this); out.handleUserAttribute("sygus-synth-grammar", this); out.handleUserAttribute( "sygus-synth-fun-var-list", this ); out.handleUserAttribute( "quant-inst-max-level", this ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 6dce6ce1e..534d92c92 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1153,9 +1153,12 @@ void QuantifiersEngine::getExplanationForInstLemmas( void QuantifiersEngine::printInstantiations( std::ostream& out ) { bool printed = false; // print the skolemizations - if (d_skolemize->printSkolemization(out)) + if (options::printInstMode() == options::PrintInstMode::LIST) { - printed = true; + if (d_skolemize->printSkolemization(out)) + { + printed = true; + } } // print the instantiations if (d_instantiate->printInstantiations(out)) 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) -- 2.30.2