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                 :            :  * Wrap assertions in BITVECTOR_EAGER_ATOM nodes.
      11                 :            :  *
      12                 :            :  * This preprocessing pass wraps all assertions in BITVECTOR_EAGER_ATOM nodes
      13                 :            :  * and allows to use eager bit-blasting in the BV solver.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "preprocessing/passes/bv_eager_atoms.h"
      17                 :            : 
      18                 :            : #include "options/smt_options.h"
      19                 :            : #include "preprocessing/assertion_pipeline.h"
      20                 :            : #include "preprocessing/preprocessing_pass_context.h"
      21                 :            : #include "proof/proof.h"
      22                 :            : #include "theory/theory_engine.h"
      23                 :            : #include "theory/theory_model.h"
      24                 :            : 
      25                 :            : namespace cvc5::internal {
      26                 :            : namespace preprocessing {
      27                 :            : namespace passes {
      28                 :            : 
      29                 :            : /**
      30                 :            :  * A proof generator for turning formulas F into (BITVECTOR_EAGER_ATOM F).
      31                 :            :  */
      32                 :            : class BVEagerAtomProofGenerator : protected EnvObj, public ProofGenerator
      33                 :            : {
      34                 :            :  public:
      35                 :      20156 :   BVEagerAtomProofGenerator(Env& env) : EnvObj(env) {}
      36                 :      40278 :   virtual ~BVEagerAtomProofGenerator() {}
      37                 :            :   /**
      38                 :            :    * Proves (BITVECTOR_EAGER_ATOM F) from F via:
      39                 :            :    *
      40                 :            :    *     ---------------------------- BV_EAGER_ATOM
      41                 :            :    *     (BITVECTOR_EAGER_ATOM F) = F
      42                 :            :    *     ---------------------------- SYMM
      43                 :            :    *     F = (BITVECTOR_EAGER_ATOM F)
      44                 :            :    */
      45                 :         38 :   std::shared_ptr<ProofNode> getProofFor(Node fact) override
      46                 :            :   {
      47                 :         38 :     Assert(fact.getKind() == Kind::EQUAL
      48                 :            :            && fact[1].getKind() == Kind::BITVECTOR_EAGER_ATOM
      49                 :            :            && fact[1][0] == fact[0]);
      50                 :         76 :     CDProof cdp(d_env);
      51                 :         76 :     Node eq = fact[1].eqNode(fact[0]);
      52                 :         76 :     cdp.addStep(eq, ProofRule::BV_EAGER_ATOM, {}, {fact[1]});
      53                 :         76 :     return cdp.getProofFor(fact);
      54                 :         38 :   }
      55                 :            :   /** identify */
      56                 :          0 :   std::string identify() const override { return "BVEagerAtomProofGenerator"; }
      57                 :            : };
      58                 :            : 
      59                 :      51756 : BvEagerAtoms::BvEagerAtoms(PreprocessingPassContext* preprocContext)
      60                 :            :     : PreprocessingPass(preprocContext, "bv-eager-atoms"),
      61         [ +  + ]:      51756 :       d_proof(options().smt.produceProofs ? new BVEagerAtomProofGenerator(d_env)
      62                 :      51756 :                                           : nullptr)
      63                 :            : {
      64                 :      51756 : }
      65                 :            : 
      66                 :         52 : PreprocessingPassResult BvEagerAtoms::applyInternal(
      67                 :            :     AssertionPipeline* assertionsToPreprocess)
      68                 :            : {
      69                 :         52 :   NodeManager* nm = nodeManager();
      70         [ +  + ]:        802 :   for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
      71                 :            :   {
      72                 :        750 :     TNode atom = (*assertionsToPreprocess)[i];
      73         [ +  + ]:        750 :     if (atom.isConst())
      74                 :            :     {
      75                 :            :       // don't bother making true/false into atoms
      76                 :        269 :       continue;
      77                 :            :     }
      78                 :        481 :     Node eager_atom = nm->mkNode(Kind::BITVECTOR_EAGER_ATOM, atom);
      79         [ +  + ]:        481 :     assertionsToPreprocess->replace(i, eager_atom, d_proof.get());
      80         [ +  + ]:        750 :   }
      81                 :         52 :   return PreprocessingPassResult::NO_CONFLICT;
      82                 :            : }
      83                 :            : 
      84                 :            : }  // namespace passes
      85                 :            : }  // namespace preprocessing
      86                 :            : }  // namespace cvc5::internal