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-2016 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_H
18 #define __CVC4__THEORY__THEORY_MODEL_H
20 #include "smt/model.h"
21 #include "theory/uf/equality_engine.h"
22 #include "theory/rep_set.h"
23 #include "theory/substitutions.h"
24 #include "theory/type_enumerator.h"
31 * For Model m, should call m.initialize() before using.
33 class TheoryModel
: public Model
35 friend class TheoryEngineModelBuilder
;
37 /** substitution map for this model */
38 SubstitutionMap d_substitutions
;
39 context::CDO
<bool> d_modelBuilt
;
41 TheoryModel(context::Context
* c
, std::string name
, bool enableFuncModels
);
42 virtual ~TheoryModel() throw();
44 /** special local context for our equalityEngine so we can clear it independently of search context */
45 context::Context
* d_eeContext
;
46 /** equality engine containing all known equalities/disequalities */
47 eq::EqualityEngine
* d_equalityEngine
;
48 /** map of representatives of equality engine to used representatives in representative set */
49 std::map
< Node
, Node
> d_reps
;
50 /** stores set of representatives for each type */
52 /** true/false nodes */
55 mutable std::hash_map
<Node
, Node
, NodeHashFunction
> d_modelCache
;
56 /** comment stream to include in printing */
57 std::stringstream d_comment_str
;
59 void getComments(std::ostream
& out
) const;
61 /** reset the model */
64 * Get model value function. This function is called by getValue
66 Node
getModelValue(TNode n
, bool hasBoundVars
= false, bool useDontCares
= false) const;
69 bool isBuilt() { return d_modelBuilt
.get(); }
71 * Get value function. This should be called only after a ModelBuilder has called buildModel(...)
74 Node
getValue( TNode n
, bool useDontCares
= false ) const;
76 /** get existing domain value, with possible exclusions
77 * This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude
79 Node
getDomainValue( TypeNode tn
, std::vector
< Node
>& exclude
);
81 /** Adds a substitution from x to t. */
82 void addSubstitution(TNode x
, TNode t
, bool invalidateCache
= true);
84 * addTerm( n ) will do any model-specific processing necessary for n,
85 * such as constraining the interpretation of uninterpreted functions,
86 * and adding n to the equality engine of this model
88 virtual void addTerm(TNode n
);
89 /** assert equality holds in the model */
90 void assertEquality(TNode a
, TNode b
, bool polarity
);
91 /** assert predicate holds in the model */
92 void assertPredicate(TNode a
, bool polarity
);
93 /** assert all equalities/predicates in equality engine hold in the model */
94 void assertEqualityEngine(const eq::EqualityEngine
* ee
, std::set
<Node
>* termSet
= NULL
);
95 /** assert representative
96 * This function tells the model that n should be the representative of its equivalence class.
97 * It should be called during model generation, before final representatives are chosen. In the
98 * case of TheoryEngineModelBuilder, it should be called during Theory's collectModelInfo( ... )
99 * functions where fullModel = true.
101 void assertRepresentative(TNode n
);
103 /** general queries */
104 bool hasTerm(TNode a
);
105 Node
getRepresentative(TNode a
);
106 bool areEqual(TNode a
, TNode b
);
107 bool areDisequal(TNode a
, TNode b
);
109 /** return whether this node is a don't-care */
110 bool isDontCare(Expr expr
) const;
111 /** get value function for Exprs. */
112 Expr
getValue( Expr expr
) const;
113 /** get cardinality for sort */
114 Cardinality
getCardinality( Type t
) const;
116 /** print representative debug function */
117 void printRepresentativeDebug( const char* c
, Node r
);
118 /** print representative function */
119 void printRepresentative( std::ostream
& out
, Node r
);
121 /** whether function models are enabled */
122 bool d_enableFuncModels
;
123 //necessary information for function models
124 std::map
< Node
, std::vector
< Node
> > d_uf_terms
;
125 std::map
< Node
, Node
> d_uf_models
;
126 };/* class TheoryModel */
129 * Class that encapsulates a map from types to sets of nodes
133 typedef std::hash_map
<TypeNode
, std::set
<Node
>*, TypeNodeHashFunction
> TypeSetMap
;
134 typedef std::hash_map
<TypeNode
, TypeEnumerator
*, TypeNodeHashFunction
> TypeToTypeEnumMap
;
135 typedef TypeSetMap::iterator iterator
;
136 typedef TypeSetMap::const_iterator const_iterator
;
138 TypeSetMap d_typeSet
;
139 TypeToTypeEnumMap d_teMap
;
140 TypeEnumeratorProperties
* d_tep
;
143 TypeSet() : d_tep(NULL
) {}
146 for (it
= d_typeSet
.begin(); it
!= d_typeSet
.end(); ++it
) {
147 if ((*it
).second
!= NULL
) {
151 TypeToTypeEnumMap::iterator it2
;
152 for (it2
= d_teMap
.begin(); it2
!= d_teMap
.end(); ++it2
) {
153 if ((*it2
).second
!= NULL
) {
154 delete (*it2
).second
;
158 void setTypeEnumeratorProperties( TypeEnumeratorProperties
* tep
) { d_tep
= tep
; }
159 void add(TypeNode t
, TNode n
)
161 iterator it
= d_typeSet
.find(t
);
163 if (it
== d_typeSet
.end()) {
164 s
= new std::set
<Node
>;
173 std::set
<Node
>* getSet(TypeNode t
) const
175 const_iterator it
= d_typeSet
.find(t
);
176 if (it
== d_typeSet
.end()) {
182 Node
nextTypeEnum(TypeNode t
, bool useBaseType
= false)
185 TypeToTypeEnumMap::iterator it
= d_teMap
.find(t
);
186 if (it
== d_teMap
.end()) {
187 te
= new TypeEnumerator(t
, d_tep
);
193 if (te
->isFinished()) {
200 iterator itSet
= d_typeSet
.find(t
);
202 if (itSet
== d_typeSet
.end()) {
203 s
= new std::set
<Node
>;
210 while (s
->find(n
) != s
->end()) {
212 if (te
->isFinished()) {
224 return d_typeSet
.empty();
229 return d_typeSet
.begin();
234 return d_typeSet
.end();
237 static TypeNode
getType(iterator it
)
242 static std::set
<Node
>& getSet(iterator it
)
244 return *(*it
).second
;
247 };/* class TypeSet */
249 /** TheoryEngineModelBuilder class
250 * This model builder will consult all theories in a theory engine for
251 * collectModelInfo( ... ) when building a model.
253 class TheoryEngineModelBuilder
: public ModelBuilder
256 /** pointer to theory engine */
258 typedef std::hash_map
<Node
, Node
, NodeHashFunction
> NodeMap
;
259 NodeMap d_normalizedCache
;
260 typedef std::hash_set
<Node
, NodeHashFunction
> NodeSet
;
262 /** process build model */
263 virtual void preProcessBuildModel(TheoryModel
* m
, bool fullModel
);
264 virtual void processBuildModel(TheoryModel
* m
, bool fullModel
);
265 /** normalize representative */
266 Node
normalize(TheoryModel
* m
, TNode r
, std::map
<Node
, Node
>& constantReps
, bool evalOnly
);
267 bool isAssignable(TNode n
);
268 void checkTerms(TNode n
, TheoryModel
* tm
, NodeSet
& cache
);
269 void assignConstantRep( TheoryModel
* tm
, std::map
<Node
, Node
>& constantReps
, Node eqc
, Node const_rep
, bool fullModel
);
270 /** is v an excluded codatatype value */
271 bool isExcludedCdtValue( Node v
, std::set
<Node
>* repSet
, std::map
< Node
, Node
>& assertedReps
, Node eqc
);
272 bool isCdtValueMatch( Node v
, Node r
, Node eqc
, Node
& eqc_m
);
273 /** involves usort */
274 bool involvesUSort( TypeNode tn
);
275 bool isExcludedUSortValue( std::map
< TypeNode
, unsigned >& eqc_usort_count
, Node v
, std::map
< Node
, bool >& visited
);
277 TheoryEngineModelBuilder(TheoryEngine
* te
);
278 virtual ~TheoryEngineModelBuilder(){}
279 /** Build model function.
280 * Should be called only on TheoryModels m
282 void buildModel(Model
* m
, bool fullModel
);
283 };/* class TheoryEngineModelBuilder */
285 }/* CVC4::theory namespace */
286 }/* CVC4 namespace */
288 #endif /* __CVC4__THEORY__THEORY_MODEL_H */