diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-14 15:44:21 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-14 15:44:36 -0600 |
commit | eb5debabce433774a0dbfd46745efb8fcf38b8ab (patch) | |
tree | 265975eab00a2919d53eb32c6bb993ed7490cbd4 /src/theory/quantifiers/quant_conflict_find.h | |
parent | 4c7f8d38445f067bb85f38cf3ea343cc92e41ef2 (diff) |
Make QCF more incremental. Fix bug in QCF handling of ITE formulas, add support for ITE terms. Add full-delay inst-when mode. Make strings come before quantifiers in check. Minor cleanup.
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.h')
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.h | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 80e56acbd..9b64a312d 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -61,6 +61,7 @@ private: std::map< int, TNode > d_qni_gterm;
std::map< int, TNode > d_qni_gterm_rep;
std::map< int, int > d_qni_bound;
+ std::vector< int > d_qni_bound_except;
std::map< int, TNode > d_qni_bound_cons;
std::map< int, int > d_qni_bound_cons_var;
std::map< int, int >::iterator d_binding_it;
@@ -81,6 +82,7 @@ public: typ_eq,
typ_formula,
typ_var,
+ typ_ite_var,
typ_top,
};
void debugPrintType( const char * c, short typ, bool isTrace = false );
@@ -156,7 +158,7 @@ private: context::Context* d_c;
context::CDO< bool > d_conflict;
bool d_performCheck;
- //void registerAssertion( Node n );
+ std::vector< Node > d_quant_order;
private:
std::map< Node, Node > d_op_node;
int d_fid_count;
@@ -204,6 +206,8 @@ private: //for equivalence classes std::map< TNode, std::vector< TNode > > d_arg_reps;
//compute arg reps
void computeArgReps( TNode n );
+ //compute
+ void computeUfTerms( TNode f );
public:
enum {
effort_conflict,
@@ -211,10 +215,6 @@ public: effort_mc,
};
short d_effort;
- //for effort_prop
- TNode d_prop_eq[2];
- bool d_prop_pol;
- bool isPropagationSet();
bool areMatchEqual( TNode n1, TNode n2 );
bool areMatchDisequal( TNode n1, TNode n2 );
public:
|