GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bv_subtheory.h Lines: 11 30 36.7 %
Date: 2021-03-22 Branches: 7 35 20.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_subtheory.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Tim King, Dejan Jovanovic
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 Interface for bit-vectors sub-solvers.
13
 **
14
 ** Interface for bit-vectors sub-solvers.
15
 **/
16
17
#ifndef CVC4__THEORY__BV__BV_SUBTHEORY_H
18
#define CVC4__THEORY__BV__BV_SUBTHEORY_H
19
20
#include "cvc4_private.h"
21
#include "context/context.h"
22
#include "context/cdqueue.h"
23
#include "theory/uf/equality_engine.h"
24
#include "theory/theory.h"
25
26
namespace CVC4 {
27
28
namespace theory {
29
30
class TheoryModel;
31
32
namespace bv {
33
34
enum SubTheory {
35
  SUB_CORE = 1,
36
  SUB_BITBLAST = 2,
37
  SUB_INEQUALITY = 3,
38
  SUB_ALGEBRAIC = 4
39
};
40
41
inline std::ostream& operator<<(std::ostream& out, SubTheory subtheory) {
42
  switch (subtheory) {
43
    case SUB_BITBLAST:
44
      return out << "BITBLASTER";
45
    case SUB_CORE:
46
      return out << "BV_CORE_SUBTHEORY";
47
    case SUB_INEQUALITY:
48
      return out << "BV_INEQUALITY_SUBTHEORY";
49
    case SUB_ALGEBRAIC:
50
      return out << "BV_ALGEBRAIC_SUBTHEORY";
51
    default:
52
      break;
53
  }
54
  Unreachable();
55
}
56
57
// forward declaration
58
class BVSolverLazy;
59
60
using AssertionQueue = context::CDQueue<Node>;
61
62
/**
63
 * Abstract base class for bit-vector subtheory solvers
64
 *
65
 */
66
class SubtheorySolver {
67
 public:
68
26860
  SubtheorySolver(context::Context* c, BVSolverLazy* bv)
69
26860
      : d_context(c), d_bv(bv), d_assertionQueue(c), d_assertionIndex(c, 0)
70
  {
71
26860
  }
72
26851
  virtual ~SubtheorySolver() {}
73
  virtual bool check(Theory::Effort e) = 0;
74
  virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0;
75
  virtual void preRegister(TNode node) {}
76
  virtual void propagate(Theory::Effort e) {}
77
  virtual bool collectModelValues(TheoryModel* m,
78
                                  const std::set<Node>& termSet) = 0;
79
  virtual Node getModelValue(TNode var) = 0;
80
  virtual bool isComplete() = 0;
81
  virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0;
82
7089873
  bool done() { return d_assertionQueue.size() == d_assertionIndex; }
83
3261863
  TNode get() {
84
3261863
    Assert(!done());
85
3261863
    TNode res = d_assertionQueue[d_assertionIndex];
86
3261863
    d_assertionIndex = d_assertionIndex + 1;
87
3261863
    return res;
88
  }
89
2275718
  virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); }
90
91
  AssertionQueue::const_iterator assertionsBegin() {
92
    return d_assertionQueue.begin();
93
  }
94
  AssertionQueue::const_iterator assertionsEnd() {
95
    return d_assertionQueue.end();
96
  }
97
98
 protected:
99
  /** The context we are using */
100
  context::Context* d_context;
101
102
  /** The bit-vector theory */
103
  BVSolverLazy* d_bv;
104
  AssertionQueue d_assertionQueue;
105
  context::CDO<uint32_t> d_assertionIndex;
106
}; /* class SubtheorySolver */
107
108
}  // namespace bv
109
}  // namespace theory
110
}  // namespace CVC4
111
112
#endif /* CVC4__THEORY__BV__BV_SUBTHEORY_H */