1 /********************* */
2 /*! \file first_order_model.h
4 ** Original author: Andrew Reynolds
5 ** Major contributors: Morgan Deters
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Model extended classes
15 #include "cvc4_private.h"
17 #ifndef __CVC4__FIRST_ORDER_MODEL_H
18 #define __CVC4__FIRST_ORDER_MODEL_H
20 #include "theory/theory_model.h"
21 #include "theory/uf/theory_uf_model.h"
22 #include "expr/attribute.h"
27 class QuantifiersEngine
;
29 namespace quantifiers
{
33 class FirstOrderModelIG
;
36 class FirstOrderModelFmc
;
37 }/* CVC4::theory::quantifiers::fmcheck namespace */
39 class FirstOrderModelQInt
;
40 class FirstOrderModelAbs
;
42 struct IsStarAttributeId
{};
43 typedef expr::Attribute
<IsStarAttributeId
, bool> IsStarAttribute
;
45 class FirstOrderModel
: public TheoryModel
49 QuantifiersEngine
* d_qe
;
50 /** whether an axiom is asserted */
51 context::CDO
< bool > d_axiom_asserted
;
52 /** list of quantifiers asserted in the current context */
53 context::CDList
<Node
> d_forall_asserts
;
55 context::CDO
< bool > d_isModelSet
;
56 /** get variable id */
57 std::map
< Node
, std::map
< Node
, int > > d_quant_var_id
;
58 /** get current model value */
59 virtual Node
getCurrentUfModelValue( Node n
, std::vector
< Node
> & args
, bool partial
) = 0;
60 public: //for Theory Quantifiers:
61 /** assert quantifier */
62 void assertQuantifier( Node n
);
63 /** get number of asserted quantifiers */
64 int getNumAssertedQuantifiers() { return (int)d_forall_asserts
.size(); }
65 /** get asserted quantifier */
66 Node
getAssertedQuantifier( int i
) { return d_forall_asserts
[i
]; }
67 /** bool axiom asserted */
68 bool isAxiomAsserted() { return d_axiom_asserted
; }
69 /** initialize model for term */
70 void initializeModelForTerm( Node n
);
71 virtual void processInitializeModelForTerm( Node n
) = 0;
72 virtual void processInitializeQuantifier( Node q
) {}
74 FirstOrderModel(QuantifiersEngine
* qe
, context::Context
* c
, std::string name
);
75 virtual ~FirstOrderModel() {}
76 virtual FirstOrderModelIG
* asFirstOrderModelIG() { return NULL
; }
77 virtual fmcheck::FirstOrderModelFmc
* asFirstOrderModelFmc() { return NULL
; }
78 virtual FirstOrderModelQInt
* asFirstOrderModelQInt() { return NULL
; }
79 virtual FirstOrderModelAbs
* asFirstOrderModelAbs() { return NULL
; }
80 // initialize the model
81 void initialize( bool considerAxioms
= true );
82 virtual void processInitialize( bool ispre
) = 0;
84 void markModelSet() { d_isModelSet
= true; }
86 bool isModelSet() { return d_isModelSet
; }
87 /** get current model value */
88 Node
getCurrentModelValue( Node n
, bool partial
= false );
89 /** get variable id */
90 int getVariableId(TNode q
, TNode n
) {
91 return d_quant_var_id
.find( q
)!=d_quant_var_id
.end() ? d_quant_var_id
[q
][n
] : -1;
93 /** get some domain element */
94 Node
getSomeDomainElement(TypeNode tn
);
96 //list of inactive quantified formulas
97 std::map
< TNode
, bool > d_quant_active
;
101 /** set quantified formula active/inactive
102 * a quantified formula may be set inactive if for instance:
103 * - it is entailed by other quantified formulas
105 void setQuantifierActive( TNode q
, bool active
);
106 /** is quantified formula active */
107 bool isQuantifierActive( TNode q
);
108 };/* class FirstOrderModel */
111 class FirstOrderModelIG
: public FirstOrderModel
113 public: //for Theory UF:
114 //models for each UF operator
115 std::map
< Node
, uf::UfModelTree
> d_uf_model_tree
;
117 std::map
< Node
, uf::UfModelTreeGenerator
> d_uf_model_gen
;
119 //map from terms to the models used to calculate their value
120 std::map
< Node
, bool > d_eval_uf_use_default
;
121 std::map
< Node
, uf::UfModelTree
> d_eval_uf_model
;
122 void makeEvalUfModel( Node n
);
123 //index ordering to use for each term
124 std::map
< Node
, std::vector
< int > > d_eval_term_index_order
;
125 void makeEvalUfIndexOrder( Node n
);
126 /** get current model value */
127 Node
getCurrentUfModelValue( Node n
, std::vector
< Node
> & args
, bool partial
);
128 //the following functions are for evaluating quantifier bodies
130 FirstOrderModelIG(QuantifiersEngine
* qe
, context::Context
* c
, std::string name
);
131 FirstOrderModelIG
* asFirstOrderModelIG() { return this; }
132 // initialize the model
133 void processInitialize( bool ispre
);
134 //for initialize model
135 void processInitializeModelForTerm( Node n
);
136 /** reset evaluation */
137 void resetEvaluate();
138 /** evaluate functions */
139 int evaluate( Node n
, int& depIndex
, RepSetIterator
* ri
);
140 Node
evaluateTerm( Node n
, int& depIndex
, RepSetIterator
* ri
);
146 int d_eval_lits_unknown
;
148 //default evaluate term function
149 Node
evaluateTermDefault( Node n
, int& depIndex
, std::vector
< int >& childDepIndex
, RepSetIterator
* ri
);
150 //temporary storing which literals have failed
151 void clearEvalFailed( int index
);
152 std::map
< Node
, bool > d_eval_failed
;
153 std::map
< int, std::vector
< Node
> > d_eval_failed_lits
;
154 };/* class FirstOrderModelIG */
161 class FirstOrderModelFmc
: public FirstOrderModel
163 friend class FullModelChecker
;
166 std::map
<Node
, Def
* > d_models
;
167 std::map
<TypeNode
, Node
> d_model_basis_rep
;
168 std::map
<TypeNode
, Node
> d_type_star
;
170 Node
getUsedRepresentative(Node n
, bool strict
= false);
171 /** get current model value */
172 Node
getCurrentUfModelValue( Node n
, std::vector
< Node
> & args
, bool partial
);
173 void processInitializeModelForTerm(Node n
);
175 FirstOrderModelFmc(QuantifiersEngine
* qe
, context::Context
* c
, std::string name
);
176 virtual ~FirstOrderModelFmc();
177 FirstOrderModelFmc
* asFirstOrderModelFmc() { return this; }
178 // initialize the model
179 void processInitialize( bool ispre
);
180 Node
getFunctionValue(Node op
, const char* argPrefix
);
183 Node
getStar(TypeNode tn
);
184 Node
getStarElement(TypeNode tn
);
185 bool isModelBasisTerm(Node n
);
186 Node
getModelBasisTerm(TypeNode tn
);
187 bool isInterval(Node n
);
188 Node
getInterval( Node lb
, Node ub
);
189 bool isInRange( Node v
, Node i
);
190 };/* class FirstOrderModelFmc */
192 }/* CVC4::theory::quantifiers::fmcheck namespace */
197 class FirstOrderModelQInt
: public FirstOrderModel
199 friend class QIntervalBuilder
;
201 /** uf op to some representation */
202 std::map
<Node
, QIntDef
* > d_models
;
203 /** representatives to ids */
204 std::map
< Node
, int > d_rep_id
;
205 std::map
< TypeNode
, Node
> d_min
;
206 std::map
< TypeNode
, Node
> d_max
;
207 /** quantifiers to information regarding variable ordering */
208 std::map
<Node
, QuantVarOrder
* > d_var_order
;
209 /** get current model value */
210 Node
getCurrentUfModelValue( Node n
, std::vector
< Node
> & args
, bool partial
);
211 void processInitializeModelForTerm(Node n
);
213 FirstOrderModelQInt(QuantifiersEngine
* qe
, context::Context
* c
, std::string name
);
214 FirstOrderModelQInt
* asFirstOrderModelQInt() { return this; }
215 void processInitialize( bool ispre
);
216 Node
getFunctionValue(Node op
, const char* argPrefix
);
218 Node
getUsedRepresentative( Node n
);
219 int getRepId( Node n
) { return d_rep_id
.find( n
)==d_rep_id
.end() ? -1 : d_rep_id
[n
]; }
220 bool isLessThan( Node v1
, Node v2
);
221 Node
getMin( Node v1
, Node v2
);
222 Node
getMax( Node v1
, Node v2
);
223 Node
getMinimum( TypeNode tn
) { return getNext( tn
, Node::null() ); }
224 Node
getMaximum( TypeNode tn
);
225 bool isMinimum( Node n
) { return n
==getMinimum( n
.getType() ); }
226 bool isMaximum( Node n
) { return n
==getMaximum( n
.getType() ); }
227 Node
getNext( TypeNode tn
, Node v
);
228 Node
getPrev( TypeNode tn
, Node v
);
229 bool doMeet( Node l1
, Node u1
, Node l2
, Node u2
, Node
& lr
, Node
& ur
);
230 QuantVarOrder
* getVarOrder( Node q
) { return d_var_order
[q
]; }
232 void processInitializeQuantifier( Node q
) ;
233 unsigned getOrderedNumVars( Node q
);
234 TypeNode
getOrderedVarType( Node q
, int i
);
235 int getOrderedVarNumToVarNum( Node q
, int i
);
236 };/* class FirstOrderModelQInt */
240 class FirstOrderModelAbs
: public FirstOrderModel
243 std::map
< Node
, AbsDef
* > d_models
;
244 std::map
< Node
, bool > d_models_valid
;
245 std::map
< TNode
, unsigned > d_rep_id
;
246 std::map
< TypeNode
, unsigned > d_domain
;
247 std::map
< Node
, std::vector
< int > > d_var_order
;
248 std::map
< Node
, std::map
< int, int > > d_var_index
;
250 /** get current model value */
251 Node
getCurrentUfModelValue( Node n
, std::vector
< Node
> & args
, bool partial
);
252 void processInitializeModelForTerm(Node n
);
253 void processInitializeQuantifier( Node q
);
254 void collectEqVars( TNode q
, TNode n
, std::map
< int, bool >& eq_vars
);
256 FirstOrderModelAbs(QuantifiersEngine
* qe
, context::Context
* c
, std::string name
);
257 FirstOrderModelAbs
* asFirstOrderModelAbs() { return this; }
258 void processInitialize( bool ispre
);
259 unsigned getRepresentativeId( TNode n
);
260 TNode
getUsedRepresentative( TNode n
);
261 bool isValidType( TypeNode tn
) { return d_domain
.find( tn
)!=d_domain
.end(); }
262 Node
getFunctionValue(Node op
, const char* argPrefix
);
263 Node
getVariable( Node q
, unsigned i
);
266 }/* CVC4::theory::quantifiers namespace */
267 }/* CVC4::theory namespace */
268 }/* CVC4 namespace */
270 #endif /* __CVC4__FIRST_ORDER_MODEL_H */