GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/first_order_model.h Lines: 4 6 66.7 %
Date: 2021-03-23 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 "theory/quantifiers/equality_query.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
// TODO (#1301) : document and refactor this class
37
17162
class FirstOrderModel : public TheoryModel
38
{
39
 public:
40
  FirstOrderModel(QuantifiersState& qs,
41
                  QuantifiersRegistry& qr,
42
                  TermRegistry& tr,
43
                  std::string name);
44
45
  //!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
46
  /** finish initialize */
47
  void finishInit(QuantifiersEngine* qe);
48
  /** get internal representative
49
   *
50
   * Choose a term that is equivalent to a in the current context that is the
51
   * best term for instantiating the index^th variable of quantified formula q.
52
   * If no legal term can be found, we return null. This can occur if:
53
   * - a's type is not a subtype of the type of the index^th variable of q,
54
   * - a is in an equivalent class with all terms that are restricted not to
55
   * appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample
56
   * guided instantiation.
57
   */
58
  Node getInternalRepresentative(Node a, Node q, size_t index);
59
60
  /** assert quantifier */
61
  void assertQuantifier( Node n );
62
  /** get number of asserted quantifiers */
63
  size_t getNumAssertedQuantifiers() const;
64
  /** get asserted quantifier */
65
  Node getAssertedQuantifier( unsigned i, bool ordered = false );
66
  /** initialize model for term */
67
  void initializeModelForTerm( Node n, std::map< Node, bool >& visited );
68
  // initialize the model
69
  void initialize();
70
  /** get variable id */
71
44909
  int getVariableId(TNode q, TNode n) {
72
44909
    return d_quant_var_id.find( q )!=d_quant_var_id.end() ? d_quant_var_id[q][n] : -1;
73
  }
74
  /** do we need to do any work? */
75
  bool checkNeeded();
76
  /** reset round */
77
  void reset_round();
78
  /** mark quantified formula relevant */
79
  void markRelevant( Node q );
80
  /** set quantified formula active/inactive
81
   *
82
   * This indicates that quantified formula is "inactive", that is, it need
83
   * not be considered during this instantiation round.
84
   *
85
   * A quantified formula may be set inactive if for instance:
86
   *   - It is entailed by other quantified formulas, or
87
   *   - All of its instances are known to be true in the current model.
88
   *
89
   * This method should be called after a call to FirstOrderModel::reset_round,
90
   * and before calls to QuantifiersModule check calls. A common place to call
91
   * this method is during QuantifiersModule reset_round calls.
92
   */
93
  void setQuantifierActive( TNode q, bool active );
94
  /** is quantified formula active?
95
   *
96
   * Returns false if there has been a call to setQuantifierActive( q, false )
97
   * during this instantiation round.
98
   */
99
  bool isQuantifierActive(TNode q) const;
100
  /** is quantified formula asserted */
101
  bool isQuantifierAsserted(TNode q) const;
102
  /** get model basis term */
103
  Node getModelBasisTerm(TypeNode tn);
104
  /** is model basis term */
105
  bool isModelBasisTerm(Node n);
106
  /** get model basis term for op */
107
  Node getModelBasisOpTerm(Node op);
108
  /** get model basis */
109
  Node getModelBasis(Node q, Node n);
110
  /** get model basis arg */
111
  unsigned getModelBasisArg(Node n);
112
  /** get some domain element */
113
  Node getSomeDomainElement(TypeNode tn);
114
  /** initialize representative set for type
115
   *
116
   * This ensures that TheoryModel::d_rep_set
117
   * is initialized for type tn. In particular:
118
   * (1) If tn is an uninitialized (unconstrained)
119
   * uninterpreted sort, then we interpret it
120
   * as a set of size one,
121
   * (2) If tn is a "small" enumerable finite type,
122
   * then we ensure that all its values are in
123
   * TheoryModel::d_rep_set.
124
   *
125
   * Returns true if the initialization was complete,
126
   * in that the set for tn in TheoryModel::d_rep_set
127
   * has all representatives of type tn.
128
   */
129
  bool initializeRepresentativesForType(TypeNode tn);
130
  /**
131
   * Has the term been marked as a model basis term?
132
   */
133
  static bool isModelBasis(TNode n);
134
  /** Get the equality query */
135
  EqualityQuery* getEqualityQuery();
136
137
 protected:
138
  //!!!!!!!!!!!!!!!!!!!!!!! TODO (project #15): temporarily available
139
  QuantifiersEngine* d_qe;
140
  /** The quantifiers registry */
141
  QuantifiersRegistry& d_qreg;
142
  /** Reference to the term registry */
143
  TermRegistry& d_treg;
144
  /** equality query class */
145
  EqualityQuery d_eq_query;
146
  /** list of quantifiers asserted in the current context */
147
  context::CDList<Node> d_forall_asserts;
148
  /**
149
   * The (ordered) list of quantified formulas marked as relevant using
150
   * markRelevant, where the quantified formula q in the most recent
151
   * call to markRelevant comes last in the list.
152
   */
153
  std::vector<Node> d_forall_rlv_vec;
154
  /** The last quantified formula marked as relevant, if one exists. */
155
  Node d_last_forall_rlv;
156
  /**
157
   * The list of asserted quantified formulas, ordered by relevance.
158
   * Relevance is a dynamic partial ordering where q1 < q2 if there has been
159
   * a call to markRelevant( q1 ) after the last call to markRelevant( q2 )
160
   * (or no call to markRelevant( q2 ) has been made).
161
   *
162
   * This list is used primarily as an optimization for conflict-based
163
   * instantiation so that quantifed formulas that have been instantiated
164
   * most recently are processed first, since these are (statistically) more
165
   * likely to have conflicting instantiations.
166
   */
167
  std::vector<Node> d_forall_rlv_assert;
168
  /**
169
   * Whether the above list has been computed. This flag is updated during
170
   * reset_round and is valid within a full effort check.
171
   */
172
  bool d_forallRlvComputed;
173
  /** get variable id */
174
  std::map<Node, std::map<Node, int> > d_quant_var_id;
175
  /** process initialize model for term */
176
  virtual void processInitializeModelForTerm(Node n) {}
177
  /** process initialize quantifier */
178
9128
  virtual void processInitializeQuantifier(Node q) {}
179
  /** process initialize */
180
  virtual void processInitialize(bool ispre) {}
181
182
 private:
183
  // list of inactive quantified formulas
184
  std::map<TNode, bool> d_quant_active;
185
  /** map from types to model basis terms */
186
  std::map<TypeNode, Node> d_model_basis_term;
187
  /** map from ops to model basis terms */
188
  std::map<Node, Node> d_model_basis_op_term;
189
  /** map from instantiation terms to their model basis equivalent */
190
  std::map<Node, Node> d_model_basis_body;
191
  /** map from universal quantifiers to model basis terms */
192
  std::map<Node, std::vector<Node> > d_model_basis_terms;
193
  /** compute model basis arg */
194
  void computeModelBasisArgAttribute(Node n);
195
};/* class FirstOrderModel */
196
197
}/* CVC4::theory::quantifiers namespace */
198
}/* CVC4::theory namespace */
199
}/* CVC4 namespace */
200
201
#endif /* CVC4__FIRST_ORDER_MODEL_H */