src/theory/sets/solver_state.h

   1 /*********************                                                        */
   2 /*! \file solver_state.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Mudathir Mohamed
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 Sets state object
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__SETS__THEORY_SOLVER_STATE_H
  18 #define CVC4__THEORY__SETS__THEORY_SOLVER_STATE_H
  19
  20 #include <map>
  21 #include <vector>
  22
  23 #include "context/cdhashset.h"
  24 #include "theory/sets/skolem_cache.h"
  25 #include "theory/uf/equality_engine.h"
  26
  27 namespace CVC4 {
  28 namespace theory {
  29 namespace sets {
  30
  31 class TheorySetsPrivate;
  32
  33 /** Sets state
  34  *
  35  * The purpose of this class is to:
  36  * (1) Maintain information concerning the current set of assertions during a
  37  * full effort check,
  38  * (2) Maintain a database of commonly used terms.
  39  *
  40  * During a full effort check, the solver for theory of sets should call:
  41  *   reset; ( registerEqc | registerTerm )*
  42  * to initialize the information in this class regarding full effort checks.
  43  * Other query calls are then valid for the remainder of the full effort check.
  44  */
  45 class SolverState
  46 {
  47   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
  48
  49  public:
  50   SolverState(TheorySetsPrivate& p,
  51               context::Context* c,
  52               context::UserContext* u);
  53   /**
  54    * Finish initialize, there ee is a pointer to the official equality engine
  55    * of theory of strings.
  56    */
  57   void finishInit(eq::EqualityEngine* ee);
  58   //-------------------------------- initialize per check
  59   /** reset, clears the data structures maintained by this class. */
  60   void reset();
  61   /** register equivalence class whose type is tn */
  62   void registerEqc(TypeNode tn, Node r);
  63   /** register term n of type tnn in the equivalence class of r */
  64   void registerTerm(Node r, TypeNode tnn, Node n);
  65   //-------------------------------- end initialize per check
  66   /** Are we currently in conflict? */
  67   bool isInConflict() const { return d_conflict; }
  68   /**
  69    * Indicate that we are in conflict, without a conflict clause. This is
  70    * called, for instance, when we have propagated a conflicting literal.
  71    */
  72   void setConflict();
  73   /** Set conf is a conflict node to be sent on the output channel.  */
  74   void setConflict(Node conf);
  75   /**
  76    * Get the representative of a in the equality engine of this class, or a
  77    * itself if it is not registered as a term.
  78    */
  79   Node getRepresentative(Node a) const;
  80   /** Is a registered as a term in the equality engine of this class? */
  81   bool hasTerm(Node a) const;
  82   /** Is a=b according to equality reasoning in the current context? */
  83   bool areEqual(Node a, Node b) const;
  84   /** Is a!=b according to equality reasoning in the current context? */
  85   bool areDisequal(Node a, Node b) const;
  86   /** get equality engine */
  87   eq::EqualityEngine* getEqualityEngine() const;
  88   /** add equality to explanation
  89    *
  90    * This adds a = b to exp if a and b are syntactically disequal. The equality
  91    * a = b should hold in the current context.
  92    */
  93   void addEqualityToExp(Node a, Node b, std::vector<Node>& exp) const;
  94   /** Is formula n entailed to have polarity pol in the current context? */
  95   bool isEntailed(Node n, bool pol) const;
  96   /**
  97    * Is the disequality between sets s and t entailed in the current context?
  98    */
  99   bool isSetDisequalityEntailed(Node s, Node t) const;
 100   /**
 101    * Get the equivalence class of the empty set of type tn, or null if it does
 102    * not exist as a term in the current context.
 103    */
 104   Node getEmptySetEqClass(TypeNode tn) const;
 105   /**
 106    * Get the equivalence class of the universe set of type tn, or null if it
 107    * does not exist as a term in the current context.
 108    */
 109   Node getUnivSetEqClass(TypeNode tn) const;
 110   /**
 111    * Get the singleton set in the equivalence class of representative r if it
 112    * exists, or null if none exists.
 113    */
 114   Node getSingletonEqClass(Node r) const;
 115   /** get binary operator term (modulo equality)
 116    *
 117    * This method returns a non-null node n if and only if a term n that is
 118    * congruent to <k>(r1,r2) exists in the current context.
 119    */
 120   Node getBinaryOpTerm(Kind k, Node r1, Node r2) const;
 121   /**
 122    * Returns a term that is congruent to n in the current context.
 123    *
 124    * To ensure that inferences and processing is not redundant,
 125    * this class computes congruence over all terms that exist in the current
 126    * context. If a set of terms f( t1 ), ... f( tn ) are pairwise congruent
 127    * (call this a "congruence class"), it selects one of these terms as a
 128    * representative. All other terms return the representative term from
 129    * its congruence class.
 130    */
 131   Node getCongruent(Node n) const;
 132   /**
 133    * This method returns true if n is not the representative of its congruence
 134    * class.
 135    */
 136   bool isCongruent(Node n) const;
 137
 138   /** Get the list of all equivalence classes of set terms */
 139   const std::vector<Node>& getSetsEqClasses() const { return d_set_eqc; }
 140   /** Get the list of all equivalence classes of set terms that have element
 141    * type t */
 142   const std::vector<Node> getSetsEqClasses(const TypeNode& t) const;
 143
 144   /**
 145    * Get the list of non-variable sets that exists in the equivalence class
 146    * whose representative is r.
 147    */
 148   const std::vector<Node>& getNonVariableSets(Node r) const;
 149   /**
 150    * Get a variable set in the equivalence class with representative r, or null
 151    * if none exist.
 152    */
 153   Node getVariableSet(Node r) const;
 154   /** Get comprehension sets in equivalence class with representative r */
 155   const std::vector<Node>& getComprehensionSets(Node r) const;
 156   /** Get (positive) members of the set equivalence class r
 157    *
 158    * The members are return as a map, which maps members to their explanation.
 159    * For example, if x = y, (member 5 y), (member 6 x), then getMembers(x)
 160    * returns the map [ 5 -> (member 5 y), 6 -> (member 6 x)].
 161    */
 162   const std::map<Node, Node>& getMembers(Node r) const;
 163   /** Get negative members of the set equivalence class r, similar to above */
 164   const std::map<Node, Node>& getNegativeMembers(Node r) const;
 165   /** Is the (positive) members list of set equivalence class r non-empty? */
 166   bool hasMembers(Node r) const;
 167   /** Get binary operator index
 168    *
 169    * This returns a mapping from binary operator kinds (INTERSECT, SETMINUS,
 170    * UNION) to index of terms of that kind. Each kind k maps to a map whose
 171    * entries are of the form [r1 -> r2 -> t], where t is a term in the current
 172    * context, and t is of the form <k>(t1,t2) where t1=r1 and t2=r2 hold in the
 173    * current context. The term t is the representative of its congruence class.
 174    */
 175   const std::map<Kind, std::map<Node, std::map<Node, Node> > >&
 176   getBinaryOpIndex() const;
 177   /** get operator list
 178    *
 179    * This returns a mapping from set kinds to a list of terms of that kind
 180    * that exist in the current context. Each of the terms in the range of this
 181    * map is a representative of its congruence class.
 182    */
 183   const std::map<Kind, std::vector<Node> >& getOperatorList() const;
 184   /** Get the list of all comprehension sets in the current context */
 185   const std::vector<Node>& getComprehensionSets() const;
 186
 187   // --------------------------------------- commonly used terms
 188   /** Get type constraint skolem
 189    *
 190    * The sets theory solver outputs equality lemmas of the form:
 191    *   n = d_tc_skolem[n][tn]
 192    * where the type of d_tc_skolem[n][tn] is tn, and the type
 193    * of n is not a subtype of tn. This is required to handle benchmarks like
 194    *   test/regress/regress0/sets/sets-of-sets-subtypes.smt2
 195    * where for s : (Set Int) and t : (Set Real), we have that
 196    *   ( s = t ^ y in t ) implies ( exists k : Int. y = k )
 197    * The type constraint Skolem for (y, Int) is the skolemization of k above.
 198    */
 199   Node getTypeConstraintSkolem(Node n, TypeNode tn);
 200   /** get the proxy variable for set n
 201    *
 202    * Proxy variables are used to communicate information that otherwise would
 203    * not be possible due to rewriting. For example, the literal
 204    *   card( singleton( 0 ) ) = 1
 205    * is rewritten to true. Instead, to communicate this fact (e.g. to other
 206    * theories), we require introducing a proxy variable x for singleton( 0 ).
 207    * Then:
 208    *   card( x ) = 1 ^ x = singleton( 0 )
 209    * communicates the equivalent of the above literal.
 210    */
 211   Node getProxy(Node n);
 212   /** Get the empty set of type tn */
 213   Node getEmptySet(TypeNode tn);
 214   /** Get the universe set of type tn if it exists or create a new one */
 215   Node getUnivSet(TypeNode tn);
 216   /**
 217    * Get the skolem cache of this theory, which manages a database of introduced
 218    * skolem variables used for various inferences.
 219    */
 220   SkolemCache& getSkolemCache() { return d_skCache; }
 221   // --------------------------------------- end commonly used terms
 222   /** debug print set */
 223   void debugPrintSet(Node s, const char* c) const;
 224
 225  private:
 226   /** constants */
 227   Node d_true;
 228   Node d_false;
 229   /** the empty vector and map */
 230   std::vector<Node> d_emptyVec;
 231   std::map<Node, Node> d_emptyMap;
 232   /** Whether or not we are in conflict. This flag is SAT context dependent. */
 233   context::CDO<bool> d_conflict;
 234   /** Reference to the parent theory of sets */
 235   TheorySetsPrivate& d_parent;
 236   /** Pointer to the official equality engine of theory of sets */
 237   eq::EqualityEngine* d_ee;
 238   /** The list of all equivalence classes of type set in the current context */
 239   std::vector<Node> d_set_eqc;
 240   /** Maps types to the equivalence class containing empty set of that type */
 241   std::map<TypeNode, Node> d_eqc_emptyset;
 242   /** Maps types to the equivalence class containing univ set of that type */
 243   std::map<TypeNode, Node> d_eqc_univset;
 244   /** Maps equivalence classes to a singleton set that exists in it. */
 245   std::map<Node, Node> d_eqc_singleton;
 246   /** Map from terms to the representative of their congruence class */
 247   std::map<Node, Node> d_congruent;
 248   /** Map from equivalence classes to the list of non-variable sets in it */
 249   std::map<Node, std::vector<Node> > d_nvar_sets;
 250   /** Map from equivalence classes to the list of comprehension sets in it */
 251   std::map<Node, std::vector<Node> > d_compSets;
 252   /** Map from equivalence classes to a variable sets in it */
 253   std::map<Node, Node> d_var_set;
 254   /** polarity memberships
 255    *
 256    * d_pol_mems[0] maps equivalence class to their positive membership list
 257    * with explanations (see getMembers), d_pol_mems[1] maps equivalence classes
 258    * to their negative memberships.
 259    */
 260   std::map<Node, std::map<Node, Node> > d_pol_mems[2];
 261   // --------------------------------------- commonly used terms
 262   /** Map from set terms to their proxy variables */
 263   NodeMap d_proxy;
 264   /** Backwards map of above */
 265   NodeMap d_proxy_to_term;
 266   /** Cache of type constraint skolems (see getTypeConstraintSkolem) */
 267   std::map<Node, std::map<TypeNode, Node> > d_tc_skolem;
 268   /** Map from types to empty set of that type */
 269   std::map<TypeNode, Node> d_emptyset;
 270   /** Map from types to universe set of that type */
 271   std::map<TypeNode, Node> d_univset;
 272   // --------------------------------------- end commonly used terms
 273   // -------------------------------- term indices
 274   /** Term index for MEMBER
 275    *
 276    * A term index maps equivalence class representatives to the representative
 277    * of their congruence class.
 278    *
 279    * For example, the term index for member may contain an entry
 280    * [ r1 -> r2 -> (member t1 t2) ] where r1 and r2 are representatives of their
 281    * equivalence classes, (member t1 t2) is the representative of its congruence
 282    * class, and r1=t1 and r2=t2 hold in the current context.
 283    */
 284   std::map<Node, std::map<Node, Node> > d_members_index;
 285   /** Term index for SINGLETON */
 286   std::map<Node, Node> d_singleton_index;
 287   /** Indices for the binary kinds INTERSECT, SETMINUS and UNION. */
 288   std::map<Kind, std::map<Node, std::map<Node, Node> > > d_bop_index;
 289   /** A list of comprehension sets */
 290   std::vector<Node> d_allCompSets;
 291   // -------------------------------- end term indices
 292   std::map<Kind, std::vector<Node> > d_op_list;
 293   /** the skolem cache */
 294   SkolemCache d_skCache;
 295   /** is set disequality entailed internal
 296    *
 297    * This returns true if disequality between sets a and b is entailed in the
 298    * current context. We use an incomplete test based on equality and membership
 299    * information.
 300    *
 301    * re is the representative of the equivalence class of the empty set
 302    * whose type is the same as a and b.
 303    */
 304   bool isSetDisequalityEntailedInternal(Node a, Node b, Node re) const;
 305   /**
 306    * Get members internal, returns the positive members if i=0, or negative
 307    * members if i=1.
 308    */
 309   const std::map<Node, Node>& getMembersInternal(Node r, unsigned i) const;
 310 }; /* class TheorySetsPrivate */
 311
 312 }  // namespace sets
 313 }  // namespace theory
 314 }  // namespace CVC4
 315
 316 #endif /* CVC4__THEORY__SETS__THEORY_SOLVER_STATE_H */