/*! \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 <unordered_set>
#include "expr/node_algorithm.h"
+#include "theory/bv/theory_bv_utils.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/quantifiers/sygus/sygus_enumerator.h"
#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 {
} while (!visit.empty());
}
+/*
+ * Add special values for a given type.
+ *
+ * @param tn: The type node.
+ * @param extra_cons: A map of TypeNode to constants, which are added in
+ * addition to the default grammar.
+ */
+void addSpecialValues(
+ const TypeNode& tn,
+ std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& extra_cons)
+{
+ if (tn.isBitVector())
+ {
+ uint32_t size = tn.getBitVectorSize();
+ extra_cons[tn].insert(bv::utils::mkOnes(size));
+ extra_cons[tn].insert(bv::utils::mkMinSigned(size));
+ extra_cons[tn].insert(bv::utils::mkMaxSigned(size));
+ }
+}
+
} // 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,
+ QuantifiersRegistry& qr)
+ : QuantifiersModule(qs, qim, qr, 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)
{
- Trace("sygus-inst") << "Instantiate " << q << std::endl;
+ if (!sendEvalUnfoldLemmas(eval_unfold_lemmas))
+ {
+ inst->addInstantiation(q, terms);
+ }
+ }
+ else
+ {
+ 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_qim.addPendingLemma(lem);
+ }
+ return added_lemma;
+}
+
bool SygusInst::checkCompleteFor(Node q)
{
return d_inactive_quant.find(q) != d_inactive_quant.end();
std::vector<TypeNode> types;
for (const Node& var : q[0])
{
+ addSpecialValues(var.getType(), extra_cons);
TypeNode tn = CegGrammarConstructor::mkSygusDefaultType(var.getType(),
Node(),
var.toString(),
{
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);
+ d_qim.addPendingPhaseRequirement(lit, true);
/* The decision strategy for quantified formula 'q' ensures that its
* counterexample literal is decided on first. It is user-context dependent.
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);
if (d_ce_lemma_added.find(q) != d_ce_lemma_added.end()) return;
Node lem = d_ce_lemmas[q];
- d_quantEngine->addLemma(lem, false);
+ d_qim.addPendingLemma(lem);
d_ce_lemma_added.insert(q);
Trace("sygus-inst") << "Add CE Lemma: " << lem << std::endl;
}