1 /********************* */ 2 /*! \file term_util.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Andrew Reynolds, Morgan Deters, Mathias Preiner 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 term utilities class 13 **/ 14 15 #include "cvc4_private.h" 16 17 #ifndef __CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H 18 #define __CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H 19 20 #include <map> 21 #include <unordered_set> 22 23 #include "expr/attribute.h" 24 #include "theory/quantifiers/quant_util.h" 25 #include "theory/type_enumerator.h" 26 27 namespace CVC4 { 28 namespace theory { 29 30 // attribute for "contains instantiation constants from" 31 struct InstConstantAttributeId {}; 32 typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute; 33 34 struct BoundVarAttributeId {}; 35 typedef expr::Attribute<BoundVarAttributeId, Node> BoundVarAttribute; 36 37 struct InstVarNumAttributeId {}; 38 typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute; 39 40 struct TermDepthAttributeId {}; 41 typedef expr::Attribute<TermDepthAttributeId, uint64_t> TermDepthAttribute; 42 43 struct ContainsUConstAttributeId {}; 44 typedef expr::Attribute<ContainsUConstAttributeId, uint64_t> ContainsUConstAttribute; 45 46 //for bounded integers 47 struct BoundIntLitAttributeId {}; 48 typedef expr::Attribute<BoundIntLitAttributeId, uint64_t> BoundIntLitAttribute; 49 50 //for quantifier instantiation level 51 struct QuantInstLevelAttributeId {}; 52 typedef expr::Attribute<QuantInstLevelAttributeId, uint64_t> QuantInstLevelAttribute; 53 54 //rewrite-rule priority 55 struct RrPriorityAttributeId {}; 56 typedef expr::Attribute<RrPriorityAttributeId, uint64_t> RrPriorityAttribute; 57 58 /** Attribute true for quantifiers that do not need to be partially instantiated */ 59 struct LtePartialInstAttributeId {}; 60 typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribute; 61 62 // attribute for associating a synthesis function with a first order variable 63 struct SygusSynthGrammarAttributeId {}; 64 typedef expr::Attribute<SygusSynthGrammarAttributeId, Node> 65 SygusSynthGrammarAttribute; 66 67 // attribute for associating a variable list with a synth fun 68 struct SygusSynthFunVarListAttributeId {}; 69 typedef expr::Attribute<SygusSynthFunVarListAttributeId, Node> SygusSynthFunVarListAttribute; 70 71 //attribute for fun-def abstraction type 72 struct AbsTypeFunDefAttributeId {}; 73 typedef expr::Attribute<AbsTypeFunDefAttributeId, bool> AbsTypeFunDefAttribute; 74 75 /** Attribute for id number */ 76 struct QuantIdNumAttributeId {}; 77 typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute; 78 79 /** Attribute to mark Skolems as virtual terms */ 80 struct VirtualTermSkolemAttributeId {}; 81 typedef expr::Attribute< VirtualTermSkolemAttributeId, bool > VirtualTermSkolemAttribute; 82 83 class QuantifiersEngine; 84 85 namespace inst{ 86 class Trigger; 87 class HigherOrderTrigger; 88 } 89 90 namespace quantifiers { 91 92 class TermDatabase; 93 class Instantiate; 94 95 // TODO : #1216 split this class, most of the functions in this class should be dispersed to where they are used. 96 class TermUtil : public QuantifiersUtil 97 { 98 // TODO : remove these 99 friend class ::CVC4::theory::QuantifiersEngine; 100 friend class Instantiate; 101 102 private: 103 /** reference to the quantifiers engine */ 104 QuantifiersEngine* d_quantEngine; 105 public: 106 TermUtil(QuantifiersEngine * qe); 107 ~TermUtil(); 108 /** boolean terms */ 109 Node d_true; 110 Node d_false; 111 /** constants */ 112 Node d_zero; 113 Node d_one; 114 115 /** reset */ reset(Theory::Effort e)116 bool reset(Theory::Effort e) override { return true; } 117 /** register quantifier */ 118 void registerQuantifier(Node q) override; 119 /** identify */ identify()120 std::string identify() const override { return "TermUtil"; } 121 // for inst constant 122 private: 123 /** map from universal quantifiers to the list of variables */ 124 std::map< Node, std::vector< Node > > d_vars; 125 std::map< Node, std::map< Node, unsigned > > d_var_num; 126 /** map from universal quantifiers to their inst constant body */ 127 std::map< Node, Node > d_inst_const_body; 128 /** map from universal quantifiers to their counterexample literals */ 129 std::map< Node, Node > d_ce_lit; 130 /** instantiation constants to universal quantifiers */ 131 std::map< Node, Node > d_inst_constants_map; 132 public: 133 /** map from universal quantifiers to the list of instantiation constants */ 134 std::map< Node, std::vector< Node > > d_inst_constants; 135 /** get variable number */ getVariableNum(Node q,Node v)136 unsigned getVariableNum( Node q, Node v ) { return d_var_num[q][v]; } 137 /** get the i^th instantiation constant of q */ 138 Node getInstantiationConstant( Node q, int i ) const; 139 /** get number of instantiation constants for q */ 140 unsigned getNumInstantiationConstants( Node q ) const; 141 /** get the ce body q[e/x] */ 142 Node getInstConstantBody( Node q ); 143 /** get counterexample literal (for cbqi) */ 144 Node getCounterexampleLiteral( Node q ); 145 /** returns node n with bound vars of q replaced by instantiation constants of q 146 node n : is the future pattern 147 node q : is the quantifier containing which bind the variable 148 return a pattern where the variable are replaced by variable for 149 instantiation. 150 */ 151 Node substituteBoundVariablesToInstConstants(Node n, Node q); 152 /** substitute { instantiation constants of q -> bound variables of q } in n 153 */ 154 Node substituteInstConstantsToBoundVariables(Node n, Node q); 155 /** substitute { variables of q -> terms } in n */ 156 Node substituteBoundVariables(Node n, Node q, std::vector<Node>& terms); 157 /** substitute { instantiation constants of q -> terms } in n */ 158 Node substituteInstConstants(Node n, Node q, std::vector<Node>& terms); 159 160 static Node getInstConstAttr( Node n ); 161 static bool hasInstConstAttr( Node n ); 162 static Node getBoundVarAttr( Node n ); 163 static bool hasBoundVarAttr( Node n ); 164 165 private: 166 /** get bound vars */ 167 static void getBoundVars2( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ); 168 /** get bound vars */ 169 static Node getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ); 170 public: 171 //get the bound variables in this node 172 static void getBoundVars( Node n, std::vector< Node >& vars ); 173 //remove quantifiers 174 static Node getRemoveQuantifiers( Node n ); 175 //quantified simplify (treat free variables in n as quantified and run rewriter) 176 static Node getQuantSimplify( Node n ); 177 178 private: 179 /** adds the set of nodes of kind k in n to vars */ 180 static void computeVarContainsInternal(Node n, 181 Kind k, 182 std::vector<Node>& vars); 183 184 public: 185 /** adds the set of nodes of kind INST_CONSTANT in n to ics */ 186 static void computeInstConstContains(Node n, std::vector<Node>& ics); 187 /** adds the set of nodes of kind BOUND_VARIABLE in n to vars */ 188 static void computeVarContains(Node n, std::vector<Node>& vars); 189 /** adds the set of (top-level) nodes of kind FORALL in n to quants */ 190 static void computeQuantContains(Node n, std::vector<Node>& quants); 191 /** 192 * Adds the set of nodes of kind INST_CONSTANT in n that belong to quantified 193 * formula q to vars. 194 */ 195 static void computeInstConstContainsForQuant(Node q, 196 Node n, 197 std::vector<Node>& vars); 198 199 //for virtual term substitution 200 private: 201 Node d_vts_delta; 202 std::map< TypeNode, Node > d_vts_inf; 203 Node d_vts_delta_free; 204 std::map< TypeNode, Node > d_vts_inf_free; 205 /** get vts infinity index */ 206 Node getVtsInfinityIndex( int i, bool isFree = false, bool create = true ); 207 /** substitute vts free terms */ 208 Node substituteVtsFreeTerms( Node n ); 209 public: 210 /** get vts delta */ 211 Node getVtsDelta( bool isFree = false, bool create = true ); 212 /** get vts infinity */ 213 Node getVtsInfinity( TypeNode tn, bool isFree = false, bool create = true ); 214 /** get all vts terms */ 215 void getVtsTerms( std::vector< Node >& t, bool isFree = false, bool create = true, bool inc_delta = true ); 216 /** rewrite delta */ 217 Node rewriteVtsSymbols( Node n ); 218 /** simple check for contains term */ 219 bool containsVtsTerm( Node n, bool isFree = false ); 220 /** simple check for contains term */ 221 bool containsVtsTerm( std::vector< Node >& n, bool isFree = false ); 222 /** simple check for contains term */ 223 bool containsVtsInfinity( Node n, bool isFree = false ); 224 /** ensure type */ 225 static Node ensureType( Node n, TypeNode tn ); 226 227 //general utilities 228 // TODO #1216 : promote these? 229 private: 230 //helper for contains term 231 static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited ); 232 /** cache for getTypeValue */ 233 std::unordered_map<TypeNode, 234 std::unordered_map<int, Node>, 235 TypeNodeHashFunction> 236 d_type_value; 237 /** cache for getTypeMaxValue */ 238 std::unordered_map<TypeNode, Node, TypeNodeHashFunction> d_type_max_value; 239 /** cache for getTypeValueOffset */ 240 std::unordered_map<TypeNode, 241 std::unordered_map<Node, 242 std::unordered_map<int, Node>, 243 NodeHashFunction>, 244 TypeNodeHashFunction> 245 d_type_value_offset; 246 /** cache for status of getTypeValueOffset*/ 247 std::unordered_map<TypeNode, 248 std::unordered_map<Node, 249 std::unordered_map<int, int>, 250 NodeHashFunction>, 251 TypeNodeHashFunction> 252 d_type_value_offset_status; 253 254 public: 255 /** simple check for contains term, true if contains at least one term in t */ 256 static bool containsTerms( Node n, std::vector< Node >& t ); 257 /** contains uninterpreted constant */ 258 static bool containsUninterpretedConstant( Node n ); 259 /** get the term depth of n */ 260 static int getTermDepth( Node n ); 261 /** simple negate */ 262 static Node simpleNegate( Node n ); 263 /** is the kind k a negation kind? 264 * 265 * A kind k is a negation kind if <k>( <k>( n ) ) = n. 266 */ 267 static bool isNegate(Kind k); 268 /** 269 * Make negated term, returns the negation of n wrt Kind notk, eliminating 270 * double negation if applicable, e.g. mkNegate( ~, ~x ) ---> x. 271 */ 272 static Node mkNegate(Kind notk, Node n); 273 /** is k associative? 274 * 275 * If flag reqNAry is true, then we additionally require that k is an 276 * n-ary operator. 277 */ 278 static bool isAssoc(Kind k, bool reqNAry = false); 279 /** is k commutative? 280 * 281 * If flag reqNAry is true, then we additionally require that k is an 282 * n-ary operator. 283 */ 284 static bool isComm(Kind k, bool reqNAry = false); 285 286 /** is k non-additive? 287 * Returns true if 288 * <k>( <k>( T1, x, T2 ), x ) = 289 * <k>( T1, x, T2 ) 290 * always holds, where T1 and T2 are vectors. 291 */ 292 static bool isNonAdditive( Kind k ); 293 /** is k a bool connective? */ 294 static bool isBoolConnective( Kind k ); 295 /** is n a bool connective term? */ 296 static bool isBoolConnectiveTerm( TNode n ); 297 298 /** is the kind k antisymmetric? 299 * If so, return true and store its inverse kind in dk. 300 */ 301 static bool isAntisymmetric(Kind k, Kind& dk); 302 303 /** has offset arg 304 * Returns true if there is a Kind ok and offset 305 * such that 306 * <ik>( ... t_{arg-1}, n, t_{arg+1}... ) = 307 * <ok>( ... t_{arg-1}, n+offset, t_{arg+1}...) 308 * always holds. 309 * If so, this function returns true and stores 310 * offset and ok in the respective fields. 311 */ 312 static bool hasOffsetArg(Kind ik, int arg, int& offset, Kind& ok); 313 314 /** is idempotent arg 315 * Returns true if 316 * <k>( ... t_{arg-1}, n, t_{arg+1}...) = 317 * <k>( ... t_{arg-1}, t_{arg+1}...) 318 * always holds. 319 */ 320 bool isIdempotentArg(Node n, Kind ik, int arg); 321 322 /** is singular arg 323 * Returns true if 324 * <k>( ... t_{arg-1}, n, t_{arg+1}...) = ret 325 * always holds for some constant ret, which is returned by this function. 326 */ 327 Node isSingularArg(Node n, Kind ik, unsigned arg); 328 329 /** get type value 330 * This gets the Node that represents value val for Type tn 331 * This is used to get simple values, e.g. -1,0,1, 332 * in a uniform way per type. 333 */ 334 Node getTypeValue(TypeNode tn, int val); 335 336 /** get type value offset 337 * Returns the value of ( val + getTypeValue( tn, offset ) ), 338 * where + is the additive operator for the type. 339 * Stores the status (0: success, -1: failure) in status. 340 */ 341 Node getTypeValueOffset(TypeNode tn, Node val, int offset, int& status); 342 343 /** get the "max" value for type tn 344 * For example, 345 * the max value for Bool is true, 346 * the max value for BitVector is 1..1. 347 */ 348 Node getTypeMaxValue(TypeNode tn); 349 350 /** make value, static version of get value */ 351 static Node mkTypeValue(TypeNode tn, int val); 352 /** make value offset, static version of get value offset */ 353 static Node mkTypeValueOffset(TypeNode tn, Node val, int offset, int& status); 354 /** make max value, static version of get max value */ 355 static Node mkTypeMaxValue(TypeNode tn); 356 /** 357 * Make const, returns pol ? mkTypeValue(tn,0) : mkTypeMaxValue(tn). 358 * In other words, this returns either the minimum element of tn if pol is 359 * true, and the maximum element in pol is false. The type tn should have 360 * minimum and maximum elements, for example tn is Bool or BitVector. 361 */ 362 static Node mkTypeConst(TypeNode tn, bool pol); 363 364 // for higher-order 365 private: 366 /** dummy predicate that states terms should be considered first-class members of equality engine */ 367 std::map< TypeNode, Node > d_ho_type_match_pred; 368 public: 369 /** get higher-order type match predicate 370 * This predicate is used to force certain functions f of type tn to appear as first-class representatives in the 371 * quantifier-free UF solver. For a typical use case, we call getHoTypeMatchPredicate which returns a fresh 372 * predicate P of type (tn -> Bool). Then, we add P( f ) as a lemma. 373 * TODO: we may eliminate this depending on how github issue #1115 is resolved. 374 */ 375 Node getHoTypeMatchPredicate( TypeNode tn ); 376 };/* class TermUtil */ 377 378 }/* CVC4::theory::quantifiers namespace */ 379 }/* CVC4::theory namespace */ 380 }/* CVC4 namespace */ 381 382 #endif /* __CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H */ 383