1 /********************* */ 2 /*! \file ext_theory.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Andrew Reynolds, Tim King 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 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/cdhashset.h" 40 #include "context/context.h" 41 #include "expr/node.h" 42 #include "theory/theory.h" 43 44 namespace CVC4 { 45 namespace theory { 46 47 /** Extended theory class 48 * 49 * This class is used for constructing generic extensions to theory solvers. 50 * In particular, it provides methods for "context-dependent simplification" 51 * and "model-based refinement". For details, see Reynolds et al "Design 52 * Theory Solvers with Extensions", FroCoS 2017. 53 * 54 * It maintains: 55 * (1) A set of "extended function" kinds (d_extf_kind), 56 * (2) A database of active/inactive extended function terms (d_ext_func_terms) 57 * that have been registered to the class. 58 * 59 * This class has methods doInferences/doReductions, which send out lemmas 60 * based on the current set of active extended function terms. The former 61 * is based on context-dependent simplification, where this class asks the 62 * underlying theory for a "derivable substitution", whereby extended functions 63 * may be reducable. 64 */ 65 class ExtTheory 66 { 67 typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; 68 typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; 69 70 public: 71 /** constructor 72 * 73 * If cacheEnabled is false, we do not cache results of getSubstitutedTerm. 74 */ 75 ExtTheory(Theory* p, bool cacheEnabled = false); ~ExtTheory()76 virtual ~ExtTheory() {} 77 /** Tells this class to treat terms with Kind k as extended functions */ addFunctionKind(Kind k)78 void addFunctionKind(Kind k) { d_extf_kind[k] = true; } 79 /** Is kind k treated as an extended function by this class? */ hasFunctionKind(Kind k)80 bool hasFunctionKind(Kind k) const 81 { 82 return d_extf_kind.find(k) != d_extf_kind.end(); 83 } 84 /** register term 85 * 86 * Registers term n with this class. Adds n to the set of extended function 87 * terms known by this class (d_ext_func_terms) if n is an extended function, 88 * that is, if addFunctionKind( n.getKind() ) was called. 89 */ 90 void registerTerm(Node n); 91 /** register all subterms of n with this class */ 92 void registerTermRec(Node n); 93 /** set n as reduced/inactive 94 * 95 * If contextDepend = false, then n remains inactive in the duration of this 96 * user-context level 97 */ 98 void markReduced(Node n, bool contextDepend = true); 99 /** 100 * Mark that a and b are congruent terms. This sets b inactive, and sets a to 101 * inactive if b was inactive. 102 */ 103 void markCongruent(Node a, Node b); 104 /** getSubstitutedTerms 105 * 106 * input : effort, terms 107 * output : sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i. 108 * 109 * For each i, sterms[i] = term[i] * sigma for some "derivable substitution" 110 * sigma. We obtain derivable substitutions and their explanations via calls 111 * to the underlying theory's Theory::getCurrentSubstitution method. This 112 * also 113 * 114 * If useCache is true, we cache the result in d_gst_cache. This is a context 115 * independent cache that can be cleared using clearCache() below. 116 */ 117 void getSubstitutedTerms(int effort, 118 const std::vector<Node>& terms, 119 std::vector<Node>& sterms, 120 std::vector<std::vector<Node> >& exp, 121 bool useCache = false); 122 /** 123 * Same as above, but for a single term. We return the substituted form of 124 * term and add its explanation to exp. 125 */ 126 Node getSubstitutedTerm(int effort, 127 Node term, 128 std::vector<Node>& exp, 129 bool useCache = false); 130 /** clear the cache for getSubstitutedTerm */ 131 void clearCache(); 132 /** doInferences 133 * 134 * This function performs "context-dependent simplification". The method takes 135 * as input: 136 * effort: an identifier used to determine which terms we reduce and the 137 * form of the derivable substitution we will use, 138 * terms: the set of terms to simplify, 139 * batch: if this flag is true, we send lemmas for all terms; if it is false 140 * we send a lemma for the first applicable term. 141 * 142 * Sends rewriting lemmas of the form ( exp => t = c ) where t is in terms 143 * and c is a constant, c = rewrite( t*sigma ) where exp |= sigma. These 144 * lemmas are determined by asking the underlying theory for a derivable 145 * substitution (through getCurrentSubstitution with getSubstitutedTerm) 146 * above, applying this substitution to terms in terms, rewriting 147 * the result and checking with the theory whether the resulting term is 148 * in reduced form (isExtfReduced). 149 * 150 * This method adds the extended terms that are still active to nred, and 151 * returns true if and only if a lemma of the above form was sent. 152 */ 153 bool doInferences(int effort, 154 const std::vector<Node>& terms, 155 std::vector<Node>& nred, 156 bool batch = true); 157 /** 158 * Calls the above function, where terms is getActive(), the set of currently 159 * active terms. 160 */ 161 bool doInferences(int effort, std::vector<Node>& nred, bool batch = true); 162 /** doReductions 163 * 164 * This method has the same interface as doInferences. In contrast to 165 * doInfereces, this method will send reduction lemmas of the form ( t = t' ) 166 * where t is in terms and t' is an equivalent reduced term. 167 */ 168 bool doReductions(int effort, 169 const std::vector<Node>& terms, 170 std::vector<Node>& nred, 171 bool batch = true); 172 bool doReductions(int effort, std::vector<Node>& nred, bool batch = true); 173 174 /** get the set of all extended function terms from d_ext_func_terms */ 175 void getTerms(std::vector<Node>& terms); 176 /** is there at least one active extended function term? */ 177 bool hasActiveTerm() const; 178 /** is n an active extended function term? */ 179 bool isActive(Node n) const; 180 /** get the set of active terms from d_ext_func_terms */ 181 std::vector<Node> getActive() const; 182 /** get the set of active terms from d_ext_func_terms of kind k */ 183 std::vector<Node> getActive(Kind k) const; 184 185 private: 186 /** returns the set of variable subterms of n */ 187 static std::vector<Node> collectVars(Node n); 188 /** is n context dependent inactive? */ 189 bool isContextIndependentInactive(Node n) const; 190 /** do inferences internal */ 191 bool doInferencesInternal(int effort, 192 const std::vector<Node>& terms, 193 std::vector<Node>& nred, 194 bool batch, 195 bool isRed); 196 /** send lemma on the output channel of d_parent */ 197 bool sendLemma(Node lem, bool preprocess = false); 198 /** reference to the underlying theory */ 199 Theory* d_parent; 200 /** the true node */ 201 Node d_true; 202 /** extended function terms, map to whether they are active */ 203 NodeBoolMap d_ext_func_terms; 204 /** 205 * The set of terms from d_ext_func_terms that are SAT-context-independent 206 * inactive. For instance, a term t is SAT-context-independent inactive if 207 * a reduction lemma of the form t = t' was added in this user-context level. 208 */ 209 NodeSet d_ci_inactive; 210 /** 211 * Watched term for checking if any non-reduced extended functions exist. 212 * This is an arbitrary active member of d_ext_func_terms. 213 */ 214 context::CDO<Node> d_has_extf; 215 /** the set of kinds we are treated as extended functions */ 216 std::map<Kind, bool> d_extf_kind; 217 /** information for each term in d_ext_func_terms */ 218 class ExtfInfo 219 { 220 public: 221 /** all variables in this term */ 222 std::vector<Node> d_vars; 223 }; 224 std::map<Node, ExtfInfo> d_extf_info; 225 226 // cache of all lemmas sent 227 NodeSet d_lemmas; 228 NodeSet d_pp_lemmas; 229 /** whether we enable caching for getSubstitutedTerm */ 230 bool d_cacheEnabled; 231 /** Substituted term info */ 232 class SubsTermInfo 233 { 234 public: 235 /** the substituted term */ 236 Node d_sterm; 237 /** an explanation */ 238 std::vector<Node> d_exp; 239 }; 240 /** 241 * This maps an (effort, term) to the information above. It is used as a 242 * cache for getSubstitutedTerm when d_cacheEnabled is true. 243 */ 244 std::map<int, std::map<Node, SubsTermInfo> > d_gst_cache; 245 }; 246 247 } /* CVC4::theory namespace */ 248 } /* CVC4 namespace */ 249 250 #endif /* __CVC4__THEORY__EXT_THEORY_H */ 251