diff options
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.h')
-rwxr-xr-x | src/theory/quantifiers/inst_strategy_cbqi.h | 90 |
1 files changed, 43 insertions, 47 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 8ed59778b..c9f62243f 100755 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -34,25 +34,64 @@ namespace quantifiers { class InstStrategyCbqi : public QuantifiersModule { typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; + typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap; protected: bool d_cbqi_set_quant_inactive; bool d_incomplete_check; /** whether we have added cbqi lemma */ NodeSet d_added_cbqi_lemma; + /** whether we have added cbqi lemma */ + NodeSet d_elim_quants; + /** parent guards */ + std::map< Node, std::vector< Node > > d_parent_quant; + std::map< Node, std::vector< Node > > d_children_quant; + std::map< Node, bool > d_active_quant; /** whether we have instantiated quantified formulas */ //NodeSet d_added_inst; - /** whether to do cbqi for this quantified formula */ - std::map< Node, bool > d_do_cbqi; + /** whether to do cbqi for this quantified formula 0 : no, 2 : yes, 1 : yes but not exclusively, -1 : heuristically */ + std::map< Node, int > d_do_cbqi; /** register ce lemma */ + bool registerCbqiLemma( Node q ); virtual void registerCounterexampleLemma( Node q, Node lem ); /** has added cbqi lemma */ bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); } /** helper functions */ - bool hasNonCbqiVariable( Node q ); + int hasNonCbqiVariable( Node q ); bool hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ); + /** get next decision request with dependency checking */ + Node getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc ); /** process functions */ virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; virtual void process( Node q, Theory::Effort effort, int e ) = 0; +protected: + //for identification + uint64_t d_qid_count; + //nested qe map + std::map< Node, Node > d_nested_qe; + //mark ids on quantifiers + Node getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited ); + // id to ce quant + std::map< Node, Node > d_id_to_ce_quant; + std::map< Node, Node > d_ce_quant_to_id; + //do nested quantifier elimination recursive + Node doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts ); + Node doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts ); + //elimination information (for delayed elimination) + class NestedQEInfo { + public: + NestedQEInfo() : d_doVts(false){} + ~NestedQEInfo(){} + Node d_q; + std::vector< Node > d_inst_terms; + bool d_doVts; + }; + std::map< Node, NestedQEInfo > d_nested_qe_info; + NodeIntMap d_nested_qe_waitlist_size; + NodeIntMap d_nested_qe_waitlist_proc; + std::map< Node, std::vector< Node > > d_nested_qe_waitlist; +public: + //do nested quantifier elimination + Node doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts ); public: InstStrategyCbqi( QuantifiersEngine * qe ); ~InstStrategyCbqi() throw(); @@ -64,56 +103,13 @@ public: void reset_round( Theory::Effort e ); void check( Theory::Effort e, unsigned quant_e ); bool checkComplete(); + bool checkCompleteFor( Node q ); void preRegisterQuantifier( Node q ); void registerQuantifier( Node q ); /** get next decision request */ Node getNextDecisionRequest(); }; - -class InstStrategySimplex : public InstStrategyCbqi { -protected: - /** reference to theory arithmetic */ - arith::TheoryArith* d_th; - /** quantifiers we should process */ - std::map< Node, bool > d_quantActive; - /** delta */ - std::map< TypeNode, Node > d_deltas; - /** for each quantifier, simplex rows */ - std::map< Node, std::vector< arith::ArithVar > > d_instRows; - /** tableaux */ - std::map< Node, std::map< arith::ArithVar, Node > > d_tableaux_term; - std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_tableaux_ce_term; - std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_tableaux; - /** ce tableaux */ - std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_ceTableaux; - /** get value */ - //Node getTableauxValue( Node n, bool minus_delta = false ); - Node getTableauxValue( arith::ArithVar v, bool minus_delta = false ); - /** do instantiation */ - bool doInstantiation( Node f, Node ic, Node term, arith::ArithVar x, InstMatch& m, Node var ); - bool doInstantiation2( Node f, Node ic, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false ); - /** add term to row */ - void addTermToRow( Node ic, arith::ArithVar x, Node n, NodeBuilder<>& t ); - /** print debug */ - void debugPrint( const char* c ); -private: - /** */ - int d_counter; - /** constants */ - Node d_zero; - Node d_negOne; - /** process functions */ - void processResetInstantiationRound( Theory::Effort effort ); - void process( Node f, Theory::Effort effort, int e ); -public: - InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie ); - ~InstStrategySimplex() throw() {} - /** identify */ - std::string identify() const { return std::string("Simplex"); } -}; - - //generalized counterexample guided quantifier instantiation class InstStrategyCegqi; |