From: Andrew Reynolds Date: Tue, 18 Sep 2018 15:26:36 +0000 (-0500) Subject: Move and rename sygus solver classes (#2488) X-Git-Tag: cvc5-1.0.0~4633 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fa557c39a89a2c8de198ea0400e6936c1790ad4e;p=cvc5.git Move and rename sygus solver classes (#2488) --- diff --git a/src/Makefile.am b/src/Makefile.am index bdba671ca..77cfccda5 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -532,10 +532,6 @@ libcvc4_la_SOURCES = \ theory/quantifiers/sygus/cegis.h \ theory/quantifiers/sygus/cegis_unif.cpp \ theory/quantifiers/sygus/cegis_unif.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/ce_guided_instantiation.h \ theory/quantifiers/sygus/ce_guided_single_inv.cpp \ theory/quantifiers/sygus/ce_guided_single_inv.h \ theory/quantifiers/sygus/sygus_pbe.cpp \ @@ -568,6 +564,10 @@ libcvc4_la_SOURCES = \ theory/quantifiers/sygus/sygus_unif_rl.h \ theory/quantifiers/sygus/sygus_unif_strat.cpp \ theory/quantifiers/sygus/sygus_unif_strat.h \ + theory/quantifiers/sygus/synth_conjecture.cpp \ + theory/quantifiers/sygus/synth_conjecture.h \ + theory/quantifiers/sygus/synth_engine.cpp \ + theory/quantifiers/sygus/synth_engine.h \ theory/quantifiers/sygus/term_database_sygus.cpp \ theory/quantifiers/sygus/term_database_sygus.h \ theory/quantifiers/sygus_sampler.cpp \ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b4bc0b8dc..15f8280b5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -127,7 +127,7 @@ #include "theory/quantifiers/fun_def_process.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/single_inv_partition.h" -#include "theory/quantifiers/sygus/ce_guided_instantiation.h" +#include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" #include "theory/sort_inference.h" @@ -3182,7 +3182,9 @@ void SmtEnginePrivate::processAssertions() { if( options::ceGuidedInst() ){ //register sygus conjecture pre-rewrite (motivated by solution reconstruction) for (unsigned i = 0; i < d_assertions.size(); ++ i) { - d_smt.d_theoryEngine->getQuantifiersEngine()->getCegInstantiation()->preregisterAssertion( d_assertions[i] ); + d_smt.d_theoryEngine->getQuantifiersEngine() + ->getSynthEngine() + ->preregisterAssertion(d_assertions[i]); } } diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 82aa570c2..db1ce1c05 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -22,7 +22,6 @@ #include "printer/printer.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes.h" -#include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/sygus_explain.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" @@ -313,11 +312,11 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std: // static conjecture-dependent symmetry breaking Trace("sygus-sb-debug") << " conjecture-dependent symmetry breaking...\n"; - std::map::iterator itc = + std::map::iterator itc = d_anchor_to_conj.find(a); if (itc != d_anchor_to_conj.end()) { - quantifiers::CegConjecture* conj = itc->second; + quantifiers::SynthConjecture* conj = itc->second; Assert(conj != NULL); Node dpred = conj->getSymmetryBreakingPredicate(x, a, ntn, tindex, ds); if (!dpred.isNull()) @@ -803,7 +802,7 @@ Node SygusSymBreakNew::registerSearchValue( d_cache[a].d_search_val_proc.insert(cnv); // get the root (for PBE symmetry breaking) Assert(d_anchor_to_conj.find(a) != d_anchor_to_conj.end()); - quantifiers::CegConjecture* aconj = d_anchor_to_conj[a]; + quantifiers::SynthConjecture* aconj = d_anchor_to_conj[a]; Assert(aconj != NULL); Trace("sygus-sb-debug") << " ...register search value " << cnv << ", type=" << tn << std::endl; @@ -827,9 +826,9 @@ Node SygusSymBreakNew::registerSearchValue( bool by_examples = false; if( itsv==d_cache[a].d_search_val[tn].end() ){ // TODO (github #1210) conjecture-specific symmetry breaking - // this should be generalized and encapsulated within the CegConjecture - // class - // is it equivalent under examples? + // this should be generalized and encapsulated within the + // SynthConjecture class. + // Is it equivalent under examples? Node bvr_equiv; if (options::sygusSymBreakPbe()) { diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index e2ed4192a..99f9672e7 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -30,8 +30,8 @@ #include "expr/datatype.h" #include "expr/node.h" #include "theory/datatypes/sygus_simple_sym.h" -#include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/sygus_explain.h" +#include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus_sampler.h" #include "theory/quantifiers/term_database.h" @@ -152,7 +152,7 @@ class SygusSymBreakNew /** * Map from anchors to the conjecture they are associated with. */ - std::map d_anchor_to_conj; + std::map d_anchor_to_conj; /** * Map from terms (selector chains) to their depth. The depth of a selector * chain S1( ... Sn( x ) ... ) is: @@ -229,7 +229,7 @@ private: * (2) static symmetry breaking clauses for subterms of n (those added to * lemmas on getSimpleSymBreakPred, see function below), * (3) conjecture-specific symmetry breaking lemmas, see - * CegConjecture::getSymmetryBreakingPredicate, + * SynthConjecture::getSymmetryBreakingPredicate, * (4) fairness conflicts if sygusFair() is SYGUS_FAIR_DIRECT, e.g.: * size( d ) <= 1 V ~is-C1( d ) V ~is-C2( d.1 ) * where C1 and C2 are non-nullary constructors. diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 3b7aab0b2..bba5b3c18 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -20,9 +20,9 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" -#include "theory/quantifiers/sygus/ce_guided_instantiation.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index dde6dc4a9..ff906a95b 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -17,7 +17,7 @@ #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/rewrite_engine.h" -#include "theory/quantifiers/sygus/ce_guided_instantiation.h" +#include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" @@ -229,10 +229,11 @@ void QuantAttributes::computeAttributes( Node q ) { d_fun_defs[f] = true; } if( d_qattr[q].d_sygus ){ - if( d_quantEngine->getCegInstantiation()==NULL ){ + if (d_quantEngine->getSynthEngine() == nullptr) + { Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl; } - d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation(), 2 ); + d_quantEngine->setOwner(q, d_quantEngine->getSynthEngine(), 2); } } diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp deleted file mode 100644 index 30c0a3ae1..000000000 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ /dev/null @@ -1,900 +0,0 @@ -/********************* */ -/*! \file ce_guided_conjecture.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Haniel Barbosa - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 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 class that encapsulates counterexample-guided instantiation - ** techniques for a single SyGuS synthesis conjecture - **/ -#include "theory/quantifiers/sygus/ce_guided_conjecture.h" - -#include "expr/datatype.h" -#include "options/base_options.h" -#include "options/datatypes_options.h" -#include "options/quantifiers_options.h" -#include "printer/printer.h" -#include "prop/prop_engine.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "smt/smt_statistics_registry.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/sygus/ce_guided_instantiation.h" -#include "theory/quantifiers/sygus/term_database_sygus.h" -#include "theory/quantifiers/term_util.h" -#include "theory/theory_engine.h" - -using namespace CVC4::kind; -using namespace std; - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -CegConjecture::CegConjecture(QuantifiersEngine* qe) - : d_qe(qe), - d_ceg_si(new CegConjectureSingleInv(qe, this)), - d_ceg_proc(new CegConjectureProcess(qe)), - d_ceg_gc(new CegGrammarConstructor(qe, this)), - d_sygus_rconst(new SygusRepairConst(qe)), - d_ceg_pbe(new CegConjecturePbe(qe, this)), - d_ceg_cegis(new Cegis(qe, this)), - d_ceg_cegisUnif(new CegisUnif(qe, this)), - d_master(nullptr), - d_set_ce_sk_vars(false), - d_repair_index(0), - d_refine_count(0) -{ - if (options::sygusSymBreakPbe() || options::sygusUnifPbe()) - { - d_modules.push_back(d_ceg_pbe.get()); - } - if (options::sygusUnif()) - { - d_modules.push_back(d_ceg_cegisUnif.get()); - } - d_modules.push_back(d_ceg_cegis.get()); -} - -CegConjecture::~CegConjecture() {} - -void CegConjecture::assign( Node q ) { - Assert( d_embed_quant.isNull() ); - Assert( q.getKind()==FORALL ); - Trace("cegqi") << "CegConjecture : assign : " << q << std::endl; - d_quant = q; - NodeManager* nm = NodeManager::currentNM(); - - // pre-simplify the quantified formula based on the process utility - d_simp_quant = d_ceg_proc->preSimplify(d_quant); - - std::map< Node, Node > templates; - std::map< Node, Node > templates_arg; - //register with single invocation if applicable - if (d_qe->getQuantAttributes()->isSygus(q)) - { - d_ceg_si->initialize(d_simp_quant); - d_simp_quant = d_ceg_si->getSimplifiedConjecture(); - // carry the templates - for( unsigned i=0; igetTemplate(v); - if( !templ.isNull() ){ - templates[v] = templ; - templates_arg[v] = d_ceg_si->getTemplateArg(v); - } - } - } - - // post-simplify the quantified formula based on the process utility - d_simp_quant = d_ceg_proc->postSimplify(d_simp_quant); - - // finished simplifying the quantified formula at this point - - // convert to deep embedding and finalize single invocation here - d_embed_quant = d_ceg_gc->process(d_simp_quant, templates, templates_arg); - Trace("cegqi") << "CegConjecture : converted to embedding : " << d_embed_quant << std::endl; - - // we now finalize the single invocation module, based on the syntax restrictions - if (d_qe->getQuantAttributes()->isSygus(q)) - { - d_ceg_si->finishInit(d_ceg_gc->isSyntaxRestricted()); - } - - Assert( d_candidates.empty() ); - std::vector< Node > vars; - for( unsigned i=0; imkSkolem( "e", d_embed_quant[0][i].getType() ); - d_candidates.push_back( e ); - } - Trace("cegqi") << "Base quantified formula is : " << d_embed_quant << std::endl; - //construct base instantiation - 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; - - // initialize the sygus constant repair utility - if (options::sygusRepairConst()) - { - d_sygus_rconst->initialize(d_base_inst.negate(), d_candidates); - if (options::sygusConstRepairAbort()) - { - if (!d_sygus_rconst->isActive()) - { - // no constant repair is possible: abort - std::stringstream ss; - ss << "Grammar does not allow repair constants." << std::endl; - throw LogicException(ss.str()); - } - } - } - - // 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); - 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); - } - - Assert(d_qe->getQuantAttributes()->isSygus(q)); - // 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); - } - } - - // initialize the guard - d_feasible_guard = nm->mkSkolem("G", nm->booleanType()); - d_feasible_guard = Rewriter::rewrite(d_feasible_guard); - d_feasible_guard = d_qe->getValuation().ensureLiteral(d_feasible_guard); - AlwaysAssert(!d_feasible_guard.isNull()); - // register the strategy - d_feasible_strategy.reset( - new DecisionStrategySingleton("sygus_feasible", - d_feasible_guard, - d_qe->getSatContext(), - d_qe->getValuation())); - d_qe->getTheoryEngine()->getDecisionManager()->registerStrategy( - DecisionManager::STRAT_QUANT_SYGUS_FEASIBLE, d_feasible_strategy.get()); - // this must be called, both to ensure that the feasible guard is - // decided on with true polariy, but also to ensure that output channel - // has been used on this call to check. - d_qe->getOutputChannel().requirePhase(d_feasible_guard, true); - - if (isSingleInvocation()) - { - std::vector< Node > lems; - d_ceg_si->getInitialSingleInvLemma(d_feasible_guard, lems); - for( unsigned i=0; igetOutputChannel().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; imkNode(OR, gneg, guarded_lemmas[i]); - Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem << std::endl; - d_qe->getOutputChannel().lemma( lem ); - } - - if (options::sygusStream()) - { - d_stream_strategy.reset(new SygusStreamDecisionStrategy( - d_qe->getSatContext(), d_qe->getValuation())); - d_qe->getTheoryEngine()->getDecisionManager()->registerStrategy( - DecisionManager::STRAT_QUANT_SYGUS_STREAM_FEASIBLE, - d_stream_strategy.get()); - d_current_stream_guard = d_stream_strategy->getLiteral(0); - } - Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() << std::endl; -} - -Node CegConjecture::getGuard() const { return d_feasible_guard; } - -bool CegConjecture::isSingleInvocation() const { - return d_ceg_si->isSingleInvocation(); -} - -bool CegConjecture::needsCheck() -{ - if( isSingleInvocation() && !d_ceg_si->needsCheck() ){ - return false; - } - bool value; - Assert(!d_feasible_guard.isNull()); - // non or fully single invocation : look at guard only - if (d_qe->getValuation().hasSatValue(d_feasible_guard, value)) - { - if (!value) - { - Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl; - return false; - } - } - else - { - Trace("cegqi-warn") << "WARNING: Guard " << d_feasible_guard - << " is not assigned!" << std::endl; - Assert(false); - } - return true; -} - - -void CegConjecture::doSingleInvCheck(std::vector< Node >& lems) { - if( d_ceg_si!=NULL ){ - d_ceg_si->check(lems); - } -} - -bool CegConjecture::needsRefinement() const { return d_set_ce_sk_vars; } -void CegConjecture::doCheck(std::vector& lems) -{ - Assert(d_master != nullptr); - - // process the sygus streaming guard - if (options::sygusStream()) - { - Assert(!isSingleInvocation()); - // it may be the case that we have a new solution now - Node currGuard = getCurrentStreamGuard(); - if (currGuard != d_current_stream_guard) - { - // we have a new guard, print and continue the stream - printAndContinueStream(); - d_current_stream_guard = currGuard; - return; - } - } - - // get the list of terms that the master strategy is interested in - std::vector terms; - d_master->getTermList(d_candidates, terms); - - Assert(!d_candidates.empty()); - - Trace("cegqi-check") << "CegConjuncture : check, build candidates..." - << std::endl; - std::vector candidate_values; - bool constructed_cand = false; - - // If a module is not trying to repair constants in solutions and the option - // sygusRepairConst is true, we use a default scheme for trying to repair - // constants here. - if (options::sygusRepairConst() && !d_master->usingRepairConst()) - { - // have we tried to repair the previous solution? - // if not, call the repair constant utility - unsigned ninst = d_cinfo[d_candidates[0]].d_inst.size(); - if (d_repair_index < ninst) - { - std::vector fail_cvs; - for (const Node& cprog : d_candidates) - { - Assert(d_repair_index < d_cinfo[cprog].d_inst.size()); - fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]); - } - if (Trace.isOn("cegqi-check")) - { - Trace("cegqi-check") << "CegConjuncture : repair previous solution "; - for (const Node& fc : fail_cvs) - { - std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, fc); - Trace("cegqi-check") << ss.str() << " "; - } - Trace("cegqi-check") << std::endl; - } - d_repair_index++; - if (d_sygus_rconst->repairSolution( - d_candidates, fail_cvs, candidate_values, true)) - { - constructed_cand = true; - } - } - } - - // get the model value of the relevant terms from the master module - std::vector enum_values; - getModelValues(terms, enum_values); - - if (!constructed_cand) - { - Assert(candidate_values.empty()); - 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, size = candidate_values.size(); i < size; i++) - { - Trace("cegqi-check") << " " << i << " : " << d_candidates[i] << " -> " - << candidate_values[i] << std::endl; - } - } - 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) && 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. - Node lem = nm->mkNode(OR, d_quant.negate(), nm->mkConst(false)); - lem = getStreamGuardedLemma(lem); - lems.push_back(lem); - recordInstantiation(candidate_values); - return; - } - Assert(!d_set_ce_sk_vars); - }else{ - if( !constructed_cand ){ - return; - } - } - - //immediately skolemize inner existentials - Node lem; - // introduce the skolem variables - std::vector sks; - if (constructed_cand) - { - if (inst.getKind() == NOT && inst[0].getKind() == FORALL) - { - std::vector vars; - for (const Node& v : inst[0][0]) - { - Node sk = nm->mkSkolem("rsk", v.getType()); - sks.push_back(sk); - vars.push_back(v); - Trace("cegqi-check-debug") - << " introduce skolem " << sk << " for " << v << "\n"; - } - lem = inst[0][1].substitute( - vars.begin(), vars.end(), sks.begin(), sks.end()); - lem = lem.negate(); - } - else - { - // use the instance itself - lem = inst; - } - } - if (sk_refine) - { - d_ce_sk_vars.insert(d_ce_sk_vars.end(), sks.begin(), sks.end()); - d_set_ce_sk_vars = true; - } - - if (lem.isNull()) - { - // no lemma to check - return; - } - - lem = Rewriter::rewrite(lem); - // eagerly unfold applications of evaluation function - Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl; - std::map visited_n; - lem = d_qe->getTermDatabaseSygus()->getEagerUnfold(lem, visited_n); - // record the instantiation - // this is used for remembering the solution - recordInstantiation(candidate_values); - Node query = lem; - bool success = false; - if (query.isConst() && !query.getConst()) - { - // short circuit the check - lem = d_quant.negate(); - success = true; - } - 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(), query); - if (options::sygusVerifySubcall()) - { - Trace("cegqi-engine") << " *** Verify with subcall..." << std::endl; - SmtEngine verifySmt(nm->toExprManager()); - verifySmt.setLogic(smt::currentSmtEngine()->getLogicInfo()); - verifySmt.assertFormula(query.toExpr()); - Result r = verifySmt.checkSat(); - Trace("cegqi-engine") << " ...got " << r << std::endl; - if (r.asSatisfiabilityResult().isSat() == Result::SAT) - { - Trace("cegqi-engine") << " * Verification lemma failed for:\n "; - // do not send out - for (const Node& v : d_ce_sk_vars) - { - Node mv = Node::fromExpr(verifySmt.getValue(v.toExpr())); - Trace("cegqi-engine") << v << " -> " << mv << " "; - d_ce_sk_var_mvs.push_back(mv); - } - Trace("cegqi-engine") << std::endl; -#ifdef CVC4_ASSERTIONS - // the values for the query should be a complete model - Node squery = query.substitute(d_ce_sk_vars.begin(), - d_ce_sk_vars.end(), - d_ce_sk_var_mvs.begin(), - d_ce_sk_var_mvs.end()); - Trace("cegqi-debug") << "...squery : " << squery << std::endl; - squery = Rewriter::rewrite(squery); - Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl; - Assert(squery.isConst() && squery.getConst()); -#endif - return; - } - else if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) - { - // if the result in the subcall was unsatisfiable, we avoid - // rechecking, hence we drop "query" from the verification lemma - lem = d_quant.negate(); - // we can short circuit adding the lemma (for sygus stream) - success = true; - } - // In the rare case that the subcall is unknown, we add the verification - // lemma in the main solver. This should only happen if the quantifier - // free logic is undecidable. - } - } - if (success && 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; - } - lem = getStreamGuardedLemma(lem); - lems.push_back(lem); -} - -void CegConjecture::doRefine( std::vector< Node >& lems ){ - Assert( lems.empty() ); - Assert(d_set_ce_sk_vars); - - //first, make skolem substitution - Trace("cegqi-refine") << "doRefine : construct skolem substitution..." << std::endl; - std::vector< Node > sk_vars; - std::vector< Node > sk_subs; - //collect the substitution over all disjuncts - if (!d_ce_sk_vars.empty()) - { - Trace("cegqi-refine") << "Get model values for skolems..." << std::endl; - Assert(d_inner_vars.size() == d_ce_sk_vars.size()); - if (d_ce_sk_var_mvs.empty()) - { - std::vector model_values; - getModelValues(d_ce_sk_vars, model_values); - sk_subs.insert(sk_subs.end(), model_values.begin(), model_values.end()); - } - else - { - Assert(d_ce_sk_var_mvs.size() == d_ce_sk_vars.size()); - sk_subs.insert( - sk_subs.end(), d_ce_sk_var_mvs.begin(), d_ce_sk_var_mvs.end()); - } - sk_vars.insert(sk_vars.end(), d_inner_vars.begin(), d_inner_vars.end()); - } - else - { - Assert(d_inner_vars.empty()); - } - - std::vector< Node > lem_c; - Trace("cegqi-refine") << "doRefine : Construct refinement lemma..." << std::endl; - Trace("cegqi-refine-debug") - << " For counterexample skolems : " << d_ce_sk_vars << std::endl; - Node base_lem; - if (d_base_inst.getKind() == NOT && d_base_inst[0].getKind() == FORALL) - { - base_lem = d_base_inst[0][1]; - } - else - { - base_lem = d_base_inst.negate(); - } - - Assert( sk_vars.size()==sk_subs.size() ); - - Trace("cegqi-refine") << "doRefine : substitute..." << std::endl; - base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); - Trace("cegqi-refine") << "doRefine : rewrite..." << std::endl; - base_lem = Rewriter::rewrite( base_lem ); - Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem - << "..." << std::endl; - d_master->registerRefinementLemma(sk_vars, base_lem, lems); - Trace("cegqi-refine") << "doRefine : finished" << std::endl; - d_set_ce_sk_vars = false; - d_ce_sk_vars.clear(); - d_ce_sk_var_mvs.clear(); -} - -void CegConjecture::preregisterConjecture( Node q ) { - d_ceg_si->preregisterConjecture( q ); -} - -void CegConjecture::getModelValues( std::vector< Node >& n, std::vector< Node >& v ) { - Trace("cegqi-engine") << " * Value is : "; - for( unsigned i=0; i "; - std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, nv); - Trace("cegqi-engine") << ss.str() << " "; - if (Trace.isOn("cegqi-engine-rr")) - { - Node bv = d_qe->getTermDatabaseSygus()->sygusToBuiltin(nv, tn); - bv = Rewriter::rewrite(bv); - Trace("cegqi-engine-rr") << " -> " << bv << std::endl; - } - } - Assert( !nv.isNull() ); - } - Trace("cegqi-engine") << std::endl; -} - -Node CegConjecture::getModelValue( Node n ) { - Trace("cegqi-mv") << "getModelValue for : " << n << std::endl; - return d_qe->getModel()->getValue( n ); -} - -void CegConjecture::debugPrint( const char * c ) { - Trace(c) << "Synthesis conjecture : " << d_embed_quant << std::endl; - Trace(c) << " * Candidate programs : " << d_candidates << std::endl; - Trace(c) << " * Counterexample skolems : " << d_ce_sk_vars << std::endl; -} - -Node CegConjecture::getCurrentStreamGuard() const { - if (d_stream_strategy != nullptr) - { - // the stream guard is the current asserted literal of the stream strategy - Node lit = d_stream_strategy->getAssertedLiteral(); - if (lit.isNull()) - { - // if none exist, get the first - lit = d_stream_strategy->getLiteral(0); - } - return lit; - } - return Node::null(); -} - -Node CegConjecture::getStreamGuardedLemma(Node n) const -{ - if (options::sygusStream()) - { - // if we are in streaming mode, we guard with the current stream guard - Node csg = getCurrentStreamGuard(); - Assert(!csg.isNull()); - return NodeManager::currentNM()->mkNode(kind::OR, csg.negate(), n); - } - return n; -} - -CegConjecture::SygusStreamDecisionStrategy::SygusStreamDecisionStrategy( - context::Context* satContext, Valuation valuation) - : DecisionStrategyFmf(satContext, valuation) -{ -} - -Node CegConjecture::SygusStreamDecisionStrategy::mkLiteral(unsigned i) -{ - NodeManager* nm = NodeManager::currentNM(); - Node curr_stream_guard = nm->mkSkolem("G_Stream", nm->booleanType()); - return curr_stream_guard; -} - -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_set_ce_sk_vars = false; - d_ce_sk_vars.clear(); - d_ce_sk_var_mvs.clear(); - // However, we need to exclude the current solution using an explicit - // blocking clause, so that we proceed to the next solution. - std::vector terms; - d_master->getTermList(d_candidates, terms); - std::vector 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()->getExplanationForEquality( - 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() ); - std::vector sols; - std::vector statuses; - if (!getSynthSolutionsInternal(sols, statuses, singleInvocation)) - { - return; - } - for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) - { - Node sol = sols[i]; - if (!sol.isNull()) - { - Node prog = d_embed_quant[0][i]; - int status = statuses[i]; - TypeNode tn = prog.getType(); - const Datatype& dt = static_cast(tn.toType()).getDatatype(); - std::stringstream ss; - ss << prog; - std::string f(ss.str()); - f.erase(f.begin()); - CegInstantiation* cei = d_qe->getCegInstantiation(); - ++(cei->d_statistics.d_solutions); - - bool is_unique_term = true; - - if (status != 0 && options::sygusRewSynth()) - { - std::map::iterator its = - d_exprm.find(prog); - if (its == d_exprm.end()) - { - d_exprm[prog].initializeSygus( - d_qe, d_candidates[i], options::sygusSamples(), true); - if (options::sygusRewSynth()) - { - d_exprm[prog].enableRewriteRuleSynth(); - } - its = d_exprm.find(prog); - } - bool rew_print = false; - is_unique_term = d_exprm[prog].addTerm(sol, out, rew_print); - if (rew_print) - { - ++(cei->d_statistics.d_candidate_rewrites_print); - } - if (!is_unique_term) - { - ++(cei->d_statistics.d_candidate_rewrites); - } - } - if (is_unique_term) - { - out << "(define-fun " << f << " "; - if (dt.getSygusVarList().isNull()) - { - out << "() "; - } - else - { - out << dt.getSygusVarList() << " "; - } - out << dt.getSygusType() << " "; - if (status == 0) - { - out << sol; - } - else - { - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(out, sol); - } - out << ")" << std::endl; - } - } - } -} - -void CegConjecture::getSynthSolutions(std::map& sol_map, - bool singleInvocation) -{ - NodeManager* nm = NodeManager::currentNM(); - TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus(); - std::vector sols; - std::vector statuses; - if (!getSynthSolutionsInternal(sols, statuses, singleInvocation)) - { - return; - } - for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) - { - Node sol = sols[i]; - int status = statuses[i]; - // get the builtin solution - Node bsol = sol; - if (status != 0) - { - // convert sygus to builtin here - bsol = sygusDb->sygusToBuiltin(sol, sol.getType()); - } - // convert to lambda - TypeNode tn = d_embed_quant[0][i].getType(); - const Datatype& dt = static_cast(tn.toType()).getDatatype(); - Node bvl = Node::fromExpr(dt.getSygusVarList()); - if (!bvl.isNull()) - { - bsol = nm->mkNode(LAMBDA, bvl, bsol); - } - // store in map - Node fvar = d_quant[0][i]; - Assert(fvar.getType() == bsol.getType()); - sol_map[fvar] = bsol; - } -} - -bool CegConjecture::getSynthSolutionsInternal(std::vector& sols, - std::vector& statuses, - bool singleInvocation) -{ - for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) - { - Node prog = d_embed_quant[0][i]; - Trace("cegqi-debug") << " get solution for " << prog << std::endl; - TypeNode tn = prog.getType(); - Assert(tn.isDatatype()); - // get the solution - Node sol; - int status = -1; - if (singleInvocation) - { - Assert(d_ceg_si != NULL); - sol = d_ceg_si->getSolution(i, tn, status, true); - if (sol.isNull()) - { - return false; - } - sol = sol.getKind() == LAMBDA ? sol[1] : sol; - } - else - { - Node cprog = getCandidate(i); - if (!d_cinfo[cprog].d_inst.empty()) - { - // the solution is just the last instantiated term - sol = d_cinfo[cprog].d_inst.back(); - status = 1; - - // check if there was a template - Node sf = d_quant[0][i]; - Node templ = d_ceg_si->getTemplate(sf); - if (!templ.isNull()) - { - Trace("cegqi-inv-debug") - << sf << " used template : " << templ << std::endl; - // if it was not embedded into the grammar - if (!options::sygusTemplEmbedGrammar()) - { - TNode templa = d_ceg_si->getTemplateArg(sf); - // make the builtin version of the full solution - TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus(); - sol = sygusDb->sygusToBuiltin(sol, sol.getType()); - Trace("cegqi-inv") << "Builtin version of solution is : " << sol - << ", type : " << sol.getType() << std::endl; - TNode tsol = sol; - sol = templ.substitute(templa, tsol); - Trace("cegqi-inv-debug") << "With template : " << sol << std::endl; - sol = Rewriter::rewrite(sol); - Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl; - // now, reconstruct to the syntax - sol = d_ceg_si->reconstructToSyntax(sol, tn, status, true); - sol = sol.getKind() == LAMBDA ? sol[1] : sol; - Trace("cegqi-inv-debug") - << "Reconstructed to syntax : " << sol << std::endl; - } - else - { - Trace("cegqi-inv-debug") - << "...was embedding into grammar." << std::endl; - } - } - else - { - Trace("cegqi-inv-debug") - << sf << " did not use template" << std::endl; - } - } - else - { - Trace("cegqi-warn") << "WARNING : No recorded instantiations for " - "syntax-guided solution!" - << std::endl; - } - } - sols.push_back(sol); - statuses.push_back(status); - } - return true; -} - -Node CegConjecture::getSymmetryBreakingPredicate( - Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth) -{ - std::vector sb_lemmas; - - // based on simple preprocessing - Node ppred = - d_ceg_proc->getSymmetryBreakingPredicate(x, e, tn, tindex, depth); - if (!ppred.isNull()) - { - sb_lemmas.push_back(ppred); - } - - // other static conjecture-dependent symmetry breaking goes here - - if (!sb_lemmas.empty()) - { - return sb_lemmas.size() == 1 - ? sb_lemmas[0] - : NodeManager::currentNM()->mkNode(kind::AND, sb_lemmas); - } - else - { - return Node::null(); - } -} - -}/* namespace CVC4::theory::quantifiers */ -}/* namespace CVC4::theory */ -}/* namespace CVC4 */ diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h deleted file mode 100644 index adc75056e..000000000 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h +++ /dev/null @@ -1,291 +0,0 @@ -/********************* */ -/*! \file ce_guided_conjecture.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Haniel Barbosa - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 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 class that encapsulates counterexample-guided instantiation - ** techniques for a single SyGuS synthesis conjecture - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H -#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H - -#include - -#include "theory/decision_manager.h" -#include "theory/quantifiers/expr_miner_manager.h" -#include "theory/quantifiers/sygus/ce_guided_single_inv.h" -#include "theory/quantifiers/sygus/cegis.h" -#include "theory/quantifiers/sygus/cegis_unif.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/sygus_repair_const.h" -#include "theory/quantifiers_engine.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -/** a synthesis conjecture - * This class implements approaches for a synthesis conecjture, given by data - * member d_quant. - * This includes both approaches for synthesis in Reynolds et al CAV 2015. It - * determines which approach and optimizations are applicable to the - * conjecture, and has interfaces for implementing them. - */ -class CegConjecture { -public: - CegConjecture( QuantifiersEngine * qe ); - ~CegConjecture(); - /** get original version of conjecture */ - Node getConjecture() { return d_quant; } - /** get deep embedding version of conjecture */ - Node getEmbeddedConjecture() { return d_embed_quant; } - //-------------------------------for counterexample-guided check/refine - /** increment the number of times we have successfully done candidate - * refinement */ - void incrementRefineCount() { d_refine_count++; } - /** whether the conjecture is waiting for a call to doCheck below */ - 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< Node >& lems); - /** do syntax-guided enumerative check - * This is step 2(a) of Figure 3 of Reynolds et al CAV 2015. - */ - void doCheck(std::vector& lems); - /** do refinement - * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015. - */ - void doRefine(std::vector< Node >& lems); - //-------------------------------end for counterexample-guided check/refine - /** - * prints the synthesis solution to output stream out. - * - * singleInvocation : set to true if we should consult the single invocation - * module to get synthesis solutions. - */ - void printSynthSolution( std::ostream& out, bool singleInvocation ); - /** get synth solutions - * - * This returns a map from function-to-synthesize variables to their - * builtin solution, which has the same type. For example, for synthesis - * conjecture exists f. forall x. f( x )>x, this function may return the map - * containing the entry: - * f -> (lambda x. x+1) - * - * singleInvocation : set to true if we should consult the single invocation - * module to get synthesis solutions. - */ - void getSynthSolutions(std::map& sol_map, bool singleInvocation); - /** - * The feasible guard whose semantics are "this conjecture is feasiable". - * This is "G" in Figure 3 of Reynolds et al CAV 2015. - */ - Node getGuard() const; - /** is ground */ - bool isGround() { return d_inner_vars.empty(); } - /** are we using single invocation techniques */ - bool isSingleInvocation() const; - /** preregister conjecture - * This is used as a heuristic for solution reconstruction, so that we - * remember expressions in the conjecture before preprocessing, since they - * may be helpful during solution reconstruction (Figure 5 of Reynolds et al CAV 2015) - */ - void preregisterConjecture( Node q ); - /** assign conjecture q to this class */ - void assign( Node q ); - /** has a conjecture been assigned to this class */ - bool isAssigned() { return !d_embed_quant.isNull(); } - /** get model values for terms n, store in vector v */ - void getModelValues( std::vector< Node >& n, std::vector< Node >& v ); - /** get model value for term n */ - Node getModelValue( Node n ); - - /** get utility for static preprocessing and analysis of conjectures */ - CegConjectureProcess* getProcess() { return d_ceg_proc.get(); } - /** get constant repair utility */ - SygusRepairConst* getRepairConst() { return d_sygus_rconst.get(); } - /** get program by examples module */ - CegConjecturePbe* getPbe() { return d_ceg_pbe.get(); } - /** get the symmetry breaking predicate for type */ - Node getSymmetryBreakingPredicate( - Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth); - /** print out debug information about this conjecture */ - void debugPrint( const char * c ); -private: - /** reference to quantifier engine */ - QuantifiersEngine * d_qe; - /** The feasible guard. */ - Node d_feasible_guard; - /** the decision strategy for the feasible guard */ - std::unique_ptr d_feasible_strategy; - /** single invocation utility */ - std::unique_ptr d_ceg_si; - /** utility for static preprocessing and analysis of conjectures */ - std::unique_ptr d_ceg_proc; - /** grammar utility */ - std::unique_ptr d_ceg_gc; - /** repair constant utility */ - std::unique_ptr d_sygus_rconst; - - //------------------------modules - /** program by examples module */ - std::unique_ptr d_ceg_pbe; - /** CEGIS module */ - std::unique_ptr d_ceg_cegis; - /** CEGIS UNIF module */ - std::unique_ptr d_ceg_cegisUnif; - /** the set of active modules (subset of the above list) */ - std::vector 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. - */ - std::vector< Node > d_candidates; - /** base instantiation - * If d_embed_quant is forall d. exists y. P( d, y ), then - * this is the formula exists y. P( d_candidates, y ). Notice that - * (exists y. F) is shorthand above for ~( forall y. ~F ). - */ - Node d_base_inst; - /** list of variables on inner quantification */ - std::vector< Node > d_inner_vars; - /** - * The set of skolems for the current "verification" lemma, if one exists. - * This may be added to during calls to doCheck(). The model values for these - * skolems are analyzed during doRefine(). - */ - std::vector d_ce_sk_vars; - /** - * If we have already tested the satisfiability of the current verification - * lemma, this stores the model values of d_ce_sk_vars in the current - * (satisfiable, failed) verification lemma. - */ - std::vector d_ce_sk_var_mvs; - /** - * Whether the above vector has been set. We have this flag since the above - * vector may be set to empty (e.g. for ground synthesis conjectures). - */ - bool d_set_ce_sk_vars; - - /** the asserted (negated) conjecture */ - Node d_quant; - /** (negated) conjecture after simplification */ - Node d_simp_quant; - /** (negated) conjecture after simplification, conversion to deep embedding */ - Node d_embed_quant; - /** candidate information */ - class CandidateInfo { - public: - CandidateInfo(){} - /** list of terms we have instantiated candidates with */ - std::vector< Node > d_inst; - }; - std::map d_cinfo; - /** - * The first index of an instantiation in CandidateInfo::d_inst that we have - * not yet tried to repair. - */ - unsigned d_repair_index; - /** number of times we have called doRefine */ - unsigned d_refine_count; - /** get candidadate */ - Node getCandidate( unsigned int i ) { return d_candidates[i]; } - /** record instantiation (this is used to construct solutions later) */ - void recordInstantiation( std::vector< Node >& vs ) { - Assert( vs.size()==d_candidates.size() ); - for( unsigned i=0; ig(x), this function - * may set ( sols, status ) to ( { x+1, d_x() }, { 1, 0 } ), where d_x() is - * the sygus datatype constructor corresponding to variable x. - */ - bool getSynthSolutionsInternal(std::vector& sols, - std::vector& status, - bool singleInvocation); - //-------------------------------- sygus stream - /** current stream guard */ - Node d_current_stream_guard; - /** the decision strategy for streaming solutions */ - class SygusStreamDecisionStrategy : public DecisionStrategyFmf - { - public: - SygusStreamDecisionStrategy(context::Context* satContext, - Valuation valuation); - /** make literal */ - Node mkLiteral(unsigned i) override; - /** identify */ - std::string identify() const override - { - return std::string("sygus_stream"); - } - }; - std::unique_ptr d_stream_strategy; - /** get current stream guard */ - Node getCurrentStreamGuard() const; - /** get stream guarded lemma - * - * If sygusStream is enabled, this returns ( G V n ) where G is the guard - * returned by getCurrentStreamGuard, otherwise this returns n. - */ - Node getStreamGuardedLemma(Node n) const; - /** - * Prints the current synthesis solution to the output stream indicated by - * the Options object, send a lemma blocking the current solution to the - * output channel. - */ - void printAndContinueStream(); - //-------------------------------- end sygus stream - /** expression miner managers for each function-to-synthesize - * - * Notice that for each function-to-synthesize, we enumerate a stream of - * candidate solutions, where each of these streams is independent. Thus, - * we maintain separate expression miner managers for each of them. - * - * This is used for the sygusRewSynth() option to synthesize new candidate - * rewrite rules. - */ - std::map d_exprm; -}; - -} /* namespace CVC4::theory::quantifiers */ -} /* namespace CVC4::theory */ -} /* namespace CVC4 */ - -#endif diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp deleted file mode 100644 index d30cccd87..000000000 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp +++ /dev/null @@ -1,407 +0,0 @@ -/********************* */ -/*! \file ce_guided_instantiation.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 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 counterexample guided instantiation class - ** This class is the entry point for both synthesis algorithms in Reynolds et al CAV 2015 - ** - **/ -#include "theory/quantifiers/sygus/ce_guided_instantiation.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/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/sygus/term_database_sygus.h" -#include "theory/quantifiers/term_util.h" -#include "theory/theory_engine.h" - -using namespace CVC4::kind; -using namespace std; - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){ - d_conj = new CegConjecture( qe ); - d_last_inst_si = false; -} - -CegInstantiation::~CegInstantiation(){ - delete d_conj; -} - -bool CegInstantiation::needsCheck( Theory::Effort e ) { - return !d_quantEngine->getTheoryEngine()->needCheck() - && e >= Theory::EFFORT_LAST_CALL; -} - -QuantifiersModule::QEffort CegInstantiation::needsModel(Theory::Effort e) -{ - return d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL; -} - -void CegInstantiation::check(Theory::Effort e, QEffort quant_e) -{ - // are we at the proper effort level? - unsigned echeck = - d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL; - if (quant_e != echeck) - { - return; - } - - // if we are waiting to assign the conjecture, do it now - if (!d_waiting_conj.isNull()) - { - Node q = d_waiting_conj; - Trace("cegqi-engine") << "--- Conjecture waiting to assign: " << q - << std::endl; - d_waiting_conj = Node::null(); - if (!d_conj->isAssigned()) - { - assignConjecture(q); - // assign conjecture always uses the output channel, we return and - // re-check here. - return; - } - } - - Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" - << std::endl; - Trace("cegqi-engine-debug") << std::endl; - bool active = false; - bool value; - if (d_quantEngine->getValuation().hasSatValue(d_conj->getConjecture(), value)) - { - active = value; - } - else - { - Trace("cegqi-engine-debug") - << "...no value for quantified formula." << std::endl; - } - Trace("cegqi-engine-debug") - << "Current conjecture status : active : " << active << std::endl; - if (active && d_conj->needsCheck()) - { - checkConjecture(d_conj); - } - Trace("cegqi-engine") - << "Finished Counterexample Guided Instantiation engine." << std::endl; -} - -bool CegInstantiation::assignConjecture(Node q) -{ - if (d_conj->isAssigned()) - { - return false; - } - Trace("cegqi-engine") << "--- Assign conjecture " << q << std::endl; - if (options::sygusQePreproc()) - { - // the following does quantifier elimination as a preprocess step - // for "non-ground single invocation synthesis conjectures": - // exists f. forall xy. P[ f(x), x, y ] - // We run quantifier elimination: - // exists y. P[ z, x, y ] ----> Q[ z, x ] - // Where we replace the original conjecture with: - // exists f. forall x. Q[ f(x), x ] - // For more details, see Example 6 of Reynolds et al. SYNT 2017. - Node body = q[1]; - if (body.getKind() == NOT && body[0].getKind() == FORALL) - { - body = body[0][1]; - } - NodeManager* nm = NodeManager::currentNM(); - Trace("cegqi-qep") << "Compute single invocation for " << q << "..." - << std::endl; - quantifiers::SingleInvocationPartition sip; - std::vector funcs; - funcs.insert(funcs.end(), q[0].begin(), q[0].end()); - sip.init(funcs, body); - Trace("cegqi-qep") << "...finished, got:" << std::endl; - sip.debugPrint("cegqi-qep"); - - if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation()) - { - // create new smt engine to do quantifier elimination - SmtEngine smt_qe(nm->toExprManager()); - smt_qe.setLogic(smt::currentSmtEngine()->getLogicInfo()); - Trace("cegqi-qep") << "Property is non-ground single invocation, run " - "QE to obtain single invocation." - << std::endl; - // partition variables - std::vector all_vars; - sip.getAllVariables(all_vars); - std::vector si_vars; - sip.getSingleInvocationVariables(si_vars); - std::vector qe_vars; - std::vector nqe_vars; - for (unsigned i = 0, size = all_vars.size(); i < size; i++) - { - Node v = all_vars[i]; - if (std::find(si_vars.begin(), si_vars.end(), v) == si_vars.end()) - { - qe_vars.push_back(v); - } - else - { - nqe_vars.push_back(v); - } - } - std::vector orig; - std::vector subs; - // skolemize non-qe variables - for (unsigned i = 0, size = nqe_vars.size(); i < size; i++) - { - Node k = nm->mkSkolem( - "k", nqe_vars[i].getType(), "qe for non-ground single invocation"); - orig.push_back(nqe_vars[i]); - subs.push_back(k); - Trace("cegqi-qep") << " subs : " << nqe_vars[i] << " -> " << k - << std::endl; - } - std::vector funcs; - sip.getFunctions(funcs); - for (unsigned i = 0, size = funcs.size(); i < size; i++) - { - Node f = funcs[i]; - Node fi = sip.getFunctionInvocationFor(f); - Node fv = sip.getFirstOrderVariableForFunction(f); - Assert(!fi.isNull()); - orig.push_back(fi); - Node k = - nm->mkSkolem("k", - fv.getType(), - "qe for function in non-ground single invocation"); - subs.push_back(k); - Trace("cegqi-qep") << " subs : " << fi << " -> " << k << std::endl; - } - Node conj_se_ngsi = sip.getFullSpecification(); - Trace("cegqi-qep") << "Full specification is " << conj_se_ngsi - << std::endl; - Node conj_se_ngsi_subs = conj_se_ngsi.substitute( - orig.begin(), orig.end(), subs.begin(), subs.end()); - Assert(!qe_vars.empty()); - conj_se_ngsi_subs = nm->mkNode(EXISTS, - nm->mkNode(BOUND_VAR_LIST, qe_vars), - conj_se_ngsi_subs.negate()); - - Trace("cegqi-qep") << "Run quantifier elimination on " - << conj_se_ngsi_subs << std::endl; - Expr qe_res = smt_qe.doQuantifierElimination( - conj_se_ngsi_subs.toExpr(), true, false); - Trace("cegqi-qep") << "Result : " << qe_res << std::endl; - - // create single invocation conjecture - Node qe_res_n = Node::fromExpr(qe_res); - qe_res_n = qe_res_n.substitute( - subs.begin(), subs.end(), orig.begin(), orig.end()); - if (!nqe_vars.empty()) - { - qe_res_n = - nm->mkNode(EXISTS, nm->mkNode(BOUND_VAR_LIST, nqe_vars), qe_res_n); - } - Assert(q.getNumChildren() == 3); - qe_res_n = nm->mkNode(FORALL, q[0], qe_res_n, q[2]); - Trace("cegqi-qep") << "Converted conjecture after QE : " << qe_res_n - << std::endl; - qe_res_n = Rewriter::rewrite(qe_res_n); - Node nq = qe_res_n; - // must assert it is equivalent to the original - Node lem = q.eqNode(nq); - Trace("cegqi-lemma") << "Cegqi::Lemma : qe-preprocess : " << lem - << std::endl; - d_quantEngine->getOutputChannel().lemma(lem); - // we've reduced the original to a preprocessed version, return - return false; - } - } - d_conj->assign(q); - return true; -} - -void CegInstantiation::registerQuantifier(Node q) -{ - if (d_quantEngine->getOwner(q) == this) - { // && d_eval_axioms.find( q )==d_eval_axioms.end() ){ - if (!d_conj->isAssigned()) - { - Trace("cegqi") << "Register conjecture : " << q << std::endl; - if (options::sygusQePreproc()) - { - d_waiting_conj = q; - } - else - { - // assign it now - assignConjecture(q); - } - }else{ - Assert( d_conj->getEmbeddedConjecture()==q ); - } - }else{ - Trace("cegqi-debug") << "Register quantifier : " << q << std::endl; - } -} - -void CegInstantiation::checkConjecture(CegConjecture* conj) -{ - Node q = conj->getEmbeddedConjecture(); - Node aq = conj->getConjecture(); - if( Trace.isOn("cegqi-engine-debug") ){ - conj->debugPrint("cegqi-engine-debug"); - Trace("cegqi-engine-debug") << std::endl; - } - - if( !conj->needsRefinement() ){ - Trace("cegqi-engine-debug") << "Do conjecture check..." << std::endl; - if (conj->isSingleInvocation()) - { - std::vector clems; - conj->doSingleInvCheck(clems); - if (!clems.empty()) - { - d_last_inst_si = true; - 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; - } - - Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl; - std::vector cclems; - conj->doCheck(cclems); - bool addedLemma = false; - for (const Node& lem : cclems) - { - d_last_inst_si = false; - Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem - << std::endl; - if (d_quantEngine->addLemma(lem)) - { - ++(d_statistics.d_cegqi_lemmas_ce); - addedLemma = true; - }else{ - // this may happen if we eagerly unfold, simplify to true - Trace("cegqi-engine-debug") - << " ...FAILED to add candidate!" << std::endl; - } - } - if (addedLemma) - { - Trace("cegqi-engine") << " ...check for counterexample." << std::endl; - }else{ - if (conj->needsRefinement()) - { - // immediately go to refine candidate - checkConjecture(conj); - return; - } - } - }else{ - Trace("cegqi-engine") << " *** Refine candidate phase..." << std::endl; - std::vector< Node > rlems; - conj->doRefine( rlems ); - bool addedLemma = false; - for( unsigned i=0; iaddLemma( lem ); - if( res ){ - ++(d_statistics.d_cegqi_lemmas_refine); - conj->incrementRefineCount(); - addedLemma = true; - }else{ - Trace("cegqi-warn") << " ...FAILED to add refinement!" << std::endl; - } - } - if( addedLemma ){ - Trace("cegqi-engine") << " ...refine candidate." << std::endl; - } - } -} - -void CegInstantiation::printSynthSolution( std::ostream& out ) { - if( d_conj->isAssigned() ) - { - d_conj->printSynthSolution( out, d_last_inst_si ); - } - else - { - Assert( false ); - } -} - -void CegInstantiation::getSynthSolutions(std::map& sol_map) -{ - if (d_conj->isAssigned()) - { - d_conj->getSynthSolutions(sol_map, d_last_inst_si); - } -} - -void CegInstantiation::preregisterAssertion( Node n ) { - //check if it sygus conjecture - if( QuantAttributes::checkSygusConjecture( n ) ){ - //this is a sygus conjecture - Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl; - d_conj->preregisterConjecture( n ); - } -} - -CegInstantiation::Statistics::Statistics() - : d_cegqi_lemmas_ce("CegInstantiation::cegqi_lemmas_ce", 0), - d_cegqi_lemmas_refine("CegInstantiation::cegqi_lemmas_refine", 0), - d_cegqi_si_lemmas("CegInstantiation::cegqi_lemmas_si", 0), - d_solutions("CegConjecture::solutions", 0), - d_candidate_rewrites_print("CegConjecture::candidate_rewrites_print", 0), - d_candidate_rewrites("CegConjecture::candidate_rewrites", 0) - -{ - smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce); - smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine); - smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas); - smtStatisticsRegistry()->registerStat(&d_solutions); - smtStatisticsRegistry()->registerStat(&d_candidate_rewrites_print); - smtStatisticsRegistry()->registerStat(&d_candidate_rewrites); -} - -CegInstantiation::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_ce); - smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine); - smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas); - smtStatisticsRegistry()->unregisterStat(&d_solutions); - smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites_print); - smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites); -} - -}/* namespace CVC4::theory::quantifiers */ -}/* namespace CVC4::theory */ -}/* namespace CVC4 */ diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.h b/src/theory/quantifiers/sygus/ce_guided_instantiation.h deleted file mode 100644 index 6bf33effb..000000000 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.h +++ /dev/null @@ -1,99 +0,0 @@ -/********************* */ -/*! \file ce_guided_instantiation.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 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 counterexample guided instantiation class - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H -#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H - -#include "context/cdhashmap.h" -#include "theory/quantifiers/sygus/ce_guided_conjecture.h" -#include "theory/quantifiers_engine.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -class CegInstantiation : public QuantifiersModule -{ - typedef context::CDHashMap NodeBoolMap; -private: - /** the quantified formula stating the synthesis conjecture */ - CegConjecture * d_conj; - /** last instantiation by single invocation module? */ - bool d_last_inst_si; - /** the conjecture we are waiting to assign */ - Node d_waiting_conj; - - private: - /** assign quantified formula q as the conjecture - * - * This method returns true if q was successfully assigned as the synthesis - * conjecture considered by this class. This method may return false, for - * instance, if this class determines that it would rather rewrite q to - * an equivalent form r (in which case this method returns the lemma - * q <=> r). An example of this is the quantifier elimination step - * option::sygusQePreproc(). - */ - bool assignConjecture(Node q); - /** check conjecture */ - void checkConjecture(CegConjecture* conj); - - public: - CegInstantiation( QuantifiersEngine * qe, context::Context* c ); - ~CegInstantiation(); -public: - bool needsCheck(Theory::Effort e) override; - QEffort needsModel(Theory::Effort e) override; - /* Call during quantifier engine's check */ - void check(Theory::Effort e, QEffort quant_e) override; - /* Called for new quantifiers */ - void registerQuantifier(Node q) override; - /** Identify this module (for debugging, dynamic configuration, etc..) */ - std::string identify() const override { return "CegInstantiation"; } - /** print solution for synthesis conjectures */ - void printSynthSolution(std::ostream& out); - /** get synth solutions - * - * This function adds entries to sol_map that map functions-to-synthesize - * with their solutions, for all active conjectures (currently just the one - * assigned to d_conj). This should be called immediately after the solver - * answers unsat for sygus input. - * - * For details on what is added to sol_map, see - * CegConjecture::getSynthSolutions. - */ - void getSynthSolutions(std::map& sol_map); - /** preregister assertion (before rewrite) */ - void preregisterAssertion(Node n); -public: - class Statistics { - public: - IntStat d_cegqi_lemmas_ce; - IntStat d_cegqi_lemmas_refine; - IntStat d_cegqi_si_lemmas; - IntStat d_solutions; - IntStat d_candidate_rewrites_print; - IntStat d_candidate_rewrites; - Statistics(); - ~Statistics(); - };/* class CegInstantiation::Statistics */ - Statistics d_statistics; -}; /* class CegInstantiation */ - -} /* namespace CVC4::theory::quantifiers */ -} /* namespace CVC4::theory */ -} /* namespace CVC4 */ - -#endif diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 7d8db8c03..36690cfcc 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -42,12 +42,11 @@ bool CegqiOutputSingleInv::addLemma( Node n ) { return d_out->addLemma( n ); } -CegConjectureSingleInv::CegConjectureSingleInv(QuantifiersEngine* qe, - CegConjecture* p) +CegSingleInv::CegSingleInv(QuantifiersEngine* qe, SynthConjecture* p) : d_qe(qe), d_parent(p), d_sip(new SingleInvocationPartition), - d_sol(new CegConjectureSingleInvSol(qe)), + 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), @@ -61,17 +60,17 @@ CegConjectureSingleInv::CegConjectureSingleInv(QuantifiersEngine* qe, } } -CegConjectureSingleInv::~CegConjectureSingleInv() { +CegSingleInv::~CegSingleInv() +{ if (d_c_inst_match_trie) { delete d_c_inst_match_trie; } delete d_cosi; - delete d_sol; // (new CegConjectureSingleInvSol(qe)), + delete d_sol; // (new CegSingleInvSol(qe)), delete d_sip; // d_sip(new SingleInvocationPartition), } -void CegConjectureSingleInv::getInitialSingleInvLemma(Node g, - std::vector& lems) +void CegSingleInv::getInitialSingleInvLemma(Node g, std::vector& lems) { Assert(!g.isNull()); Assert(!d_single_inv.isNull()); @@ -114,12 +113,13 @@ void CegConjectureSingleInv::getInitialSingleInvLemma(Node g, d_cinst->registerCounterexampleLemma(lems, d_single_inv_sk); } -void CegConjectureSingleInv::initialize( Node q ) { +void CegSingleInv::initialize(Node q) +{ // can only register one quantified formula with this Assert( d_quant.isNull() ); d_quant = q; d_simp_quant = q; - Trace("cegqi-si") << "CegConjectureSingleInv::initialize : " << q << std::endl; + Trace("cegqi-si") << "CegSingleInv::initialize : " << q << std::endl; // infer single invocation-ness // get the variables @@ -293,7 +293,7 @@ void CegConjectureSingleInv::initialize( Node q ) { } } -void CegConjectureSingleInv::finishInit(bool syntaxRestricted) +void CegSingleInv::finishInit(bool syntaxRestricted) { Trace("cegqi-si-debug") << "Single invocation: finish init" << std::endl; // do not do single invocation if grammar is restricted and CEGQI_SI_MODE_ALL is not enabled @@ -343,9 +343,10 @@ void CegConjectureSingleInv::finishInit(bool syntaxRestricted) } } -bool CegConjectureSingleInv::doAddInstantiation( std::vector< Node >& subs ){ +bool CegSingleInv::doAddInstantiation(std::vector& subs) +{ Assert( d_single_inv_sk.size()==subs.size() ); - Trace("cegqi-si-inst-debug") << "CegConjectureSingleInv::doAddInstantiation, #vars = "; + 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") ){ @@ -400,19 +401,23 @@ bool CegConjectureSingleInv::doAddInstantiation( std::vector< Node >& subs ){ return true; } -bool CegConjectureSingleInv::isEligibleForInstantiation( Node n ) { +bool CegSingleInv::isEligibleForInstantiation(Node n) +{ 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 CegConjectureSingleInv::addLemma( Node n ) { +bool CegSingleInv::addLemma(Node n) +{ d_curr_lemmas.push_back( n ); return true; } -bool CegConjectureSingleInv::check( std::vector< Node >& lems ) { +bool CegSingleInv::check(std::vector& lems) +{ if( !d_single_inv.isNull() ) { - Trace("cegqi-si-debug") << "CegConjectureSingleInv::check..." << std::endl; - Trace("cegqi-si-debug") << "CegConjectureSingleInv::check consulting ceg instantiation..." << std::endl; + 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 @@ -427,7 +432,11 @@ bool CegConjectureSingleInv::check( std::vector< Node >& lems ) { } } -Node CegConjectureSingleInv::constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index, std::map< Node, Node >& weak_imp ) { +Node CegSingleInv::constructSolution(std::vector& indices, + unsigned i, + unsigned index, + std::map& weak_imp) +{ Assert( index& indices //TODO: use term size? struct sortSiInstanceIndices { - CegConjectureSingleInv* d_ccsi; + CegSingleInv* d_ccsi; int d_i; bool operator() (unsigned i, unsigned j) { if( d_ccsi->d_inst[i][d_i].isConst() && !d_ccsi->d_inst[j][d_i].isConst() ){ @@ -460,8 +469,8 @@ struct sortSiInstanceIndices { } }; - -Node CegConjectureSingleInv::postProcessSolution( Node n ){ +Node CegSingleInv::postProcessSolution(Node n) +{ bool childChanged = false; Kind k = n.getKind(); if( n.getKind()==INTS_DIVISION_TOTAL ){ @@ -487,8 +496,11 @@ Node CegConjectureSingleInv::postProcessSolution( Node n ){ } } - -Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& reconstructed, bool rconsSygus ){ +Node CegSingleInv::getSolution(unsigned sol_index, + TypeNode stn, + int& reconstructed, + bool rconsSygus) +{ Assert( d_sol!=NULL ); Assert( !d_lemmas_produced.empty() ); const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); @@ -563,7 +575,11 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& return reconstructToSyntax( s, stn, reconstructed, rconsSygus ); } -Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& reconstructed, bool rconsSygus ) { +Node CegSingleInv::reconstructToSyntax(Node s, + TypeNode stn, + int& reconstructed, + bool rconsSygus) +{ d_solution = s; const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); @@ -645,13 +661,9 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec } } -bool CegConjectureSingleInv::needsCheck() { - return true; -} +bool CegSingleInv::needsCheck() { return true; } -void CegConjectureSingleInv::preregisterConjecture( Node q ) { - d_orig_conjecture = q; -} +void CegSingleInv::preregisterConjecture(Node q) { d_orig_conjecture = q; } bool DetTrace::DetTraceTrie::add( Node loc, std::vector< Node >& val, unsigned index ){ if( index==val.size() ){ diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index b27163549..c797bc3cb 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -28,18 +28,17 @@ namespace CVC4 { namespace theory { namespace quantifiers { -class CegConjecture; -class CegConjectureSingleInv; -class CegEntailmentInfer; +class SynthConjecture; +class CegSingleInv; class CegqiOutputSingleInv : public CegqiOutput { -public: - CegqiOutputSingleInv( CegConjectureSingleInv * out ) : d_out( out ){} - virtual ~CegqiOutputSingleInv() {} - CegConjectureSingleInv * d_out; - bool doAddInstantiation(std::vector& subs) override; - bool isEligibleForInstantiation(Node n) override; - bool addLemma(Node lem) override; + 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 { @@ -123,7 +122,8 @@ private: // (2) inferring whether the conjecture corresponds to a deterministic transistion system (by utility d_ti). // For these techniques, we may generate a template (d_templ) which specifies a restricted // solution space. We may in turn embed this template as a SyGuS grammar. -class CegConjectureSingleInv { +class CegSingleInv +{ private: friend class CegqiOutputSingleInv; //presolve @@ -138,14 +138,16 @@ class CegConjectureSingleInv { unsigned index, std::map& weak_imp); Node postProcessSolution(Node n); private: + /** pointer to the quantifiers engine */ QuantifiersEngine* d_qe; - CegConjecture* d_parent; + /** the parent of this class */ + SynthConjecture* d_parent; // single invocation inference utility SingleInvocationPartition* d_sip; // transition inference module for each function to synthesize std::map< Node, TransitionInference > d_ti; // solution reconstruction - CegConjectureSingleInvSol* d_sol; + CegSingleInvSol* d_sol; // the instantiator's output channel CegqiOutputSingleInv* d_cosi; // the instantiator @@ -197,8 +199,8 @@ class CegConjectureSingleInv { std::map< Node, Node > d_templ_arg; public: - CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p ); - ~CegConjectureSingleInv(); + CegSingleInv(QuantifiersEngine* qe, SynthConjecture* p); + ~CegSingleInv(); // get simplified conjecture Node getSimplifiedConjecture() { return d_simp_quant; } diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index e575dff9b..7f7c56f84 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -20,8 +20,8 @@ #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/sygus/ce_guided_instantiation.h" #include "theory/quantifiers/sygus/ce_guided_single_inv.h" +#include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" @@ -42,10 +42,13 @@ bool doCompare(Node a, Node b, Kind k) return com.isConst() && com.getConst(); } -CegConjectureSingleInvSol::CegConjectureSingleInvSol(QuantifiersEngine* qe) - : d_qe(qe), d_id_count(0), d_root_id() {} +CegSingleInvSol::CegSingleInvSol(QuantifiersEngine* qe) + : d_qe(qe), d_id_count(0), d_root_id() +{ +} -bool CegConjectureSingleInvSol::debugSolution( Node sol ) { +bool CegSingleInvSol::debugSolution(Node sol) +{ if( sol.getKind()==SKOLEM ){ return false; }else{ @@ -59,7 +62,8 @@ bool CegConjectureSingleInvSol::debugSolution( Node sol ) { } -void CegConjectureSingleInvSol::debugTermSize( Node sol, int& t_size, int& num_ite ) { +void CegSingleInvSol::debugTermSize(Node sol, int& t_size, int& num_ite) +{ std::map< Node, int >::iterator it = d_dterm_size.find( sol ); if( it==d_dterm_size.end() ){ int prev = t_size; @@ -79,8 +83,8 @@ void CegConjectureSingleInvSol::debugTermSize( Node sol, int& t_size, int& num_i } } - -Node CegConjectureSingleInvSol::pullITEs( Node s ) { +Node CegSingleInvSol::pullITEs(Node s) +{ if( s.getKind()==ITE ){ bool success; do { @@ -107,7 +111,13 @@ Node CegConjectureSingleInvSol::pullITEs( Node s ) { } // pull condition common to all ITE conditions in path of size > 1 -bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::vector< Node >& conj, Node& t, Node& rem, int depth ) { +bool CegSingleInvSol::pullITECondition(Node root, + Node n_ite, + std::vector& conj, + Node& t, + Node& rem, + int depth) +{ Assert( n_ite.getKind()==ITE ); std::vector< Node > curr_conj; std::vector< Node > orig_conj; @@ -196,7 +206,8 @@ bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::ve } } -Node CegConjectureSingleInvSol::flattenITEs( Node n, bool rec ) { +Node CegSingleInvSol::flattenITEs(Node n, bool rec) +{ Assert( !n.isNull() ); if( n.getKind()==ITE ){ Trace("csi-sol-debug") << "Flatten ITE." << std::endl; @@ -260,8 +271,14 @@ Node CegConjectureSingleInvSol::flattenITEs( Node n, bool rec ) { // assign is from literals to booleans // union_find is from args to values -bool CegConjectureSingleInvSol::getAssign( bool pol, Node n, std::map< Node, bool >& assign, std::vector< Node >& new_assign, std::vector< Node >& vars, - std::vector< Node >& new_vars, std::vector< Node >& new_subs ) { +bool CegSingleInvSol::getAssign(bool pol, + Node n, + std::map& assign, + std::vector& new_assign, + std::vector& vars, + std::vector& new_vars, + std::vector& new_subs) +{ std::map< Node, bool >::iterator ita = assign.find( n ); if( ita!=assign.end() ){ Trace("csi-simp-debug") << "---already assigned, lookup " << pol << " " << ita->second << std::endl; @@ -287,7 +304,11 @@ bool CegConjectureSingleInvSol::getAssign( bool pol, Node n, std::map< Node, boo return true; } -bool CegConjectureSingleInvSol::getAssignEquality( Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs ) { +bool CegSingleInvSol::getAssignEquality(Node eq, + std::vector& vars, + std::vector& new_vars, + std::vector& new_subs) +{ Assert( eq.getKind()==EQUAL ); //try to find valid argument for( unsigned r=0; r<2; r++ ){ @@ -309,7 +330,8 @@ bool CegConjectureSingleInvSol::getAssignEquality( Node eq, std::vector< Node >& return false; } -Node CegConjectureSingleInvSol::simplifySolution( Node sol, TypeNode stn ){ +Node CegSingleInvSol::simplifySolution(Node sol, TypeNode stn) +{ int tsize, itesize; if( Trace.isOn("csi-sol") ){ tsize = 0;itesize = 0; @@ -373,9 +395,13 @@ Node CegConjectureSingleInvSol::simplifySolution( Node sol, TypeNode stn ){ return curr_sol; } -Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, std::map< Node, bool >& assign, - std::vector< Node >& vars, std::vector< Node >& subs, int status ) { - +Node CegSingleInvSol::simplifySolutionNode(Node sol, + TypeNode stn, + std::map& assign, + std::vector& vars, + std::vector& subs, + int status) +{ Assert( vars.size()==subs.size() ); std::map< Node, bool >::iterator ita = assign.find( sol ); if( ita!=assign.end() ){ @@ -618,8 +644,8 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st } } - -void CegConjectureSingleInvSol::preregisterConjecture( Node q ) { +void CegSingleInvSol::preregisterConjecture(Node q) +{ Trace("csi-sol") << "Preregister conjecture : " << q << std::endl; Node n = q; if( n.getKind()==FORALL ){ @@ -641,10 +667,10 @@ void CegConjectureSingleInvSol::preregisterConjecture( Node q ) { registerEquivalentTerms( n ); } -Node CegConjectureSingleInvSol::reconstructSolution(Node sol, - TypeNode stn, - int& reconstructed, - int enumLimit) +Node CegSingleInvSol::reconstructSolution(Node sol, + TypeNode stn, + int& reconstructed, + int enumLimit) { Trace("csi-rcons") << "Solution (pre-reconstruction) is : " << sol << std::endl; int status; @@ -743,7 +769,8 @@ Node CegConjectureSingleInvSol::reconstructSolution(Node sol, return Node::null(); } -int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, int& status ) { +int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status) +{ std::map< Node, int >::iterator itri = d_rcons_to_status[stn].find( t ); if( itri!=d_rcons_to_status[stn].end() ){ status = itri->second; @@ -956,7 +983,12 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in } } -bool CegConjectureSingleInvSol::collectReconstructNodes( int pid, std::vector< Node >& ts, const DatatypeConstructor& dtc, std::vector< int >& ids, int& status ) { +bool CegSingleInvSol::collectReconstructNodes(int pid, + std::vector& ts, + const DatatypeConstructor& dtc, + std::vector& ids, + int& status) +{ Assert( dtc.getNumArgs()==ts.size() ); for( unsigned i=0; igetTermDatabaseSygus()->getArgType( dtc, i ); @@ -1001,8 +1033,9 @@ bool CegConjectureSingleInvSol::collectReconstructNodes( int pid, std::vector< N } */ - -Node CegConjectureSingleInvSol::CegConjectureSingleInvSol::getReconstructedSolution( int id, bool mod_eq ) { +Node CegSingleInvSol::CegSingleInvSol::getReconstructedSolution(int id, + bool mod_eq) +{ std::map< int, Node >::iterator it = d_reconstruct.find( id ); if( it!=d_reconstruct.end() ){ return it->second; @@ -1053,7 +1086,8 @@ Node CegConjectureSingleInvSol::CegConjectureSingleInvSol::getReconstructedSolut } } -int CegConjectureSingleInvSol::allocate( Node n, TypeNode stn ) { +int CegSingleInvSol::allocate(Node n, TypeNode stn) +{ std::map< Node, int >::iterator it = d_rcons_to_id[stn].find( n ); if( it==d_rcons_to_id[stn].end() ){ int ret = d_id_count; @@ -1073,7 +1107,8 @@ int CegConjectureSingleInvSol::allocate( Node n, TypeNode stn ) { } } -bool CegConjectureSingleInvSol::getPathToRoot( int id ) { +bool CegSingleInvSol::getPathToRoot(int id) +{ if( id==d_root_id ){ return true; }else{ @@ -1092,7 +1127,8 @@ bool CegConjectureSingleInvSol::getPathToRoot( int id ) { } } -void CegConjectureSingleInvSol::setReconstructed( int id, Node n ) { +void CegSingleInvSol::setReconstructed(int id, Node n) +{ //set all equivalent to this as reconstructed int rid = d_rep[id]; for( unsigned i=0; i& equiv ) { +void CegSingleInvSol::getEquivalentTerms(Kind k, + Node n, + std::vector& equiv) +{ if( k==AND || k==OR ){ equiv.push_back( NodeManager::currentNM()->mkNode( k, n, n ) ); equiv.push_back( NodeManager::currentNM()->mkNode( k, n, NodeManager::currentNM()->mkConst( k==AND ) ) ); @@ -1201,7 +1240,8 @@ void CegConjectureSingleInvSol::getEquivalentTerms( Kind k, Node n, std::vector< } } -void CegConjectureSingleInvSol::registerEquivalentTerms( Node n ) { +void CegSingleInvSol::registerEquivalentTerms(Node n) +{ for( unsigned i=0; i::iterator it = d_builtin_const_to_sygus[tn].find(c); if (it != d_builtin_const_to_sygus[tn].end()) @@ -1350,7 +1388,7 @@ struct sortConstants } }; -void CegConjectureSingleInvSol::registerType(TypeNode tn) +void CegSingleInvSol::registerType(TypeNode tn) { if (d_const_list_pos.find(tn) != d_const_list_pos.end()) { @@ -1407,10 +1445,10 @@ void CegConjectureSingleInvSol::registerType(TypeNode tn) } } -bool CegConjectureSingleInvSol::getMatch(Node p, - Node n, - std::map& s, - std::vector& new_s) +bool CegSingleInvSol::getMatch(Node p, + Node n, + std::map& s, + std::vector& new_s) { TermDbSygus* tds = d_qe->getTermDatabaseSygus(); if (tds->isFreeVar(p)) @@ -1461,12 +1499,12 @@ bool CegConjectureSingleInvSol::getMatch(Node p, return false; } -bool CegConjectureSingleInvSol::getMatch(Node t, - TypeNode st, - int& index_found, - std::vector& args, - int index_exc, - int index_start) +bool CegSingleInvSol::getMatch(Node t, + TypeNode st, + int& index_found, + std::vector& args, + int index_exc, + int index_start) { Assert(st.isDatatype()); const Datatype& dt = static_cast(st.toType()).getDatatype(); @@ -1517,9 +1555,7 @@ bool CegConjectureSingleInvSol::getMatch(Node t, return false; } -Node CegConjectureSingleInvSol::getGenericBase(TypeNode tn, - const Datatype& dt, - int c) +Node CegSingleInvSol::getGenericBase(TypeNode tn, const Datatype& dt, int c) { std::map::iterator it = d_generic_base[tn].find(c); if (it != d_generic_base[tn].end()) diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h index 8d18611cf..fb0862413 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h @@ -24,19 +24,19 @@ namespace CVC4 { namespace theory { namespace quantifiers { +class CegSingleInv; -class CegConjectureSingleInv; - -/** CegConjectureSingleInvSol +/** CegSingleInvSol * * This function implements Figure 5 of "Counterexample-Guided Quantifier * Instantiation for Synthesis in SMT", Reynolds et al CAV 2015. * */ -class CegConjectureSingleInvSol +class CegSingleInvSol { - friend class CegConjectureSingleInv; -private: + friend class CegSingleInv; + + private: QuantifiersEngine * d_qe; std::vector< Node > d_varList; std::map< Node, int > d_dterm_size; @@ -55,7 +55,7 @@ private: std::vector< Node >& vars, std::vector< Node >& subs, int status ); public: - CegConjectureSingleInvSol(QuantifiersEngine* qe); + CegSingleInvSol(QuantifiersEngine* qe); /** simplify solution * * Returns the simplified version of node sol whose syntax is restricted by diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 204daa49a..fbe0da7a8 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -16,7 +16,7 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" -#include "theory/quantifiers/sygus/ce_guided_conjecture.h" +#include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/theory_engine.h" @@ -28,7 +28,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -Cegis::Cegis(QuantifiersEngine* qe, CegConjecture* p) +Cegis::Cegis(QuantifiersEngine* qe, SynthConjecture* p) : SygusModule(qe, p), d_eval_unfold(nullptr), d_using_gr_repair(false) { if (options::sygusEvalUnfold()) diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index ce4186eb2..c7392b378 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -41,7 +41,7 @@ namespace quantifiers { class Cegis : public SygusModule { public: - Cegis(QuantifiersEngine* qe, CegConjecture* p); + Cegis(QuantifiersEngine* qe, SynthConjecture* p); ~Cegis() override {} /** initialize */ virtual bool initialize(Node n, @@ -69,11 +69,11 @@ class Cegis : public SygusModule protected: /** the evaluation unfold utility of d_tds */ SygusEvalUnfold* d_eval_unfold; - /** If CegConjecture::d_base_inst is exists y. P( d, y ), then this is y. */ + /** If SynthConjecture::d_base_inst is exists y. P( d, y ), then this is y. */ std::vector d_base_vars; /** - * If CegConjecture::d_base_inst is exists y. P( d, y ), then this is the - * formula P( CegConjecture::d_candidates, y ). + * If SynthConjecture::d_base_inst is exists y. P( d, y ), then this is the + * formula P( SynthConjecture::d_candidates, y ). */ Node d_base_body; //----------------------------------cegis-implementation-specific diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 56cc40244..456f44019 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -17,8 +17,8 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" -#include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/sygus_unif_rl.h" +#include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/theory_engine.h" @@ -28,7 +28,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -CegisUnif::CegisUnif(QuantifiersEngine* qe, CegConjecture* p) +CegisUnif::CegisUnif(QuantifiersEngine* qe, SynthConjecture* p) : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, p) { } @@ -299,8 +299,8 @@ void CegisUnif::registerRefinementLemma(const std::vector& vars, OR, d_parent->getGuard().negate(), plem)); } -CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe, - CegConjecture* parent) +CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy( + QuantifiersEngine* qe, SynthConjecture* parent) : DecisionStrategyFmf(qe->getSatContext(), qe->getValuation()), d_qe(qe), d_parent(parent) diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index ae2d7964b..00cc5af72 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -47,7 +47,7 @@ namespace quantifiers { class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf { public: - CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe, CegConjecture* parent); + CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe, SynthConjecture* parent); /** Make the n^th literal of this strategy (G_uq_n). * * This call may add new lemmas of the form described above @@ -96,7 +96,7 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf /** sygus term database of d_qe */ TermDbSygus* d_tds; /** reference to the parent conjecture */ - CegConjecture* d_parent; + SynthConjecture* d_parent; /** whether this module has been initialized */ bool d_initialized; /** null node */ @@ -194,7 +194,7 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf class CegisUnif : public Cegis { public: - CegisUnif(QuantifiersEngine* qe, CegConjecture* p); + CegisUnif(QuantifiersEngine* qe, SynthConjecture* p); ~CegisUnif() override; /** Retrieves enumerators for constructing solutions * diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index e05df8581..eadbf766a 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -20,9 +20,9 @@ #include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" #include "theory/datatypes/datatypes_rewriter.h" -#include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/sygus_grammar_norm.h" #include "theory/quantifiers/sygus/sygus_process_conj.h" +#include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" @@ -33,7 +33,7 @@ namespace theory { namespace quantifiers { CegGrammarConstructor::CegGrammarConstructor(QuantifiersEngine* qe, - CegConjecture* p) + SynthConjecture* p) : d_qe(qe), d_parent(p), d_is_syntax_restricted(false) { } @@ -95,10 +95,11 @@ Node CegGrammarConstructor::process(Node q, { // convert to deep embedding and finalize single invocation here // now, construct the grammar - Trace("cegqi") << "CegConjecture : convert to deep embedding..." << std::endl; + Trace("cegqi") << "SynthConjecture : convert to deep embedding..." + << std::endl; std::map< TypeNode, std::vector< Node > > extra_cons; if( options::sygusAddConstGrammar() ){ - Trace("cegqi") << "CegConjecture : collect constants..." << std::endl; + Trace("cegqi") << "SynthConjecture : collect constants..." << std::endl; collectTerms( q[1], extra_cons ); } std::map> exc_cons; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 33c0a836b..022031bef 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -24,7 +24,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -class CegConjecture; +class SynthConjecture; /** utility for constructing datatypes that correspond to syntactic restrictions, * and applying the deep embedding from Section 4 of Reynolds et al CAV 2015. @@ -32,7 +32,7 @@ class CegConjecture; class CegGrammarConstructor { public: - CegGrammarConstructor(QuantifiersEngine* qe, CegConjecture* p); + CegGrammarConstructor(QuantifiersEngine* qe, SynthConjecture* p); ~CegGrammarConstructor() {} /** process * @@ -114,7 +114,7 @@ public: /** parent conjecture * This contains global information about the synthesis conjecture. */ - CegConjecture* d_parent; + SynthConjecture* d_parent; /** is the syntax restricted? */ bool d_is_syntax_restricted; /** collect terms */ diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index 868e69b21..3d066e8dd 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -22,7 +22,6 @@ #include "smt/smt_engine_scope.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" -#include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/sygus_grammar_red.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp index 54a3cce50..24b47b216 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -14,8 +14,8 @@ #include "theory/quantifiers/sygus/sygus_invariance.h" -#include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/sygus_pbe.h" +#include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" using namespace CVC4::kind; @@ -87,7 +87,7 @@ bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) } void EquivSygusInvarianceTest::init( - TermDbSygus* tds, TypeNode tn, CegConjecture* aconj, Node e, Node bvr) + TermDbSygus* tds, TypeNode tn, SynthConjecture* aconj, Node e, Node bvr) { // compute the current examples d_bvr = bvr; diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index 20cd1fd03..59761da5c 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -27,7 +27,7 @@ namespace theory { namespace quantifiers { class TermDbSygus; -class CegConjecture; +class SynthConjecture; /* SygusInvarianceTest * @@ -181,7 +181,7 @@ class EquivSygusInvarianceTest : public SygusInvarianceTest * are checking for invariance */ void init( - TermDbSygus* tds, TypeNode tn, CegConjecture* aconj, Node e, Node bvr); + TermDbSygus* tds, TypeNode tn, SynthConjecture* aconj, Node e, Node bvr); protected: /** checks whether the analog of nvn still rewrites to d_bvr */ @@ -189,7 +189,7 @@ class EquivSygusInvarianceTest : public SygusInvarianceTest private: /** the conjecture associated with the enumerator d_enum */ - CegConjecture* d_conj; + SynthConjecture* d_conj; /** the enumerator associated with the term for which this test is for */ Node d_enum; /** the RHS of the evaluation */ diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp index b36fe4281..3471472fa 100644 --- a/src/theory/quantifiers/sygus/sygus_module.cpp +++ b/src/theory/quantifiers/sygus/sygus_module.cpp @@ -18,7 +18,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SygusModule::SygusModule(QuantifiersEngine* qe, CegConjecture* p) +SygusModule::SygusModule(QuantifiersEngine* qe, SynthConjecture* p) : d_qe(qe), d_tds(qe->getTermDatabaseSygus()), d_parent(p) { } diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index e2a9fae80..c1b12dfd0 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -25,20 +25,20 @@ namespace CVC4 { namespace theory { namespace quantifiers { -class CegConjecture; +class SynthConjecture; /** 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. + * This is the base class of sygus modules, owned by SynthConjecture. The + * purpose of this class is to, when applicable, suggest candidate solutions for + * SynthConjecture to test. * - * In more detail, an instance of the conjecture class (CegConjecture) creates + * In more detail, an instance of the conjecture class (SynthConjecture) 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: + * conjecture (see SynthConjecture::d_base_inst) is the formula: * exists y. P( k, y ) * where k are the "candidate" variables for the conjecture. * @@ -48,12 +48,12 @@ class CegConjecture; class SygusModule { public: - SygusModule(QuantifiersEngine* qe, CegConjecture* p); + SygusModule(QuantifiersEngine* qe, SynthConjecture* p); virtual ~SygusModule() {} /** initialize * * n is the "base instantiation" of the deep-embedding version of the - * synthesis conjecture under candidates (see CegConjecture::d_base_inst). + * synthesis conjecture under candidates (see SynthConjecture::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. @@ -127,7 +127,7 @@ class SygusModule /** sygus term database of d_qe */ quantifiers::TermDbSygus* d_tds; /** reference to the parent conjecture */ - CegConjecture* d_parent; + SynthConjecture* d_parent; }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 6a82b9dad..9a6645560 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -28,7 +28,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -CegConjecturePbe::CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p) +SygusPbe::SygusPbe(QuantifiersEngine* qe, SynthConjecture* p) : SygusModule(qe, p) { d_true = NodeManager::currentNM()->mkConst(true); @@ -36,13 +36,15 @@ CegConjecturePbe::CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p) d_is_pbe = false; } -CegConjecturePbe::~CegConjecturePbe() { - -} +SygusPbe::~SygusPbe() {} //--------------------------------- collecting finite input/output domain information -void CegConjecturePbe::collectExamples( Node n, std::map< Node, bool >& visited, bool hasPol, bool pol ) { +void SygusPbe::collectExamples(Node n, + std::map& visited, + bool hasPol, + bool pol) +{ if( visited.find( n )==visited.end() ){ visited[n] = true; Node neval; @@ -116,9 +118,9 @@ void CegConjecturePbe::collectExamples( Node n, std::map< Node, bool >& visited, } } -bool CegConjecturePbe::initialize(Node n, - const std::vector& candidates, - std::vector& lemmas) +bool SygusPbe::initialize(Node n, + const std::vector& candidates, + std::vector& lemmas) { Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl; @@ -248,9 +250,13 @@ bool CegConjecturePbe::initialize(Node n, return true; } -Node CegConjecturePbe::PbeTrie::addPbeExample(TypeNode etn, Node e, Node b, - CegConjecturePbe* cpbe, - unsigned index, unsigned ntotal) { +Node SygusPbe::PbeTrie::addPbeExample(TypeNode etn, + Node e, + Node b, + SygusPbe* cpbe, + unsigned index, + unsigned ntotal) +{ if (index == ntotal) { // lazy child holds the leaf data if (d_lazy_child.isNull()) { @@ -281,16 +287,20 @@ Node CegConjecturePbe::PbeTrie::addPbeExample(TypeNode etn, Node e, Node b, } } -Node CegConjecturePbe::PbeTrie::addPbeExampleEval(TypeNode etn, Node e, Node b, - std::vector& ex, - CegConjecturePbe* cpbe, - unsigned index, - unsigned ntotal) { +Node SygusPbe::PbeTrie::addPbeExampleEval(TypeNode etn, + Node e, + Node b, + std::vector& ex, + SygusPbe* cpbe, + unsigned index, + unsigned ntotal) +{ Node eb = cpbe->d_tds->evaluateBuiltin(etn, b, ex); return d_children[eb].addPbeExample(etn, e, b, cpbe, index + 1, ntotal); } -bool CegConjecturePbe::hasExamples(Node e) { +bool SygusPbe::hasExamples(Node e) +{ if (isPbe()) { e = d_tds->getSynthFunForEnumerator(e); Assert(!e.isNull()); @@ -302,7 +312,8 @@ bool CegConjecturePbe::hasExamples(Node e) { return false; } -unsigned CegConjecturePbe::getNumExamples(Node e) { +unsigned SygusPbe::getNumExamples(Node e) +{ e = d_tds->getSynthFunForEnumerator(e); Assert(!e.isNull()); std::map > >::iterator it = @@ -314,7 +325,8 @@ unsigned CegConjecturePbe::getNumExamples(Node e) { } } -void CegConjecturePbe::getExample(Node e, unsigned i, std::vector& ex) { +void SygusPbe::getExample(Node e, unsigned i, std::vector& ex) +{ e = d_tds->getSynthFunForEnumerator(e); Assert(!e.isNull()); std::map > >::iterator it = @@ -327,7 +339,8 @@ void CegConjecturePbe::getExample(Node e, unsigned i, std::vector& ex) { } } -Node CegConjecturePbe::getExampleOut(Node e, unsigned i) { +Node SygusPbe::getExampleOut(Node e, unsigned i) +{ e = d_tds->getSynthFunForEnumerator(e); Assert(!e.isNull()); std::map >::iterator it = d_examples_out.find(e); @@ -340,7 +353,8 @@ Node CegConjecturePbe::getExampleOut(Node e, unsigned i) { } } -Node CegConjecturePbe::addSearchVal(TypeNode tn, Node e, Node bvr) { +Node SygusPbe::addSearchVal(TypeNode tn, Node e, Node bvr) +{ Assert(isPbe()); Assert(!e.isNull()); e = d_tds->getSynthFunForEnumerator(e); @@ -355,8 +369,8 @@ Node CegConjecturePbe::addSearchVal(TypeNode tn, Node e, Node bvr) { return Node::null(); } -Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, - unsigned i) { +Node SygusPbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i) +{ e = d_tds->getSynthFunForEnumerator(e); Assert(!e.isNull()); std::map::iterator itx = d_examples_invalid.find(e); @@ -373,8 +387,8 @@ Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, // ------------------------------------------- solution construction from enumeration -void CegConjecturePbe::getTermList(const std::vector& candidates, - std::vector& terms) +void SygusPbe::getTermList(const std::vector& candidates, + std::vector& terms) { Valuation& valuation = d_qe->getValuation(); for( unsigned i=0; i& candidates, } } -bool CegConjecturePbe::constructCandidates(const std::vector& enums, - const std::vector& enum_values, - const std::vector& candidates, - std::vector& candidate_values, - std::vector& lems) +bool SygusPbe::constructCandidates(const std::vector& enums, + const std::vector& enum_values, + const std::vector& candidates, + std::vector& candidate_values, + std::vector& lems) { Assert( enums.size()==enum_values.size() ); if( !enums.empty() ){ diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index 49d853248..66e19b6c9 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_PBE_H -#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_PBE_H +#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H +#define __CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H #include "context/cdhashmap.h" #include "theory/quantifiers/sygus/sygus_module.h" @@ -25,79 +25,79 @@ namespace CVC4 { namespace theory { namespace quantifiers { -class CegConjecture; +class SynthConjecture; -/** CegConjecturePbe -* -* This class implements optimizations that target synthesis conjectures -* that are in Programming-By-Examples (PBE) form. -* -* [EX#1] An example of a synthesis conjecture in PBE form is : -* exists f. forall x. -* ( x = 0 => f( x ) = 2 ) ^ ( x = 5 => f( x ) = 7 ) ^ ( x = 6 => f( x ) = 8 ) -* -* We say that the above conjecture has I/O examples (0)->2, (5)->7, (6)->8. -* -* Internally, this class does the following for SyGuS inputs: -* -* (1) Infers whether the input conjecture is in PBE form or not. -* (2) Based on this information and on the syntactic restrictions, it -* devises a strategy for enumerating terms and construction solutions, -* which is inspired by Alur et al. "Scaling Enumerative Program Synthesis -* via Divide and Conquer" TACAS 2017. In particular, it may consider -* strategies for constructing decision trees when the grammar permits ITEs -* and a strategy for divide-and-conquer string synthesis when the grammar -* permits string concatenation. This is managed through the SygusUnif -* utilities, d_sygus_unif. -* (3) It makes (possibly multiple) calls to -* TermDatabaseSygus::regstierEnumerator(...) based -* on the strategy, which inform the rest of the system to enumerate values -* of particular types in the grammar through use of fresh variables which -* we call "enumerators". -* -* Points (1)-(3) happen within a call to CegConjecturePbe::initialize(...). -* -* Notice that each enumerator is associated with a single -* function-to-synthesize, but a function-to-sythesize may be mapped to multiple -* enumerators. Some public functions of this class expect an enumerator as -* input, which we map to a function-to-synthesize via -* TermDatabaseSygus::getSynthFunFor(e). -* -* An enumerator is initially "active" but may become inactive if the enumeration -* exhausts all possible values in the datatype corresponding to syntactic -* restrictions for it. The search may continue unless all enumerators become -* inactive. -* -* (4) During search, the extension of quantifier-free datatypes procedure for -* SyGuS datatypes may ask this class whether current candidates can be -* discarded based on inferring when two candidate solutions are equivalent -* up to examples. For example, the candidate solutions: -* f = \x ite( x < 0, x+1, x ) and f = \x x -* are equivalent up to examples on the above conjecture, since they have the -* same value on the points x = 0,5,6. Hence, we need only consider one of -* them. The interface for querying this is -* CegConjecturePbe::addSearchVal(...). -* For details, see Reynolds et al. SYNT 2017. -* -* (5) When the extension of quantifier-free datatypes procedure for SyGuS -* datatypes terminates with a model, the parent of this class calls -* CegConjecturePbe::getCandidateList(...), where this class returns the list -* of active enumerators. -* (6) The parent class subsequently calls -* CegConjecturePbe::constructValues(...), which informs this class that new -* values have been enumerated for active enumerators, as indicated by the -* current model. This call also requests that based on these -* newly enumerated values, whether this class is now able to construct a -* solution based on the high-level strategy (stored in d_sygus_unif). -* -* This class is not designed to work in incremental mode, since there is no way -* to specify incremental problems in SyguS. -*/ -class CegConjecturePbe : public SygusModule +/** SygusPbe + * + * This class implements optimizations that target synthesis conjectures + * that are in Programming-By-Examples (PBE) form. + * + * [EX#1] An example of a synthesis conjecture in PBE form is : + * exists f. forall x. + * ( x = 0 => f( x ) = 2 ) ^ ( x = 5 => f( x ) = 7 ) ^ ( x = 6 => f( x ) = 8 ) + * + * We say that the above conjecture has I/O examples (0)->2, (5)->7, (6)->8. + * + * Internally, this class does the following for SyGuS inputs: + * + * (1) Infers whether the input conjecture is in PBE form or not. + * (2) Based on this information and on the syntactic restrictions, it + * devises a strategy for enumerating terms and construction solutions, + * which is inspired by Alur et al. "Scaling Enumerative Program Synthesis + * via Divide and Conquer" TACAS 2017. In particular, it may consider + * strategies for constructing decision trees when the grammar permits ITEs + * and a strategy for divide-and-conquer string synthesis when the grammar + * permits string concatenation. This is managed through the SygusUnif + * utilities, d_sygus_unif. + * (3) It makes (possibly multiple) calls to + * TermDatabaseSygus::regstierEnumerator(...) based + * on the strategy, which inform the rest of the system to enumerate values + * of particular types in the grammar through use of fresh variables which + * we call "enumerators". + * + * Points (1)-(3) happen within a call to SygusPbe::initialize(...). + * + * Notice that each enumerator is associated with a single + * function-to-synthesize, but a function-to-sythesize may be mapped to multiple + * enumerators. Some public functions of this class expect an enumerator as + * input, which we map to a function-to-synthesize via + * TermDatabaseSygus::getSynthFunFor(e). + * + * An enumerator is initially "active" but may become inactive if the + * enumeration exhausts all possible values in the datatype corresponding to + * syntactic restrictions for it. The search may continue unless all enumerators + * become inactive. + * + * (4) During search, the extension of quantifier-free datatypes procedure for + * SyGuS datatypes may ask this class whether current candidates can be + * discarded based on inferring when two candidate solutions are equivalent + * up to examples. For example, the candidate solutions: + * f = \x ite( x < 0, x+1, x ) and f = \x x + * are equivalent up to examples on the above conjecture, since they have + * the same value on the points x = 0,5,6. Hence, we need only consider one of + * them. The interface for querying this is + * SygusPbe::addSearchVal(...). + * For details, see Reynolds et al. SYNT 2017. + * + * (5) When the extension of quantifier-free datatypes procedure for SyGuS + * datatypes terminates with a model, the parent of this class calls + * SygusPbe::getCandidateList(...), where this class returns the list + * of active enumerators. + * (6) The parent class subsequently calls + * SygusPbe::constructValues(...), which informs this class that new + * values have been enumerated for active enumerators, as indicated by the + * current model. This call also requests that based on these + * newly enumerated values, whether this class is now able to construct a + * solution based on the high-level strategy (stored in d_sygus_unif). + * + * This class is not designed to work in incremental mode, since there is no way + * to specify incremental problems in SyguS. + */ +class SygusPbe : public SygusModule { public: - CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p); - ~CegConjecturePbe(); + SygusPbe(QuantifiersEngine* qe, SynthConjecture* p); + ~SygusPbe(); /** initialize this class * @@ -276,7 +276,7 @@ class CegConjecturePbe : public SygusModule Node addPbeExample(TypeNode etn, Node e, Node b, - CegConjecturePbe* cpbe, + SygusPbe* cpbe, unsigned index, unsigned ntotal); @@ -286,7 +286,7 @@ class CegConjecturePbe : public SygusModule Node e, Node b, std::vector& ex, - CegConjecturePbe* cpbe, + SygusPbe* cpbe, unsigned index, unsigned ntotal); }; diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp index b0b6159be..a2454758a 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp @@ -29,7 +29,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -void CegConjectureProcessFun::init(Node f) +void SynthConjectureProcessFun::init(Node f) { d_synth_fun = f; Assert(f.getType().isFunction()); @@ -47,11 +47,11 @@ void CegConjectureProcessFun::init(Node f) Node k = NodeManager::currentNM()->mkBoundVar(ss.str(), atn); d_arg_vars.push_back(k); d_arg_var_num[k] = j; - d_arg_props.push_back(CegConjectureProcessArg()); + d_arg_props.push_back(SynthConjectureProcessArg()); } } -bool CegConjectureProcessFun::checkMatch( +bool SynthConjectureProcessFun::checkMatch( Node cn, Node n, std::unordered_map& n_arg_map) { std::vector vars; @@ -73,7 +73,7 @@ bool CegConjectureProcessFun::checkMatch( return cn_subs == n; } -bool CegConjectureProcessFun::isArgVar(Node n, unsigned& arg_index) +bool SynthConjectureProcessFun::isArgVar(Node n, unsigned& arg_index) { if (n.isVar()) { @@ -88,7 +88,7 @@ bool CegConjectureProcessFun::isArgVar(Node n, unsigned& arg_index) return false; } -Node CegConjectureProcessFun::inferDefinition( +Node SynthConjectureProcessFun::inferDefinition( Node n, std::unordered_map& term_to_arg_carry, std::unordered_map& args) +unsigned SynthConjectureProcessFun::assignRelevantDef( + Node def, std::vector& args) { unsigned id = 0; if (def.isNull()) @@ -250,7 +250,7 @@ unsigned CegConjectureProcessFun::assignRelevantDef(Node def, return rid; } -void CegConjectureProcessFun::processTerms( +void SynthConjectureProcessFun::processTerms( std::vector& ns, std::vector& ks, Node nf, @@ -504,12 +504,12 @@ void CegConjectureProcessFun::processTerms( } } -bool CegConjectureProcessFun::isArgRelevant(unsigned i) +bool SynthConjectureProcessFun::isArgRelevant(unsigned i) { return d_arg_props[i].d_relevant; } -void CegConjectureProcessFun::getIrrelevantArgs( +void SynthConjectureProcessFun::getIrrelevantArgs( std::unordered_set& args) { for (unsigned i = 0; i < d_arg_vars.size(); i++) @@ -521,15 +521,15 @@ void CegConjectureProcessFun::getIrrelevantArgs( } } -CegConjectureProcess::CegConjectureProcess(QuantifiersEngine* qe) {} -CegConjectureProcess::~CegConjectureProcess() {} -Node CegConjectureProcess::preSimplify(Node q) +SynthConjectureProcess::SynthConjectureProcess(QuantifiersEngine* qe) {} +SynthConjectureProcess::~SynthConjectureProcess() {} +Node SynthConjectureProcess::preSimplify(Node q) { Trace("sygus-process") << "Pre-simplify conjecture : " << q << std::endl; return q; } -Node CegConjectureProcess::postSimplify(Node q) +Node SynthConjectureProcess::postSimplify(Node q) { Trace("sygus-process") << "Post-simplify conjecture : " << q << std::endl; Assert(q.getKind() == FORALL); @@ -561,7 +561,7 @@ Node CegConjectureProcess::postSimplify(Node q) getComponentVector(AND, base, conjuncts); // process the conjunctions - for (std::map::iterator it = + for (std::map::iterator it = d_sf_info.begin(); it != d_sf_info.end(); ++it) @@ -577,7 +577,7 @@ Node CegConjectureProcess::postSimplify(Node q) return q; } -void CegConjectureProcess::initialize(Node n, std::vector& candidates) +void SynthConjectureProcess::initialize(Node n, std::vector& candidates) { if (Trace.isOn("sygus-process")) { @@ -590,13 +590,13 @@ void CegConjectureProcess::initialize(Node n, std::vector& candidates) } } -bool CegConjectureProcess::isArgRelevant(Node f, unsigned i) +bool SynthConjectureProcess::isArgRelevant(Node f, unsigned i) { if (!options::sygusArgRelevant()) { return true; } - std::map::iterator its = d_sf_info.find(f); + std::map::iterator its = d_sf_info.find(f); if (its != d_sf_info.end()) { return its->second.isArgRelevant(i); @@ -605,10 +605,10 @@ bool CegConjectureProcess::isArgRelevant(Node f, unsigned i) return true; } -bool CegConjectureProcess::getIrrelevantArgs(Node f, - std::unordered_set& args) +bool SynthConjectureProcess::getIrrelevantArgs( + Node f, std::unordered_set& args) { - std::map::iterator its = d_sf_info.find(f); + std::map::iterator its = d_sf_info.find(f); if (its != d_sf_info.end()) { its->second.getIrrelevantArgs(args); @@ -617,7 +617,7 @@ bool CegConjectureProcess::getIrrelevantArgs(Node f, return false; } -void CegConjectureProcess::processConjunct( +void SynthConjectureProcess::processConjunct( Node n, Node f, std::unordered_set& synth_fv) { Trace("sygus-process-arg-deps") << "Process conjunct: " << std::endl; @@ -655,7 +655,7 @@ void CegConjectureProcess::processConjunct( // process the applications of synthesis functions if (!ns.empty()) { - std::map::iterator its = d_sf_info.find(f); + std::map::iterator its = d_sf_info.find(f); if (its != d_sf_info.end()) { its->second.processTerms(ns, ks, nf, synth_fv_n, free_vars); @@ -663,7 +663,7 @@ void CegConjectureProcess::processConjunct( } } -Node CegConjectureProcess::CegConjectureProcess::flatten( +Node SynthConjectureProcess::SynthConjectureProcess::flatten( Node n, Node f, std::unordered_set& synth_fv, @@ -728,7 +728,7 @@ Node CegConjectureProcess::CegConjectureProcess::flatten( return visited[n]; } -void CegConjectureProcess::getFreeVariables( +void SynthConjectureProcess::getFreeVariables( Node n, std::unordered_set& synth_fv, std::unordered_map& args) +void SynthConjectureProcess::debugPrint(const char* c) {} +void SynthConjectureProcess::getComponentVector(Kind k, + Node n, + std::vector& args) { if (n.getKind() == k) { diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h index b16118b2e..199619699 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.h +++ b/src/theory/quantifiers/sygus/sygus_process_conj.h @@ -88,10 +88,10 @@ namespace quantifiers { * position in the function to synthesize is * relevant. */ -class CegConjectureProcessArg +class SynthConjectureProcessArg { public: - CegConjectureProcessArg() : d_var_single_occ(false), d_relevant(false) {} + SynthConjectureProcessArg() : d_var_single_occ(false), d_relevant(false) {} /** template definition * This is the term s[z] described * under "Argument Invariance" above. @@ -120,11 +120,11 @@ class CegConjectureProcessArg * It maintains information about each of the function to * synthesize's arguments. */ -struct CegConjectureProcessFun +struct SynthConjectureProcessFun { public: - CegConjectureProcessFun() {} - ~CegConjectureProcessFun() {} + SynthConjectureProcessFun() {} + ~SynthConjectureProcessFun() {} /** initialize this class for function f */ void init(Node f); /** process terms @@ -159,12 +159,12 @@ struct CegConjectureProcessFun /** the synth fun associated with this */ Node d_synth_fun; /** properties of each argument */ - std::vector d_arg_props; + std::vector d_arg_props; /** variables for each argument type of f * * These are used to express templates for argument * invariance, in the data member - * CegConjectureProcessArg::d_template. + * SynthConjectureProcessArg::d_template. */ std::vector d_arg_vars; /** map from d_arg_vars to the argument # @@ -254,51 +254,50 @@ struct CegConjectureProcessFun }; /** Ceg Conjecture Process -* -* This class implements static techniques for preprocessing and analysis of -* sygus conjectures. -* -* It is used as a back-end to CegConjecture, which calls it using the following -* interface: -* (1) When a sygus conjecture is asserted, we call -* CegConjectureProcess::simplify( q ), -* where q is the sygus conjecture in original form. -* -* (2) After a sygus conjecture is simplified and converted to deep -* embedding form, we call CegConjectureProcess::initialize( n, candidates ). -* -* (3) During enumerative SyGuS search, calls may be made by -* the extension of the quantifier-free datatypes decision procedure for -* sygus to CegConjectureProcess::getSymmetryBreakingPredicate(...), which are -* used for pruning search space based on conjecture-specific analysis. -*/ -class CegConjectureProcess + * + * This class implements static techniques for preprocessing and analysis of + * sygus conjectures. + * + * It is used as a back-end to SynthConjecture, which calls it using the + * following interface: (1) When a sygus conjecture is asserted, we call + * SynthConjectureProcess::simplify( q ), + * where q is the sygus conjecture in original form. + * + * (2) After a sygus conjecture is simplified and converted to deep + * embedding form, we call SynthConjectureProcess::initialize( n, candidates ). + * + * (3) During enumerative SyGuS search, calls may be made by + * the extension of the quantifier-free datatypes decision procedure for + * sygus to SynthConjectureProcess::getSymmetryBreakingPredicate(...), which are + * used for pruning search space based on conjecture-specific analysis. + */ +class SynthConjectureProcess { public: - CegConjectureProcess(QuantifiersEngine* qe); - ~CegConjectureProcess(); + SynthConjectureProcess(QuantifiersEngine* qe); + ~SynthConjectureProcess(); /** simplify the synthesis conjecture q - * Returns a formula that is equivalent to q. - * This simplification pass is called before all others - * in CegConjecture::assign. - * - * This function is intended for simplifications that - * impact whether or not the synthesis conjecture is - * single-invocation. - */ + * Returns a formula that is equivalent to q. + * This simplification pass is called before all others + * in SynthConjecture::assign. + * + * This function is intended for simplifications that + * impact whether or not the synthesis conjecture is + * single-invocation. + */ Node preSimplify(Node q); /** simplify the synthesis conjecture q - * Returns a formula that is equivalent to q. - * This simplification pass is called after all others - * in CegConjecture::assign. - */ + * Returns a formula that is equivalent to q. + * This simplification pass is called after all others + * in SynthConjecture::assign. + */ Node postSimplify(Node q); /** initialize - * - * n is the "base instantiation" of the deep-embedding version of - * the synthesis conjecture under "candidates". - * (see CegConjecture::d_base_inst) - */ + * + * n is the "base instantiation" of the deep-embedding version of + * the synthesis conjecture under "candidates". + * (see SynthConjecture::d_base_inst) + */ void initialize(Node n, std::vector& candidates); /** is the i^th argument of the function-to-synthesize f relevant? */ bool isArgRelevant(Node f, unsigned i); @@ -352,7 +351,7 @@ class CegConjectureProcess std::unordered_set, NodeHashFunction>& free_vars); /** for each synth-fun, information that is specific to this conjecture */ - std::map d_sf_info; + std::map d_sf_info; /** get component vector */ void getComponentVector(Kind k, Node n, std::vector& args); diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 66639b750..b8d98a6f7 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -18,7 +18,7 @@ #include "options/quantifiers_options.h" #include "printer/printer.h" #include "theory/datatypes/datatypes_rewriter.h" -#include "theory/quantifiers/sygus/ce_guided_conjecture.h" +#include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include @@ -29,7 +29,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SygusUnifRl::SygusUnifRl(CegConjecture* p) : d_parent(p) {} +SygusUnifRl::SygusUnifRl(SynthConjecture* p) : d_parent(p) {} SygusUnifRl::~SygusUnifRl() {} void SygusUnifRl::initializeCandidate( QuantifiersEngine* qe, diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index aad3c0b49..7b07de34e 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -35,7 +35,7 @@ using BoolNodePairMap = using NodePairMap = std::unordered_map; using NodePair = std::pair; -class CegConjecture; +class SynthConjecture; /** Sygus unification Refinement Lemmas utility * @@ -46,7 +46,7 @@ class CegConjecture; class SygusUnifRl : public SygusUnif { public: - SygusUnifRl(CegConjecture* p); + SygusUnifRl(SynthConjecture* p); ~SygusUnifRl(); /** initialize */ @@ -105,7 +105,7 @@ class SygusUnifRl : public SygusUnif protected: /** reference to the parent conjecture */ - CegConjecture* d_parent; + SynthConjecture* d_parent; /* Functions-to-synthesize (a.k.a. candidates) with unification strategies */ std::unordered_set d_unif_candidates; /** construct sol */ diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp new file mode 100644 index 000000000..fde69d196 --- /dev/null +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -0,0 +1,940 @@ +/********************* */ +/*! \file synth_conjecture.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King, Haniel Barbosa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 class that encapsulates techniques for a single + ** (SyGuS) synthesis conjecture. + **/ +#include "theory/quantifiers/sygus/synth_conjecture.h" + +#include "expr/datatype.h" +#include "options/base_options.h" +#include "options/datatypes_options.h" +#include "options/quantifiers_options.h" +#include "printer/printer.h" +#include "prop/prop_engine.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "smt/smt_statistics_registry.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/sygus/synth_engine.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/quantifiers/term_util.h" +#include "theory/theory_engine.h" + +using namespace CVC4::kind; +using namespace std; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +SynthConjecture::SynthConjecture(QuantifiersEngine* qe) + : d_qe(qe), + d_ceg_si(new CegSingleInv(qe, this)), + d_ceg_proc(new SynthConjectureProcess(qe)), + d_ceg_gc(new CegGrammarConstructor(qe, this)), + d_sygus_rconst(new SygusRepairConst(qe)), + d_ceg_pbe(new SygusPbe(qe, this)), + d_ceg_cegis(new Cegis(qe, this)), + d_ceg_cegisUnif(new CegisUnif(qe, this)), + d_master(nullptr), + d_set_ce_sk_vars(false), + d_repair_index(0), + d_refine_count(0) +{ + if (options::sygusSymBreakPbe() || options::sygusUnifPbe()) + { + d_modules.push_back(d_ceg_pbe.get()); + } + if (options::sygusUnif()) + { + d_modules.push_back(d_ceg_cegisUnif.get()); + } + d_modules.push_back(d_ceg_cegis.get()); +} + +SynthConjecture::~SynthConjecture() {} + +void SynthConjecture::assign(Node q) +{ + Assert(d_embed_quant.isNull()); + Assert(q.getKind() == FORALL); + Trace("cegqi") << "SynthConjecture : assign : " << q << std::endl; + d_quant = q; + NodeManager* nm = NodeManager::currentNM(); + + // pre-simplify the quantified formula based on the process utility + d_simp_quant = d_ceg_proc->preSimplify(d_quant); + + std::map templates; + std::map templates_arg; + // register with single invocation if applicable + if (d_qe->getQuantAttributes()->isSygus(q)) + { + d_ceg_si->initialize(d_simp_quant); + d_simp_quant = d_ceg_si->getSimplifiedConjecture(); + // carry the templates + for (unsigned i = 0; i < q[0].getNumChildren(); i++) + { + Node v = q[0][i]; + Node templ = d_ceg_si->getTemplate(v); + if (!templ.isNull()) + { + templates[v] = templ; + templates_arg[v] = d_ceg_si->getTemplateArg(v); + } + } + } + + // post-simplify the quantified formula based on the process utility + d_simp_quant = d_ceg_proc->postSimplify(d_simp_quant); + + // finished simplifying the quantified formula at this point + + // convert to deep embedding and finalize single invocation here + d_embed_quant = d_ceg_gc->process(d_simp_quant, templates, templates_arg); + Trace("cegqi") << "SynthConjecture : converted to embedding : " + << d_embed_quant << std::endl; + + // we now finalize the single invocation module, based on the syntax + // restrictions + if (d_qe->getQuantAttributes()->isSygus(q)) + { + d_ceg_si->finishInit(d_ceg_gc->isSyntaxRestricted()); + } + + Assert(d_candidates.empty()); + std::vector vars; + for (unsigned i = 0; i < d_embed_quant[0].getNumChildren(); i++) + { + vars.push_back(d_embed_quant[0][i]); + Node e = + NodeManager::currentNM()->mkSkolem("e", d_embed_quant[0][i].getType()); + d_candidates.push_back(e); + } + Trace("cegqi") << "Base quantified formula is : " << d_embed_quant + << std::endl; + // construct base instantiation + 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; + + // initialize the sygus constant repair utility + if (options::sygusRepairConst()) + { + d_sygus_rconst->initialize(d_base_inst.negate(), d_candidates); + if (options::sygusConstRepairAbort()) + { + if (!d_sygus_rconst->isActive()) + { + // no constant repair is possible: abort + std::stringstream ss; + ss << "Grammar does not allow repair constants." << std::endl; + throw LogicException(ss.str()); + } + } + } + + // register this term with sygus database and other utilities that impact + // the enumerative sygus search + std::vector guarded_lemmas; + if (!isSingleInvocation()) + { + d_ceg_proc->initialize(d_base_inst, d_candidates); + 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); + } + + Assert(d_qe->getQuantAttributes()->isSygus(q)); + // 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); + } + } + + // initialize the guard + d_feasible_guard = nm->mkSkolem("G", nm->booleanType()); + d_feasible_guard = Rewriter::rewrite(d_feasible_guard); + d_feasible_guard = d_qe->getValuation().ensureLiteral(d_feasible_guard); + AlwaysAssert(!d_feasible_guard.isNull()); + // register the strategy + d_feasible_strategy.reset( + new DecisionStrategySingleton("sygus_feasible", + d_feasible_guard, + d_qe->getSatContext(), + d_qe->getValuation())); + d_qe->getTheoryEngine()->getDecisionManager()->registerStrategy( + DecisionManager::STRAT_QUANT_SYGUS_FEASIBLE, d_feasible_strategy.get()); + // this must be called, both to ensure that the feasible guard is + // decided on with true polariy, but also to ensure that output channel + // 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++) + { + Node lem = nm->mkNode(OR, gneg, guarded_lemmas[i]); + Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem + << std::endl; + d_qe->getOutputChannel().lemma(lem); + } + + if (options::sygusStream()) + { + d_stream_strategy.reset(new SygusStreamDecisionStrategy( + d_qe->getSatContext(), d_qe->getValuation())); + d_qe->getTheoryEngine()->getDecisionManager()->registerStrategy( + DecisionManager::STRAT_QUANT_SYGUS_STREAM_FEASIBLE, + d_stream_strategy.get()); + d_current_stream_guard = d_stream_strategy->getLiteral(0); + } + Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() + << std::endl; +} + +Node SynthConjecture::getGuard() const { return d_feasible_guard; } + +bool SynthConjecture::isSingleInvocation() const +{ + return d_ceg_si->isSingleInvocation(); +} + +bool SynthConjecture::needsCheck() +{ + if (isSingleInvocation() && !d_ceg_si->needsCheck()) + { + return false; + } + bool value; + Assert(!d_feasible_guard.isNull()); + // non or fully single invocation : look at guard only + if (d_qe->getValuation().hasSatValue(d_feasible_guard, value)) + { + if (!value) + { + Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl; + return false; + } + } + else + { + Trace("cegqi-warn") << "WARNING: Guard " << d_feasible_guard + << " is not assigned!" << std::endl; + Assert(false); + } + 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; } +void SynthConjecture::doCheck(std::vector& lems) +{ + Assert(d_master != nullptr); + + // process the sygus streaming guard + if (options::sygusStream()) + { + Assert(!isSingleInvocation()); + // it may be the case that we have a new solution now + Node currGuard = getCurrentStreamGuard(); + if (currGuard != d_current_stream_guard) + { + // we have a new guard, print and continue the stream + printAndContinueStream(); + d_current_stream_guard = currGuard; + return; + } + } + + // get the list of terms that the master strategy is interested in + std::vector terms; + d_master->getTermList(d_candidates, terms); + + Assert(!d_candidates.empty()); + + Trace("cegqi-check") << "CegConjuncture : check, build candidates..." + << std::endl; + std::vector candidate_values; + bool constructed_cand = false; + + // If a module is not trying to repair constants in solutions and the option + // sygusRepairConst is true, we use a default scheme for trying to repair + // constants here. + if (options::sygusRepairConst() && !d_master->usingRepairConst()) + { + // have we tried to repair the previous solution? + // if not, call the repair constant utility + unsigned ninst = d_cinfo[d_candidates[0]].d_inst.size(); + if (d_repair_index < ninst) + { + std::vector fail_cvs; + for (const Node& cprog : d_candidates) + { + Assert(d_repair_index < d_cinfo[cprog].d_inst.size()); + fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]); + } + if (Trace.isOn("cegqi-check")) + { + Trace("cegqi-check") << "CegConjuncture : repair previous solution "; + for (const Node& fc : fail_cvs) + { + std::stringstream ss; + Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, fc); + Trace("cegqi-check") << ss.str() << " "; + } + Trace("cegqi-check") << std::endl; + } + d_repair_index++; + if (d_sygus_rconst->repairSolution( + d_candidates, fail_cvs, candidate_values, true)) + { + constructed_cand = true; + } + } + } + + // get the model value of the relevant terms from the master module + std::vector enum_values; + getModelValues(terms, enum_values); + + if (!constructed_cand) + { + Assert(candidate_values.empty()); + 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, size = candidate_values.size(); i < size; i++) + { + Trace("cegqi-check") << " " << i << " : " << d_candidates[i] << " -> " + << candidate_values[i] << std::endl; + } + } + 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) && 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. + Node lem = nm->mkNode(OR, d_quant.negate(), nm->mkConst(false)); + lem = getStreamGuardedLemma(lem); + lems.push_back(lem); + recordInstantiation(candidate_values); + return; + } + Assert(!d_set_ce_sk_vars); + } + else + { + if (!constructed_cand) + { + return; + } + } + + // immediately skolemize inner existentials + Node lem; + // introduce the skolem variables + std::vector sks; + if (constructed_cand) + { + if (inst.getKind() == NOT && inst[0].getKind() == FORALL) + { + std::vector vars; + for (const Node& v : inst[0][0]) + { + Node sk = nm->mkSkolem("rsk", v.getType()); + sks.push_back(sk); + vars.push_back(v); + Trace("cegqi-check-debug") + << " introduce skolem " << sk << " for " << v << "\n"; + } + lem = inst[0][1].substitute( + vars.begin(), vars.end(), sks.begin(), sks.end()); + lem = lem.negate(); + } + else + { + // use the instance itself + lem = inst; + } + } + if (sk_refine) + { + d_ce_sk_vars.insert(d_ce_sk_vars.end(), sks.begin(), sks.end()); + d_set_ce_sk_vars = true; + } + + if (lem.isNull()) + { + // no lemma to check + return; + } + + lem = Rewriter::rewrite(lem); + // eagerly unfold applications of evaluation function + Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl; + std::map visited_n; + lem = d_qe->getTermDatabaseSygus()->getEagerUnfold(lem, visited_n); + // record the instantiation + // this is used for remembering the solution + recordInstantiation(candidate_values); + Node query = lem; + bool success = false; + if (query.isConst() && !query.getConst()) + { + // short circuit the check + lem = d_quant.negate(); + success = true; + } + 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(), query); + if (options::sygusVerifySubcall()) + { + Trace("cegqi-engine") << " *** Verify with subcall..." << std::endl; + SmtEngine verifySmt(nm->toExprManager()); + verifySmt.setLogic(smt::currentSmtEngine()->getLogicInfo()); + verifySmt.assertFormula(query.toExpr()); + Result r = verifySmt.checkSat(); + Trace("cegqi-engine") << " ...got " << r << std::endl; + if (r.asSatisfiabilityResult().isSat() == Result::SAT) + { + Trace("cegqi-engine") << " * Verification lemma failed for:\n "; + // do not send out + for (const Node& v : d_ce_sk_vars) + { + Node mv = Node::fromExpr(verifySmt.getValue(v.toExpr())); + Trace("cegqi-engine") << v << " -> " << mv << " "; + d_ce_sk_var_mvs.push_back(mv); + } + Trace("cegqi-engine") << std::endl; +#ifdef CVC4_ASSERTIONS + // the values for the query should be a complete model + Node squery = query.substitute(d_ce_sk_vars.begin(), + d_ce_sk_vars.end(), + d_ce_sk_var_mvs.begin(), + d_ce_sk_var_mvs.end()); + Trace("cegqi-debug") << "...squery : " << squery << std::endl; + squery = Rewriter::rewrite(squery); + Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl; + Assert(squery.isConst() && squery.getConst()); +#endif + return; + } + else if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + // if the result in the subcall was unsatisfiable, we avoid + // rechecking, hence we drop "query" from the verification lemma + lem = d_quant.negate(); + // we can short circuit adding the lemma (for sygus stream) + success = true; + } + // In the rare case that the subcall is unknown, we add the verification + // lemma in the main solver. This should only happen if the quantifier + // free logic is undecidable. + } + } + if (success && 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; + } + lem = getStreamGuardedLemma(lem); + lems.push_back(lem); +} + +void SynthConjecture::doRefine(std::vector& lems) +{ + Assert(lems.empty()); + Assert(d_set_ce_sk_vars); + + // first, make skolem substitution + Trace("cegqi-refine") << "doRefine : construct skolem substitution..." + << std::endl; + std::vector sk_vars; + std::vector sk_subs; + // collect the substitution over all disjuncts + if (!d_ce_sk_vars.empty()) + { + Trace("cegqi-refine") << "Get model values for skolems..." << std::endl; + Assert(d_inner_vars.size() == d_ce_sk_vars.size()); + if (d_ce_sk_var_mvs.empty()) + { + std::vector model_values; + getModelValues(d_ce_sk_vars, model_values); + sk_subs.insert(sk_subs.end(), model_values.begin(), model_values.end()); + } + else + { + Assert(d_ce_sk_var_mvs.size() == d_ce_sk_vars.size()); + sk_subs.insert( + sk_subs.end(), d_ce_sk_var_mvs.begin(), d_ce_sk_var_mvs.end()); + } + sk_vars.insert(sk_vars.end(), d_inner_vars.begin(), d_inner_vars.end()); + } + else + { + Assert(d_inner_vars.empty()); + } + + std::vector lem_c; + Trace("cegqi-refine") << "doRefine : Construct refinement lemma..." + << std::endl; + Trace("cegqi-refine-debug") + << " For counterexample skolems : " << d_ce_sk_vars << std::endl; + Node base_lem; + if (d_base_inst.getKind() == NOT && d_base_inst[0].getKind() == FORALL) + { + base_lem = d_base_inst[0][1]; + } + else + { + base_lem = d_base_inst.negate(); + } + + Assert(sk_vars.size() == sk_subs.size()); + + Trace("cegqi-refine") << "doRefine : substitute..." << std::endl; + base_lem = base_lem.substitute( + sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end()); + Trace("cegqi-refine") << "doRefine : rewrite..." << std::endl; + base_lem = Rewriter::rewrite(base_lem); + Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem + << "..." << std::endl; + d_master->registerRefinementLemma(sk_vars, base_lem, lems); + Trace("cegqi-refine") << "doRefine : finished" << std::endl; + d_set_ce_sk_vars = false; + d_ce_sk_vars.clear(); + d_ce_sk_var_mvs.clear(); +} + +void SynthConjecture::preregisterConjecture(Node q) +{ + d_ceg_si->preregisterConjecture(q); +} + +void SynthConjecture::getModelValues(std::vector& n, std::vector& v) +{ + Trace("cegqi-engine") << " * Value is : "; + for (unsigned i = 0; i < n.size(); i++) + { + Node nv = getModelValue(n[i]); + v.push_back(nv); + if (Trace.isOn("cegqi-engine")) + { + TypeNode tn = nv.getType(); + Trace("cegqi-engine") << n[i] << " -> "; + std::stringstream ss; + Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, nv); + Trace("cegqi-engine") << ss.str() << " "; + if (Trace.isOn("cegqi-engine-rr")) + { + Node bv = d_qe->getTermDatabaseSygus()->sygusToBuiltin(nv, tn); + bv = Rewriter::rewrite(bv); + Trace("cegqi-engine-rr") << " -> " << bv << std::endl; + } + } + Assert(!nv.isNull()); + } + Trace("cegqi-engine") << std::endl; +} + +Node SynthConjecture::getModelValue(Node n) +{ + Trace("cegqi-mv") << "getModelValue for : " << n << std::endl; + return d_qe->getModel()->getValue(n); +} + +void SynthConjecture::debugPrint(const char* c) +{ + Trace(c) << "Synthesis conjecture : " << d_embed_quant << std::endl; + Trace(c) << " * Candidate programs : " << d_candidates << std::endl; + Trace(c) << " * Counterexample skolems : " << d_ce_sk_vars << std::endl; +} + +Node SynthConjecture::getCurrentStreamGuard() const +{ + if (d_stream_strategy != nullptr) + { + // the stream guard is the current asserted literal of the stream strategy + Node lit = d_stream_strategy->getAssertedLiteral(); + if (lit.isNull()) + { + // if none exist, get the first + lit = d_stream_strategy->getLiteral(0); + } + return lit; + } + return Node::null(); +} + +Node SynthConjecture::getStreamGuardedLemma(Node n) const +{ + if (options::sygusStream()) + { + // if we are in streaming mode, we guard with the current stream guard + Node csg = getCurrentStreamGuard(); + Assert(!csg.isNull()); + return NodeManager::currentNM()->mkNode(kind::OR, csg.negate(), n); + } + return n; +} + +SynthConjecture::SygusStreamDecisionStrategy::SygusStreamDecisionStrategy( + context::Context* satContext, Valuation valuation) + : DecisionStrategyFmf(satContext, valuation) +{ +} + +Node SynthConjecture::SygusStreamDecisionStrategy::mkLiteral(unsigned i) +{ + NodeManager* nm = NodeManager::currentNM(); + Node curr_stream_guard = nm->mkSkolem("G_Stream", nm->booleanType()); + return curr_stream_guard; +} + +void SynthConjecture::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_set_ce_sk_vars = false; + d_ce_sk_vars.clear(); + d_ce_sk_var_mvs.clear(); + // However, we need to exclude the current solution using an explicit + // blocking clause, so that we proceed to the next solution. + std::vector terms; + d_master->getTermList(d_candidates, terms); + std::vector 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()->getExplanationForEquality( + 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 SynthConjecture::printSynthSolution(std::ostream& out, + bool singleInvocation) +{ + Trace("cegqi-debug") << "Printing synth solution..." << std::endl; + Assert(d_quant[0].getNumChildren() == d_embed_quant[0].getNumChildren()); + std::vector sols; + std::vector statuses; + if (!getSynthSolutionsInternal(sols, statuses, singleInvocation)) + { + return; + } + for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) + { + Node sol = sols[i]; + if (!sol.isNull()) + { + Node prog = d_embed_quant[0][i]; + int status = statuses[i]; + TypeNode tn = prog.getType(); + const Datatype& dt = static_cast(tn.toType()).getDatatype(); + std::stringstream ss; + ss << prog; + std::string f(ss.str()); + f.erase(f.begin()); + SynthEngine* cei = d_qe->getSynthEngine(); + ++(cei->d_statistics.d_solutions); + + bool is_unique_term = true; + + if (status != 0 && options::sygusRewSynth()) + { + std::map::iterator its = + d_exprm.find(prog); + if (its == d_exprm.end()) + { + d_exprm[prog].initializeSygus( + d_qe, d_candidates[i], options::sygusSamples(), true); + if (options::sygusRewSynth()) + { + d_exprm[prog].enableRewriteRuleSynth(); + } + its = d_exprm.find(prog); + } + bool rew_print = false; + is_unique_term = d_exprm[prog].addTerm(sol, out, rew_print); + if (rew_print) + { + ++(cei->d_statistics.d_candidate_rewrites_print); + } + if (!is_unique_term) + { + ++(cei->d_statistics.d_candidate_rewrites); + } + } + if (is_unique_term) + { + out << "(define-fun " << f << " "; + if (dt.getSygusVarList().isNull()) + { + out << "() "; + } + else + { + out << dt.getSygusVarList() << " "; + } + out << dt.getSygusType() << " "; + if (status == 0) + { + out << sol; + } + else + { + Printer::getPrinter(options::outputLanguage()) + ->toStreamSygus(out, sol); + } + out << ")" << std::endl; + } + } + } +} + +void SynthConjecture::getSynthSolutions(std::map& sol_map, + bool singleInvocation) +{ + NodeManager* nm = NodeManager::currentNM(); + TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus(); + std::vector sols; + std::vector statuses; + if (!getSynthSolutionsInternal(sols, statuses, singleInvocation)) + { + return; + } + for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) + { + Node sol = sols[i]; + int status = statuses[i]; + // get the builtin solution + Node bsol = sol; + if (status != 0) + { + // convert sygus to builtin here + bsol = sygusDb->sygusToBuiltin(sol, sol.getType()); + } + // convert to lambda + TypeNode tn = d_embed_quant[0][i].getType(); + const Datatype& dt = static_cast(tn.toType()).getDatatype(); + Node bvl = Node::fromExpr(dt.getSygusVarList()); + if (!bvl.isNull()) + { + bsol = nm->mkNode(LAMBDA, bvl, bsol); + } + // store in map + Node fvar = d_quant[0][i]; + Assert(fvar.getType() == bsol.getType()); + sol_map[fvar] = bsol; + } +} + +bool SynthConjecture::getSynthSolutionsInternal(std::vector& sols, + std::vector& statuses, + bool singleInvocation) +{ + for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) + { + Node prog = d_embed_quant[0][i]; + Trace("cegqi-debug") << " get solution for " << prog << std::endl; + TypeNode tn = prog.getType(); + Assert(tn.isDatatype()); + // get the solution + Node sol; + int status = -1; + if (singleInvocation) + { + Assert(d_ceg_si != NULL); + sol = d_ceg_si->getSolution(i, tn, status, true); + if (sol.isNull()) + { + return false; + } + sol = sol.getKind() == LAMBDA ? sol[1] : sol; + } + else + { + Node cprog = getCandidate(i); + if (!d_cinfo[cprog].d_inst.empty()) + { + // the solution is just the last instantiated term + sol = d_cinfo[cprog].d_inst.back(); + status = 1; + + // check if there was a template + Node sf = d_quant[0][i]; + Node templ = d_ceg_si->getTemplate(sf); + if (!templ.isNull()) + { + Trace("cegqi-inv-debug") + << sf << " used template : " << templ << std::endl; + // if it was not embedded into the grammar + if (!options::sygusTemplEmbedGrammar()) + { + TNode templa = d_ceg_si->getTemplateArg(sf); + // make the builtin version of the full solution + TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus(); + sol = sygusDb->sygusToBuiltin(sol, sol.getType()); + Trace("cegqi-inv") << "Builtin version of solution is : " << sol + << ", type : " << sol.getType() << std::endl; + TNode tsol = sol; + sol = templ.substitute(templa, tsol); + Trace("cegqi-inv-debug") << "With template : " << sol << std::endl; + sol = Rewriter::rewrite(sol); + Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl; + // now, reconstruct to the syntax + sol = d_ceg_si->reconstructToSyntax(sol, tn, status, true); + sol = sol.getKind() == LAMBDA ? sol[1] : sol; + Trace("cegqi-inv-debug") + << "Reconstructed to syntax : " << sol << std::endl; + } + else + { + Trace("cegqi-inv-debug") + << "...was embedding into grammar." << std::endl; + } + } + else + { + Trace("cegqi-inv-debug") + << sf << " did not use template" << std::endl; + } + } + else + { + Trace("cegqi-warn") << "WARNING : No recorded instantiations for " + "syntax-guided solution!" + << std::endl; + } + } + sols.push_back(sol); + statuses.push_back(status); + } + return true; +} + +Node SynthConjecture::getSymmetryBreakingPredicate( + Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth) +{ + std::vector sb_lemmas; + + // based on simple preprocessing + Node ppred = + d_ceg_proc->getSymmetryBreakingPredicate(x, e, tn, tindex, depth); + if (!ppred.isNull()) + { + sb_lemmas.push_back(ppred); + } + + // other static conjecture-dependent symmetry breaking goes here + + if (!sb_lemmas.empty()) + { + return sb_lemmas.size() == 1 + ? sb_lemmas[0] + : NodeManager::currentNM()->mkNode(kind::AND, sb_lemmas); + } + else + { + return Node::null(); + } +} + +} // namespace quantifiers +} // namespace theory +} /* namespace CVC4 */ diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h new file mode 100644 index 000000000..1cbd4e949 --- /dev/null +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -0,0 +1,298 @@ +/********************* */ +/*! \file synth_conjecture.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King, Haniel Barbosa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 Class that encapsulates techniques for a single (SyGuS) synthesis + ** conjecture. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H +#define __CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H + +#include + +#include "theory/decision_manager.h" +#include "theory/quantifiers/expr_miner_manager.h" +#include "theory/quantifiers/sygus/ce_guided_single_inv.h" +#include "theory/quantifiers/sygus/cegis.h" +#include "theory/quantifiers/sygus/cegis_unif.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/sygus_repair_const.h" +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** a synthesis conjecture + * This class implements approaches for a synthesis conecjture, given by data + * member d_quant. + * This includes both approaches for synthesis in Reynolds et al CAV 2015. It + * determines which approach and optimizations are applicable to the + * conjecture, and has interfaces for implementing them. + */ +class SynthConjecture +{ + public: + SynthConjecture(QuantifiersEngine* qe); + ~SynthConjecture(); + /** get original version of conjecture */ + Node getConjecture() { return d_quant; } + /** get deep embedding version of conjecture */ + Node getEmbeddedConjecture() { return d_embed_quant; } + //-------------------------------for counterexample-guided check/refine + /** increment the number of times we have successfully done candidate + * refinement */ + void incrementRefineCount() { d_refine_count++; } + /** whether the conjecture is waiting for a call to doCheck below */ + 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. + */ + void doCheck(std::vector& lems); + /** do refinement + * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015. + */ + void doRefine(std::vector& lems); + //-------------------------------end for counterexample-guided check/refine + /** + * prints the synthesis solution to output stream out. + * + * singleInvocation : set to true if we should consult the single invocation + * module to get synthesis solutions. + */ + void printSynthSolution(std::ostream& out, bool singleInvocation); + /** get synth solutions + * + * This returns a map from function-to-synthesize variables to their + * builtin solution, which has the same type. For example, for synthesis + * conjecture exists f. forall x. f( x )>x, this function may return the map + * containing the entry: + * f -> (lambda x. x+1) + * + * singleInvocation : set to true if we should consult the single invocation + * module to get synthesis solutions. + */ + void getSynthSolutions(std::map& sol_map, bool singleInvocation); + /** + * The feasible guard whose semantics are "this conjecture is feasiable". + * This is "G" in Figure 3 of Reynolds et al CAV 2015. + */ + Node getGuard() const; + /** is ground */ + bool isGround() { return d_inner_vars.empty(); } + /** are we using single invocation techniques */ + bool isSingleInvocation() const; + /** preregister conjecture + * This is used as a heuristic for solution reconstruction, so that we + * remember expressions in the conjecture before preprocessing, since they + * may be helpful during solution reconstruction (Figure 5 of Reynolds et al + * CAV 2015) + */ + void preregisterConjecture(Node q); + /** assign conjecture q to this class */ + void assign(Node q); + /** has a conjecture been assigned to this class */ + bool isAssigned() { return !d_embed_quant.isNull(); } + /** get model values for terms n, store in vector v */ + void getModelValues(std::vector& n, std::vector& v); + /** get model value for term n */ + Node getModelValue(Node n); + + /** get utility for static preprocessing and analysis of conjectures */ + SynthConjectureProcess* getProcess() { return d_ceg_proc.get(); } + /** get constant repair utility */ + SygusRepairConst* getRepairConst() { return d_sygus_rconst.get(); } + /** get program by examples module */ + SygusPbe* getPbe() { return d_ceg_pbe.get(); } + /** get the symmetry breaking predicate for type */ + Node getSymmetryBreakingPredicate( + Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth); + /** print out debug information about this conjecture */ + void debugPrint(const char* c); + + private: + /** reference to quantifier engine */ + QuantifiersEngine* d_qe; + /** The feasible guard. */ + Node d_feasible_guard; + /** the decision strategy for the feasible guard */ + std::unique_ptr d_feasible_strategy; + /** single invocation utility */ + std::unique_ptr d_ceg_si; + /** utility for static preprocessing and analysis of conjectures */ + std::unique_ptr d_ceg_proc; + /** grammar utility */ + std::unique_ptr d_ceg_gc; + /** repair constant utility */ + std::unique_ptr d_sygus_rconst; + + //------------------------modules + /** program by examples module */ + std::unique_ptr d_ceg_pbe; + /** CEGIS module */ + std::unique_ptr d_ceg_cegis; + /** CEGIS UNIF module */ + std::unique_ptr d_ceg_cegisUnif; + /** the set of active modules (subset of the above list) */ + std::vector 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. + */ + std::vector d_candidates; + /** base instantiation + * If d_embed_quant is forall d. exists y. P( d, y ), then + * this is the formula exists y. P( d_candidates, y ). Notice that + * (exists y. F) is shorthand above for ~( forall y. ~F ). + */ + Node d_base_inst; + /** list of variables on inner quantification */ + std::vector d_inner_vars; + /** + * The set of skolems for the current "verification" lemma, if one exists. + * This may be added to during calls to doCheck(). The model values for these + * skolems are analyzed during doRefine(). + */ + std::vector d_ce_sk_vars; + /** + * If we have already tested the satisfiability of the current verification + * lemma, this stores the model values of d_ce_sk_vars in the current + * (satisfiable, failed) verification lemma. + */ + std::vector d_ce_sk_var_mvs; + /** + * Whether the above vector has been set. We have this flag since the above + * vector may be set to empty (e.g. for ground synthesis conjectures). + */ + bool d_set_ce_sk_vars; + + /** the asserted (negated) conjecture */ + Node d_quant; + /** (negated) conjecture after simplification */ + Node d_simp_quant; + /** (negated) conjecture after simplification, conversion to deep embedding */ + Node d_embed_quant; + /** candidate information */ + class CandidateInfo + { + public: + CandidateInfo() {} + /** list of terms we have instantiated candidates with */ + std::vector d_inst; + }; + std::map d_cinfo; + /** + * The first index of an instantiation in CandidateInfo::d_inst that we have + * not yet tried to repair. + */ + unsigned d_repair_index; + /** number of times we have called doRefine */ + unsigned d_refine_count; + /** get candidadate */ + Node getCandidate(unsigned int i) { return d_candidates[i]; } + /** record instantiation (this is used to construct solutions later) */ + void recordInstantiation(std::vector& vs) + { + Assert(vs.size() == d_candidates.size()); + for (unsigned i = 0; i < vs.size(); i++) + { + d_cinfo[d_candidates[i]].d_inst.push_back(vs[i]); + } + } + /** get synth solutions internal + * + * This function constructs the body of solutions for all + * functions-to-synthesize in this conjecture and stores them in sols, in + * order. For each solution added to sols, we add an integer indicating what + * kind of solution n is, where if sols[i] = n, then + * if status[i] = 0: n is the (builtin term) corresponding to the solution, + * if status[i] = 1: n is the sygus representation of the solution. + * We store builtin versions under some conditions (such as when the sygus + * grammar is being ignored). + * + * singleInvocation : set to true if we should consult the single invocation + * module to get synthesis solutions. + * + * For example, for conjecture exists fg. forall x. f(x)>g(x), this function + * may set ( sols, status ) to ( { x+1, d_x() }, { 1, 0 } ), where d_x() is + * the sygus datatype constructor corresponding to variable x. + */ + bool getSynthSolutionsInternal(std::vector& sols, + std::vector& status, + bool singleInvocation); + //-------------------------------- sygus stream + /** current stream guard */ + Node d_current_stream_guard; + /** the decision strategy for streaming solutions */ + class SygusStreamDecisionStrategy : public DecisionStrategyFmf + { + public: + SygusStreamDecisionStrategy(context::Context* satContext, + Valuation valuation); + /** make literal */ + Node mkLiteral(unsigned i) override; + /** identify */ + std::string identify() const override + { + return std::string("sygus_stream"); + } + }; + std::unique_ptr d_stream_strategy; + /** get current stream guard */ + Node getCurrentStreamGuard() const; + /** get stream guarded lemma + * + * If sygusStream is enabled, this returns ( G V n ) where G is the guard + * returned by getCurrentStreamGuard, otherwise this returns n. + */ + Node getStreamGuardedLemma(Node n) const; + /** + * Prints the current synthesis solution to the output stream indicated by + * the Options object, send a lemma blocking the current solution to the + * output channel. + */ + void printAndContinueStream(); + //-------------------------------- end sygus stream + /** expression miner managers for each function-to-synthesize + * + * Notice that for each function-to-synthesize, we enumerate a stream of + * candidate solutions, where each of these streams is independent. Thus, + * we maintain separate expression miner managers for each of them. + * + * This is used for the sygusRewSynth() option to synthesize new candidate + * rewrite rules. + */ + std::map d_exprm; +}; + +} // namespace quantifiers +} // namespace theory +} /* namespace CVC4 */ + +#endif diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp new file mode 100644 index 000000000..56844ec1f --- /dev/null +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -0,0 +1,431 @@ +/********************* */ +/*! \file synth_engine.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 the quantifiers module for managing all approaches + ** to synthesis, in particular, those described in Reynolds et al CAV 2015. + ** + **/ +#include "theory/quantifiers/sygus/synth_engine.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/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/quantifiers/term_util.h" +#include "theory/theory_engine.h" + +using namespace CVC4::kind; +using namespace std; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c) + : QuantifiersModule(qe) +{ + d_conj = new SynthConjecture(qe); + d_last_inst_si = false; +} + +SynthEngine::~SynthEngine() { delete d_conj; } + +bool SynthEngine::needsCheck(Theory::Effort e) +{ + return !d_quantEngine->getTheoryEngine()->needCheck() + && e >= Theory::EFFORT_LAST_CALL; +} + +QuantifiersModule::QEffort SynthEngine::needsModel(Theory::Effort e) +{ + return d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL; +} + +void SynthEngine::check(Theory::Effort e, QEffort quant_e) +{ + // are we at the proper effort level? + unsigned echeck = + d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL; + if (quant_e != echeck) + { + return; + } + + // if we are waiting to assign the conjecture, do it now + if (!d_waiting_conj.isNull()) + { + Node q = d_waiting_conj; + Trace("cegqi-engine") << "--- Conjecture waiting to assign: " << q + << std::endl; + d_waiting_conj = Node::null(); + if (!d_conj->isAssigned()) + { + assignConjecture(q); + // assign conjecture always uses the output channel, we return and + // re-check here. + return; + } + } + + Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" + << std::endl; + Trace("cegqi-engine-debug") << std::endl; + bool active = false; + bool value; + if (d_quantEngine->getValuation().hasSatValue(d_conj->getConjecture(), value)) + { + active = value; + } + else + { + Trace("cegqi-engine-debug") + << "...no value for quantified formula." << std::endl; + } + Trace("cegqi-engine-debug") + << "Current conjecture status : active : " << active << std::endl; + if (active && d_conj->needsCheck()) + { + checkConjecture(d_conj); + } + Trace("cegqi-engine") + << "Finished Counterexample Guided Instantiation engine." << std::endl; +} + +bool SynthEngine::assignConjecture(Node q) +{ + if (d_conj->isAssigned()) + { + return false; + } + Trace("cegqi-engine") << "--- Assign conjecture " << q << std::endl; + if (options::sygusQePreproc()) + { + // the following does quantifier elimination as a preprocess step + // for "non-ground single invocation synthesis conjectures": + // exists f. forall xy. P[ f(x), x, y ] + // We run quantifier elimination: + // exists y. P[ z, x, y ] ----> Q[ z, x ] + // Where we replace the original conjecture with: + // exists f. forall x. Q[ f(x), x ] + // For more details, see Example 6 of Reynolds et al. SYNT 2017. + Node body = q[1]; + if (body.getKind() == NOT && body[0].getKind() == FORALL) + { + body = body[0][1]; + } + NodeManager* nm = NodeManager::currentNM(); + Trace("cegqi-qep") << "Compute single invocation for " << q << "..." + << std::endl; + quantifiers::SingleInvocationPartition sip; + std::vector funcs; + funcs.insert(funcs.end(), q[0].begin(), q[0].end()); + sip.init(funcs, body); + Trace("cegqi-qep") << "...finished, got:" << std::endl; + sip.debugPrint("cegqi-qep"); + + if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation()) + { + // create new smt engine to do quantifier elimination + SmtEngine smt_qe(nm->toExprManager()); + smt_qe.setLogic(smt::currentSmtEngine()->getLogicInfo()); + Trace("cegqi-qep") << "Property is non-ground single invocation, run " + "QE to obtain single invocation." + << std::endl; + // partition variables + std::vector all_vars; + sip.getAllVariables(all_vars); + std::vector si_vars; + sip.getSingleInvocationVariables(si_vars); + std::vector qe_vars; + std::vector nqe_vars; + for (unsigned i = 0, size = all_vars.size(); i < size; i++) + { + Node v = all_vars[i]; + if (std::find(si_vars.begin(), si_vars.end(), v) == si_vars.end()) + { + qe_vars.push_back(v); + } + else + { + nqe_vars.push_back(v); + } + } + std::vector orig; + std::vector subs; + // skolemize non-qe variables + for (unsigned i = 0, size = nqe_vars.size(); i < size; i++) + { + Node k = nm->mkSkolem( + "k", nqe_vars[i].getType(), "qe for non-ground single invocation"); + orig.push_back(nqe_vars[i]); + subs.push_back(k); + Trace("cegqi-qep") << " subs : " << nqe_vars[i] << " -> " << k + << std::endl; + } + std::vector funcs; + sip.getFunctions(funcs); + for (unsigned i = 0, size = funcs.size(); i < size; i++) + { + Node f = funcs[i]; + Node fi = sip.getFunctionInvocationFor(f); + Node fv = sip.getFirstOrderVariableForFunction(f); + Assert(!fi.isNull()); + orig.push_back(fi); + Node k = + nm->mkSkolem("k", + fv.getType(), + "qe for function in non-ground single invocation"); + subs.push_back(k); + Trace("cegqi-qep") << " subs : " << fi << " -> " << k << std::endl; + } + Node conj_se_ngsi = sip.getFullSpecification(); + Trace("cegqi-qep") << "Full specification is " << conj_se_ngsi + << std::endl; + Node conj_se_ngsi_subs = conj_se_ngsi.substitute( + orig.begin(), orig.end(), subs.begin(), subs.end()); + Assert(!qe_vars.empty()); + conj_se_ngsi_subs = nm->mkNode(EXISTS, + nm->mkNode(BOUND_VAR_LIST, qe_vars), + conj_se_ngsi_subs.negate()); + + Trace("cegqi-qep") << "Run quantifier elimination on " + << conj_se_ngsi_subs << std::endl; + Expr qe_res = smt_qe.doQuantifierElimination( + conj_se_ngsi_subs.toExpr(), true, false); + Trace("cegqi-qep") << "Result : " << qe_res << std::endl; + + // create single invocation conjecture + Node qe_res_n = Node::fromExpr(qe_res); + qe_res_n = qe_res_n.substitute( + subs.begin(), subs.end(), orig.begin(), orig.end()); + if (!nqe_vars.empty()) + { + qe_res_n = + nm->mkNode(EXISTS, nm->mkNode(BOUND_VAR_LIST, nqe_vars), qe_res_n); + } + Assert(q.getNumChildren() == 3); + qe_res_n = nm->mkNode(FORALL, q[0], qe_res_n, q[2]); + Trace("cegqi-qep") << "Converted conjecture after QE : " << qe_res_n + << std::endl; + qe_res_n = Rewriter::rewrite(qe_res_n); + Node nq = qe_res_n; + // must assert it is equivalent to the original + Node lem = q.eqNode(nq); + Trace("cegqi-lemma") << "Cegqi::Lemma : qe-preprocess : " << lem + << std::endl; + d_quantEngine->getOutputChannel().lemma(lem); + // we've reduced the original to a preprocessed version, return + return false; + } + } + d_conj->assign(q); + return true; +} + +void SynthEngine::registerQuantifier(Node q) +{ + if (d_quantEngine->getOwner(q) == this) + { // && d_eval_axioms.find( q )==d_eval_axioms.end() ){ + if (!d_conj->isAssigned()) + { + Trace("cegqi") << "Register conjecture : " << q << std::endl; + if (options::sygusQePreproc()) + { + d_waiting_conj = q; + } + else + { + // assign it now + assignConjecture(q); + } + } + else + { + Assert(d_conj->getEmbeddedConjecture() == q); + } + } + else + { + Trace("cegqi-debug") << "Register quantifier : " << q << std::endl; + } +} + +void SynthEngine::checkConjecture(SynthConjecture* conj) +{ + Node q = conj->getEmbeddedConjecture(); + Node aq = conj->getConjecture(); + if (Trace.isOn("cegqi-engine-debug")) + { + conj->debugPrint("cegqi-engine-debug"); + Trace("cegqi-engine-debug") << std::endl; + } + + if (!conj->needsRefinement()) + { + Trace("cegqi-engine-debug") << "Do conjecture check..." << std::endl; + if (conj->isSingleInvocation()) + { + std::vector clems; + conj->doSingleInvCheck(clems); + if (!clems.empty()) + { + d_last_inst_si = true; + 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; + } + + Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl; + std::vector cclems; + conj->doCheck(cclems); + bool addedLemma = false; + for (const Node& lem : cclems) + { + d_last_inst_si = false; + Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem + << std::endl; + if (d_quantEngine->addLemma(lem)) + { + ++(d_statistics.d_cegqi_lemmas_ce); + addedLemma = true; + } + else + { + // this may happen if we eagerly unfold, simplify to true + Trace("cegqi-engine-debug") + << " ...FAILED to add candidate!" << std::endl; + } + } + if (addedLemma) + { + Trace("cegqi-engine") << " ...check for counterexample." << std::endl; + } + else + { + if (conj->needsRefinement()) + { + // immediately go to refine candidate + checkConjecture(conj); + return; + } + } + } + else + { + Trace("cegqi-engine") << " *** Refine candidate phase..." << std::endl; + std::vector rlems; + conj->doRefine(rlems); + bool addedLemma = false; + for (unsigned i = 0; i < rlems.size(); i++) + { + Node lem = rlems[i]; + Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem + << std::endl; + bool res = d_quantEngine->addLemma(lem); + if (res) + { + ++(d_statistics.d_cegqi_lemmas_refine); + conj->incrementRefineCount(); + addedLemma = true; + } + else + { + Trace("cegqi-warn") << " ...FAILED to add refinement!" << std::endl; + } + } + if (addedLemma) + { + Trace("cegqi-engine") << " ...refine candidate." << std::endl; + } + } +} + +void SynthEngine::printSynthSolution(std::ostream& out) +{ + if (d_conj->isAssigned()) + { + d_conj->printSynthSolution(out, d_last_inst_si); + } + else + { + Assert(false); + } +} + +void SynthEngine::getSynthSolutions(std::map& sol_map) +{ + if (d_conj->isAssigned()) + { + d_conj->getSynthSolutions(sol_map, d_last_inst_si); + } +} + +void SynthEngine::preregisterAssertion(Node n) +{ + // check if it sygus conjecture + if (QuantAttributes::checkSygusConjecture(n)) + { + // this is a sygus conjecture + Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl; + d_conj->preregisterConjecture(n); + } +} + +SynthEngine::Statistics::Statistics() + : d_cegqi_lemmas_ce("SynthEngine::cegqi_lemmas_ce", 0), + d_cegqi_lemmas_refine("SynthEngine::cegqi_lemmas_refine", 0), + d_cegqi_si_lemmas("SynthEngine::cegqi_lemmas_si", 0), + d_solutions("SynthConjecture::solutions", 0), + d_candidate_rewrites_print("SynthConjecture::candidate_rewrites_print", + 0), + d_candidate_rewrites("SynthConjecture::candidate_rewrites", 0) + +{ + smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce); + smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine); + smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas); + smtStatisticsRegistry()->registerStat(&d_solutions); + smtStatisticsRegistry()->registerStat(&d_candidate_rewrites_print); + smtStatisticsRegistry()->registerStat(&d_candidate_rewrites); +} + +SynthEngine::Statistics::~Statistics() +{ + smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_ce); + smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine); + smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_solutions); + smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites_print); + smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites); +} + +} // namespace quantifiers +} // namespace theory +} /* namespace CVC4 */ diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h new file mode 100644 index 000000000..a7004c5c7 --- /dev/null +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -0,0 +1,104 @@ +/********************* */ +/*! \file synth_engine.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Mathias Preiner, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 The quantifiers module for managing all approaches to synthesis, + ** in particular, those described in Reynolds et al CAV 2015. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H +#define __CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H + +#include "context/cdhashmap.h" +#include "theory/quantifiers/sygus/synth_conjecture.h" +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class SynthEngine : public QuantifiersModule +{ + typedef context::CDHashMap NodeBoolMap; + + private: + /** the quantified formula stating the synthesis conjecture */ + SynthConjecture* d_conj; + /** last instantiation by single invocation module? */ + bool d_last_inst_si; + /** the conjecture we are waiting to assign */ + Node d_waiting_conj; + + private: + /** assign quantified formula q as the conjecture + * + * This method returns true if q was successfully assigned as the synthesis + * conjecture considered by this class. This method may return false, for + * instance, if this class determines that it would rather rewrite q to + * an equivalent form r (in which case this method returns the lemma + * q <=> r). An example of this is the quantifier elimination step + * option::sygusQePreproc(). + */ + bool assignConjecture(Node q); + /** check conjecture */ + void checkConjecture(SynthConjecture* conj); + + public: + SynthEngine(QuantifiersEngine* qe, context::Context* c); + ~SynthEngine(); + + public: + bool needsCheck(Theory::Effort e) override; + QEffort needsModel(Theory::Effort e) override; + /* Call during quantifier engine's check */ + void check(Theory::Effort e, QEffort quant_e) override; + /* Called for new quantifiers */ + void registerQuantifier(Node q) override; + /** Identify this module (for debugging, dynamic configuration, etc..) */ + std::string identify() const override { return "SynthEngine"; } + /** print solution for synthesis conjectures */ + void printSynthSolution(std::ostream& out); + /** get synth solutions + * + * This function adds entries to sol_map that map functions-to-synthesize + * with their solutions, for all active conjectures (currently just the one + * assigned to d_conj). This should be called immediately after the solver + * answers unsat for sygus input. + * + * For details on what is added to sol_map, see + * SynthConjecture::getSynthSolutions. + */ + void getSynthSolutions(std::map& sol_map); + /** preregister assertion (before rewrite) */ + void preregisterAssertion(Node n); + + public: + class Statistics + { + public: + IntStat d_cegqi_lemmas_ce; + IntStat d_cegqi_lemmas_refine; + IntStat d_cegqi_si_lemmas; + IntStat d_solutions; + IntStat d_candidate_rewrites_print; + IntStat d_candidate_rewrites; + Statistics(); + ~Statistics(); + }; /* class SynthEngine::Statistics */ + Statistics d_statistics; +}; /* class SynthEngine */ + +} // namespace quantifiers +} // namespace theory +} /* namespace CVC4 */ + +#endif diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 64adea6c5..1f4e34c1f 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -423,7 +423,7 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { void TermDbSygus::registerEnumerator(Node e, Node f, - CegConjecture* conj, + SynthConjecture* conj, bool mkActiveGuard, bool useSymbolicCons) { @@ -522,9 +522,9 @@ bool TermDbSygus::isEnumerator(Node e) const return d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end(); } -CegConjecture* TermDbSygus::getConjectureForEnumerator(Node e) const +SynthConjecture* TermDbSygus::getConjectureForEnumerator(Node e) const { - std::map::const_iterator itm = + std::map::const_iterator itm = d_enum_to_conjecture.find(e); if (itm != d_enum_to_conjecture.end()) { return itm->second; @@ -563,9 +563,11 @@ bool TermDbSygus::usingSymbolicConsForEnumerator(Node e) const void TermDbSygus::getEnumerators(std::vector& mts) { - for (std::map::iterator itm = + for (std::map::iterator itm = d_enum_to_conjecture.begin(); - itm != d_enum_to_conjecture.end(); ++itm) { + itm != d_enum_to_conjecture.end(); + ++itm) + { mts.push_back( itm->first ); } } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index fee556cf8..b7bdba3ab 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -29,7 +29,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -class CegConjecture; +class SynthConjecture; // TODO :issue #1235 split and document this class class TermDbSygus { @@ -76,13 +76,13 @@ class TermDbSygus { */ void registerEnumerator(Node e, Node f, - CegConjecture* conj, + SynthConjecture* conj, bool mkActiveGuard = false, bool useSymbolicCons = false); /** is e an enumerator registered with this class? */ bool isEnumerator(Node e) const; /** return the conjecture e is associated with */ - CegConjecture* getConjectureForEnumerator(Node e) const; + SynthConjecture* getConjectureForEnumerator(Node e) const; /** return the function-to-synthesize e is associated with */ Node getSynthFunForEnumerator(Node e) const; /** get active guard for e */ @@ -252,7 +252,7 @@ class TermDbSygus { //------------------------------enumerators /** mapping from enumerator terms to the conjecture they are associated with */ - std::map d_enum_to_conjecture; + std::map d_enum_to_conjecture; /** mapping from enumerator terms to the function-to-synthesize they are * associated with */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 7a5652e2f..320f50afb 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -47,8 +47,8 @@ #include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/rewrite_engine.h" #include "theory/quantifiers/skolemize.h" -#include "theory/quantifiers/sygus/ce_guided_instantiation.h" #include "theory/quantifiers/sygus/sygus_eval_unfold.h" +#include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_canonize.h" #include "theory/quantifiers/term_database.h" @@ -96,7 +96,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_qcf(nullptr), d_rr_engine(nullptr), d_sg_gen(nullptr), - d_ceg_inst(nullptr), + d_synth_e(nullptr), d_lte_part_inst(nullptr), d_fs(nullptr), d_i_cbqi(nullptr), @@ -192,8 +192,8 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, } } if( options::ceGuidedInst() ){ - d_ceg_inst.reset(new quantifiers::CegInstantiation(this, c)); - d_modules.push_back(d_ceg_inst.get()); + d_synth_e.reset(new quantifiers::SynthEngine(this, c)); + d_modules.push_back(d_synth_e.get()); //needsBuilder = true; } //finite model finding @@ -374,9 +374,9 @@ quantifiers::RewriteEngine* QuantifiersEngine::getRewriteEngine() const { return d_rr_engine.get(); } -quantifiers::CegInstantiation* QuantifiersEngine::getCegInstantiation() const +quantifiers::SynthEngine* QuantifiersEngine::getSynthEngine() const { - return d_ceg_inst.get(); + return d_synth_e.get(); } quantifiers::InstStrategyEnum* QuantifiersEngine::getInstStrategyEnum() const { @@ -1148,8 +1148,9 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) { } void QuantifiersEngine::printSynthSolution( std::ostream& out ) { - if( d_ceg_inst ){ - d_ceg_inst->printSynthSolution( out ); + if (d_synth_e) + { + d_synth_e->printSynthSolution(out); }else{ out << "Internal error : module for synth solution not found." << std::endl; } @@ -1260,7 +1261,7 @@ Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){ void QuantifiersEngine::getSynthSolutions(std::map& sol_map) { - d_ceg_inst->getSynthSolutions(sol_map); + d_synth_e->getSynthSolutions(sol_map); } void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 77713744b..512f0c651 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -68,7 +68,7 @@ namespace quantifiers { class RewriteEngine; class QModelBuilder; class ConjectureGenerator; - class CegInstantiation; + class SynthEngine; class LtePartialInst; class AlphaEquivalence; class InstStrategyEnum; @@ -150,7 +150,7 @@ public: /** rewrite rules utility */ quantifiers::RewriteEngine* getRewriteEngine() const; /** ceg instantiation */ - quantifiers::CegInstantiation* getCegInstantiation() const; + quantifiers::SynthEngine* getSynthEngine() const; /** get full saturation */ quantifiers::InstStrategyEnum* getInstStrategyEnum() const; /** get inst strategy cbqi */ @@ -375,7 +375,7 @@ public: /** subgoal generator */ std::unique_ptr d_sg_gen; /** ceg instantiation */ - std::unique_ptr d_ceg_inst; + std::unique_ptr d_synth_e; /** lte partial instantiation */ std::unique_ptr d_lte_part_inst; /** full saturation */