src/theory/bv/abstraction.h

   1 /*********************                                                        */
   2 /*! \file abstraction.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Guy Katz, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 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:
  50     ArgsTableEntry(unsigned n)
  51       : d_arity(n)
  52     {}
  53     ArgsTableEntry()
  54       : d_arity(0)
  55     {}
  56     void addArguments(const ArgsVec& args);
  57     typedef std::vector<ArgsVec>::iterator iterator;
  58
  59     iterator begin() { return d_data.begin(); }
  60     iterator end() { return d_data.end(); }
  61     unsigned getArity() { return d_arity; }
  62     unsigned getNumEntries() { return d_data.size(); }
  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;
  71     ArgsTable() {}
  72     void addEntry(TNode signature, const ArgsVec& args);
  73     ArgsTableEntry& getEntry(TNode signature);
  74     iterator begin() { return d_data.begin(); }
  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:
 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);
 159   bool isConjunctionOfAtomsRec(TNode node, TNodeSet& seen);
 160
 161   TNode getGeneralization(TNode term);
 162   void storeGeneralization(TNode s, TNode t);
 163
 164   // signature skolem stuff
 165   Node getGeneralizedSignature(Node node);
 166   Node getSignatureSkolem(TNode node);
 167
 168   unsigned getBitwidthIndex(unsigned bitwidth);
 169   void resetSignatureIndex();
 170   Node computeSignatureRec(TNode, NodeNodeMap&);
 171   void storeSignature(Node signature, TNode assertion);
 172   bool hasSignature(Node node);
 173
 174   Node substituteArguments(TNode signature, TNode apply, unsigned& i, TNodeTNodeMap& seen);
 175
 176   // crazy instantiation methods
 177   void generateInstantiations(unsigned current,
 178                               std::vector<ArgsTableEntry>& matches,
 179                               std::vector<std::vector<ArgsVec> >& instantiations,
 180                               std::vector<std::vector<ArgsVec> >& new_instantiations);
 181
 182   Node tryMatching(const std::vector<Node>& ss, const std::vector<TNode>& tt, TNode conflict);
 183   void makeFreshArgs(TNode func, std::vector<Node>& fresh_args);
 184   void makeFreshSkolems(TNode node, SubstitutionMap& map, SubstitutionMap& reverse_map);
 185
 186   void skolemizeArguments(std::vector<Node>& assertions);
 187   Node reverseAbstraction(Node assertion, NodeNodeMap& seen);
 188
 189   TNodeSet d_addedLemmas;
 190   TNodeSet d_lemmaAtoms;
 191   TNodeSet d_inputAtoms;
 192   void storeLemma(TNode lemma);
 193
 194   Statistics d_statistics;
 195
 196 public:
 197   AbstractionModule(const std::string& name)
 198     : d_argsTable()
 199     , d_signatureToFunc()
 200     , d_funcToSignature()
 201     , d_assertionToSignature()
 202     , d_signatures()
 203     , d_sigToGeneralization()
 204     , d_skolems()
 205     , d_signatureIndices()
 206     , d_signatureSkolems()
 207     , d_addedLemmas()
 208     , d_lemmaAtoms()
 209     , d_inputAtoms()
 210     , d_statistics(name)
 211   {}
 212   /**
 213    * returns true if there are new uninterepreted functions symbols in the output
 214    *
 215    * @param assertions
 216    * @param new_assertions
 217    *
 218    * @return
 219    */
 220   bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
 221   /**
 222    * Returns true if the node represents an abstraction predicate.
 223    *
 224    * @param node
 225    *
 226    * @return
 227    */
 228   bool isAbstraction(TNode node);
 229   /**
 230    * Returns the interpretation of the abstraction predicate.
 231    *
 232    * @param node
 233    *
 234    * @return
 235    */
 236   Node getInterpretation(TNode node);
 237   Node simplifyConflict(TNode conflict);
 238   void generalizeConflict(TNode conflict, std::vector<Node>& lemmas);
 239   void addInputAtom(TNode atom);
 240   bool isLemmaAtom(TNode node) const;
 241 };
 242
 243 }
 244 }
 245 }
 246
 247 #endif