theory/quantifiers/single_inv_partition.h \
theory/quantifiers/skolemize.cpp \
theory/quantifiers/skolemize.h \
+ theory/quantifiers/sygus/cegis.cpp \
+ theory/quantifiers/sygus/cegis.h \
theory/quantifiers/sygus/ce_guided_conjecture.cpp \
theory/quantifiers/sygus/ce_guided_conjecture.h \
theory/quantifiers/sygus/ce_guided_instantiation.cpp \
theory/quantifiers/sygus/sygus_grammar_norm.h \
theory/quantifiers/sygus/sygus_grammar_red.cpp \
theory/quantifiers/sygus/sygus_grammar_red.h \
+ theory/quantifiers/sygus/sygus_module.cpp \
+ theory/quantifiers/sygus/sygus_module.h \
theory/quantifiers/sygus/sygus_process_conj.cpp \
theory/quantifiers/sygus/sygus_process_conj.h \
theory/quantifiers/sygus/term_database_sygus.cpp \
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() {}
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))
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;
}
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
bool CegConjecture::needsRefinement() {
return !d_ce_sk.empty();
}
+void CegConjecture::doCheck(std::vector<Node>& lems)
+{
+ Assert(d_master != nullptr);
-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() );
- }
-}
+ // get the list of terms that the master strategy is interested in
+ std::vector<Node> terms;
+ d_master->getTermList(d_candidates, terms);
-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 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() );
}
}
if( constructed_cand ){
- Node lem = NodeManager::currentNM()->mkNode( OR, ic );
+ Node lem = nm->mkNode(OR, ic);
lem = Rewriter::rewrite( lem );
//eagerly unfold applications of evaluation function
if( options::sygusDirectEval() ){
}
lem = getStreamGuardedLemma(lem);
lems.push_back( lem );
- recordInstantiation( c_model_values );
+ recordInstantiation(candidate_values);
}
}
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);
+ d_master->registerRefinementLemma(base_lem);
Node lem =
NodeManager::currentNM()->mkNode(OR, getGuard().negate(), base_lem);
return curr_stream_guard;
}else{
if( !value ){
+ Assert(d_master != nullptr);
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
// 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 );
+ // However, we need to exclude the current solution using an
+ // explicit refinement
+ // so that we proceed to the next solution.
+ std::vector<Node> terms;
+ d_master->getTermList(d_candidates, terms);
Trace("cegqi-debug") << "getNextDecision : solution was : " << std::endl;
std::vector< Node > exp;
- for( unsigned i=0; i<clist.size(); i++ ){
- Node cprog = clist[i];
+ for (const Node& cprog : terms)
+ {
Node sol = cprog;
if( !d_cinfo[cprog].d_inst.empty() ){
sol = d_cinfo[cprog].d_inst.back();
}
}
-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 */
#include <memory>
-#include "theory/quantifiers/sygus/sygus_pbe.h"
#include "theory/quantifiers/sygus/ce_guided_single_inv.h"
+#include "theory/quantifiers/sygus/cegis.h"
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include "theory/quantifiers/sygus/sygus_pbe.h"
#include "theory/quantifiers/sygus/sygus_process_conj.h"
#include "theory/quantifiers/sygus_sampler.h"
#include "theory/quantifiers_engine.h"
bool needsCheck( std::vector< Node >& lem );
/** whether the conjecture is waiting for a call to doRefine below */
bool needsRefinement();
- /** get the list of candidates */
- void getCandidateList( std::vector< Node >& clist, bool forceOrig = false );
/** do single invocation check
* This updates Gamma for an iteration of step 2 of Figure 1 of Reynolds et al CAV 2015.
*/
/** do syntax-guided enumerative check
* This is step 2(a) of Figure 3 of Reynolds et al CAV 2015.
*/
- void doCheck(std::vector< Node >& lems, std::vector< Node >& model_values);
+ void doCheck(std::vector<Node>& lems);
/** do basic check
* This is called for non-SyGuS synthesis conjectures
*/
/** get model value for term n */
Node getModelValue( Node n );
- //-----------------------------------refinement lemmas
- /** get number of refinement lemmas we have added so far */
- unsigned getNumRefinementLemmas() { return d_refinement_lemmas.size(); }
- /** get refinement lemma
- *
- * If d_embed_quant is forall d. exists y. P( d, y ), then a refinement
- * lemma is one of the form ~P( d_candidates, c ) for some c.
- */
- Node getRefinementLemma( unsigned i ) { return d_refinement_lemmas[i]; }
- /** sample add refinement lemma
- *
- * This function will check if there is a sample point in d_sampler that
- * refutes the candidate solution (d_quant_vars->vals). If so, it adds a
- * refinement lemma to the lists d_refinement_lemmas that corresponds to that
- * sample point, and adds a lemma to lems if cegisSample mode is not trust.
- */
- bool sampleAddRefinementLemma(std::vector<Node>& vals,
- std::vector<Node>& lems);
- //-----------------------------------end refinement lemmas
-
/** get program by examples utility */
CegConjecturePbe* getPbe() { return d_ceg_pbe.get(); }
/** get utility for static preprocessing and analysis of conjectures */
QuantifiersEngine * d_qe;
/** single invocation utility */
std::unique_ptr<CegConjectureSingleInv> d_ceg_si;
- /** program by examples utility */
- std::unique_ptr<CegConjecturePbe> d_ceg_pbe;
/** utility for static preprocessing and analysis of conjectures */
std::unique_ptr<CegConjectureProcess> d_ceg_proc;
/** grammar utility */
std::unique_ptr<CegGrammarConstructor> d_ceg_gc;
+
+ //------------------------modules
+ /** program by examples module */
+ std::unique_ptr<CegConjecturePbe> d_ceg_pbe;
+ /** CEGIS module */
+ std::unique_ptr<Cegis> d_ceg_cegis;
+ /** the set of active modules (subset of the above list) */
+ std::vector<SygusModule*> d_modules;
+ /** master module
+ *
+ * This is the module (one of those above) that takes sole responsibility
+ * for this conjecture, determined during assign(...).
+ */
+ SygusModule* d_master;
+ //------------------------end modules
+
/** list of constants for quantified formula
* The outer Skolems for the negation of d_embed_quant.
*/
* this is the formula exists y. P( d_candidates, y ).
*/
Node d_base_inst;
- /** If d_base_inst is exists y. P( d, y ), then this is y. */
- std::vector<Node> d_base_vars;
- /**
- * If d_base_inst is exists y. P( d, y ), then this is the formula
- * P( d_candidates, y ).
- */
- Node d_base_body;
/** expand base inst to disjuncts */
std::vector< Node > d_base_disj;
/** list of variables on inner quantification */
/** current extential quantifeirs whose couterexamples we must refine */
std::vector< std::vector< Node > > d_ce_sk;
- //-----------------------------------refinement lemmas
- /** refinement lemmas */
- std::vector< Node > d_refinement_lemmas;
- //-----------------------------------end refinement lemmas
/** the asserted (negated) conjecture */
Node d_quant;
std::map< Node, CandidateInfo > d_cinfo;
/** number of times we have called doRefine */
unsigned d_refine_count;
- /** construct candidates */
- bool constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values,
- std::vector< Node >& candidate_values, std::vector< Node >& lems );
/** get candidadate */
Node getCandidate( unsigned int i ) { return d_candidates[i]; }
/** record instantiation (this is used to construct solutions later) */
* rewrite rules.
*/
std::map<Node, SygusSamplerExt> d_sampler;
- /** sampler object for the option cegisSample()
- *
- * This samples points of the type of the inner variables of the synthesis
- * conjecture (d_base_vars).
- */
- SygusSampler d_cegis_sampler;
- /** cegis sample refine points
- *
- * Stores the list of indices of sample points in d_cegis_sampler we have
- * added as refinement lemmas.
- */
- std::unordered_set<unsigned> d_cegis_sample_refine;
};
} /* namespace CVC4::theory::quantifiers */
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
-//FIXME : remove this include (github issue #1156)
-#include "theory/bv/theory_bv_rewriter.h"
using namespace CVC4::kind;
using namespace std;
Trace("cegqi-engine") << " ...try single invocation." << std::endl;
return;
}
- //ignore return value here
- std::vector< Node > clist;
- conj->getCandidateList( clist );
- std::vector< Node > model_values;
- conj->getModelValues( clist, model_values );
- if( options::sygusDirectEval() ){
- bool addedEvalLemmas = false;
- if( options::sygusCRefEval() ){
- Trace("cegqi-engine") << " *** Do conjecture refinement evaluation..." << std::endl;
- // see if any refinement lemma is refuted by evaluation
- std::vector< Node > cre_lems;
- getCRefEvaluationLemmas( conj, clist, model_values, cre_lems );
- if( !cre_lems.empty() ){
- for( unsigned j=0; j<cre_lems.size(); j++ ){
- Node lem = cre_lems[j];
- if( d_quantEngine->addLemma( lem ) ){
- Trace("cegqi-lemma") << "Cegqi::Lemma : cref evaluation : " << lem << std::endl;
- addedEvalLemmas = true;
- }
- }
- if( addedEvalLemmas ){
- //return;
- }
- }
- }
- Trace("cegqi-engine") << " *** Do direct evaluation..." << std::endl;
- std::vector< Node > eager_terms;
- std::vector< Node > eager_vals;
- std::vector< Node > eager_exps;
- for( unsigned j=0; j<clist.size(); j++ ){
- Trace("cegqi-debug") << " register " << clist[j] << " -> " << model_values[j] << std::endl;
- d_quantEngine->getTermDatabaseSygus()->registerModelValue( clist[j], model_values[j], eager_terms, eager_vals, eager_exps );
- }
- Trace("cegqi-debug") << "...produced " << eager_terms.size() << " eager evaluation lemmas." << std::endl;
- if( !eager_terms.empty() ){
- for( unsigned j=0; j<eager_terms.size(); j++ ){
- Node lem = NodeManager::currentNM()->mkNode( kind::OR, eager_exps[j].negate(), eager_terms[j].eqNode( eager_vals[j] ) );
- if( d_quantEngine->getTheoryEngine()->isTheoryEnabled(THEORY_BV) ){
- //FIXME: hack to incorporate hacks from BV for division by zero (github issue #1156)
- lem = bv::TheoryBVRewriter::eliminateBVSDiv( lem );
- }
- if( d_quantEngine->addLemma( lem ) ){
- Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem << std::endl;
- addedEvalLemmas = true;
- }
- }
- }
- if( addedEvalLemmas ){
- return;
- }
- }
Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl;
std::vector< Node > cclems;
- conj->doCheck( cclems, model_values );
+ conj->doCheck(cclems);
bool addedLemma = false;
for( unsigned i=0; i<cclems.size(); i++ ){
Node lem = cclems[i];
}
}
-void CegInstantiation::getCRefEvaluationLemmas( CegConjecture * conj, std::vector< Node >& vs, std::vector< Node >& ms, std::vector< Node >& lems ) {
- Trace("sygus-cref-eval") << "Cref eval : conjecture has " << conj->getNumRefinementLemmas() << " refinement lemmas." << std::endl;
- unsigned nlemmas = conj->getNumRefinementLemmas();
- if (nlemmas > 0 || options::cegisSample() != CEGIS_SAMPLE_NONE)
- {
- Assert( vs.size()==ms.size() );
-
- TermDbSygus* tds = d_quantEngine->getTermDatabaseSygus();
- Node nfalse = d_quantEngine->getTermUtil()->d_false;
- Node neg_guard = conj->getGuard().negate();
- for (unsigned i = 0; i <= nlemmas; i++)
- {
- if (i == nlemmas)
- {
- bool addedSample = false;
- // find a new one by sampling, if applicable
- if (options::cegisSample() != CEGIS_SAMPLE_NONE)
- {
- addedSample = conj->sampleAddRefinementLemma(ms, lems);
- }
- if (!addedSample)
- {
- return;
- }
- }
- Node lem;
- std::map< Node, Node > visited;
- std::map< Node, std::vector< Node > > exp;
- lem = conj->getRefinementLemma(i);
- if( !lem.isNull() ){
- std::vector< Node > lem_conj;
- //break into conjunctions
- if( lem.getKind()==kind::AND ){
- for( unsigned i=0; i<lem.getNumChildren(); i++ ){
- lem_conj.push_back( lem[i] );
- }
- }else{
- lem_conj.push_back( lem );
- }
- EvalSygusInvarianceTest vsit;
- for( unsigned j=0; j<lem_conj.size(); j++ ){
- Node lemc = lem_conj[j];
- Trace("sygus-cref-eval") << "Check refinement lemma conjunct " << lemc << " against current model." << std::endl;
- Trace("sygus-cref-eval2") << "Check refinement lemma conjunct " << lemc << " against current model." << std::endl;
- Node cre_lem;
- Node lemcs = lemc.substitute( vs.begin(), vs.end(), ms.begin(), ms.end() );
- Trace("sygus-cref-eval2") << "...under substitution it is : " << lemcs << std::endl;
- Node lemcsu = vsit.doEvaluateWithUnfolding(tds, lemcs);
- Trace("sygus-cref-eval2") << "...after unfolding is : " << lemcsu << std::endl;
- if( lemcsu==d_quantEngine->getTermUtil()->d_false ){
- std::vector< Node > msu;
- std::vector< Node > mexp;
- msu.insert( msu.end(), ms.begin(), ms.end() );
- for( unsigned k=0; k<vs.size(); k++ ){
- vsit.setUpdatedTerm(msu[k]);
- msu[k] = vs[k];
- // substitute for everything except this
- Node sconj =
- lemc.substitute(vs.begin(), vs.end(), msu.begin(), msu.end());
- vsit.init(sconj, vs[k], nfalse);
- // get minimal explanation for this
- Node ut = vsit.getUpdatedTerm();
- Trace("sygus-cref-eval2-debug")
- << " compute min explain of : " << vs[k] << " = " << ut
- << std::endl;
- d_quantEngine->getTermDatabaseSygus()
- ->getExplain()
- ->getExplanationFor(vs[k], ut, mexp, vsit);
- msu[k] = ut;
- }
- if( !mexp.empty() ){
- Node en = mexp.size()==1 ? mexp[0] : NodeManager::currentNM()->mkNode( kind::AND, mexp );
- cre_lem = NodeManager::currentNM()->mkNode( kind::OR, en.negate(), neg_guard );
- }else{
- cre_lem = neg_guard;
- }
- }
- if( !cre_lem.isNull() ){
- if( std::find( lems.begin(), lems.end(), cre_lem )==lems.end() ){
- Trace("sygus-cref-eval") << "...produced lemma : " << cre_lem << std::endl;
- lems.push_back( cre_lem );
- }
- }
- }
- }
- }
- }
-}
-
void CegInstantiation::printSynthSolution( std::ostream& out ) {
if( d_conj->isAssigned() )
{
CegConjecture * d_conj;
/** last instantiation by single invocation module? */
bool d_last_inst_si;
-private: //for direct evaluation
- /** get refinement evaluation */
- void getCRefEvaluationLemmas( CegConjecture * conj, std::vector< Node >& vs, std::vector< Node >& ms, std::vector< Node >& lems );
private:
/** check conjecture */
void checkCegConjecture( CegConjecture * conj );
--- /dev/null
+/********************* */
+/*! \file cegis.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of cegis
+ **/
+
+#include "theory/quantifiers/sygus/cegis.h"
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+// FIXME : remove these includes (github issue #1156)
+#include "theory/bv/theory_bv_rewriter.h"
+#include "theory/theory_engine.h"
+
+using namespace std;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+Cegis::Cegis(QuantifiersEngine* qe, CegConjecture* p) : SygusModule(qe, p) {}
+bool Cegis::initialize(Node n,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& lemmas)
+{
+ d_base_body = n;
+ 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];
+ }
+
+ // 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());
+ }
+
+ // initialize an enumerator for each candidate
+ TermDbSygus* tds = d_qe->getTermDatabaseSygus();
+ for (unsigned i = 0; i < candidates.size(); i++)
+ {
+ tds->registerEnumerator(candidates[i], candidates[i], d_parent);
+ }
+ return true;
+}
+
+void Cegis::getTermList(const std::vector<Node>& candidates,
+ std::vector<Node>& enums)
+{
+ enums.insert(enums.end(), candidates.begin(), candidates.end());
+}
+
+/** construct candidate */
+bool Cegis::constructCandidates(const std::vector<Node>& enums,
+ const std::vector<Node>& enum_values,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& candidate_values,
+ std::vector<Node>& lems)
+{
+ candidate_values.insert(
+ candidate_values.end(), enum_values.begin(), enum_values.end());
+
+ if (options::sygusDirectEval())
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ bool addedEvalLemmas = false;
+ if (options::sygusCRefEval())
+ {
+ Trace("cegqi-engine") << " *** Do conjecture refinement evaluation..."
+ << std::endl;
+ // see if any refinement lemma is refuted by evaluation
+ std::vector<Node> cre_lems;
+ getRefinementEvalLemmas(candidates, candidate_values, cre_lems);
+ if (!cre_lems.empty())
+ {
+ for (unsigned j = 0; j < cre_lems.size(); j++)
+ {
+ Node lem = cre_lems[j];
+ if (d_qe->addLemma(lem))
+ {
+ Trace("cegqi-lemma") << "Cegqi::Lemma : cref evaluation : " << lem
+ << std::endl;
+ addedEvalLemmas = true;
+ }
+ }
+ // we could, but do not return here.
+ // experimentally, it is better to add the lemmas below as well,
+ // in parallel.
+ }
+ }
+ Trace("cegqi-engine") << " *** Do direct evaluation..." << std::endl;
+ std::vector<Node> eager_terms;
+ std::vector<Node> eager_vals;
+ std::vector<Node> eager_exps;
+ TermDbSygus* tds = d_qe->getTermDatabaseSygus();
+ for (unsigned j = 0, size = candidates.size(); j < size; j++)
+ {
+ Trace("cegqi-debug") << " register " << candidates[j] << " -> "
+ << candidate_values[j] << std::endl;
+ tds->registerModelValue(candidates[j],
+ candidate_values[j],
+ eager_terms,
+ eager_vals,
+ eager_exps);
+ }
+ Trace("cegqi-debug") << "...produced " << eager_terms.size()
+ << " eager evaluation lemmas." << std::endl;
+
+ for (unsigned j = 0, size = eager_terms.size(); j < size; j++)
+ {
+ Node lem = nm->mkNode(kind::OR,
+ eager_exps[j].negate(),
+ eager_terms[j].eqNode(eager_vals[j]));
+ if (d_qe->getTheoryEngine()->isTheoryEnabled(THEORY_BV))
+ {
+ // FIXME: hack to incorporate hacks from BV for division by zero
+ // (github issue #1156)
+ lem = bv::TheoryBVRewriter::eliminateBVSDiv(lem);
+ }
+ if (d_qe->addLemma(lem))
+ {
+ Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem
+ << std::endl;
+ addedEvalLemmas = true;
+ }
+ }
+ if (addedEvalLemmas)
+ {
+ return false;
+ }
+ }
+
+ return true;
+}
+
+void Cegis::registerRefinementLemma(Node lem)
+{
+ d_refinement_lemmas.push_back(lem);
+}
+
+void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs,
+ const std::vector<Node>& ms,
+ std::vector<Node>& lems)
+{
+ Trace("sygus-cref-eval") << "Cref eval : conjecture has "
+ << getNumRefinementLemmas() << " refinement lemmas."
+ << std::endl;
+ unsigned nlemmas = getNumRefinementLemmas();
+ if (nlemmas > 0 || options::cegisSample() != CEGIS_SAMPLE_NONE)
+ {
+ Assert(vs.size() == ms.size());
+
+ TermDbSygus* tds = d_qe->getTermDatabaseSygus();
+ NodeManager* nm = NodeManager::currentNM();
+
+ Node nfalse = nm->mkConst(false);
+ Node neg_guard = d_parent->getGuard().negate();
+ for (unsigned i = 0; i <= nlemmas; i++)
+ {
+ if (i == nlemmas)
+ {
+ bool addedSample = false;
+ // find a new one by sampling, if applicable
+ if (options::cegisSample() != CEGIS_SAMPLE_NONE)
+ {
+ addedSample = sampleAddRefinementLemma(vs, ms, lems);
+ }
+ if (!addedSample)
+ {
+ return;
+ }
+ }
+ Node lem;
+ std::map<Node, Node> visited;
+ std::map<Node, std::vector<Node> > exp;
+ lem = getRefinementLemma(i);
+ if (!lem.isNull())
+ {
+ std::vector<Node> lem_conj;
+ // break into conjunctions
+ if (lem.getKind() == kind::AND)
+ {
+ for (unsigned i = 0; i < lem.getNumChildren(); i++)
+ {
+ lem_conj.push_back(lem[i]);
+ }
+ }
+ else
+ {
+ lem_conj.push_back(lem);
+ }
+ EvalSygusInvarianceTest vsit;
+ for (unsigned j = 0; j < lem_conj.size(); j++)
+ {
+ Node lemc = lem_conj[j];
+ Trace("sygus-cref-eval") << "Check refinement lemma conjunct " << lemc
+ << " against current model." << std::endl;
+ Trace("sygus-cref-eval2") << "Check refinement lemma conjunct "
+ << lemc << " against current model."
+ << std::endl;
+ Node cre_lem;
+ Node lemcs =
+ lemc.substitute(vs.begin(), vs.end(), ms.begin(), ms.end());
+ Trace("sygus-cref-eval2") << "...under substitution it is : " << lemcs
+ << std::endl;
+ Node lemcsu = vsit.doEvaluateWithUnfolding(tds, lemcs);
+ Trace("sygus-cref-eval2") << "...after unfolding is : " << lemcsu
+ << std::endl;
+ if (lemcsu.isConst() && !lemcsu.getConst<bool>())
+ {
+ std::vector<Node> msu;
+ std::vector<Node> mexp;
+ msu.insert(msu.end(), ms.begin(), ms.end());
+ for (unsigned k = 0; k < vs.size(); k++)
+ {
+ vsit.setUpdatedTerm(msu[k]);
+ msu[k] = vs[k];
+ // substitute for everything except this
+ Node sconj =
+ lemc.substitute(vs.begin(), vs.end(), msu.begin(), msu.end());
+ vsit.init(sconj, vs[k], nfalse);
+ // get minimal explanation for this
+ Node ut = vsit.getUpdatedTerm();
+ Trace("sygus-cref-eval2-debug")
+ << " compute min explain of : " << vs[k] << " = " << ut
+ << std::endl;
+ tds->getExplain()->getExplanationFor(vs[k], ut, mexp, vsit);
+ msu[k] = ut;
+ }
+ if (!mexp.empty())
+ {
+ Node en =
+ mexp.size() == 1 ? mexp[0] : nm->mkNode(kind::AND, mexp);
+ cre_lem = nm->mkNode(kind::OR, en.negate(), neg_guard);
+ }
+ else
+ {
+ cre_lem = neg_guard;
+ }
+ }
+ if (!cre_lem.isNull())
+ {
+ if (std::find(lems.begin(), lems.end(), cre_lem) == lems.end())
+ {
+ Trace("sygus-cref-eval") << "...produced lemma : " << cre_lem
+ << std::endl;
+ lems.push_back(cre_lem);
+ }
+ }
+ }
+ }
+ }
+ }
+}
+
+bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
+ const 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") << " " << candidates[i] << " -> " << vals[i]
+ << std::endl;
+ }
+ }
+ Assert(vals.size() == candidates.size());
+ Node sbody = d_base_body.substitute(
+ candidates.begin(), 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, d_parent->getGuard().negate(), rlem);
+ lems.push_back(lem);
+ }
+ return true;
+ }
+ else
+ {
+ Trace("cegis-sample-debug") << "...duplicate." << std::endl;
+ }
+ }
+ }
+ }
+ return false;
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file cegis.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief cegis
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__CEGIS_H
+#define __CVC4__THEORY__QUANTIFIERS__CEGIS_H
+
+#include <map>
+#include "theory/quantifiers/sygus/sygus_module.h"
+#include "theory/quantifiers/sygus_sampler.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** Cegis
+ *
+ * The default sygus module for synthesis, counterexample-guided inductive
+ * synthesis (CEGIS).
+ *
+ * It initializes a list of sygus enumerators that are one-to-one with
+ * candidates, and returns a list of candidates that are the model values
+ * of these enumerators on calls to constructCandidates.
+ *
+ * It implements an optimization (getRefinementEvalLemmas) that evaluates all
+ * previous refinement lemmas for a term before returning it as a candidate
+ * in calls to constructCandidates.
+ */
+class Cegis : public SygusModule
+{
+ public:
+ Cegis(QuantifiersEngine* qe, CegConjecture* p);
+ ~Cegis() {}
+ /** initialize */
+ virtual bool initialize(Node n,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& lemmas) override;
+ /** get term list */
+ virtual void getTermList(const std::vector<Node>& candidates,
+ std::vector<Node>& enums) override;
+ /** construct candidate */
+ virtual bool constructCandidates(const std::vector<Node>& enums,
+ const std::vector<Node>& enum_values,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& candidate_values,
+ std::vector<Node>& lems) override;
+ /** register refinement lemma */
+ virtual void registerRefinementLemma(Node lem) override;
+
+ private:
+ /** If CegConjecture::d_base_inst is exists y. P( d, y ), then this is y. */
+ std::vector<Node> d_base_vars;
+ /**
+ * If CegConjecture::d_base_inst is exists y. P( d, y ), then this is the
+ * formula P( CegConjecture::d_candidates, y ).
+ */
+ Node d_base_body;
+
+ //-----------------------------------refinement lemmas
+ /** refinement lemmas */
+ std::vector<Node> d_refinement_lemmas;
+ /** get number of refinement lemmas we have added so far */
+ unsigned getNumRefinementLemmas() { return d_refinement_lemmas.size(); }
+ /** get refinement lemma
+ *
+ * If d_embed_quant is forall d. exists y. P( d, y ), then a refinement
+ * lemma is one of the form ~P( d_candidates, c ) for some c.
+ */
+ Node getRefinementLemma(unsigned i) { return d_refinement_lemmas[i]; }
+ /** sample add refinement lemma
+ *
+ * This function will check if there is a sample point in d_sampler that
+ * refutes the candidate solution (d_quant_vars->vals). If so, it adds a
+ * refinement lemma to the lists d_refinement_lemmas that corresponds to that
+ * sample point, and adds a lemma to lems if cegisSample mode is not trust.
+ */
+ bool sampleAddRefinementLemma(const std::vector<Node>& candidates,
+ const std::vector<Node>& vals,
+ std::vector<Node>& lems);
+ //-----------------------------------end refinement lemmas
+
+ /** Get refinement evaluation lemmas
+ *
+ * Given a candidate solution ms for candidates vs, this function adds lemmas
+ * to lems based on evaluating the conjecture, instantiated for ms, on lemmas
+ * for previous refinements (d_refinement_lemmas).
+ */
+ void getRefinementEvalLemmas(const std::vector<Node>& vs,
+ const std::vector<Node>& ms,
+ std::vector<Node>& lems);
+ /** sampler object for the option cegisSample()
+ *
+ * This samples points of the type of the inner variables of the synthesis
+ * conjecture (d_base_vars).
+ */
+ SygusSampler d_cegis_sampler;
+ /** cegis sample refine points
+ *
+ * Stores the list of indices of sample points in d_cegis_sampler we have
+ * added as refinement lemmas.
+ */
+ std::unordered_set<unsigned> d_cegis_sample_refine;
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__CEGIS_H */
--- /dev/null
+/********************* */
+/*! \file sygus_module.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of sygus_module
+ **/
+
+#include "theory/quantifiers/sygus/sygus_module.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+SygusModule::SygusModule(QuantifiersEngine* qe, CegConjecture* p)
+ : d_qe(qe), d_parent(p)
+{
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file sygus_module.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief sygus_module
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
+
+#include <map>
+#include "expr/node.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class CegConjecture;
+
+/** SygusModule
+ *
+ * This is the base class of sygus modules, owned by CegConjecture. The purpose
+ * of this class is to, when applicable, suggest candidate solutions for
+ * CegConjecture to test.
+ *
+ * In more detail, an instance of the conjecture class (CegConjecture) creates
+ * the negated deep embedding form of the synthesis conjecture. In the
+ * following, assume this is:
+ * forall d. exists x. P( d, x )
+ * where d are of sygus datatype type. The "base instantiation" of this
+ * conjecture (see CegConjecture::d_base_inst) is the formula:
+ * exists y. P( k, y )
+ * where k are the "candidate" variables for the conjecture.
+ *
+ * Modules implement an initialize function, which determines whether the module
+ * will take responsibility for the given conjecture.
+ */
+class SygusModule
+{
+ public:
+ SygusModule(QuantifiersEngine* qe, CegConjecture* p);
+ ~SygusModule() {}
+ /** initialize
+ *
+ * n is the "base instantiation" of the deep-embedding version of the
+ * synthesis conjecture under candidates (see CegConjecture::d_base_inst).
+ *
+ * This function may add lemmas to the argument lemmas, which should be
+ * sent out on the output channel of quantifiers by the caller.
+ *
+ * This function returns true if this module will take responsibility for
+ * constructing candidates for the given conjecture.
+ */
+ virtual bool initialize(Node n,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& lemmas) = 0;
+ /** get term list
+ *
+ * This gets the list of terms that will appear as arguments to a subsequent
+ * call to constructCandidates.
+ */
+ virtual void getTermList(const std::vector<Node>& candidates,
+ std::vector<Node>& terms) = 0;
+ /** construct candidate
+ *
+ * This function takes as input:
+ * terms : the terms returned by a call to getTermList,
+ * term_values : the current model values of terms,
+ * candidates : the list of candidates.
+ *
+ * If this function returns true, it adds to candidate_values a list of terms
+ * of the same length and type as candidates that are candidate solutions
+ * to the synthesis conjecture in question. This candidate { v } will then be
+ * tested by testing the (un)satisfiablity of P( v, k' ) for fresh k' by the
+ * caller.
+ *
+ * This function may also add lemmas to lems, which are sent out as lemmas
+ * on the output channel of quantifiers by the caller. For an example of
+ * such lemmas, see SygusPbe::constructCandidates.
+ *
+ * This function may return false if it does not have a candidate it wants
+ * to test on this iteration. In this case, lems should be non-empty.
+ */
+ virtual bool constructCandidates(const std::vector<Node>& terms,
+ const std::vector<Node>& term_values,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& candidate_values,
+ std::vector<Node>& lems) = 0;
+ /** register refinement lemma
+ *
+ * Assume this module, on a previous call to constructCandidates, added the
+ * value { v } to candidate_values for candidates = { k }. This function is
+ * called if the base instantiation of the synthesis conjecture has a model
+ * under this substitution. In particular, in the above example, this function
+ * is called when the refinement lemma P( v, k' ) has a model. The argument
+ * lem in the call to this function is P( v, k' ).
+ */
+ virtual void registerRefinementLemma(Node lem) {}
+ protected:
+ /** reference to quantifier engine */
+ QuantifiersEngine* d_qe;
+ /** reference to the parent conjecture */
+ CegConjecture* d_parent;
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */
}
CegConjecturePbe::CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p)
- : d_qe(qe),
- d_parent(p){
+ : SygusModule(qe, p)
+{
d_tds = d_qe->getTermDatabaseSygus();
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
}
}
-void CegConjecturePbe::initialize(Node n,
- std::vector<Node>& candidates,
+bool CegConjecturePbe::initialize(Node n,
+ const std::vector<Node>& candidates,
std::vector<Node>& lemmas)
{
Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
}
}
}
- if( !d_is_pbe ){
- Trace("sygus-unif") << "Do not do PBE optimizations, register..." << std::endl;
- for( unsigned i=0; i<candidates.size(); i++ ){
- d_qe->getTermDatabaseSygus()->registerEnumerator(
- candidates[i], candidates[i], d_parent);
- }
- }
+ return d_is_pbe;
}
Node CegConjecturePbe::PbeTrie::addPbeExample(TypeNode etn, Node e, Node b,
// ------------------------------------------- solution construction from enumeration
-void CegConjecturePbe::getCandidateList( std::vector< Node >& candidates, std::vector< Node >& clist ) {
+void CegConjecturePbe::getTermList(const std::vector<Node>& candidates,
+ std::vector<Node>& terms)
+{
Valuation& valuation = d_qe->getValuation();
for( unsigned i=0; i<candidates.size(); i++ ){
Node v = candidates[i];
Node gstatus = valuation.getSatValue(it->second.d_active_guard);
if (!gstatus.isNull() && gstatus.getConst<bool>())
{
- clist.push_back( e );
+ terms.push_back(e);
}
}
}
}
}
-bool CegConjecturePbe::constructCandidates( std::vector< Node >& enums, std::vector< Node >& enum_values,
- std::vector< Node >& candidates, std::vector< Node >& candidate_values,
- std::vector< Node >& lems ) {
+bool CegConjecturePbe::constructCandidates(const std::vector<Node>& enums,
+ const std::vector<Node>& enum_values,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& candidate_values,
+ std::vector<Node>& lems)
+{
Assert( enums.size()==enum_values.size() );
if( !enums.empty() ){
unsigned min_term_size = 0;
#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_PBE_H
#include "context/cdhashmap.h"
-#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/sygus/sygus_module.h"
namespace CVC4 {
namespace theory {
* This class is not designed to work in incremental mode, since there is no way
* to specify incremental problems in SyguS.
*/
-class CegConjecturePbe {
+class CegConjecturePbe : public SygusModule
+{
public:
CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p);
~CegConjecturePbe();
/** initialize this class
*
- * n is the "base instantiation" of the deep-embedding version of
- * the synthesis conjecture under "candidates".
- * (see CegConjecture::d_base_inst)
- *
* This function may add lemmas to the vector lemmas corresponding
* to initial lemmas regarding static analysis of enumerators it
* introduced. For example, we may say that the top-level symbol
* of an enumerator is not ITE if it is being used to construct
* return values for decision trees.
*/
- void initialize(Node n,
- std::vector<Node>& candidates,
- std::vector<Node>& lemmas);
- /** get candidate list
+ bool initialize(Node n,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& lemmas) override;
+ /** get term list
+ *
* Adds all active enumerators associated with functions-to-synthesize in
- * candidates to clist.
+ * candidates to terms.
*/
- void getCandidateList(std::vector<Node>& candidates,
- std::vector<Node>& clist);
+ void getTermList(const std::vector<Node>& candidates,
+ std::vector<Node>& terms) override;
/** construct candidates
- * (1) Indicates that the list of enumerators in "enums" currently have model
- * values "enum_values".
- * (2) Asks whether based on these new enumerated values, we can construct a
- * solution for
- * the functions-to-synthesize in "candidates". If so, this function
- * returns "true" and
- * adds solutions for candidates into "candidate_values".
- * During this class, this class may add auxiliary lemmas to "lems", which the
- * caller should send on the output channel via lemma(...).
- */
- bool constructCandidates(std::vector<Node>& enums,
- std::vector<Node>& enum_values,
- std::vector<Node>& candidates,
+ *
+ * This function attempts to use unification-based approaches for constructing
+ * solutions for all functions-to-synthesize (indicated by candidates). These
+ * approaches include decision tree learning and a divide-and-conquer
+ * algorithm based on string concatenation.
+ *
+ * Calls to this function are such that terms is the list of active
+ * enumerators (returned by getTermList), and term_values are their current
+ * model values. This function registers { terms -> terms_values } in
+ * the database of values that have been enumerated, which are in turn used
+ * for constructing candidate solutions when possible.
+ *
+ * This function also excludes models where (terms = terms_values) by adding
+ * blocking clauses to lems. For example, for grammar:
+ * A -> A+A | x | 1 | 0
+ * and a call where terms = { d } and term_values = { +( x, 1 ) }, it adds:
+ * ~G V ~is_+( d ) V ~is_x( d.1 ) V ~is_1( d.2 )
+ * to lems, where G is active guard of the enumerator d (see
+ * TermDatabaseSygus::getActiveGuardForEnumerator). This blocking clause
+ * indicates that d should not be given the model value +( x, 1 ) anymore,
+ * since { d -> +( x, 1 ) } has now been added to the database of this class.
+ */
+ bool constructCandidates(const std::vector<Node>& terms,
+ const std::vector<Node>& term_values,
+ const std::vector<Node>& candidates,
std::vector<Node>& candidate_values,
- std::vector<Node>& lems);
+ std::vector<Node>& lems) override;
/** is PBE enabled for any enumerator? */
bool isPbe() { return d_is_pbe; }
/** is the enumerator e associated with I/O example pairs? */
Node evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i);
private:
- /** quantifiers engine associated with this class */
- QuantifiersEngine* d_qe;
/** sygus term database of d_qe */
quantifiers::TermDbSygus * d_tds;
/** true and false nodes */
Node d_true;
Node d_false;
- /** A reference to the conjecture that owns this class. */
- CegConjecture* d_parent;
/** is this a PBE conjecture for any function? */
bool d_is_pbe;
/** for each candidate variable f (a function-to-synthesize), whether the
projects / cvc5.git / commitdiff