1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
|
/********************* */
/*! \file model.h
** \verbatim
** Original author: ajreynol
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief Model class
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY_MODEL_H
#define __CVC4__THEORY_MODEL_H
#include "util/model.h"
#include "theory/uf/equality_engine.h"
#include "theory/rep_set.h"
#include "theory/substitutions.h"
namespace CVC4 {
namespace theory {
class QuantifiersEngine;
class TheoryEngineModelBuilder;
/** Theory Model class
* For Model m, should call m.initialize() before using
*/
class TheoryModel : public Model
{
friend class TheoryEngineModelBuilder;
protected:
/** substitution map for this model */
SubstitutionMap d_substitutions;
public:
TheoryModel( context::Context* c, std::string name, bool enableFuncModels );
virtual ~TheoryModel(){}
/** equality engine containing all known equalities/disequalities */
eq::EqualityEngine d_equalityEngine;
/** map of representatives of equality engine to used representatives in representative set */
std::map< Node, Node > d_reps;
/** stores set of representatives for each type */
RepSet d_rep_set;
/** true/false nodes */
Node d_true;
Node d_false;
protected:
/** reset the model */
virtual void reset();
/**
* Get model value function. This function is called by getValue
*/
Node getModelValue( TNode n );
/** get interpreted value
* This function is called when the value of the node cannot be determined by the theory rewriter
* This should function should return a representative in d_reps
*/
virtual Node getInterpretedValue( TNode n );
public:
/**
* Get value function. This should be called only after a ModelBuilder has called buildModel(...)
* on this model.
*/
Node getValue( TNode n );
/** get existing domain value, with possible exclusions
* This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude
*/
Node getDomainValue( TypeNode tn, std::vector< Node >& exclude );
/** get new domain value
* This function returns a constant term of type tn that is not in d_rep_set.d_type_reps[tn]
* If it cannot find such a node, it returns null.
*/
Node getNewDomainValue( TypeNode tn );
/** complete all values for type
* Calling this function ensures that all terms of type tn exist in d_rep_set.d_type_reps[tn]
*/
void completeDomainValues( TypeNode tn ){
d_rep_set.complete( tn );
}
public:
/** Adds a substitution from x to t. */
void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
/** add term function
* addTerm( n ) will do any model-specific processing necessary for n,
* such as contraining the interpretation of uninterpretted functions,
* and adding n to the equality engine of this model
*/
virtual void addTerm( Node n );
/** assert equality holds in the model */
void assertEquality( Node a, Node b, bool polarity );
/** assert predicate holds in the model */
void assertPredicate( Node a, bool polarity );
/** assert all equalities/predicates in equality engine hold in the model */
void assertEqualityEngine( const eq::EqualityEngine* ee );
/** assert representative
* This function tells the model that n should be the representative of its equivalence class.
* It should be called during model generation, before final representatives are chosen. In the
* case of TheoryEngineModelBuilder, it should be called during Theory's collectModelInfo( ... )
* functions where fullModel = true.
*/
void assertRepresentative( Node n );
public:
/** general queries */
bool hasTerm( Node a );
Node getRepresentative( Node a );
bool areEqual( Node a, Node b );
bool areDisequal( Node a, Node b );
public:
/** get value function for Exprs. */
Expr getValue( Expr expr );
/** get cardinality for sort */
Cardinality getCardinality( Type t );
/** to stream function */
void toStream( std::ostream& out );
public:
/** print representative debug function */
void printRepresentativeDebug( const char* c, Node r );
/** print representative function */
void printRepresentative( std::ostream& out, Node r );
public:
/** whether function models are enabled */
bool d_enableFuncModels;
//necessary information for function models
std::map< Node, std::vector< Node > > d_uf_terms;
std::map< Node, Node > d_uf_models;
};
/** TheoryEngineModelBuilder class
* This model builder will consult all theories in a theory engine for
* collectModelInfo( ... ) when building a model.
*/
class TheoryEngineModelBuilder : public ModelBuilder
{
protected:
/** pointer to theory engine */
TheoryEngine* d_te;
/** process build model */
virtual void processBuildModel( TheoryModel* m, bool fullModel );
/** choose representative for unconstrained equivalence class */
virtual Node chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel );
/** normalize representative */
Node normalizeRepresentative( TheoryModel* m, Node r, std::map< Node, Node >& reps,
std::map< Node, bool >& normalized,
std::map< Node, bool >& normalizing );
Node normalizeNode( TheoryModel* m, Node r, std::map< Node, Node >& reps,
std::map< Node, bool >& normalized,
std::map< Node, bool >& normalizing );
public:
TheoryEngineModelBuilder( TheoryEngine* te );
virtual ~TheoryEngineModelBuilder(){}
/** Build model function.
* Should be called only on TheoryModels m
*/
void buildModel( Model* m, bool fullModel );
};
}
}
#endif
|
