src/theory/strings/base_solver.h

   1 /*********************                                                        */
   2 /*! \file base_solver.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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(context::Context* c,
  45              context::UserContext* u,
  46              SolverState& s,
  47              InferenceManager& im);
  48   ~BaseSolver();
  49
  50   //-----------------------inference steps
  51   /** check initial
  52    *
  53    * This function initializes term indices for each strings function symbol.
  54    * One key aspect of this construction is that concat terms are indexed by
  55    * their list of non-empty components. For example, if x = "" is an equality
  56    * asserted in this SAT context, then y ++ x ++ z may be indexed by (y,z).
  57    * This method may infer various facts while building these term indices, for
  58    * instance, based on congruence. An example would be inferring:
  59    *   y ++ x ++ z = y ++ z
  60    * if both terms are registered in this SAT context.
  61    *
  62    * This function should be called as a first step of any strategy.
  63    */
  64   void checkInit();
  65   /** check constant equivalence classes
  66    *
  67    * This function infers whether CONCAT terms can be simplified to constants.
  68    * For example, if x = "a" and y = "b" are equalities in the current SAT
  69    * context, then we may infer x ++ "c" ++ y is equivalent to "acb". In this
  70    * case, we infer the fact x ++ "c" ++ y = "acb".
  71    */
  72   void checkConstantEquivalenceClasses();
  73   /** check cardinality
  74    *
  75    * This function checks whether a cardinality inference needs to be applied
  76    * to a set of equivalence classes. For details, see Step 5 of the proof
  77    * procedure from Liang et al, CAV 2014.
  78    */
  79   void checkCardinality();
  80   //-----------------------end inference steps
  81
  82   //-----------------------query functions
  83   /**
  84    * Is n congruent to another term in the current context that has not been
  85    * marked congruent? If so, we can ignore n.
  86    *
  87    * Note this and the functions in this block below are valid during a full
  88    * effort check after a call to checkInit.
  89    */
  90   bool isCongruent(Node n);
  91   /**
  92    * Get the constant that the equivalence class eqc is entailed to be equal
  93    * to, or null if none exist.
  94    */
  95   Node getConstantEqc(Node eqc);
  96   /**
  97    * Same as above, where the explanation for n = c is added to exp if c is
  98    * the (non-null) return value of this function, where n is a term in the
  99    * equivalence class of eqc.
 100    */
 101   Node explainConstantEqc(Node n, Node eqc, std::vector<Node>& exp);
 102   /**
 103    * Get the set of equivalence classes of type string.
 104    */
 105   const std::vector<Node>& getStringEqc() const;
 106   //-----------------------end query functions
 107
 108  private:
 109   /**
 110    * A term index that considers terms modulo flattening and constant merging
 111    * for concatenation terms.
 112    */
 113   class TermIndex
 114   {
 115    public:
 116     /** Add n to this trie
 117      *
 118      * A term is indexed by flattening arguments of concatenation terms,
 119      * and replacing them by (non-empty) constants when possible, for example
 120      * if n is (str.++ x y z) and x = "abc" and y = "" are asserted, then n is
 121      * indexed by ("abc", z).
 122      *
 123      * index: the child of n we are currently processing,
 124      * s : reference to solver state,
 125      * er : the representative of the empty equivalence class.
 126      *
 127      * We store the vector of terms that n was indexed by in the vector c.
 128      */
 129     Node add(TNode n,
 130              unsigned index,
 131              const SolverState& s,
 132              Node er,
 133              std::vector<Node>& c);
 134     /** Clear this trie */
 135     void clear() { d_children.clear(); }
 136     /** The data at this node of the trie */
 137     Node d_data;
 138     /** The children of this node of the trie */
 139     std::map<TNode, TermIndex> d_children;
 140   };
 141   /**
 142    * This method is called as we are traversing the term index ti, where vecc
 143    * accumulates the list of constants in the path to ti. If ti has a non-null
 144    * data n, then we have inferred that d_data is equivalent to the
 145    * constant specified by vecc.
 146    */
 147   void checkConstantEquivalenceClasses(TermIndex* ti, std::vector<Node>& vecc);
 148   /** The solver state object */
 149   SolverState& d_state;
 150   /** The (custom) output channel of the theory of strings */
 151   InferenceManager& d_im;
 152   /** Commonly used constants */
 153   Node d_emptyString;
 154   Node d_false;
 155   /**
 156    * A congruence class is a set of terms f( t1 ), ..., f( tn ) where
 157    * t1 = ... = tn. Congruence classes are important since all but
 158    * one of the above terms (the representative of the congruence class)
 159    * can be ignored by the solver.
 160    *
 161    * This set contains a set of nodes that are not representatives of their
 162    * congruence class. This set is used to skip reasoning about terms in
 163    * various inference schemas implemnted by this class.
 164    */
 165   NodeSet d_congruent;
 166   /**
 167    * The following three vectors are used for tracking constants that each
 168    * equivalence class is entailed to be equal to.
 169    * - The map d_eqcToConst maps (representatives) r of equivalence classes to
 170    * the constant that that equivalence class is entailed to be equal to,
 171    * - The term d_eqcToConstBase[r] is the term in the equivalence class r
 172    * that is entailed to be equal to the constant d_eqcToConst[r],
 173    * - The term d_eqcToConstExp[r] is the explanation of why
 174    * d_eqcToConstBase[r] is equal to d_eqcToConst[r].
 175    *
 176    * For example, consider the equivalence class { r, x++"a"++y, x++z }, and
 177    * assume x = "" and y = "bb" in the current context. We have that
 178    *   d_eqcToConst[r] = "abb",
 179    *   d_eqcToConstBase[r] = x++"a"++y
 180    *   d_eqcToConstExp[r] = ( x = "" AND y = "bb" )
 181    *
 182    * This information is computed during checkInit and is used during various
 183    * inference schemas for deriving inferences.
 184    */
 185   std::map<Node, Node> d_eqcToConst;
 186   std::map<Node, Node> d_eqcToConstBase;
 187   std::map<Node, Node> d_eqcToConstExp;
 188   /** The list of equivalence classes of type string */
 189   std::vector<Node> d_stringsEqc;
 190   /** A term index for each function kind */
 191   std::map<Kind, TermIndex> d_termIndex;
 192   /** the cardinality of the alphabet */
 193   uint32_t d_cardSize;
 194 }; /* class BaseSolver */
 195
 196 }  // namespace strings
 197 }  // namespace theory
 198 }  // namespace CVC4
 199
 200 #endif /* CVC4__THEORY__STRINGS__BASE_SOLVER_H */