src/theory/bv/bitblast/node_bitblaster.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Mathias Preiner
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * Bitblaster used to bitblast to Boolean Nodes.
  14  */
  15 #include "cvc5_private.h"
  16
  17 #ifndef CVC5__THEORY__BV__BITBLAST_NODE_BITBLASTER_H
  18 #define CVC5__THEORY__BV__BITBLAST_NODE_BITBLASTER_H
  19
  20 #include "theory/bv/bitblast/bitblaster.h"
  21
  22 namespace cvc5 {
  23 namespace theory {
  24 namespace bv {
  25
  26 /**
  27  * Implementation of a simple Node-based bit-blaster.
  28  *
  29  * Implements the bare minimum to bit-blast bit-vector atoms/terms.
  30  */
  31 class NodeBitblaster : public TBitblaster<Node>
  32 {
  33   using Bits = std::vector<Node>;
  34
  35  public:
  36   NodeBitblaster(TheoryState* state);
  37   ~NodeBitblaster() = default;
  38
  39   /** Bit-blast term 'node' and return bit-blasted 'bits'. */
  40   void bbTerm(TNode node, Bits& bits) override;
  41   /** Bit-blast atom 'node'. */
  42   void bbAtom(TNode node) override;
  43   /** Get bit-blasted atom, returns 'atom' itself since it's Boolean. */
  44   Node getBBAtom(TNode atom) const override;
  45   /** Store Boolean node representing the bit-blasted atom. */
  46   void storeBBAtom(TNode atom, Node atom_bb) override;
  47   /** Store bits of bit-blasted term. */
  48   void storeBBTerm(TNode node, const Bits& bits) override;
  49   /** Check if atom was already bit-blasted. */
  50   bool hasBBAtom(TNode atom) const override;
  51   /** Get bit-blasted node stored for atom. */
  52   Node getStoredBBAtom(TNode node);
  53   /** Create 'bits' for variable 'var'. */
  54   void makeVariable(TNode var, Bits& bits) override;
  55
  56   /** Add d_variables to termSet. */
  57   void computeRelevantTerms(std::set<Node>& termSet);
  58   /** Collect model values for all relevant terms given in 'relevantTerms'. */
  59   bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms);
  60
  61   prop::SatSolver* getSatSolver() override { Unreachable(); }
  62
  63   /** Checks whether node is a variable introduced via `makeVariable`.*/
  64   bool isVariable(TNode node);
  65
  66  private:
  67   /** Query SAT solver for assignment of node 'a'. */
  68   Node getModelFromSatSolver(TNode a, bool fullModel) override;
  69
  70   /** Caches variables for which we already created bits. */
  71   TNodeSet d_variables;
  72   /** Stores bit-blasted atoms. */
  73   std::unordered_map<Node, Node> d_bbAtoms;
  74   /** Theory state. */
  75   TheoryState* d_state;
  76 };
  77
  78 }  // namespace bv
  79 }  // namespace theory
  80 }  // namespace cvc5
  81
  82 #endif