src/theory/bv/bv_solver.h

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