/*! \file sygus_inst.cpp
** \verbatim
** Top contributors (to current version):
- ** Mathias Preiner, Andrew Reynolds
+ ** Mathias Preiner, Aina Niemetz, Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
** in the top-level source directory and their institutional affiliations.
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
#include "theory/quantifiers/sygus/synth_engine.h"
#include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
namespace CVC4 {
namespace theory {
} // namespace
-SygusInst::SygusInst(QuantifiersEngine* qe)
- : QuantifiersModule(qe),
- d_lemma_cache(qe->getUserContext()),
- d_ce_lemma_added(qe->getUserContext()),
- d_global_terms(qe->getUserContext()),
- d_notified_assertions(qe->getUserContext())
+SygusInst::SygusInst(QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ QuantifiersInferenceManager& qim)
+ : QuantifiersModule(qs, qim, qe),
+ d_ce_lemma_added(qs.getUserContext()),
+ d_global_terms(qs.getUserContext()),
+ d_notified_assertions(qs.getUserContext())
{
}
TermDbSygus* db = d_quantEngine->getTermDatabaseSygus();
SygusExplain syexplain(db);
NodeManager* nm = NodeManager::currentNM();
+ options::SygusInstMode mode = options::sygusInstMode();
for (const Node& q : d_active_quant)
{
- std::vector<Node> terms;
- for (const Node& var : q[0])
+ const std::vector<Node>& inst_constants = d_inst_constants.at(q);
+ const std::vector<Node>& dt_evals = d_var_eval.at(q);
+ Assert(inst_constants.size() == dt_evals.size());
+ Assert(inst_constants.size() == q[0].getNumChildren());
+
+ std::vector<Node> terms, eval_unfold_lemmas;
+ for (size_t i = 0, size = q[0].getNumChildren(); i < size; ++i)
{
- Node dt_var = d_inst_constants[var];
- Node dt_eval = d_var_eval[var];
+ Node dt_var = inst_constants[i];
+ Node dt_eval = dt_evals[i];
Node value = model->getValue(dt_var);
Node t = datatypes::utils::sygusToBuiltin(value);
terms.push_back(t);
exp.size() == 1 ? exp[0] : nm->mkNode(kind::AND, exp),
dt_eval.eqNode(t));
}
+ eval_unfold_lemmas.push_back(lem);
+ }
- if (d_lemma_cache.find(lem) == d_lemma_cache.end())
+ if (mode == options::SygusInstMode::PRIORITY_INST)
+ {
+ if (!inst->addInstantiation(q, terms))
{
- Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl;
- d_quantEngine->addLemma(lem, false);
- d_lemma_cache.insert(lem);
+ sendEvalUnfoldLemmas(eval_unfold_lemmas);
}
}
-
- if (inst->addInstantiation(q, terms))
+ else if (mode == options::SygusInstMode::PRIORITY_EVAL)
+ {
+ if (!sendEvalUnfoldLemmas(eval_unfold_lemmas))
+ {
+ inst->addInstantiation(q, terms);
+ }
+ }
+ else
{
- Trace("sygus-inst") << "Instantiate " << q << std::endl;
+ Assert(mode == options::SygusInstMode::INTERLEAVE);
+ inst->addInstantiation(q, terms);
+ sendEvalUnfoldLemmas(eval_unfold_lemmas);
}
}
}
+bool SygusInst::sendEvalUnfoldLemmas(const std::vector<Node>& lemmas)
+{
+ bool added_lemma = false;
+ for (const Node& lem : lemmas)
+ {
+ Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl;
+ added_lemma |= d_quantEngine->addLemma(lem);
+ }
+ return added_lemma;
+}
+
bool SygusInst::checkCompleteFor(Node q)
{
return d_inactive_quant.find(q) != d_inactive_quant.end();
{
Assert(q[0].getNumChildren() == types.size());
Assert(d_ce_lemmas.find(q) == d_ce_lemmas.end());
+ Assert(d_inst_constants.find(q) == d_inst_constants.end());
+ Assert(d_var_eval.find(q) == d_var_eval.end());
+
+ Trace("sygus-inst") << "Register CE Lemma for " << q << std::endl;
/* Generate counterexample lemma for 'q'. */
NodeManager* nm = NodeManager::currentNM();
/* For each variable x_i of \forall x_i . P[x_i], create a fresh datatype
* instantiation constant ic_i with type types[i] and wrap each ic_i in
* DT_SYGUS_EVAL(ic_i), which will be used to instantiate x_i. */
- std::vector<Node> vars;
std::vector<Node> evals;
+ std::vector<Node> inst_constants;
for (size_t i = 0, size = types.size(); i < size; ++i)
{
TypeNode tn = types[i];
Node ic = nm->mkInstConstant(tn);
InstConstantAttribute ica;
ic.setAttribute(ica, q);
+ Trace("sygus-inst") << "Create " << ic << " for " << var << std::endl;
db->registerEnumerator(ic, ic, nullptr, ROLE_ENUM_MULTI_SOLUTION);
}
Node eval = nm->mkNode(kind::DT_SYGUS_EVAL, args);
- d_inst_constants.emplace(std::make_pair(var, ic));
- d_var_eval.emplace(std::make_pair(var, eval));
-
- vars.push_back(var);
+ inst_constants.push_back(ic);
evals.push_back(eval);
}
+ d_inst_constants.emplace(q, inst_constants);
+ d_var_eval.emplace(q, evals);
+
Node lit = getCeLiteral(q);
d_quantEngine->addRequirePhase(lit, true);
DecisionStrategy* ds =
new DecisionStrategySingleton("CeLiteral",
lit,
- d_quantEngine->getSatContext(),
+ d_qstate.getSatContext(),
d_quantEngine->getValuation());
d_dstrat[q].reset(ds);
/* Add counterexample lemma (lit => ~P[x_i/eval_i]) */
Node body =
- q[1].substitute(vars.begin(), vars.end(), evals.begin(), evals.end());
+ q[1].substitute(q[0].begin(), q[0].end(), evals.begin(), evals.end());
Node lem = nm->mkNode(kind::OR, lit.negate(), body.negate());
lem = Rewriter::rewrite(lem);
projects / cvc5.git / blobdiff