diff options
Diffstat (limited to 'src/theory/model.h')
-rw-r--r-- | src/theory/model.h | 81 |
1 files changed, 34 insertions, 47 deletions
diff --git a/src/theory/model.h b/src/theory/model.h index 4a4bf48c9..086e39f3e 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -21,36 +21,13 @@ #include "util/model.h" #include "theory/uf/equality_engine.h" +#include "theory/rep_set.h" +#include "theory/substitutions.h" namespace CVC4 { namespace theory { class QuantifiersEngine; - -/** this class stores a representative set */ -class RepSet { -public: - RepSet(){} - ~RepSet(){} - std::map< TypeNode, std::vector< Node > > d_type_reps; - std::map< Node, int > d_tmap; - /** clear the set */ - void clear(); - /** has type */ - bool hasType( TypeNode tn ) { return d_type_reps.find( tn )!=d_type_reps.end(); } - /** add representative for type */ - void add( Node n ); - /** 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 toStream(std::ostream& out); -}; - -//representative domain -typedef std::vector< int > RepDomain; - class TheoryEngineModelBuilder; /** Theory Model class @@ -66,18 +43,8 @@ protected: * such as contraining the interpretation of uninterpretted functions. */ virtual void addTerm( Node n ) {} -private: - /** List of definitions that the user has given - * This is necessary for supporting the get-model command. - */ - std::vector< Node > d_define_funcs; - std::vector< TypeNode > d_define_types; - std::vector< int > d_defines; -protected: - /** print the value of the function n to stream */ - virtual void toStreamFunction( Node n, std::ostream& out ); - /** print the value of the type tn to stream */ - virtual void toStreamType( TypeNode tn, std::ostream& out ); + /** substitution map for this model */ + SubstitutionMap d_substitutions; public: TheoryModel( context::Context* c, std::string name ); virtual ~TheoryModel(){} @@ -90,7 +57,7 @@ public: /** true/false nodes */ Node d_true; Node d_false; -public: +protected: /** reset the model */ virtual void reset(); /** get interpreted value @@ -98,11 +65,11 @@ public: * This should function should return a representative in d_reps */ virtual Node getInterpretedValue( TNode n ) = 0; + /** + * Get model value function. This function is called by getValue + */ + Node getModelValue( TNode n ); public: - /** add defined function (for get-model) */ - void addDefineFunction( Node n ); - /** add defined type (for get-model) */ - void addDefineType( TypeNode tn ); /** * Get value function. This should be called only after a ModelBuilder has called buildModel(...) * on this model. @@ -117,13 +84,28 @@ public: * If it cannot find such a node, it returns null. */ Node getNewDomainValue( TypeNode tn ); + /** complete all values for type + * Calling this function ensures that all terms of type tn exist in d_rep_set.d_type_reps[tn] + */ + void completeDomainValues( TypeNode tn ){ + d_rep_set.complete( tn ); + } public: + /** Adds a substitution from x to t. */ + void addSubstitution(TNode x, TNode t, bool invalidateCache = true); /** assert equality holds in the model */ void assertEquality( Node a, Node b, bool polarity ); /** assert predicate holds in the model */ void assertPredicate( Node a, bool polarity ); /** assert all equalities/predicates in equality engine hold in the model */ void assertEqualityEngine( const eq::EqualityEngine* ee ); + /** assert representative + * This function tells the model that n should be the representative of its equivalence class. + * It should be called during model generation, before final representatives are chosen. In the + * case of TheoryEngineModelBuilder, it should be called during Theory's collectModelInfo( ... ) + * functions where fullModel = true. + */ + void assertRepresentative( Node n ); public: /** general queries */ bool hasTerm( Node a ); @@ -170,19 +152,24 @@ class TheoryEngineModelBuilder : public ModelBuilder protected: /** pointer to theory engine */ TheoryEngine* d_te; - /** choose representative for unresolved equivalence class */ - void initializeType( TypeNode tn, std::map< TypeNode, bool >& unresolved_types ); /** process build model */ - virtual void processBuildModel( TheoryModel* m ){} + virtual void processBuildModel( TheoryModel* m, bool fullModel ){} /** choose representative for unconstrained equivalence class */ - virtual Node chooseRepresentative( TheoryModel* m, Node eqc ); + virtual Node chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel ); + /** normalize representative */ + Node normalizeRepresentative( TheoryModel* m, Node r, std::map< Node, Node >& reps, + std::map< Node, bool >& normalized, + std::map< Node, bool >& normalizing ); + Node normalizeNode( TheoryModel* m, Node r, std::map< Node, Node >& reps, + std::map< Node, bool >& normalized, + std::map< Node, bool >& normalizing ); public: TheoryEngineModelBuilder( TheoryEngine* te ); virtual ~TheoryEngineModelBuilder(){} /** Build model function. * Should be called only on TheoryModels m */ - void buildModel( Model* m ); + void buildModel( Model* m, bool fullModel ); }; } |