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/ce_guided_single_inv.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/ce_guided_single_inv.h')
| -rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 54f762720..eb99fc4f6 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -72,7 +72,7 @@ public: //delta Node d_n_delta; //check : add instantiations based on valuation of d_vars - void check(); + bool check(); // get delta lemmas : on-demand force minimality of d_n_delta void getDeltaLemmas( std::vector< Node >& lems ); }; |