d_treg(tr),
d_stats(s),
d_tds(tr.getTermDatabaseSygus()),
- d_verify(options(), qs.getLogicInfo(), d_tds),
+ d_verify(options(), logicInfo(), d_tds),
d_hasSolution(false),
d_ceg_si(new CegSingleInv(env, tr, s)),
d_templInfer(new SygusTemplateInfer),
d_ceg_cegisUnif(new CegisUnif(env, qs, qim, d_tds, this)),
d_sygus_ccore(new CegisCoreConnective(env, qs, qim, d_tds, this)),
d_master(nullptr),
- d_set_ce_sk_vars(false),
+ d_setInnerSksModel(false),
d_repair_index(0),
d_guarded_stream_exc(false)
{
// initialize the guard
d_feasible_guard = sm->mkDummySkolem("G", nm->booleanType());
- d_feasible_guard = Rewriter::rewrite(d_feasible_guard);
+ d_feasible_guard = rewrite(d_feasible_guard);
d_feasible_guard = d_qstate.getValuation().ensureLiteral(d_feasible_guard);
AlwaysAssert(!d_feasible_guard.isNull());
Trace("cegqi") << "Base quantified formula is : " << d_embed_quant
<< std::endl;
// construct base instantiation
- d_base_inst = Rewriter::rewrite(d_qim.getInstantiate()->getInstantiation(
- d_embed_quant, vars, d_candidates));
+ Subs bsubs;
+ bsubs.add(vars, d_candidates);
+ d_base_inst = rewrite(bsubs.apply(d_embed_quant[1]));
+ d_checkBody = d_embed_quant[1];
+ if (d_checkBody.getKind() == NOT && d_checkBody[0].getKind() == FORALL)
+ {
+ for (const Node& v : d_checkBody[0][0])
+ {
+ Node sk = sm->mkDummySkolem("rsk", v.getType());
+ bsubs.add(v, sk);
+ d_innerVars.push_back(v);
+ d_innerSks.push_back(sk);
+ }
+ d_checkBody = d_checkBody[0][1].negate();
+ }
+ d_checkBody = rewrite(bsubs.apply(d_checkBody));
if (!d_embedSideCondition.isNull() && !vars.empty())
{
d_embedSideCondition = d_embedSideCondition.substitute(
}
Assert(d_qreg.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);
- }
- }
// register the strategy
d_feasible_strategy.reset(new DecisionStrategySingleton(
return true;
}
-bool SynthConjecture::needsRefinement() const { return d_set_ce_sk_vars; }
+bool SynthConjecture::needsRefinement() const { return d_setInnerSksModel; }
bool SynthConjecture::doCheck()
{
if (isSingleInvocation())
if (Trace.isOn("sygus-engine-rr"))
{
Node bv = d_tds->sygusToBuiltin(nv, tn);
- bv = Rewriter::rewrite(bv);
+ bv = rewrite(bv);
Trace("sygus-engine-rr") << " -> " << bv << std::endl;
}
}
}
}
- NodeManager* nm = NodeManager::currentNM();
- SkolemManager* sm = nm->getSkolemManager();
-
// check the side condition if we constructed a candidate
if (constructed_cand)
{
}
// must get a counterexample to the value of the current candidate
- Node inst;
+ Node query;
if (constructed_cand)
{
if (Trace.isOn("cegqi-check"))
}
}
Assert(candidate_values.size() == d_candidates.size());
- inst = d_base_inst.substitute(d_candidates.begin(),
- d_candidates.end(),
- candidate_values.begin(),
- candidate_values.end());
+ query = d_checkBody.substitute(d_candidates.begin(),
+ d_candidates.end(),
+ candidate_values.begin(),
+ candidate_values.end());
}
else
{
- inst = d_base_inst;
+ query = d_checkBody;
}
if (!constructed_cand)
recordSolution(candidate_values);
return true;
}
- Assert(!d_set_ce_sk_vars);
+ Assert(!d_setInnerSksModel);
- // immediately skolemize inner existentials
- Node query;
- // introduce the skolem variables
- std::vector<Node> sks;
- std::vector<Node> vars;
- if (constructed_cand)
+ // print the candidate solution for debugging
+ if (constructed_cand && printDebug)
{
- if (printDebug)
- {
- const Options& sopts = options();
- std::ostream& out = *sopts.base.out;
- out << "(sygus-candidate ";
- Assert(d_quant[0].getNumChildren() == candidate_values.size());
- for (unsigned i = 0, ncands = candidate_values.size(); i < ncands; i++)
- {
- Node v = candidate_values[i];
- std::stringstream ss;
- TermDbSygus::toStreamSygus(ss, v);
- out << "(" << d_quant[0][i] << " " << ss.str() << ")";
- }
- out << ")" << std::endl;
- }
- if (inst.getKind() == NOT && inst[0].getKind() == FORALL)
+ const Options& sopts = options();
+ std::ostream& out = *sopts.base.out;
+ out << "(sygus-candidate ";
+ Assert(d_quant[0].getNumChildren() == candidate_values.size());
+ for (size_t i = 0, ncands = candidate_values.size(); i < ncands; i++)
{
- for (const Node& v : inst[0][0])
- {
- Node sk = sm->mkDummySkolem("rsk", v.getType());
- sks.push_back(sk);
- vars.push_back(v);
- Trace("cegqi-check-debug")
- << " introduce skolem " << sk << " for " << v << "\n";
- }
- query = inst[0][1].substitute(
- vars.begin(), vars.end(), sks.begin(), sks.end());
- query = query.negate();
- }
- else
- {
- // use the instance itself
- query = inst;
+ Node v = candidate_values[i];
+ std::stringstream ss;
+ TermDbSygus::toStreamSygus(ss, v);
+ out << "(" << d_quant[0][i] << " " << ss.str() << ")";
}
+ out << ")" << std::endl;
}
- d_ce_sk_vars.insert(d_ce_sk_vars.end(), sks.begin(), sks.end());
- d_set_ce_sk_vars = true;
+
+ d_setInnerSksModel = true;
if (query.isNull())
{
// here since the result of the satisfiability test may be unknown.
recordSolution(candidate_values);
- Result r = d_verify.verify(query, d_ce_sk_vars, d_ce_sk_var_mvs);
+ Result r = d_verify.verify(query, d_innerSks, d_innerSksModel);
if (r.asSatisfiabilityResult().isSat() == Result::SAT)
{
bool SynthConjecture::doRefine()
{
- 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;
- for (const Node& v : d_ce_sk_vars)
- {
- Node mv = getModelValue(v);
- Trace("cegqi-refine") << " " << v << " -> " << mv << std::endl;
- model_values.push_back(mv);
- }
- 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());
- }
-
+ Assert(d_setInnerSksModel);
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();
- }
+ << " For counterexample skolems : " << d_innerSks << std::endl;
+ Node base_lem = d_checkBody.negate();
- Assert(sk_vars.size() == sk_subs.size());
+ Assert(d_innerSks.size() == d_innerSksModel.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());
+ base_lem = base_lem.substitute(d_innerSks.begin(),
+ d_innerSks.end(),
+ d_innerSksModel.begin(),
+ d_innerSksModel.end());
Trace("cegqi-refine") << "doRefine : rewrite..." << std::endl;
base_lem = d_tds->rewriteNode(base_lem);
Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem
<< "..." << std::endl;
size_t prevPending = d_qim.numPendingLemmas();
- d_master->registerRefinementLemma(sk_vars, base_lem);
+ d_master->registerRefinementLemma(d_innerSks, base_lem);
Trace("cegqi-refine") << "doRefine : finished" << std::endl;
- d_set_ce_sk_vars = false;
- d_ce_sk_vars.clear();
- d_ce_sk_var_mvs.clear();
+ d_setInnerSksModel = false;
+ d_innerSksModel.clear();
// check if we added a lemma
bool addedLemma = d_qim.numPendingLemmas() > prevPending;
{
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;
+ Trace(c) << " * Counterexample skolems : " << d_innerSks << std::endl;
}
void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums,
<< values << std::endl;
// 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();
+ d_setInnerSksModel = false;
+ d_innerSksModel.clear();
// However, we need to exclude the current solution using an explicit
// blocking clause, so that we proceed to the next solution. We do this only
// for passively-generated enumerators (TermDbSygus::isPassiveEnumerator).
TNode tsol = sol;
sol = templ.substitute(templa, tsol);
Trace("cegqi-inv-debug") << "With template : " << sol << std::endl;
- sol = Rewriter::rewrite(sol);
+ sol = rewrite(sol);
Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl;
// now, reconstruct to the syntax
sol = d_ceg_si->reconstructToSyntax(sol, tn, status, true);
projects / cvc5.git / commitdiff