1 /********************* */ 2 /*! \file abstraction.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Liana Hadarean, Tim King, Guy Katz 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 Bitvector theory. 13 ** 14 ** Bitvector theory. 15 **/ 16 17 #include "cvc4_private.h" 18 19 #ifndef __CVC4__THEORY__BV__ABSTRACTION_H 20 #define __CVC4__THEORY__BV__ABSTRACTION_H 21 22 #include <unordered_map> 23 #include <unordered_set> 24 25 #include "expr/node.h" 26 #include "theory/substitutions.h" 27 #include "util/statistics_registry.h" 28 29 namespace CVC4 { 30 namespace theory { 31 namespace bv { 32 33 typedef std::vector<TNode> ArgsVec; 34 35 class AbstractionModule { 36 37 struct Statistics { 38 IntStat d_numFunctionsAbstracted; 39 IntStat d_numArgsSkolemized; 40 TimerStat d_abstractionTime; 41 Statistics(const std::string& name); 42 ~Statistics(); 43 }; 44 45 46 class ArgsTableEntry { 47 std::vector<ArgsVec> d_data; 48 unsigned d_arity; 49 public: ArgsTableEntry(unsigned n)50 ArgsTableEntry(unsigned n) 51 : d_arity(n) 52 {} ArgsTableEntry()53 ArgsTableEntry() 54 : d_arity(0) 55 {} 56 void addArguments(const ArgsVec& args); 57 typedef std::vector<ArgsVec>::iterator iterator; 58 begin()59 iterator begin() { return d_data.begin(); } end()60 iterator end() { return d_data.end(); } getArity()61 unsigned getArity() { return d_arity; } getNumEntries()62 unsigned getNumEntries() { return d_data.size(); } getEntry(unsigned i)63 ArgsVec& getEntry(unsigned i ) { Assert (i < d_data.size()); return d_data[i]; } 64 }; 65 66 class ArgsTable { 67 std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data; 68 bool hasEntry(TNode signature) const; 69 public: 70 typedef std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator; ArgsTable()71 ArgsTable() {} 72 void addEntry(TNode signature, const ArgsVec& args); 73 ArgsTableEntry& getEntry(TNode signature); begin()74 iterator begin() { return d_data.begin(); } end()75 iterator end() { return d_data.end(); } 76 }; 77 78 /** 79 * Checks if one pattern is a generalization of the other 80 * 81 * @param s 82 * @param t 83 * 84 * @return 1 if s :> t, 2 if s <: t, 0 if they equivalent and -1 if they are incomparable 85 */ 86 static int comparePatterns(TNode s, TNode t); 87 88 class LemmaInstantiatior { 89 std::vector<TNode> d_functions; 90 std::vector<int> d_maxMatch; 91 ArgsTable& d_argsTable; 92 context::Context* d_ctx; 93 theory::SubstitutionMap d_subst; 94 TNode d_conflict; 95 std::vector<Node> d_lemmas; 96 97 void backtrack(std::vector<int>& stack); 98 int next(int val, int index); 99 bool isConsistent(const std::vector<int>& stack); 100 bool accept(const std::vector<int>& stack); 101 void mkLemma(); 102 public: LemmaInstantiatior(const std::vector<TNode> & functions,ArgsTable & table,TNode conflict)103 LemmaInstantiatior(const std::vector<TNode>& functions, ArgsTable& table, TNode conflict) 104 : d_functions(functions) 105 , d_argsTable(table) 106 , d_ctx(new context::Context()) 107 , d_subst(d_ctx) 108 , d_conflict(conflict) 109 , d_lemmas() 110 { 111 Debug("bv-abstraction-gen") << "LemmaInstantiator conflict:" << conflict << "\n"; 112 // initializing the search space 113 for (unsigned i = 0; i < functions.size(); ++i) { 114 TNode func_op = functions[i].getOperator(); 115 // number of matches for this function 116 unsigned maxCount = table.getEntry(func_op).getNumEntries(); 117 d_maxMatch.push_back(maxCount); 118 } 119 } 120 121 void generateInstantiations(std::vector<Node>& lemmas); 122 123 }; 124 125 typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap; 126 typedef std::unordered_map<Node, TNode, NodeHashFunction> NodeTNodeMap; 127 typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap; 128 typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap; 129 typedef std::unordered_map<Node, TNode, NodeHashFunction> TNodeNodeMap; 130 typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; 131 typedef std::unordered_map<unsigned, Node> IntNodeMap; 132 typedef std::unordered_map<unsigned, unsigned> IndexMap; 133 typedef std::unordered_map<unsigned, std::vector<Node> > SkolemMap; 134 typedef std::unordered_map<TNode, unsigned, TNodeHashFunction > SignatureMap; 135 136 ArgsTable d_argsTable; 137 138 // mapping between signature and uninterpreted function symbol used to 139 // abstract the signature 140 NodeNodeMap d_signatureToFunc; 141 NodeNodeMap d_funcToSignature; 142 143 NodeNodeMap d_assertionToSignature; 144 SignatureMap d_signatures; 145 NodeNodeMap d_sigToGeneralization; 146 TNodeSet d_skolems; 147 148 // skolems maps 149 IndexMap d_signatureIndices; 150 SkolemMap d_signatureSkolems; 151 152 void collectArgumentTypes(TNode sig, std::vector<TypeNode>& types, TNodeSet& seen); 153 void collectArguments(TNode node, TNode sig, std::vector<Node>& args, TNodeSet& seen); 154 void finalizeSignatures(); 155 Node abstractSignatures(TNode assertion); 156 Node computeSignature(TNode node); 157 158 bool isConjunctionOfAtoms(TNode node, TNodeSet& seen); 159 160 TNode getGeneralization(TNode term); 161 void storeGeneralization(TNode s, TNode t); 162 163 // signature skolem stuff 164 Node getGeneralizedSignature(Node node); 165 Node getSignatureSkolem(TNode node); 166 167 unsigned getBitwidthIndex(unsigned bitwidth); 168 void resetSignatureIndex(); 169 Node computeSignatureRec(TNode, NodeNodeMap&); 170 void storeSignature(Node signature, TNode assertion); 171 bool hasSignature(Node node); 172 173 Node substituteArguments(TNode signature, TNode apply, unsigned& i, TNodeTNodeMap& seen); 174 175 // crazy instantiation methods 176 void generateInstantiations(unsigned current, 177 std::vector<ArgsTableEntry>& matches, 178 std::vector<std::vector<ArgsVec> >& instantiations, 179 std::vector<std::vector<ArgsVec> >& new_instantiations); 180 181 Node tryMatching(const std::vector<Node>& ss, const std::vector<TNode>& tt, TNode conflict); 182 void makeFreshArgs(TNode func, std::vector<Node>& fresh_args); 183 void makeFreshSkolems(TNode node, SubstitutionMap& map, SubstitutionMap& reverse_map); 184 185 void skolemizeArguments(std::vector<Node>& assertions); 186 Node reverseAbstraction(Node assertion, NodeNodeMap& seen); 187 188 TNodeSet d_addedLemmas; 189 TNodeSet d_lemmaAtoms; 190 TNodeSet d_inputAtoms; 191 void storeLemma(TNode lemma); 192 193 Statistics d_statistics; 194 195 public: AbstractionModule(const std::string & name)196 AbstractionModule(const std::string& name) 197 : d_argsTable() 198 , d_signatureToFunc() 199 , d_funcToSignature() 200 , d_assertionToSignature() 201 , d_signatures() 202 , d_sigToGeneralization() 203 , d_skolems() 204 , d_signatureIndices() 205 , d_signatureSkolems() 206 , d_addedLemmas() 207 , d_lemmaAtoms() 208 , d_inputAtoms() 209 , d_statistics(name) 210 {} 211 /** 212 * returns true if there are new uninterepreted functions symbols in the output 213 * 214 * @param assertions 215 * @param new_assertions 216 * 217 * @return 218 */ 219 bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); 220 /** 221 * Returns true if the node represents an abstraction predicate. 222 * 223 * @param node 224 * 225 * @return 226 */ 227 bool isAbstraction(TNode node); 228 /** 229 * Returns the interpretation of the abstraction predicate. 230 * 231 * @param node 232 * 233 * @return 234 */ 235 Node getInterpretation(TNode node); 236 Node simplifyConflict(TNode conflict); 237 void generalizeConflict(TNode conflict, std::vector<Node>& lemmas); 238 void addInputAtom(TNode atom); 239 bool isLemmaAtom(TNode node) const; 240 }; 241 242 } 243 } 244 } 245 246 #endif 247