src/theory/bv/bv_solver.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Mathias Preiner, Andrew Reynolds, Andres Noetzli
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * Bit-vector solver interface.
  14  *
  15  * Describes the interface for the internal bit-vector solver of TheoryBV.
  16  */
  17
  18 #include "cvc5_private.h"
  19
  20 #ifndef CVC5__THEORY__BV__BV_SOLVER_H
  21 #define CVC5__THEORY__BV__BV_SOLVER_H
  22
  23 #include "theory/theory.h"
  24
  25 namespace cvc5 {
  26 namespace theory {
  27 namespace bv {
  28
  29 class BVSolver
  30 {
  31  public:
  32   BVSolver(TheoryState& state, TheoryInferenceManager& inferMgr)
  33       : d_state(state), d_im(inferMgr){};
  34
  35   virtual ~BVSolver() {}
  36
  37   /**
  38    * Returns true if we need an equality engine. If so, we initialize the
  39    * information regarding how it should be setup. For details, see the
  40    * documentation in Theory::needsEqualityEngine.
  41    */
  42   virtual bool needsEqualityEngine(EeSetupInfo& esi) { return false; }
  43
  44   virtual void finishInit(){};
  45
  46   virtual void preRegisterTerm(TNode n) = 0;
  47
  48   /**
  49    * Forwarded from TheoryBV::preCheck().
  50    */
  51   virtual bool preCheck(Theory::Effort level = Theory::Effort::EFFORT_FULL)
  52   {
  53     return false;
  54   }
  55   /**
  56    * Forwarded from TheoryBV::postCheck().
  57    */
  58   virtual void postCheck(Theory::Effort level = Theory::Effort::EFFORT_FULL){};
  59   /**
  60    * Forwarded from TheoryBV:preNotifyFact().
  61    */
  62   virtual bool preNotifyFact(
  63       TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
  64   {
  65     return false;
  66   }
  67   /**
  68    * Forwarded from TheoryBV::notifyFact().
  69    */
  70   virtual void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) {}
  71
  72   virtual bool needsCheckLastEffort() { return false; }
  73
  74   virtual void propagate(Theory::Effort e) {}
  75
  76   virtual TrustNode explain(TNode n)
  77   {
  78     Unimplemented() << "BVSolver propagated a node but doesn't implement the "
  79                        "BVSolver::explain() interface!";
  80     return TrustNode::null();
  81   }
  82
  83   /** Additionally collect terms relevant for collecting model values. */
  84   virtual void computeRelevantTerms(std::set<Node>& termSet) {}
  85
  86   /** Collect model values in m based on the relevant terms given by termSet */
  87   virtual bool collectModelValues(TheoryModel* m,
  88                                   const std::set<Node>& termSet) = 0;
  89
  90   virtual std::string identify() const = 0;
  91
  92   virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); }
  93
  94   virtual void ppStaticLearn(TNode in, NodeBuilder& learned) {}
  95
  96   virtual void presolve() {}
  97
  98   virtual void notifySharedTerm(TNode t) {}
  99
 100   virtual EqualityStatus getEqualityStatus(TNode a, TNode b)
 101   {
 102     return EqualityStatus::EQUALITY_UNKNOWN;
 103   }
 104
 105   /** Called by abstraction preprocessing pass. */
 106   virtual bool applyAbstraction(const std::vector<Node>& assertions,
 107                                 std::vector<Node>& new_assertions)
 108   {
 109     new_assertions.insert(
 110         new_assertions.end(), assertions.begin(), assertions.end());
 111     return false;
 112   };
 113
 114  protected:
 115   TheoryState& d_state;
 116   TheoryInferenceManager& d_im;
 117 };
 118
 119 }  // namespace bv
 120 }  // namespace theory
 121 }  // namespace cvc5
 122
 123 #endif /* CVC5__THEORY__BV__BV_SOLVER_H */