diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-18 22:50:05 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-18 22:50:05 -0600 |
commit | f47f24528f5d19ac0affd572f3d34c090e97f9f9 (patch) | |
tree | 6a21c1964d862f99d9137f968881a0da33c59d1d /src/theory/quantifiers_engine.h | |
parent | 793361d81f0766c6a28ff699ed5447d9b8f8c123 (diff) |
Implement dynamic splitting for quantified formulas. Minor refactoring of reductions in quantifiers engine.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 28fcbbc85..c5c88487b 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -64,8 +64,8 @@ public: virtual void check( Theory::Effort e, unsigned quant_e ) = 0; /* check was complete (e.g. no lemmas implies a model) */ virtual bool checkComplete() { return true; } - /* Called for new quantifiers */ - virtual void preRegisterQuantifier( Node q ) {} + /* Called for new quantified formulas */ + virtual void preRegisterQuantifier( Node q ) { } /* Called for new quantifiers after owners are finalized */ virtual void registerQuantifier( Node q ) = 0; virtual void assertNode( Node n ) {} @@ -99,6 +99,7 @@ namespace quantifiers { class QuantEqualityEngine; class FullSaturation; class InstStrategyCbqi; + class QuantDSplit; }/* CVC4::theory::quantifiers */ namespace inst { @@ -157,6 +158,8 @@ private: quantifiers::FullSaturation * d_fs; /** counterexample-based quantifier instantiation */ quantifiers::InstStrategyCbqi * d_i_cbqi; + /** quantifiers splitting */ + quantifiers::QuantDSplit * d_qsplit; public: //effort levels enum { QEFFORT_CONFLICT, @@ -253,6 +256,8 @@ public: //modules quantifiers::FullSaturation * getFullSaturation() { return d_fs; } /** get inst strategy cbqi */ quantifiers::InstStrategyCbqi * getInstStrategyCbqi() { return d_i_cbqi; } + /** get quantifiers splitting */ + quantifiers::QuantDSplit * getQuantDSplit() { return d_qsplit; } private: /** owner of quantified formulas */ std::map< Node, QuantifiersModule * > d_owner; @@ -281,7 +286,7 @@ public: /** get next decision request */ Node getNextDecisionRequest(); private: - /** reduce quantifier */ + /** reduceQuantifier, return true if reduced */ bool reduceQuantifier( Node q ); /** compute term vector */ void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ); |