#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"
// constants here.
if (options::sygusRepairConst() && !d_master->usingRepairConst())
{
- Trace("cegqi-check") << "CegConjuncture : repair previous solution..."
- << std::endl;
// 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();
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))
}
//immediately skolemize inner existentials
- d_set_ce_sk_vars = sk_refine;
Node lem;
- if (inst.getKind() == NOT && inst[0].getKind() == FORALL)
+ // introduce the skolem variables
+ std::vector<Node> sks;
+ if (constructed_cand)
{
- // 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();
}
- if (sk_refine)
- {
- d_ce_sk_vars.insert(d_ce_sk_vars.end(), sks.begin(), sks.end());
- }
- Assert(!isGround());
- }
- else
- {
- if (constructed_cand)
+ else
{
// use the instance itself
lem = inst;
}
- // we add null so that one test of the conjecture for the empty
- // substitution is checked
}
+ 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())
{
lem = Rewriter::rewrite( lem );
// record the instantiation
// this is used for remembering the solution
recordInstantiation(candidate_values);
- if (lem.isConst() && !lem.getConst<bool>() && options::sygusStream())
+ Node query = lem;
+ if (query.isConst() && !query.getConst<bool>() && options::sygusStream())
{
// short circuit the check
// instead, we immediately print the current solution.
// this saves us from introducing a check lemma and a new guard.
printAndContinueStream();
+ return;
}
- 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())
{
- // This is the "verification lemma", which states
- // either this conjecture does not have a solution, or candidate_values
- // is a solution for this conjecture.
- lem = nm->mkNode(OR, d_quant.negate(), lem);
- lem = getStreamGuardedLemma(lem);
- lems.push_back(lem);
+ Trace("cegqi-engine") << " *** Direct verify..." << 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;
+ 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();
+ }
+ // 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.
}
+ lem = getStreamGuardedLemma(lem);
+ lems.push_back(lem);
}
}
{
Trace("cegqi-refine") << "Get model values for skolems..." << std::endl;
Assert(d_inner_vars.size() == d_ce_sk_vars.size());
- std::vector<Node> model_values;
- getModelValues(d_ce_sk_vars, model_values);
+ 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());
- sk_subs.insert(sk_subs.end(), model_values.begin(), model_values.end());
}
else
{
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 ) {
// 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;
Assert( d_quant[0].getNumChildren()==d_embed_quant[0].getNumChildren() );
std::vector<Node> sols;
std::vector<int> statuses;
- getSynthSolutionsInternal(sols, statuses, singleInvocation);
+ if (!getSynthSolutionsInternal(sols, statuses, singleInvocation))
+ {
+ return;
+ }
for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
{
Node sol = sols[i];
TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus();
std::vector<Node> sols;
std::vector<int> statuses;
- getSynthSolutionsInternal(sols, statuses, singleInvocation);
+ if (!getSynthSolutionsInternal(sols, statuses, singleInvocation))
+ {
+ return;
+ }
for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
{
Node sol = sols[i];
}
}
-void CegConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
+bool CegConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
std::vector<int>& statuses,
bool singleInvocation)
{
{
Assert(d_ceg_si != NULL);
sol = d_ceg_si->getSolution(i, tn, status, true);
- if (!sol.isNull())
+ if (sol.isNull())
{
- sol = sol.getKind() == LAMBDA ? sol[1] : sol;
+ return false;
}
+ sol = sol.getKind() == LAMBDA ? sol[1] : sol;
}
else
{
sols.push_back(sol);
statuses.push_back(status);
}
+ return true;
}
Node CegConjecture::getSymmetryBreakingPredicate(
projects / cvc5.git / commitdiff