diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/ce_guided_conjecture.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_conjecture.cpp | 480 |
1 files changed, 189 insertions, 291 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index 7bcaa0cba..1dd4dcbeb 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -36,26 +36,23 @@ namespace CVC4 { namespace theory { namespace quantifiers { -// recursion is not an issue since OR nodes are flattened by the (quantifiers) rewriter -// this function is for sanity since solution correctness in SyGuS depends on fully miniscoping based on this function -void collectDisjuncts( Node n, std::vector< Node >& d ) { - if( n.getKind()==OR ){ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - collectDisjuncts( n[i], d ); - } - }else{ - d.push_back( n ); - } -} - CegConjecture::CegConjecture(QuantifiersEngine* qe) : d_qe(qe), d_ceg_si(new CegConjectureSingleInv(qe, this)), - d_ceg_pbe(new CegConjecturePbe(qe, this)), d_ceg_proc(new CegConjectureProcess(qe)), d_ceg_gc(new CegGrammarConstructor(qe, this)), + d_ceg_pbe(new CegConjecturePbe(qe, this)), + d_ceg_cegis(new Cegis(qe, this)), + d_master(nullptr), d_refine_count(0), - d_syntax_guided(false) {} + d_syntax_guided(false) +{ + if (options::sygusPbe()) + { + d_modules.push_back(d_ceg_pbe.get()); + } + d_modules.push_back(d_ceg_cegis.get()); +} CegConjecture::~CegConjecture() {} @@ -113,45 +110,31 @@ void CegConjecture::assign( Node q ) { d_base_inst = Rewriter::rewrite(d_qe->getInstantiate()->getInstantiation( d_embed_quant, vars, d_candidates)); Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl; - d_base_body = d_base_inst; - if (d_base_body.getKind() == NOT && d_base_body[0].getKind() == FORALL) - { - for (const Node& v : d_base_body[0][0]) - { - d_base_vars.push_back(v); - } - d_base_body = d_base_body[0][1]; - } // register this term with sygus database and other utilities that impact // the enumerative sygus search std::vector< Node > guarded_lemmas; if( !isSingleInvocation() ){ d_ceg_proc->initialize(d_base_inst, d_candidates); - if( options::sygusPbe() ){ - d_ceg_pbe->initialize(d_base_inst, d_candidates, guarded_lemmas); - } else { - for (unsigned i = 0; i < d_candidates.size(); i++) { - Node e = d_candidates[i]; - d_qe->getTermDatabaseSygus()->registerEnumerator(e, e, this); + for (unsigned i = 0, size = d_modules.size(); i < size; i++) + { + if (d_modules[i]->initialize(d_base_inst, d_candidates, guarded_lemmas)) + { + d_master = d_modules[i]; + break; } } + Assert(d_master != nullptr); } if (d_qe->getQuantAttributes()->isSygus(q)) { - collectDisjuncts( d_base_inst, d_base_disj ); - Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl; - //store the inner variables for each disjunct - for( unsigned j=0; j<d_base_disj.size(); j++ ){ - Trace("cegqi") << " " << j << " : " << d_base_disj[j] << std::endl; - d_inner_vars_disj.push_back( std::vector< Node >() ); - //if the disjunct is an existential, store it - if( d_base_disj[j].getKind()==NOT && d_base_disj[j][0].getKind()==FORALL ){ - for( unsigned k=0; k<d_base_disj[j][0][0].getNumChildren(); k++ ){ - d_inner_vars.push_back( d_base_disj[j][0][0][k] ); - d_inner_vars_disj[j].push_back( d_base_disj[j][0][0][k] ); - } + // if the base instantiation is an existential, store its variables + if (d_base_inst.getKind() == NOT && d_base_inst[0].getKind() == FORALL) + { + for (const Node& v : d_base_inst[0][0]) + { + d_inner_vars.push_back(v); } } d_syntax_guided = true; @@ -193,15 +176,6 @@ void CegConjecture::assign( Node q ) { d_qe->getOutputChannel().lemma( lem ); } - // assign the cegis sampler if applicable - if (options::cegisSample() != CEGIS_SAMPLE_NONE) - { - Trace("cegis-sample") << "Initialize sampler for " << d_base_body << "..." - << std::endl; - TypeNode bt = d_base_body.getType(); - d_cegis_sampler.initialize(bt, d_base_vars, options::sygusSamples()); - } - Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() << std::endl; } @@ -241,10 +215,8 @@ void CegConjecture::doSingleInvCheck(std::vector< Node >& lems) { void CegConjecture::doBasicCheck(std::vector< Node >& lems) { std::vector< Node > model_terms; - std::vector< Node > clist; - getCandidateList( clist, true ); - Assert( clist.size()==d_quant[0].getNumChildren() ); - getModelValues( clist, model_terms ); + Assert(d_candidates.size() == d_quant[0].getNumChildren()); + getModelValues(d_candidates, model_terms); if (d_qe->getInstantiate()->addInstantiation(d_quant, model_terms)) { //record the instantiation @@ -258,101 +230,97 @@ bool CegConjecture::needsRefinement() { return !d_ce_sk.empty(); } -void CegConjecture::getCandidateList( std::vector< Node >& clist, bool forceOrig ) { - if( d_ceg_pbe->isPbe() && !forceOrig ){ - d_ceg_pbe->getCandidateList( d_candidates, clist ); - }else{ - clist.insert( clist.end(), d_candidates.begin(), d_candidates.end() ); - } -} +void CegConjecture::doCheck(std::vector<Node>& lems) +{ + Assert(d_master != nullptr); -bool CegConjecture::constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, std::vector< Node >& candidate_values, - std::vector< Node >& lems ) { - Assert( clist.size()==model_values.size() ); - if( d_ceg_pbe->isPbe() ){ - return d_ceg_pbe->constructCandidates( clist, model_values, d_candidates, candidate_values, lems ); - }else{ - Assert( model_values.size()==d_candidates.size() ); - candidate_values.insert( candidate_values.end(), model_values.begin(), model_values.end() ); - } - return true; -} + // get the list of terms that the master strategy is interested in + std::vector<Node> terms; + d_master->getTermList(d_candidates, terms); + + // get their model value + std::vector<Node> enum_values; + getModelValues(terms, enum_values); -void CegConjecture::doCheck(std::vector< Node >& lems, std::vector< Node >& model_values) { - std::vector< Node > clist; - getCandidateList( clist ); - std::vector< Node > c_model_values; + std::vector<Node> candidate_values; Trace("cegqi-check") << "CegConjuncture : check, build candidates..." << std::endl; - bool constructed_cand = constructCandidates( clist, model_values, c_model_values, lems ); + bool constructed_cand = d_master->constructCandidates( + terms, enum_values, d_candidates, candidate_values, lems); + + NodeManager* nm = NodeManager::currentNM(); //must get a counterexample to the value of the current candidate Node inst; if( constructed_cand ){ if( Trace.isOn("cegqi-check") ){ Trace("cegqi-check") << "CegConjuncture : check candidate : " << std::endl; - for( unsigned i=0; i<c_model_values.size(); i++ ){ - Trace("cegqi-check") << " " << i << " : " << d_candidates[i] << " -> " << c_model_values[i] << std::endl; + for (unsigned i = 0, size = candidate_values.size(); i < size; i++) + { + Trace("cegqi-check") << " " << i << " : " << d_candidates[i] << " -> " + << candidate_values[i] << std::endl; } } - Assert( c_model_values.size()==d_candidates.size() ); - inst = d_base_inst.substitute( d_candidates.begin(), d_candidates.end(), c_model_values.begin(), c_model_values.end() ); + Assert(candidate_values.size() == d_candidates.size()); + inst = d_base_inst.substitute(d_candidates.begin(), + d_candidates.end(), + candidate_values.begin(), + candidate_values.end()); }else{ inst = d_base_inst; } //check whether we will run CEGIS on inner skolem variables - bool sk_refine = ( !isGround() || d_refine_count==0 ) && ( !d_ceg_pbe->isPbe() || constructed_cand ); + bool sk_refine = (!isGround() || d_refine_count == 0) && constructed_cand; if( sk_refine ){ if (options::cegisSample() == CEGIS_SAMPLE_TRUST) { // we have that the current candidate passed a sample test // since we trust sampling in this mode, we assert there is no // counterexample to the conjecture here. - NodeManager* nm = NodeManager::currentNM(); Node lem = nm->mkNode(OR, d_quant.negate(), nm->mkConst(false)); lem = getStreamGuardedLemma(lem); lems.push_back(lem); - recordInstantiation(c_model_values); + recordInstantiation(candidate_values); return; } Assert( d_ce_sk.empty() ); - d_ce_sk.push_back( std::vector< Node >() ); }else{ if( !constructed_cand ){ return; } } - std::vector< Node > ic; - ic.push_back( d_quant.negate() ); - std::vector< Node > d; - collectDisjuncts( inst, d ); - Assert( d.size()==d_base_disj.size() ); //immediately skolemize inner existentials - for( unsigned i=0; i<d.size(); i++ ){ - Node dr = Rewriter::rewrite( d[i] ); - if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){ - if( constructed_cand ){ - ic.push_back(d_qe->getSkolemize()->getSkolemizedBody(dr[0]).negate()); - } - if( sk_refine ){ - Assert( !isGround() ); - d_ce_sk.back().push_back( dr[0] ); - } - }else{ - if( constructed_cand ){ - ic.push_back( dr ); - if( !d_inner_vars_disj[i].empty() ){ - Trace("cegqi-debug") << "*** quantified disjunct : " << d[i] << " simplifies to " << dr << std::endl; - } - } - if( sk_refine ){ - d_ce_sk.back().push_back( Node::null() ); - } + Node instr = Rewriter::rewrite(inst); + Node lem; + if (instr.getKind() == NOT && instr[0].getKind() == FORALL) + { + if (constructed_cand) + { + lem = d_qe->getSkolemize()->getSkolemizedBody(instr[0]).negate(); + } + if (sk_refine) + { + Assert(!isGround()); + d_ce_sk.push_back(instr[0]); } } - if( constructed_cand ){ - Node lem = NodeManager::currentNM()->mkNode( OR, ic ); + else + { + if (constructed_cand) + { + // use the instance itself + lem = instr; + } + if (sk_refine) + { + // we add null so that one test of the conjecture for the empty + // substitution is checked + d_ce_sk.push_back(Node::null()); + } + } + if (!lem.isNull()) + { lem = Rewriter::rewrite( lem ); //eagerly unfold applications of evaluation function if( options::sygusDirectEval() ){ @@ -360,9 +328,25 @@ void CegConjecture::doCheck(std::vector< Node >& lems, std::vector< Node >& mode std::map< Node, Node > visited_n; lem = d_qe->getTermDatabaseSygus()->getEagerUnfold( lem, visited_n ); } - lem = getStreamGuardedLemma(lem); - lems.push_back( lem ); - recordInstantiation( c_model_values ); + // record the instantiation + // this is used for remembering the solution + recordInstantiation(candidate_values); + if (lem.isConst() && !lem.getConst<bool>() && options::sygusStream()) + { + // short circuit the check + // instead, we immediately print the current solution. + // this saves us from introducing a check lemma and a new guard. + printAndContinueStream(); + } + else + { + // This is the "verification lemma", which states + // either this conjecture does not have a solution, or candidate_values + // is a solution for this conjecture. + lem = nm->mkNode(OR, d_quant.negate(), lem); + lem = getStreamGuardedLemma(lem); + lems.push_back(lem); + } } } @@ -375,69 +359,45 @@ void CegConjecture::doRefine( std::vector< Node >& lems ){ std::vector< Node > sk_vars; std::vector< Node > sk_subs; //collect the substitution over all disjuncts - for( unsigned k=0; k<d_ce_sk[0].size(); k++ ){ - Node ce_q = d_ce_sk[0][k]; - if( !ce_q.isNull() ){ - Assert( !d_inner_vars_disj[k].empty() ); - std::vector<Node> skolems; - d_qe->getSkolemize()->getSkolemConstants(ce_q, skolems); - Assert(d_inner_vars_disj[k].size() == skolems.size()); - std::vector< Node > model_values; - getModelValues(skolems, model_values); - sk_vars.insert( sk_vars.end(), d_inner_vars_disj[k].begin(), d_inner_vars_disj[k].end() ); - sk_subs.insert( sk_subs.end(), model_values.begin(), model_values.end() ); - }else{ - if( !d_inner_vars_disj[k].empty() ){ - //denegrate case : quantified disjunct was trivially true and does not need to be refined - //add trivial substitution (in case we need substitution for previous cex's) - for( unsigned i=0; i<d_inner_vars_disj[k].size(); i++ ){ - sk_vars.push_back( d_inner_vars_disj[k][i] ); - sk_subs.push_back( getModelValue( d_inner_vars_disj[k][i] ) ); // will return dummy value - } - } - } - } - - //for conditional evaluation + Node ce_q = d_ce_sk[0]; + if (!ce_q.isNull()) + { + std::vector<Node> skolems; + d_qe->getSkolemize()->getSkolemConstants(ce_q, skolems); + Assert(d_inner_vars.size() == skolems.size()); + std::vector<Node> model_values; + getModelValues(skolems, model_values); + sk_vars.insert(sk_vars.end(), d_inner_vars.begin(), d_inner_vars.end()); + sk_subs.insert(sk_subs.end(), model_values.begin(), model_values.end()); + } + else + { + Assert(d_inner_vars.empty()); + } + std::vector< Node > lem_c; - Assert( d_ce_sk[0].size()==d_base_disj.size() ); - std::vector< Node > inst_cond_c; Trace("cegqi-refine") << "doRefine : Construct refinement lemma..." << std::endl; - for( unsigned k=0; k<d_ce_sk[0].size(); k++ ){ - Node ce_q = d_ce_sk[0][k]; - Trace("cegqi-refine-debug") << " For counterexample point, disjunct " << k << " : " << ce_q << " " << d_base_disj[k] << std::endl; - Node c_disj; - if( !ce_q.isNull() ){ - Assert( d_base_disj[k].getKind()==kind::NOT && d_base_disj[k][0].getKind()==kind::FORALL ); - c_disj = d_base_disj[k][0][1]; - }else{ - if( d_inner_vars_disj[k].empty() ){ - c_disj = d_base_disj[k].negate(); - }else{ - //denegrate case : quantified disjunct was trivially true and does not need to be refined - Trace("cegqi-refine-debug") << "*** skip " << d_base_disj[k] << std::endl; - } - } - if( !c_disj.isNull() ){ - //compute the body, inst_cond - //standard CEGIS refinement : plug in values, assert that d_candidates must satisfy entire specification - lem_c.push_back( c_disj ); - } + Trace("cegqi-refine-debug") + << " For counterexample point : " << ce_q << std::endl; + Node base_lem; + if (!ce_q.isNull()) + { + Assert(d_base_inst.getKind() == kind::NOT + && d_base_inst[0].getKind() == kind::FORALL); + base_lem = d_base_inst[0][1]; } + else + { + base_lem = d_base_inst.negate(); + } + Assert( sk_vars.size()==sk_subs.size() ); - - Node base_lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c ); - + Trace("cegqi-refine") << "doRefine : construct and finalize lemmas..." << std::endl; - - + base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); base_lem = Rewriter::rewrite( base_lem ); - d_refinement_lemmas.push_back(base_lem); - - Node lem = - NodeManager::currentNM()->mkNode(OR, getGuard().negate(), base_lem); - lems.push_back( lem ); + d_master->registerRefinementLemma(sk_vars, base_lem, lems); d_ce_sk.clear(); } @@ -534,40 +494,12 @@ Node CegConjecture::getNextDecisionRequest( unsigned& priority ) { }else{ if( !value ){ Trace("cegqi-debug") << "getNextDecision : we have a new solution since stream guard was propagated false: " << curr_stream_guard << std::endl; - // we have generated a solution, print it - // get the current output stream - // this output stream should coincide with wherever --dump-synth is output on - Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); - printSynthSolution( *nodeManagerOptions.getOut(), false ); // need to make the next stream guard needs_new_stream_guard = true; - - // We will not refine the current candidate solution since it is a solution - // thus, we clear information regarding the current refinement - d_ce_sk.clear(); - // However, we need to exclude the current solution using an explicit refinement - // so that we proceed to the next solution. - std::vector< Node > clist; - getCandidateList( clist ); - Trace("cegqi-debug") << "getNextDecision : solution was : " << std::endl; - std::vector< Node > exp; - for( unsigned i=0; i<clist.size(); i++ ){ - Node cprog = clist[i]; - Node sol = cprog; - if( !d_cinfo[cprog].d_inst.empty() ){ - sol = d_cinfo[cprog].d_inst.back(); - // add to explanation of exclusion - d_qe->getTermDatabaseSygus() - ->getExplain() - ->getExplanationForConstantEquality(cprog, sol, exp); - } - Trace("cegqi-debug") << " " << cprog << " -> " << sol << std::endl; - } - Assert( !exp.empty() ); - Node exc_lem = exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( kind::AND, exp ); - exc_lem = exc_lem.negate(); - Trace("cegqi-lemma") << "Cegqi::Lemma : stream exclude current solution : " << exc_lem << std::endl; - d_qe->getOutputChannel().lemma( exc_lem ); + // the guard has propagated false, indicating that a verify + // lemma was unsatisfiable. Hence, the previous candidate is + // an actual solution. We print and continue the stream. + printAndContinueStream(); } } } @@ -591,6 +523,45 @@ Node CegConjecture::getNextDecisionRequest( unsigned& priority ) { return Node::null(); } +void CegConjecture::printAndContinueStream() +{ + Assert(d_master != nullptr); + // we have generated a solution, print it + // get the current output stream + // this output stream should coincide with wherever --dump-synth is output on + Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); + printSynthSolution(*nodeManagerOptions.getOut(), false); + + // We will not refine the current candidate solution since it is a solution + // thus, we clear information regarding the current refinement + d_ce_sk.clear(); + // However, we need to exclude the current solution using an explicit + // blocking clause, so that we proceed to the next solution. + std::vector<Node> terms; + d_master->getTermList(d_candidates, terms); + std::vector<Node> exp; + for (const Node& cprog : terms) + { + Node sol = cprog; + if (!d_cinfo[cprog].d_inst.empty()) + { + sol = d_cinfo[cprog].d_inst.back(); + // add to explanation of exclusion + d_qe->getTermDatabaseSygus() + ->getExplain() + ->getExplanationForConstantEquality(cprog, sol, exp); + } + } + Assert(!exp.empty()); + Node exc_lem = exp.size() == 1 + ? exp[0] + : NodeManager::currentNM()->mkNode(kind::AND, exp); + exc_lem = exc_lem.negate(); + Trace("cegqi-lemma") << "Cegqi::Lemma : stream exclude current solution : " + << exc_lem << std::endl; + d_qe->getOutputChannel().lemma(exc_lem); +} + void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation ) { Trace("cegqi-debug") << "Printing synth solution..." << std::endl; Assert( d_quant[0].getNumChildren()==d_embed_quant[0].getNumChildren() ); @@ -633,29 +604,34 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation if (its == d_sampler.end()) { d_sampler[prog].initializeSygusExt( - d_qe, prog, options::sygusSamples()); + d_qe, prog, options::sygusSamples(), true); its = d_sampler.find(prog); } - Node solb = sygusDb->sygusToBuiltin(sol, prog.getType()); - Node eq_sol = its->second.registerTerm(solb); + Node eq_sol = its->second.registerTerm(sol); // eq_sol is a candidate solution that is equivalent to sol - if (eq_sol != solb) + if (eq_sol != sol) { ++(cei->d_statistics.d_candidate_rewrites); if (!eq_sol.isNull()) { - // Terms solb and eq_sol are equivalent under sample points but do - // not rewrite to the same term. Hence, this indicates a candidate - // rewrite. - out << "(candidate-rewrite " << solb << " " << eq_sol << ")" - << std::endl; + // The analog of terms sol and eq_sol are equivalent under sample + // points but do not rewrite to the same term. Hence, this indicates + // a candidate rewrite. + Printer* p = Printer::getPrinter(options::outputLanguage()); + out << "(candidate-rewrite "; + p->toStreamSygus(out, sol); + out << " "; + p->toStreamSygus(out, eq_sol); + out << ")" << std::endl; ++(cei->d_statistics.d_candidate_rewrites_print); // debugging information if (Trace.isOn("sygus-rr-debug")) { ExtendedRewriter* er = sygusDb->getExtRewriter(); + Node solb = sygusDb->sygusToBuiltin(sol); Node solbr = er->extendedRewrite(solb); - Node eq_solr = er->extendedRewrite(eq_sol); + Node eq_solb = sygusDb->sygusToBuiltin(eq_sol); + Node eq_solr = er->extendedRewrite(eq_solb); Trace("sygus-rr-debug") << "; candidate #1 ext-rewrites to: " << solbr << std::endl; Trace("sygus-rr-debug") @@ -811,84 +787,6 @@ Node CegConjecture::getSymmetryBreakingPredicate( } } -bool CegConjecture::sampleAddRefinementLemma(std::vector<Node>& vals, - std::vector<Node>& lems) -{ - if (Trace.isOn("cegis-sample")) - { - Trace("cegis-sample") << "Check sampling for candidate solution" - << std::endl; - for (unsigned i = 0, size = vals.size(); i < size; i++) - { - Trace("cegis-sample") - << " " << d_candidates[i] << " -> " << vals[i] << std::endl; - } - } - Assert(vals.size() == d_candidates.size()); - Node sbody = d_base_body.substitute( - d_candidates.begin(), d_candidates.end(), vals.begin(), vals.end()); - Trace("cegis-sample-debug") << "Sample " << sbody << std::endl; - // do eager unfolding - std::map<Node, Node> visited_n; - sbody = d_qe->getTermDatabaseSygus()->getEagerUnfold(sbody, visited_n); - Trace("cegis-sample") << "Sample (after unfolding): " << sbody << std::endl; - - NodeManager* nm = NodeManager::currentNM(); - for (unsigned i = 0, size = d_cegis_sampler.getNumSamplePoints(); i < size; - i++) - { - if (d_cegis_sample_refine.find(i) == d_cegis_sample_refine.end()) - { - Node ev = d_cegis_sampler.evaluate(sbody, i); - Trace("cegis-sample-debug") - << "...evaluate point #" << i << " to " << ev << std::endl; - Assert(ev.isConst()); - Assert(ev.getType().isBoolean()); - if (!ev.getConst<bool>()) - { - Trace("cegis-sample-debug") << "...false for point #" << i << std::endl; - // mark this as a CEGIS point (no longer sampled) - d_cegis_sample_refine.insert(i); - std::vector<Node> vars; - std::vector<Node> pt; - d_cegis_sampler.getSamplePoint(i, vars, pt); - Assert(d_base_vars.size() == pt.size()); - Node rlem = d_base_body.substitute( - d_base_vars.begin(), d_base_vars.end(), pt.begin(), pt.end()); - rlem = Rewriter::rewrite(rlem); - if (std::find( - d_refinement_lemmas.begin(), d_refinement_lemmas.end(), rlem) - == d_refinement_lemmas.end()) - { - if (Trace.isOn("cegis-sample")) - { - Trace("cegis-sample") << " false for point #" << i << " : "; - for (const Node& cn : pt) - { - Trace("cegis-sample") << cn << " "; - } - Trace("cegis-sample") << std::endl; - } - Trace("cegqi-engine") << " *** Refine by sampling" << std::endl; - d_refinement_lemmas.push_back(rlem); - // if trust, we are not interested in sending out refinement lemmas - if (options::cegisSample() != CEGIS_SAMPLE_TRUST) - { - Node lem = nm->mkNode(OR, getGuard().negate(), rlem); - lems.push_back(lem); - } - return true; - } - else - { - Trace("cegis-sample-debug") << "...duplicate." << std::endl; - } - } - } - } - return false; -} - }/* namespace CVC4::theory::quantifiers */ }/* namespace CVC4::theory */ }/* namespace CVC4 */ |