diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-14 12:11:14 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-14 12:11:14 -0500 |
commit | 126966a8d9cb6564b0ac31dd20f32059cc35156f (patch) | |
tree | a9de10f9e2efad78437aa05c5c832c6f9d885c05 /src/theory/quantifiers/model_builder.h | |
parent | 24d60fa5654a32b09dc8de79b7704fbf40051478 (diff) |
Refactoring to separate old and new model building/checking code.
Diffstat (limited to 'src/theory/quantifiers/model_builder.h')
-rw-r--r-- | src/theory/quantifiers/model_builder.h | 73 |
1 files changed, 43 insertions, 30 deletions
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 31448acee..2b38f3381 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -25,6 +25,35 @@ namespace CVC4 { namespace theory { namespace quantifiers { + +class QModelBuilder : public TheoryEngineModelBuilder +{ +protected: + //the model we are working with + context::CDO< FirstOrderModel* > d_curr_model; + //quantifiers engine + QuantifiersEngine* d_qe; +public: + QModelBuilder( context::Context* c, QuantifiersEngine* qe ); + virtual ~QModelBuilder(){} + // is quantifier active? + virtual bool isQuantifierActive( Node f ) { return true; } + //do exhaustive instantiation + virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas ) { return false; } + //whether to construct model + virtual bool optUseModel(); + /** number of lemmas generated while building model */ + int d_addedLemmas; + //consider axioms + bool d_considerAxioms; + /** exist instantiation ? */ + virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; } +}; + + + + + /** Attribute true for nodes that should not be used when considered for inst-gen basis */ struct BasisNoMatchAttributeId {}; /** use the special for boolean flag */ @@ -47,17 +76,13 @@ public: /** model builder class * This class is capable of building candidate models based on the current quantified formulas * that are asserted. Use: - * (1) call ModelEngineBuilder::buildModel( m, false );, where m is a FirstOrderModel + * (1) call QModelBuilder::buildModel( m, false );, where m is a FirstOrderModel * (2) if candidate model is determined to be a real model, - then call ModelEngineBuilder::buildModel( m, true ); + then call QModelBuilder::buildModel( m, true ); */ -class ModelEngineBuilder : public TheoryEngineModelBuilder +class QModelBuilderIG : public QModelBuilder { protected: - //quantifiers engine - QuantifiersEngine* d_qe; - //the model we are working with - context::CDO< FirstOrderModel* > d_curr_model; //map from operators to model preference data std::map< Node, uf::UfModelPreferenceData > d_uf_prefs; //built model uf @@ -90,25 +115,15 @@ protected: //helper functions /** term has constant definition */ bool hasConstantDefinition( Node n ); public: - ModelEngineBuilder( context::Context* c, QuantifiersEngine* qe ); - virtual ~ModelEngineBuilder(){} - /** number of lemmas generated while building model */ - int d_addedLemmas; - //consider axioms - bool d_considerAxioms; - // set effort - void setEffort( int effort ); + QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ); + virtual ~QModelBuilderIG(){} //debug model void debugModel( FirstOrderModel* fm ); public: - //whether to construct model - virtual bool optUseModel(); //whether to add inst-gen lemmas virtual bool optInstGen(); //whether to only consider only quantifier per round of inst-gen virtual bool optOneQuantPerRoundInstGen(); - //whether we should exhaustively instantiate quantifiers where inst-gen is not working - virtual bool optExhInstNonInstGenQuant(); /** statistics class */ class Statistics { public: @@ -120,18 +135,16 @@ public: ~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; } - /** exist instantiation ? */ - virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; } /** quantifier has inst-gen definition */ virtual bool hasInstGen( Node f ) = 0; /** did inst gen this round? */ bool didInstGen() { return d_didInstGen; } + // is quantifier active? + bool isQuantifierActive( Node f ); //temporary stats int d_numQuantSat; @@ -140,10 +153,10 @@ public: int d_numQuantNoSelForm; //temporary stat int d_instGenMatches; -};/* class ModelEngineBuilder */ +};/* class QModelBuilder */ -class ModelEngineBuilderDefault : public ModelEngineBuilder +class QModelBuilderDefault : public QModelBuilderIG { private: ///information for (old) InstGen //map from quantifiers to their selection literals @@ -167,15 +180,15 @@ protected: //theory-specific build models void constructModelUf( FirstOrderModel* fm, Node op ); public: - ModelEngineBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : ModelEngineBuilder( c, qe ){} - ~ModelEngineBuilderDefault(){} + QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){} + ~QModelBuilderDefault(){} //options bool optReconsiderFuncConstants() { return true; } //has inst gen bool hasInstGen( Node f ) { return !d_quant_selection_lit[f].isNull(); } }; -class ModelEngineBuilderInstGen : public ModelEngineBuilder +class QModelBuilderInstGen : public QModelBuilderIG { private: ///information for (new) InstGen //map from quantifiers to their selection formulas @@ -217,8 +230,8 @@ private: //get parent quantifier Node getParentQuantifier( Node f ) { return d_sub_quant_parent.find( f )==d_sub_quant_parent.end() ? f : d_sub_quant_parent[f]; } public: - ModelEngineBuilderInstGen( context::Context* c, QuantifiersEngine* qe ) : ModelEngineBuilder( c, qe ){} - ~ModelEngineBuilderInstGen(){} + QModelBuilderInstGen( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){} + ~QModelBuilderInstGen(){} // is term selected bool isTermSelected( Node n ) { return d_term_selected.find( n )!=d_term_selected.end(); } /** exist instantiation ? */ |