This PR refactors ppAssert from the lazy BV solver and moves it to TheoryBV.
virtual std::string identify() const = 0;
- virtual Theory::PPAssertStatus ppAssert(
- TrustNode in, TrustSubstitutionMap& outSubstitutions) = 0;
-
virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); };
virtual void ppStaticLearn(TNode in, NodeBuilder& learned){};
std::string identify() const override { return "BVSolverBitblast"; };
- Theory::PPAssertStatus ppAssert(
- TrustNode in, TrustSubstitutionMap& outSubstitutions) override
- {
- return Theory::PPAssertStatus::PP_ASSERT_STATUS_UNSOLVED;
- }
-
EqualityStatus getEqualityStatus(TNode a, TNode b) override;
bool collectModelValues(TheoryModel* m,
#include "theory/bv/theory_bv_rewriter.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/theory_model.h"
-#include "theory/trust_substitutions.h"
using namespace cvc5::theory::bv::utils;
BVSolverLazy::Statistics::Statistics()
: d_avgConflictSize(smtStatisticsRegistry().registerAverage(
"theory::bv::lazy::AvgBVConflictSize")),
- d_solveSubstitutions(smtStatisticsRegistry().registerInt(
- "theory::bv::lazy::NumSolveSubstitutions")),
d_solveTimer(smtStatisticsRegistry().registerTimer(
"theory::bv::lazy::solveTimer")),
d_numCallsToCheckFullEffort(smtStatisticsRegistry().registerInt(
}
}
-Theory::PPAssertStatus BVSolverLazy::ppAssert(
- TrustNode tin, TrustSubstitutionMap& outSubstitutions)
-{
- TNode in = tin.getNode();
- switch (in.getKind())
- {
- case kind::EQUAL:
- {
- if (in[0].isVar() && d_bv.isLegalElimination(in[0], in[1]))
- {
- ++(d_statistics.d_solveSubstitutions);
- outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
- return Theory::PP_ASSERT_STATUS_SOLVED;
- }
- if (in[1].isVar() && d_bv.isLegalElimination(in[1], in[0]))
- {
- ++(d_statistics.d_solveSubstitutions);
- outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
- return Theory::PP_ASSERT_STATUS_SOLVED;
- }
- Node node = Rewriter::rewrite(in);
- if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst())
- || (node[1].getKind() == kind::BITVECTOR_EXTRACT
- && node[0].isConst()))
- {
- Node extract = node[0].isConst() ? node[1] : node[0];
- if (extract[0].isVar())
- {
- Node c = node[0].isConst() ? node[0] : node[1];
-
- unsigned high = utils::getExtractHigh(extract);
- unsigned low = utils::getExtractLow(extract);
- unsigned var_bitwidth = utils::getSize(extract[0]);
- std::vector<Node> children;
-
- if (low == 0)
- {
- Assert(high != var_bitwidth - 1);
- unsigned skolem_size = var_bitwidth - high - 1;
- Node skolem = utils::mkVar(skolem_size);
- children.push_back(skolem);
- children.push_back(c);
- }
- else if (high == var_bitwidth - 1)
- {
- unsigned skolem_size = low;
- Node skolem = utils::mkVar(skolem_size);
- children.push_back(c);
- children.push_back(skolem);
- }
- else
- {
- unsigned skolem1_size = low;
- unsigned skolem2_size = var_bitwidth - high - 1;
- Node skolem1 = utils::mkVar(skolem1_size);
- Node skolem2 = utils::mkVar(skolem2_size);
- children.push_back(skolem2);
- children.push_back(c);
- children.push_back(skolem1);
- }
- Node concat = utils::mkConcat(children);
- Assert(utils::getSize(concat) == utils::getSize(extract[0]));
- if (d_bv.isLegalElimination(extract[0], concat))
- {
- outSubstitutions.addSubstitutionSolved(extract[0], concat, tin);
- return Theory::PP_ASSERT_STATUS_SOLVED;
- }
- }
- }
- }
- break;
- case kind::BITVECTOR_ULT:
- case kind::BITVECTOR_SLT:
- case kind::BITVECTOR_ULE:
- case kind::BITVECTOR_SLE:
-
- default:
- // TODO other predicates
- break;
- }
- return Theory::PP_ASSERT_STATUS_UNSOLVED;
-}
-
TrustNode BVSolverLazy::ppRewrite(TNode t)
{
Debug("bv-pp-rewrite") << "BVSolverLazy::ppRewrite " << t << "\n";
std::string identify() const override { return std::string("BVSolverLazy"); }
- Theory::PPAssertStatus ppAssert(
- TrustNode tin, TrustSubstitutionMap& outSubstitutions) override;
-
TrustNode ppRewrite(TNode t) override;
void ppStaticLearn(TNode in, NodeBuilder& learned) override;
{
public:
AverageStat d_avgConflictSize;
- IntStat d_solveSubstitutions;
TimerStat d_solveTimer;
IntStat d_numCallsToCheckFullEffort;
IntStat d_numCallsToCheckStandardEffort;
std::string identify() const override { return "BVSolverSimple"; };
- Theory::PPAssertStatus ppAssert(
- TrustNode in, TrustSubstitutionMap& outSubstitutions) override
- {
- return Theory::PPAssertStatus::PP_ASSERT_STATUS_UNSOLVED;
- }
-
bool collectModelValues(TheoryModel* m,
const std::set<Node>& termSet) override;
#include "expr/proof_checker.h"
#include "options/bv_options.h"
#include "options/smt_options.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/bv/bv_solver_bitblast.h"
#include "theory/bv/bv_solver_lazy.h"
#include "theory/bv/bv_solver_simple.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/ee_setup_info.h"
+#include "theory/trust_substitutions.h"
namespace cvc5 {
namespace theory {
d_rewriter(),
d_state(c, u, valuation),
d_im(*this, d_state, nullptr, "theory::bv::"),
- d_notify(d_im)
+ d_notify(d_im),
+ d_stats("theory::bv::")
{
switch (options::bvSolver())
{
Theory::PPAssertStatus TheoryBV::ppAssert(
TrustNode tin, TrustSubstitutionMap& outSubstitutions)
{
- return d_internal->ppAssert(tin, outSubstitutions);
+ TNode in = tin.getNode();
+ Kind k = in.getKind();
+ if (k == kind::EQUAL)
+ {
+ // Substitute variables
+ if (in[0].isVar() && isLegalElimination(in[0], in[1]))
+ {
+ ++d_stats.d_solveSubstitutions;
+ outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
+ return Theory::PP_ASSERT_STATUS_SOLVED;
+ }
+ if (in[1].isVar() && isLegalElimination(in[1], in[0]))
+ {
+ ++d_stats.d_solveSubstitutions;
+ outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
+ return Theory::PP_ASSERT_STATUS_SOLVED;
+ }
+ /**
+ * Eliminate extract over bit-vector variables.
+ *
+ * Given x[h:l] = c, where c is a constant and x is a variable.
+ *
+ * We rewrite to:
+ *
+ * x = sk1::c if l == 0, where bw(sk1) = bw(x)-1-h
+ * x = c::sk2 if h == bw(x)-1, where bw(sk2) = l
+ * x = sk1::c::sk2 otherwise, where bw(sk1) = bw(x)-1-h and bw(sk2) = l
+ */
+ Node node = Rewriter::rewrite(in);
+ if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst())
+ || (node[1].getKind() == kind::BITVECTOR_EXTRACT
+ && node[0].isConst()))
+ {
+ Node extract = node[0].isConst() ? node[1] : node[0];
+ if (extract[0].isVar())
+ {
+ Node c = node[0].isConst() ? node[0] : node[1];
+
+ uint32_t high = utils::getExtractHigh(extract);
+ uint32_t low = utils::getExtractLow(extract);
+ uint32_t var_bw = utils::getSize(extract[0]);
+ std::vector<Node> children;
+
+ // create sk1 with size bw(x)-1-h
+ if (low == 0 || high != var_bw - 1)
+ {
+ Assert(high != var_bw - 1);
+ uint32_t skolem_size = var_bw - high - 1;
+ Node skolem = utils::mkVar(skolem_size);
+ children.push_back(skolem);
+ }
+
+ children.push_back(c);
+
+ // create sk2 with size l
+ if (high == var_bw - 1 || low != 0)
+ {
+ Assert(low != 0);
+ uint32_t skolem_size = low;
+ Node skolem = utils::mkVar(skolem_size);
+ children.push_back(skolem);
+ }
+
+ Node concat = utils::mkConcat(children);
+ Assert(utils::getSize(concat) == utils::getSize(extract[0]));
+ if (isLegalElimination(extract[0], concat))
+ {
+ outSubstitutions.addSubstitutionSolved(extract[0], concat, tin);
+ return Theory::PP_ASSERT_STATUS_SOLVED;
+ }
+ }
+ }
+ }
+ return Theory::PP_ASSERT_STATUS_UNSOLVED;
}
TrustNode TheoryBV::ppRewrite(TNode t, std::vector<SkolemLemma>& lems)
return d_internal->applyAbstraction(assertions, new_assertions);
}
+TheoryBV::Statistics::Statistics(const std::string& name)
+ : d_solveSubstitutions(
+ smtStatisticsRegistry().registerInt(name + "NumSolveSubstitutions"))
+{
+}
+
} // namespace bv
} // namespace theory
} // namespace cvc5
/** The notify class for equality engine. */
TheoryEqNotifyClass d_notify;
+ /** TheoryBV statistics. */
+ struct Statistics
+ {
+ Statistics(const std::string& name);
+ IntStat d_solveSubstitutions;
+ } d_stats;
+
}; /* class TheoryBV */
} // namespace bv
projects / cvc5.git / commitdiff