1 /********************* */
2 /*! \file theory_model.h
4 ** Top contributors (to current version):
5 ** Clark Barrett, Morgan Deters, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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
15 #include "cvc4_private.h"
17 #ifndef __CVC4__THEORY__THEORY_MODEL_BUILDER_H
18 #define __CVC4__THEORY__THEORY_MODEL_BUILDER_H
20 #include <unordered_map>
21 #include <unordered_set>
23 #include "theory/theory_model.h"
28 /** TheoryEngineModelBuilder class
30 * This is the class used by TheoryEngine
31 * for constructing TheoryModel objects, which is the class
32 * that represents models for a set of assertions.
34 * A call to TheoryEngineModelBuilder::buildModel(...) is made
35 * after a full effort check passes with no theory solvers
36 * adding lemmas or conflicts, and theory combination passes
37 * with no splits on shared terms. If buildModel is successful,
38 * this will set up the data structures in TheoryModel to represent
39 * a model for the current set of assertions.
41 class TheoryEngineModelBuilder
: public ModelBuilder
43 typedef std::unordered_map
<Node
, Node
, NodeHashFunction
> NodeMap
;
44 typedef std::unordered_set
<Node
, NodeHashFunction
> NodeSet
;
47 TheoryEngineModelBuilder(TheoryEngine
* te
);
48 virtual ~TheoryEngineModelBuilder() {}
49 /** Build model function.
51 * Should be called only on TheoryModels m.
53 * This constructs the model m, via the following steps:
54 * (1) call TheoryEngine::collectModelInfo,
55 * (2) builder-specified pre-processing,
56 * (3) find the equivalence classes of m's
57 * equality engine that initially contain constants,
58 * (4) assign constants to all equivalence classes
59 * of m's equality engine, through alternating
60 * iterations of evaluation and enumeration,
61 * (5) builder-specific processing, which includes assigning total
62 * interpretations to uninterpreted functions.
64 * This function returns false if any of the above
65 * steps results in a lemma sent on an output channel.
66 * Lemmas may be sent on an output channel by this
67 * builder in steps (2) or (5), for instance, if the model we
68 * are building fails to satisfy a quantified formula.
70 bool buildModel(Model
* m
) override
;
71 /** Debug check model.
73 * This throws an assertion failure if the model
74 * contains an equivalence class with two terms t1 and t2
75 * such that t1^M != t2^M.
77 void debugCheckModel(Model
* m
);
80 /** pointer to theory engine */
83 //-----------------------------------virtual functions
84 /** pre-process build model
85 * Do pre-processing specific to this model builder.
86 * Called in step (2) of the build construction,
89 virtual bool preProcessBuildModel(TheoryModel
* m
);
90 /** process build model
91 * Do processing specific to this model builder.
92 * Called in step (5) of the build construction,
94 * By default, this assigns values to each function
95 * that appears in m's equality engine.
97 virtual bool processBuildModel(TheoryModel
* m
);
99 * Check assertions and printing debug information for the model.
100 * Calls after step (5) described above is complete.
102 virtual void debugModel(TheoryModel
* m
) {}
103 //-----------------------------------end virtual functions
107 * A term n is assignable if its value
108 * is unconstrained by a standard model.
109 * Examples of assignable terms are:
111 * - applications of array select,
112 * - applications of datatype selectors,
113 * - applications of uninterpreted functions.
114 * Assignable terms must be first-order, that is,
115 * all instances of the above terms are not
116 * assignable if they have a higher-order (function) type.
118 bool isAssignable(TNode n
);
119 /** add assignable subterms
120 * Adds all assignable subterms of n to tm's equality engine.
122 void addAssignableSubterms(TNode n
, TheoryModel
* tm
, NodeSet
& cache
);
123 /** normalize representative r
125 * This returns a term that is equivalent to r's
126 * interpretation in the model m. It may do so
127 * by rewriting the application of r's operator to the
128 * result of normalizing each of r's children, if
129 * each child is constant.
131 Node
normalize(TheoryModel
* m
, TNode r
, bool evalOnly
);
132 /** assign constant representative
134 * Called when equivalence class eqc is assigned a constant
135 * representative const_rep.
137 * eqc should be a representative of tm's equality engine.
139 void assignConstantRep(TheoryModel
* tm
, Node eqc
, Node const_rep
);
142 * This adds to type_list the list of types that tn is built from.
143 * For example, if tn is (Array Int Bool) and type_list is empty,
144 * then we append ( Int, Bool, (Array Int Bool) ) to type_list.
148 std::vector
<TypeNode
>& type_list
,
149 std::unordered_set
<TypeNode
, TypeNodeHashFunction
>& visiting
);
150 /** assign function f based on the model m.
151 * This construction is based on "table form". For example:
157 * f = (lambda xy. (ite (and (= x 0) (= y 1)) 1
158 * (ite (and (= x 0) (= y 2)) 2
159 * (ite (and (= x 1) (= y 1)) 3 ...)))
161 void assignFunction(TheoryModel
* m
, Node f
);
162 /** assign function f based on the model m.
163 * This construction is based on "dag form". For example:
169 * f = (lambda xy. (ite (= x 0) (ite (= y 1) 1
170 * (ite (= y 2) 2 ...))
171 * (ite (= x 1) (ite (= y 1) 3 ...)
174 * where the above is represented as a directed acyclic graph (dag).
175 * This construction is accomplished by assigning values to (f c)
176 * terms before f, e.g.
177 * (f 0) = (lambda y. (ite (= y 1) 1
178 * (ite (= y 2) 2 ...))
179 * (f 1) = (lambda y. (ite (= y 1) 3 ...))
181 * f = (lambda xy. (ite (= x 0) ((f 0) y)
182 * (ite (= x 1) ((f 1) y) ...))
184 void assignHoFunction(TheoryModel
* m
, Node f
);
187 * Assign all unassigned functions in the model m (those returned by
188 * TheoryModel::getFunctionsToAssign),
189 * using the two functions above. Currently:
190 * If ufHo is disabled, we call assignFunction for all functions.
191 * If ufHo is enabled, we call assignHoFunction.
193 void assignFunctions(TheoryModel
* m
);
197 * A temporary cache mapping terms to their
198 * normalized form, used during buildModel.
200 NodeMap d_normalizedCache
;
201 /** mapping from terms to the constant associated with their equivalence class
203 std::map
<Node
, Node
> d_constantReps
;
205 //------------------------------------for codatatypes
206 /** is v an excluded codatatype value?
208 * If this returns true, then v is a value
209 * that cannot be used during enumeration in step (4)
210 * of model construction.
212 * repSet is the set of representatives of the same type as v,
213 * assertedReps is a map from representatives t,
214 * eqc is the equivalence class that v reside.
216 * This function is used to avoid alpha-equivalent
217 * assignments for codatatype terms, described in
218 * Reynolds/Blanchette CADE 2015. In particular,
219 * this function returns true if v is in
220 * the set V^{x}_I from page 9, where x is eqc
221 * and I is the model we are building.
223 bool isExcludedCdtValue(Node v
,
224 std::set
<Node
>* repSet
,
225 std::map
<Node
, Node
>& assertedReps
,
227 /** is codatatype value match
229 * This returns true if v is r{ eqc -> t } for some t.
230 * If this function returns true, then t above is
233 bool isCdtValueMatch(Node v
, Node r
, Node eqc
, Node
& eqc_m
);
234 //------------------------------------end for codatatypes
236 //---------------------------------for debugging finite model finding
237 /** does type tn involve an uninterpreted sort? */
238 bool involvesUSort(TypeNode tn
);
239 /** is v an excluded value based on uninterpreted sorts?
240 * This gives an assertion failure in the case that v contains
241 * an uninterpreted constant whose index is out of the bounds
242 * specified by eqc_usort_count.
244 bool isExcludedUSortValue(std::map
<TypeNode
, unsigned>& eqc_usort_count
,
246 std::map
<Node
, bool>& visited
);
247 //---------------------------------end for debugging finite model finding
249 }; /* class TheoryEngineModelBuilder */
251 } /* CVC4::theory namespace */
252 } /* CVC4 namespace */
254 #endif /* __CVC4__THEORY__THEORY_MODEL_BUILDER_H */