diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-07 17:38:53 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-07 17:38:59 +0100 |
| commit | 4ad0191e20e4d812d9a5dc3a733153cb10f6d728 (patch) | |
| tree | f25fa219a0d464ca7a30b40d27fa45b05ff33638 /src/theory/quantifiers/quant_conflict_find.h | |
| parent | 3a3a57583fd8bd4af5c3b99b0047c9b20de38bb1 (diff) | |
Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor improvement to performance of E-matching.
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.h')
| -rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 93e1f72a6..b2dc680f2 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -118,6 +118,7 @@ public: QuantInfo() : d_mg( NULL ) {}
~QuantInfo() { delete d_mg; }
std::vector< TNode > d_vars;
+ std::vector< TypeNode > d_var_types;
std::map< TNode, int > d_var_num;
std::vector< int > d_tsym_vars;
std::map< TNode, bool > d_inMatchConstraint;
|