Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Method for handling cases of TheoryBv::ppAssert.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/bv/bv_pp_assert.h"
      14                 :            : 
      15                 :            : #include "expr/skolem_manager.h"
      16                 :            : #include "proof/proof.h"
      17                 :            : #include "smt/env.h"
      18                 :            : #include "theory/bv/theory_bv_utils.h"
      19                 :            : #include "theory/trust_substitutions.h"
      20                 :            : 
      21                 :            : namespace cvc5::internal {
      22                 :            : namespace theory {
      23                 :            : namespace bv {
      24                 :            : 
      25                 :      50937 : BvPpAssert::BvPpAssert(Env& env, Valuation val)
      26                 :            :     : EnvObj(env),
      27                 :      50937 :       d_valuation(val),
      28                 :      50937 :       d_ppsolves(userContext()),
      29                 :     101874 :       d_origForm(userContext())
      30                 :            : {
      31                 :      50937 : }
      32                 :            : 
      33                 :      50592 : BvPpAssert::~BvPpAssert() {}
      34                 :            : 
      35                 :       1592 : bool BvPpAssert::ppAssert(TrustNode tin, TrustSubstitutionMap& outSubstitutions)
      36                 :            : {
      37                 :            :   /**
      38                 :            :    * Eliminate extract over bit-vector variables.
      39                 :            :    *
      40                 :            :    * Given x[h:l] = c, where c is a constant and x is a variable.
      41                 :            :    *
      42                 :            :    * We rewrite to:
      43                 :            :    *
      44                 :            :    * x = sk1::c       if l == 0, where bw(sk1) = bw(x)-1-h
      45                 :            :    * x = c::sk2       if h == bw(x)-1, where bw(sk2) = l
      46                 :            :    * x = sk1::c::sk2  otherwise, where bw(sk1) = bw(x)-1-h and bw(sk2) = l
      47                 :            :    */
      48                 :       3184 :   Node node = rewrite(tin.getNode());
      49                 :       1802 :   if ((node[0].getKind() == Kind::BITVECTOR_EXTRACT && node[1].isConst())
      50                 :       1802 :       || (node[1].getKind() == Kind::BITVECTOR_EXTRACT && node[0].isConst()))
      51                 :            :   {
      52         [ +  + ]:        136 :     Node extract = node[0].isConst() ? node[1] : node[0];
      53         [ +  + ]:        136 :     if (extract[0].isVar())
      54                 :            :     {
      55         [ +  + ]:        107 :       Node c = node[0].isConst() ? node[0] : node[1];
      56                 :            : 
      57                 :        107 :       uint32_t high = utils::getExtractHigh(extract);
      58                 :        107 :       uint32_t low = utils::getExtractLow(extract);
      59                 :        107 :       uint32_t var_bw = utils::getSize(extract[0]);
      60                 :        107 :       std::vector<Node> children;
      61                 :        107 :       std::vector<Node> ochildren;
      62                 :            : 
      63                 :        107 :       SkolemManager* sm = nodeManager()->getSkolemManager();
      64                 :            :       // create sk1 with size bw(x)-1-h
      65 [ +  + ][ +  + ]:        107 :       if (low == 0 || high != var_bw - 1)
      66                 :            :       {
      67 [ -  + ][ -  + ]:         86 :         Assert(high != var_bw - 1);
                 [ -  - ]
      68                 :        172 :         Node ext = utils::mkExtract(extract[0], var_bw - 1, high + 1);
      69                 :         86 :         Node skolem = sm->mkPurifySkolem(ext);
      70                 :         86 :         children.push_back(skolem);
      71                 :         86 :         ochildren.push_back(ext);
      72                 :         86 :       }
      73                 :            : 
      74                 :        107 :       children.push_back(c);
      75                 :        107 :       ochildren.push_back(c);
      76                 :            : 
      77                 :            :       // create sk2 with size l
      78 [ +  + ][ +  + ]:        107 :       if (high == var_bw - 1 || low != 0)
      79                 :            :       {
      80 [ -  + ][ -  + ]:         32 :         Assert(low != 0);
                 [ -  - ]
      81                 :         64 :         Node ext = utils::mkExtract(extract[0], low - 1, 0);
      82                 :         32 :         Node skolem = sm->mkPurifySkolem(ext);
      83                 :         32 :         children.push_back(skolem);
      84                 :         32 :         ochildren.push_back(ext);
      85                 :         32 :       }
      86                 :            : 
      87                 :        107 :       Node concat = utils::mkConcat(children);
      88 [ -  + ][ -  + ]:        214 :       AssertEqual(utils::getSize(concat), utils::getSize(extract[0]));
                 [ -  - ]
      89         [ +  - ]:        107 :       if (d_valuation.isLegalElimination(extract[0], concat))
      90                 :            :       {
      91         [ +  + ]:        107 :         if (d_env.isProofProducing())
      92                 :            :         {
      93                 :         74 :           Node oconcat = utils::mkConcat(ochildren);
      94                 :         74 :           d_origForm[concat] = oconcat;
      95                 :         74 :         }
      96                 :        107 :         addSubstitution(outSubstitutions, extract[0], concat, tin);
      97                 :        107 :         return true;
      98                 :            :       }
      99 [ -  + ][ -  + ]:        428 :     }
         [ -  + ][ -  + ]
     100         [ +  + ]:        136 :   }
     101                 :       1485 :   return false;
     102                 :       1592 : }
     103                 :         61 : std::shared_ptr<ProofNode> BvPpAssert::getProofFor(Node fact)
     104                 :            : {
     105 [ -  + ][ -  + ]:         61 :   Assert(fact.getKind() == Kind::EQUAL);
                 [ -  - ]
     106                 :         61 :   context::CDHashMap<Node, TrustNode>::iterator it = d_ppsolves.find(fact);
     107         [ -  + ]:         61 :   if (it == d_ppsolves.end())
     108                 :            :   {
     109                 :          0 :     DebugUnhandled() << "BvPpAssert::getProofFor: Failed to find source for "
     110                 :            :                      << fact;
     111                 :            :     return nullptr;
     112                 :            :   }
     113                 :         61 :   Node assump = it->second.getProven();
     114 [ -  + ][ -  + ]:         61 :   Assert(assump.getKind() == Kind::EQUAL);
                 [ -  - ]
     115                 :         61 :   context::CDHashMap<Node, Node>::iterator ito;
     116                 :         61 :   ito = d_origForm.find(fact[1]);
     117                 :         61 :   Node oconcat = ito->second;
     118         [ +  - ]:         61 :   Trace("bv-pp-assert") << "Find proof: " << fact << std::endl;
     119         [ +  - ]:         61 :   Trace("bv-pp-assert") << "Have: " << assump << std::endl;
     120         [ +  - ]:         61 :   Trace("bv-pp-assert") << "Orig form: " << oconcat << std::endl;
     121                 :        122 :   CDProof cdp(d_env);
     122                 :         61 :   Node eqo = fact[0].eqNode(oconcat);
     123                 :         61 :   Node equiv = assump.eqNode(eqo);
     124                 :         61 :   std::shared_ptr<ProofNode> pfa = it->second.toProofNode();
     125                 :         61 :   cdp.addProof(pfa);
     126                 :            :   // This step should be justifiable by a RARE rule bv-eq-extract-elim{1,2,3}
     127                 :         61 :   cdp.addTrustedStep(equiv, TrustId::BV_PP_ASSERT, {}, {});
     128 [ +  + ][ -  - ]:        183 :   cdp.addStep(eqo, ProofRule::EQ_RESOLVE, {assump, equiv}, {});
     129                 :            :   // Justify the usage of purification skolems
     130                 :        183 :   cdp.addStep(fact, ProofRule::MACRO_SR_PRED_TRANSFORM, {eqo}, {fact});
     131                 :         61 :   return cdp.getProofFor(fact);
     132                 :         61 : }
     133                 :            : 
     134                 :          0 : std::string BvPpAssert::identify() const { return "BvPpAssert"; }
     135                 :            : 
     136                 :        107 : void BvPpAssert::addSubstitution(TrustSubstitutionMap& outSubstitutions,
     137                 :            :                                  const Node& x,
     138                 :            :                                  const Node& t,
     139                 :            :                                  TrustNode tin)
     140                 :            : {
     141         [ +  + ]:        107 :   if (d_env.isProofProducing())
     142                 :            :   {
     143                 :         74 :     Node eq = x.eqNode(t);
     144                 :         74 :     d_ppsolves[eq] = tin;
     145                 :            :     // we will provide the proof of (= x t)
     146                 :         74 :     TrustNode tnew = TrustNode::mkTrustLemma(eq, this);
     147                 :         74 :     outSubstitutions.addSubstitutionSolved(x, t, tnew);
     148                 :         74 :   }
     149                 :            :   else
     150                 :            :   {
     151                 :         33 :     outSubstitutions.addSubstitutionSolved(x, t, tin);
     152                 :            :   }
     153                 :        107 : }
     154                 :            : 
     155                 :            : }  // namespace bv
     156                 :            : }  // namespace theory
     157                 :            : }  // namespace cvc5::internal