GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/first_order_model.h Lines: 4 6 66.7 %
Date: 2021-03-22 Branches: 9 22 40.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file first_order_model.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Paul Meng, Morgan Deters
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 Model extended classes
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__FIRST_ORDER_MODEL_H
18
#define CVC4__FIRST_ORDER_MODEL_H
19
20
#include "context/cdlist.h"
21
#include "expr/attribute.h"
22
#include "theory/theory_model.h"
23
#include "theory/uf/theory_uf_model.h"
24
25
namespace CVC4 {
26
namespace theory {
27
28
class QuantifiersEngine;
29
30
namespace quantifiers {
31
32
class QuantifiersState;
33
class TermRegistry;
34
class QuantifiersRegistry;
35
36
namespace fmcheck {
37
  class FirstOrderModelFmc;
38
}/* CVC4::theory::quantifiers::fmcheck namespace */
39
40
struct IsStarAttributeId {};
41
typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
42
43
// TODO (#1301) : document and refactor this class
44
17160
class FirstOrderModel : public TheoryModel
45
{
46
 public:
47
  FirstOrderModel(QuantifiersState& qs,
48
                  QuantifiersRegistry& qr,
49
                  TermRegistry& tr,
50
                  std::string name);
51
52
  //!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
53
  /** finish initialize */
54
  void finishInit(QuantifiersEngine* qe);
55
56
  /** assert quantifier */
57
  void assertQuantifier( Node n );
58
  /** get number of asserted quantifiers */
59
  size_t getNumAssertedQuantifiers() const;
60
  /** get asserted quantifier */
61
  Node getAssertedQuantifier( unsigned i, bool ordered = false );
62
  /** initialize model for term */
63
  void initializeModelForTerm( Node n, std::map< Node, bool >& visited );
64
  // initialize the model
65
  void initialize();
66
  /** get variable id */
67
44909
  int getVariableId(TNode q, TNode n) {
68
44909
    return d_quant_var_id.find( q )!=d_quant_var_id.end() ? d_quant_var_id[q][n] : -1;
69
  }
70
  /** do we need to do any work? */
71
  bool checkNeeded();
72
  /** reset round */
73
  void reset_round();
74
  /** mark quantified formula relevant */
75
  void markRelevant( Node q );
76
  /** set quantified formula active/inactive
77
   *
78
   * This indicates that quantified formula is "inactive", that is, it need
79
   * not be considered during this instantiation round.
80
   *
81
   * A quantified formula may be set inactive if for instance:
82
   *   - It is entailed by other quantified formulas, or
83
   *   - All of its instances are known to be true in the current model.
84
   *
85
   * This method should be called after a call to FirstOrderModel::reset_round,
86
   * and before calls to QuantifiersModule check calls. A common place to call
87
   * this method is during QuantifiersModule reset_round calls.
88
   */
89
  void setQuantifierActive( TNode q, bool active );
90
  /** is quantified formula active?
91
   *
92
   * Returns false if there has been a call to setQuantifierActive( q, false )
93
   * during this instantiation round.
94
   */
95
  bool isQuantifierActive(TNode q) const;
96
  /** is quantified formula asserted */
97
  bool isQuantifierAsserted(TNode q) const;
98
  /** get model basis term */
99
  Node getModelBasisTerm(TypeNode tn);
100
  /** is model basis term */
101
  bool isModelBasisTerm(Node n);
102
  /** get model basis term for op */
103
  Node getModelBasisOpTerm(Node op);
104
  /** get model basis */
105
  Node getModelBasis(Node q, Node n);
106
  /** get model basis arg */
107
  unsigned getModelBasisArg(Node n);
108
  /** get some domain element */
109
  Node getSomeDomainElement(TypeNode tn);
110
  /** initialize representative set for type
111
   *
112
   * This ensures that TheoryModel::d_rep_set
113
   * is initialized for type tn. In particular:
114
   * (1) If tn is an uninitialized (unconstrained)
115
   * uninterpreted sort, then we interpret it
116
   * as a set of size one,
117
   * (2) If tn is a "small" enumerable finite type,
118
   * then we ensure that all its values are in
119
   * TheoryModel::d_rep_set.
120
   *
121
   * Returns true if the initialization was complete,
122
   * in that the set for tn in TheoryModel::d_rep_set
123
   * has all representatives of type tn.
124
   */
125
  bool initializeRepresentativesForType(TypeNode tn);
126
  /**
127
   * Has the term been marked as a model basis term?
128
   */
129
  static bool isModelBasis(TNode n);
130
131
 protected:
132
  //!!!!!!!!!!!!!!!!!!!!!!! TODO (project #15): temporarily available
133
  QuantifiersEngine* d_qe;
134
  /** The quantifiers registry */
135
  QuantifiersRegistry& d_qreg;
136
  /** Reference to the term registry */
137
  TermRegistry& d_treg;
138
  /** list of quantifiers asserted in the current context */
139
  context::CDList<Node> d_forall_asserts;
140
  /**
141
   * The (ordered) list of quantified formulas marked as relevant using
142
   * markRelevant, where the quantified formula q in the most recent
143
   * call to markRelevant comes last in the list.
144
   */
145
  std::vector<Node> d_forall_rlv_vec;
146
  /** The last quantified formula marked as relevant, if one exists. */
147
  Node d_last_forall_rlv;
148
  /**
149
   * The list of asserted quantified formulas, ordered by relevance.
150
   * Relevance is a dynamic partial ordering where q1 < q2 if there has been
151
   * a call to markRelevant( q1 ) after the last call to markRelevant( q2 )
152
   * (or no call to markRelevant( q2 ) has been made).
153
   *
154
   * This list is used primarily as an optimization for conflict-based
155
   * instantiation so that quantifed formulas that have been instantiated
156
   * most recently are processed first, since these are (statistically) more
157
   * likely to have conflicting instantiations.
158
   */
159
  std::vector<Node> d_forall_rlv_assert;
160
  /**
161
   * Whether the above list has been computed. This flag is updated during
162
   * reset_round and is valid within a full effort check.
163
   */
164
  bool d_forallRlvComputed;
165
  /** get variable id */
166
  std::map<Node, std::map<Node, int> > d_quant_var_id;
167
  /** process initialize model for term */
168
  virtual void processInitializeModelForTerm(Node n) {}
169
  /** process initialize quantifier */
170
9124
  virtual void processInitializeQuantifier(Node q) {}
171
  /** process initialize */
172
  virtual void processInitialize(bool ispre) {}
173
174
 private:
175
  // list of inactive quantified formulas
176
  std::map<TNode, bool> d_quant_active;
177
  /** map from types to model basis terms */
178
  std::map<TypeNode, Node> d_model_basis_term;
179
  /** map from ops to model basis terms */
180
  std::map<Node, Node> d_model_basis_op_term;
181
  /** map from instantiation terms to their model basis equivalent */
182
  std::map<Node, Node> d_model_basis_body;
183
  /** map from universal quantifiers to model basis terms */
184
  std::map<Node, std::vector<Node> > d_model_basis_terms;
185
  /** compute model basis arg */
186
  void computeModelBasisArgAttribute(Node n);
187
};/* class FirstOrderModel */
188
189
}/* CVC4::theory::quantifiers namespace */
190
}/* CVC4::theory namespace */
191
}/* CVC4 namespace */
192
193
#endif /* CVC4__FIRST_ORDER_MODEL_H */