src/theory/bv/theory_bv.cpp

   1 /*********************                                                        */
   2 /*! \file theory_bv.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Mathias Preiner, Andrew Reynolds, Martin Brain
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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  ** [[ Add lengthier description here ]]
  13  ** \todo document this file
  14  **/
  15
  16 #include "theory/bv/theory_bv.h"
  17
  18 #include "options/bv_options.h"
  19 #include "theory/bv/bv_solver_lazy.h"
  20 #include "theory/bv/theory_bv_utils.h"
  21
  22 namespace CVC4 {
  23 namespace theory {
  24 namespace bv {
  25
  26 TheoryBV::TheoryBV(context::Context* c,
  27                    context::UserContext* u,
  28                    OutputChannel& out,
  29                    Valuation valuation,
  30                    const LogicInfo& logicInfo,
  31                    ProofNodeManager* pnm,
  32                    std::string name)
  33     : Theory(THEORY_BV, c, u, out, valuation, logicInfo, pnm, name),
  34       d_internal(nullptr),
  35       d_ufDivByZero(),
  36       d_ufRemByZero(),
  37       d_rewriter(),
  38       d_state(c, u, valuation),
  39       d_inferMgr(*this, d_state, pnm)
  40 {
  41   d_internal.reset(new BVSolverLazy(*this, c, u, pnm, name));
  42   d_theoryState = &d_state;
  43   d_inferManager = &d_inferMgr;
  44 }
  45
  46 TheoryBV::~TheoryBV() {}
  47
  48 TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; }
  49
  50 bool TheoryBV::needsEqualityEngine(EeSetupInfo& esi)
  51 {
  52   return d_internal->needsEqualityEngine(esi);
  53 }
  54
  55 void TheoryBV::finishInit()
  56 {
  57   // these kinds are semi-evaluated in getModelValue (applications of this
  58   // kind are treated as variables)
  59   getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
  60   getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
  61   d_internal->finishInit();
  62 }
  63
  64 Node TheoryBV::getUFDivByZero(Kind k, unsigned width)
  65 {
  66   NodeManager* nm = NodeManager::currentNM();
  67   if (k == kind::BITVECTOR_UDIV)
  68   {
  69     if (d_ufDivByZero.find(width) == d_ufDivByZero.end())
  70     {
  71       // lazily create the function symbols
  72       std::ostringstream os;
  73       os << "BVUDivByZero_" << width;
  74       Node divByZero =
  75           nm->mkSkolem(os.str(),
  76                        nm->mkFunctionType(nm->mkBitVectorType(width),
  77                                           nm->mkBitVectorType(width)),
  78                        "partial bvudiv",
  79                        NodeManager::SKOLEM_EXACT_NAME);
  80       d_ufDivByZero[width] = divByZero;
  81     }
  82     return d_ufDivByZero[width];
  83   }
  84   else if (k == kind::BITVECTOR_UREM)
  85   {
  86     if (d_ufRemByZero.find(width) == d_ufRemByZero.end())
  87     {
  88       std::ostringstream os;
  89       os << "BVURemByZero_" << width;
  90       Node divByZero =
  91           nm->mkSkolem(os.str(),
  92                        nm->mkFunctionType(nm->mkBitVectorType(width),
  93                                           nm->mkBitVectorType(width)),
  94                        "partial bvurem",
  95                        NodeManager::SKOLEM_EXACT_NAME);
  96       d_ufRemByZero[width] = divByZero;
  97     }
  98     return d_ufRemByZero[width];
  99   }
 100
 101   Unreachable();
 102 }
 103
 104 TrustNode TheoryBV::expandDefinition(Node node)
 105 {
 106   Debug("bitvector-expandDefinition")
 107       << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
 108
 109   Node ret;
 110   switch (node.getKind())
 111   {
 112     case kind::BITVECTOR_SDIV:
 113     case kind::BITVECTOR_SREM:
 114     case kind::BITVECTOR_SMOD:
 115       ret = TheoryBVRewriter::eliminateBVSDiv(node);
 116       break;
 117
 118     case kind::BITVECTOR_UDIV:
 119     case kind::BITVECTOR_UREM:
 120     {
 121       NodeManager* nm = NodeManager::currentNM();
 122       unsigned width = node.getType().getBitVectorSize();
 123
 124       if (options::bitvectorDivByZeroConst())
 125       {
 126         Kind kind = node.getKind() == kind::BITVECTOR_UDIV
 127                         ? kind::BITVECTOR_UDIV_TOTAL
 128                         : kind::BITVECTOR_UREM_TOTAL;
 129         ret = nm->mkNode(kind, node[0], node[1]);
 130         break;
 131       }
 132
 133       TNode num = node[0], den = node[1];
 134       Node den_eq_0 = nm->mkNode(kind::EQUAL, den, utils::mkZero(width));
 135       Node divTotalNumDen = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV
 136                                            ? kind::BITVECTOR_UDIV_TOTAL
 137                                            : kind::BITVECTOR_UREM_TOTAL,
 138                                        num,
 139                                        den);
 140       Node divByZero = getUFDivByZero(node.getKind(), width);
 141       Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
 142       ret = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
 143     }
 144     break;
 145
 146     default: break;
 147   }
 148   if (!ret.isNull() && node != ret)
 149   {
 150     return TrustNode::mkTrustRewrite(node, ret, nullptr);
 151   }
 152   return TrustNode::null();
 153 }
 154
 155 void TheoryBV::preRegisterTerm(TNode node)
 156 {
 157   d_internal->preRegisterTerm(node);
 158 }
 159
 160 bool TheoryBV::preCheck(Effort e) { return d_internal->preCheck(e); }
 161
 162 bool TheoryBV::needsCheckLastEffort()
 163 {
 164   return d_internal->needsCheckLastEffort();
 165 }
 166
 167 bool TheoryBV::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
 168 {
 169   return d_internal->collectModelValues(m, termSet);
 170 }
 171
 172 void TheoryBV::propagate(Effort e) { return d_internal->propagate(e); }
 173
 174 Theory::PPAssertStatus TheoryBV::ppAssert(TNode in,
 175                                           SubstitutionMap& outSubstitutions)
 176 {
 177   return d_internal->ppAssert(in, outSubstitutions);
 178 }
 179
 180 TrustNode TheoryBV::ppRewrite(TNode t) { return d_internal->ppRewrite(t); }
 181
 182 void TheoryBV::presolve() { d_internal->presolve(); }
 183
 184 TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); }
 185
 186 void TheoryBV::notifySharedTerm(TNode t)
 187 {
 188   d_internal->notifySharedTerm(t);
 189   // temporary, will be built into Theory::addSharedTerm
 190   if (d_equalityEngine != nullptr)
 191   {
 192     d_equalityEngine->addTriggerTerm(t, THEORY_BV);
 193   }
 194 }
 195
 196 void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned)
 197 {
 198   d_internal->ppStaticLearn(in, learned);
 199 }
 200
 201 bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions,
 202                                 std::vector<Node>& new_assertions)
 203 {
 204   return d_internal->applyAbstraction(assertions, new_assertions);
 205 }
 206
 207 }  // namespace bv
 208 }  // namespace theory
 209 }  // namespace CVC4