src/theory/sets/theory_sets_private.h

   1 /*********************                                                        */
   2 /*! \file theory_sets_private.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Kshitij Bansal, Mathias Preiner
   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 theory implementation.
  13  **
  14  ** Sets theory implementation.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H
  20 #define CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H
  21
  22 #include "context/cdhashset.h"
  23 #include "context/cdqueue.h"
  24 #include "expr/node_trie.h"
  25 #include "theory/sets/cardinality_extension.h"
  26 #include "theory/sets/inference_manager.h"
  27 #include "theory/sets/solver_state.h"
  28 #include "theory/sets/theory_sets_rels.h"
  29 #include "theory/sets/theory_sets_rewriter.h"
  30 #include "theory/theory.h"
  31 #include "theory/uf/equality_engine.h"
  32
  33 namespace CVC4 {
  34 namespace theory {
  35 namespace sets {
  36
  37 /** Internal classes, forward declared here */
  38 class TheorySets;
  39
  40 class TheorySetsPrivate {
  41   typedef context::CDHashMap< Node, bool, NodeHashFunction> NodeBoolMap;
  42   typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
  43   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
  44
  45  public:
  46   void eqNotifyNewClass(TNode t);
  47   void eqNotifyPreMerge(TNode t1, TNode t2);
  48   void eqNotifyPostMerge(TNode t1, TNode t2);
  49   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
  50   /** Assert fact holds in the current context with explanation exp.
  51    *
  52    * exp should be explainable by the equality engine of this class, and fact
  53    * should be a literal.
  54    */
  55   bool assertFact(Node fact, Node exp);
  56
  57  private:
  58   /** Are a and b trigger terms in the equality engine that may be disequal? */
  59   bool areCareDisequal(Node a, Node b);
  60   NodeIntMap d_members;
  61   std::map< Node, std::vector< Node > > d_members_data;
  62   /**
  63    * Invoke the decision procedure for this theory, which is run at
  64    * full effort. This will either send a lemma or conflict on the output
  65    * channel of this class, or otherwise the current set of constraints is
  66    * satisfiable w.r.t. the theory of sets.
  67    */
  68   void fullEffortCheck();
  69   /**
  70    * Reset the information for a full effort check.
  71    */
  72   void fullEffortReset();
  73   /**
  74    * This ensures that subtype constraints are met for all set terms. In
  75    * particular, for a set equivalence class E, let Set(T) be the most
  76    * common type among the types of terms in that class. In other words,
  77    * if E contains two terms of Set(Int) and Set(Real), then Set(Int) is the
  78    * most common type. Then, for each membership x in S where S is a set in
  79    * this equivalence class, we ensure x has type T by asserting:
  80    *   x = k
  81    * for a fresh constant k of type T. This is done only if the type of x is not
  82    * a subtype of Int (e.g. if x is of type Real). We call k the "type
  83    * constraint skolem for x of type Int".
  84    */
  85   void checkSubtypes();
  86   /**
  87    * This implements an inference schema based on the "downwards closure" of
  88    * set membership. This roughly corresponds to the rules UNION DOWN I and II,
  89    * INTER DOWN I and II from Bansal et al IJCAR 2016, as well as rules for set
  90    * difference.
  91    */
  92   void checkDownwardsClosure();
  93   /**
  94    * This implements an inference schema based on the "upwards closure" of
  95    * set membership. This roughly corresponds to the rules UNION UP, INTER
  96    * UP I and II from Bansal et al IJCAR 2016, as well as rules for set
  97    * difference.
  98    */
  99   void checkUpwardsClosure();
 100   /**
 101    * This implements a strategy for splitting for set disequalities which
 102    * roughly corresponds the SET DISEQUALITY rule from Bansal et al IJCAR 2016.
 103    */
 104   void checkDisequalities();
 105   /**
 106    * Check comprehensions. This adds reduction lemmas for all set comprehensions
 107    * in the current context.
 108    */
 109   void checkReduceComprehensions();
 110
 111   void addCarePairs(TNodeTrie* t1,
 112                     TNodeTrie* t2,
 113                     unsigned arity,
 114                     unsigned depth,
 115                     unsigned& n_pairs);
 116
 117   Node d_true;
 118   Node d_false;
 119   Node d_zero;
 120   NodeBoolMap d_deq;
 121   /**
 122    * The set of terms that we have reduced via a lemma in the current user
 123    * context.
 124    */
 125   NodeSet d_termProcessed;
 126   NodeSet d_keep;
 127
 128   //propagation
 129   class EqcInfo
 130   {
 131   public:
 132     EqcInfo( context::Context* c );
 133     ~EqcInfo(){}
 134     // singleton or emptyset equal to this eqc
 135     context::CDO< Node > d_singleton;
 136   };
 137   /** information necessary for equivalence classes */
 138   std::map< Node, EqcInfo* > d_eqc_info;
 139   /** get or make eqc info */
 140   EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false );
 141
 142   /** full check incomplete
 143    *
 144    * This flag is set to true during a full effort check if this theory
 145    * is incomplete for some reason (for instance, if we combine cardinality
 146    * with a relation or extended function kind).
 147    */
 148   bool d_full_check_incomplete;
 149   std::map< Node, TypeNode > d_most_common_type;
 150   std::map< Node, Node > d_most_common_type_term;
 151
 152  public:
 153
 154   /**
 155    * Constructs a new instance of TheorySetsPrivate w.r.t. the provided
 156    * contexts.
 157    */
 158   TheorySetsPrivate(TheorySets& external,
 159                     context::Context* c,
 160                     context::UserContext* u);
 161
 162   ~TheorySetsPrivate();
 163
 164   TheoryRewriter* getTheoryRewriter() { return &d_rewriter; }
 165
 166   void setMasterEqualityEngine(eq::EqualityEngine* eq);
 167
 168   void addSharedTerm(TNode);
 169
 170   void check(Theory::Effort);
 171
 172   bool collectModelInfo(TheoryModel* m);
 173
 174   void computeCareGraph();
 175
 176   Node explain(TNode);
 177
 178   EqualityStatus getEqualityStatus(TNode a, TNode b);
 179
 180   void preRegisterTerm(TNode node);
 181
 182   /** expandDefinition
 183    * If the sets-ext option is not set and we have an extended operator,
 184    * we throw an exception. This function is a no-op otherwise.
 185    *
 186    * TheorySets uses expandDefinition as an entry point to see if the input
 187    * contains extended operators.
 188    *
 189    * We need to be notified when a universe set occurs in our input,
 190    * before preprocessing and simplification takes place. Otherwise the models
 191    * may be inaccurate when setsExt is false, here is an example:
 192    *
 193    * x,y : (Set Int)
 194    * x = (as univset (Set Int));
 195    * 0 in y;
 196    * check-sat;
 197    *
 198    * If setsExt is enabled, the model value of (as univset (Set Int)) is always accurate.
 199    *
 200    * If setsExt is not enabled, the following can happen for the above example:
 201    * x = (as univset (Set Int)) is made into a model substitution during
 202    * simplification. This means (as univset (Set Int)) is not a term in any assertion,
 203    * and hence we do not throw an exception, nor do we infer that 0 is a member of
 204    * (as univset (Set Int)). We instead report a model where x = {}. The correct behavior
 205    * is to throw an exception that says universe set is not supported when setsExt disabled.
 206    * Hence we check for the existence of universe set before simplification here.
 207    *
 208    * Another option to fix this is to make TheoryModel::getValue more general
 209    * so that it makes theory-specific calls to evaluate interpreted symbols.
 210    */
 211   TrustNode expandDefinition(Node n);
 212
 213   void presolve();
 214
 215   void propagate(Theory::Effort);
 216
 217   /** get default output channel */
 218   OutputChannel* getOutputChannel();
 219   /** get the valuation */
 220   Valuation& getValuation();
 221
 222  private:
 223   TheorySets& d_external;
 224
 225   /** Functions to handle callbacks from equality engine */
 226   class NotifyClass : public eq::EqualityEngineNotify {
 227     TheorySetsPrivate& d_theory;
 228
 229   public:
 230     NotifyClass(TheorySetsPrivate& theory): d_theory(theory) {}
 231     bool eqNotifyTriggerEquality(TNode equality, bool value) override;
 232     bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
 233     bool eqNotifyTriggerTermEquality(TheoryId tag,
 234                                      TNode t1,
 235                                      TNode t2,
 236                                      bool value) override;
 237     void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
 238     void eqNotifyNewClass(TNode t) override;
 239     void eqNotifyPreMerge(TNode t1, TNode t2) override;
 240     void eqNotifyPostMerge(TNode t1, TNode t2) override;
 241     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;
 242   } d_notify;
 243
 244   /** Equality engine */
 245   eq::EqualityEngine d_equalityEngine;
 246
 247   /** Proagate out to output channel */
 248   bool propagate(TNode);
 249
 250   /** generate and send out conflict node */
 251   void conflict(TNode, TNode);
 252
 253   bool isCareArg( Node n, unsigned a );
 254
 255  public:
 256   /** Is formula n entailed to have polarity pol in the current context? */
 257   bool isEntailed(Node n, bool pol) { return d_state.isEntailed(n, pol); }
 258   /** Is x entailed to be a member of set s in the current context? */
 259   bool isMember(Node x, Node s);
 260
 261  private:
 262   /** get choose function
 263    *
 264    * Returns the existing uninterpreted function for the choose operator for the
 265    * given set type, or creates a new one if it does not exist.
 266    */
 267   Node getChooseFunction(const TypeNode& setType);
 268   /** The state of the sets solver at full effort */
 269   SolverState d_state;
 270   /** The inference manager of the sets solver */
 271   InferenceManager d_im;
 272   /** subtheory solver for the theory of relations */
 273   std::unique_ptr<TheorySetsRels> d_rels;
 274   /** subtheory solver for the theory of sets with cardinality */
 275   std::unique_ptr<CardinalityExtension> d_cardSolver;
 276   /** are relations enabled?
 277    *
 278    * This flag is set to true during a full effort check if any constraint
 279    * involving relational constraints is asserted to this theory.
 280    */
 281   bool d_rels_enabled;
 282   /** is cardinality enabled?
 283    *
 284    * This flag is set to true during a full effort check if any constraint
 285    * involving cardinality constraints is asserted to this theory.
 286    */
 287   bool d_card_enabled;
 288
 289   /** The theory rewriter for this theory. */
 290   TheorySetsRewriter d_rewriter;
 291
 292   /*
 293    * a map that stores the choose functions for set types
 294    */
 295   std::map<TypeNode, Node> d_chooseFunctions;
 296 };/* class TheorySetsPrivate */
 297
 298
 299 }/* CVC4::theory::sets namespace */
 300 }/* CVC4::theory namespace */
 301 }/* CVC4 namespace */
 302
 303 #endif /* CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H */