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 "options/smt_options.h"
  20 #include "theory/bv/bv_solver_bitblast.h"
  21 #include "theory/bv/bv_solver_lazy.h"
  22 #include "theory/bv/bv_solver_simple.h"
  23 #include "theory/bv/theory_bv_utils.h"
  24
  25 namespace CVC4 {
  26 namespace theory {
  27 namespace bv {
  28
  29 TheoryBV::TheoryBV(context::Context* c,
  30                    context::UserContext* u,
  31                    OutputChannel& out,
  32                    Valuation valuation,
  33                    const LogicInfo& logicInfo,
  34                    ProofNodeManager* pnm,
  35                    std::string name)
  36     : Theory(THEORY_BV, c, u, out, valuation, logicInfo, pnm, name),
  37       d_internal(nullptr),
  38       d_ufDivByZero(),
  39       d_ufRemByZero(),
  40       d_rewriter(),
  41       d_state(c, u, valuation),
  42       d_im(*this, d_state, nullptr),
  43       d_notify(d_im)
  44 {
  45   switch (options::bvSolver())
  46   {
  47     case options::BVSolver::BITBLAST:
  48       d_internal.reset(new BVSolverBitblast(&d_state, d_im, pnm));
  49       break;
  50
  51     case options::BVSolver::LAZY:
  52       d_internal.reset(new BVSolverLazy(*this, c, u, pnm, name));
  53       break;
  54
  55     default:
  56       AlwaysAssert(options::bvSolver() == options::BVSolver::SIMPLE);
  57       d_internal.reset(new BVSolverSimple(&d_state, d_im, pnm));
  58   }
  59   d_theoryState = &d_state;
  60   d_inferManager = &d_im;
  61 }
  62
  63 TheoryBV::~TheoryBV() {}
  64
  65 TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; }
  66
  67 bool TheoryBV::needsEqualityEngine(EeSetupInfo& esi)
  68 {
  69   bool need_ee = d_internal->needsEqualityEngine(esi);
  70
  71   /* Set up default notify class for equality engine. */
  72   if (need_ee && esi.d_notify == nullptr)
  73   {
  74     esi.d_notify = &d_notify;
  75     esi.d_name = "theory::bv::ee";
  76   }
  77
  78   return need_ee;
  79 }
  80
  81 void TheoryBV::finishInit()
  82 {
  83   // these kinds are semi-evaluated in getModelValue (applications of this
  84   // kind are treated as variables)
  85   getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
  86   getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
  87   d_internal->finishInit();
  88
  89   eq::EqualityEngine* ee = getEqualityEngine();
  90   if (ee)
  91   {
  92     // The kinds we are treating as function application in congruence
  93     ee->addFunctionKind(kind::BITVECTOR_CONCAT, true);
  94     //    ee->addFunctionKind(kind::BITVECTOR_AND);
  95     //    ee->addFunctionKind(kind::BITVECTOR_OR);
  96     //    ee->addFunctionKind(kind::BITVECTOR_XOR);
  97     //    ee->addFunctionKind(kind::BITVECTOR_NOT);
  98     //    ee->addFunctionKind(kind::BITVECTOR_NAND);
  99     //    ee->addFunctionKind(kind::BITVECTOR_NOR);
 100     //    ee->addFunctionKind(kind::BITVECTOR_XNOR);
 101     //    ee->addFunctionKind(kind::BITVECTOR_COMP);
 102     ee->addFunctionKind(kind::BITVECTOR_MULT, true);
 103     ee->addFunctionKind(kind::BITVECTOR_PLUS, true);
 104     ee->addFunctionKind(kind::BITVECTOR_EXTRACT, true);
 105     //    ee->addFunctionKind(kind::BITVECTOR_SUB);
 106     //    ee->addFunctionKind(kind::BITVECTOR_NEG);
 107     //    ee->addFunctionKind(kind::BITVECTOR_UDIV);
 108     //    ee->addFunctionKind(kind::BITVECTOR_UREM);
 109     //    ee->addFunctionKind(kind::BITVECTOR_SDIV);
 110     //    ee->addFunctionKind(kind::BITVECTOR_SREM);
 111     //    ee->addFunctionKind(kind::BITVECTOR_SMOD);
 112     //    ee->addFunctionKind(kind::BITVECTOR_SHL);
 113     //    ee->addFunctionKind(kind::BITVECTOR_LSHR);
 114     //    ee->addFunctionKind(kind::BITVECTOR_ASHR);
 115     //    ee->addFunctionKind(kind::BITVECTOR_ULT);
 116     //    ee->addFunctionKind(kind::BITVECTOR_ULE);
 117     //    ee->addFunctionKind(kind::BITVECTOR_UGT);
 118     //    ee->addFunctionKind(kind::BITVECTOR_UGE);
 119     //    ee->addFunctionKind(kind::BITVECTOR_SLT);
 120     //    ee->addFunctionKind(kind::BITVECTOR_SLE);
 121     //    ee->addFunctionKind(kind::BITVECTOR_SGT);
 122     //    ee->addFunctionKind(kind::BITVECTOR_SGE);
 123     ee->addFunctionKind(kind::BITVECTOR_TO_NAT);
 124     ee->addFunctionKind(kind::INT_TO_BITVECTOR);
 125   }
 126 }
 127
 128 Node TheoryBV::getUFDivByZero(Kind k, unsigned width)
 129 {
 130   NodeManager* nm = NodeManager::currentNM();
 131   if (k == kind::BITVECTOR_UDIV)
 132   {
 133     if (d_ufDivByZero.find(width) == d_ufDivByZero.end())
 134     {
 135       // lazily create the function symbols
 136       std::ostringstream os;
 137       os << "BVUDivByZero_" << width;
 138       Node divByZero =
 139           nm->mkSkolem(os.str(),
 140                        nm->mkFunctionType(nm->mkBitVectorType(width),
 141                                           nm->mkBitVectorType(width)),
 142                        "partial bvudiv",
 143                        NodeManager::SKOLEM_EXACT_NAME);
 144       d_ufDivByZero[width] = divByZero;
 145     }
 146     return d_ufDivByZero[width];
 147   }
 148   else if (k == kind::BITVECTOR_UREM)
 149   {
 150     if (d_ufRemByZero.find(width) == d_ufRemByZero.end())
 151     {
 152       std::ostringstream os;
 153       os << "BVURemByZero_" << width;
 154       Node divByZero =
 155           nm->mkSkolem(os.str(),
 156                        nm->mkFunctionType(nm->mkBitVectorType(width),
 157                                           nm->mkBitVectorType(width)),
 158                        "partial bvurem",
 159                        NodeManager::SKOLEM_EXACT_NAME);
 160       d_ufRemByZero[width] = divByZero;
 161     }
 162     return d_ufRemByZero[width];
 163   }
 164
 165   Unreachable();
 166 }
 167
 168 TrustNode TheoryBV::expandDefinition(Node node)
 169 {
 170   Debug("bitvector-expandDefinition")
 171       << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
 172
 173   Node ret;
 174   switch (node.getKind())
 175   {
 176     case kind::BITVECTOR_SDIV:
 177     case kind::BITVECTOR_SREM:
 178     case kind::BITVECTOR_SMOD:
 179       ret = TheoryBVRewriter::eliminateBVSDiv(node);
 180       break;
 181
 182     case kind::BITVECTOR_UDIV:
 183     case kind::BITVECTOR_UREM:
 184     {
 185       NodeManager* nm = NodeManager::currentNM();
 186
 187       Kind kind = node.getKind() == kind::BITVECTOR_UDIV
 188                       ? kind::BITVECTOR_UDIV_TOTAL
 189                       : kind::BITVECTOR_UREM_TOTAL;
 190       ret = nm->mkNode(kind, node[0], node[1]);
 191       break;
 192     }
 193     break;
 194
 195     default: break;
 196   }
 197   if (!ret.isNull() && node != ret)
 198   {
 199     return TrustNode::mkTrustRewrite(node, ret, nullptr);
 200   }
 201   return TrustNode::null();
 202 }
 203
 204 void TheoryBV::preRegisterTerm(TNode node)
 205 {
 206   d_internal->preRegisterTerm(node);
 207
 208   eq::EqualityEngine* ee = getEqualityEngine();
 209   if (ee)
 210   {
 211     if (node.getKind() == kind::EQUAL)
 212     {
 213       ee->addTriggerPredicate(node);
 214     }
 215     else
 216     {
 217       ee->addTerm(node);
 218     }
 219   }
 220 }
 221
 222 bool TheoryBV::preCheck(Effort e) { return d_internal->preCheck(e); }
 223
 224 void TheoryBV::postCheck(Effort e) { d_internal->postCheck(e); }
 225
 226 bool TheoryBV::preNotifyFact(
 227     TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
 228 {
 229   return d_internal->preNotifyFact(atom, pol, fact, isPrereg, isInternal);
 230 }
 231
 232 void TheoryBV::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
 233 {
 234   d_internal->notifyFact(atom, pol, fact, isInternal);
 235 }
 236
 237 bool TheoryBV::needsCheckLastEffort()
 238 {
 239   return d_internal->needsCheckLastEffort();
 240 }
 241
 242 bool TheoryBV::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
 243 {
 244   return d_internal->collectModelValues(m, termSet);
 245 }
 246
 247 void TheoryBV::propagate(Effort e) { return d_internal->propagate(e); }
 248
 249 Theory::PPAssertStatus TheoryBV::ppAssert(
 250     TrustNode tin, TrustSubstitutionMap& outSubstitutions)
 251 {
 252   return d_internal->ppAssert(tin, outSubstitutions);
 253 }
 254
 255 TrustNode TheoryBV::ppRewrite(TNode t)
 256 {
 257   // first, see if we need to expand definitions
 258   TrustNode texp = expandDefinition(t);
 259   if (!texp.isNull())
 260   {
 261     return texp;
 262   }
 263   return d_internal->ppRewrite(t);
 264 }
 265
 266 void TheoryBV::presolve() { d_internal->presolve(); }
 267
 268 EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
 269 {
 270   return d_internal->getEqualityStatus(a, b);
 271 }
 272
 273 TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); }
 274
 275 void TheoryBV::notifySharedTerm(TNode t)
 276 {
 277   d_internal->notifySharedTerm(t);
 278 }
 279
 280 void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned)
 281 {
 282   d_internal->ppStaticLearn(in, learned);
 283 }
 284
 285 bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions,
 286                                 std::vector<Node>& new_assertions)
 287 {
 288   return d_internal->applyAbstraction(assertions, new_assertions);
 289 }
 290
 291 }  // namespace bv
 292 }  // namespace theory
 293 }  // namespace CVC4