using namespace cvc5::theory::bv;
using namespace cvc5::theory::bv::utils;
-bool CoreSolverExtTheoryCallback::getCurrentSubstitution(
- int effort,
- const std::vector<Node>& vars,
- std::vector<Node>& subs,
- std::map<Node, std::vector<Node> >& exp)
-{
- if (d_equalityEngine == nullptr)
- {
- return false;
- }
- // get the constant equivalence classes
- bool retVal = false;
- for (const Node& n : vars)
- {
- if (d_equalityEngine->hasTerm(n))
- {
- Node nr = d_equalityEngine->getRepresentative(n);
- if (nr.isConst())
- {
- subs.push_back(nr);
- exp[n].push_back(n.eqNode(nr));
- retVal = true;
- }
- else
- {
- subs.push_back(n);
- }
- }
- else
- {
- subs.push_back(n);
- }
- }
- // return true if the substitution is non-trivial
- return retVal;
-}
-
-bool CoreSolverExtTheoryCallback::getReduction(int effort,
- Node n,
- Node& nr,
- bool& satDep)
-{
- Trace("bv-ext") << "TheoryBV::checkExt : non-reduced : " << n << std::endl;
- if (n.getKind() == kind::BITVECTOR_TO_NAT)
- {
- nr = utils::eliminateBv2Nat(n);
- satDep = false;
- return true;
- }
- else if (n.getKind() == kind::INT_TO_BITVECTOR)
- {
- nr = utils::eliminateInt2Bv(n);
- satDep = false;
- return true;
- }
- return false;
-}
-
CoreSolver::CoreSolver(context::Context* c, BVSolverLazy* bv)
: SubtheorySolver(c, bv),
d_notify(*this),
d_preregisterCalled(false),
d_checkCalled(false),
d_bv(bv),
- d_extTheoryCb(),
- d_extTheory(new ExtTheory(d_extTheoryCb,
- bv->d_bv.getSatContext(),
- bv->d_bv.getUserContext(),
- bv->d_bv.getOutputChannel())),
- d_reasons(c),
- d_needsLastCallCheck(false),
- d_extf_range_infer(bv->d_bv.getUserContext()),
- d_extf_collapse_infer(bv->d_bv.getUserContext())
+ d_reasons(c)
{
- d_extTheory->addFunctionKind(kind::BITVECTOR_TO_NAT);
- d_extTheory->addFunctionKind(kind::INT_TO_BITVECTOR);
}
CoreSolver::~CoreSolver() {}
d_equalityEngine->addTriggerPredicate(node);
} else {
d_equalityEngine->addTerm(node);
- // Register with the extended theory, for context-dependent simplification.
- // Notice we do this for registered terms but not internally generated
- // equivalence classes. The two should roughly cooincide. Since ExtTheory is
- // being used as a heuristic, it is good enough to be registered here.
- d_extTheory->registerTerm(node);
}
}
"theory::bv::CoreSolver::NumCallsToCheck"))
{
}
-
-void CoreSolver::checkExtf(Theory::Effort e)
-{
- if (e == Theory::EFFORT_LAST_CALL)
- {
- std::vector<Node> nred = d_extTheory->getActive();
- doExtfReductions(nred);
- }
- Assert(e == Theory::EFFORT_FULL);
- // do inferences (adds external lemmas) TODO: this can be improved to add
- // internal inferences
- std::vector<Node> nred;
- if (d_extTheory->doInferences(0, nred))
- {
- return;
- }
- d_needsLastCallCheck = false;
- if (!nred.empty())
- {
- // other inferences involving bv2nat, int2bv
- if (options::bvAlgExtf())
- {
- if (doExtfInferences(nred))
- {
- return;
- }
- }
- if (!options::bvLazyReduceExtf())
- {
- if (doExtfReductions(nred))
- {
- return;
- }
- }
- else
- {
- d_needsLastCallCheck = true;
- }
- }
-}
-
-bool CoreSolver::needsCheckLastEffort() const { return d_needsLastCallCheck; }
-
-bool CoreSolver::doExtfInferences(std::vector<Node>& terms)
-{
- NodeManager* nm = NodeManager::currentNM();
- SkolemManager* sm = nm->getSkolemManager();
- bool sentLemma = false;
- eq::EqualityEngine* ee = d_equalityEngine;
- std::map<Node, Node> op_map;
- for (unsigned j = 0; j < terms.size(); j++)
- {
- TNode n = terms[j];
- Assert(n.getKind() == kind::BITVECTOR_TO_NAT
- || n.getKind() == kind::INT_TO_BITVECTOR);
- if (n.getKind() == kind::BITVECTOR_TO_NAT)
- {
- // range lemmas
- if (d_extf_range_infer.find(n) == d_extf_range_infer.end())
- {
- d_extf_range_infer.insert(n);
- unsigned bvs = n[0].getType().getBitVectorSize();
- Node min = nm->mkConst(Rational(0));
- Node max = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
- Node lem = nm->mkNode(kind::AND,
- nm->mkNode(kind::GEQ, n, min),
- nm->mkNode(kind::LT, n, max));
- Trace("bv-extf-lemma")
- << "BV extf lemma (range) : " << lem << std::endl;
- d_bv->d_im.lemma(lem, InferenceId::BV_EXTF_LEMMA);
- sentLemma = true;
- }
- }
- Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n[0]) : n[0];
- op_map[r] = n;
- }
- for (unsigned j = 0; j < terms.size(); j++)
- {
- TNode n = terms[j];
- Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n) : n;
- std::map<Node, Node>::iterator it = op_map.find(r);
- if (it != op_map.end())
- {
- Node parent = it->second;
- // Node cterm = parent[0]==n ? parent : nm->mkNode( parent.getOperator(),
- // n );
- Node cterm = parent[0].eqNode(n);
- Trace("bv-extf-lemma-debug")
- << "BV extf collapse based on : " << cterm << std::endl;
- if (d_extf_collapse_infer.find(cterm) == d_extf_collapse_infer.end())
- {
- d_extf_collapse_infer.insert(cterm);
-
- Node t = n[0];
- if (t.getType() == parent.getType())
- {
- if (n.getKind() == kind::INT_TO_BITVECTOR)
- {
- Assert(t.getType().isInteger());
- // congruent modulo 2^( bv width )
- unsigned bvs = n.getType().getBitVectorSize();
- Node coeff = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
- Node k = sm->mkDummySkolem(
- "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence");
- t = nm->mkNode(kind::PLUS, t, nm->mkNode(kind::MULT, coeff, k));
- }
- Node lem = parent.eqNode(t);
-
- if (parent[0] != n)
- {
- Assert(ee->areEqual(parent[0], n));
- lem = nm->mkNode(kind::IMPLIES, parent[0].eqNode(n), lem);
- }
- // this handles inferences of the form, e.g.:
- // ((_ int2bv w) (bv2nat x)) == x (if x is bit-width w)
- // (bv2nat ((_ int2bv w) x)) == x + k*2^w for some k
- Trace("bv-extf-lemma")
- << "BV extf lemma (collapse) : " << lem << std::endl;
- d_bv->d_im.lemma(lem, InferenceId::BV_EXTF_COLLAPSE);
- sentLemma = true;
- }
- }
- Trace("bv-extf-lemma-debug")
- << "BV extf f collapse based on : " << cterm << std::endl;
- }
- }
- return sentLemma;
-}
-
-bool CoreSolver::doExtfReductions(std::vector<Node>& terms)
-{
- std::vector<Node> nredr;
- if (d_extTheory->doReductions(0, terms, nredr))
- {
- return true;
- }
- Assert(nredr.empty());
- return false;
-}
#include "context/cdhashset.h"
#include "theory/bv/bv_subtheory.h"
-#include "theory/ext_theory.h"
namespace cvc5 {
namespace theory {
namespace bv {
-class Base;
-
-/** An extended theory callback used by the core solver */
-class CoreSolverExtTheoryCallback : public ExtTheoryCallback
-{
- public:
- CoreSolverExtTheoryCallback() : d_equalityEngine(nullptr) {}
- /** Get current substitution based on the underlying equality engine. */
- bool getCurrentSubstitution(int effort,
- const std::vector<Node>& vars,
- std::vector<Node>& subs,
- std::map<Node, std::vector<Node> >& exp) override;
- /** Get reduction. */
- bool getReduction(int effort, Node n, Node& nr, bool& satDep) override;
- /** The underlying equality engine */
- eq::EqualityEngine* d_equalityEngine;
-};
-
/**
* Bitvector equality solver
*/
BVSolverLazy* d_bv;
/** Pointer to the equality engine of the parent */
eq::EqualityEngine* d_equalityEngine;
- /** The extended theory callback */
- CoreSolverExtTheoryCallback d_extTheoryCb;
- /** Extended theory module, for context-dependent simplification. */
- std::unique_ptr<ExtTheory> d_extTheory;
/** To make sure we keep the explanations */
context::CDHashSet<Node> d_reasons;
bool isCompleteForTerm(TNode term, TNodeBoolMap& seen);
Statistics d_statistics;
- /** Whether we need a last call effort check */
- bool d_needsLastCallCheck;
- /** For extended functions */
- context::CDHashSet<Node> d_extf_range_infer;
- context::CDHashSet<Node> d_extf_collapse_infer;
-
- /** do extended function inferences
- *
- * This method adds lemmas on the output channel of TheoryBV based on
- * reasoning about extended functions, such as bv2nat and int2bv. Examples
- * of lemmas added by this method include:
- * 0 <= ((_ int2bv w) x) < 2^w
- * ((_ int2bv w) (bv2nat x)) = x
- * (bv2nat ((_ int2bv w) x)) == x + k*2^w
- * The purpose of these lemmas is to recognize easy conflicts before fully
- * reducing extended functions based on their full semantics.
- */
- bool doExtfInferences(std::vector<Node>& terms);
- /** do extended function reductions
- *
- * This method adds lemmas on the output channel of TheoryBV based on
- * reducing all extended function applications that are preregistered to
- * this theory and have not already been reduced by context-dependent
- * simplification (see theory/ext_theory.h). Examples of lemmas added by
- * this method include:
- * (bv2nat x) = (ite ((_ extract w w-1) x) 2^{w-1} 0) + ... +
- * (ite ((_ extract 1 0) x) 1 0)
- */
- bool doExtfReductions(std::vector<Node>& terms);
-
public:
CoreSolver(context::Context* c, BVSolverLazy* bv);
~CoreSolver();
EqualityStatus getEqualityStatus(TNode a, TNode b) override;
bool hasTerm(TNode node) const;
void addTermToEqualityEngine(TNode node);
- /** check extended functions at the given effort */
- void checkExtf(Theory::Effort e);
- bool needsCheckLastEffort() const;
};
}
projects / cvc5.git / commitdiff