Split lazy bit-vector solver from TheoryBV (#5009)

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.

1 files changed, 119 insertions, 0 deletions

diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h
new file mode 100644
index 000000000..fef95ceef
--- /dev/null
+++ b/src/theory/bv/bv_solver.h
@@ -0,0 +1,119 @@
+/*********************                                                        */
+/*! \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 */