1 /********************* */
2 /*! \file first_order_model.h
4 ** Original author: ajreynol
5 ** Major contributors: mdeters
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 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"
22 #include "theory/arrays/theory_arrays_model.h"
27 class QuantifiersEngine
;
29 namespace quantifiers
{
33 class FirstOrderModel
: public TheoryModel
36 //for initialize model
37 void initializeModelForTerm( Node n
);
38 /** whether an axiom is asserted */
39 context::CDO
< bool > d_axiom_asserted
;
40 /** list of quantifiers asserted in the current context */
41 context::CDList
<Node
> d_forall_asserts
;
43 context::CDO
< bool > d_isModelSet
;
44 public: //for Theory UF:
45 //models for each UF operator
46 std::map
< Node
, uf::UfModelTree
> d_uf_model_tree
;
48 std::map
< Node
, uf::UfModelTreeGenerator
> d_uf_model_gen
;
50 //map from terms to the models used to calculate their value
51 std::map
< Node
, bool > d_eval_uf_use_default
;
52 std::map
< Node
, uf::UfModelTree
> d_eval_uf_model
;
53 void makeEvalUfModel( Node n
);
54 //index ordering to use for each term
55 std::map
< Node
, std::vector
< int > > d_eval_term_index_order
;
56 void makeEvalUfIndexOrder( Node n
);
57 public: //for Theory Arrays:
58 //default value for each non-store array
59 std::map
< Node
, arrays::ArrayModel
> d_array_model
;
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
; }
70 FirstOrderModel( context::Context
* c
, std::string name
);
71 virtual ~FirstOrderModel(){}
74 // initialize the model
75 void initialize( bool considerAxioms
= true );
77 void markModelSet() { d_isModelSet
= true; }
79 bool isModelSet() { return d_isModelSet
; }
80 //the following functions are for evaluating quantifier bodies
82 /** reset evaluation */
84 /** evaluate functions */
85 int evaluate( Node n
, int& depIndex
, RepSetIterator
* ri
);
86 Node
evaluateTerm( Node n
, int& depIndex
, RepSetIterator
* ri
);
92 int d_eval_lits_unknown
;
94 //default evaluate term function
95 Node
evaluateTermDefault( Node n
, int& depIndex
, std::vector
< int >& childDepIndex
, RepSetIterator
* ri
);
96 //temporary storing which literals have failed
97 void clearEvalFailed( int index
);
98 std::map
< Node
, bool > d_eval_failed
;
99 std::map
< int, std::vector
< Node
> > d_eval_failed_lits
;
100 };/* class FirstOrderModel */
102 }/* CVC4::theory::quantifiers namespace */
103 }/* CVC4::theory namespace */
104 }/* CVC4 namespace */
106 #endif /* __CVC4__FIRST_ORDER_MODEL_H */