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 \
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 \
#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"
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]);
}
}
#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"
// static conjecture-dependent symmetry breaking
Trace("sygus-sb-debug")
<< " conjecture-dependent symmetry breaking...\n";
- std::map<Node, quantifiers::CegConjecture*>::iterator itc =
+ std::map<Node, quantifiers::SynthConjecture*>::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())
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;
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())
{
#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"
/**
* Map from anchors to the conjecture they are associated with.
*/
- std::map<Node, quantifiers::CegConjecture*> d_anchor_to_conj;
+ std::map<Node, quantifiers::SynthConjecture*> d_anchor_to_conj;
/**
* Map from terms (selector chains) to their depth. The depth of a selector
* chain S1( ... Sn( x ) ... ) is:
* (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.
#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;
#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"
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);
}
}
+++ /dev/null
-/********************* */
-/*! \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; 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") << "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; 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< 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; 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 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<Node>& 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<Node> terms;
- d_master->getTermList(d_candidates, terms);
-
- Assert(!d_candidates.empty());
-
- Trace("cegqi-check") << "CegConjuncture : check, build candidates..."
- << std::endl;
- std::vector<Node> 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<Node> 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<Node> 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<Node> sks;
- if (constructed_cand)
- {
- if (inst.getKind() == NOT && inst[0].getKind() == FORALL)
- {
- std::vector<Node> 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<Node, Node> 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<bool>())
- {
- // 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<bool>());
-#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<Node> 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<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 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<Node> terms;
- d_master->getTermList(d_candidates, terms);
- std::vector<Node> exp;
- for (const Node& cprog : terms)
- {
- Node sol = cprog;
- if (!d_cinfo[cprog].d_inst.empty())
- {
- sol = d_cinfo[cprog].d_inst.back();
- // add to explanation of exclusion
- d_qe->getTermDatabaseSygus()->getExplain()->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<Node> sols;
- std::vector<int> 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<DatatypeType>(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<Node, ExpressionMinerManager>::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<Node, Node>& sol_map,
- bool singleInvocation)
-{
- NodeManager* nm = NodeManager::currentNM();
- TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus();
- std::vector<Node> sols;
- std::vector<int> 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<DatatypeType>(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<Node>& sols,
- std::vector<int>& 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<Node> 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 */
+++ /dev/null
-/********************* */
-/*! \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 <memory>
-
-#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<Node>& 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<Node, Node>& 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<DecisionStrategy> d_feasible_strategy;
- /** single invocation utility */
- std::unique_ptr<CegConjectureSingleInv> d_ceg_si;
- /** utility for static preprocessing and analysis of conjectures */
- std::unique_ptr<CegConjectureProcess> d_ceg_proc;
- /** grammar utility */
- std::unique_ptr<CegGrammarConstructor> d_ceg_gc;
- /** repair constant utility */
- std::unique_ptr<SygusRepairConst> d_sygus_rconst;
-
- //------------------------modules
- /** program by examples module */
- std::unique_ptr<CegConjecturePbe> d_ceg_pbe;
- /** CEGIS module */
- std::unique_ptr<Cegis> d_ceg_cegis;
- /** CEGIS UNIF module */
- std::unique_ptr<CegisUnif> d_ceg_cegisUnif;
- /** the set of active modules (subset of the above list) */
- std::vector<SygusModule*> d_modules;
- /** master module
- *
- * This is the module (one of those above) that takes sole responsibility
- * for this conjecture, determined during assign(...).
- */
- SygusModule* d_master;
- //------------------------end modules
-
- /** list of constants for quantified formula
- * The outer Skolems for the negation of d_embed_quant.
- */
- 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<Node> 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<Node> 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<Node, CandidateInfo> 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; 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<Node>& sols,
- std::vector<int>& 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<SygusStreamDecisionStrategy> 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<Node, ExpressionMinerManager> d_exprm;
-};
-
-} /* namespace CVC4::theory::quantifiers */
-} /* namespace CVC4::theory */
-} /* namespace CVC4 */
-
-#endif
+++ /dev/null
-/********************* */
-/*! \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<Node> 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<Node> all_vars;
- sip.getAllVariables(all_vars);
- std::vector<Node> si_vars;
- sip.getSingleInvocationVariables(si_vars);
- std::vector<Node> qe_vars;
- std::vector<Node> 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<Node> orig;
- std::vector<Node> 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<Node> 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<Node> 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<Node> 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; 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 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<Node, Node>& 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 */
+++ /dev/null
-/********************* */
-/*! \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<Node, bool, NodeHashFunction> 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<Node, Node>& 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
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),
}
}
-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<Node>& lems)
+void CegSingleInv::getInitialSingleInvLemma(Node g, std::vector<Node>& lems)
{
Assert(!g.isNull());
Assert(!d_single_inv.isNull());
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
}
}
-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
}
}
-bool CegConjectureSingleInv::doAddInstantiation( std::vector< Node >& subs ){
+bool CegSingleInv::doAddInstantiation(std::vector<Node>& 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") ){
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<Node>& 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
}
}
-Node CegConjectureSingleInv::constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index, std::map< Node, Node >& weak_imp ) {
+Node CegSingleInv::constructSolution(std::vector<unsigned>& indices,
+ unsigned i,
+ unsigned index,
+ std::map<Node, Node>& weak_imp)
+{
Assert( index<d_inst.size() );
Assert( i<d_inst[index].size() );
unsigned uindex = indices[index];
//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() ){
}
};
-
-Node CegConjectureSingleInv::postProcessSolution( Node n ){
+Node CegSingleInv::postProcessSolution(Node n)
+{
bool childChanged = false;
Kind k = n.getKind();
if( n.getKind()==INTS_DIVISION_TOTAL ){
}
}
-
-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();
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();
}
}
-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() ){
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<Node>& 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<Node>& subs) override;
+ bool isEligibleForInstantiation(Node n) override;
+ bool addLemma(Node lem) override;
};
class DetTrace {
// (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
unsigned index, std::map<Node, Node>& 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
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; }
#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"
return com.isConst() && com.getConst<bool>();
}
-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{
}
-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;
}
}
-
-Node CegConjectureSingleInvSol::pullITEs( Node s ) {
+Node CegSingleInvSol::pullITEs(Node s)
+{
if( s.getKind()==ITE ){
bool success;
do {
}
// 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<Node>& conj,
+ Node& t,
+ Node& rem,
+ int depth)
+{
Assert( n_ite.getKind()==ITE );
std::vector< Node > curr_conj;
std::vector< Node > orig_conj;
}
}
-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;
// 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<Node, bool>& assign,
+ std::vector<Node>& new_assign,
+ std::vector<Node>& vars,
+ std::vector<Node>& new_vars,
+ std::vector<Node>& 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;
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<Node>& vars,
+ std::vector<Node>& new_vars,
+ std::vector<Node>& new_subs)
+{
Assert( eq.getKind()==EQUAL );
//try to find valid argument
for( unsigned r=0; r<2; r++ ){
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;
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<Node, bool>& assign,
+ std::vector<Node>& vars,
+ std::vector<Node>& subs,
+ int status)
+{
Assert( vars.size()==subs.size() );
std::map< Node, bool >::iterator ita = assign.find( sol );
if( ita!=assign.end() ){
}
}
-
-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 ){
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;
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;
}
}
-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<Node>& ts,
+ const DatatypeConstructor& dtc,
+ std::vector<int>& ids,
+ int& status)
+{
Assert( dtc.getNumArgs()==ts.size() );
for( unsigned i=0; i<ts.size(); i++ ){
TypeNode cstn = d_qe->getTermDatabaseSygus()->getArgType( dtc, i );
}
*/
-
-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;
}
}
-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;
}
}
-bool CegConjectureSingleInvSol::getPathToRoot( int id ) {
+bool CegSingleInvSol::getPathToRoot(int id)
+{
if( id==d_root_id ){
return true;
}else{
}
}
-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<d_eqc[rid].size(); i++ ){
}
}
-void CegConjectureSingleInvSol::getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv ) {
+void CegSingleInvSol::getEquivalentTerms(Kind k,
+ Node n,
+ std::vector<Node>& 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 ) ) );
}
}
-void CegConjectureSingleInvSol::registerEquivalentTerms( Node n ) {
+void CegSingleInvSol::registerEquivalentTerms(Node n)
+{
for( unsigned i=0; i<n.getNumChildren(); i++ ){
registerEquivalentTerms( n[i] );
}
}
}
-Node CegConjectureSingleInvSol::builtinToSygusConst(Node c,
- TypeNode tn,
- int rcons_depth)
+Node CegSingleInvSol::builtinToSygusConst(Node c, TypeNode tn, int rcons_depth)
{
std::map<Node, Node>::iterator it = d_builtin_const_to_sygus[tn].find(c);
if (it != d_builtin_const_to_sygus[tn].end())
}
};
-void CegConjectureSingleInvSol::registerType(TypeNode tn)
+void CegSingleInvSol::registerType(TypeNode tn)
{
if (d_const_list_pos.find(tn) != d_const_list_pos.end())
{
}
}
-bool CegConjectureSingleInvSol::getMatch(Node p,
- Node n,
- std::map<int, Node>& s,
- std::vector<int>& new_s)
+bool CegSingleInvSol::getMatch(Node p,
+ Node n,
+ std::map<int, Node>& s,
+ std::vector<int>& new_s)
{
TermDbSygus* tds = d_qe->getTermDatabaseSygus();
if (tds->isFreeVar(p))
return false;
}
-bool CegConjectureSingleInvSol::getMatch(Node t,
- TypeNode st,
- int& index_found,
- std::vector<Node>& args,
- int index_exc,
- int index_start)
+bool CegSingleInvSol::getMatch(Node t,
+ TypeNode st,
+ int& index_found,
+ std::vector<Node>& args,
+ int index_exc,
+ int index_start)
{
Assert(st.isDatatype());
const Datatype& dt = static_cast<DatatypeType>(st.toType()).getDatatype();
return false;
}
-Node CegConjectureSingleInvSol::getGenericBase(TypeNode tn,
- const Datatype& dt,
- int c)
+Node CegSingleInvSol::getGenericBase(TypeNode tn, const Datatype& dt, int c)
{
std::map<int, Node>::iterator it = d_generic_base[tn].find(c);
if (it != d_generic_base[tn].end())
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;
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
#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"
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())
class Cegis : public SygusModule
{
public:
- Cegis(QuantifiersEngine* qe, CegConjecture* p);
+ Cegis(QuantifiersEngine* qe, SynthConjecture* p);
~Cegis() override {}
/** initialize */
virtual bool initialize(Node n,
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<Node> d_base_vars;
/**
- * If CegConjecture::d_base_inst is exists y. P( d, y ), then this is the
- * formula P( CegConjecture::d_candidates, y ).
+ * 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
#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"
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)
{
}
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)
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
/** 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 */
class CegisUnif : public Cegis
{
public:
- CegisUnif(QuantifiersEngine* qe, CegConjecture* p);
+ CegisUnif(QuantifiersEngine* qe, SynthConjecture* p);
~CegisUnif() override;
/** Retrieves enumerators for constructing solutions
*
#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"
namespace quantifiers {
CegGrammarConstructor::CegGrammarConstructor(QuantifiersEngine* qe,
- CegConjecture* p)
+ SynthConjecture* p)
: d_qe(qe), d_parent(p), d_is_syntax_restricted(false)
{
}
{
// 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<TypeNode, std::vector<Node>> exc_cons;
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.
class CegGrammarConstructor
{
public:
- CegGrammarConstructor(QuantifiersEngine* qe, CegConjecture* p);
+ CegGrammarConstructor(QuantifiersEngine* qe, SynthConjecture* p);
~CegGrammarConstructor() {}
/** process
*
/** 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 */
#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"
#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;
}
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;
namespace quantifiers {
class TermDbSygus;
-class CegConjecture;
+class SynthConjecture;
/* 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 */
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 */
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)
{
}
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.
*
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.
/** 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 */
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);
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<Node, bool>& visited,
+ bool hasPol,
+ bool pol)
+{
if( visited.find( n )==visited.end() ){
visited[n] = true;
Node neval;
}
}
-bool CegConjecturePbe::initialize(Node n,
- const std::vector<Node>& candidates,
- std::vector<Node>& lemmas)
+bool SygusPbe::initialize(Node n,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& lemmas)
{
Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
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()) {
}
}
-Node CegConjecturePbe::PbeTrie::addPbeExampleEval(TypeNode etn, Node e, Node b,
- std::vector<Node>& ex,
- CegConjecturePbe* cpbe,
- unsigned index,
- unsigned ntotal) {
+Node SygusPbe::PbeTrie::addPbeExampleEval(TypeNode etn,
+ Node e,
+ Node b,
+ std::vector<Node>& 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());
return false;
}
-unsigned CegConjecturePbe::getNumExamples(Node e) {
+unsigned SygusPbe::getNumExamples(Node e)
+{
e = d_tds->getSynthFunForEnumerator(e);
Assert(!e.isNull());
std::map<Node, std::vector<std::vector<Node> > >::iterator it =
}
}
-void CegConjecturePbe::getExample(Node e, unsigned i, std::vector<Node>& ex) {
+void SygusPbe::getExample(Node e, unsigned i, std::vector<Node>& ex)
+{
e = d_tds->getSynthFunForEnumerator(e);
Assert(!e.isNull());
std::map<Node, std::vector<std::vector<Node> > >::iterator it =
}
}
-Node CegConjecturePbe::getExampleOut(Node e, unsigned i) {
+Node SygusPbe::getExampleOut(Node e, unsigned i)
+{
e = d_tds->getSynthFunForEnumerator(e);
Assert(!e.isNull());
std::map<Node, std::vector<Node> >::iterator it = d_examples_out.find(e);
}
}
-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);
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<Node, bool>::iterator itx = d_examples_invalid.find(e);
// ------------------------------------------- solution construction from enumeration
-void CegConjecturePbe::getTermList(const std::vector<Node>& candidates,
- std::vector<Node>& terms)
+void SygusPbe::getTermList(const std::vector<Node>& candidates,
+ std::vector<Node>& terms)
{
Valuation& valuation = d_qe->getValuation();
for( unsigned i=0; i<candidates.size(); i++ ){
}
}
-bool CegConjecturePbe::constructCandidates(const std::vector<Node>& enums,
- const std::vector<Node>& enum_values,
- const std::vector<Node>& candidates,
- std::vector<Node>& candidate_values,
- std::vector<Node>& lems)
+bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
+ const std::vector<Node>& enum_values,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& candidate_values,
+ std::vector<Node>& lems)
{
Assert( enums.size()==enum_values.size() );
if( !enums.empty() ){
#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"
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
*
Node addPbeExample(TypeNode etn,
Node e,
Node b,
- CegConjecturePbe* cpbe,
+ SygusPbe* cpbe,
unsigned index,
unsigned ntotal);
Node e,
Node b,
std::vector<Node>& ex,
- CegConjecturePbe* cpbe,
+ SygusPbe* cpbe,
unsigned index,
unsigned ntotal);
};
namespace theory {
namespace quantifiers {
-void CegConjectureProcessFun::init(Node f)
+void SynthConjectureProcessFun::init(Node f)
{
d_synth_fun = f;
Assert(f.getType().isFunction());
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<unsigned, Node>& n_arg_map)
{
std::vector<Node> vars;
return cn_subs == n;
}
-bool CegConjectureProcessFun::isArgVar(Node n, unsigned& arg_index)
+bool SynthConjectureProcessFun::isArgVar(Node n, unsigned& arg_index)
{
if (n.isVar())
{
return false;
}
-Node CegConjectureProcessFun::inferDefinition(
+Node SynthConjectureProcessFun::inferDefinition(
Node n,
std::unordered_map<Node, unsigned, NodeHashFunction>& term_to_arg_carry,
std::unordered_map<Node,
return visited[n];
}
-unsigned CegConjectureProcessFun::assignRelevantDef(Node def,
- std::vector<unsigned>& args)
+unsigned SynthConjectureProcessFun::assignRelevantDef(
+ Node def, std::vector<unsigned>& args)
{
unsigned id = 0;
if (def.isNull())
return rid;
}
-void CegConjectureProcessFun::processTerms(
+void SynthConjectureProcessFun::processTerms(
std::vector<Node>& ns,
std::vector<Node>& ks,
Node nf,
}
}
-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<unsigned>& args)
{
for (unsigned i = 0; i < d_arg_vars.size(); i++)
}
}
-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);
getComponentVector(AND, base, conjuncts);
// process the conjunctions
- for (std::map<Node, CegConjectureProcessFun>::iterator it =
+ for (std::map<Node, SynthConjectureProcessFun>::iterator it =
d_sf_info.begin();
it != d_sf_info.end();
++it)
return q;
}
-void CegConjectureProcess::initialize(Node n, std::vector<Node>& candidates)
+void SynthConjectureProcess::initialize(Node n, std::vector<Node>& candidates)
{
if (Trace.isOn("sygus-process"))
{
}
}
-bool CegConjectureProcess::isArgRelevant(Node f, unsigned i)
+bool SynthConjectureProcess::isArgRelevant(Node f, unsigned i)
{
if (!options::sygusArgRelevant())
{
return true;
}
- std::map<Node, CegConjectureProcessFun>::iterator its = d_sf_info.find(f);
+ std::map<Node, SynthConjectureProcessFun>::iterator its = d_sf_info.find(f);
if (its != d_sf_info.end())
{
return its->second.isArgRelevant(i);
return true;
}
-bool CegConjectureProcess::getIrrelevantArgs(Node f,
- std::unordered_set<unsigned>& args)
+bool SynthConjectureProcess::getIrrelevantArgs(
+ Node f, std::unordered_set<unsigned>& args)
{
- std::map<Node, CegConjectureProcessFun>::iterator its = d_sf_info.find(f);
+ std::map<Node, SynthConjectureProcessFun>::iterator its = d_sf_info.find(f);
if (its != d_sf_info.end())
{
its->second.getIrrelevantArgs(args);
return false;
}
-void CegConjectureProcess::processConjunct(
+void SynthConjectureProcess::processConjunct(
Node n, Node f, std::unordered_set<Node, NodeHashFunction>& synth_fv)
{
Trace("sygus-process-arg-deps") << "Process conjunct: " << std::endl;
// process the applications of synthesis functions
if (!ns.empty())
{
- std::map<Node, CegConjectureProcessFun>::iterator its = d_sf_info.find(f);
+ std::map<Node, SynthConjectureProcessFun>::iterator its = d_sf_info.find(f);
if (its != d_sf_info.end())
{
its->second.processTerms(ns, ks, nf, synth_fv_n, free_vars);
}
}
-Node CegConjectureProcess::CegConjectureProcess::flatten(
+Node SynthConjectureProcess::SynthConjectureProcess::flatten(
Node n,
Node f,
std::unordered_set<Node, NodeHashFunction>& synth_fv,
return visited[n];
}
-void CegConjectureProcess::getFreeVariables(
+void SynthConjectureProcess::getFreeVariables(
Node n,
std::unordered_set<Node, NodeHashFunction>& synth_fv,
std::unordered_map<Node,
} while (!visit.empty());
}
-Node CegConjectureProcess::getSymmetryBreakingPredicate(
+Node SynthConjectureProcess::getSymmetryBreakingPredicate(
Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth)
{
return Node::null();
}
-void CegConjectureProcess::debugPrint(const char* c) {}
-void CegConjectureProcess::getComponentVector(Kind k,
- Node n,
- std::vector<Node>& args)
+void SynthConjectureProcess::debugPrint(const char* c) {}
+void SynthConjectureProcess::getComponentVector(Kind k,
+ Node n,
+ std::vector<Node>& args)
{
if (n.getKind() == k)
{
* 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.
* 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
/** the synth fun associated with this */
Node d_synth_fun;
/** properties of each argument */
- std::vector<CegConjectureProcessArg> d_arg_props;
+ std::vector<SynthConjectureProcessArg> 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<Node> d_arg_vars;
/** map from d_arg_vars to the argument #
};
/** 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<Node>& candidates);
/** is the i^th argument of the function-to-synthesize f relevant? */
bool isArgRelevant(Node f, unsigned i);
std::unordered_set<Node, NodeHashFunction>,
NodeHashFunction>& free_vars);
/** for each synth-fun, information that is specific to this conjecture */
- std::map<Node, CegConjectureProcessFun> d_sf_info;
+ std::map<Node, SynthConjectureProcessFun> d_sf_info;
/** get component vector */
void getComponentVector(Kind k, Node n, std::vector<Node>& args);
#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 <math.h>
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,
using NodePairMap = std::unordered_map<Node, Node, NodeHashFunction>;
using NodePair = std::pair<Node, Node>;
-class CegConjecture;
+class SynthConjecture;
/** Sygus unification Refinement Lemmas utility
*
class SygusUnifRl : public SygusUnif
{
public:
- SygusUnifRl(CegConjecture* p);
+ SygusUnifRl(SynthConjecture* p);
~SygusUnifRl();
/** initialize */
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<Node, NodeHashFunction> d_unif_candidates;
/** construct sol */
--- /dev/null
+/********************* */
+/*! \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<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; 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<Node> 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<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; 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<Node>& 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<Node>& 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<Node> terms;
+ d_master->getTermList(d_candidates, terms);
+
+ Assert(!d_candidates.empty());
+
+ Trace("cegqi-check") << "CegConjuncture : check, build candidates..."
+ << std::endl;
+ std::vector<Node> 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<Node> 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<Node> 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<Node> sks;
+ if (constructed_cand)
+ {
+ if (inst.getKind() == NOT && inst[0].getKind() == FORALL)
+ {
+ std::vector<Node> 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<Node, Node> 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<bool>())
+ {
+ // 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<bool>());
+#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<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<Node> 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 SynthConjecture::preregisterConjecture(Node q)
+{
+ d_ceg_si->preregisterConjecture(q);
+}
+
+void SynthConjecture::getModelValues(std::vector<Node>& n, std::vector<Node>& 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<Node> terms;
+ d_master->getTermList(d_candidates, terms);
+ std::vector<Node> exp;
+ for (const Node& cprog : terms)
+ {
+ Node sol = cprog;
+ if (!d_cinfo[cprog].d_inst.empty())
+ {
+ sol = d_cinfo[cprog].d_inst.back();
+ // add to explanation of exclusion
+ d_qe->getTermDatabaseSygus()->getExplain()->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<Node> sols;
+ std::vector<int> 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<DatatypeType>(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<Node, ExpressionMinerManager>::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<Node, Node>& sol_map,
+ bool singleInvocation)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus();
+ std::vector<Node> sols;
+ std::vector<int> 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<DatatypeType>(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<Node>& sols,
+ std::vector<int>& 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<Node> 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 */
--- /dev/null
+/********************* */
+/*! \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 <memory>
+
+#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<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<Node>& 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<Node, Node>& 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 */
+ 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<DecisionStrategy> d_feasible_strategy;
+ /** single invocation utility */
+ std::unique_ptr<CegSingleInv> d_ceg_si;
+ /** utility for static preprocessing and analysis of conjectures */
+ std::unique_ptr<SynthConjectureProcess> d_ceg_proc;
+ /** grammar utility */
+ std::unique_ptr<CegGrammarConstructor> d_ceg_gc;
+ /** repair constant utility */
+ std::unique_ptr<SygusRepairConst> d_sygus_rconst;
+
+ //------------------------modules
+ /** program by examples module */
+ std::unique_ptr<SygusPbe> d_ceg_pbe;
+ /** CEGIS module */
+ std::unique_ptr<Cegis> d_ceg_cegis;
+ /** CEGIS UNIF module */
+ std::unique_ptr<CegisUnif> d_ceg_cegisUnif;
+ /** the set of active modules (subset of the above list) */
+ std::vector<SygusModule*> d_modules;
+ /** master module
+ *
+ * This is the module (one of those above) that takes sole responsibility
+ * for this conjecture, determined during assign(...).
+ */
+ SygusModule* d_master;
+ //------------------------end modules
+
+ /** list of constants for quantified formula
+ * The outer Skolems for the negation of d_embed_quant.
+ */
+ 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<Node> 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<Node> 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<Node, CandidateInfo> 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; 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<Node>& sols,
+ std::vector<int>& 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<SygusStreamDecisionStrategy> 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<Node, ExpressionMinerManager> d_exprm;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} /* namespace CVC4 */
+
+#endif
--- /dev/null
+/********************* */
+/*! \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<Node> 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<Node> all_vars;
+ sip.getAllVariables(all_vars);
+ std::vector<Node> si_vars;
+ sip.getSingleInvocationVariables(si_vars);
+ std::vector<Node> qe_vars;
+ std::vector<Node> 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<Node> orig;
+ std::vector<Node> 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<Node> 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<Node> 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<Node> 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; 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<Node, Node>& 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 */
--- /dev/null
+/********************* */
+/*! \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<Node, bool, NodeHashFunction> 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<Node, Node>& 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
void TermDbSygus::registerEnumerator(Node e,
Node f,
- CegConjecture* conj,
+ SynthConjecture* conj,
bool mkActiveGuard,
bool useSymbolicCons)
{
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<Node, CegConjecture*>::const_iterator itm =
+ std::map<Node, SynthConjecture*>::const_iterator itm =
d_enum_to_conjecture.find(e);
if (itm != d_enum_to_conjecture.end()) {
return itm->second;
void TermDbSygus::getEnumerators(std::vector<Node>& mts)
{
- for (std::map<Node, CegConjecture*>::iterator itm =
+ for (std::map<Node, SynthConjecture*>::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 );
}
}
namespace theory {
namespace quantifiers {
-class CegConjecture;
+class SynthConjecture;
// TODO :issue #1235 split and document this class
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 */
//------------------------------enumerators
/** mapping from enumerator terms to the conjecture they are associated with
*/
- std::map<Node, CegConjecture*> d_enum_to_conjecture;
+ std::map<Node, SynthConjecture*> d_enum_to_conjecture;
/** mapping from enumerator terms to the function-to-synthesize they are
* associated with
*/
#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"
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),
}
}
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
{
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
{
}
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;
}
void QuantifiersEngine::getSynthSolutions(std::map<Node, Node>& sol_map)
{
- d_ceg_inst->getSynthSolutions(sol_map);
+ d_synth_e->getSynthSolutions(sol_map);
}
void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
class RewriteEngine;
class QModelBuilder;
class ConjectureGenerator;
- class CegInstantiation;
+ class SynthEngine;
class LtePartialInst;
class AlphaEquivalence;
class InstStrategyEnum;
/** 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 */
/** subgoal generator */
std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen;
/** ceg instantiation */
- std::unique_ptr<quantifiers::CegInstantiation> d_ceg_inst;
+ std::unique_ptr<quantifiers::SynthEngine> d_synth_e;
/** lte partial instantiation */
std::unique_ptr<quantifiers::LtePartialInst> d_lte_part_inst;
/** full saturation */
projects / cvc5.git / commitdiff