src/theory/bv/theory_bv.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Mathias Preiner, Andrew Reynolds, Haniel Barbosa
   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  * Theory of bit-vectors.
  14  */
  15
  16 #include "theory/bv/theory_bv.h"
  17
  18 #include "options/bv_options.h"
  19 #include "options/smt_options.h"
  20 #include "proof/proof_checker.h"
  21 #include "smt/smt_statistics_registry.h"
  22 #include "theory/bv/bv_solver_bitblast.h"
  23 #include "theory/bv/bv_solver_bitblast_internal.h"
  24 #include "theory/bv/bv_solver_layered.h"
  25 #include "theory/bv/theory_bv_utils.h"
  26 #include "theory/ee_setup_info.h"
  27 #include "theory/trust_substitutions.h"
  28
  29 namespace cvc5 {
  30 namespace theory {
  31 namespace bv {
  32
  33 TheoryBV::TheoryBV(context::Context* c,
  34                    context::UserContext* u,
  35                    OutputChannel& out,
  36                    Valuation valuation,
  37                    const LogicInfo& logicInfo,
  38                    ProofNodeManager* pnm,
  39                    std::string name)
  40     : Theory(THEORY_BV, c, u, out, valuation, logicInfo, pnm, name),
  41       d_internal(nullptr),
  42       d_rewriter(),
  43       d_state(c, u, valuation),
  44       d_im(*this, d_state, nullptr, "theory::bv::"),
  45       d_notify(d_im),
  46       d_stats("theory::bv::")
  47 {
  48   switch (options::bvSolver())
  49   {
  50     case options::BVSolver::BITBLAST:
  51       d_internal.reset(new BVSolverBitblast(&d_state, d_im, pnm));
  52       break;
  53
  54     case options::BVSolver::LAYERED:
  55       d_internal.reset(new BVSolverLayered(*this, c, u, pnm, name));
  56       break;
  57
  58     default:
  59       AlwaysAssert(options::bvSolver() == options::BVSolver::BITBLAST_INTERNAL);
  60       d_internal.reset(new BVSolverBitblastInternal(&d_state, d_im, pnm));
  61   }
  62   d_theoryState = &d_state;
  63   d_inferManager = &d_im;
  64 }
  65
  66 TheoryBV::~TheoryBV() {}
  67
  68 TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; }
  69
  70 ProofRuleChecker* TheoryBV::getProofChecker()
  71 {
  72   if (options::bvSolver() == options::BVSolver::BITBLAST_INTERNAL)
  73   {
  74     return static_cast<BVSolverBitblastInternal*>(d_internal.get())
  75         ->getProofChecker();
  76   }
  77   return nullptr;
  78 }
  79
  80 bool TheoryBV::needsEqualityEngine(EeSetupInfo& esi)
  81 {
  82   bool need_ee = d_internal->needsEqualityEngine(esi);
  83
  84   /* Set up default notify class for equality engine. */
  85   if (need_ee && esi.d_notify == nullptr)
  86   {
  87     esi.d_notify = &d_notify;
  88     esi.d_name = "theory::bv::ee";
  89   }
  90
  91   return need_ee;
  92 }
  93
  94 void TheoryBV::finishInit()
  95 {
  96   // these kinds are semi-evaluated in getModelValue (applications of this
  97   // kind are treated as variables)
  98   getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
  99   getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
 100   d_internal->finishInit();
 101
 102   eq::EqualityEngine* ee = getEqualityEngine();
 103   if (ee)
 104   {
 105     // The kinds we are treating as function application in congruence
 106     ee->addFunctionKind(kind::BITVECTOR_CONCAT, true);
 107     //    ee->addFunctionKind(kind::BITVECTOR_AND);
 108     //    ee->addFunctionKind(kind::BITVECTOR_OR);
 109     //    ee->addFunctionKind(kind::BITVECTOR_XOR);
 110     //    ee->addFunctionKind(kind::BITVECTOR_NOT);
 111     //    ee->addFunctionKind(kind::BITVECTOR_NAND);
 112     //    ee->addFunctionKind(kind::BITVECTOR_NOR);
 113     //    ee->addFunctionKind(kind::BITVECTOR_XNOR);
 114     //    ee->addFunctionKind(kind::BITVECTOR_COMP);
 115     ee->addFunctionKind(kind::BITVECTOR_MULT, true);
 116     ee->addFunctionKind(kind::BITVECTOR_ADD, true);
 117     ee->addFunctionKind(kind::BITVECTOR_EXTRACT, true);
 118     //    ee->addFunctionKind(kind::BITVECTOR_SUB);
 119     //    ee->addFunctionKind(kind::BITVECTOR_NEG);
 120     //    ee->addFunctionKind(kind::BITVECTOR_UDIV);
 121     //    ee->addFunctionKind(kind::BITVECTOR_UREM);
 122     //    ee->addFunctionKind(kind::BITVECTOR_SDIV);
 123     //    ee->addFunctionKind(kind::BITVECTOR_SREM);
 124     //    ee->addFunctionKind(kind::BITVECTOR_SMOD);
 125     //    ee->addFunctionKind(kind::BITVECTOR_SHL);
 126     //    ee->addFunctionKind(kind::BITVECTOR_LSHR);
 127     //    ee->addFunctionKind(kind::BITVECTOR_ASHR);
 128     //    ee->addFunctionKind(kind::BITVECTOR_ULT);
 129     //    ee->addFunctionKind(kind::BITVECTOR_ULE);
 130     //    ee->addFunctionKind(kind::BITVECTOR_UGT);
 131     //    ee->addFunctionKind(kind::BITVECTOR_UGE);
 132     //    ee->addFunctionKind(kind::BITVECTOR_SLT);
 133     //    ee->addFunctionKind(kind::BITVECTOR_SLE);
 134     //    ee->addFunctionKind(kind::BITVECTOR_SGT);
 135     //    ee->addFunctionKind(kind::BITVECTOR_SGE);
 136     ee->addFunctionKind(kind::BITVECTOR_TO_NAT);
 137     ee->addFunctionKind(kind::INT_TO_BITVECTOR);
 138   }
 139 }
 140
 141 void TheoryBV::preRegisterTerm(TNode node)
 142 {
 143   d_internal->preRegisterTerm(node);
 144
 145   eq::EqualityEngine* ee = getEqualityEngine();
 146   if (ee)
 147   {
 148     if (node.getKind() == kind::EQUAL)
 149     {
 150       ee->addTriggerPredicate(node);
 151     }
 152     else
 153     {
 154       ee->addTerm(node);
 155     }
 156   }
 157 }
 158
 159 bool TheoryBV::preCheck(Effort e) { return d_internal->preCheck(e); }
 160
 161 void TheoryBV::postCheck(Effort e) { d_internal->postCheck(e); }
 162
 163 bool TheoryBV::preNotifyFact(
 164     TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
 165 {
 166   return d_internal->preNotifyFact(atom, pol, fact, isPrereg, isInternal);
 167 }
 168
 169 void TheoryBV::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
 170 {
 171   d_internal->notifyFact(atom, pol, fact, isInternal);
 172 }
 173
 174 bool TheoryBV::needsCheckLastEffort()
 175 {
 176   return d_internal->needsCheckLastEffort();
 177 }
 178
 179 void TheoryBV::computeRelevantTerms(std::set<Node>& termSet)
 180 {
 181   return d_internal->computeRelevantTerms(termSet);
 182 }
 183
 184 bool TheoryBV::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
 185 {
 186   return d_internal->collectModelValues(m, termSet);
 187 }
 188
 189 void TheoryBV::propagate(Effort e) { return d_internal->propagate(e); }
 190
 191 Theory::PPAssertStatus TheoryBV::ppAssert(
 192     TrustNode tin, TrustSubstitutionMap& outSubstitutions)
 193 {
 194   TNode in = tin.getNode();
 195   Kind k = in.getKind();
 196   if (k == kind::EQUAL)
 197   {
 198     // Substitute variables
 199     if (in[0].isVar() && isLegalElimination(in[0], in[1]))
 200     {
 201       ++d_stats.d_solveSubstitutions;
 202       outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
 203       return Theory::PP_ASSERT_STATUS_SOLVED;
 204     }
 205     if (in[1].isVar() && isLegalElimination(in[1], in[0]))
 206     {
 207       ++d_stats.d_solveSubstitutions;
 208       outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
 209       return Theory::PP_ASSERT_STATUS_SOLVED;
 210     }
 211     /**
 212      * Eliminate extract over bit-vector variables.
 213      *
 214      * Given x[h:l] = c, where c is a constant and x is a variable.
 215      *
 216      * We rewrite to:
 217      *
 218      * x = sk1::c       if l == 0, where bw(sk1) = bw(x)-1-h
 219      * x = c::sk2       if h == bw(x)-1, where bw(sk2) = l
 220      * x = sk1::c::sk2  otherwise, where bw(sk1) = bw(x)-1-h and bw(sk2) = l
 221      */
 222     Node node = Rewriter::rewrite(in);
 223     if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst())
 224         || (node[1].getKind() == kind::BITVECTOR_EXTRACT
 225             && node[0].isConst()))
 226     {
 227       Node extract = node[0].isConst() ? node[1] : node[0];
 228       if (extract[0].isVar())
 229       {
 230         Node c = node[0].isConst() ? node[0] : node[1];
 231
 232         uint32_t high = utils::getExtractHigh(extract);
 233         uint32_t low = utils::getExtractLow(extract);
 234         uint32_t var_bw = utils::getSize(extract[0]);
 235         std::vector<Node> children;
 236
 237         // create sk1 with size bw(x)-1-h
 238         if (low == 0 || high != var_bw - 1)
 239         {
 240           Assert(high != var_bw - 1);
 241           uint32_t skolem_size = var_bw - high - 1;
 242           Node skolem = utils::mkVar(skolem_size);
 243           children.push_back(skolem);
 244         }
 245
 246         children.push_back(c);
 247
 248         // create sk2 with size l
 249         if (high == var_bw - 1 || low != 0)
 250         {
 251           Assert(low != 0);
 252           uint32_t skolem_size = low;
 253           Node skolem = utils::mkVar(skolem_size);
 254           children.push_back(skolem);
 255         }
 256
 257         Node concat = utils::mkConcat(children);
 258         Assert(utils::getSize(concat) == utils::getSize(extract[0]));
 259         if (isLegalElimination(extract[0], concat))
 260         {
 261           outSubstitutions.addSubstitutionSolved(extract[0], concat, tin);
 262           return Theory::PP_ASSERT_STATUS_SOLVED;
 263         }
 264       }
 265     }
 266   }
 267   return Theory::PP_ASSERT_STATUS_UNSOLVED;
 268 }
 269
 270 TrustNode TheoryBV::ppRewrite(TNode t, std::vector<SkolemLemma>& lems)
 271 {
 272   // first, see if we need to expand definitions
 273   TrustNode texp = d_rewriter.expandDefinition(t);
 274   if (!texp.isNull())
 275   {
 276     return texp;
 277   }
 278   return d_internal->ppRewrite(t);
 279 }
 280
 281 void TheoryBV::presolve() { d_internal->presolve(); }
 282
 283 EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
 284 {
 285   return d_internal->getEqualityStatus(a, b);
 286 }
 287
 288 TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); }
 289
 290 void TheoryBV::notifySharedTerm(TNode t)
 291 {
 292   d_internal->notifySharedTerm(t);
 293 }
 294
 295 void TheoryBV::ppStaticLearn(TNode in, NodeBuilder& learned)
 296 {
 297   d_internal->ppStaticLearn(in, learned);
 298 }
 299
 300 bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions,
 301                                 std::vector<Node>& new_assertions)
 302 {
 303   return d_internal->applyAbstraction(assertions, new_assertions);
 304 }
 305
 306 TheoryBV::Statistics::Statistics(const std::string& name)
 307     : d_solveSubstitutions(
 308         smtStatisticsRegistry().registerInt(name + "NumSolveSubstitutions"))
 309 {
 310 }
 311
 312 }  // namespace bv
 313 }  // namespace theory
 314 }  // namespace cvc5