diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-26 15:49:23 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-26 15:49:23 +0200 |
| commit | 7c3790db478c4f06e65ef0f777317a4c6a803059 (patch) | |
| tree | 89f95e1e0db42a580980b34f58ee1315b73004db /src/theory/quantifiers_engine.h | |
| parent | d9c22c34d122a34d8a8a914936d9186be9a638fe (diff) | |
Minor improvements to cbqi, fix bug in solving with vts symbols, round up for integer lower bounds. Add presolve infrastructure to quantifiers engine, modify --cbqi-prereg-inst.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 101aa43cd..2658d09f0 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -53,6 +53,8 @@ public: QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; } /** initialize */ virtual void finishInit() {} + /** presolve */ + virtual void presolve() {} /* whether this module needs to check this round */ virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; } /* whether this module needs a model built */ @@ -251,6 +253,8 @@ public: public: /** initialize */ void finishInit(); + /** presolve */ + void presolve(); /** check at level */ void check( Theory::Effort e ); /** register quantifier */ |