diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-23 15:28:24 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-23 15:28:24 +0000 |
commit | b11f6d3a27d33b9075e57b37f77ad9d11732fce5 (patch) | |
tree | b00e257f54c8adebe15f92927fc7b51cb61887c7 /src/theory/quantifiers/model_builder.h | |
parent | 19f0a337307ce0e424b12acf6102829d81dbbf99 (diff) |
more updates to inst gen: fixed partial instantiations, recognize duplicate defaults for uf
Diffstat (limited to 'src/theory/quantifiers/model_builder.h')
-rw-r--r-- | src/theory/quantifiers/model_builder.h | 77 |
1 files changed, 48 insertions, 29 deletions
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index a4c38d608..e2f422a0a 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -23,6 +23,27 @@ namespace CVC4 { namespace theory { + +/** Attribute true for nodes that should not be used when considered for inst-gen basis */ +struct BasisNoMatchAttributeId {}; +/** use the special for boolean flag */ +typedef expr::Attribute< BasisNoMatchAttributeId, + bool, + expr::attr::NullCleanupStrategy, + true // context dependent + > BasisNoMatchAttribute; + +class TermArgBasisTrie { +private: + bool addTerm2( QuantifiersEngine* qe, Node n, int argIndex ); +public: + /** the data */ + std::map< Node, TermArgBasisTrie > d_data; +public: + bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); } +};/* class TermArgBasisTrie */ + + namespace quantifiers { /** model builder class @@ -44,27 +65,25 @@ protected: //built model uf std::map< Node, bool > d_uf_model_constructed; /** process build model */ - void processBuildModel( TheoryModel* m, bool fullModel ); + virtual void processBuildModel( TheoryModel* m, bool fullModel ); protected: - //initialize quantifiers, return number of lemmas produced - int initializeQuantifier( Node f ); + //reset + virtual void reset( FirstOrderModel* fm ) = 0; + //initialize quantifiers, return number of lemmas produced, fp is the parent of quantifier f + virtual int initializeQuantifier( Node f, Node fp ); //analyze model - void analyzeModel( FirstOrderModel* fm ); + virtual void analyzeModel( FirstOrderModel* fm ); //analyze quantifiers - 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; + virtual void analyzeQuantifier( FirstOrderModel* fm, Node f ) = 0; //do InstGen techniques for quantifier, return number of lemmas produced virtual int doInstGen( FirstOrderModel* fm, Node f ) = 0; + //theory-specific build models + virtual void constructModelUf( FirstOrderModel* fm, Node op ) = 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; + std::map< Node, bool > d_quant_basis_match_added; //map from quantifiers to model basis match std::map< Node, InstMatch > d_quant_basis_match; public: @@ -81,20 +100,21 @@ public: 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; + IntStat d_num_quants_init_success; Statistics(); ~Statistics(); }; Statistics d_statistics; // is quantifier active? bool isQuantifierActive( Node f ); + // is term active + bool isTermActive( Node n ); // is term selected virtual bool isTermSelected( Node n ) { return false; } };/* class ModelEngineBuilder */ @@ -113,15 +133,14 @@ private: ///information for (old) InstGen //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: + //reset + void reset( FirstOrderModel* fm ); //analyze quantifier void analyzeQuantifier( FirstOrderModel* fm, Node f ); + //do InstGen techniques for quantifier, return number of lemmas produced + int doInstGen( FirstOrderModel* fm, Node f ); + //theory-specific build models + void constructModelUf( FirstOrderModel* fm, Node op ); public: ModelEngineBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : ModelEngineBuilder( c, qe ){} ~ModelEngineBuilderDefault(){} @@ -145,23 +164,23 @@ private: ///information for (new) InstGen //*root* parent of each partial instantiation std::map< Node, Node > d_sub_quant_parent; protected: - //analyze quantifiers - void analyzeQuantifiers( FirstOrderModel* fm ); + //reset + void reset( FirstOrderModel* fm ); + //initialize quantifiers, return number of lemmas produced, fp is the parent of quantifier f + int initializeQuantifier( Node f, Node fp ); + //analyze quantifier + void analyzeQuantifier( FirstOrderModel* fm, Node f ); //do InstGen techniques for quantifier, return number of lemmas produced int doInstGen( FirstOrderModel* fm, Node f ); - /** set default value */ - bool shouldSetDefaultValue( Node n ); + //theory-specific build models + void constructModelUf( FirstOrderModel* fm, Node op ); 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: |