This commit refactors the getEqualityStatus handling for bitblast and bitblast-internal.
return d_bb->getStoredBBAtom(node);
}
+void BBProof::getBBTerm(TNode node, Bits& bits) const
+{
+ d_bb->getBBTerm(node, bits);
+}
+
bool BBProof::collectModelValues(TheoryModel* m,
const std::set<Node>& relevantTerms)
{
bool hasBBTerm(TNode node) const;
/** Get bit-blasted node stored for atom. */
Node getStoredBBAtom(TNode node);
+ /** Get bit-blasted bits stored for node. */
+ void getBBTerm(TNode node, Bits& bits) const;
/** Collect model values for all relevant terms given in 'relevantTerms'. */
bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms);
return EqualityStatus::EQUALITY_UNKNOWN;
}
+ /**
+ * Get the current value of `node`.
+ *
+ * The `initialize` flag indicates whether bits should be zero-initialized
+ * if they don't have a value yet.
+ */
+ virtual Node getValue(TNode node, bool initialize) { return Node::null(); }
+
/** Called by abstraction preprocessing pass. */
virtual bool applyAbstraction(const std::vector<Node>& assertions,
std::vector<Node>& new_assertions)
d_bbInputFacts(s->getSatContext()),
d_assumptions(s->getSatContext()),
d_assertions(s->getSatContext()),
- d_invalidateModelCache(s->getSatContext(), true),
- d_inSatMode(s->getSatContext(), false),
d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
: nullptr),
d_factLiteralCache(s->getSatContext()),
d_assumptions.push_back(d_factLiteralCache[fact]);
}
- d_invalidateModelCache.set(true);
std::vector<prop::SatLiteral> assumptions(d_assumptions.begin(),
d_assumptions.end());
prop::SatValue val = d_satSolver->solve(assumptions);
- d_inSatMode = val == prop::SatValue::SAT_VALUE_TRUE;
- Debug("bv-bitblast") << "d_inSatMode: " << d_inSatMode << std::endl;
if (val == prop::SatValue::SAT_VALUE_FALSE)
{
continue;
}
- Node value = getValueFromSatSolver(term, true);
+ Node value = getValue(term, true);
Assert(value.isConst());
if (!m->assertEquality(term, value, true))
{
return true;
}
-EqualityStatus BVSolverBitblast::getEqualityStatus(TNode a, TNode b)
-{
- Debug("bv-bitblast") << "getEqualityStatus on " << a << " and " << b
- << std::endl;
- if (!d_inSatMode)
- {
- Debug("bv-bitblast") << EQUALITY_UNKNOWN << std::endl;
- return EQUALITY_UNKNOWN;
- }
- Node value_a = getValue(a);
- Node value_b = getValue(b);
-
- if (value_a == value_b)
- {
- Debug("bv-bitblast") << EQUALITY_TRUE_IN_MODEL << std::endl;
- return EQUALITY_TRUE_IN_MODEL;
- }
- Debug("bv-bitblast") << EQUALITY_FALSE_IN_MODEL << std::endl;
- return EQUALITY_FALSE_IN_MODEL;
-}
-
void BVSolverBitblast::initSatSolver()
{
switch (options::bvSatSolver())
"theory::bv::BVSolverBitblast"));
}
-Node BVSolverBitblast::getValueFromSatSolver(TNode node, bool initialize)
+Node BVSolverBitblast::getValue(TNode node, bool initialize)
{
if (node.isConst())
{
return utils::mkConst(bits.size(), value);
}
-Node BVSolverBitblast::getValue(TNode node)
-{
- if (d_invalidateModelCache.get())
- {
- d_modelCache.clear();
- }
- d_invalidateModelCache.set(false);
-
- std::vector<TNode> visit;
-
- TNode cur;
- visit.push_back(node);
- do
- {
- cur = visit.back();
- visit.pop_back();
-
- auto it = d_modelCache.find(cur);
- if (it != d_modelCache.end() && !it->second.isNull())
- {
- continue;
- }
-
- if (d_bitblaster->hasBBTerm(cur))
- {
- Node value = getValueFromSatSolver(cur, false);
- if (value.isConst())
- {
- d_modelCache[cur] = value;
- continue;
- }
- }
- if (Theory::isLeafOf(cur, theory::THEORY_BV))
- {
- Node value = getValueFromSatSolver(cur, true);
- d_modelCache[cur] = value;
- continue;
- }
-
- if (it == d_modelCache.end())
- {
- visit.push_back(cur);
- d_modelCache.emplace(cur, Node());
- visit.insert(visit.end(), cur.begin(), cur.end());
- }
- else if (it->second.isNull())
- {
- NodeBuilder nb(cur.getKind());
- if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
- {
- nb << cur.getOperator();
- }
-
- std::unordered_map<Node, Node>::iterator iit;
- for (const TNode& child : cur)
- {
- iit = d_modelCache.find(child);
- Assert(iit != d_modelCache.end());
- Assert(iit->second.isConst());
- nb << iit->second;
- }
- it->second = Rewriter::rewrite(nb.constructNode());
- }
- } while (!visit.empty());
-
- auto it = d_modelCache.find(node);
- Assert(it != d_modelCache.end());
- return it->second;
-}
-
void BVSolverBitblast::handleEagerAtom(TNode fact, bool assertFact)
{
Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
std::string identify() const override { return "BVSolverBitblast"; };
- EqualityStatus getEqualityStatus(TNode a, TNode b) override;
-
void computeRelevantTerms(std::set<Node>& termSet) override;
bool collectModelValues(TheoryModel* m,
const std::set<Node>& termSet) override;
- private:
- /** Initialize SAT solver and CNF stream. */
- void initSatSolver();
-
/**
- * Get value of `node` from SAT solver.
+ * Get the current value of `node`.
*
* The `initialize` flag indicates whether bits should be zero-initialized
* if they were not bit-blasted yet.
*/
- Node getValueFromSatSolver(TNode node, bool initialize);
+ Node getValue(TNode node, bool initialize) override;
- /**
- * Get the current value of `node`.
- *
- * Computes the value if `node` was not yet bit-blasted.
- */
- Node getValue(TNode node);
+ private:
+ /** Initialize SAT solver and CNF stream. */
+ void initSatSolver();
/**
* Handle BITVECTOR_EAGER_ATOM atoms and assert/assume to CnfStream.
*/
void handleEagerAtom(TNode fact, bool assertFact);
- /**
- * Cache for getValue() calls.
- *
- * Is cleared at the beginning of a getValue() call if the
- * `d_invalidateModelCache` flag is set to true.
- */
- std::unordered_map<Node, Node> d_modelCache;
-
/** Bit-blaster used to bit-blast atoms/terms. */
std::unique_ptr<NodeBitblaster> d_bitblaster;
/** Stores the current input assertions. */
context::CDList<Node> d_assertions;
- /** Flag indicating whether `d_modelCache` should be invalidated. */
- context::CDO<bool> d_invalidateModelCache;
-
- /** Indicates whether the last check() call was satisfiable. */
- context::CDO<bool> d_inSatMode;
-
/** Proof generator that manages proofs for lemmas generated by this class. */
std::unique_ptr<EagerProofGenerator> d_epg;
return d_bitblaster->collectModelValues(m, termSet);
}
+Node BVSolverBitblastInternal::getValue(TNode node, bool initialize)
+{
+ if (node.isConst())
+ {
+ return node;
+ }
+
+ if (!d_bitblaster->hasBBTerm(node))
+ {
+ return initialize ? utils::mkConst(utils::getSize(node), 0u) : Node();
+ }
+
+ Valuation& val = d_state.getValuation();
+
+ std::vector<Node> bits;
+ d_bitblaster->getBBTerm(node, bits);
+ Integer value(0), one(1), zero(0), bit;
+ for (size_t i = 0, size = bits.size(), j = size - 1; i < size; ++i, --j)
+ {
+ bool satValue;
+ if (val.hasSatValue(bits[j], satValue))
+ {
+ bit = satValue ? one : zero;
+ }
+ else
+ {
+ if (!initialize) return Node();
+ bit = zero;
+ }
+ value = value * 2 + bit;
+ }
+ return utils::mkConst(bits.size(), value);
+}
+
BVProofRuleChecker* BVSolverBitblastInternal::getProofChecker()
{
return &d_checker;
ProofNodeManager* pnm);
~BVSolverBitblastInternal() = default;
+ bool needsEqualityEngine(EeSetupInfo& esi) override { return true; }
+
void preRegisterTerm(TNode n) override {}
bool preNotifyFact(TNode atom,
bool collectModelValues(TheoryModel* m,
const std::set<Node>& termSet) override;
+ Node getValue(TNode node, bool initialize) override;
+
/** get the proof checker of this theory */
BVProofRuleChecker* getProofChecker();
d_state(c, u, valuation),
d_im(*this, d_state, nullptr, "theory::bv::"),
d_notify(d_im),
+ d_invalidateModelCache(c, true),
d_stats("theory::bv::")
{
switch (options::bvSolver())
bool TheoryBV::preCheck(Effort e) { return d_internal->preCheck(e); }
-void TheoryBV::postCheck(Effort e) { d_internal->postCheck(e); }
+void TheoryBV::postCheck(Effort e)
+{
+ d_invalidateModelCache = true;
+ d_internal->postCheck(e);
+}
bool TheoryBV::preNotifyFact(
TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
{
- return d_internal->getEqualityStatus(a, b);
+ EqualityStatus status = d_internal->getEqualityStatus(a, b);
+
+ if (status == EqualityStatus::EQUALITY_UNKNOWN)
+ {
+ Node value_a = getValue(a);
+ Node value_b = getValue(b);
+
+ if (value_a.isNull() || value_b.isNull())
+ {
+ return status;
+ }
+
+ if (value_a == value_b)
+ {
+ Debug("theory-bv") << EQUALITY_TRUE_IN_MODEL << std::endl;
+ return EQUALITY_TRUE_IN_MODEL;
+ }
+ Debug("theory-bv") << EQUALITY_FALSE_IN_MODEL << std::endl;
+ return EQUALITY_FALSE_IN_MODEL;
+ }
+ return status;
}
TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); }
return d_internal->applyAbstraction(assertions, new_assertions);
}
+Node TheoryBV::getValue(TNode node)
+{
+ if (d_invalidateModelCache.get())
+ {
+ d_modelCache.clear();
+ }
+ d_invalidateModelCache.set(false);
+
+ std::vector<TNode> visit;
+
+ TNode cur;
+ visit.push_back(node);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+
+ auto it = d_modelCache.find(cur);
+ if (it != d_modelCache.end() && !it->second.isNull())
+ {
+ continue;
+ }
+
+ if (cur.isConst())
+ {
+ d_modelCache[cur] = cur;
+ continue;
+ }
+
+ Node value = d_internal->getValue(cur, false);
+ if (value.isConst())
+ {
+ d_modelCache[cur] = value;
+ continue;
+ }
+
+ if (Theory::isLeafOf(cur, theory::THEORY_BV))
+ {
+ value = d_internal->getValue(cur, true);
+ d_modelCache[cur] = value;
+ continue;
+ }
+
+ if (it == d_modelCache.end())
+ {
+ visit.push_back(cur);
+ d_modelCache.emplace(cur, Node());
+ visit.insert(visit.end(), cur.begin(), cur.end());
+ }
+ else if (it->second.isNull())
+ {
+ NodeBuilder nb(cur.getKind());
+ if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
+ {
+ nb << cur.getOperator();
+ }
+
+ std::unordered_map<Node, Node>::iterator iit;
+ for (const TNode& child : cur)
+ {
+ iit = d_modelCache.find(child);
+ Assert(iit != d_modelCache.end());
+ Assert(iit->second.isConst());
+ nb << iit->second;
+ }
+ it->second = Rewriter::rewrite(nb.constructNode());
+ }
+ } while (!visit.empty());
+
+ auto it = d_modelCache.find(node);
+ Assert(it != d_modelCache.end());
+ return it->second;
+}
+
TheoryBV::Statistics::Statistics(const std::string& name)
: d_solveSubstitutions(
smtStatisticsRegistry().registerInt(name + "NumSolveSubstitutions"))
private:
void notifySharedTerm(TNode t) override;
+ Node getValue(TNode node);
+
/** Internal BV solver. */
std::unique_ptr<BVSolver> d_internal;
/** The notify class for equality engine. */
TheoryEqNotifyClass d_notify;
+ /** Flag indicating whether `d_modelCache` should be invalidated. */
+ context::CDO<bool> d_invalidateModelCache;
+
+ /**
+ * Cache for getValue() calls.
+ *
+ * Is cleared at the beginning of a getValue() call if the
+ * `d_invalidateModelCache` flag is set to true.
+ */
+ std::unordered_map<Node, Node> d_modelCache;
+
/** TheoryBV statistics. */
struct Statistics
{
projects / cvc5.git / commitdiff