diff options
Diffstat (limited to 'src/theory/quantifiers/ce_guided_instantiation.h')
| -rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.h | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 81f70d600..c8b41c035 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -126,6 +126,8 @@ private: CegConjecture * d_conj; /** last instantiation by single invocation module? */ bool d_last_inst_si; + /** evaluation axioms */ + std::map< Node, bool > d_eval_axioms; private: //for enforcing fairness /** measure functions */ std::map< TypeNode, Node > d_uf_measure; @@ -140,7 +142,7 @@ private: //for enforcing fairness /** get measure lemmas */ void getMeasureLemmas( Node n, Node v, std::vector< Node >& lems ); /** get eager unfolding */ - void getEagerUnfoldLemmas( std::vector< Node >& lems, Node n, std::map< Node, bool >& visited ); + Node getEagerUnfold( Node n, std::map< Node, Node >& visited ); private: /** check conjecture */ void checkCegConjecture( CegConjecture * conj ); @@ -158,6 +160,7 @@ public: /* Call during quantifier engine's check */ void check( Theory::Effort e, unsigned quant_e ); /* Called for new quantifiers */ + void preRegisterQuantifier( Node q ); void registerQuantifier( Node q ); void assertNode( Node n ); Node getNextDecisionRequest(); |