diff options
-rw-r--r-- | src/options/printer_options.toml | 23 | ||||
-rw-r--r-- | src/options/quantifiers_options.toml | 23 | ||||
-rw-r--r-- | src/smt/quant_elim_solver.cpp | 6 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 87 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 110 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiate.h | 21 | ||||
-rw-r--r-- | src/theory/quantifiers/skolemize.cpp | 29 | ||||
-rw-r--r-- | src/theory/quantifiers/skolemize.h | 15 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 47 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 18 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 33 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 19 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 3 |
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: |