Branch data     Line data    Source code

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