diff options
Diffstat (limited to 'src/theory/quantifiers/model_engine.h')
-rw-r--r-- | src/theory/quantifiers/model_engine.h | 369 |
1 files changed, 369 insertions, 0 deletions
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h new file mode 100644 index 000000000..4031efdf9 --- /dev/null +++ b/src/theory/quantifiers/model_engine.h @@ -0,0 +1,369 @@ +/********************* */ +/*! \file instantiation_engine.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Instantiation Engine classes + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__MODEL_ENGINE_H +#define __CVC4__MODEL_ENGINE_H + +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/theory_quantifiers.h" + +namespace CVC4 { +namespace theory { + +namespace uf{ + class StrongSolverTheoryUf; +} + +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 +{ +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 ); +}; + + + + +class ModelEngine : public QuantifiersModule +{ + friend class UfModel; + friend class RepAlphabetIterator; +private: + TheoryQuantifiers* d_th; + QuantifiersEngine* d_quantEngine; + uf::StrongSolverTheoryUf* d_ss; + //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: + 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; +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 ); +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 ); +public: + ModelEngine( TheoryQuantifiers* th ); + ~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 ); + void assertNode( Node f ); + Node explain(TNode n){ return Node::null(); } + void propagate( Theory::Effort level ){} + void debugPrint( const char* c ); +public: + /** statistics class */ + 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; + IntStat d_num_quants_init; + IntStat d_num_quants_init_fail; + Statistics(); + ~Statistics(); + }; + Statistics d_statistics; +}; + +} +} +} + +#endif |