This makes printing instantiations done at the SmtEngine level instead of deeply embedded within the Instantiate module. This provides much better flexibility for future uses of instantiations (e.g. how they are minimized in the new proof infrastructure).
Note this PR breaks the functionality that instantiations are minimized based on the old unsat cores infrastructure (see the disabled regression). This will be fixed once proof-new is fully merged.
type = "bool"
default = "false"
help = "print (binary) application chains in a flattened way, e.g. (a b c) rather than ((a b) c)"
+
+[[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 = "false"
+ help = "print instantiations for formulas that do not have given identifiers"
### 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 = "false"
- help = "print instantiations for formulas that do not have given identifiers"
-
[[option]]
name = "debugInst"
category = "regular"
#include "smt/smt_solver.h"
#include "theory/quantifiers/cegqi/nested_qe.h"
#include "theory/quantifiers/extended_rewrite.h"
+#include "theory/quantifiers_engine.h"
#include "theory/rewriter.h"
#include "theory/theory_engine.h"
Assert(te != nullptr);
te->setUserAttribute(
doFull ? "quant-elim" : "quant-elim-partial", n_attr, node_values, "");
+ QuantifiersEngine* qe = te->getQuantifiersEngine();
n_attr = nm->mkNode(INST_ATTRIBUTE, n_attr);
n_attr = nm->mkNode(INST_PATTERN_LIST, n_attr);
std::vector<Node> children;
// that the (single) quantified formula is preprocessed, rewritten
// version of the input quantified formula q.
std::vector<Node> inst_qs;
- te->getInstantiatedQuantifiedFormulas(inst_qs);
+ qe->getInstantiatedQuantifiedFormulas(inst_qs);
Assert(inst_qs.size() <= 1);
Node ret;
if (inst_qs.size() == 1)
Trace("smt-qe") << "Get qe based on preprocessed quantified formula "
<< topq << std::endl;
std::vector<std::vector<Node>> insts;
- te->getInstantiationTermVectors(topq, insts);
+ qe->getInstantiationTermVectors(topq, insts);
std::vector<Node> vars(ne[0].begin(), ne[0].end());
std::vector<Node> conjs;
// apply the instantiation on the original body
#include "smt/smt_engine_stats.h"
#include "smt/smt_solver.h"
#include "smt/sygus_solver.h"
+#include "theory/quantifiers/instantiation_list.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/rewriter.h"
#include "theory/smt_engine_subsolver.h"
#include "theory/theory_engine.h"
+#include "theory/quantifiers_engine.h"
#include "util/random.h"
#include "util/resource_manager.h"
}
TheoryEngine* te = getTheoryEngine();
Assert(te != nullptr);
- te->printInstantiations(out);
+ QuantifiersEngine* qe = te->getQuantifiersEngine();
+
+ // First, extract and print the skolemizations
+ bool printed = false;
+ bool reqNames = !options::printInstFull();
+ // only print when in list mode
+ if (options::printInstMode() == options::PrintInstMode::LIST)
+ {
+ std::map<Node, std::vector<Node>> sks;
+ qe->getSkolemTermVectors(sks);
+ for (const std::pair<const Node, std::vector<Node>>& s : sks)
+ {
+ Node name;
+ if (!qe->getNameForQuant(s.first, name, reqNames))
+ {
+ // did not have a name and we are only printing formulas with names
+ continue;
+ }
+ SkolemList slist(name, s.second);
+ out << slist;
+ printed = true;
+ }
+ }
+
+ // Second, extract and print the instantiations
+ std::map<Node, std::vector<std::vector<Node>>> insts;
+ getInstantiationTermVectors(insts);
+ for (const std::pair<const Node, std::vector<std::vector<Node>>>& i : insts)
+ {
+ if (i.second.empty())
+ {
+ // no instantiations, skip
+ continue;
+ }
+ Node name;
+ if (!qe->getNameForQuant(i.first, name, reqNames))
+ {
+ // did not have a name and we are only printing formulas with names
+ continue;
+ }
+ // must have a name
+ if (options::printInstMode() == options::PrintInstMode::NUM)
+ {
+ out << "(num-instantiations " << name << " " << i.second.size() << ")"
+ << std::endl;
+ }
+ else
+ {
+ Assert(options::printInstMode() == options::PrintInstMode::LIST);
+ InstantiationList ilist(name, i.second);
+ out << ilist;
+ }
+ printed = true;
+ }
+ // if we did not print anything, we indicate this
+ if (!printed)
+ {
+ out << "No instantiations" << std::endl;
+ }
if (options::instFormatMode() == options::InstFormatMode::SZS)
{
out << "% SZS output end Proof for " << d_state->getFilename() << std::endl;
}
}
+void SmtEngine::getInstantiationTermVectors(
+ std::map<Node, std::vector<std::vector<Node>>>& insts)
+{
+ SmtScope smts(this);
+ finishInit();
+ if (options::proofNew() && getSmtMode() == SmtMode::UNSAT)
+ {
+ // TODO (project #37): minimize instantiations based on proof manager
+ }
+ else
+ {
+ TheoryEngine* te = getTheoryEngine();
+ Assert(te != nullptr);
+ QuantifiersEngine* qe = te->getQuantifiersEngine();
+ // otherwise, just get the list of all instantiations
+ qe->getInstantiationTermVectors(insts);
+ }
+}
+
void SmtEngine::printSynthSolution( std::ostream& out ) {
SmtScope smts(this);
finishInit();
SmtScope smts(this);
TheoryEngine* te = getTheoryEngine();
Assert(te != nullptr);
- te->getInstantiatedQuantifiedFormulas(qs);
+ QuantifiersEngine* qe = te->getQuantifiersEngine();
+ qe->getInstantiatedQuantifiedFormulas(qs);
}
void SmtEngine::getInstantiationTermVectors(
SmtScope smts(this);
TheoryEngine* te = getTheoryEngine();
Assert(te != nullptr);
- te->getInstantiationTermVectors(q, tvecs);
+ QuantifiersEngine* qe = te->getQuantifiersEngine();
+ qe->getInstantiationTermVectors(q, tvecs);
}
std::vector<Node> SmtEngine::getAssertions()
*/
void getInstantiationTermVectors(Node q,
std::vector<std::vector<Node>>& tvecs);
+ /**
+ * Get instantiation term vectors, which maps each instantiated quantified
+ * formula to the list of instantiations for that quantified formula. This
+ * list is minimized if proofs are enabled, and this call is immediately
+ * preceded by an UNSAT or ENTAILED query
+ */
+ void getInstantiationTermVectors(
+ std::map<Node, std::vector<std::vector<Node>>>& insts);
/**
* Get an unsatisfiable core (only if immediately preceded by an UNSAT or
#include "theory/quantifiers/instantiate.h"
#include "expr/node_algorithm.h"
+#include "options/printer_options.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "proof/proof_manager.h"
return d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(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))
- {
- 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)
- {
- 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;
- }
- }
- }
- else
- {
- for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
- {
- 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;
- }
- }
- }
- 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())
}
if (options::debugInst())
{
- bool isFull = options::printInstFull();
+ bool req = !options::printInstFull();
for (std::pair<const Node, uint32_t>& i : d_temp_inst_debug)
{
- std::stringstream ss;
- if (!printQuant(i.first, ss, isFull))
+ Node name;
+ if (!d_qe->getNameForQuant(i.first, name, req))
{
continue;
}
- out << "(num-instantiations " << ss.str() << " " << i.second << ")"
+ out << "(num-instantiations " << name << " " << i.second << ")"
<< std::endl;
}
}
void debugPrintModel();
//--------------------------------------user-level interface utilities
- /** print instantiations
- *
- * Print all instantiations for all quantified formulas on out,
- * 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
*
* Get the list of quantified formulas that were instantiated in the current
Node getInstantiatedConjunction(Node q);
/** get unsat core lemmas
*
- * If this method returns true, then it appends to active_lemmas all lemmas
+ * If this method returns true, then it appends to activeLemmas all lemmas
* that are in the unsat core that originated from the theory of quantifiers.
* This method returns false if the unsat core is not available.
*/
- bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas);
+ bool getUnsatCoreLemmas(std::vector<Node>& activeLemmas);
/** get explanation for instantiation lemmas
*
*
* 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;
return false;
}
-bool Skolemize::printSkolemization(std::ostream& out)
+void Skolemize::getSkolemTermVectors(
+ std::map<Node, std::vector<Node> >& sks) const
{
- bool printed = false;
- for (NodeNodeMap::iterator it = d_skolemized.begin();
- it != d_skolemized.end();
- ++it)
+ std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::const_iterator
+ itk;
+ for (const std::pair<const Node, Node>& p : d_skolemized)
{
- Node q = (*it).first;
- printed = true;
- out << "(skolem " << q << std::endl;
- out << " ( ";
- for (unsigned i = 0; i < d_skolem_constants[q].size(); i++)
- {
- if (i > 0)
- {
- out << " ";
- }
- out << d_skolem_constants[q][i];
- }
- out << " )" << std::endl;
- out << ")" << std::endl;
+ Node q = p.first;
+ itk = d_skolem_constants.find(q);
+ Assert(itk != d_skolem_constants.end());
+ sks[q].insert(sks[q].end(), itk->second.begin(), itk->second.end());
}
- return printed;
}
bool Skolemize::isProofEnabled() const { return d_epg != nullptr; }
Node getSkolemizedBody(Node q);
/** is n a variable that we can apply inductive strenghtening to? */
static bool isInductionTerm(Node n);
- /** print all skolemizations
+ /**
+ * Get skolemization vectors, where for each quantified formula that was
+ * skolemized, this is the list of skolems that were used to witness the
+ * negation of that quantified formula (which is equivalent to an existential
+ * one).
+ *
* This is used for the command line option
* --dump-instantiations
- * which prints an informal justification
- * of steps taken by the quantifiers module.
- * Returns true if we printed at least one
- * skolemization.
+ * which prints an informal justification of steps taken by the quantifiers
+ * module.
*/
- bool printSkolemization(std::ostream& out);
+ void getSkolemTermVectors(std::map<Node, std::vector<Node> >& sks) const;
private:
/** Are proofs enabled? */
#include "theory/quantifiers_engine.h"
+#include "options/printer_options.h"
#include "options/quantifiers_options.h"
#include "options/uf_options.h"
#include "smt/smt_engine_scope.h"
d_instantiate->getInstantiationTermVectors(insts);
}
-void QuantifiersEngine::printInstantiations( std::ostream& out ) {
- bool printed = false;
- // print the skolemizations
- if (options::printInstMode() == options::PrintInstMode::LIST)
- {
- if (d_skolemize->printSkolemization(out))
- {
- printed = true;
- }
- }
- // print the instantiations
- if (d_instantiate->printInstantiations(out))
- {
- printed = true;
- }
- if( !printed ){
- out << "No instantiations" << std::endl;
- }
-}
-
void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
if (d_qmodules->d_synth_e)
{
}
}
-void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) {
+void QuantifiersEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
+{
d_instantiate->getInstantiatedQuantifiedFormulas(qs);
}
+void QuantifiersEngine::getSkolemTermVectors(
+ std::map<Node, std::vector<Node> >& sks) const
+{
+ d_skolemize->getSkolemTermVectors(sks);
+}
+
QuantifiersEngine::Statistics::Statistics()
: d_time("theory::QuantifiersEngine::time"),
d_qcf_time("theory::QuantifiersEngine::time_qcf"),
return d_eq_query->getInternalRepresentative(a, q, index);
}
+Node QuantifiersEngine::getNameForQuant(Node q) const
+{
+ Node name = d_quant_attr->getQuantName(q);
+ if (!name.isNull())
+ {
+ return name;
+ }
+ return q;
+}
+
+bool QuantifiersEngine::getNameForQuant(Node q, Node& name, bool req) const
+{
+ name = getNameForQuant(q);
+ // if we have a name, or we did not require one
+ return name != q || !req;
+}
+
bool QuantifiersEngine::getSynthSolutions(
std::map<Node, std::map<Node, Node> >& sol_map)
{
* guided instantiation.
*/
Node getInternalRepresentative(Node a, Node q, int index);
+ /**
+ * Get quantifiers name, which returns a variable corresponding to the name of
+ * quantified formula q if q has a name, or otherwise returns q itself.
+ */
+ Node getNameForQuant(Node q) const;
+ /**
+ * Get name for quantified formula. Returns true if q has a name or if req
+ * is false. Sets name to the result of the above method.
+ */
+ bool getNameForQuant(Node q, Node& name, bool req = true) const;
public:
//----------user interface for instantiations (see quantifiers/instantiate.h)
- /** print instantiations */
- void printInstantiations(std::ostream& out);
/** print solution for synthesis conjectures */
void printSynthSolution(std::ostream& out);
/** get list of quantified formulas that were instantiated */
std::vector<std::vector<Node> >& tvecs);
void getInstantiationTermVectors(
std::map<Node, std::vector<std::vector<Node> > >& insts);
+ /**
+ * Get skolemization vectors, where for each quantified formula that was
+ * skolemized, this is the list of skolems that were used to witness the
+ * negation of that quantified formula.
+ */
+ void getSkolemTermVectors(std::map<Node, std::vector<Node> >& sks) const;
/** get synth solutions
*
return d_propEngine->getPreprocessedTerm(rewritten);
}
-void TheoryEngine::printInstantiations( std::ostream& out ) {
- if( d_quantEngine ){
- d_quantEngine->printInstantiations( out );
- }else{
- out << "Internal error : instantiations not available when quantifiers are not present." << std::endl;
- Assert(false);
- }
-}
-
void TheoryEngine::printSynthSolution( std::ostream& out ) {
if( d_quantEngine ){
d_quantEngine->printSynthSolution( out );
}
}
-void TheoryEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) {
- if( d_quantEngine ){
- d_quantEngine->getInstantiatedQuantifiedFormulas( qs );
- }else{
- Assert(false);
- }
-}
-
-void TheoryEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
- if( d_quantEngine ){
- d_quantEngine->getInstantiationTermVectors( q, tvecs );
- }else{
- Assert(false);
- }
-}
-
-void TheoryEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
- if( d_quantEngine ){
- d_quantEngine->getInstantiationTermVectors( insts );
- }else{
- Assert(false);
- }
-}
-
TrustNode TheoryEngine::getExplanation(TNode node)
{
Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
* if preprocessing n involves introducing new skolems.
*/
Node getPreprocessedTerm(TNode n);
- /**
- * Print all instantiations made by the quantifiers module.
- */
- void printInstantiations( std::ostream& out );
-
/**
* Print solution for synthesis conjectures found by ce_guided_instantiation module
*/
void printSynthSolution( std::ostream& out );
- /**
- * Get list of quantified formulas that were instantiated
- */
- void getInstantiatedQuantifiedFormulas( std::vector< Node >& qs );
-
- /**
- * Get instantiation methods
- * the first given forall x.q[x] returns ( a, ..., z )
- * the second returns mappings e.g. forall x.q1[x] -> ( q1[a]...q1[z] )
- * , ... , forall x.qn[x] -> ( qn[a]...qn[z] )
- */
- void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs );
- void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts );
-
/**
* Forwards an entailment check according to the given theoryOfMode.
* See theory.h for documentation on entailmentCheck().
regress1/quantifiers/constfunc.cvc
regress1/quantifiers/dt-tc-opt-small.smt2
regress1/quantifiers/dump-inst-i.smt2
- regress1/quantifiers/dump-inst-proof.smt2
regress1/quantifiers/dump-inst.smt2
regress1/quantifiers/eqrange_ex_1.smt2
regress1/quantifiers/ext-ex-deq-trigger.smt2
regress1/quantifiers/anti-sk-simp.smt2
# no longer support snorm option
regress1/quantifiers/arith-snorm.smt2
+ # until we have support for minimizing instantiations based on unsat core
+ regress1/quantifiers/dump-inst-proof.smt2
# ajreynol: different error messages on production and debug:
regress1/quantifiers/macro-subtype-param.smt2
# times out with competition build, ok with other builds:
projects / cvc5.git / commitdiff