GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bv_solver.h Lines: 16 26 61.5 %
Date: 2021-03-22 Branches: 0 8 0.0 %

Line Exec Source
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-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.\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
8995
  BVSolver(TheoryState& state, TheoryInferenceManager& inferMgr)
32
8995
      : d_state(state), d_im(inferMgr){};
33
34
8992
  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
10
  virtual bool needsEqualityEngine(EeSetupInfo& esi) { return false; }
42
43
10
  virtual void finishInit(){};
44
45
  virtual void preRegisterTerm(TNode n) = 0;
46
47
  /**
48
   * Forwarded from TheoryBV::preCheck().
49
   */
50
6114
  virtual bool preCheck(Theory::Effort level = Theory::Effort::EFFORT_FULL)
51
  {
52
6114
    return false;
53
  }
54
  /**
55
   * Forwarded from TheoryBV::postCheck().
56
   */
57
6114
  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
12
  virtual bool needsCheckLastEffort() { return false; }
72
73
6128
  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
1056
  virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); };
92
93
28
  virtual void ppStaticLearn(TNode in, NodeBuilder<>& learned){};
94
95
14
  virtual void presolve(){};
96
97
100
  virtual void notifySharedTerm(TNode t) {}
98
99
64
  virtual EqualityStatus getEqualityStatus(TNode a, TNode b)
100
  {
101
64
    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 */