diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-28 12:48:18 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-28 12:48:18 +0100 |
| commit | e6b097f5f43405951561994009e8d7e6ed8772f4 (patch) | |
| tree | d59b3a1c90d6d198d9b845295695903dfc8b4925 /src/theory/quantifiers/ce_guided_instantiation.h | |
| parent | 670cc5fccd6e98e88c9eeedfede07d053faad26e (diff) | |
Initial work on --cegqi-si-partial, refactoring.
Diffstat (limited to 'src/theory/quantifiers/ce_guided_instantiation.h')
| -rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.h | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 8aa2e2c26..82c57b3d8 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -33,10 +33,6 @@ private: QuantifiersEngine * d_qe; public: CegConjecture( QuantifiersEngine * qe, context::Context* c ); - /** is conjecture active */ - context::CDO< bool > d_active; - /** is conjecture infeasible */ - context::CDO< bool > d_infeasible; /** quantified formula asserted */ Node d_assert_quant; /** quantified formula (after processing) */ @@ -87,6 +83,8 @@ public: //for fairness CegqiFairMode getCegqiFairMode(); /** is single invocation */ bool isSingleInvocation(); + /** is single invocation */ + bool isFullySingleInvocation(); /** needs check */ bool needsCheck(); /** preregister conjecture */ |