summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/options/quantifiers_options.toml24
-rw-r--r--src/parser/smt2/Smt2.g11
-rw-r--r--src/theory/quantifiers/inst_match_trie.cpp16
-rw-r--r--src/theory/quantifiers/inst_match_trie.h8
-rw-r--r--src/theory/quantifiers/instantiate.cpp95
-rw-r--r--src/theory/quantifiers/instantiate.h21
-rw-r--r--src/theory/quantifiers/quantifiers_attributes.cpp13
-rw-r--r--src/theory/quantifiers/quantifiers_attributes.h10
-rw-r--r--src/theory/quantifiers/theory_quantifiers.cpp2
-rw-r--r--src/theory/quantifiers_engine.cpp7
10 files changed, 159 insertions, 48 deletions
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<TNode>& terms,
- bool& firstTime,
bool useActive,
std::vector<Node>& 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<const Node, InstMatchTrie>& 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<TNode>& terms,
- bool& firstTime,
bool useActive,
std::vector<Node>& 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<const Node, CDInstMatchTrie*>& 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<Node>& active) const
{
std::vector<TNode> terms;
- print(out, q, terms, firstTime, useActive, active);
+ print(out, q, terms, useActive, active);
}
/** the data */
std::map<Node, InstMatchTrie> d_data;
@@ -181,7 +180,6 @@ class InstMatchTrie
void print(std::ostream& out,
Node q,
std::vector<TNode>& terms,
- bool& firstTime,
bool useActive,
std::vector<Node>& 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<Node>& active) const
{
std::vector<TNode> 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<TNode>& terms,
- bool& firstTime,
bool useActive,
std::vector<Node>& 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;
@@ -466,6 +465,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<Node> active_lemmas;
if (options::trackInstLemmas() && getUnsatCoreLemmas(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<const Node, inst::CDInstMatchTrie*>& 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<const Node, inst::InstMatchTrie>& 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<Node>& qs)
{
if (options::incrementalSolving())
@@ -726,7 +789,7 @@ void Instantiate::debugPrint()
// debug information
if (Trace.isOn("inst-per-quant-round"))
{
- for (std::pair<const Node, int>& i : d_temp_inst_debug)
+ for (std::pair<const Node, uint32_t>& 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<const Node, int>& 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<Node, uint32_t, NodeHashFunction> 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<InstantiationRewriter*> d_instRewrite;
- /** statistics for debugging total instantiation */
- int d_total_inst_count_debug;
/** statistics for debugging total instantiations per quantifier */
- std::map<Node, int> d_total_inst_debug;
+ NodeUIntMap d_total_inst_debug;
/** statistics for debugging total instantiations per quantifier per round */
- std::map<Node, int> d_temp_inst_debug;
+ std::map<Node, uint32_t> 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<Node, QAttributes>::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))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback