src/theory/strings/extf_solver.h

   1 /*********************                                                        */
   2 /*! \file extf_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 Solver for extended functions of theory of strings.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__STRINGS__EXTF_SOLVER_H
  18 #define CVC4__THEORY__STRINGS__EXTF_SOLVER_H
  19
  20 #include <map>
  21 #include <vector>
  22
  23 #include "context/cdo.h"
  24 #include "expr/node.h"
  25 #include "theory/ext_theory.h"
  26 #include "theory/strings/base_solver.h"
  27 #include "theory/strings/core_solver.h"
  28 #include "theory/strings/inference_manager.h"
  29 #include "theory/strings/sequences_stats.h"
  30 #include "theory/strings/skolem_cache.h"
  31 #include "theory/strings/solver_state.h"
  32 #include "theory/strings/strings_rewriter.h"
  33 #include "theory/strings/theory_strings_preprocess.h"
  34
  35 namespace CVC4 {
  36 namespace theory {
  37 namespace strings {
  38
  39 /**
  40  * Non-static information about an extended function t. This information is
  41  * constructed and used during the check extended function evaluation
  42  * inference schema.
  43  *
  44  * In the following, we refer to the "context-dependent simplified form"
  45  * of a term t to be the result of rewriting t * sigma, where sigma is a
  46  * derivable substitution in the current context. For example, the
  47  * context-depdendent simplified form of contains( x++y, "a" ) given
  48  * sigma = { x -> "" } is contains(y,"a").
  49  */
  50 class ExtfInfoTmp
  51 {
  52  public:
  53   ExtfInfoTmp() : d_modelActive(true) {}
  54   /**
  55    * If s is in d_ctn[true] (resp. d_ctn[false]), then contains( t, s )
  56    * (resp. ~contains( t, s )) holds in the current context. The vector
  57    * d_ctnFrom is the explanation for why this holds. For example,
  58    * if d_ctn[false][i] is "A", then d_ctnFrom[false][i] might be
  59    * t = x ++ y AND x = "" AND y = "B".
  60    */
  61   std::map<bool, std::vector<Node> > d_ctn;
  62   std::map<bool, std::vector<Node> > d_ctnFrom;
  63   /**
  64    * The constant that t is entailed to be equal to, or null if none exist.
  65    */
  66   Node d_const;
  67   /**
  68    * The explanation for why t is equal to its context-dependent simplified
  69    * form.
  70    */
  71   std::vector<Node> d_exp;
  72   /** This flag is false if t is reduced in the model. */
  73   bool d_modelActive;
  74 };
  75
  76 /**
  77  * Extended function solver for the theory of strings. This manages extended
  78  * functions for the theory of strings using a combination of context-dependent
  79  * simplification (Reynolds et al CAV 2017) and lazy reductions.
  80  */
  81 class ExtfSolver
  82 {
  83   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
  84
  85  public:
  86   ExtfSolver(context::Context* c,
  87              context::UserContext* u,
  88              SolverState& s,
  89              InferenceManager& im,
  90              TermRegistry& tr,
  91              StringsRewriter& rewriter,
  92              BaseSolver& bs,
  93              CoreSolver& cs,
  94              ExtTheory& et,
  95              SequencesStatistics& statistics);
  96   ~ExtfSolver();
  97
  98   /**
  99    * Called when a shared term is added to theory of strings, this registers
 100    * n with the extended theory utility for context-depdendent simplification.
 101    */
 102   void addSharedTerm(TNode n);
 103   /** check extended functions evaluation
 104    *
 105    * This applies "context-dependent simplification" for all active extended
 106    * function terms in this SAT context. This infers facts of the form:
 107    *   x = c => f( t1 ... tn ) = c'
 108    * where the rewritten form of f( t1...tn ) { x |-> c } is c', and x = c
 109    * is a (tuple of) equalities that are asserted in this SAT context, and
 110    * f( t1 ... tn ) is a term from this SAT context.
 111    *
 112    * For more details, this is steps 4 when effort=0 and step 6 when
 113    * effort=1 from Strategy 1 in Reynolds et al, "Scaling up DPLL(T) String
 114    * Solvers using Context-Dependent Simplification", CAV 2017. When called with
 115    * effort=3, we apply context-dependent simplification based on model values.
 116    */
 117   void checkExtfEval(int effort);
 118   /** check extended function reductions
 119    *
 120    * This adds "reduction" lemmas for each active extended function in this SAT
 121    * context. These are generally lemmas of the form:
 122    *   F[t1...tn,k] ^ f( t1 ... tn ) = k
 123    * where f( t1 ... tn ) is an active extended function, k is a fresh constant
 124    * and F is a formula that constrains k based on the definition of f.
 125    *
 126    * For more details, this is step 7 from Strategy 1 in Reynolds et al,
 127    * CAV 2017. We stratify this in practice, where calling this with effort=1
 128    * reduces some of the "easier" extended functions, and effort=2 reduces
 129    * the rest.
 130    */
 131   void checkExtfReductions(int effort);
 132   /** get preprocess module */
 133   StringsPreprocess* getPreprocess() { return &d_preproc; }
 134
 135   /**
 136    * Get the current substitution for term n.
 137    *
 138    * This method returns a term that n is currently equal to in the current
 139    * context. It updates exp to contain an explanation of why it is currently
 140    * equal to that term.
 141    *
 142    * The argument effort determines what kind of term to return, either
 143    * a constant in the equivalence class of n (effort=0), the normal form of
 144    * n (effort=1,2) or the model value of n (effort>=3). The latter is only
 145    * valid at LAST_CALL effort. If a term of the above form cannot be returned,
 146    * then n itself is returned.
 147    */
 148   Node getCurrentSubstitutionFor(int effort, Node n, std::vector<Node>& exp);
 149   /** get mapping from extended functions to their information
 150    *
 151    * This information is valid during a full effort check after a call to
 152    * checkExtfEval.
 153    */
 154   const std::map<Node, ExtfInfoTmp>& getInfo() const;
 155   //---------------------------------- information about ExtTheory
 156   /** Are there any active extended functions? */
 157   bool hasExtendedFunctions() const;
 158   /**
 159    * Get the function applications of kind k that are active in the current
 160    * context (see ExtTheory::getActive).
 161    */
 162   std::vector<Node> getActive(Kind k) const;
 163   //---------------------------------- end information about ExtTheory
 164  private:
 165   /** do reduction
 166    *
 167    * This is called when an extended function application n is not able to be
 168    * simplified by context-depdendent simplification, and we are resorting to
 169    * expanding n to its full semantics via a reduction. This method returns
 170    * true if it successfully reduced n by some reduction. If so, it either
 171    * caches that the reduction lemma was sent, or marks n as reduced in this
 172    * SAT-context. The argument effort has the same meaning as in
 173    * checkExtfReductions.
 174    */
 175   bool doReduction(int effort, Node n);
 176   /** check extended function inferences
 177    *
 178    * This function makes additional inferences for n that do not contribute
 179    * to its reduction, but may help show a refutation.
 180    *
 181    * This function is called when the context-depdendent simplified form of
 182    * n is nr. The argument "in" is the information object for n. The argument
 183    * "effort" has the same meaning as the effort argument of checkExtfEval.
 184    */
 185   void checkExtfInference(Node n, Node nr, ExtfInfoTmp& in, int effort);
 186   /** The solver state object */
 187   SolverState& d_state;
 188   /** The (custom) output channel of the theory of strings */
 189   InferenceManager& d_im;
 190   /** Reference to the term registry of theory of strings */
 191   TermRegistry& d_termReg;
 192   /** The theory rewriter for this theory. */
 193   StringsRewriter& d_rewriter;
 194   /** reference to the base solver, used for certain queries */
 195   BaseSolver& d_bsolver;
 196   /** reference to the core solver, used for certain queries */
 197   CoreSolver& d_csolver;
 198   /** the extended theory object for the theory of strings */
 199   ExtTheory& d_extt;
 200   /** Reference to the statistics for the theory of strings/sequences. */
 201   SequencesStatistics& d_statistics;
 202   /** preprocessing utility, for performing strings reductions */
 203   StringsPreprocess d_preproc;
 204   /** Common constants */
 205   Node d_true;
 206   Node d_false;
 207   /** Empty vector */
 208   std::vector<Node> d_emptyVec;
 209   /** map extended functions to the above information */
 210   std::map<Node, ExtfInfoTmp> d_extfInfoTmp;
 211   /** any non-reduced extended functions exist? */
 212   context::CDO<bool> d_hasExtf;
 213   /** extended functions inferences cache */
 214   NodeSet d_extfInferCache;
 215   /** The set of extended functions we have sent reduction lemmas for */
 216   NodeSet d_reduced;
 217 };
 218
 219 }  // namespace strings
 220 }  // namespace theory
 221 }  // namespace CVC4
 222
 223 #endif /* CVC4__THEORY__STRINGS__EXTF_SOLVER_H */