From c130a81b3578898dcb5cacaf746e4dd923e2c5d6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 14 Aug 2019 13:23:07 -0500 Subject: [PATCH] Call separate SMT engine for single invocation sygus (#3151) --- src/options/quantifiers_options.toml | 18 - src/smt/smt_engine.cpp | 16 +- src/smt/smt_engine.h | 26 +- .../sygus/ce_guided_single_inv.cpp | 358 ++++++------------ .../quantifiers/sygus/ce_guided_single_inv.h | 65 +--- .../quantifiers/sygus/synth_conjecture.cpp | 60 +-- .../quantifiers/sygus/synth_conjecture.h | 12 +- src/theory/quantifiers/sygus/synth_engine.cpp | 28 -- 8 files changed, 210 insertions(+), 373 deletions(-) diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 717ee9dae..00059bba6 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -940,24 +940,6 @@ header = "options/quantifiers_options.h" read_only = true help = "include constants when reconstruct solutions for single invocation conjectures in original grammar" -[[option]] - name = "cegqiSolMinCore" - category = "regular" - long = "cegqi-si-sol-min-core" - type = "bool" - default = "false" - read_only = true - help = "minimize solutions for single invocation conjectures based on unsat core" - -[[option]] - name = "cegqiSolMinInst" - category = "regular" - long = "cegqi-si-sol-min-inst" - type = "bool" - default = "true" - read_only = true - help = "minimize individual instantiations for single invocation conjectures based on unsat core" - [[option]] name = "cegqiSingleInvAbort" category = "regular" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 27ee446fe..78f47993f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1321,14 +1321,6 @@ void SmtEngine::setDefaults() { options::unconstrainedSimp.set(uncSimp); } } - if (!options::proof()) - { - // minimizing solutions from single invocation requires proofs - if (options::cegqiSolMinCore() && options::cegqiSolMinCore.wasSetByUser()) - { - throw OptionException("cegqi-si-sol-min-core requires --proof"); - } - } // Disable options incompatible with unsat cores and proofs or output an // error if enabled explicitly @@ -1804,8 +1796,12 @@ void SmtEngine::setDefaults() { Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << endl; options::cbqi.set(false); } - //track instantiations? - if( options::cbqiNestedQE() || ( options::proof() && !options::trackInstLemmas.wasSetByUser() ) ){ + // Do we need to track instantiations? + // Needed for sygus due to single invocation techniques. + if (options::cbqiNestedQE() + || (options::proof() && !options::trackInstLemmas.wasSetByUser()) + || is_sygus) + { options::trackInstLemmas.set( true ); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index eba73c380..4ac21d392 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -587,11 +587,33 @@ class CVC4_PUBLIC SmtEngine /** Same as above, but without user-provided grammar restrictions */ bool getAbduct(const Expr& conj, Expr& abd); - /** Get list of quantified formulas that were instantiated. */ + /** + * Get list of quantified formulas that were instantiated on the last call + * to check-sat. + */ void getInstantiatedQuantifiedFormulas(std::vector& qs); - /** Get instantiations. */ + /** + * Get instantiations for quantified formula q. + * + * If q was a quantified formula that was instantiated on the last call to + * check-sat (i.e. q is returned as part of the vector in the method + * getInstantiatedQuantifiedFormulas above), then the list of instantiations + * of that formula that were generated are added to insts. + * + * In particular, if q is of the form forall x. P(x), then insts is a list + * of formulas of the form P(t1), ..., P(tn). + */ void getInstantiations(Expr q, std::vector& insts); + /** + * Get instantiation term vectors for quantified formula q. + * + * This method is similar to above, but in the example above, we return the + * (vectors of) terms t1, ..., tn instead. + * + * Notice that these are not guaranteed to come in the same order as the + * instantiation lemmas above. + */ void getInstantiationTermVectors(Expr q, std::vector >& tvecs); diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 24a594351..59c463b96 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -16,7 +16,11 @@ #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "smt/smt_statistics_registry.h" #include "theory/arith/arith_msum.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_enumeration.h" @@ -31,89 +35,22 @@ using namespace std; namespace CVC4 { -bool CegqiOutputSingleInv::doAddInstantiation( std::vector< Node >& subs ) { - return d_out->doAddInstantiation( subs ); -} - -bool CegqiOutputSingleInv::isEligibleForInstantiation( Node n ) { - return d_out->isEligibleForInstantiation( n ); -} - -bool CegqiOutputSingleInv::addLemma( Node n ) { - return d_out->addLemma( n ); -} - CegSingleInv::CegSingleInv(QuantifiersEngine* qe, SynthConjecture* p) : d_qe(qe), d_parent(p), d_sip(new SingleInvocationPartition), d_sol(new CegSingleInvSol(qe)), - d_cosi(new CegqiOutputSingleInv(this)), - d_cinst(new CegInstantiator(d_qe, d_cosi, false, false)), - d_c_inst_match_trie(NULL), d_single_invocation(false) { - // The third and fourth arguments of d_cosi set to (false,false) until we have - // solution reconstruction for delta and infinity. - if (options::incrementalSolving()) { - d_c_inst_match_trie = new inst::CDInstMatchTrie(qe->getUserContext()); - } } CegSingleInv::~CegSingleInv() { - if (d_c_inst_match_trie) { - delete d_c_inst_match_trie; - } - delete d_cosi; delete d_sol; // (new CegSingleInvSol(qe)), delete d_sip; // d_sip(new SingleInvocationPartition), } -void CegSingleInv::getInitialSingleInvLemma(Node g, std::vector& lems) -{ - Assert(!g.isNull()); - Assert(!d_single_inv.isNull()); - // make for new var/sk - d_single_inv_var.clear(); - d_single_inv_sk.clear(); - Node inst; - NodeManager* nm = NodeManager::currentNM(); - if (d_single_inv.getKind() == FORALL) - { - for (unsigned i = 0, size = d_single_inv[0].getNumChildren(); i < size; i++) - { - std::stringstream ss; - ss << "k_" << d_single_inv[0][i]; - Node k = nm->mkSkolem(ss.str(), - d_single_inv[0][i].getType(), - "single invocation function skolem"); - d_single_inv_var.push_back(d_single_inv[0][i]); - d_single_inv_sk.push_back(k); - d_single_inv_sk_index[k] = i; - } - inst = d_single_inv[1].substitute(d_single_inv_var.begin(), - d_single_inv_var.end(), - d_single_inv_sk.begin(), - d_single_inv_sk.end()); - } - else - { - inst = d_single_inv; - } - inst = TermUtil::simpleNegate(inst); - Trace("cegqi-si") << "Single invocation initial lemma : " << inst - << std::endl; - - // register with the instantiator - Node ginst = nm->mkNode(OR, g.negate(), inst); - lems.push_back(ginst); - // make and register the instantiator - d_cinst.reset(new CegInstantiator(d_qe, d_cosi, false, false)); - d_cinst->registerCounterexampleLemma(lems, d_single_inv_sk); -} - void CegSingleInv::initialize(Node q) { // can only register one quantified formula with this @@ -340,44 +277,7 @@ void CegSingleInv::finishInit(bool syntaxRestricted) } // we now have determined whether we will do single invocation techniques - if( d_single_invocation ){ - d_single_inv = d_sip->getSingleInvocation(); - d_single_inv = TermUtil::simpleNegate( d_single_inv ); - std::vector func_vars; - d_sip->getFunctionVariables(func_vars); - if (!func_vars.empty()) - { - Node pbvl = NodeManager::currentNM()->mkNode(BOUND_VAR_LIST, func_vars); - d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, d_single_inv ); - } - //now, introduce the skolems - std::vector sivars; - d_sip->getSingleInvocationVariables(sivars); - for (unsigned i = 0, size = sivars.size(); i < size; i++) - { - Node v = NodeManager::currentNM()->mkSkolem( - "a", sivars[i].getType(), "single invocation arg"); - d_single_inv_arg_sk.push_back( v ); - } - d_single_inv = d_single_inv.substitute(sivars.begin(), - sivars.end(), - d_single_inv_arg_sk.begin(), - d_single_inv_arg_sk.end()); - Trace("cegqi-si") << "Single invocation formula is : " << d_single_inv << std::endl; - // check whether we can handle this quantified formula - CegHandledStatus status = CegInstantiator::isCbqiQuant(d_single_inv); - if( statuspresolve( d_single_inv ); - } - } - if( !d_single_invocation ) + if (!d_single_invocation) { d_single_inv = Node::null(); Trace("cegqi-si") << "Formula is not single invocation." << std::endl; @@ -387,120 +287,117 @@ void CegSingleInv::finishInit(bool syntaxRestricted) ss << "Property is not handled by single invocation." << std::endl; throw LogicException(ss.str()); } + return; } -} - -bool CegSingleInv::doAddInstantiation(std::vector& subs) -{ - Assert( d_single_inv_sk.size()==subs.size() ); - Trace("cegqi-si-inst-debug") << "CegSingleInv::doAddInstantiation, #vars = "; - Trace("cegqi-si-inst-debug") << d_single_inv_sk.size() << "..." << std::endl; - std::stringstream siss; - if( Trace.isOn("cegqi-si-inst-debug") || Trace.isOn("cegqi-engine") ){ - siss << " * single invocation: " << std::endl; - for( unsigned j=0; jgetFunctionForFirstOrderVariable(d_single_inv[0][j]); - Assert(!op.isNull()); - siss << " * " << op; - siss << " (" << d_single_inv_sk[j] << ")"; - siss << " -> " << subs[j] << std::endl; - } + NodeManager* nm = NodeManager::currentNM(); + d_single_inv = d_sip->getSingleInvocation(); + d_single_inv = TermUtil::simpleNegate(d_single_inv); + std::vector func_vars; + d_sip->getFunctionVariables(func_vars); + if (!func_vars.empty()) + { + Node pbvl = nm->mkNode(BOUND_VAR_LIST, func_vars); + // mark as quantifier elimination to ensure its structure is preserved + Node n_attr = + nm->mkSkolem("qe_si", + nm->booleanType(), + "Auxiliary variable for qe attr for single invocation."); + QuantElimAttribute qea; + n_attr.setAttribute(qea, true); + n_attr = nm->mkNode(INST_ATTRIBUTE, n_attr); + n_attr = nm->mkNode(INST_PATTERN_LIST, n_attr); + // make the single invocation conjecture + d_single_inv = nm->mkNode(FORALL, pbvl, d_single_inv, n_attr); } - Trace("cegqi-si-inst-debug") << siss.str(); - - bool alreadyExists; - Node lem; - if( subs.empty() ){ - Assert( d_single_inv.getKind()!=FORALL ); - alreadyExists = false; - lem = d_single_inv; - }else{ - Assert( d_single_inv.getKind()==FORALL ); - if( options::incrementalSolving() ){ - alreadyExists = !d_c_inst_match_trie->addInstMatch( d_qe, d_single_inv, subs, d_qe->getUserContext() ); - }else{ - alreadyExists = !d_inst_match_trie.addInstMatch( d_qe, d_single_inv, subs ); - } - Trace("cegqi-si-inst-debug") << " * success = " << !alreadyExists << std::endl; - //Trace("cegqi-si-inst-debug") << siss.str(); - //Trace("cegqi-si-inst-debug") << " * success = " << !alreadyExists << std::endl; - if( alreadyExists ){ - return false; - }else{ - Trace("cegqi-engine") << siss.str() << std::endl; - Assert( d_single_inv_var.size()==subs.size() ); - lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() ); - if( d_qe->getTermUtil()->containsVtsTerm( lem ) ){ - Trace("cegqi-engine-debug") << "Rewrite based on vts symbols..." << std::endl; - lem = d_qe->getTermUtil()->rewriteVtsSymbols( lem ); - } - } + // now, introduce the skolems + std::vector sivars; + d_sip->getSingleInvocationVariables(sivars); + for (unsigned i = 0, size = sivars.size(); i < size; i++) + { + Node v = NodeManager::currentNM()->mkSkolem( + "a", sivars[i].getType(), "single invocation arg"); + d_single_inv_arg_sk.push_back(v); } - Trace("cegqi-engine-debug") << "Rewrite..." << std::endl; - lem = Rewriter::rewrite( lem ); - Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl; - if( std::find( d_lemmas_produced.begin(), d_lemmas_produced.end(), lem )==d_lemmas_produced.end() ){ - d_curr_lemmas.push_back( lem ); - d_lemmas_produced.push_back( lem ); - d_inst.push_back( std::vector< Node >() ); - d_inst.back().insert( d_inst.back().end(), subs.begin(), subs.end() ); + d_single_inv = d_single_inv.substitute(sivars.begin(), + sivars.end(), + d_single_inv_arg_sk.begin(), + d_single_inv_arg_sk.end()); + Trace("cegqi-si") << "Single invocation formula is : " << d_single_inv + << std::endl; + // check whether we can handle this quantified formula + CegHandledStatus status = CegInstantiator::isCbqiQuant(d_single_inv); + if (status < CEG_HANDLED) + { + Trace("cegqi-si") << "...do not invoke single invocation techniques since " + "the quantified formula does not have a handled " + "counterexample-guided instantiation strategy!" + << std::endl; + d_single_invocation = false; + d_single_inv = Node::null(); } - return true; } - -bool CegSingleInv::isEligibleForInstantiation(Node n) +bool CegSingleInv::solve() { - return n.getKind()!=SKOLEM || std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )!=d_single_inv_arg_sk.end(); -} - -bool CegSingleInv::addLemma(Node n) -{ - d_curr_lemmas.push_back( n ); - return true; -} - -bool CegSingleInv::check(std::vector& lems) -{ - if( !d_single_inv.isNull() ) { - Trace("cegqi-si-debug") << "CegSingleInv::check..." << std::endl; - Trace("cegqi-si-debug") - << "CegSingleInv::check consulting ceg instantiation..." << std::endl; - d_curr_lemmas.clear(); - Assert( d_cinst!=NULL ); - //call check for instantiator - d_cinst->check(); - Trace("cegqi-si-debug") << "...returned " << d_curr_lemmas.size() << " lemmas " << std::endl; - //add lemmas - lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() ); - return !lems.empty(); - }else{ - // not single invocation + if (d_single_inv.isNull()) + { + // not using single invocation techniques return false; } -} - -Node CegSingleInv::constructSolution(std::vector& indices, - unsigned i, - unsigned index, - std::map& weak_imp) -{ - Assert( index::iterator itw = weak_imp.find( cond ); - if( itw!=weak_imp.end() ){ - cond = itw->second; + Trace("cegqi-si") << "Solve using single invocation..." << std::endl; + NodeManager* nm = NodeManager::currentNM(); + // solve the single invocation conjecture using a fresh copy of SMT engine + SmtEngine siSmt(nm->toExprManager()); + siSmt.setLogic(smt::currentSmtEngine()->getLogicInfo()); + siSmt.assertFormula(d_single_inv.toExpr()); + Result r = siSmt.checkSat(); + Trace("cegqi-si") << "Result: " << r << std::endl; + if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) + { + // conjecture is infeasible or unknown + return false; + } + // now, get the instantiations + std::vector qs; + siSmt.getInstantiatedQuantifiedFormulas(qs); + Assert(qs.size() <= 1); + // track the instantiations, as solution construction is based on this + Trace("cegqi-si") << "#instantiated quantified formulas=" << qs.size() + << std::endl; + d_inst.clear(); + d_instConds.clear(); + for (const Expr& q : qs) + { + TNode qn = Node::fromExpr(q); + Assert(qn.getKind() == FORALL); + std::vector > tvecs; + siSmt.getInstantiationTermVectors(q, tvecs); + Trace("cegqi-si") << "#instantiations of " << q << "=" << tvecs.size() + << std::endl; + std::vector vars; + for (const Node& v : qn[0]) + { + vars.push_back(v); + } + Node body = qn[1]; + for (unsigned i = 0, ninsts = tvecs.size(); i < ninsts; i++) + { + std::vector& tvi = tvecs[i]; + std::vector inst; + for (const Expr& t : tvi) + { + inst.push_back(Node::fromExpr(t)); + } + Trace("cegqi-si") << " Instantiation: " << inst << std::endl; + d_inst.push_back(inst); + Assert(inst.size() == vars.size()); + Node ilem = + body.substitute(vars.begin(), vars.end(), inst.begin(), inst.end()); + ilem = Rewriter::rewrite(ilem); + d_instConds.push_back(ilem); + Trace("cegqi-si") << " Instantiation Lemma: " << ilem << std::endl; } - cond = TermUtil::simpleNegate( cond ); - Node ite1 = d_inst[uindex][i]; - Node ite2 = constructSolution( indices, i, index+1, weak_imp ); - return NodeManager::currentNM()->mkNode( ITE, cond, ite1, ite2 ); } + return true; } //TODO: use term size? @@ -549,7 +446,7 @@ Node CegSingleInv::getSolution(unsigned sol_index, bool rconsSygus) { Assert( d_sol!=NULL ); - Assert( !d_lemmas_produced.empty() ); + Assert(!d_inst.empty()); const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); Node varList = Node::fromExpr( dt.getSygusVarList() ); Node prog = d_quant[0][sol_index]; @@ -573,34 +470,11 @@ Node CegSingleInv::getSolution(unsigned sol_index, //construct the solution Trace("csi-sol") << "Sort solution return values " << sol_index << std::endl; - bool useUnsatCore = false; - std::vector< Node > active_lemmas; - //minimize based on unsat core, if possible - std::map< Node, Node > weak_imp; - if( options::cegqiSolMinCore() ){ - if( options::cegqiSolMinInst() ){ - if( d_qe->getUnsatCoreLemmas( active_lemmas, weak_imp ) ){ - useUnsatCore = true; - } - }else{ - if( d_qe->getUnsatCoreLemmas( active_lemmas ) ){ - useUnsatCore = true; - } - } - } - Assert( d_lemmas_produced.size()==d_inst.size() ); std::vector< unsigned > indices; - for( unsigned i=0; imkNode(ITE, cond, d_inst[uindex][sol_index], s); + } Assert( vars.size()==d_sol->d_varList.size() ); s = s.substitute( vars.begin(), vars.end(), d_sol->d_varList.begin(), d_sol->d_varList.end() ); } diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index b6f282c65..fb216ce0b 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -28,17 +28,6 @@ namespace theory { namespace quantifiers { class SynthConjecture; -class CegSingleInv; - -class CegqiOutputSingleInv : public CegqiOutput { - public: - CegqiOutputSingleInv(CegSingleInv* out) : d_out(out) {} - virtual ~CegqiOutputSingleInv() {} - CegSingleInv* d_out; - bool doAddInstantiation(std::vector& subs) override; - bool isEligibleForInstantiation(Node n) override; - bool addLemma(Node lem) override; -}; class DetTrace { private: @@ -174,9 +163,6 @@ class CegSingleInv std::vector< Node >& terms, std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj ); - // constructing solution - Node constructSolution(std::vector& indices, unsigned i, - unsigned index, std::map& weak_imp); Node postProcessSolution(Node n); private: /** pointer to the quantifiers engine */ @@ -189,10 +175,6 @@ class CegSingleInv std::map< Node, TransitionInference > d_ti; // solution reconstruction CegSingleInvSol* d_sol; - // the instantiator's output channel - CegqiOutputSingleInv* d_cosi; - // the instantiator - std::unique_ptr d_cinst; // list of skolems for each argument of programs std::vector d_single_inv_arg_sk; @@ -202,9 +184,6 @@ class CegSingleInv std::map d_single_inv_sk_index; // program to solution index std::map d_prog_to_sol_index; - // lemmas produced - inst::InstMatchTrie d_inst_match_trie; - inst::CDInstMatchTrie* d_c_inst_match_trie; // original conjecture Node d_orig_conjecture; // solution @@ -212,18 +191,18 @@ class CegSingleInv Node d_solution; Node d_sygus_solution; public: - // lemmas produced - std::vector d_lemmas_produced; + /** + * The list of instantiations that suffice to show the first-order equivalent + * of the negated synthesis conjecture is unsatisfiable. + */ std::vector > d_inst; + /** + * The list of instantiation lemmas, corresponding to instantiations of the + * first order conjecture for the term vectors above. + */ + std::vector d_instConds; private: - std::vector d_curr_lemmas; - // add instantiation - bool doAddInstantiation( std::vector< Node >& subs ); - //is eligible for instantiation - bool isEligibleForInstantiation( Node n ); - // add lemma - bool addLemma( Node lem ); // conjecture Node d_quant; Node d_simp_quant; @@ -246,27 +225,25 @@ class CegSingleInv // get simplified conjecture Node getSimplifiedConjecture() { return d_simp_quant; } public: - /** get the single invocation lemma(s) - * - * This adds lemmas to lem that initializes this class for doing - * counterexample-guided instantiation for the synthesis conjecture. These - * lemmas correspond to the negation of the body of the (anti-skolemized) - * form of the conjecture for fresh skolems. - * - * Argument g is guard, for which all the above lemmas are guarded. - */ - void getInitialSingleInvLemma(Node g, std::vector& lems); // initialize this class for synthesis conjecture q void initialize( Node q ); /** finish initialize * * This method sets up final decisions about whether to use single invocation - * techniques. The argument syntaxRestricted is whether the syntax for - * solutions for the initialized conjecture is restricted. + * techniques. + * + * The argument syntaxRestricted is whether the syntax for solutions for the + * initialized conjecture is restricted. */ void finishInit(bool syntaxRestricted); - //check - bool check( std::vector< Node >& lems ); + /** solve + * + * If single invocation techniques are being used, it solves + * the first order form of the negated synthesis conjecture using a fresh + * copy of the SMT engine. This method returns true if it has successfully + * found a solution to the synthesis conjecture using this method. + */ + bool solve(); //get solution Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed, bool rconsSygus = true ); //reconstruct to syntax diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index b302c4657..6fdbfd0bc 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -46,6 +46,7 @@ namespace quantifiers { SynthConjecture::SynthConjecture(QuantifiersEngine* qe) : d_qe(qe), d_tds(qe->getTermDatabaseSygus()), + d_hasSolution(false, qe->getUserContext()), d_ceg_si(new CegSingleInv(qe, this)), d_ceg_proc(new SynthConjectureProcess(qe)), d_ceg_gc(new CegGrammarConstructor(qe, this)), @@ -72,6 +73,12 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe) SynthConjecture::~SynthConjecture() {} +void SynthConjecture::presolve() +{ + // we don't have a solution yet + d_hasSolution = false; +} + void SynthConjecture::assign(Node q) { Assert(d_embed_quant.isNull()); @@ -216,22 +223,6 @@ void SynthConjecture::assign(Node q) // has been used on this call to check. d_qe->getOutputChannel().requirePhase(d_feasible_guard, true); - if (isSingleInvocation()) - { - std::vector lems; - d_ceg_si->getInitialSingleInvLemma(d_feasible_guard, lems); - for (unsigned i = 0; i < lems.size(); i++) - { - Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation " << i << " : " - << lems[i] << std::endl; - d_qe->getOutputChannel().lemma(lems[i]); - if (Trace.isOn("cegqi-debug")) - { - Node rlem = Rewriter::rewrite(lems[i]); - Trace("cegqi-debug") << "...rewritten : " << rlem << std::endl; - } - } - } Node gneg = d_feasible_guard.negate(); for (unsigned i = 0; i < guarded_lemmas.size(); i++) { @@ -288,17 +279,24 @@ bool SynthConjecture::needsCheck() return true; } -void SynthConjecture::doSingleInvCheck(std::vector& lems) -{ - if (d_ceg_si != NULL) - { - d_ceg_si->check(lems); - } -} - bool SynthConjecture::needsRefinement() const { return d_set_ce_sk_vars; } bool SynthConjecture::doCheck(std::vector& lems) { + if (isSingleInvocation()) + { + // We now try to solve with the single invocation solver, which may or may + // not succeed in solving the conjecture. In either case, we are done and + // return true. + if (d_ceg_si->solve()) + { + d_hasSolution = true; + // the conjecture has a solution, so its negation holds + Node lem = d_quant.negate(); + lem = getStreamGuardedLemma(lem); + lems.push_back(lem); + } + return true; + } Assert(d_master != nullptr); // process the sygus streaming guard @@ -618,12 +616,16 @@ bool SynthConjecture::doCheck(std::vector& lems) // free logic is undecidable. } } - if (success && options::sygusStream()) + if (success) { - // if we were successful, we immediately print the current solution. - // this saves us from introducing a verification lemma and a new guard. - printAndContinueStream(); - return false; + if (options::sygusStream()) + { + // if we were successful, we immediately print the current solution. + // this saves us from introducing a verification lemma and a new guard. + printAndContinueStream(); + return false; + } + d_hasSolution = true; } lem = getStreamGuardedLemma(lem); lems.push_back(lem); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 1cc3702b6..605592d0a 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -70,6 +70,8 @@ class SynthConjecture public: SynthConjecture(QuantifiersEngine* qe); ~SynthConjecture(); + /** presolve */ + void presolve(); /** get original version of conjecture */ Node getConjecture() { return d_quant; } /** get deep embedding version of conjecture */ @@ -82,11 +84,6 @@ class SynthConjecture bool needsCheck(); /** whether the conjecture is waiting for a call to doRefine below */ bool needsRefinement() const; - /** do single invocation check - * This updates Gamma for an iteration of step 2 of Figure 1 of Reynolds et al - * CAV 2015. - */ - void doSingleInvCheck(std::vector& lems); /** do syntax-guided enumerative check * * This is step 2(a) of Figure 3 of Reynolds et al CAV 2015. @@ -165,6 +162,11 @@ class SynthConjecture TermDbSygus* d_tds; /** The feasible guard. */ Node d_feasible_guard; + /** + * Do we have a solution in this user context? This is user-context dependent + * to enable use cases of sygus in incremental mode. + */ + context::CDO d_hasSolution; /** the decision strategy for the feasible guard */ std::unique_ptr d_feasible_strategy; /** single invocation utility */ diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index afa40bdd8..f78886249 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -295,34 +295,6 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj) if (!conj->needsRefinement()) { Trace("cegqi-engine-debug") << "Do conjecture check..." << std::endl; - if (conj->isSingleInvocation()) - { - std::vector clems; - conj->doSingleInvCheck(clems); - if (!clems.empty()) - { - for (const Node& lem : clems) - { - Trace("cegqi-lemma") - << "Cegqi::Lemma : single invocation instantiation : " << lem - << std::endl; - d_quantEngine->addLemma(lem); - } - d_statistics.d_cegqi_si_lemmas += clems.size(); - Trace("cegqi-engine") << " ...try single invocation." << std::endl; - } - else - { - // This can happen for non-monotonic instantiation strategies. We - // set --cbqi-full to ensure that for most strategies (e.g. BV), we - // are using a monotonic strategy. - Trace("cegqi-warn") - << " ...FAILED to add cbqi instantiation for single invocation!" - << std::endl; - } - return true; - } - Trace("cegqi-engine-debug") << " *** Check candidate phase..." << std::endl; std::vector cclems; -- 2.30.2