summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/printer_options.toml23
-rw-r--r--src/options/quantifiers_options.toml23
-rw-r--r--src/smt/quant_elim_solver.cpp6
-rw-r--r--src/smt/smt_engine.cpp87
-rw-r--r--src/smt/smt_engine.h8
-rw-r--r--src/theory/quantifiers/instantiate.cpp110
-rw-r--r--src/theory/quantifiers/instantiate.h21
-rw-r--r--src/theory/quantifiers/skolemize.cpp29
-rw-r--r--src/theory/quantifiers/skolemize.h15
-rw-r--r--src/theory/quantifiers_engine.cpp47
-rw-r--r--src/theory/quantifiers_engine.h18
-rw-r--r--src/theory/theory_engine.cpp33
-rw-r--r--src/theory/theory_engine.h19
-rw-r--r--test/regress/CMakeLists.txt3
14 files changed, 188 insertions, 254 deletions
diff --git a/src/options/printer_options.toml b/src/options/printer_options.toml
index db2f3d6c9..1f27326a0 100644
--- a/src/options/printer_options.toml
+++ b/src/options/printer_options.toml
@@ -43,3 +43,26 @@ header = "options/printer_options.h"
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"
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index d3b3502fc..4b98cb84d 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1889,29 +1889,6 @@ header = "options/quantifiers_options.h"
### 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"
long = "debug-inst"
diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp
index 4636cf17a..d1d86b5e0 100644
--- a/src/smt/quant_elim_solver.cpp
+++ b/src/smt/quant_elim_solver.cpp
@@ -19,6 +19,7 @@
#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"
@@ -58,6 +59,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
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;
@@ -88,7 +90,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
// 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)
@@ -98,7 +100,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
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
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6f775f6b5..19fa8dc34 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -53,10 +53,12 @@
#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"
@@ -1533,13 +1535,90 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
}
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();
@@ -1609,7 +1688,8 @@ void SmtEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
SmtScope smts(this);
TheoryEngine* te = getTheoryEngine();
Assert(te != nullptr);
- te->getInstantiatedQuantifiedFormulas(qs);
+ QuantifiersEngine* qe = te->getQuantifiersEngine();
+ qe->getInstantiatedQuantifiedFormulas(qs);
}
void SmtEngine::getInstantiationTermVectors(
@@ -1618,7 +1698,8 @@ 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()
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 558bd2b40..a392e8c42 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -675,6 +675,14 @@ class CVC4_PUBLIC SmtEngine
*/
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
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index ed02c6b32..3bbe15b8c 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -15,6 +15,7 @@
#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"
@@ -559,107 +560,6 @@ Node Instantiate::getTermForType(TypeNode tn)
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())
@@ -902,15 +802,15 @@ void Instantiate::debugPrint(std::ostream& out)
}
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;
}
}
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index 3a51c8904..bbb1a0a44 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -223,13 +223,6 @@ class Instantiate : public QuantifiersUtil
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
@@ -274,11 +267,11 @@ class Instantiate : public QuantifiersUtil
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
*
*
@@ -328,16 +321,6 @@ 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;
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index 901b7ad82..3ddfc4c9f 100644
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -378,29 +378,18 @@ bool Skolemize::isInductionTerm(Node n)
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; }
diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
index 8cf3e3176..b28854baf 100644
--- a/src/theory/quantifiers/skolemize.h
+++ b/src/theory/quantifiers/skolemize.h
@@ -108,15 +108,18 @@ class Skolemize
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? */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 94f70a2d9..7cec8721c 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -14,6 +14,7 @@
#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"
@@ -979,26 +980,6 @@ void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector
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)
{
@@ -1008,10 +989,17 @@ void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
}
}
-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"),
@@ -1088,6 +1076,23 @@ Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
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)
{
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index d09090da3..126fca01f 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -258,11 +258,19 @@ public:
* 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 */
@@ -272,6 +280,12 @@ public:
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
*
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 16d68ea5c..ba65fe69d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1175,15 +1175,6 @@ Node TheoryEngine::getPreprocessedTerm(TNode n)
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 );
@@ -1193,30 +1184,6 @@ void TheoryEngine::printSynthSolution( std::ostream& 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
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 0be511e47..747c1ccc9 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -663,30 +663,11 @@ class TheoryEngine {
*/
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().
*/
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 52bdd6854..a3eaeee57 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1711,7 +1711,6 @@ set(regress_1_tests
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
@@ -2491,6 +2490,8 @@ set(regression_disabled_tests
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:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback