diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-02 16:54:10 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-02 16:54:10 +0200 |
| commit | 69769dae4886621f82c2905b82db727bf2e8cf3f (patch) | |
| tree | fde0dfe43acb6fc7f0f07251de91db6ed8c2a148 /src/theory/quantifiers/inst_strategy_cbqi.h | |
| parent | d475d255f3c61380524517cd9b97725dcb0c9c22 (diff) | |
On-demand upper bound lemmas for deltas in quantified LRA (for casc). Force no macros-quant in incremental. Update casc TFN script.
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.h')
| -rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 586cd492c..13e8cf54b 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -100,8 +100,10 @@ private: CegqiOutputInstStrategy * d_out; std::map< Node, CegInstantiator * > d_cinst; Node d_n_delta; + Node d_n_delta_ub; Node d_curr_quant; bool d_check_delta_lemma; + bool d_check_delta_lemma_lc; /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); int process( Node f, Theory::Effort effort, int e ); |