GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/quant_module.h Lines: 9 11 81.8 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quant_module.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   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 quantifier module
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANT_MODULE_H
18
#define CVC4__THEORY__QUANT_MODULE_H
19
20
#include <iostream>
21
#include <map>
22
#include <vector>
23
24
#include "theory/quantifiers/quantifiers_inference_manager.h"
25
#include "theory/quantifiers/quantifiers_registry.h"
26
#include "theory/quantifiers/quantifiers_state.h"
27
#include "theory/theory.h"
28
#include "theory/uf/equality_engine.h"
29
30
namespace CVC4 {
31
namespace theory {
32
33
class QuantifiersEngine;
34
35
namespace quantifiers {
36
class TermDb;
37
}  // namespace quantifiers
38
39
/** QuantifiersModule class
40
 *
41
 * This is the virtual class for defining subsolvers of the quantifiers theory.
42
 * It has a similar interface to a Theory object.
43
 */
44
class QuantifiersModule
45
{
46
 public:
47
  /** effort levels for quantifiers modules check */
48
  enum QEffort
49
  {
50
    // conflict effort, for conflict-based instantiation
51
    QEFFORT_CONFLICT,
52
    // standard effort, for heuristic instantiation
53
    QEFFORT_STANDARD,
54
    // model effort, for model-based instantiation
55
    QEFFORT_MODEL,
56
    // last call effort, for last resort techniques
57
    QEFFORT_LAST_CALL,
58
    // none
59
    QEFFORT_NONE,
60
  };
61
62
 public:
63
  QuantifiersModule(quantifiers::QuantifiersState& qs,
64
                    quantifiers::QuantifiersInferenceManager& qim,
65
                    quantifiers::QuantifiersRegistry& qr,
66
                    QuantifiersEngine* qe);
67
24141
  virtual ~QuantifiersModule() {}
68
  /** Presolve.
69
   *
70
   * Called at the beginning of check-sat call.
71
   */
72
16606
  virtual void presolve() {}
73
  /** Needs check.
74
   *
75
   * Returns true if this module wishes a call to be made
76
   * to check(e) during QuantifiersEngine::check(e).
77
   */
78
  virtual bool needsCheck(Theory::Effort e)
79
  {
80
    return e >= Theory::EFFORT_LAST_CALL;
81
  }
82
  /** Needs model.
83
   *
84
   * Whether this module needs a model built during a
85
   * call to QuantifiersEngine::check(e)
86
   * It returns one of QEFFORT_* from quantifiers_engine.h,
87
   * which specifies the quantifiers effort in which it requires the model to
88
   * be built.
89
   */
90
  virtual QEffort needsModel(Theory::Effort e);
91
  /** Reset.
92
   *
93
   * Called at the beginning of QuantifiersEngine::check(e).
94
   */
95
36262
  virtual void reset_round(Theory::Effort e) {}
96
  /** Check.
97
   *
98
   *   Called during QuantifiersEngine::check(e) depending
99
   *   if needsCheck(e) returns true.
100
   */
101
  virtual void check(Theory::Effort e, QEffort quant_e) = 0;
102
  /** Check complete?
103
   *
104
   * Returns false if the module's reasoning was globally incomplete
105
   * (e.g. "sat" must be replaced with "incomplete").
106
   *
107
   * This is called just before the quantifiers engine will return
108
   * with no lemmas added during a LAST_CALL effort check.
109
   */
110
10461
  virtual bool checkComplete() { return true; }
111
  /** Check was complete for quantified formula q
112
   *
113
   * If for each quantified formula q, some module returns true for
114
   * checkCompleteFor( q ),
115
   * and no lemmas are added by the quantifiers theory, then we may answer
116
   * "sat", unless
117
   * we are incomplete for other reasons.
118
   */
119
4799
  virtual bool checkCompleteFor(Node q) { return false; }
120
  /** Check ownership
121
   *
122
   * Called once for new quantified formulas that are registered by the
123
   * quantifiers theory. The primary purpose of this function is to establish
124
   * if this module is the owner of quantified formula q.
125
   */
126
28347
  virtual void checkOwnership(Node q) {}
127
  /** Register quantifier
128
   *
129
   * Called once for new quantified formulas q that are pre-registered by the
130
   * quantifiers theory, after internal ownership of quantified formulas is
131
   * finalized. This does context-independent initialization of this module
132
   * for quantified formula q.
133
   */
134
38938
  virtual void registerQuantifier(Node q) {}
135
  /** Pre-register quantifier
136
   *
137
   * Called once for new quantified formulas that are
138
   * pre-registered by the quantifiers theory, after
139
   * internal ownership of quantified formulas is finalized.
140
   */
141
62778
  virtual void preRegisterQuantifier(Node q) {}
142
  /** Assert node.
143
   *
144
   * Called when a quantified formula q is asserted to the quantifiers theory
145
   */
146
118594
  virtual void assertNode(Node q) {}
147
  /** Identify this module (for debugging, dynamic configuration, etc..) */
148
  virtual std::string identify() const = 0;
149
  //----------------------------general queries
150
  /** get currently used the equality engine */
151
  eq::EqualityEngine* getEqualityEngine() const;
152
  /** are n1 and n2 equal in the current used equality engine? */
153
  bool areEqual(TNode n1, TNode n2) const;
154
  /** are n1 and n2 disequal in the current used equality engine? */
155
  bool areDisequal(TNode n1, TNode n2) const;
156
  /** get the representative of n in the current used equality engine */
157
  TNode getRepresentative(TNode n) const;
158
  /** get quantifiers engine that owns this module */
159
  QuantifiersEngine* getQuantifiersEngine() const;
160
  /** get currently used term database */
161
  quantifiers::TermDb* getTermDatabase() const;
162
  /** get the quantifiers state */
163
  quantifiers::QuantifiersState& getState();
164
  /** get the quantifiers inference manager */
165
  quantifiers::QuantifiersInferenceManager& getInferenceManager();
166
  /** get the quantifiers registry */
167
  quantifiers::QuantifiersRegistry& getQuantifiersRegistry();
168
  //----------------------------end general queries
169
 protected:
170
  /** pointer to the quantifiers engine that owns this module */
171
  QuantifiersEngine* d_quantEngine;
172
  /** The state of the quantifiers engine */
173
  quantifiers::QuantifiersState& d_qstate;
174
  /** The quantifiers inference manager */
175
  quantifiers::QuantifiersInferenceManager& d_qim;
176
  /** The quantifiers registry */
177
  quantifiers::QuantifiersRegistry& d_qreg;
178
}; /* class QuantifiersModule */
179
180
}  // namespace theory
181
}  // namespace CVC4
182
183
#endif /* CVC4__THEORY__QUANT_UTIL_H */