GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/fmf/full_model_check.h Lines: 13 13 100.0 %
Date: 2021-03-22 Branches: 3 6 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file full_model_check.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, 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 Full model check class
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
18
#define CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
19
20
#include "theory/quantifiers/fmf/first_order_model_fmc.h"
21
#include "theory/quantifiers/fmf/model_builder.h"
22
23
namespace CVC4 {
24
namespace theory {
25
namespace quantifiers {
26
namespace fmcheck {
27
28
29
class FirstOrderModelFmc;
30
class FullModelChecker;
31
32
1034542
class EntryTrie
33
{
34
private:
35
  int d_complete;
36
public:
37
498160
  EntryTrie() : d_complete(-1), d_data(-1){}
38
  std::map<Node,EntryTrie> d_child;
39
  int d_data;
40
86685
  void reset() { d_data = -1; d_child.clear(); d_complete = -1; }
41
  void addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index = 0 );
42
  bool hasGeneralization( FirstOrderModelFmc * m, Node c, int index = 0 );
43
  int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index = 0 );
44
  void getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true );
45
};/* class EntryTrie */
46
47
48
304139
class Def
49
{
50
public:
51
  EntryTrie d_et;
52
  //cond is APPLY_UF whose arguments are returned by FullModelChecker::getRepresentative
53
  std::vector< Node > d_cond;
54
  //value is returned by FullModelChecker::getRepresentative
55
  std::vector< Node > d_value;
56
  void basic_simplify( FirstOrderModelFmc * m );
57
private:
58
  enum {
59
    status_unk,
60
    status_redundant,
61
    status_non_redundant
62
  };
63
  std::vector< int > d_status;
64
  bool d_has_simplified;
65
public:
66
86807
  Def() : d_has_simplified(false){}
67
16324
  void reset() {
68
16324
    d_et.reset();
69
16324
    d_cond.clear();
70
16324
    d_value.clear();
71
16324
    d_status.clear();
72
16324
    d_has_simplified = false;
73
16324
  }
74
  bool addEntry( FirstOrderModelFmc * m, Node c, Node v);
75
  Node evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst );
76
  int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst );
77
  void simplify( FullModelChecker * mc, FirstOrderModelFmc * m );
78
  void debugPrint(const char * tr, Node op, FullModelChecker * m);
79
};/* class Def */
80
81
82
1616
class FullModelChecker : public QModelBuilder
83
{
84
protected:
85
  Node d_true;
86
  Node d_false;
87
  std::map<TypeNode, std::map< Node, int > > d_rep_ids;
88
  std::map<Node, Def > d_quant_models;
89
  /**
90
   * The predicate for the quantified formula. This is used to express
91
   * conditions under which the quantified formula is false in the model.
92
   * For example, for quantified formula (forall x:Int, y:U. P), this is
93
   * a predicate of type (Int x U) -> Bool.
94
   */
95
  std::map<Node, Node > d_quant_cond;
96
  /** A set of quantified formulas that cannot be handled by model-based
97
   * quantifier instantiation */
98
  std::unordered_set<Node, NodeHashFunction> d_unhandledQuant;
99
  std::map< TypeNode, Node > d_array_cond;
100
  std::map< Node, Node > d_array_term_cond;
101
  std::map< Node, std::vector< int > > d_star_insts;
102
  //--------------------for preinitialization
103
  /** preInitializeType
104
   *
105
   * This function ensures that the model fm is properly initialized with
106
   * respect to type tn.
107
   *
108
   * In particular, this class relies on the use of "model basis" terms, which
109
   * are distinguished terms that are used to specify default values for
110
   * uninterpreted functions. This method enforces that the model basis term
111
   * occurs in the model for each relevant type T, where a type T is relevant
112
   * if a bound variable is of type T, or an uninterpreted function has an
113
   * argument or a return value of type T.
114
   */
115
  void preInitializeType( FirstOrderModelFmc * fm, TypeNode tn );
116
  /** for each type, an equivalence class of that type from the model */
117
  std::map<TypeNode, Node> d_preinitialized_eqc;
118
  /** map from types to whether we have called the method above */
119
  std::map<TypeNode, bool> d_preinitialized_types;
120
  //--------------------end for preinitialization
121
  Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);
122
  /**
123
   * Exhaustively instantiate quantified formula q based on condition c, which
124
   * indicate the domain to instantiate.
125
   */
126
  bool exhaustiveInstantiate(FirstOrderModelFmc* fm, Node q, Node c);
127
128
 private:
129
  void doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n );
130
131
  void doNegate( Def & dc );
132
  void doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq );
133
  void doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v);
134
  void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, std::vector< Def > & dc );
135
136
  void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d,
137
                               Def & df, std::vector< Def > & dc, int index,
138
                               std::vector< Node > & cond, std::vector<Node> & val );
139
  void doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
140
                                std::map< int, Node > & entries, int index,
141
                                std::vector< Node > & cond, std::vector< Node > & val,
142
                                EntryTrie & curr);
143
144
  void doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n,
145
                             std::vector< Def > & dc, int index,
146
                             std::vector< Node > & cond, std::vector<Node> & val );
147
  int isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );
148
  bool doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );
149
  Node mkCond( std::vector< Node > & cond );
150
  Node mkCondDefault( FirstOrderModelFmc * fm, Node f );
151
  void mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond );
152
  void mkCondVec( Node n, std::vector< Node > & cond );
153
  Node evaluateInterpreted( Node n, std::vector< Node > & vals );
154
  Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
155
156
 public:
157
  FullModelChecker(QuantifiersState& qs, QuantifiersRegistry& qr);
158
159
  void debugPrintCond(const char * tr, Node n, bool dispStar = false);
160
  void debugPrint(const char * tr, Node n, bool dispStar = false);
161
162
  int doExhaustiveInstantiation(FirstOrderModel* fm,
163
                                Node f,
164
                                int effort) override;
165
166
  Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix );
167
168
  /** process build model */
169
  bool preProcessBuildModel(TheoryModel* m) override;
170
  bool processBuildModel(TheoryModel* m) override;
171
172
  bool useSimpleModels();
173
174
 private:
175
  /**
176
   * Register quantified formula.
177
   * This checks whether q can be handled by model-based instantiation and
178
   * initializes the necessary information if so.
179
   */
180
  void registerQuantifiedFormula(Node q);
181
  /** Is quantified formula q handled by model-based instantiation? */
182
  bool isHandled(Node q) const;
183
};/* class FullModelChecker */
184
185
}/* CVC4::theory::quantifiers::fmcheck namespace */
186
}/* CVC4::theory::quantifiers namespace */
187
}/* CVC4::theory namespace */
188
}/* CVC4 namespace */
189
190
#endif /* CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */