src/theory/strings/base_solver.h

   1 /*********************                                                        */
   2 /*! \file base_solver.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Andres Noetzli
   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 Base solver for term indexing and constant inference for the
  13  ** theory of strings.
  14  **/
  15
  16 #include "cvc4_private.h"
  17
  18 #ifndef CVC4__THEORY__STRINGS__BASE_SOLVER_H
  19 #define CVC4__THEORY__STRINGS__BASE_SOLVER_H
  20
  21 #include "context/cdhashset.h"
  22 #include "context/cdlist.h"
  23 #include "theory/strings/infer_info.h"
  24 #include "theory/strings/inference_manager.h"
  25 #include "theory/strings/normal_form.h"
  26 #include "theory/strings/skolem_cache.h"
  27 #include "theory/strings/solver_state.h"
  28
  29 namespace CVC4 {
  30 namespace theory {
  31 namespace strings {
  32
  33 /** The base solver for the theory of strings
  34  *
  35  * This implements techniques for inferring when terms are congruent in the
  36  * current context, and techniques for inferring when equivalence classes
  37  * are equivalent to constants.
  38  */
  39 class BaseSolver
  40 {
  41   using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
  42
  43  public:
  44   BaseSolver(SolverState& s, InferenceManager& im);
  45   ~BaseSolver();
  46
  47   //-----------------------inference steps
  48   /** check initial
  49    *
  50    * This function initializes term indices for each strings function symbol.
  51    * One key aspect of this construction is that concat terms are indexed by
  52    * their list of non-empty components. For example, if x = "" is an equality
  53    * asserted in this SAT context, then y ++ x ++ z may be indexed by (y,z).
  54    * This method may infer various facts while building these term indices, for
  55    * instance, based on congruence. An example would be inferring:
  56    *   y ++ x ++ z = y ++ z
  57    * if both terms are registered in this SAT context.
  58    *
  59    * This function should be called as a first step of any strategy.
  60    */
  61   void checkInit();
  62   /** check constant equivalence classes
  63    *
  64    * This function infers whether CONCAT terms can be simplified to constants.
  65    * For example, if x = "a" and y = "b" are equalities in the current SAT
  66    * context, then we may infer x ++ "c" ++ y is equivalent to "acb". In this
  67    * case, we infer the fact x ++ "c" ++ y = "acb".
  68    */
  69   void checkConstantEquivalenceClasses();
  70   /** check cardinality
  71    *
  72    * This function checks whether a cardinality inference needs to be applied
  73    * to a set of equivalence classes. For details, see Step 5 of the proof
  74    * procedure from Liang et al, CAV 2014.
  75    */
  76   void checkCardinality();
  77   //-----------------------end inference steps
  78
  79   //-----------------------query functions
  80   /**
  81    * Is n congruent to another term in the current context that has not been
  82    * marked congruent? If so, we can ignore n.
  83    *
  84    * Note this and the functions in this block below are valid during a full
  85    * effort check after a call to checkInit.
  86    */
  87   bool isCongruent(Node n);
  88   /**
  89    * Get the constant that the equivalence class eqc is entailed to be equal
  90    * to, or null if none exist.
  91    */
  92   Node getConstantEqc(Node eqc);
  93   /**
  94    * Same as above, where the explanation for n = c is added to exp if c is
  95    * the (non-null) return value of this function, where n is a term in the
  96    * equivalence class of eqc.
  97    */
  98   Node explainConstantEqc(Node n, Node eqc, std::vector<Node>& exp);
  99   /**
 100    * Same as above, for "best content" terms.
 101    */
 102   Node explainBestContentEqc(Node n, Node eqc, std::vector<Node>& exp);
 103   /**
 104    * Get the set of equivalence classes of type string.
 105    */
 106   const std::vector<Node>& getStringEqc() const;
 107   //-----------------------end query functions
 108
 109  private:
 110   /**
 111    * The information that we associated with each equivalence class.
 112    *
 113    * Example 1. Consider the equivalence class { r, x++"a"++y, x++z }, and
 114    * assume x = "" and y = "bb" in the current context. We have that
 115    *   d_bestContent = "abb",
 116    *   d_base = x++"a"++y
 117    *   d_exp = ( x = "" AND y = "bb" )
 118    *
 119    * Example 2. Consider the equivalence class { r, x++"a"++w++y, x++z }, and
 120    * assume x = "" and y = "bb" in the current context. We have that
 121    *   d_bestContent = "a" ++ w ++ "bb",
 122    *   d_bestScore = 3
 123    *   d_base = x++"a"++w++y
 124    *   d_exp = ( x = "" AND y = "bb" )
 125    *
 126    * This information is computed during checkInit and is used during various
 127    * inference schemas for deriving inferences.
 128    */
 129   struct BaseEqcInfo
 130   {
 131     /**
 132      * Either a constant or a concatentation of constants and variables that
 133      * this equivalence class is entailed to be equal to. If it is a
 134      * concatenation, this is the concatenation that is currently known to have
 135      * the highest score (see `d_bestScore`).
 136      */
 137     Node d_bestContent;
 138     /**
 139      * The sum of the number of characters in the string literals of
 140      * `d_bestContent`.
 141      */
 142     size_t d_bestScore;
 143     /**
 144      * The term in the equivalence class that is entailed to be equal to
 145      * `d_bestContent`.
 146      */
 147     Node d_base;
 148     /** This term explains why `d_bestContent` is equal to `d_base`. */
 149     Node d_exp;
 150   };
 151
 152   /**
 153    * A term index that considers terms modulo flattening and constant merging
 154    * for concatenation terms.
 155    */
 156   class TermIndex
 157   {
 158    public:
 159     /** Add n to this trie
 160      *
 161      * A term is indexed by flattening arguments of concatenation terms,
 162      * and replacing them by (non-empty) constants when possible, for example
 163      * if n is (str.++ x y z) and x = "abc" and y = "" are asserted, then n is
 164      * indexed by ("abc", z).
 165      *
 166      * index: the child of n we are currently processing,
 167      * s : reference to solver state,
 168      * er : the representative of the empty equivalence class.
 169      *
 170      * We store the vector of terms that n was indexed by in the vector c.
 171      */
 172     Node add(TNode n,
 173              unsigned index,
 174              const SolverState& s,
 175              Node er,
 176              std::vector<Node>& c);
 177     /** Clear this trie */
 178     void clear() { d_children.clear(); }
 179     /** The data at this node of the trie */
 180     Node d_data;
 181     /** The children of this node of the trie */
 182     std::map<TNode, TermIndex> d_children;
 183   };
 184   /**
 185    * This method is called as we are traversing the term index ti, where vecc
 186    * accumulates the list of constants in the path to ti. If ti has a non-null
 187    * data n, then we have inferred that d_data is equivalent to the
 188    * constant specified by vecc.
 189    *
 190    * @param ti The term index for string concatenations
 191    * @param vecc The list of constants in the path to ti
 192    * @param ensureConst If true, require that each element in the path is
 193    *                    constant
 194    * @param isConst If true, the path so far only includes constants
 195    */
 196   void checkConstantEquivalenceClasses(TermIndex* ti,
 197                                        std::vector<Node>& vecc,
 198                                        bool ensureConst = true,
 199                                        bool isConst = true);
 200   /**
 201    * Check cardinality for type tn. This adds a lemma corresponding to
 202    * cardinality for terms of type tn, if applicable.
 203    *
 204    * @param tn The string-like type of terms we are considering,
 205    * @param cols The list of collections of equivalence classes. This is a
 206    * partition of all string equivalence classes, grouped by those with equal
 207    * lengths.
 208    * @param lts The length of each of the collections in cols.
 209    */
 210   void checkCardinalityType(TypeNode tn,
 211                             std::vector<std::vector<Node> >& cols,
 212                             std::vector<Node>& lts);
 213   /** The solver state object */
 214   SolverState& d_state;
 215   /** The (custom) output channel of the theory of strings */
 216   InferenceManager& d_im;
 217   /** Commonly used constants */
 218   Node d_emptyString;
 219   Node d_false;
 220   /**
 221    * A congruence class is a set of terms f( t1 ), ..., f( tn ) where
 222    * t1 = ... = tn. Congruence classes are important since all but
 223    * one of the above terms (the representative of the congruence class)
 224    * can be ignored by the solver.
 225    *
 226    * This set contains a set of nodes that are not representatives of their
 227    * congruence class. This set is used to skip reasoning about terms in
 228    * various inference schemas implemented by this class.
 229    */
 230   NodeSet d_congruent;
 231   /**
 232    * Maps equivalence classes to their info, see description of `BaseEqcInfo`
 233    * for more information.
 234    */
 235   std::map<Node, BaseEqcInfo> d_eqcInfo;
 236   /** The list of equivalence classes of type string */
 237   std::vector<Node> d_stringsEqc;
 238   /** A term index for each type, function kind pair */
 239   std::map<TypeNode, std::map<Kind, TermIndex> > d_termIndex;
 240   /** the cardinality of the alphabet */
 241   uint32_t d_cardSize;
 242 }; /* class BaseSolver */
 243
 244 }  // namespace strings
 245 }  // namespace theory
 246 }  // namespace CVC4
 247
 248 #endif /* CVC4__THEORY__STRINGS__BASE_SOLVER_H */