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-2013 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/model.h"
21 #include "theory/uf/theory_uf_model.h"
26 class QuantifiersEngine
;
28 namespace quantifiers
{
32 class FirstOrderModelIG
;
34 class FirstOrderModelFmc
;
37 class FirstOrderModel
: public TheoryModel
40 /** whether an axiom is asserted */
41 context::CDO
< bool > d_axiom_asserted
;
42 /** list of quantifiers asserted in the current context */
43 context::CDList
<Node
> d_forall_asserts
;
45 context::CDO
< bool > d_isModelSet
;
46 /** get current model value */
47 virtual Node
getCurrentUfModelValue( Node n
, std::vector
< Node
> & args
, bool partial
) = 0;
48 public: //for Theory Quantifiers:
49 /** assert quantifier */
50 void assertQuantifier( Node n
);
51 /** get number of asserted quantifiers */
52 int getNumAssertedQuantifiers() { return (int)d_forall_asserts
.size(); }
53 /** get asserted quantifier */
54 Node
getAssertedQuantifier( int i
) { return d_forall_asserts
[i
]; }
55 /** bool axiom asserted */
56 bool isAxiomAsserted() { return d_axiom_asserted
; }
57 /** initialize model for term */
58 void initializeModelForTerm( Node n
);
59 virtual void processInitializeModelForTerm( Node n
) = 0;
61 FirstOrderModel( context::Context
* c
, std::string name
);
62 virtual ~FirstOrderModel(){}
63 virtual FirstOrderModelIG
* asFirstOrderModelIG() { return NULL
; }
64 virtual fmcheck::FirstOrderModelFmc
* asFirstOrderModelFmc() { return NULL
; }
65 // initialize the model
66 void initialize( bool considerAxioms
= true );
67 virtual void processInitialize() = 0;
69 void markModelSet() { d_isModelSet
= true; }
71 bool isModelSet() { return d_isModelSet
; }
72 /** get current model value */
73 Node
getCurrentModelValue( Node n
, bool partial
= false );
74 };/* class FirstOrderModel */
77 class FirstOrderModelIG
: public FirstOrderModel
79 public: //for Theory UF:
80 //models for each UF operator
81 std::map
< Node
, uf::UfModelTree
> d_uf_model_tree
;
83 std::map
< Node
, uf::UfModelTreeGenerator
> d_uf_model_gen
;
85 //map from terms to the models used to calculate their value
86 std::map
< Node
, bool > d_eval_uf_use_default
;
87 std::map
< Node
, uf::UfModelTree
> d_eval_uf_model
;
88 void makeEvalUfModel( Node n
);
89 //index ordering to use for each term
90 std::map
< Node
, std::vector
< int > > d_eval_term_index_order
;
91 void makeEvalUfIndexOrder( Node n
);
92 /** get current model value */
93 Node
getCurrentUfModelValue( Node n
, std::vector
< Node
> & args
, bool partial
);
94 //the following functions are for evaluating quantifier bodies
96 FirstOrderModelIG(context::Context
* c
, std::string name
);
97 FirstOrderModelIG
* asFirstOrderModelIG() { return this; }
98 // initialize the model
99 void processInitialize();
100 //for initialize model
101 void processInitializeModelForTerm( Node n
);
102 /** reset evaluation */
103 void resetEvaluate();
104 /** evaluate functions */
105 int evaluate( Node n
, int& depIndex
, RepSetIterator
* ri
);
106 Node
evaluateTerm( Node n
, int& depIndex
, RepSetIterator
* ri
);
112 int d_eval_lits_unknown
;
114 //default evaluate term function
115 Node
evaluateTermDefault( Node n
, int& depIndex
, std::vector
< int >& childDepIndex
, RepSetIterator
* ri
);
116 //temporary storing which literals have failed
117 void clearEvalFailed( int index
);
118 std::map
< Node
, bool > d_eval_failed
;
119 std::map
< int, std::vector
< Node
> > d_eval_failed_lits
;
127 class FirstOrderModelFmc
: public FirstOrderModel
129 friend class FullModelChecker
;
132 QuantifiersEngine
* d_qe
;
134 std::map
<Node
, Def
* > d_models
;
135 std::map
<TypeNode
, Node
> d_model_basis_rep
;
136 std::map
<TypeNode
, Node
> d_type_star
;
137 Node
getUsedRepresentative(Node n
, bool strict
= false);
138 /** get current model value */
139 Node
getCurrentUfModelValue( Node n
, std::vector
< Node
> & args
, bool partial
);
140 void processInitializeModelForTerm(Node n
);
142 FirstOrderModelFmc(QuantifiersEngine
* qe
, context::Context
* c
, std::string name
);
143 FirstOrderModelFmc
* asFirstOrderModelFmc() { return this; }
144 // initialize the model
145 void processInitialize();
147 Node
getFunctionValue(Node op
, const char* argPrefix
);
150 Node
getStar(TypeNode tn
);
151 bool isModelBasisTerm(Node n
);
152 Node
getModelBasisTerm(TypeNode tn
);
153 Node
getSomeDomainElement(TypeNode tn
);
159 }/* CVC4::theory::quantifiers namespace */
160 }/* CVC4::theory namespace */
161 }/* CVC4 namespace */
163 #endif /* __CVC4__FIRST_ORDER_MODEL_H */