src/theory/theory_model.h

   1 /*********************                                                        */
   2 /*! \file theory_model.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Clark Barrett, Morgan Deters, Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Model class
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef __CVC4__THEORY__THEORY_MODEL_H
  18 #define __CVC4__THEORY__THEORY_MODEL_H
  19
  20 #include "smt/model.h"
  21 #include "theory/uf/equality_engine.h"
  22 #include "theory/rep_set.h"
  23 #include "theory/substitutions.h"
  24 #include "theory/type_enumerator.h"
  25
  26 namespace CVC4 {
  27 namespace theory {
  28
  29 /**
  30  * Theory Model class.
  31  *    For Model m, should call m.initialize() before using.
  32  */
  33 class TheoryModel : public Model
  34 {
  35   friend class TheoryEngineModelBuilder;
  36 protected:
  37   /** substitution map for this model */
  38   SubstitutionMap d_substitutions;
  39   context::CDO<bool> d_modelBuilt;
  40 public:
  41   TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
  42   virtual ~TheoryModel() throw();
  43
  44   /** special local context for our equalityEngine so we can clear it independently of search context */
  45   context::Context* d_eeContext;
  46   /** equality engine containing all known equalities/disequalities */
  47   eq::EqualityEngine* d_equalityEngine;
  48   /** map of representatives of equality engine to used representatives in representative set */
  49   std::map< Node, Node > d_reps;
  50   /** stores set of representatives for each type */
  51   RepSet d_rep_set;
  52   /** true/false nodes */
  53   Node d_true;
  54   Node d_false;
  55   mutable std::hash_map<Node, Node, NodeHashFunction> d_modelCache;
  56   /** comment stream to include in printing */
  57   std::stringstream d_comment_str;
  58   /** get comments */
  59   void getComments(std::ostream& out) const;
  60 protected:
  61   /** reset the model */
  62   virtual void reset();
  63   /**
  64    * Get model value function.  This function is called by getValue
  65    */
  66   Node getModelValue(TNode n, bool hasBoundVars = false, bool useDontCares = false) const;
  67 public:
  68   /** is built */
  69   bool isBuilt() { return d_modelBuilt.get(); }
  70   /**
  71    * Get value function.  This should be called only after a ModelBuilder has called buildModel(...)
  72    * on this model.
  73    */
  74   Node getValue( TNode n, bool useDontCares = false ) const;
  75
  76   /** get existing domain value, with possible exclusions
  77     *   This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude
  78     */
  79   Node getDomainValue( TypeNode tn, std::vector< Node >& exclude );
  80 public:
  81   /** Adds a substitution from x to t. */
  82   void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
  83   /** add term function
  84     *   addTerm( n ) will do any model-specific processing necessary for n,
  85     *   such as constraining the interpretation of uninterpreted functions,
  86     *   and adding n to the equality engine of this model
  87     */
  88   virtual void addTerm(TNode n);
  89   /** assert equality holds in the model */
  90   void assertEquality(TNode a, TNode b, bool polarity);
  91   /** assert predicate holds in the model */
  92   void assertPredicate(TNode a, bool polarity);
  93   /** assert all equalities/predicates in equality engine hold in the model */
  94   void assertEqualityEngine(const eq::EqualityEngine* ee, std::set<Node>* termSet = NULL);
  95   /** assert representative
  96     *  This function tells the model that n should be the representative of its equivalence class.
  97     *  It should be called during model generation, before final representatives are chosen.  In the
  98     *  case of TheoryEngineModelBuilder, it should be called during Theory's collectModelInfo( ... )
  99     *  functions where fullModel = true.
 100     */
 101   void assertRepresentative(TNode n);
 102 public:
 103   /** general queries */
 104   bool hasTerm(TNode a);
 105   Node getRepresentative(TNode a);
 106   bool areEqual(TNode a, TNode b);
 107   bool areDisequal(TNode a, TNode b);
 108 public:
 109   /** return whether this node is a don't-care */
 110   bool isDontCare(Expr expr) const;
 111   /** get value function for Exprs. */
 112   Expr getValue( Expr expr ) const;
 113   /** get cardinality for sort */
 114   Cardinality getCardinality( Type t ) const;
 115 public:
 116   /** print representative debug function */
 117   void printRepresentativeDebug( const char* c, Node r );
 118   /** print representative function */
 119   void printRepresentative( std::ostream& out, Node r );
 120 public:
 121   /** whether function models are enabled */
 122   bool d_enableFuncModels;
 123   //necessary information for function models
 124   std::map< Node, std::vector< Node > > d_uf_terms;
 125   std::map< Node, Node > d_uf_models;
 126 };/* class TheoryModel */
 127
 128 /*
 129  * Class that encapsulates a map from types to sets of nodes
 130  */
 131 class TypeSet {
 132 public:
 133   typedef std::hash_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap;
 134   typedef std::hash_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap;
 135   typedef TypeSetMap::iterator iterator;
 136   typedef TypeSetMap::const_iterator const_iterator;
 137 private:
 138   TypeSetMap d_typeSet;
 139   TypeToTypeEnumMap d_teMap;
 140   TypeEnumeratorProperties * d_tep;
 141
 142   public:
 143   TypeSet() : d_tep(NULL) {}
 144   ~TypeSet() {
 145     iterator it;
 146     for (it = d_typeSet.begin(); it != d_typeSet.end(); ++it) {
 147       if ((*it).second != NULL) {
 148         delete (*it).second;
 149       }
 150     }
 151     TypeToTypeEnumMap::iterator it2;
 152     for (it2 = d_teMap.begin(); it2 != d_teMap.end(); ++it2) {
 153       if ((*it2).second != NULL) {
 154         delete (*it2).second;
 155       }
 156     }
 157   }
 158   void setTypeEnumeratorProperties( TypeEnumeratorProperties * tep ) { d_tep = tep; }
 159   void add(TypeNode t, TNode n)
 160   {
 161     iterator it = d_typeSet.find(t);
 162     std::set<Node>* s;
 163     if (it == d_typeSet.end()) {
 164       s = new std::set<Node>;
 165       d_typeSet[t] = s;
 166     }
 167     else {
 168       s = (*it).second;
 169     }
 170     s->insert(n);
 171   }
 172
 173   std::set<Node>* getSet(TypeNode t) const
 174   {
 175     const_iterator it = d_typeSet.find(t);
 176     if (it == d_typeSet.end()) {
 177       return NULL;
 178     }
 179     return (*it).second;
 180   }
 181
 182   Node nextTypeEnum(TypeNode t, bool useBaseType = false)
 183   {
 184     TypeEnumerator* te;
 185     TypeToTypeEnumMap::iterator it = d_teMap.find(t);
 186     if (it == d_teMap.end()) {
 187       te = new TypeEnumerator(t, d_tep);
 188       d_teMap[t] = te;
 189     }
 190     else {
 191       te = (*it).second;
 192     }
 193     if (te->isFinished()) {
 194       return Node();
 195     }
 196
 197     if (useBaseType) {
 198       t = t.getBaseType();
 199     }
 200     iterator itSet = d_typeSet.find(t);
 201     std::set<Node>* s;
 202     if (itSet == d_typeSet.end()) {
 203       s = new std::set<Node>;
 204       d_typeSet[t] = s;
 205     }
 206     else {
 207       s = (*itSet).second;
 208     }
 209     Node n = **te;
 210     while (s->find(n) != s->end()) {
 211       ++(*te);
 212       if (te->isFinished()) {
 213         return Node();
 214       }
 215       n = **te;
 216     }
 217     s->insert(n);
 218     ++(*te);
 219     return n;
 220   }
 221
 222   bool empty()
 223   {
 224     return d_typeSet.empty();
 225   }
 226
 227   iterator begin()
 228   {
 229     return d_typeSet.begin();
 230   }
 231
 232   iterator end()
 233   {
 234     return d_typeSet.end();
 235   }
 236
 237   static TypeNode getType(iterator it)
 238   {
 239     return (*it).first;
 240   }
 241
 242   static std::set<Node>& getSet(iterator it)
 243   {
 244     return *(*it).second;
 245   }
 246
 247 };/* class TypeSet */
 248
 249 /** TheoryEngineModelBuilder class
 250   *    This model builder will consult all theories in a theory engine for
 251   *    collectModelInfo( ... ) when building a model.
 252   */
 253 class TheoryEngineModelBuilder : public ModelBuilder
 254 {
 255 protected:
 256   /** pointer to theory engine */
 257   TheoryEngine* d_te;
 258   typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
 259   NodeMap d_normalizedCache;
 260   typedef std::hash_set<Node, NodeHashFunction> NodeSet;
 261
 262   /** process build model */
 263   virtual void preProcessBuildModel(TheoryModel* m, bool fullModel);
 264   virtual void processBuildModel(TheoryModel* m, bool fullModel);
 265   /** normalize representative */
 266   Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly);
 267   bool isAssignable(TNode n);
 268   void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache);
 269   void assignConstantRep( TheoryModel* tm, std::map<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel );
 270   /** is v an excluded codatatype value */
 271   bool isExcludedCdtValue( Node v, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc );
 272   bool isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m );
 273   /** involves usort */
 274   bool involvesUSort( TypeNode tn );
 275   bool isExcludedUSortValue( std::map< TypeNode, unsigned >& eqc_usort_count, Node v, std::map< Node, bool >& visited );
 276 public:
 277   TheoryEngineModelBuilder(TheoryEngine* te);
 278   virtual ~TheoryEngineModelBuilder(){}
 279   /** Build model function.
 280    *    Should be called only on TheoryModels m
 281    */
 282   void buildModel(Model* m, bool fullModel);
 283 };/* class TheoryEngineModelBuilder */
 284
 285 }/* CVC4::theory namespace */
 286 }/* CVC4 namespace */
 287
 288 #endif /* __CVC4__THEORY__THEORY_MODEL_H */