diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-08-01 15:16:17 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-08-01 15:16:17 +0200 |
commit | 8d3446768446f16e71dca48bdf14d4ed767756aa (patch) | |
tree | ab8e01fdb9fe7e5f4f7db5aa378a424f19488f0c /src/theory/quantifiers/quant_conflict_find.h | |
parent | a9f4d3e2aed0c6d8d8b218c5f5d2bc95af2d45a6 (diff) |
Minor cleanup from previous commit. Better organization for how quantifiers modules check (introduce QuantifiersEngine::QEffort).
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.h')
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.h | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 1f3635e78..d8f1c8e6f 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -166,7 +166,6 @@ class QuantConflictFind : public QuantifiersModule private:
context::Context* d_c;
context::CDO< bool > d_conflict;
- bool d_performCheck;
std::vector< Node > d_quant_order;
std::map< Kind, Node > d_zero;
//for storing nodes created during t-constraint solving (prevents memory leaks)
@@ -220,12 +219,12 @@ public: void merge( Node a, Node b );
/** assert disequal */
void assertDisequal( Node a, Node b );
+ /** needs check */
+ bool needsCheck( Theory::Effort level );
/** reset round */
void reset_round( Theory::Effort level );
/** check */
- void check( Theory::Effort level );
- /** needs check */
- bool needsCheck( Theory::Effort level );
+ void check( Theory::Effort level, unsigned quant_e );
private:
bool d_needs_computeRelEqr;
public:
|