diff options
Diffstat (limited to 'src/theory/quantifiers/model_engine.h')
-rw-r--r-- | src/theory/quantifiers/model_engine.h | 366 |
1 files changed, 71 insertions, 295 deletions
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index cf6691918..b01139826 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Instantiation Engine classes + ** \brief Model Engine classes **/ #include "cvc4_private.h" @@ -21,6 +21,9 @@ #include "theory/quantifiers_engine.h" #include "theory/quantifiers/theory_quantifiers.h" +#include "theory/model.h" +#include "theory/uf/theory_uf_model.h" +#include "theory/quantifiers/relevant_domain.h" namespace CVC4 { namespace theory { @@ -31,312 +34,87 @@ namespace uf{ namespace quantifiers { -/** this class stores a representative alphabet */ -class RepAlphabet { -public: - RepAlphabet(){} - RepAlphabet( RepAlphabet& ra, QuantifiersEngine* qe ); - ~RepAlphabet(){} - std::map< TypeNode, std::vector< Node > > d_type_reps; - std::map< Node, int > d_tmap; - /** clear the alphabet */ - void clear(){ - d_type_reps.clear(); - d_tmap.clear(); - } - /** set the representatives for type */ - void set( TypeNode t, std::vector< Node >& reps ); - /** returns index in d_type_reps for node n */ - int getIndexFor( Node n ) { return d_tmap.find( n )!=d_tmap.end() ? d_tmap[n] : -1; } - /** debug print */ - void debugPrint( const char* c, QuantifiersEngine* qe ); -}; - -class ModelEngine; - -/** this class iterates over a RepAlphabet */ -class RepAlphabetIterator { -private: - void initialize( QuantifiersEngine* qe, Node f, ModelEngine* model ); -public: - RepAlphabetIterator( QuantifiersEngine* qe, Node f, ModelEngine* model ); - RepAlphabetIterator( QuantifiersEngine* qe, Node f, ModelEngine* model, std::vector< int >& indexOrder ); - ~RepAlphabetIterator(){} - //pointer to quantifier - Node d_f; - //pointer to model - ModelEngine* d_model; - //index we are considering - std::vector< int > d_index; - //ordering for variables we are indexing over - // for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 }, - // then we consider instantiations in this order: - // a/x a/y a/z - // a/x b/y a/z - // b/x a/y a/z - // b/x b/y a/z - // ... - std::vector< int > d_index_order; - //variables to index they are considered at - // for example, if d_index_order = { 2, 0, 1 } - // then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 } - std::map< int, int > d_var_order; - //the instantiation constants of d_f - std::vector< Node > d_ic; - //the current terms we are considering - std::vector< Node > d_terms; -public: - /** increment the iterator */ - void increment2( QuantifiersEngine* qe, int counter ); - void increment( QuantifiersEngine* qe ); - /** is the iterator finished? */ - bool isFinished(); - /** produce the match that this iterator represents */ - void getMatch( QuantifiersEngine* qe, InstMatch& m ); - /** get the i_th term we are considering */ - Node getTerm( int i ); - /** get the number of terms we are considering */ - int getNumTerms() { return d_f[0].getNumChildren(); } - /** refresh d_term to be current with d_index */ - void calculateTerms( QuantifiersEngine* qe ); - /** debug print */ - void debugPrint( const char* c ); - void debugPrintSmall( const char* c ); - //for debugging - int d_inst_tried; - int d_inst_tests; -}; - - -class UfModelTree -{ -public: - UfModelTree(){} - /** the data */ - std::map< Node, UfModelTree > d_data; - /** the value of this tree node (if all paths lead to same value) */ - Node d_value; -public: - //is this model tree empty? - bool isEmpty() { return d_data.empty(); } - //clear - void clear(){ - d_data.clear(); - d_value = Node::null(); - } - /** setValue function - * - * For each argument of n with ModelBasisAttribute() set to true will be considered default arguments if ground=false - * - */ - void setValue( QuantifiersEngine* qe, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ); - /** getValue function - * - * returns $val, the value of ground term n - * Say n is f( t_0...t_n ) - * depIndex is the index for which every term of the form f( t_0 ... t_depIndex, *,... * ) is equal to $val - * for example, if g( x_0, x_1, x_2 ) := lambda x_0 x_1 x_2. if( x_1==a ) b else c, - * then g( a, a, a ) would return b with depIndex = 1 - * If ground = true, we are asking whether the term n is constant (assumes that all non-model basis arguments are ground) - * - */ - Node getValue( QuantifiersEngine* qe, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ); - ///** getConstant Value function - // * - // * given term n, where n may contain model basis arguments - // * if n is constant for its entire domain, then this function returns the value of its domain - // * otherwise, it returns null - // * for example, if f( x_0, x_1 ) := if( x_0 = a ) b else if( x_1 = a ) a else b, - // * then f( a, e ) would return b, while f( e, a ) would return null - // * - // */ - Node getConstantValue( QuantifiersEngine* qe, Node n, std::vector< int >& indexOrder, int argIndex ); - /** simplify function */ - void simplify( Node op, Node defaultVal, int argIndex ); - // is total ? - bool isTotal( Node op, int argIndex ); -public: - void debugPrint( const char* c, QuantifiersEngine* qe, std::vector< int >& indexOrder, int ind = 0, int arg = 0 ); -}; -class UfModelTreeOrdered +//the model builder +class ModelEngineBuilder : public TheoryEngineModelBuilder { -private: - Node d_op; - std::vector< int > d_index_order; - UfModelTree d_tree; -public: - UfModelTreeOrdered(){} - UfModelTreeOrdered( Node op ) : d_op( op ){ - TypeNode tn = d_op.getType(); - for( int i=0; i<(int)(tn.getNumChildren()-1); i++ ){ - d_index_order.push_back( i ); - } - } - UfModelTreeOrdered( Node op, std::vector< int >& indexOrder ) : d_op( op ){ - d_index_order.insert( d_index_order.end(), indexOrder.begin(), indexOrder.end() ); - } - bool isEmpty() { return d_tree.isEmpty(); } - void clear() { d_tree.clear(); } - void setValue( QuantifiersEngine* qe, Node n, Node v, bool ground = true ){ - d_tree.setValue( qe, n, v, d_index_order, ground, 0 ); - } - Node getValue( QuantifiersEngine* qe, Node n, int& depIndex ){ - return d_tree.getValue( qe, n, d_index_order, depIndex, 0 ); - } - Node getConstantValue( QuantifiersEngine* qe, Node n ) { - return d_tree.getConstantValue( qe, n, d_index_order, 0 ); - } - void simplify() { d_tree.simplify( d_op, Node::null(), 0 ); } - bool isTotal() { return d_tree.isTotal( d_op, 0 ); } -public: - void debugPrint( const char* c, QuantifiersEngine* qe, int ind = 0 ){ - d_tree.debugPrint( c, qe, d_index_order, ind ); - } -}; - -class UfModel -{ -//public: - //std::map< Node, std::vector< Node > > d_reqs[2]; - //std::map< Node, std::map< Node, std::vector< Node > > > d_eq_reqs[2]; - ///** add requirement */ - //void addRequirement( Node f, Node p, bool phase ) { d_reqs[ phase ? 1 : 0 ][ f ].push_back( p ); } - ///** add equality requirement */ - //void addEqRequirement( Node f, Node t, Node te, bool phase ) { d_eq_reqs[ phase ? 1 : 0 ][ f ][ t ].push_back( te ); } -private: - Node d_op; - ModelEngine* d_me; - std::vector< Node > d_ground_asserts; - std::vector< Node > d_ground_asserts_reps; - bool d_model_constructed; - //store for set values - std::map< Node, Node > d_set_values[2]; - // preferences for default values - std::vector< Node > d_values; - std::map< Node, std::vector< Node > > d_value_pro_con[2]; - /** set value */ - void setValue( Node n, Node v, bool ground = true ); - /** set model */ - void setModel(); - /** clear model */ - void clearModel(); -public: - UfModel(){} - UfModel( Node op, ModelEngine* qe ); - ~UfModel(){} - //data structure that stores the model - UfModelTreeOrdered d_tree; - //quantifiers that are satisfied because of the constant definition of d_op - bool d_reconsider_model; -public: - /** debug print */ - void debugPrint( const char* c ); - /** get constant value */ - Node getConstantValue( QuantifiersEngine* qe, Node n ); - /** is empty */ - bool isEmpty() { return d_ground_asserts.empty(); } - /** is constant */ - bool isConstant(); -public: - /** build model */ - void buildModel(); - /** make model */ - void makeModel( QuantifiersEngine* qe, UfModelTreeOrdered& tree ); -public: - /** set value preference */ - void setValuePreference( Node f, Node n, bool isPro ); +protected: + //quantifiers engine + QuantifiersEngine* d_qe; + //map from operators to model preference data + std::map< Node, uf::UfModelPreferenceData > d_uf_prefs; + /** choose representative */ + Node chooseRepresentative( TheoryModel* tm, Node eqc ); + /** use constants for representatives */ + void processBuildModel( TheoryModel* m ); + //analyze quantifiers + void analyzeQuantifiers( FirstOrderModel* fm ); + //build model + void finishBuildModel( FirstOrderModel* fm ); + //theory-specific build models + void finishBuildModelUf( FirstOrderModel* fm, uf::UfModel& model ); + //do InstGen techniques for quantifier, return number of lemmas produced + int doInstGen( FirstOrderModel* fm, Node f ); +public: + ModelEngineBuilder( QuantifiersEngine* qe ); + virtual ~ModelEngineBuilder(){} +public: + /** number of lemmas generated while building model */ + int d_addedLemmas; + //map from quantifiers to if are constant SAT + std::map< Node, bool > d_quant_sat; + //map from quantifiers to the instantiation literals that their model is dependent upon + std::map< Node, std::vector< Node > > d_quant_selection_lits; +public: + //map from quantifiers to model basis match + std::map< Node, InstMatch > d_quant_basis_match; + //options + bool optUseModel(); + bool optInstGen(); + bool optOneQuantPerRoundInstGen(); + /** statistics class */ + class Statistics { + public: + IntStat d_pre_sat_quant; + IntStat d_pre_nsat_quant; + Statistics(); + ~Statistics(); + }; + Statistics d_statistics; }; - - - class ModelEngine : public QuantifiersModule { - friend class UfModel; - friend class RepAlphabetIterator; + friend class uf::UfModel; + friend class RepSetIterator; private: - TheoryQuantifiers* d_th; - QuantifiersEngine* d_quantEngine; - uf::StrongSolverTheoryUf* d_ss; + /** builder class */ + ModelEngineBuilder d_builder; +private: //data maintained globally: //which quantifiers have been initialized std::map< Node, bool > d_quant_init; - //map from ops to model basis terms - std::map< Node, Node > d_model_basis_term; - //map from instantiation terms to their model basis equivalent - std::map< Node, Node > d_model_basis; - //the model we are working with - RepAlphabet d_ra; - std::map< Node, UfModel > d_uf_model; - ////map from model basis terms to quantifiers that are pro/con their definition - //std::map< Node, std::vector< Node > > d_quant_pro_con[2]; - //map from quantifiers to model basis terms that are pro the definition of - std::map< Node, std::vector< Node > > d_pro_con_quant[2]; - //map from quantifiers to if are constant SAT - std::map< Node, bool > d_quant_sat; +private: //analysis of current model: + //relevant domain + RelevantDomain d_rel_domain; private: - int evaluate( RepAlphabetIterator* rai, Node n, int& depIndex ); - int evaluateEquality( Node n1, Node n2, Node gn1, Node gn2, std::vector< Node >& fv_deps ); - Node evaluateTerm( Node n, Node gn, std::vector< Node >& fv_deps ); - //temporary storing which literals have failed - void clearEvalFailed( int index ); - std::map< Node, bool > d_eval_failed; - std::map< int, std::vector< Node > > d_eval_failed_lits; - ////temporary storing for values/free variable dependencies - //std::map< Node, Node > d_eval_term_vals; - //std::map< Node, std::map< Node, std::vector< Node > > > d_eval_term_fv_deps; + //options + bool optOneInstPerQuantRound(); + bool optUseRelevantDomain(); + bool optOneQuantPerRound(); private: - //map from terms to the models used to calculate their value - std::map< Node, UfModelTreeOrdered > d_eval_term_model; - std::map< Node, bool > d_eval_term_use_default_model; - void makeEvalTermModel( Node n ); - //index ordering to use for each term - std::map< Node, std::vector< int > > d_eval_term_index_order; - int getMaxVariableNum( int n ); - void makeEvalTermIndexOrder( Node n ); -public: - void increment( RepAlphabetIterator* rai ); + //initialize quantifiers, return number of lemmas produced + int initializeQuantifier( Node f ); + //exhaustively instantiate quantifier (possibly using mbqi), return number of lemmas produced + int exhaustiveInstantiate( Node f, bool useRelInstDomain = false ); private: - //queries about equality - bool areEqual( Node a, Node b ); - bool areDisequal( Node a, Node b ); -private: - bool useModel(); -private: - //initialize quantifiers, return false if lemma needed to be added - bool initializeQuantifier( Node f ); - //build representatives - void buildRepresentatives(); - //initialize model - void initializeModel(); - //analyze quantifiers - void analyzeQuantifiers(); - //instantiate quantifier, return number of lemmas produced - int instantiateQuantifier( Node f ); -private: - //register instantiation terms with their corresponding model basis terms - void registerModelBasis( Node n, Node gn ); - //for building UF model - void initializeUf( Node n ); - void collectUfTerms( Node n, std::vector< Node >& terms ); - void initializeUfModel( Node op ); - //void processPredicate( Node f, Node p, bool phase ); - //void processEquality( Node f, Node eq, bool phase ); + //temporary statistics + int d_triedLemmas; + int d_testLemmas; + int d_totalLemmas; + int d_relevantLemmas; public: - ModelEngine( TheoryQuantifiers* th ); + ModelEngine( QuantifiersEngine* qe ); ~ModelEngine(){} - //get quantifiers engine - QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; } - //get representatives - RepAlphabet* getReps() { return &d_ra; } - //get arbitrary element - Node getArbitraryElement( TypeNode tn, std::vector< Node >& exclude ); - //get model basis term - Node getModelBasisTerm( TypeNode tn, int i = 0 ); - //get model basis term for op - Node getModelBasisApplyUfTerm( Node op ); - //is model basis term for op - bool isModelBasisTerm( Node op, Node n ); public: void check( Theory::Effort e ); void registerQuantifier( Node f ); @@ -349,8 +127,6 @@ public: class Statistics { public: IntStat d_inst_rounds; - IntStat d_pre_sat_quant; - IntStat d_pre_nsat_quant; IntStat d_eval_formulas; IntStat d_eval_eqs; IntStat d_eval_uf_terms; |