diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-24 18:34:25 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-24 18:34:25 +0200 |
| commit | d7dc7c2b3038b862af5ea55e7cf6b1fc4e1fe684 (patch) | |
| tree | d6c229a2659bfcb3cdf7c7c786414ecc1e59e61c /src/theory/quantifiers/ce_guided_instantiation.h | |
| parent | 1ec95c559074ed7575a0165deb16fcee45920e9f (diff) | |
Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts symbols. Move presolve for sygus to cbqi. Enable --cbqi-recurse by default, add option --cbqi-min-bound. Enable qcf for finite model finding by default.
Diffstat (limited to 'src/theory/quantifiers/ce_guided_instantiation.h')
| -rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index af3a19d62..9228f11b6 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -29,8 +29,10 @@ namespace quantifiers { /** a synthesis conjecture */ class CegConjecture { +private: + QuantifiersEngine * d_qe; public: - CegConjecture( context::Context* c ); + CegConjecture( QuantifiersEngine * qe, context::Context* c ); /** is conjecture active */ context::CDO< bool > d_active; /** is conjecture infeasible */ @@ -65,7 +67,7 @@ public: /** refine count */ unsigned d_refine_count; /** assign */ - void assign( QuantifiersEngine * qe, Node q ); + void assign( Node q ); /** is assigned */ bool isAssigned() { return !d_quant.isNull(); } /** current extential quantifeirs whose couterexamples we must refine */ |