This commit separates the lazy bit-vector solver from TheoryBV, which is now a thin wrapper around a bit-vector solver d_internal . This will allow us to easily swap out the bit-vector solver in the future.
theory/bv/bv_inequality_graph.h
theory/bv/bv_quick_check.cpp
theory/bv/bv_quick_check.h
+ theory/bv/bv_solver.h
+ theory/bv/bv_solver_lazy.cpp
+ theory/bv/bv_solver_lazy.h
theory/bv/bv_subtheory.h
theory/bv/bv_subtheory_algebraic.cpp
theory/bv/bv_subtheory_algebraic.h
** Bitblaster for the eager bv solver.
**/
-#include "cvc4_private.h"
-
#include "theory/bv/bitblast/eager_bitblaster.h"
+#include "cvc4_private.h"
#include "options/bv_options.h"
#include "prop/cnf_stream.h"
#include "prop/sat_solver_factory.h"
#include "smt/smt_statistics_registry.h"
+#include "theory/bv/bv_solver_lazy.h"
#include "theory/bv/theory_bv.h"
#include "theory/theory_model.h"
namespace theory {
namespace bv {
-EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c)
+EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c)
: TBitblaster<Node>(),
d_context(c),
d_satSolver(),
namespace bv {
class BitblastingRegistrar;
-class TheoryBV;
+class BVSolverLazy;
class EagerBitblaster : public TBitblaster<Node>
{
public:
- EagerBitblaster(TheoryBV* theory_bv, context::Context* context);
+ EagerBitblaster(BVSolverLazy* theory_bv, context::Context* context);
~EagerBitblaster();
void addAtom(TNode atom);
std::unique_ptr<prop::SatSolver> d_satSolver;
std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar;
- TheoryBV* d_bv;
+ BVSolverLazy* d_bv;
TNodeSet d_bbAtoms;
TNodeSet d_variables;
** Bitblaster for the lazy bv solver.
**/
-#include "cvc4_private.h"
-
#include "theory/bv/bitblast/lazy_bitblaster.h"
+#include "cvc4_private.h"
#include "options/bv_options.h"
#include "prop/cnf_stream.h"
#include "prop/sat_solver.h"
#include "prop/sat_solver_factory.h"
#include "smt/smt_statistics_registry.h"
#include "theory/bv/abstraction.h"
+#include "theory/bv/bv_solver_lazy.h"
#include "theory/bv/theory_bv.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/rewriter.h"
}
TLazyBitblaster::TLazyBitblaster(context::Context* c,
- bv::TheoryBV* bv,
+ bv::BVSolverLazy* bv,
const std::string name,
bool emptyNotify)
: TBitblaster<Node>(),
markerLit = ~markerLit;
}
- Debug("bitvector-bb") << "TheoryBV::TLazyBitblaster::assertToSat asserting node: " << atom <<"\n";
- Debug("bitvector-bb") << "TheoryBV::TLazyBitblaster::assertToSat with literal: " << markerLit << "\n";
+ Debug("bitvector-bb")
+ << "BVSolverLazy::TLazyBitblaster::assertToSat asserting node: " << atom
+ << "\n";
+ Debug("bitvector-bb")
+ << "BVSolverLazy::TLazyBitblaster::assertToSat with literal: "
+ << markerLit << "\n";
prop::SatValue ret = d_satSolver->assertAssumption(markerLit, propagate);
lemmab << d_cnf->getNode(clause[i]);
}
Node lemma = lemmab;
- d_bv->d_out->lemma(lemma);
+ d_bv->d_inferManager.lemma(lemma);
} else {
- d_bv->d_out->lemma(d_cnf->getNode(clause[0]));
+ d_bv->d_inferManager.lemma(d_cnf->getNode(clause[0]));
}
}
void TLazyBitblaster::MinisatNotify::safePoint(ResourceManager::Resource r)
{
- d_bv->d_out->safePoint(r);
+ d_bv->d_inferManager.safePoint(r);
}
EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b)
namespace theory {
namespace bv {
-class TheoryBV;
+class BVSolverLazy;
class TLazyBitblaster : public TBitblaster<Node>
{
bool hasBBAtom(TNode atom) const override;
TLazyBitblaster(context::Context* c,
- TheoryBV* bv,
+ BVSolverLazy* bv,
const std::string name = "",
bool emptyNotify = false);
~TLazyBitblaster();
class MinisatNotify : public prop::BVSatSolverNotify
{
prop::CnfStream* d_cnf;
- TheoryBV* d_bv;
+ BVSolverLazy* d_bv;
TLazyBitblaster* d_lazyBB;
public:
- MinisatNotify(prop::CnfStream* cnf, TheoryBV* bv, TLazyBitblaster* lbv)
+ MinisatNotify(prop::CnfStream* cnf, BVSolverLazy* bv, TLazyBitblaster* lbv)
: d_cnf(cnf), d_bv(bv), d_lazyBB(lbv)
{
}
void safePoint(ResourceManager::Resource r) override;
};
- TheoryBV* d_bv;
+ BVSolverLazy* d_bv;
context::Context* d_ctx;
std::unique_ptr<prop::NullRegistrar> d_nullRegistrar;
namespace theory {
namespace bv {
-EagerBitblastSolver::EagerBitblastSolver(context::Context* c, TheoryBV* bv)
+EagerBitblastSolver::EagerBitblastSolver(context::Context* c, BVSolverLazy* bv)
: d_assertionSet(c),
d_assumptionSet(c),
d_context(c),
#include <vector>
#include "expr/node.h"
-#include "theory/bv/theory_bv.h"
+#include "theory/bv/bv_solver_lazy.h"
#include "theory/theory_model.h"
namespace CVC4 {
*/
class EagerBitblastSolver {
public:
- EagerBitblastSolver(context::Context* c, theory::bv::TheoryBV* bv);
+ EagerBitblastSolver(context::Context* c, theory::bv::BVSolverLazy* bv);
~EagerBitblastSolver();
bool checkSat();
void assertFormula(TNode formula);
std::unique_ptr<AigBitblaster> d_aigBitblaster;
bool d_useAig;
- TheoryBV* d_bv;
+ BVSolverLazy* d_bv;
}; // class EagerBitblastSolver
} // namespace bv
#include "smt/smt_statistics_registry.h"
#include "theory/bv/bitblast/lazy_bitblaster.h"
+#include "theory/bv/bv_solver_lazy.h"
#include "theory/bv/theory_bv_utils.h"
using namespace CVC4::prop;
namespace theory {
namespace bv {
-BVQuickCheck::BVQuickCheck(const std::string& name, theory::bv::TheoryBV* bv)
- : d_ctx()
- , d_bitblaster(new TLazyBitblaster(&d_ctx, bv, name, true))
- , d_conflict()
- , d_inConflict(&d_ctx, false)
+BVQuickCheck::BVQuickCheck(const std::string& name,
+ theory::bv::BVSolverLazy* bv)
+ : d_ctx(),
+ d_bitblaster(new TLazyBitblaster(&d_ctx, bv, name, true)),
+ d_conflict(),
+ d_inConflict(&d_ctx, false)
{}
#ifndef CVC4__BV_QUICK_CHECK_H
#define CVC4__BV_QUICK_CHECK_H
-#include <vector>
#include <unordered_set>
+#include <vector>
#include "context/cdo.h"
#include "expr/node.h"
namespace bv {
class TLazyBitblaster;
-class TheoryBV;
+class BVSolverLazy;
-class BVQuickCheck {
+class BVQuickCheck
+{
context::Context d_ctx;
std::unique_ptr<TLazyBitblaster> d_bitblaster;
Node d_conflict;
context::CDO<bool> d_inConflict;
void setConflict();
-public:
- BVQuickCheck(const std::string& name, theory::bv::TheoryBV* bv);
+ public:
+ BVQuickCheck(const std::string& name, theory::bv::BVSolverLazy* bv);
~BVQuickCheck();
bool inConflict();
Node getConflict() { return d_conflict; }
- /**
+ /**
* Checks the satisfiability for a given set of assumptions.
- *
+ *
* @param assumptions literals assumed true
* @param budget max number of conflicts
- *
- * @return
+ *
+ * @return
*/
prop::SatValue checkSat(std::vector<Node>& assumptions, unsigned long budget);
- /**
+ /**
* Checks the satisfiability of given assertions.
- *
+ *
* @param budget max number of conflicts
- *
- * @return
+ *
+ * @return
*/
prop::SatValue checkSat(unsigned long budget);
-
- /**
+
+ /**
* Convert to CNF and assert the given literal.
- *
+ *
* @param assumption bv literal
- *
+ *
* @return false if a conflict has been found via bcp.
*/
bool addAssertion(TNode assumption);
void push();
void pop();
void popToZero();
- /**
+ /**
* Deletes the SAT solver and CNF stream, but maintains the
- * bit-blasting term cache.
- *
+ * bit-blasting term cache.
+ *
*/
- void clearSolver();
+ void clearSolver();
- /**
+ /**
* Computes the size of the circuit required to bit-blast
- * atom, by not recounting the nodes in seen.
- *
- * @param node
- * @param seen
- *
- * @return
+ * atom, by not recounting the nodes in seen.
+ *
+ * @param node
+ * @param seen
+ *
+ * @return
*/
uint64_t computeAtomWeight(TNode atom, NodeSet& seen);
bool collectModelInfo(theory::TheoryModel* model, bool fullModel);
- typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator vars_iterator;
- vars_iterator beginVars();
- vars_iterator endVars();
-
- Node getVarValue(TNode var, bool fullModel);
+ typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator
+ vars_iterator;
+ vars_iterator beginVars();
+ vars_iterator endVars();
+ Node getVarValue(TNode var, bool fullModel);
};
-
-class QuickXPlain {
- struct Statistics {
+class QuickXPlain
+{
+ struct Statistics
+ {
TimerStat d_xplainTime;
IntStat d_numSolved;
IntStat d_numUnknown;
unsigned long d_budget;
// crazy heuristic variables
- unsigned d_numCalled; // number of times called
- double d_minRatioSum; // sum of minimization ratio for computing average min ratio
- unsigned d_numConflicts; // number of conflicts (including when minimization not applied)
+ unsigned d_numCalled; // number of times called
+ double d_minRatioSum; // sum of minimization ratio for computing average min
+ // ratio
+ unsigned d_numConflicts; // number of conflicts (including when minimization
+ // not applied)
// unsigned d_period; // after how many conflicts to try minimizing again
// double d_thresh; // if minimization ratio is less, increase period
- // double d_hardThresh; // decrease period if minimization ratio is greater than this
-
-
+ // double d_hardThresh; // decrease period if minimization ratio is greater
+ // than this
+
Statistics d_statistics;
- /**
+ /**
* Uses solve with assumptions unsat core feature to
* further minimize a conflict. The minimized conflict
* will be between low and the returned value in conflict.
- *
- * @param low
- * @param high
- * @param conflict
- *
- * @return
+ *
+ * @param low
+ * @param high
+ * @param conflict
+ *
+ * @return
*/
- unsigned selectUnsatCore(unsigned low, unsigned high,
+ unsigned selectUnsatCore(unsigned low,
+ unsigned high,
std::vector<TNode>& conflict);
- /**
+ /**
* Internal conflict minimization, attempts to minimize
* literals in conflict between low and high and adds the
- * result in new_conflict.
- *
- * @param low
- * @param high
- * @param conflict
- * @param new_conflict
+ * result in new_conflict.
+ *
+ * @param low
+ * @param high
+ * @param conflict
+ * @param new_conflict
*/
- void minimizeConflictInternal(unsigned low, unsigned high,
+ void minimizeConflictInternal(unsigned low,
+ unsigned high,
std::vector<TNode>& conflict,
std::vector<TNode>& new_conflict);
bool useHeuristic();
-public:
- QuickXPlain(const std::string& name, BVQuickCheck* solver, unsigned long budged = 10000);
+
+ public:
+ QuickXPlain(const std::string& name,
+ BVQuickCheck* solver,
+ unsigned long budged = 10000);
~QuickXPlain();
- Node minimizeConflict(TNode conflict);
+ Node minimizeConflict(TNode conflict);
};
-} /* bv namespace */
-} /* theory namespace */
-} /* CVC4 namespace */
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
#endif /* CVC4__BV_QUICK_CHECK_H */
--- /dev/null
+/********************* */
+/*! \file bv_solver.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mathias Preiner
+ ** 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.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Bit-vector solver interface.
+ **
+ ** Describes the interface for the internal bit-vector solver of TheoryBV.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BV__BV_SOLVER_H
+#define CVC4__THEORY__BV__BV_SOLVER_H
+
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class BVSolver
+{
+ public:
+ BVSolver(TheoryState& state, TheoryInferenceManager& inferMgr)
+ : d_state(state), d_inferManager(inferMgr){};
+
+ virtual ~BVSolver(){};
+
+ /**
+ * Returns true if we need an equality engine. If so, we initialize the
+ * information regarding how it should be setup. For details, see the
+ * documentation in Theory::needsEqualityEngine.
+ */
+ virtual bool needsEqualityEngine(EeSetupInfo& esi) { return false; }
+
+ virtual void finishInit(){};
+
+ virtual void preRegisterTerm(TNode n) = 0;
+
+ /**
+ * Forwarded from TheoryBV::preCheck().
+ */
+ virtual bool preCheck(Theory::Effort level = Theory::Effort::EFFORT_FULL)
+ {
+ return false;
+ }
+ /**
+ * Forwarded from TheoryBV::postCheck().
+ */
+ virtual void postCheck(Theory::Effort level = Theory::Effort::EFFORT_FULL){};
+ /**
+ * Forwarded from TheoryBV:preNotifyFact().
+ */
+ virtual bool preNotifyFact(
+ TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
+ {
+ return false;
+ }
+ /**
+ * Forwarded from TheoryBV::notifyFact().
+ */
+ virtual void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) {}
+
+ virtual bool needsCheckLastEffort() = 0;
+
+ virtual void propagate(Theory::Effort e){};
+
+ virtual TrustNode explain(TNode n)
+ {
+ Unimplemented() << "BVSolver propagated a node but doesn't implement the "
+ "BVSolver::explain() interface!";
+ return TrustNode::null();
+ };
+
+ /**
+ * This is temporary only and will be deprecated soon in favor of
+ * Theory::collectModelValues.
+ */
+ virtual bool collectModelInfo(TheoryModel* m) = 0;
+
+ virtual std::string identify() const = 0;
+
+ virtual Theory::PPAssertStatus ppAssert(
+ TNode in, SubstitutionMap& outSubstitutions) = 0;
+
+ virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); };
+
+ virtual void ppStaticLearn(TNode in, NodeBuilder<>& learned){};
+
+ virtual void presolve(){};
+
+ virtual void notifySharedTerm(TNode t) = 0;
+
+ virtual EqualityStatus getEqualityStatus(TNode a, TNode b)
+ {
+ return EqualityStatus::EQUALITY_UNKNOWN;
+ }
+
+ /** Called by abstraction preprocessing pass. */
+ virtual bool applyAbstraction(const std::vector<Node>& assertions,
+ std::vector<Node>& new_assertions) = 0;
+
+ protected:
+ TheoryState& d_state;
+ TheoryInferenceManager& d_inferManager;
+};
+
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__BV__BV_SOLVER_H */
--- /dev/null
+/********************* */
+/*! \file theory_bv_lazy.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Andrew Reynolds, Aina Niemetz
+ ** 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.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "theory/bv/bv_solver_lazy.h"
+
+#include "expr/node_algorithm.h"
+#include "options/bv_options.h"
+#include "options/smt_options.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/bv/abstraction.h"
+#include "theory/bv/bv_eager_solver.h"
+#include "theory/bv/bv_subtheory_algebraic.h"
+#include "theory/bv/bv_subtheory_bitblast.h"
+#include "theory/bv/bv_subtheory_core.h"
+#include "theory/bv/bv_subtheory_inequality.h"
+#include "theory/bv/theory_bv_rewrite_rules_normalization.h"
+#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
+#include "theory/bv/theory_bv_rewriter.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/theory_model.h"
+
+using namespace CVC4::theory::bv::utils;
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+BVSolverLazy::BVSolverLazy(TheoryBV& bv,
+ context::Context* c,
+ context::UserContext* u,
+ ProofNodeManager* pnm,
+ std::string name)
+ : BVSolver(bv.d_state, bv.d_inferMgr),
+ d_bv(bv),
+ d_context(c),
+ d_alreadyPropagatedSet(c),
+ d_sharedTermsSet(c),
+ d_subtheories(),
+ d_subtheoryMap(),
+ d_statistics(),
+ d_staticLearnCache(),
+ d_lemmasAdded(c, false),
+ d_conflict(c, false),
+ d_invalidateModelCache(c, true),
+ d_literalsToPropagate(c),
+ d_literalsToPropagateIndex(c, 0),
+ d_propagatedBy(c),
+ d_eagerSolver(),
+ d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
+ d_calledPreregister(false)
+{
+ if (options::bitblastMode() == options::BitblastMode::EAGER)
+ {
+ d_eagerSolver.reset(new EagerBitblastSolver(c, this));
+ return;
+ }
+
+ if (options::bitvectorEqualitySolver())
+ {
+ d_subtheories.emplace_back(new CoreSolver(c, this));
+ d_subtheoryMap[SUB_CORE] = d_subtheories.back().get();
+ }
+
+ if (options::bitvectorInequalitySolver())
+ {
+ d_subtheories.emplace_back(new InequalitySolver(c, u, this));
+ d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get();
+ }
+
+ if (options::bitvectorAlgebraicSolver())
+ {
+ d_subtheories.emplace_back(new AlgebraicSolver(c, this));
+ d_subtheoryMap[SUB_ALGEBRAIC] = d_subtheories.back().get();
+ }
+
+ BitblastSolver* bb_solver = new BitblastSolver(c, this);
+ if (options::bvAbstraction())
+ {
+ bb_solver->setAbstraction(d_abstractionModule.get());
+ }
+ d_subtheories.emplace_back(bb_solver);
+ d_subtheoryMap[SUB_BITBLAST] = bb_solver;
+}
+
+BVSolverLazy::~BVSolverLazy() {}
+
+bool BVSolverLazy::needsEqualityEngine(EeSetupInfo& esi)
+{
+ CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+ if (core)
+ {
+ return core->needsEqualityEngine(esi);
+ }
+ // otherwise we don't use an equality engine
+ return false;
+}
+
+void BVSolverLazy::finishInit()
+{
+ CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+ if (core)
+ {
+ // must finish initialization in the core solver
+ core->finishInit();
+ }
+}
+
+void BVSolverLazy::spendResource(ResourceManager::Resource r)
+{
+ d_inferManager.spendResource(r);
+}
+
+BVSolverLazy::Statistics::Statistics()
+ : d_avgConflictSize("theory::bv::lazy::AvgBVConflictSize"),
+ d_solveSubstitutions("theory::bv::lazy::NumSolveSubstitutions", 0),
+ d_solveTimer("theory::bv::lazy::solveTimer"),
+ d_numCallsToCheckFullEffort("theory::bv::lazy::NumFullCheckCalls", 0),
+ d_numCallsToCheckStandardEffort("theory::bv::lazy::NumStandardCheckCalls",
+ 0),
+ d_weightComputationTimer("theory::bv::lazy::weightComputationTimer"),
+ d_numMultSlice("theory::bv::lazy::NumMultSliceApplied", 0)
+{
+ smtStatisticsRegistry()->registerStat(&d_avgConflictSize);
+ smtStatisticsRegistry()->registerStat(&d_solveSubstitutions);
+ smtStatisticsRegistry()->registerStat(&d_solveTimer);
+ smtStatisticsRegistry()->registerStat(&d_numCallsToCheckFullEffort);
+ smtStatisticsRegistry()->registerStat(&d_numCallsToCheckStandardEffort);
+ smtStatisticsRegistry()->registerStat(&d_weightComputationTimer);
+ smtStatisticsRegistry()->registerStat(&d_numMultSlice);
+}
+
+BVSolverLazy::Statistics::~Statistics()
+{
+ smtStatisticsRegistry()->unregisterStat(&d_avgConflictSize);
+ smtStatisticsRegistry()->unregisterStat(&d_solveSubstitutions);
+ smtStatisticsRegistry()->unregisterStat(&d_solveTimer);
+ smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckFullEffort);
+ smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckStandardEffort);
+ smtStatisticsRegistry()->unregisterStat(&d_weightComputationTimer);
+ smtStatisticsRegistry()->unregisterStat(&d_numMultSlice);
+}
+
+void BVSolverLazy::preRegisterTerm(TNode node)
+{
+ d_calledPreregister = true;
+ Debug("bitvector-preregister")
+ << "BVSolverLazy::preRegister(" << node << ")" << std::endl;
+
+ if (options::bitblastMode() == options::BitblastMode::EAGER)
+ {
+ // the aig bit-blaster option is set heuristically
+ // if bv abstraction is used
+ if (!d_eagerSolver->isInitialized())
+ {
+ d_eagerSolver->initialize();
+ }
+
+ if (node.getKind() == kind::BITVECTOR_EAGER_ATOM)
+ {
+ Node formula = node[0];
+ d_eagerSolver->assertFormula(formula);
+ }
+ return;
+ }
+
+ for (unsigned i = 0; i < d_subtheories.size(); ++i)
+ {
+ d_subtheories[i]->preRegister(node);
+ }
+
+ // AJR : equality solver currently registers all terms to ExtTheory, if we
+ // want a lazy reduction without the bv equality solver, need to call this
+ // d_bv.d_extTheory->registerTermRec( node );
+}
+
+void BVSolverLazy::sendConflict()
+{
+ Assert(d_conflict);
+ if (d_conflictNode.isNull())
+ {
+ return;
+ }
+ else
+ {
+ Debug("bitvector") << indent() << "BVSolverLazy::check(): conflict "
+ << d_conflictNode << std::endl;
+ d_inferManager.conflict(d_conflictNode);
+ d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
+ d_conflictNode = Node::null();
+ }
+}
+
+void BVSolverLazy::checkForLemma(TNode fact)
+{
+ if (fact.getKind() == kind::EQUAL)
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL)
+ {
+ TNode urem = fact[0];
+ TNode result = fact[1];
+ TNode divisor = urem[1];
+ Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
+ Node divisor_eq_0 =
+ nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
+ Node split = nm->mkNode(
+ kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
+ lemma(split);
+ }
+ if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL)
+ {
+ TNode urem = fact[1];
+ TNode result = fact[0];
+ TNode divisor = urem[1];
+ Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
+ Node divisor_eq_0 =
+ nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
+ Node split = nm->mkNode(
+ kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
+ lemma(split);
+ }
+ }
+}
+
+bool BVSolverLazy::preCheck(Theory::Effort e)
+{
+ check(e);
+ return true;
+}
+
+void BVSolverLazy::check(Theory::Effort e)
+{
+ if (done() && e < Theory::EFFORT_FULL)
+ {
+ return;
+ }
+
+ // last call : do reductions on extended bitvector functions
+ if (e == Theory::EFFORT_LAST_CALL)
+ {
+ CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+ if (core)
+ {
+ // check extended functions at last call effort
+ core->checkExtf(e);
+ }
+ return;
+ }
+
+ Debug("bitvector") << "BVSolverLazy::check(" << e << ")" << std::endl;
+ TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
+ // we may be getting new assertions so the model cache may not be sound
+ d_invalidateModelCache.set(true);
+ // if we are using the eager solver
+ if (options::bitblastMode() == options::BitblastMode::EAGER)
+ {
+ // this can only happen on an empty benchmark
+ if (!d_eagerSolver->isInitialized())
+ {
+ d_eagerSolver->initialize();
+ }
+ if (!Theory::fullEffort(e)) return;
+
+ std::vector<TNode> assertions;
+ while (!done())
+ {
+ TNode fact = get().d_assertion;
+ Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
+ assertions.push_back(fact);
+ d_eagerSolver->assertFormula(fact[0]);
+ }
+
+ bool ok = d_eagerSolver->checkSat();
+ if (!ok)
+ {
+ if (assertions.size() == 1)
+ {
+ d_inferManager.conflict(assertions[0]);
+ return;
+ }
+ Node conflict = utils::mkAnd(assertions);
+ d_inferManager.conflict(conflict);
+ return;
+ }
+ return;
+ }
+
+ if (Theory::fullEffort(e))
+ {
+ ++(d_statistics.d_numCallsToCheckFullEffort);
+ }
+ else
+ {
+ ++(d_statistics.d_numCallsToCheckStandardEffort);
+ }
+ // if we are already in conflict just return the conflict
+ if (inConflict())
+ {
+ sendConflict();
+ return;
+ }
+
+ while (!done())
+ {
+ TNode fact = get().d_assertion;
+
+ checkForLemma(fact);
+
+ for (unsigned i = 0; i < d_subtheories.size(); ++i)
+ {
+ d_subtheories[i]->assertFact(fact);
+ }
+ }
+
+ bool ok = true;
+ bool complete = false;
+ for (unsigned i = 0; i < d_subtheories.size(); ++i)
+ {
+ Assert(!inConflict());
+ ok = d_subtheories[i]->check(e);
+ complete = d_subtheories[i]->isComplete();
+
+ if (!ok)
+ {
+ // if we are in a conflict no need to check with other theories
+ Assert(inConflict());
+ sendConflict();
+ return;
+ }
+ if (complete)
+ {
+ // if the last subtheory was complete we stop
+ break;
+ }
+ }
+
+ // check extended functions
+ if (Theory::fullEffort(e))
+ {
+ CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+ if (core)
+ {
+ // check extended functions at full effort
+ core->checkExtf(e);
+ }
+ }
+}
+
+bool BVSolverLazy::needsCheckLastEffort()
+{
+ CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+ if (core)
+ {
+ return core->needsCheckLastEffort();
+ }
+ return false;
+}
+
+bool BVSolverLazy::collectModelInfo(TheoryModel* m)
+{
+ Assert(!inConflict());
+ if (options::bitblastMode() == options::BitblastMode::EAGER)
+ {
+ if (!d_eagerSolver->collectModelInfo(m, true))
+ {
+ return false;
+ }
+ }
+ for (unsigned i = 0; i < d_subtheories.size(); ++i)
+ {
+ if (d_subtheories[i]->isComplete())
+ {
+ return d_subtheories[i]->collectModelInfo(m, true);
+ }
+ }
+ return true;
+}
+
+Node BVSolverLazy::getModelValue(TNode var)
+{
+ Assert(!inConflict());
+ for (unsigned i = 0; i < d_subtheories.size(); ++i)
+ {
+ if (d_subtheories[i]->isComplete())
+ {
+ return d_subtheories[i]->getModelValue(var);
+ }
+ }
+ Unreachable();
+}
+
+void BVSolverLazy::propagate(Theory::Effort e)
+{
+ Debug("bitvector") << indent() << "BVSolverLazy::propagate()" << std::endl;
+ if (options::bitblastMode() == options::BitblastMode::EAGER)
+ {
+ return;
+ }
+
+ if (inConflict())
+ {
+ return;
+ }
+
+ // go through stored propagations
+ bool ok = true;
+ for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok;
+ d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1)
+ {
+ TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
+ // temporary fix for incremental bit-blasting
+ if (d_state.isSatLiteral(literal))
+ {
+ Debug("bitvector::propagate")
+ << "BVSolverLazy:: propagating " << literal << "\n";
+ ok = d_inferManager.propagateLit(literal);
+ }
+ }
+
+ if (!ok)
+ {
+ Debug("bitvector::propagate")
+ << indent() << "BVSolverLazy::propagate(): conflict from theory engine"
+ << std::endl;
+ setConflict();
+ }
+}
+
+Theory::PPAssertStatus BVSolverLazy::ppAssert(TNode in,
+ SubstitutionMap& outSubstitutions)
+{
+ switch (in.getKind())
+ {
+ case kind::EQUAL:
+ {
+ if (in[0].isVar() && d_bv.isLegalElimination(in[0], in[1]))
+ {
+ ++(d_statistics.d_solveSubstitutions);
+ outSubstitutions.addSubstitution(in[0], in[1]);
+ return Theory::PP_ASSERT_STATUS_SOLVED;
+ }
+ if (in[1].isVar() && d_bv.isLegalElimination(in[1], in[0]))
+ {
+ ++(d_statistics.d_solveSubstitutions);
+ outSubstitutions.addSubstitution(in[1], in[0]);
+ 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.addSubstitution(extract[0], concat);
+ 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";
+ Node res = t;
+ if (options::bitwiseEq() && RewriteRule<BitwiseEq>::applies(t))
+ {
+ Node result = RewriteRule<BitwiseEq>::run<false>(t);
+ res = Rewriter::rewrite(result);
+ }
+ else if (RewriteRule<UltPlusOne>::applies(t))
+ {
+ Node result = RewriteRule<UltPlusOne>::run<false>(t);
+ res = Rewriter::rewrite(result);
+ }
+ else if (res.getKind() == kind::EQUAL
+ && ((res[0].getKind() == kind::BITVECTOR_PLUS
+ && RewriteRule<ConcatToMult>::applies(res[1]))
+ || (res[1].getKind() == kind::BITVECTOR_PLUS
+ && RewriteRule<ConcatToMult>::applies(res[0]))))
+ {
+ Node mult = RewriteRule<ConcatToMult>::applies(res[0])
+ ? RewriteRule<ConcatToMult>::run<false>(res[0])
+ : RewriteRule<ConcatToMult>::run<true>(res[1]);
+ Node factor = mult[0];
+ Node sum = RewriteRule<ConcatToMult>::applies(res[0]) ? res[1] : res[0];
+ Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult);
+ Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq);
+ if (rewr_eq[0].isVar() || rewr_eq[1].isVar())
+ {
+ res = Rewriter::rewrite(rewr_eq);
+ }
+ else
+ {
+ res = t;
+ }
+ }
+ else if (RewriteRule<SignExtendEqConst>::applies(t))
+ {
+ res = RewriteRule<SignExtendEqConst>::run<false>(t);
+ }
+ else if (RewriteRule<ZeroExtendEqConst>::applies(t))
+ {
+ res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
+ }
+ else if (RewriteRule<NormalizeEqPlusNeg>::applies(t))
+ {
+ res = RewriteRule<NormalizeEqPlusNeg>::run<false>(t);
+ }
+
+ // if(t.getKind() == kind::EQUAL &&
+ // ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() ==
+ // kind::BITVECTOR_PLUS) ||
+ // (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() ==
+ // kind::BITVECTOR_PLUS))) {
+ // // if we have an equality between a multiplication and addition
+ // // try to express multiplication in terms of addition
+ // Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1];
+ // Node add = t[0].getKind() == kind::BITVECTOR_PLUS? t[0] : t[1];
+ // if (RewriteRule<MultSlice>::applies(mult)) {
+ // Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
+ // Node new_eq =
+ // Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL,
+ // new_mult, add));
+
+ // // the simplification can cause the formula to blow up
+ // // only apply if formula reduced
+ // if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) {
+ // BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST];
+ // uint64_t old_size = bv->computeAtomWeight(t);
+ // Assert (old_size);
+ // uint64_t new_size = bv->computeAtomWeight(new_eq);
+ // double ratio = ((double)new_size)/old_size;
+ // if (ratio <= 0.4) {
+ // ++(d_statistics.d_numMultSlice);
+ // return new_eq;
+ // }
+ // }
+
+ // if (new_eq.getKind() == kind::CONST_BOOLEAN) {
+ // ++(d_statistics.d_numMultSlice);
+ // return new_eq;
+ // }
+ // }
+ // }
+
+ if (options::bvAbstraction() && t.getType().isBoolean())
+ {
+ d_abstractionModule->addInputAtom(res);
+ }
+ Debug("bv-pp-rewrite") << "to " << res << "\n";
+ if (res != t)
+ {
+ return TrustNode::mkTrustRewrite(t, res, nullptr);
+ }
+ return TrustNode::null();
+}
+
+void BVSolverLazy::presolve()
+{
+ Debug("bitvector") << "BVSolverLazy::presolve" << std::endl;
+}
+
+static int prop_count = 0;
+
+bool BVSolverLazy::storePropagation(TNode literal, SubTheory subtheory)
+{
+ Debug("bitvector::propagate") << indent() << d_context->getLevel() << " "
+ << "BVSolverLazy::storePropagation(" << literal
+ << ", " << subtheory << ")" << std::endl;
+ prop_count++;
+
+ // If already in conflict, no more propagation
+ if (d_conflict)
+ {
+ Debug("bitvector::propagate")
+ << indent() << "BVSolverLazy::storePropagation(" << literal << ", "
+ << subtheory << "): already in conflict" << std::endl;
+ return false;
+ }
+
+ // If propagated already, just skip
+ PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
+ if (find != d_propagatedBy.end())
+ {
+ return true;
+ }
+ else
+ {
+ bool polarity = literal.getKind() != kind::NOT;
+ Node negatedLiteral = polarity ? literal.notNode() : (Node)literal[0];
+ find = d_propagatedBy.find(negatedLiteral);
+ if (find != d_propagatedBy.end() && (*find).second != subtheory)
+ {
+ // Safe to ignore this one, subtheory should produce a conflict
+ return true;
+ }
+
+ d_propagatedBy[literal] = subtheory;
+ }
+
+ // Propagate differs depending on the subtheory
+ // * bitblaster needs to be left alone until it's done, otherwise it doesn't
+ // know how to explain
+ // * equality engine can propagate eagerly
+ // TODO(2348): Determine if ok should be set by propagate. If not, remove ok.
+ constexpr bool ok = true;
+ if (subtheory == SUB_CORE)
+ {
+ d_inferManager.propagateLit(literal);
+ if (!ok)
+ {
+ setConflict();
+ }
+ }
+ else
+ {
+ d_literalsToPropagate.push_back(literal);
+ }
+ return ok;
+
+} /* BVSolverLazy::propagate(TNode) */
+
+void BVSolverLazy::explain(TNode literal, std::vector<TNode>& assumptions)
+{
+ Assert(wasPropagatedBySubtheory(literal));
+ SubTheory sub = getPropagatingSubtheory(literal);
+ d_subtheoryMap[sub]->explain(literal, assumptions);
+}
+
+TrustNode BVSolverLazy::explain(TNode node)
+{
+ Debug("bitvector::explain")
+ << "BVSolverLazy::explain(" << node << ")" << std::endl;
+ std::vector<TNode> assumptions;
+
+ // Ask for the explanation
+ explain(node, assumptions);
+ // this means that it is something true at level 0
+ Node explanation;
+ if (assumptions.size() == 0)
+ {
+ explanation = utils::mkTrue();
+ }
+ else
+ {
+ // return the explanation
+ explanation = utils::mkAnd(assumptions);
+ }
+ Debug("bitvector::explain") << "BVSolverLazy::explain(" << node << ") => "
+ << explanation << std::endl;
+ Debug("bitvector::explain") << "BVSolverLazy::explain done. \n";
+ return TrustNode::mkTrustPropExp(node, explanation, nullptr);
+}
+
+void BVSolverLazy::notifySharedTerm(TNode t)
+{
+ Debug("bitvector::sharing")
+ << indent() << "BVSolverLazy::notifySharedTerm(" << t << ")" << std::endl;
+ d_sharedTermsSet.insert(t);
+ if (options::bitvectorEqualitySolver())
+ {
+ for (unsigned i = 0; i < d_subtheories.size(); ++i)
+ {
+ d_subtheories[i]->addSharedTerm(t);
+ }
+ }
+}
+
+EqualityStatus BVSolverLazy::getEqualityStatus(TNode a, TNode b)
+{
+ if (options::bitblastMode() == options::BitblastMode::EAGER)
+ return EQUALITY_UNKNOWN;
+ Assert(options::bitblastMode() == options::BitblastMode::LAZY);
+ for (unsigned i = 0; i < d_subtheories.size(); ++i)
+ {
+ EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
+ if (status != EQUALITY_UNKNOWN)
+ {
+ return status;
+ }
+ }
+ return EQUALITY_UNKNOWN;
+ ;
+}
+
+void BVSolverLazy::ppStaticLearn(TNode in, NodeBuilder<>& learned)
+{
+ if (d_staticLearnCache.find(in) != d_staticLearnCache.end())
+ {
+ return;
+ }
+ d_staticLearnCache.insert(in);
+
+ if (in.getKind() == kind::EQUAL)
+ {
+ if ((in[0].getKind() == kind::BITVECTOR_PLUS
+ && in[1].getKind() == kind::BITVECTOR_SHL)
+ || (in[1].getKind() == kind::BITVECTOR_PLUS
+ && in[0].getKind() == kind::BITVECTOR_SHL))
+ {
+ TNode p = in[0].getKind() == kind::BITVECTOR_PLUS ? in[0] : in[1];
+ TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0];
+
+ if (p.getNumChildren() == 2 && p[0].getKind() == kind::BITVECTOR_SHL
+ && p[1].getKind() == kind::BITVECTOR_SHL)
+ {
+ unsigned size = utils::getSize(s);
+ Node one = utils::mkConst(size, 1u);
+ if (s[0] == one && p[0][0] == one && p[1][0] == one)
+ {
+ Node zero = utils::mkConst(size, 0u);
+ TNode b = p[0];
+ TNode c = p[1];
+ // (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
+ Node b_eq_0 = b.eqNode(zero);
+ Node c_eq_0 = c.eqNode(zero);
+ Node b_eq_c = b.eqNode(c);
+
+ Node dis = NodeManager::currentNM()->mkNode(
+ kind::OR, b_eq_0, c_eq_0, b_eq_c);
+ Node imp = in.impNode(dis);
+ learned << imp;
+ }
+ }
+ }
+ }
+ else if (in.getKind() == kind::AND)
+ {
+ for (size_t i = 0, N = in.getNumChildren(); i < N; ++i)
+ {
+ ppStaticLearn(in[i], learned);
+ }
+ }
+}
+
+bool BVSolverLazy::applyAbstraction(const std::vector<Node>& assertions,
+ std::vector<Node>& new_assertions)
+{
+ bool changed =
+ d_abstractionModule->applyAbstraction(assertions, new_assertions);
+ if (changed && options::bitblastMode() == options::BitblastMode::EAGER
+ && options::bitvectorAig())
+ {
+ // disable AIG mode
+ AlwaysAssert(!d_eagerSolver->isInitialized());
+ d_eagerSolver->turnOffAig();
+ d_eagerSolver->initialize();
+ }
+ return changed;
+}
+
+void BVSolverLazy::setConflict(Node conflict)
+{
+ if (options::bvAbstraction())
+ {
+ NodeManager* const nm = NodeManager::currentNM();
+ Node new_conflict = d_abstractionModule->simplifyConflict(conflict);
+
+ std::vector<Node> lemmas;
+ lemmas.push_back(new_conflict);
+ d_abstractionModule->generalizeConflict(new_conflict, lemmas);
+ for (unsigned i = 0; i < lemmas.size(); ++i)
+ {
+ lemma(nm->mkNode(kind::NOT, lemmas[i]));
+ }
+ }
+ d_conflict = true;
+ d_conflictNode = conflict;
+}
+
+} // namespace bv
+} // namespace theory
+} /* namespace CVC4 */
--- /dev/null
+/********************* */
+/*! \file bv_solver_lazy.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Andrew Reynolds, Tim King
+ ** 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.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Lazy bit-vector solver.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BV__BV_SOLVER_LAZY_H
+#define CVC4__THEORY__BV__BV_SOLVER_LAZY_H
+
+#include <unordered_map>
+#include <unordered_set>
+
+#include "context/cdhashset.h"
+#include "context/cdlist.h"
+#include "context/context.h"
+#include "theory/bv/bv_solver.h"
+#include "theory/bv/bv_subtheory.h"
+#include "theory/bv/theory_bv.h"
+#include "util/hash.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class CoreSolver;
+class InequalitySolver;
+class AlgebraicSolver;
+class BitblastSolver;
+class EagerBitblastSolver;
+class AbstractionModule;
+
+class BVSolverLazy : public BVSolver
+{
+ /** Back reference to TheoryBV */
+ TheoryBV& d_bv;
+
+ /** The context we are using */
+ context::Context* d_context;
+
+ /** Context dependent set of atoms we already propagated */
+ context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
+ context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
+
+ std::vector<std::unique_ptr<SubtheorySolver>> d_subtheories;
+ std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int>>
+ d_subtheoryMap;
+
+ public:
+ BVSolverLazy(TheoryBV& bv,
+ context::Context* c,
+ context::UserContext* u,
+ ProofNodeManager* pnm = nullptr,
+ std::string name = "");
+
+ ~BVSolverLazy();
+
+ //--------------------------------- initialization
+
+ /**
+ * Returns true if we need an equality engine. If so, we initialize the
+ * information regarding how it should be setup. For details, see the
+ * documentation in Theory::needsEqualityEngine.
+ */
+ bool needsEqualityEngine(EeSetupInfo& esi) override;
+
+ /** finish initialization */
+ void finishInit() override;
+ //--------------------------------- end initialization
+
+ void preRegisterTerm(TNode n) override;
+
+ bool preCheck(Theory::Effort e) override;
+
+ bool needsCheckLastEffort() override;
+
+ void propagate(Theory::Effort e) override;
+
+ TrustNode explain(TNode n) override;
+
+ bool collectModelInfo(TheoryModel* m) override;
+
+ std::string identify() const override { return std::string("BVSolverLazy"); }
+
+ Theory::PPAssertStatus ppAssert(TNode in,
+ SubstitutionMap& outSubstitutions) override;
+
+ TrustNode ppRewrite(TNode t) override;
+
+ void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
+
+ void presolve() override;
+
+ bool applyAbstraction(const std::vector<Node>& assertions,
+ std::vector<Node>& new_assertions) override;
+
+ bool isLeaf(TNode node) { return d_bv.isLeaf(node); }
+
+ private:
+ class Statistics
+ {
+ public:
+ AverageStat d_avgConflictSize;
+ IntStat d_solveSubstitutions;
+ TimerStat d_solveTimer;
+ IntStat d_numCallsToCheckFullEffort;
+ IntStat d_numCallsToCheckStandardEffort;
+ TimerStat d_weightComputationTimer;
+ IntStat d_numMultSlice;
+ Statistics();
+ ~Statistics();
+ };
+
+ Statistics d_statistics;
+
+ void check(Theory::Effort e);
+ void spendResource(ResourceManager::Resource r);
+
+ typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+ typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+ NodeSet d_staticLearnCache;
+
+ typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode;
+
+ context::CDO<bool> d_lemmasAdded;
+
+ // Are we in conflict?
+ context::CDO<bool> d_conflict;
+
+ // Invalidate the model cache if check was called
+ context::CDO<bool> d_invalidateModelCache;
+
+ /** The conflict node */
+ Node d_conflictNode;
+
+ /** Literals to propagate */
+ context::CDList<Node> d_literalsToPropagate;
+
+ /** Index of the next literal to propagate */
+ context::CDO<unsigned> d_literalsToPropagateIndex;
+
+ /**
+ * Keeps a map from nodes to the subtheory that propagated it so that we can
+ * explain it properly.
+ */
+ typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap;
+ PropagatedMap d_propagatedBy;
+
+ std::unique_ptr<EagerBitblastSolver> d_eagerSolver;
+ std::unique_ptr<AbstractionModule> d_abstractionModule;
+ bool d_calledPreregister;
+
+ bool wasPropagatedBySubtheory(TNode literal) const
+ {
+ return d_propagatedBy.find(literal) != d_propagatedBy.end();
+ }
+
+ SubTheory getPropagatingSubtheory(TNode literal) const
+ {
+ Assert(wasPropagatedBySubtheory(literal));
+ PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
+ return (*find).second;
+ }
+
+ /** Should be called to propagate the literal. */
+ bool storePropagation(TNode literal, SubTheory subtheory);
+
+ /**
+ * Explains why this literal (propagated by subtheory) is true by adding
+ * assumptions.
+ */
+ void explain(TNode literal, std::vector<TNode>& assumptions);
+
+ void notifySharedTerm(TNode t) override;
+
+ bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); }
+
+ EqualityStatus getEqualityStatus(TNode a, TNode b) override;
+
+ Node getModelValue(TNode var);
+
+ inline std::string indent()
+ {
+ std::string indentStr(d_context->getLevel(), ' ');
+ return indentStr;
+ }
+
+ void setConflict(Node conflict = Node::null());
+
+ bool inConflict() { return d_conflict; }
+
+ void sendConflict();
+
+ void lemma(TNode node)
+ {
+ d_inferManager.lemma(node);
+ d_lemmasAdded = true;
+ }
+
+ void checkForLemma(TNode node);
+
+ void computeAssertedTerms(std::set<Node>& termSet,
+ const std::set<Kind>& irrKinds,
+ bool includeShared) const
+ {
+ return d_bv.computeAssertedTerms(termSet, irrKinds, includeShared);
+ }
+
+ size_t numAssertions() { return d_bv.numAssertions(); }
+
+ theory::Assertion get() { return d_bv.get(); }
+
+ bool done() { return d_bv.done(); }
+
+ friend class LazyBitblaster;
+ friend class TLazyBitblaster;
+ friend class EagerBitblaster;
+ friend class BitblastSolver;
+ friend class EqualitySolver;
+ friend class CoreSolver;
+ friend class InequalitySolver;
+ friend class AlgebraicSolver;
+ friend class EagerBitblastSolver;
+}; /* class BVSolverLazy */
+
+} // namespace bv
+} // namespace theory
+
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__BV__BV_SOLVER_LAZY_H */
}
// forward declaration
-class TheoryBV;
+class BVSolverLazy;
using AssertionQueue = context::CDQueue<Node>;
*/
class SubtheorySolver {
public:
- SubtheorySolver(context::Context* c, TheoryBV* bv)
- : d_context(c),
- d_bv(bv),
- d_assertionQueue(c),
- d_assertionIndex(c, 0) {}
+ SubtheorySolver(context::Context* c, BVSolverLazy* bv)
+ : d_context(c), d_bv(bv), d_assertionQueue(c), d_assertionIndex(c, 0)
+ {
+ }
virtual ~SubtheorySolver() {}
virtual bool check(Theory::Effort e) = 0;
virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0;
context::Context* d_context;
/** The bit-vector theory */
- TheoryBV* d_bv;
+ BVSolverLazy* d_bv;
AssertionQueue d_assertionQueue;
context::CDO<uint32_t> d_assertionIndex;
}; /* class SubtheorySolver */
#include "smt/smt_statistics_registry.h"
#include "smt_util/boolean_simplification.h"
#include "theory/bv/bv_quick_check.h"
-#include "theory/bv/theory_bv.h"
+#include "theory/bv/bv_solver_lazy.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/theory_model.h"
d_cache[from] = SubstitutionElement(to, reason);
}
-AlgebraicSolver::AlgebraicSolver(context::Context* c, TheoryBV* bv)
+AlgebraicSolver::AlgebraicSolver(context::Context* c, BVSolverLazy* bv)
: SubtheorySolver(c, bv),
d_modelMap(),
d_quickSolver(new BVQuickCheck("theory::bv::algebraic", bv)),
Debug("bv-subtheory-algebraic") << " UNSAT: assertion simplfies to false with conflict: "<< conflict << "\n";
if (Dump.isOn("bv-algebraic")) {
- Dump("bv-algebraic") << EchoCommand("TheoryBV::AlgebraicSolver::conflict");
+ Dump("bv-algebraic")
+ << EchoCommand("BVSolverLazy::AlgebraicSolver::conflict");
Dump("bv-algebraic") << PushCommand();
Dump("bv-algebraic") << AssertCommand(conflict.toExpr());
Dump("bv-algebraic") << CheckSatCommand();
class AlgebraicSolver;
-
Node mergeExplanations(TNode expl1, TNode expl2);
Node mergeExplanations(const std::vector<Node>& expls);
-
/**
* Non-context dependent substitution with explanations.
- *
+ *
*/
-class SubstitutionEx {
- struct SubstitutionElement {
+class SubstitutionEx
+{
+ struct SubstitutionElement
+ {
Node to;
Node reason;
- SubstitutionElement()
- : to()
- , reason()
- {}
-
- SubstitutionElement(TNode t, TNode r)
- : to(t)
- , reason(r)
- {}
+ SubstitutionElement() : to(), reason() {}
+
+ SubstitutionElement(TNode t, TNode r) : to(t), reason(r) {}
};
- struct SubstitutionStackElement {
+ struct SubstitutionStackElement
+ {
TNode node;
bool childrenAdded;
SubstitutionStackElement(TNode n, bool ca = false)
- : node(n)
- , childrenAdded(ca)
- {}
+ : node(n), childrenAdded(ca)
+ {
+ }
};
- typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> Substitutions;
- typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> SubstitutionsCache;
+ typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction>
+ Substitutions;
+ typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction>
+ SubstitutionsCache;
Substitutions d_substitutions;
SubstitutionsCache d_cache;
bool d_cacheInvalid;
- theory::SubstitutionMap* d_modelMap;
+ theory::SubstitutionMap* d_modelMap;
-
Node getReason(TNode node) const;
bool hasCache(TNode node) const;
Node getCache(TNode node) const;
void storeCache(TNode from, TNode to, Node rason);
Node internalApply(TNode node);
-public:
+ public:
SubstitutionEx(theory::SubstitutionMap* modelMap);
- /**
- * Returnst true if the substitution map did not contain from.
- *
- * @param from
- * @param to
- * @param reason
- *
- * @return
+ /**
+ * Returnst true if the substitution map did not contain from.
+ *
+ * @param from
+ * @param to
+ * @param reason
+ *
+ * @return
*/
bool addSubstitution(TNode from, TNode to, TNode reason);
Node apply(TNode node);
/**
* In-processing worklist element, id keeps track of
- * original assertion.
- *
+ * original assertion.
+ *
*/
-struct WorklistElement {
+struct WorklistElement
+{
Node node;
unsigned id;
WorklistElement(Node n, unsigned i) : node(n), id(i) {}
WorklistElement() : node(), id(-1) {}
-};
-
+};
typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
typedef std::unordered_map<Node, unsigned, NodeHashFunction> NodeIdMap;
typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
-
-class ExtractSkolemizer {
- struct Extract {
+class ExtractSkolemizer
+{
+ struct Extract
+ {
unsigned high;
unsigned low;
Extract(unsigned h, unsigned l) : high(h), low(l) {}
};
-
- struct ExtractList {
+
+ struct ExtractList
+ {
Base base;
std::vector<Extract> extracts;
ExtractList(unsigned bitwidth) : base(bitwidth), extracts() {}
ExtractList() : base(1), extracts() {}
- void addExtract(Extract& e);
+ void addExtract(Extract& e);
};
- typedef std::unordered_map<Node, ExtractList, NodeHashFunction> VarExtractMap;
+ typedef std::unordered_map<Node, ExtractList, NodeHashFunction> VarExtractMap;
context::Context d_emptyContext;
VarExtractMap d_varToExtract;
theory::SubstitutionMap* d_modelMap;
Node unSkolemize(TNode);
Node mkSkolem(Node node);
-public:
- ExtractSkolemizer(theory::SubstitutionMap* modelMap);
+
+ public:
+ ExtractSkolemizer(theory::SubstitutionMap* modelMap);
void skolemize(std::vector<WorklistElement>&);
void unSkolemize(std::vector<WorklistElement>&);
~ExtractSkolemizer();
-};
+};
class BVQuickCheck;
class QuickXPlain;
/**
* AlgebraicSolver
*/
-class AlgebraicSolver : public SubtheorySolver {
-
- struct Statistics {
+class AlgebraicSolver : public SubtheorySolver
+{
+ struct Statistics
+ {
IntStat d_numCallstoCheck;
IntStat d_numSimplifiesToTrue;
IntStat d_numSimplifiesToFalse;
std::unique_ptr<SubstitutionMap> d_modelMap;
std::unique_ptr<BVQuickCheck> d_quickSolver;
- context::CDO<bool> d_isComplete;
- context::CDO<bool> d_isDifficult; /**< flag to indicate whether the current assertions contain expensive BV operators */
-
+ context::CDO<bool> d_isComplete;
+ context::CDO<bool>
+ d_isDifficult; /**< flag to indicate whether the current assertions
+ contain expensive BV operators */
+
unsigned long d_budget;
- std::vector<Node> d_explanations; /**< explanations for assertions indexed by assertion id */
- TNodeSet d_inputAssertions; /**< assertions in current context (for debugging purposes only) */
- NodeIdMap d_ids; /**< map from assertions to ids */
+ std::vector<Node> d_explanations; /**< explanations for assertions indexed by
+ assertion id */
+ TNodeSet d_inputAssertions; /**< assertions in current context (for debugging
+ purposes only) */
+ NodeIdMap d_ids; /**< map from assertions to ids */
uint64_t d_numSolved;
uint64_t d_numCalls;
bool checkExplanation(TNode expl);
void storeExplanation(TNode expl);
void storeExplanation(unsigned id, TNode expl);
- /**
+ /**
* Apply substitutions and rewriting to the worklist assertions to a fixpoint.
- * Subsitutions learned store in subst.
+ * Subsitutions learned store in subst.
*
- * @param worklist
- * @param subst
+ * @param worklist
+ * @param subst
*/
- void processAssertions(std::vector<WorklistElement>& worklist, SubstitutionEx& subst);
- /**
+ void processAssertions(std::vector<WorklistElement>& worklist,
+ SubstitutionEx& subst);
+ /**
* Attempt to solve the equation in fact, and if successful
- * add a substitution to subst.
- *
+ * add a substitution to subst.
+ *
* @param fact equation we are trying to solve
* @param reason the reason in terms of original assertions
* @param subst substitution map
- *
+ *
* @return true if added a substitution to subst
*/
bool solve(TNode fact, TNode reason, SubstitutionEx& subst);
- /**
+ /**
* Run a SAT solver on the given facts with the given budget.
- * Sets the isComplete flag and conflict accordingly.
- *
- * @param facts
- *
- * @return true if no conflict was detected.
+ * Sets the isComplete flag and conflict accordingly.
+ *
+ * @param facts
+ *
+ * @return true if no conflict was detected.
*/
bool quickCheck(std::vector<Node>& facts);
-public:
- AlgebraicSolver(context::Context* c, TheoryBV* bv);
+ public:
+ AlgebraicSolver(context::Context* c, BVSolverLazy* bv);
~AlgebraicSolver();
void preRegister(TNode node) override {}
**/
#include "theory/bv/bv_subtheory_bitblast.h"
+
#include "decision/decision_attributes.h"
#include "options/bv_options.h"
#include "options/decision_options.h"
#include "theory/bv/abstraction.h"
#include "theory/bv/bitblast/lazy_bitblaster.h"
#include "theory/bv/bv_quick_check.h"
-#include "theory/bv/theory_bv.h"
+#include "theory/bv/bv_solver_lazy.h"
#include "theory/bv/theory_bv_utils.h"
using namespace std;
namespace theory {
namespace bv {
-BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
+BitblastSolver::BitblastSolver(context::Context* c, BVSolverLazy* bv)
: SubtheorySolver(c, bv),
d_bitblaster(new TLazyBitblaster(c, bv, "theory::bv::lazy")),
d_bitblastQueue(c),
/**
* BitblastSolver
*/
-class BitblastSolver : public SubtheorySolver {
- struct Statistics {
+class BitblastSolver : public SubtheorySolver
+{
+ struct Statistics
+ {
IntStat d_numCallstoCheck;
IntStat d_numBBLemmas;
Statistics();
/** Queue for bit-blasting lemma atoms only in full check if we are sat */
context::CDQueue<TNode> d_lemmaAtomsQueue;
- bool d_useSatPropagation;
+ bool d_useSatPropagation;
AbstractionModule* d_abstractionModule;
std::unique_ptr<BVQuickCheck> d_quickCheck;
std::unique_ptr<QuickXPlain> d_quickXplain;
// Node getModelValueRec(TNode node);
void setConflict(TNode conflict);
-public:
- BitblastSolver(context::Context* c, TheoryBV* bv);
+
+ public:
+ BitblastSolver(context::Context* c, BVSolverLazy* bv);
~BitblastSolver();
void preRegister(TNode node) override;
uint64_t computeAtomWeight(TNode atom);
};
-} /* namespace CVC4::theory::bv */
-} /* namespace CVC4::theory */
+} // namespace bv
+} // namespace theory
} /* namespace CVC4 */
#include "options/bv_options.h"
#include "options/smt_options.h"
#include "smt/smt_statistics_registry.h"
-#include "theory/bv/theory_bv.h"
+#include "theory/bv/bv_solver_lazy.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/ext_theory.h"
#include "theory/theory_model.h"
return false;
}
-CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
+CoreSolver::CoreSolver(context::Context* c, BVSolverLazy* bv)
: SubtheorySolver(c, bv),
d_notify(*this),
d_isComplete(c, true),
d_bv(bv),
d_extTheoryCb(),
d_extTheory(new ExtTheory(d_extTheoryCb,
- bv->getSatContext(),
- bv->getUserContext(),
- bv->getOutputChannel())),
+ bv->d_bv.getSatContext(),
+ bv->d_bv.getUserContext(),
+ bv->d_bv.getOutputChannel())),
d_reasons(c),
d_needsLastCallCheck(false),
- d_extf_range_infer(bv->getUserContext()),
- d_extf_collapse_infer(bv->getUserContext())
+ d_extf_range_infer(bv->d_bv.getUserContext()),
+ d_extf_collapse_infer(bv->d_bv.getUserContext())
{
d_extTheory->addFunctionKind(kind::BITVECTOR_TO_NAT);
d_extTheory->addFunctionKind(kind::INT_TO_BITVECTOR);
void CoreSolver::finishInit()
{
// use the parent's equality engine, which may be the one we allocated above
- d_equalityEngine = d_bv->getEqualityEngine();
+ d_equalityEngine = d_bv->d_bv.getEqualityEngine();
// The kinds we are treating as function application in congruence
d_equalityEngine->addFunctionKind(kind::BITVECTOR_CONCAT, true);
bool CoreSolver::check(Theory::Effort e) {
Trace("bitvector::core") << "CoreSolver::check \n";
- d_bv->spendResource(ResourceManager::Resource::TheoryCheckStep);
+ d_bv->d_inferManager.spendResource(
+ ResourceManager::Resource::TheoryCheckStep);
d_checkCalled = true;
Assert(!d_bv->inConflict());
nm->mkNode(kind::LT, n, max));
Trace("bv-extf-lemma")
<< "BV extf lemma (range) : " << lem << std::endl;
- d_bv->getOutputChannel().lemma(lem);
+ d_bv->d_inferManager.lemma(lem);
sentLemma = true;
}
}
// (bv2nat ((_ int2bv w) x)) == x + k*2^w for some k
Trace("bv-extf-lemma")
<< "BV extf lemma (collapse) : " << lem << std::endl;
- d_bv->getOutputChannel().lemma(lem);
+ d_bv->d_inferManager.lemma(lem);
sentLemma = true;
}
}
bool d_checkCalled;
/** Pointer to the parent theory solver that owns this */
- TheoryBV* d_bv;
+ BVSolverLazy* d_bv;
/** Pointer to the equality engine of the parent */
eq::EqualityEngine* d_equalityEngine;
/** The extended theory callback */
bool doExtfReductions(std::vector<Node>& terms);
public:
- CoreSolver(context::Context* c, TheoryBV* bv);
+ CoreSolver(context::Context* c, BVSolverLazy* bv);
~CoreSolver();
bool needsEqualityEngine(EeSetupInfo& esi);
void finishInit();
#include "options/smt_options.h"
#include "smt/smt_statistics_registry.h"
-#include "theory/bv/theory_bv.h"
+#include "theory/bv/bv_solver_lazy.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/theory_model.h"
namespace bv {
/** Cache for InequalitySolver::isInequalityOnly() */
-struct IneqOnlyAttributeId {};
+struct IneqOnlyAttributeId
+{
+};
typedef expr::Attribute<IneqOnlyAttributeId, bool> IneqOnlyAttribute;
/** Whether the above has been computed yet or not for an expr */
-struct IneqOnlyComputedAttributeId {};
-typedef expr::Attribute<IneqOnlyComputedAttributeId, bool> IneqOnlyComputedAttribute;
+struct IneqOnlyComputedAttributeId
+{
+};
+typedef expr::Attribute<IneqOnlyComputedAttributeId, bool>
+ IneqOnlyComputedAttribute;
class InequalitySolver : public SubtheorySolver
{
bool isInequalityOnly(TNode node);
bool addInequality(TNode a, TNode b, bool strict, TNode fact);
Statistics d_statistics;
-public:
- InequalitySolver(context::Context* c, context::Context* u, TheoryBV* bv)
- : SubtheorySolver(c, bv),
- d_assertionSet(c),
- d_inequalityGraph(c, u),
- d_explanations(c),
- d_isComplete(c, true),
- d_ineqTerms(),
- d_statistics()
- {}
+
+ public:
+ InequalitySolver(context::Context* c, context::Context* u, BVSolverLazy* bv)
+ : SubtheorySolver(c, bv),
+ d_assertionSet(c),
+ d_inequalityGraph(c, u),
+ d_explanations(c),
+ d_isComplete(c, true),
+ d_ineqTerms(),
+ d_statistics()
+ {
+ }
bool check(Theory::Effort e) override;
void propagate(Theory::Effort e) override;
void preRegister(TNode node) override;
};
-}
-}
-}
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
#endif /* CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */
#include "theory/bv/theory_bv.h"
-#include "expr/node_algorithm.h"
#include "options/bv_options.h"
-#include "options/smt_options.h"
-#include "smt/smt_statistics_registry.h"
-#include "theory/bv/abstraction.h"
-#include "theory/bv/bv_eager_solver.h"
-#include "theory/bv/bv_subtheory_algebraic.h"
-#include "theory/bv/bv_subtheory_bitblast.h"
-#include "theory/bv/bv_subtheory_core.h"
-#include "theory/bv/bv_subtheory_inequality.h"
-#include "theory/bv/theory_bv_rewrite_rules_normalization.h"
-#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
-#include "theory/bv/theory_bv_rewriter.h"
+#include "theory/bv/bv_solver_lazy.h"
#include "theory/bv/theory_bv_utils.h"
-#include "theory/theory_model.h"
-#include "theory/valuation.h"
-
-using namespace CVC4::context;
-using namespace CVC4::theory::bv::utils;
-using namespace std;
namespace CVC4 {
namespace theory {
ProofNodeManager* pnm,
std::string name)
: Theory(THEORY_BV, c, u, out, valuation, logicInfo, pnm, name),
- d_context(c),
- d_alreadyPropagatedSet(c),
- d_sharedTermsSet(c),
- d_subtheories(),
- d_subtheoryMap(),
- d_statistics(),
- d_staticLearnCache(),
- d_BVDivByZero(),
- d_BVRemByZero(),
- d_lemmasAdded(c, false),
- d_conflict(c, false),
- d_invalidateModelCache(c, true),
- d_literalsToPropagate(c),
- d_literalsToPropagateIndex(c, 0),
- d_propagatedBy(c),
- d_eagerSolver(),
- d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
- d_calledPreregister(false),
- d_state(c, u, valuation)
-{
- if (options::bitblastMode() == options::BitblastMode::EAGER)
- {
- d_eagerSolver.reset(new EagerBitblastSolver(c, this));
- return;
- }
-
- if (options::bitvectorEqualitySolver())
- {
- d_subtheories.emplace_back(new CoreSolver(c, this));
- d_subtheoryMap[SUB_CORE] = d_subtheories.back().get();
- }
-
- if (options::bitvectorInequalitySolver())
- {
- d_subtheories.emplace_back(new InequalitySolver(c, u, this));
- d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get();
- }
-
- if (options::bitvectorAlgebraicSolver())
- {
- d_subtheories.emplace_back(new AlgebraicSolver(c, this));
- d_subtheoryMap[SUB_ALGEBRAIC] = d_subtheories.back().get();
- }
-
- BitblastSolver* bb_solver = new BitblastSolver(c, this);
- if (options::bvAbstraction())
- {
- bb_solver->setAbstraction(d_abstractionModule.get());
- }
- d_subtheories.emplace_back(bb_solver);
- d_subtheoryMap[SUB_BITBLAST] = bb_solver;
-
- // indicate we are using the default theory state object
+ d_internal(nullptr),
+ d_ufDivByZero(),
+ d_ufRemByZero(),
+ d_rewriter(),
+ d_state(c, u, valuation),
+ d_inferMgr(*this, d_state, pnm)
+{
+ d_internal.reset(new BVSolverLazy(*this, c, u, pnm, name));
d_theoryState = &d_state;
+ d_inferManager = &d_inferMgr;
}
TheoryBV::~TheoryBV() {}
bool TheoryBV::needsEqualityEngine(EeSetupInfo& esi)
{
- CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
- if (core)
- {
- return core->needsEqualityEngine(esi);
- }
- // otherwise we don't use an equality engine
- return false;
+ return d_internal->needsEqualityEngine(esi);
}
void TheoryBV::finishInit()
{
// these kinds are semi-evaluated in getModelValue (applications of this
// kind are treated as variables)
- d_valuation.setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
- d_valuation.setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
-
- CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
- if (core)
- {
- // must finish initialization in the core solver
- core->finishInit();
- }
-}
-
-void TheoryBV::spendResource(ResourceManager::Resource r)
-{
- getOutputChannel().spendResource(r);
+ getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
+ getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
+ d_internal->finishInit();
}
-TheoryBV::Statistics::Statistics():
- d_avgConflictSize("theory::bv::AvgBVConflictSize"),
- d_solveSubstitutions("theory::bv::NumSolveSubstitutions", 0),
- d_solveTimer("theory::bv::solveTimer"),
- d_numCallsToCheckFullEffort("theory::bv::NumFullCheckCalls", 0),
- d_numCallsToCheckStandardEffort("theory::bv::NumStandardCheckCalls", 0),
- d_weightComputationTimer("theory::bv::weightComputationTimer"),
- d_numMultSlice("theory::bv::NumMultSliceApplied", 0)
+Node TheoryBV::getUFDivByZero(Kind k, unsigned width)
{
- smtStatisticsRegistry()->registerStat(&d_avgConflictSize);
- smtStatisticsRegistry()->registerStat(&d_solveSubstitutions);
- smtStatisticsRegistry()->registerStat(&d_solveTimer);
- smtStatisticsRegistry()->registerStat(&d_numCallsToCheckFullEffort);
- smtStatisticsRegistry()->registerStat(&d_numCallsToCheckStandardEffort);
- smtStatisticsRegistry()->registerStat(&d_weightComputationTimer);
- smtStatisticsRegistry()->registerStat(&d_numMultSlice);
-}
-
-TheoryBV::Statistics::~Statistics() {
- smtStatisticsRegistry()->unregisterStat(&d_avgConflictSize);
- smtStatisticsRegistry()->unregisterStat(&d_solveSubstitutions);
- smtStatisticsRegistry()->unregisterStat(&d_solveTimer);
- smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckFullEffort);
- smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckStandardEffort);
- smtStatisticsRegistry()->unregisterStat(&d_weightComputationTimer);
- smtStatisticsRegistry()->unregisterStat(&d_numMultSlice);
-}
-
-Node TheoryBV::getBVDivByZero(Kind k, unsigned width) {
NodeManager* nm = NodeManager::currentNM();
- if (k == kind::BITVECTOR_UDIV) {
- if (d_BVDivByZero.find(width) == d_BVDivByZero.end()) {
+ if (k == kind::BITVECTOR_UDIV)
+ {
+ if (d_ufDivByZero.find(width) == d_ufDivByZero.end())
+ {
// lazily create the function symbols
- ostringstream os;
+ std::ostringstream os;
os << "BVUDivByZero_" << width;
- Node divByZero = nm->mkSkolem(os.str(),
- nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
- "partial bvudiv", NodeManager::SKOLEM_EXACT_NAME);
- d_BVDivByZero[width] = divByZero;
+ Node divByZero =
+ nm->mkSkolem(os.str(),
+ nm->mkFunctionType(nm->mkBitVectorType(width),
+ nm->mkBitVectorType(width)),
+ "partial bvudiv",
+ NodeManager::SKOLEM_EXACT_NAME);
+ d_ufDivByZero[width] = divByZero;
}
- return d_BVDivByZero[width];
+ return d_ufDivByZero[width];
}
- else if (k == kind::BITVECTOR_UREM) {
- if (d_BVRemByZero.find(width) == d_BVRemByZero.end()) {
- ostringstream os;
+ else if (k == kind::BITVECTOR_UREM)
+ {
+ if (d_ufRemByZero.find(width) == d_ufRemByZero.end())
+ {
+ std::ostringstream os;
os << "BVURemByZero_" << width;
- Node divByZero = nm->mkSkolem(os.str(),
- nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
- "partial bvurem", NodeManager::SKOLEM_EXACT_NAME);
- d_BVRemByZero[width] = divByZero;
+ Node divByZero =
+ nm->mkSkolem(os.str(),
+ nm->mkFunctionType(nm->mkBitVectorType(width),
+ nm->mkBitVectorType(width)),
+ "partial bvurem",
+ NodeManager::SKOLEM_EXACT_NAME);
+ d_ufRemByZero[width] = divByZero;
}
- return d_BVRemByZero[width];
+ return d_ufRemByZero[width];
}
Unreachable();
TrustNode TheoryBV::expandDefinition(Node node)
{
- Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
+ Debug("bitvector-expandDefinition")
+ << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
Node ret;
- switch (node.getKind()) {
- case kind::BITVECTOR_SDIV:
- case kind::BITVECTOR_SREM:
- case kind::BITVECTOR_SMOD:
- ret = TheoryBVRewriter::eliminateBVSDiv(node);
- break;
+ switch (node.getKind())
+ {
+ case kind::BITVECTOR_SDIV:
+ case kind::BITVECTOR_SREM:
+ case kind::BITVECTOR_SMOD:
+ ret = TheoryBVRewriter::eliminateBVSDiv(node);
+ break;
- case kind::BITVECTOR_UDIV:
- case kind::BITVECTOR_UREM: {
- NodeManager* nm = NodeManager::currentNM();
- unsigned width = node.getType().getBitVectorSize();
+ case kind::BITVECTOR_UDIV:
+ case kind::BITVECTOR_UREM:
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ unsigned width = node.getType().getBitVectorSize();
- if (options::bitvectorDivByZeroConst()) {
- Kind kind = node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UREM_TOTAL;
- ret = nm->mkNode(kind, node[0], node[1]);
- break;
- }
+ if (options::bitvectorDivByZeroConst())
+ {
+ Kind kind = node.getKind() == kind::BITVECTOR_UDIV
+ ? kind::BITVECTOR_UDIV_TOTAL
+ : kind::BITVECTOR_UREM_TOTAL;
+ ret = nm->mkNode(kind, node[0], node[1]);
+ break;
+ }
- TNode num = node[0], den = node[1];
- Node den_eq_0 = nm->mkNode(kind::EQUAL, den, utils::mkZero(width));
- Node divTotalNumDen = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV
- ? kind::BITVECTOR_UDIV_TOTAL
- : kind::BITVECTOR_UREM_TOTAL,
- num,
- den);
- Node divByZero = getBVDivByZero(node.getKind(), width);
- Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
- ret = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
- }
+ TNode num = node[0], den = node[1];
+ Node den_eq_0 = nm->mkNode(kind::EQUAL, den, utils::mkZero(width));
+ Node divTotalNumDen = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV
+ ? kind::BITVECTOR_UDIV_TOTAL
+ : kind::BITVECTOR_UREM_TOTAL,
+ num,
+ den);
+ Node divByZero = getUFDivByZero(node.getKind(), width);
+ Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
+ ret = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
+ }
break;
- default:
- break;
+ default: break;
}
if (!ret.isNull() && node != ret)
{
return TrustNode::null();
}
-void TheoryBV::preRegisterTerm(TNode node) {
- d_calledPreregister = true;
- Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
-
- if (options::bitblastMode() == options::BitblastMode::EAGER)
- {
- // the aig bit-blaster option is set heuristically
- // if bv abstraction is used
- if (!d_eagerSolver->isInitialized())
- {
- d_eagerSolver->initialize();
- }
-
- if (node.getKind() == kind::BITVECTOR_EAGER_ATOM)
- {
- Node formula = node[0];
- d_eagerSolver->assertFormula(formula);
- }
- return;
- }
-
- for (unsigned i = 0; i < d_subtheories.size(); ++i) {
- d_subtheories[i]->preRegister(node);
- }
-
- // AJR : equality solver currently registers all terms to ExtTheory, if we
- // want a lazy reduction without the bv equality solver, need to call this
- // d_extTheory->registerTermRec( node );
-}
-
-void TheoryBV::sendConflict() {
- Assert(d_conflict);
- if (d_conflictNode.isNull()) {
- return;
- } else {
- Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode << std::endl;
- d_out->conflict(d_conflictNode);
- d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
- d_conflictNode = Node::null();
- }
-}
-
-void TheoryBV::checkForLemma(TNode fact)
+void TheoryBV::preRegisterTerm(TNode node)
{
- if (fact.getKind() == kind::EQUAL)
- {
- NodeManager* nm = NodeManager::currentNM();
- if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL)
- {
- TNode urem = fact[0];
- TNode result = fact[1];
- TNode divisor = urem[1];
- Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
- Node divisor_eq_0 =
- nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
- Node split = nm->mkNode(
- kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
- lemma(split);
- }
- if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL)
- {
- TNode urem = fact[1];
- TNode result = fact[0];
- TNode divisor = urem[1];
- Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
- Node divisor_eq_0 =
- nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
- Node split = nm->mkNode(
- kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
- lemma(split);
- }
- }
+ d_internal->preRegisterTerm(node);
}
-void TheoryBV::check(Effort e)
-{
- if (done() && e<Theory::EFFORT_FULL) {
- return;
- }
-
- //last call : do reductions on extended bitvector functions
- if (e == Theory::EFFORT_LAST_CALL) {
- CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
- if (core)
- {
- // check extended functions at last call effort
- core->checkExtf(e);
- }
- return;
- }
-
- TimerStat::CodeTimer checkTimer(d_checkTime);
- Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
- TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
- // we may be getting new assertions so the model cache may not be sound
- d_invalidateModelCache.set(true);
- // if we are using the eager solver
- if (options::bitblastMode() == options::BitblastMode::EAGER)
- {
- // this can only happen on an empty benchmark
- if (!d_eagerSolver->isInitialized()) {
- d_eagerSolver->initialize();
- }
- if (!Theory::fullEffort(e))
- return;
-
- std::vector<TNode> assertions;
- while (!done()) {
- TNode fact = get().d_assertion;
- Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
- assertions.push_back(fact);
- d_eagerSolver->assertFormula(fact[0]);
- }
-
- bool ok = d_eagerSolver->checkSat();
- if (!ok) {
- if (assertions.size() == 1) {
- d_out->conflict(assertions[0]);
- return;
- }
- Node conflict = utils::mkAnd(assertions);
- d_out->conflict(conflict);
- return;
- }
- return;
- }
-
- if (Theory::fullEffort(e)) {
- ++(d_statistics.d_numCallsToCheckFullEffort);
- } else {
- ++(d_statistics.d_numCallsToCheckStandardEffort);
- }
- // if we are already in conflict just return the conflict
- if (inConflict()) {
- sendConflict();
- return;
- }
-
- while (!done()) {
- TNode fact = get().d_assertion;
-
- checkForLemma(fact);
-
- for (unsigned i = 0; i < d_subtheories.size(); ++i) {
- d_subtheories[i]->assertFact(fact);
- }
- }
-
- bool ok = true;
- bool complete = false;
- for (unsigned i = 0; i < d_subtheories.size(); ++i) {
- Assert(!inConflict());
- ok = d_subtheories[i]->check(e);
- complete = d_subtheories[i]->isComplete();
-
- if (!ok) {
- // if we are in a conflict no need to check with other theories
- Assert(inConflict());
- sendConflict();
- return;
- }
- if (complete) {
- // if the last subtheory was complete we stop
- break;
- }
- }
-
- //check extended functions
- if (Theory::fullEffort(e)) {
- CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
- if (core)
- {
- // check extended functions at full effort
- core->checkExtf(e);
- }
- }
-}
+bool TheoryBV::preCheck(Effort e) { return d_internal->preCheck(e); }
bool TheoryBV::needsCheckLastEffort()
{
- CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
- if (core)
- {
- return core->needsCheckLastEffort();
- }
- return false;
+ return d_internal->needsCheckLastEffort();
}
+
bool TheoryBV::collectModelInfo(TheoryModel* m)
{
- Assert(!inConflict());
- if (options::bitblastMode() == options::BitblastMode::EAGER)
- {
- if (!d_eagerSolver->collectModelInfo(m, true))
- {
- return false;
- }
- }
- for (unsigned i = 0; i < d_subtheories.size(); ++i) {
- if (d_subtheories[i]->isComplete()) {
- return d_subtheories[i]->collectModelInfo(m, true);
- }
- }
- return true;
+ return d_internal->collectModelInfo(m);
}
-Node TheoryBV::getModelValue(TNode var) {
- Assert(!inConflict());
- for (unsigned i = 0; i < d_subtheories.size(); ++i) {
- if (d_subtheories[i]->isComplete()) {
- return d_subtheories[i]->getModelValue(var);
- }
- }
- Unreachable();
-}
-
-void TheoryBV::propagate(Effort e) {
- Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
- if (options::bitblastMode() == options::BitblastMode::EAGER)
- {
- return;
- }
-
- if (inConflict()) {
- return;
- }
-
- // go through stored propagations
- bool ok = true;
- for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok; d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
- TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
- // temporary fix for incremental bit-blasting
- if (d_valuation.isSatLiteral(literal)) {
- Debug("bitvector::propagate") << "TheoryBV:: propagating " << literal <<"\n";
- ok = d_out->propagate(literal);
- }
- }
-
- if (!ok) {
- Debug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl;
- setConflict();
- }
-}
+void TheoryBV::propagate(Effort e) { return d_internal->propagate(e); }
Theory::PPAssertStatus TheoryBV::ppAssert(TNode in,
SubstitutionMap& outSubstitutions)
{
- switch (in.getKind())
- {
- case kind::EQUAL:
- {
- if (in[0].isVar() && isLegalElimination(in[0], in[1]))
- {
- ++(d_statistics.d_solveSubstitutions);
- outSubstitutions.addSubstitution(in[0], in[1]);
- return PP_ASSERT_STATUS_SOLVED;
- }
- if (in[1].isVar() && isLegalElimination(in[1], in[0]))
- {
- ++(d_statistics.d_solveSubstitutions);
- outSubstitutions.addSubstitution(in[1], in[0]);
- return 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 (isLegalElimination(extract[0], concat))
- {
- outSubstitutions.addSubstitution(extract[0], concat);
- return 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 PP_ASSERT_STATUS_UNSOLVED;
-}
-
-TrustNode TheoryBV::ppRewrite(TNode t)
-{
- Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n";
- Node res = t;
- if (options::bitwiseEq() && RewriteRule<BitwiseEq>::applies(t)) {
- Node result = RewriteRule<BitwiseEq>::run<false>(t);
- res = Rewriter::rewrite(result);
- } else if (RewriteRule<UltPlusOne>::applies(t)) {
- Node result = RewriteRule<UltPlusOne>::run<false>(t);
- res = Rewriter::rewrite(result);
- }
- else if (res.getKind() == kind::EQUAL
- && ((res[0].getKind() == kind::BITVECTOR_PLUS
- && RewriteRule<ConcatToMult>::applies(res[1]))
- || (res[1].getKind() == kind::BITVECTOR_PLUS
- && RewriteRule<ConcatToMult>::applies(res[0]))))
- {
- Node mult = RewriteRule<ConcatToMult>::applies(res[0])?
- RewriteRule<ConcatToMult>::run<false>(res[0]) :
- RewriteRule<ConcatToMult>::run<true>(res[1]);
- Node factor = mult[0];
- Node sum = RewriteRule<ConcatToMult>::applies(res[0])? res[1] : res[0];
- Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult);
- Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq);
- if (rewr_eq[0].isVar() || rewr_eq[1].isVar()){
- res = Rewriter::rewrite(rewr_eq);
- } else {
- res = t;
- }
- }
- else if (RewriteRule<SignExtendEqConst>::applies(t))
- {
- res = RewriteRule<SignExtendEqConst>::run<false>(t);
- }
- else if (RewriteRule<ZeroExtendEqConst>::applies(t))
- {
- res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
- }
- else if (RewriteRule<NormalizeEqPlusNeg>::applies(t))
- {
- res = RewriteRule<NormalizeEqPlusNeg>::run<false>(t);
- }
-
- // if(t.getKind() == kind::EQUAL &&
- // ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() ==
- // kind::BITVECTOR_PLUS) ||
- // (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() ==
- // kind::BITVECTOR_PLUS))) {
- // // if we have an equality between a multiplication and addition
- // // try to express multiplication in terms of addition
- // Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1];
- // Node add = t[0].getKind() == kind::BITVECTOR_PLUS? t[0] : t[1];
- // if (RewriteRule<MultSlice>::applies(mult)) {
- // Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
- // Node new_eq =
- // Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL,
- // new_mult, add));
-
- // // the simplification can cause the formula to blow up
- // // only apply if formula reduced
- // if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) {
- // BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST];
- // uint64_t old_size = bv->computeAtomWeight(t);
- // Assert (old_size);
- // uint64_t new_size = bv->computeAtomWeight(new_eq);
- // double ratio = ((double)new_size)/old_size;
- // if (ratio <= 0.4) {
- // ++(d_statistics.d_numMultSlice);
- // return new_eq;
- // }
- // }
-
- // if (new_eq.getKind() == kind::CONST_BOOLEAN) {
- // ++(d_statistics.d_numMultSlice);
- // return new_eq;
- // }
- // }
- // }
-
- if (options::bvAbstraction() && t.getType().isBoolean()) {
- d_abstractionModule->addInputAtom(res);
- }
- Debug("bv-pp-rewrite") << "to " << res << "\n";
- if (res != t)
- {
- return TrustNode::mkTrustRewrite(t, res, nullptr);
- }
- return TrustNode::null();
-}
-
-void TheoryBV::presolve() {
- Debug("bitvector") << "TheoryBV::presolve" << endl;
-}
-
-static int prop_count = 0;
-
-bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
-{
- Debug("bitvector::propagate") << indent() << getSatContext()->getLevel() << " " << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ")" << std::endl;
- prop_count++;
-
- // If already in conflict, no more propagation
- if (d_conflict) {
- Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << "): already in conflict" << std::endl;
- return false;
- }
-
- // If propagated already, just skip
- PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
- if (find != d_propagatedBy.end()) {
- return true;
- } else {
- bool polarity = literal.getKind() != kind::NOT;
- Node negatedLiteral = polarity ? literal.notNode() : (Node) literal[0];
- find = d_propagatedBy.find(negatedLiteral);
- if (find != d_propagatedBy.end() && (*find).second != subtheory) {
- // Safe to ignore this one, subtheory should produce a conflict
- return true;
- }
-
- d_propagatedBy[literal] = subtheory;
- }
-
- // Propagate differs depending on the subtheory
- // * bitblaster needs to be left alone until it's done, otherwise it doesn't
- // know how to explain
- // * equality engine can propagate eagerly
- // TODO(2348): Determine if ok should be set by propagate. If not, remove ok.
- constexpr bool ok = true;
- if (subtheory == SUB_CORE) {
- d_out->propagate(literal);
- if (!ok) {
- setConflict();
- }
- } else {
- d_literalsToPropagate.push_back(literal);
- }
- return ok;
-
-}/* TheoryBV::propagate(TNode) */
-
-
-void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
- Assert(wasPropagatedBySubtheory(literal));
- SubTheory sub = getPropagatingSubtheory(literal);
- d_subtheoryMap[sub]->explain(literal, assumptions);
+ return d_internal->ppAssert(in, outSubstitutions);
}
-TrustNode TheoryBV::explain(TNode node)
-{
- Debug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl;
- std::vector<TNode> assumptions;
+TrustNode TheoryBV::ppRewrite(TNode t) { return d_internal->ppRewrite(t); }
- // Ask for the explanation
- explain(node, assumptions);
- // this means that it is something true at level 0
- Node explanation;
- if (assumptions.size() == 0) {
- explanation = utils::mkTrue();
- }
- else
- {
- // return the explanation
- explanation = utils::mkAnd(assumptions);
- }
- Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl;
- Debug("bitvector::explain") << "TheoryBV::explain done. \n";
- return TrustNode::mkTrustPropExp(node, explanation, nullptr);
-}
+void TheoryBV::presolve() { d_internal->presolve(); }
-void TheoryBV::notifySharedTerm(TNode t)
-{
- Debug("bitvector::sharing")
- << indent() << "TheoryBV::notifySharedTerm(" << t << ")" << std::endl;
- d_sharedTermsSet.insert(t);
- if (options::bitvectorEqualitySolver()) {
- for (unsigned i = 0; i < d_subtheories.size(); ++i) {
- d_subtheories[i]->addSharedTerm(t);
- }
- }
-}
+TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); }
+void TheoryBV::notifySharedTerm(TNode t) { d_internal->notifySharedTerm(t); };
-EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
+void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned)
{
- if (options::bitblastMode() == options::BitblastMode::EAGER)
- return EQUALITY_UNKNOWN;
- Assert(options::bitblastMode() == options::BitblastMode::LAZY);
- for (unsigned i = 0; i < d_subtheories.size(); ++i) {
- EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
- if (status != EQUALITY_UNKNOWN) {
- return status;
- }
- }
- return EQUALITY_UNKNOWN; ;
-}
-
-void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
- if(d_staticLearnCache.find(in) != d_staticLearnCache.end()){
- return;
- }
- d_staticLearnCache.insert(in);
-
- if (in.getKind() == kind::EQUAL) {
- if((in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL) ||
- (in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL)) {
- TNode p = in[0].getKind() == kind::BITVECTOR_PLUS ? in[0] : in[1];
- TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0];
-
- if(p.getNumChildren() == 2
- && p[0].getKind() == kind::BITVECTOR_SHL
- && p[1].getKind() == kind::BITVECTOR_SHL ){
- unsigned size = utils::getSize(s);
- Node one = utils::mkConst(size, 1u);
- if(s[0] == one && p[0][0] == one && p[1][0] == one){
- Node zero = utils::mkConst(size, 0u);
- TNode b = p[0];
- TNode c = p[1];
- // (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
- Node b_eq_0 = b.eqNode(zero);
- Node c_eq_0 = c.eqNode(zero);
- Node b_eq_c = b.eqNode(c);
-
- Node dis = NodeManager::currentNM()->mkNode(
- kind::OR, b_eq_0, c_eq_0, b_eq_c);
- Node imp = in.impNode(dis);
- learned << imp;
- }
- }
- }
- }else if(in.getKind() == kind::AND){
- for(size_t i = 0, N = in.getNumChildren(); i < N; ++i){
- ppStaticLearn(in[i], learned);
- }
- }
+ d_internal->ppStaticLearn(in, learned);
}
-bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
- bool changed = d_abstractionModule->applyAbstraction(assertions, new_assertions);
- if (changed && options::bitblastMode() == options::BitblastMode::EAGER
- && options::bitvectorAig())
- {
- // disable AIG mode
- AlwaysAssert(!d_eagerSolver->isInitialized());
- d_eagerSolver->turnOffAig();
- d_eagerSolver->initialize();
- }
- return changed;
-}
-
-void TheoryBV::setConflict(Node conflict)
+bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions,
+ std::vector<Node>& new_assertions)
{
- if (options::bvAbstraction())
- {
- NodeManager* const nm = NodeManager::currentNM();
- Node new_conflict = d_abstractionModule->simplifyConflict(conflict);
-
- std::vector<Node> lemmas;
- lemmas.push_back(new_conflict);
- d_abstractionModule->generalizeConflict(new_conflict, lemmas);
- for (unsigned i = 0; i < lemmas.size(); ++i)
- {
- lemma(nm->mkNode(kind::NOT, lemmas[i]));
- }
- }
- d_conflict = true;
- d_conflictNode = conflict;
+ return d_internal->applyAbstraction(assertions, new_assertions);
}
-} /* namespace CVC4::theory::bv */
-} /* namespace CVC4::theory */
-} /* namespace CVC4 */
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
#define CVC4__THEORY__BV__THEORY_BV_H
#include <unordered_map>
-#include <unordered_set>
-#include "context/cdhashset.h"
-#include "context/cdlist.h"
-#include "context/context.h"
-#include "theory/bv/bv_subtheory.h"
#include "theory/bv/theory_bv_rewriter.h"
-#include "theory/bv/theory_bv_utils.h"
#include "theory/theory.h"
-#include "util/hash.h"
-#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
namespace bv {
-class CoreSolver;
-class InequalitySolver;
-class AlgebraicSolver;
-class BitblastSolver;
+class BVSolver;
-class EagerBitblastSolver;
-
-class AbstractionModule;
-
-class TheoryBV : public Theory {
-
- /** The context we are using */
- context::Context* d_context;
-
- /** Context dependent set of atoms we already propagated */
- context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
- context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
-
- std::vector<std::unique_ptr<SubtheorySolver>> d_subtheories;
- std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
+class TheoryBV : public Theory
+{
+ /* BVSolverLazy accesses methods from theory in a way that is deprecated and
+ * will be removed in the future. For now we allow direct access. */
+ friend class BVSolverLazy;
public:
TheoryBV(context::Context* c,
~TheoryBV();
- //--------------------------------- initialization
/** get the official theory rewriter of this theory */
TheoryRewriter* getTheoryRewriter() override;
+
/**
* Returns true if we need an equality engine. If so, we initialize the
* information regarding how it should be setup. For details, see the
* documentation in Theory::needsEqualityEngine.
*/
bool needsEqualityEngine(EeSetupInfo& esi) override;
- /** finish initialization */
+
void finishInit() override;
- //--------------------------------- end initialization
TrustNode expandDefinition(Node node) override;
void preRegisterTerm(TNode n) override;
- void check(Effort e) override;
+ bool preCheck(Effort e) override;
bool needsCheckLastEffort() override;
void presolve() override;
+ /** Called by abstraction preprocessing pass. */
bool applyAbstraction(const std::vector<Node>& assertions,
std::vector<Node>& new_assertions);
private:
- class Statistics
- {
- public:
- AverageStat d_avgConflictSize;
- IntStat d_solveSubstitutions;
- TimerStat d_solveTimer;
- IntStat d_numCallsToCheckFullEffort;
- IntStat d_numCallsToCheckStandardEffort;
- TimerStat d_weightComputationTimer;
- IntStat d_numMultSlice;
- Statistics();
- ~Statistics();
- };
-
- Statistics d_statistics;
-
- void spendResource(ResourceManager::Resource r);
+ void notifySharedTerm(TNode t) override;
/**
- * Return the uninterpreted function symbol corresponding to division-by-zero
- * for this particular bit-width
+ * Return the UF symbol corresponding to division-by-zero for this particular
+ * bit-width.
* @param k should be UREM or UDIV
- * @param width
- *
- * @return
+ * @param width bit-width
*/
- Node getBVDivByZero(Kind k, unsigned width);
+ Node getUFDivByZero(Kind k, unsigned width);
- typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
- typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
- NodeSet d_staticLearnCache;
+ /** Internal BV solver. */
+ std::unique_ptr<BVSolver> d_internal;
/**
* Maps from bit-vector width to division-by-zero uninterpreted
* function symbols.
*/
- std::unordered_map<unsigned, Node> d_BVDivByZero;
- std::unordered_map<unsigned, Node> d_BVRemByZero;
-
- typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode;
-
- context::CDO<bool> d_lemmasAdded;
-
- // Are we in conflict?
- context::CDO<bool> d_conflict;
-
- // Invalidate the model cache if check was called
- context::CDO<bool> d_invalidateModelCache;
-
- /** The conflict node */
- Node d_conflictNode;
-
- /** Literals to propagate */
- context::CDList<Node> d_literalsToPropagate;
-
- /** Index of the next literal to propagate */
- context::CDO<unsigned> d_literalsToPropagateIndex;
-
- /**
- * Keeps a map from nodes to the subtheory that propagated it so that we can explain it
- * properly.
- */
- typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap;
- PropagatedMap d_propagatedBy;
-
- std::unique_ptr<EagerBitblastSolver> d_eagerSolver;
- std::unique_ptr<AbstractionModule> d_abstractionModule;
- bool d_calledPreregister;
-
- bool wasPropagatedBySubtheory(TNode literal) const {
- return d_propagatedBy.find(literal) != d_propagatedBy.end();
- }
-
- SubTheory getPropagatingSubtheory(TNode literal) const {
- Assert(wasPropagatedBySubtheory(literal));
- PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
- return (*find).second;
- }
-
- /** Should be called to propagate the literal. */
- bool storePropagation(TNode literal, SubTheory subtheory);
-
- /**
- * Explains why this literal (propagated by subtheory) is true by adding assumptions.
- */
- void explain(TNode literal, std::vector<TNode>& assumptions);
-
- void notifySharedTerm(TNode t) override;
-
- bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); }
-
- EqualityStatus getEqualityStatus(TNode a, TNode b) override;
-
- Node getModelValue(TNode var) override;
-
- inline std::string indent()
- {
- std::string indentStr(getSatContext()->getLevel(), ' ');
- return indentStr;
- }
-
- void setConflict(Node conflict = Node::null());
-
- bool inConflict() {
- return d_conflict;
- }
-
- void sendConflict();
-
- void lemma(TNode node)
- {
- d_out->lemma(node);
- d_lemmasAdded = true;
- }
-
- void checkForLemma(TNode node);
+ std::unordered_map<unsigned, Node> d_ufDivByZero;
+ std::unordered_map<unsigned, Node> d_ufRemByZero;
/** The theory rewriter for this theory. */
TheoryBVRewriter d_rewriter;
+
/** A (default) theory state object */
TheoryState d_state;
- friend class LazyBitblaster;
- friend class TLazyBitblaster;
- friend class EagerBitblaster;
- friend class BitblastSolver;
- friend class EqualitySolver;
- friend class CoreSolver;
- friend class InequalitySolver;
- friend class AlgebraicSolver;
- friend class EagerBitblastSolver;
-};/* class TheoryBV */
-
-}/* CVC4::theory::bv namespace */
-}/* CVC4::theory namespace */
-
-}/* CVC4 namespace */
+ /** A (default) theory inference manager. */
+ TheoryInferenceManager d_inferMgr;
+
+}; /* class TheoryBV */
+
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
#endif /* CVC4__THEORY__BV__THEORY_BV_H */
return d_out.requirePhase(n, pol);
}
+void TheoryInferenceManager::spendResource(ResourceManager::Resource r)
+{
+ d_out.spendResource(r);
+}
+
+void TheoryInferenceManager::safePoint(ResourceManager::Resource r)
+{
+ d_out.safePoint(r);
+}
+
} // namespace theory
} // namespace CVC4
* decided with polarity pol, for details see OutputChannel::requirePhase.
*/
void requirePhase(TNode n, bool pol);
+
+ /**
+ * Forward to OutputChannel::spendResource() to spend resources.
+ */
+ void spendResource(ResourceManager::Resource r);
+
+ /**
+ * Forward to OutputChannel::safePoint() to spend resources.
+ */
+ void safePoint(ResourceManager::Resource r);
+
protected:
/**
* Process internal fact. This is a common helper method for the
bool TheoryState::isInConflict() const { return d_conflict; }
+bool TheoryState::isSatLiteral(TNode lit) const
+{
+ return d_valuation.isSatLiteral(lit);
+}
+
} // namespace theory
} // namespace CVC4
/** Are we currently in conflict? */
virtual bool isInConflict() const;
+ /** Returns true if lit is a SAT literal. */
+ virtual bool isSatLiteral(TNode lit) const;
+
protected:
/** Pointer to the SAT context object used by the theory. */
context::Context* d_context;
** \todo document this file
**/
-
#include <cxxtest/TestSuite.h>
-#include "theory/theory.h"
+#include <vector>
+
+#include "context/context.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
-#include "theory/bv/theory_bv.h"
#include "theory/bv/bitblast/eager_bitblaster.h"
-#include "expr/node.h"
-#include "expr/node_manager.h"
-#include "context/context.h"
-
+#include "theory/bv/bv_solver_lazy.h"
+#include "theory/theory.h"
#include "theory/theory_test_utils.h"
-#include <vector>
-
using namespace CVC4;
using namespace CVC4::theory;
using namespace CVC4::theory::bv;
// engine d_smt. We must ensure that d_smt is properly initialized via
// the following call, which constructs its underlying theory engine.
d_smt->finishInit();
- EagerBitblaster* bb = new EagerBitblaster(
- dynamic_cast<TheoryBV*>(
- d_smt->getTheoryEngine()->d_theoryTable[THEORY_BV]),
- d_smt->getContext());
+ TheoryBV* tbv = dynamic_cast<TheoryBV*>(
+ d_smt->getTheoryEngine()->d_theoryTable[THEORY_BV]);
+ BVSolverLazy* bvsl = dynamic_cast<BVSolverLazy*>(tbv->d_internal.get());
+ EagerBitblaster* bb = new EagerBitblaster(bvsl, d_smt->getContext());
+
Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(16));
Node y = d_nm->mkVar("y", d_nm->mkBitVectorType(16));
Node x_plus_y = d_nm->mkNode(kind::BITVECTOR_PLUS, x, y);
projects / cvc5.git / commitdiff