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