diff options
Diffstat (limited to 'src/theory/quantifiers/model_builder.h')
-rw-r--r-- | src/theory/quantifiers/model_builder.h | 116 |
1 files changed, 95 insertions, 21 deletions
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index a57ca2b37..a4c38d608 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -46,16 +46,27 @@ protected: /** process build model */ void processBuildModel( TheoryModel* m, bool fullModel ); protected: + //initialize quantifiers, return number of lemmas produced + int initializeQuantifier( Node f ); //analyze model void analyzeModel( FirstOrderModel* fm ); //analyze quantifiers - void analyzeQuantifiers( FirstOrderModel* fm ); + virtual void analyzeQuantifiers( FirstOrderModel* fm ) = 0; //build model void constructModel( FirstOrderModel* fm ); //theory-specific build models void constructModelUf( FirstOrderModel* fm, Node op ); + /** set default value */ + virtual bool shouldSetDefaultValue( Node n ) = 0; //do InstGen techniques for quantifier, return number of lemmas produced - int doInstGen( FirstOrderModel* fm, Node f ); + virtual int doInstGen( FirstOrderModel* fm, Node f ) = 0; +protected: + //map from quantifiers to if are SAT + std::map< Node, bool > d_quant_sat; + //which quantifiers have been initialized + std::map< Node, bool > d_quant_init; + //map from quantifiers to model basis match + std::map< Node, InstMatch > d_quant_basis_match; public: ModelEngineBuilder( context::Context* c, QuantifiersEngine* qe ); virtual ~ModelEngineBuilder(){} @@ -63,40 +74,103 @@ public: int d_addedLemmas; //consider axioms bool d_considerAxioms; -private: ///information for InstGen - //map from quantifiers to if are constant SAT - std::map< Node, bool > d_quant_sat; - //map from quantifiers to their selection literals - std::map< Node, Node > d_quant_selection_lit; - std::map< Node, std::vector< Node > > d_quant_selection_lit_candidates; - //map from quantifiers to their selection literal terms - std::map< Node, std::vector< Node > > d_quant_selection_lit_terms; - //map from terms to the selection literals they exist in - std::map< Node, Node > d_term_selection_lit; - //map from operators to terms that appear in selection literals - std::map< Node, std::vector< Node > > d_op_selection_terms; -public: - //map from quantifiers to model basis match - std::map< Node, InstMatch > d_quant_basis_match; - //options - bool optUseModel(); - bool optInstGen(); - bool optOneQuantPerRoundInstGen(); // set effort void setEffort( int effort ); +public: + //options + virtual bool optUseModel(); + virtual bool optInstGen(); + virtual bool optOneQuantPerRoundInstGen(); + virtual bool optReconsiderFuncConstants(); /** statistics class */ class Statistics { public: IntStat d_pre_sat_quant; IntStat d_pre_nsat_quant; + IntStat d_num_quants_init; + IntStat d_num_quants_init_fail; Statistics(); ~Statistics(); }; Statistics d_statistics; // is quantifier active? bool isQuantifierActive( Node f ); + // is term selected + virtual bool isTermSelected( Node n ) { return false; } };/* class ModelEngineBuilder */ + +class ModelEngineBuilderDefault : public ModelEngineBuilder +{ +private: ///information for (old) InstGen + //map from quantifiers to their selection literals + std::map< Node, Node > d_quant_selection_lit; + std::map< Node, std::vector< Node > > d_quant_selection_lit_candidates; + //map from quantifiers to their selection literal terms + std::map< Node, std::vector< Node > > d_quant_selection_lit_terms; + //map from terms to the selection literals they exist in + std::map< Node, Node > d_term_selection_lit; + //map from operators to terms that appear in selection literals + std::map< Node, std::vector< Node > > d_op_selection_terms; +protected: + //analyze quantifiers + void analyzeQuantifiers( FirstOrderModel* fm ); + //do InstGen techniques for quantifier, return number of lemmas produced + int doInstGen( FirstOrderModel* fm, Node f ); + /** set default value */ + bool shouldSetDefaultValue( Node n ); +private: + //analyze quantifier + void analyzeQuantifier( FirstOrderModel* fm, Node f ); +public: + ModelEngineBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : ModelEngineBuilder( c, qe ){} + ~ModelEngineBuilderDefault(){} + //options + bool optReconsiderFuncConstants() { return true; } +}; + +class ModelEngineBuilderInstGen : public ModelEngineBuilder +{ +private: ///information for (new) InstGen + //map from quantifiers to their selection literals + std::map< Node, Node > d_quant_selection_formula; + //map of terms that are selected + std::map< Node, bool > d_term_selected; + //a collection of InstMatch structures produced for each quantifier + std::map< Node, inst::InstMatchTrie > d_sub_quant_inst_trie; + //children quantifiers for each quantifier, each is an instance + std::map< Node, std::vector< Node > > d_sub_quants; + //instances of each partial instantiation with respect to the root + std::map< Node, InstMatch > d_sub_quant_inst; + //*root* parent of each partial instantiation + std::map< Node, Node > d_sub_quant_parent; +protected: + //analyze quantifiers + void analyzeQuantifiers( FirstOrderModel* fm ); + //do InstGen techniques for quantifier, return number of lemmas produced + int doInstGen( FirstOrderModel* fm, Node f ); + /** set default value */ + bool shouldSetDefaultValue( Node n ); +private: + //analyze quantifier + void analyzeQuantifier( FirstOrderModel* fm, Node f ); + //get selection formula for quantifier body + Node getSelectionFormula( Node fn, Node n, bool polarity, int useOption ); + //set selected terms in term + void setSelectedTerms( Node s ); + //is usable selection literal + bool isUsableSelectionLiteral( Node n, int useOption ); + // get parent quantifier + Node getParentQuantifier( Node f ); + //get parent quantifier match + void getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f ); +public: + ModelEngineBuilderInstGen( context::Context* c, QuantifiersEngine* qe ) : ModelEngineBuilder( c, qe ){} + ~ModelEngineBuilderInstGen(){} + // is term selected + bool isTermSelected( Node n ) { return d_term_selected.find( n )!=d_term_selected.end(); } +}; + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |