diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-10 23:27:39 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-10 23:27:45 +0200 |
commit | 089d232454e89dc44a6ca2136f9b408c9335d8f1 (patch) | |
tree | 21c815088431e820ccc3b3e42fa05e5a5a9bea68 /src/theory/quantifiers/ce_guided_instantiation.h | |
parent | 859ab54a3cc8afdc01980e3e97e91b45480586dc (diff) |
Initial draft of CEGQI.
Diffstat (limited to 'src/theory/quantifiers/ce_guided_instantiation.h')
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.h | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 7861deffa..6139f8f59 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -25,16 +25,59 @@ namespace CVC4 { namespace theory { namespace quantifiers { + + class CegInstantiation : public QuantifiersModule { + typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; +private: + class CegConjecture { + public: + CegConjecture(); + /** quantified formula */ + Node d_quant; + /** guard */ + Node d_guard; + /** base instantiation */ + Node d_base_inst; + /** guard split */ + Node d_guard_split; + /** list of constants for quantified formula */ + std::vector< Node > d_candidates; + /** list of variables on inner quantification */ + std::vector< Node > d_inner_vars; + /** is assigned */ + bool isAssigned() { return !d_quant.isNull(); } + /** assign */ + void assign( Node q ); + /** initialize guard */ + void initializeGuard( QuantifiersEngine * qe ); + }; + /** the quantified formula stating the synthesis conjecture */ + CegConjecture d_conj; + /** is conjecture active */ + context::CDO< bool > d_conj_active; + /** is conjecture infeasible */ + context::CDO< bool > d_conj_infeasible; + /** assertions for guards */ + NodeBoolMap d_guard_assertions; +private: + /** check conjecture */ + void checkCegConjecture( CegConjecture * conj ); + /** get model value */ + Node getModelValue( Node n ); + /** get model term */ + Node getModelTerm( Node n ); public: CegInstantiation( QuantifiersEngine * qe, context::Context* c ); public: + bool needsCheck( Theory::Effort e ); /* Call during quantifier engine's check */ void check( Theory::Effort e, unsigned quant_e ); /* Called for new quantifiers */ void registerQuantifier( Node q ); void assertNode( Node n ); + Node getNextDecisionRequest(); /** Identify this module (for debugging, dynamic configuration, etc..) */ std::string identify() const { return "CegInstantiation"; } }; |