diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-05 19:56:42 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-05 19:56:42 +0200 |
| commit | ba56661b4a49d4b470c6298d3531324b3bf15005 (patch) | |
| tree | 6dee0cde13ab4e86a6bde22bf130e1d3f70c2a6f /src/theory/quantifiers/inst_strategy_cbqi.h | |
| parent | 69769dae4886621f82c2905b82db727bf2e8cf3f (diff) | |
Add options --partial-triggers, --elim-taut-quant, improve robustness of --purify-triggers. Enable --quant-alpha-equiv by default. Fix fairness issue when combining cbqi+E-matching. Avoid unecessary delta lemmas. Update casc scripts.
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.h')
| -rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 13e8cf54b..d59690c84 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -104,6 +104,7 @@ private: Node d_curr_quant; bool d_check_delta_lemma; bool d_check_delta_lemma_lc; + bool d_used_delta; /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); int process( Node f, Theory::Effort effort, int e ); |