1 /********************* */ 2 /*! \file arith_ite_utils.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Tim King, Aina Niemetz 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 [[ Add one-line brief description here ]] 13 ** 14 ** [[ Add lengthier description here ]] 15 ** \todo document this file 16 **/ 17 18 // Pass 1: label the ite as (constant) or (+ constant variable) 19 20 #include "cvc4_private.h" 21 22 #ifndef __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H 23 #define __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H 24 25 #include <unordered_map> 26 27 #include "expr/node.h" 28 #include "context/cdo.h" 29 #include "context/cdinsert_hashmap.h" 30 31 namespace CVC4 { 32 namespace preprocessing { 33 namespace util { 34 class ContainsTermITEVisitor; 35 } 36 } // namespace preprocessing 37 38 namespace theory { 39 40 class SubstitutionMap; 41 class TheoryModel; 42 43 namespace arith { 44 45 class ArithIteUtils { 46 preprocessing::util::ContainsTermITEVisitor& d_contains; 47 SubstitutionMap* d_subs; 48 TheoryModel* d_model; 49 50 typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; 51 // cache for reduce vars 52 NodeMap d_reduceVar; // if reduceVars[n].isNull(), treat reduceVars[n] == n 53 54 // reduceVars[n] = d_constants[n] + d_varParts[n] 55 NodeMap d_constants; // d_constants[n] is a constant ite tree 56 NodeMap d_varParts; // d_varParts[n] is a polynomial 57 58 59 NodeMap d_reduceGcd; 60 typedef std::unordered_map<Node, Integer, NodeHashFunction> NodeIntegerMap; 61 NodeIntegerMap d_gcds; 62 63 Integer d_one; 64 65 context::CDO<unsigned> d_subcount; 66 typedef context::CDInsertHashMap<Node, Node, NodeHashFunction> CDNodeMap; 67 CDNodeMap d_skolems; 68 69 typedef std::map<Node, std::set<Node> > ImpMap; 70 ImpMap d_implies; 71 72 std::vector<Node> d_skolemsAdded; 73 74 std::vector<Node> d_orBinEqs; 75 76 public: 77 ArithIteUtils(preprocessing::util::ContainsTermITEVisitor& contains, 78 context::Context* userContext, 79 TheoryModel* model); 80 ~ArithIteUtils(); 81 82 //(ite ?v_2 ?v_1 (ite ?v_3 (- ?v_1 128) (- ?v_1 256))) 83 84 /** removes common sums variables sums from term ites. */ 85 Node reduceVariablesInItes(Node n); 86 87 Node reduceConstantIteByGCD(Node n); 88 89 void clear(); 90 91 Node applySubstitutions(TNode f); 92 unsigned getSubCount() const; 93 94 void learnSubstitutions(const std::vector<Node>& assertions); 95 96 private: 97 /* applies this to all children of n and constructs the result */ 98 Node applyReduceVariablesInItes(Node n); 99 100 const Integer& gcdIte(Node n); 101 Node reduceIteConstantIteByGCD_rec(Node n, const Rational& q); 102 Node reduceIteConstantIteByGCD(Node n); 103 104 void addSubstitution(TNode f, TNode t); 105 Node selectForCmp(Node n) const; 106 107 void collectAssertions(TNode assertion); 108 void addImplications(Node x, Node y); 109 Node findIteCnd(TNode tb, TNode fb) const; 110 bool solveBinOr(TNode binor); 111 112 }; /* class ArithIteUtils */ 113 114 }/* CVC4::theory::arith namespace */ 115 }/* CVC4::theory namespace */ 116 }/* CVC4 namespace */ 117 118 #endif /* __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H */ 119