src/theory/ext_theory.h

   1 /*********************                                                        */
   2 /*! \file ext_theory.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Tim King, 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 Extended theory interface.
  13  **
  14  ** This implements a generic module, used by theory solvers, for performing
  15  ** "context-dependent simplification", as described in Reynolds et al
  16  ** "Designing Theory Solvers with Extensions", FroCoS 2017.
  17  **
  18  ** At a high level, this technique implements a generic inference scheme based
  19  ** on the combination of SAT-context-dependent equality reasoning and
  20  ** SAT-context-indepedent rewriting.
  21  **
  22  ** As a simple example, say
  23  ** (1) TheoryStrings tells us that the following facts hold in the SAT context:
  24  **     x = "A" ^ str.contains( str.++( x, z ), "B" ) = true.
  25  ** (2) The Rewriter tells us that:
  26  **     str.contains( str.++( "A", z ), "B" ) ----> str.contains( z, "B" ).
  27  ** From this, this class may infer that the following lemma is T-valid:
  28  **   x = "A" ^ str.contains( str.++( x, z ), "B" ) => str.contains( z, "B" )
  29  **/
  30
  31 #include "cvc4_private.h"
  32
  33 #ifndef CVC4__THEORY__EXT_THEORY_H
  34 #define CVC4__THEORY__EXT_THEORY_H
  35
  36 #include <map>
  37 #include <set>
  38
  39 #include "context/cdhashmap.h"
  40 #include "context/cdhashset.h"
  41 #include "context/context.h"
  42 #include "expr/node.h"
  43 #include "theory/theory.h"
  44
  45 namespace CVC4 {
  46 namespace theory {
  47
  48 /**
  49  * A callback class for ExtTheory below. This class is responsible for
  50  * determining how to apply context-dependent simplification.
  51  */
  52 class ExtTheoryCallback
  53 {
  54  public:
  55   virtual ~ExtTheoryCallback() {}
  56   /*
  57    * Get current substitution at an effort
  58    * @param effort The effort identifier
  59    * @param vars The variables to get a substitution for
  60    * @param subs The terms to substitute for variables, in order. This vector
  61    * should be updated to one the same size as vars.
  62    * @param exp The map containing the explanation for each variable. Together
  63    * with subs, we have that:
  64    *   ( exp[vars[i]] => vars[i] = subs[i] ) holds for all i
  65    * @return true if any (non-identity) substitution was added to subs.
  66    */
  67   virtual bool getCurrentSubstitution(int effort,
  68                                       const std::vector<Node>& vars,
  69                                       std::vector<Node>& subs,
  70                                       std::map<Node, std::vector<Node> >& exp);
  71
  72   /*
  73    * Is extended function n reduced? This returns true if n is reduced to a
  74    * form that requires no further interaction from the theory.
  75    *
  76    * @param effort The effort identifier
  77    * @param n The term to reduce
  78    * @param on The original form of n, before substitution
  79    * @param exp The explanation of on = n
  80    * @return true if n is reduced.
  81    */
  82   virtual bool isExtfReduced(int effort,
  83                              Node n,
  84                              Node on,
  85                              std::vector<Node>& exp);
  86
  87   /**
  88    * Get reduction for node n.
  89    * If return value is true, then n is reduced.
  90    * If satDep is updated to false, then n is reduced independent of the
  91    * SAT context (e.g. by a lemma that persists at this
  92    * user-context level).
  93    * If nr is non-null, then ( n = nr ) should be added as a lemma by caller,
  94    * and return value of this method should be true.
  95    */
  96   virtual bool getReduction(int effort, Node n, Node& nr, bool& satDep);
  97 };
  98
  99 /** Extended theory class
 100  *
 101  * This class is used for constructing generic extensions to theory solvers.
 102  * In particular, it provides methods for "context-dependent simplification"
 103  * and "model-based refinement". For details, see Reynolds et al "Design
 104  * Theory Solvers with Extensions", FroCoS 2017.
 105  *
 106  * It maintains:
 107  * (1) A set of "extended function" kinds (d_extf_kind),
 108  * (2) A database of active/inactive extended function terms (d_ext_func_terms)
 109  * that have been registered to the class.
 110  *
 111  * This class has methods doInferences/doReductions, which send out lemmas
 112  * based on the current set of active extended function terms. The former
 113  * is based on context-dependent simplification, where this class asks the
 114  * underlying theory for a "derivable substitution", whereby extended functions
 115  * may be reducable.
 116  */
 117 class ExtTheory
 118 {
 119   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
 120   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 121
 122  public:
 123   /** constructor
 124    *
 125    * If cacheEnabled is false, we do not cache results of getSubstitutedTerm.
 126    */
 127   ExtTheory(ExtTheoryCallback& p,
 128             context::Context* c,
 129             context::UserContext* u,
 130             OutputChannel& out,
 131             bool cacheEnabled = false);
 132   virtual ~ExtTheory() {}
 133   /** Tells this class to treat terms with Kind k as extended functions */
 134   void addFunctionKind(Kind k) { d_extf_kind[k] = true; }
 135   /** Is kind k treated as an extended function by this class? */
 136   bool hasFunctionKind(Kind k) const
 137   {
 138     return d_extf_kind.find(k) != d_extf_kind.end();
 139   }
 140   /** register term
 141    *
 142    * Registers term n with this class. Adds n to the set of extended function
 143    * terms known by this class (d_ext_func_terms) if n is an extended function,
 144    * that is, if addFunctionKind( n.getKind() ) was called.
 145    */
 146   void registerTerm(Node n);
 147   /** register all subterms of n with this class */
 148   void registerTermRec(Node n);
 149   /** set n as reduced/inactive
 150    *
 151    * If satDep = false, then n remains inactive in the duration of this
 152    * user-context level
 153    */
 154   void markReduced(Node n, bool satDep = true);
 155   /**
 156    * Mark that a and b are congruent terms. This sets b inactive, and sets a to
 157    * inactive if b was inactive.
 158    */
 159   void markCongruent(Node a, Node b);
 160   /** getSubstitutedTerms
 161    *
 162    *  input : effort, terms
 163    *  output : sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i.
 164    *
 165    * For each i, sterms[i] = term[i] * sigma for some "derivable substitution"
 166    * sigma. We obtain derivable substitutions and their explanations via calls
 167    * to the underlying theory's Theory::getCurrentSubstitution method. This
 168    * also
 169    *
 170    * If useCache is true, we cache the result in d_gst_cache. This is a context
 171    * independent cache that can be cleared using clearCache() below.
 172    */
 173   void getSubstitutedTerms(int effort,
 174                            const std::vector<Node>& terms,
 175                            std::vector<Node>& sterms,
 176                            std::vector<std::vector<Node> >& exp,
 177                            bool useCache = false);
 178   /**
 179    * Same as above, but for a single term. We return the substituted form of
 180    * term and add its explanation to exp.
 181    */
 182   Node getSubstitutedTerm(int effort,
 183                           Node term,
 184                           std::vector<Node>& exp,
 185                           bool useCache = false);
 186   /** clear the cache for getSubstitutedTerm */
 187   void clearCache();
 188   /** doInferences
 189    *
 190    * This function performs "context-dependent simplification". The method takes
 191    * as input:
 192    *  effort: an identifier used to determine which terms we reduce and the
 193    *          form of the derivable substitution we will use,
 194    *  terms: the set of terms to simplify,
 195    *  batch: if this flag is true, we send lemmas for all terms; if it is false
 196    *         we send a lemma for the first applicable term.
 197    *
 198    * Sends rewriting lemmas of the form ( exp => t = c ) where t is in terms
 199    * and c is a constant, c = rewrite( t*sigma ) where exp |= sigma. These
 200    * lemmas are determined by asking the underlying theory for a derivable
 201    * substitution (through getCurrentSubstitution with getSubstitutedTerm)
 202    * above, applying this substitution to terms in terms, rewriting
 203    * the result and checking with the theory whether the resulting term is
 204    * in reduced form (isExtfReduced).
 205    *
 206    * This method adds the extended terms that are still active to nred, and
 207    * returns true if and only if a lemma of the above form was sent.
 208    */
 209   bool doInferences(int effort,
 210                     const std::vector<Node>& terms,
 211                     std::vector<Node>& nred,
 212                     bool batch = true);
 213   /**
 214    * Calls the above function, where terms is getActive(), the set of currently
 215    * active terms.
 216    */
 217   bool doInferences(int effort, std::vector<Node>& nred, bool batch = true);
 218   /** doReductions
 219    *
 220    * This method has the same interface as doInferences. In contrast to
 221    * doInfereces, this method will send reduction lemmas of the form ( t = t' )
 222    * where t is in terms and t' is an equivalent reduced term.
 223    */
 224   bool doReductions(int effort,
 225                     const std::vector<Node>& terms,
 226                     std::vector<Node>& nred,
 227                     bool batch = true);
 228   bool doReductions(int effort, std::vector<Node>& nred, bool batch = true);
 229
 230   /** get the set of all extended function terms from d_ext_func_terms */
 231   void getTerms(std::vector<Node>& terms);
 232   /** is there at least one active extended function term? */
 233   bool hasActiveTerm() const;
 234   /** is n an active extended function term? */
 235   bool isActive(Node n) const;
 236   /** get the set of active terms from d_ext_func_terms */
 237   std::vector<Node> getActive() const;
 238   /** get the set of active terms from d_ext_func_terms of kind k */
 239   std::vector<Node> getActive(Kind k) const;
 240
 241  private:
 242   /** returns the set of variable subterms of n */
 243   static std::vector<Node> collectVars(Node n);
 244   /** is n context dependent inactive? */
 245   bool isContextIndependentInactive(Node n) const;
 246   /** do inferences internal */
 247   bool doInferencesInternal(int effort,
 248                             const std::vector<Node>& terms,
 249                             std::vector<Node>& nred,
 250                             bool batch,
 251                             bool isRed);
 252   /** send lemma on the output channel */
 253   bool sendLemma(Node lem, bool preprocess = false);
 254   /** reference to the callback */
 255   ExtTheoryCallback& d_parent;
 256   /** Reference to the output channel we are using */
 257   OutputChannel& d_out;
 258   /** the true node */
 259   Node d_true;
 260   /** extended function terms, map to whether they are active */
 261   NodeBoolMap d_ext_func_terms;
 262   /**
 263    * The set of terms from d_ext_func_terms that are SAT-context-independent
 264    * inactive. For instance, a term t is SAT-context-independent inactive if
 265    * a reduction lemma of the form t = t' was added in this user-context level.
 266    */
 267   NodeSet d_ci_inactive;
 268   /**
 269    * Watched term for checking if any non-reduced extended functions exist.
 270    * This is an arbitrary active member of d_ext_func_terms.
 271    */
 272   context::CDO<Node> d_has_extf;
 273   /** the set of kinds we are treated as extended functions */
 274   std::map<Kind, bool> d_extf_kind;
 275   /** information for each term in d_ext_func_terms */
 276   class ExtfInfo
 277   {
 278    public:
 279     /** all variables in this term */
 280     std::vector<Node> d_vars;
 281   };
 282   std::map<Node, ExtfInfo> d_extf_info;
 283
 284   // cache of all lemmas sent
 285   NodeSet d_lemmas;
 286   NodeSet d_pp_lemmas;
 287   /** whether we enable caching for getSubstitutedTerm */
 288   bool d_cacheEnabled;
 289   /** Substituted term info */
 290   class SubsTermInfo
 291   {
 292    public:
 293     /** the substituted term */
 294     Node d_sterm;
 295     /** an explanation */
 296     std::vector<Node> d_exp;
 297   };
 298   /**
 299    * This maps an (effort, term) to the information above. It is used as a
 300    * cache for getSubstitutedTerm when d_cacheEnabled is true.
 301    */
 302   std::map<int, std::map<Node, SubsTermInfo> > d_gst_cache;
 303 };
 304
 305 } /* CVC4::theory namespace */
 306 } /* CVC4 namespace */
 307
 308 #endif /* CVC4__THEORY__EXT_THEORY_H */