From 8d3446768446f16e71dca48bdf14d4ed767756aa Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 1 Aug 2014 15:16:17 +0200 Subject: Minor cleanup from previous commit. Better organization for how quantifiers modules check (introduce QuantifiersEngine::QEffort). --- src/theory/quantifiers/quant_conflict_find.h | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'src/theory/quantifiers/quant_conflict_find.h') 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: -- cgit v1.2.3