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                 :            :  * The TheoryRewriter class.
      11                 :            :  *
      12                 :            :  * The interface that theory rewriters implement.
      13                 :            :  */
      14                 :            : 
      15                 :            : #include "theory/theory_rewriter.h"
      16                 :            : 
      17                 :            : #include "smt/logic_exception.h"
      18                 :            : 
      19                 :            : namespace cvc5::internal {
      20                 :            : namespace theory {
      21                 :            : 
      22                 :          0 : std::ostream& operator<<(std::ostream& os, TheoryRewriteCtx trc)
      23                 :            : {
      24 [ -  - ][ -  - ]:          0 :   switch (trc)
      25                 :            :   {
      26                 :          0 :     case TheoryRewriteCtx::PRE_DSL: return os << "PRE_DSL";
      27                 :          0 :     case TheoryRewriteCtx::DSL_SUBCALL: return os << "DSL_SUBCALL";
      28                 :          0 :     case TheoryRewriteCtx::POST_DSL: return os << "POST_DSL";
      29                 :            :   }
      30                 :          0 :   Unreachable();
      31                 :            :   return os;
      32                 :            : }
      33                 :            : 
      34                 :          0 : std::ostream& operator<<(std::ostream& os, RewriteStatus rs)
      35                 :            : {
      36 [ -  - ][ -  - ]:          0 :   switch (rs)
      37                 :            :   {
      38                 :          0 :     case RewriteStatus::REWRITE_DONE:       return os << "DONE";
      39                 :          0 :     case RewriteStatus::REWRITE_AGAIN:      return os << "AGAIN";
      40                 :          0 :     case RewriteStatus::REWRITE_AGAIN_FULL: return os << "AGAIN_FULL";
      41                 :            :   }
      42                 :          0 :   Unreachable();
      43                 :            :   return os;
      44                 :            : }
      45                 :            : 
      46                 :    3741975 : TrustRewriteResponse::TrustRewriteResponse(RewriteStatus status,
      47                 :            :                                            Node n,
      48                 :            :                                            Node nr,
      49                 :    3741975 :                                            ProofGenerator* pg)
      50                 :    3741975 :     : d_status(status)
      51                 :            : {
      52                 :            :   // we always make non-null, regardless of whether n = nr
      53                 :    3741975 :   d_node = TrustNode::mkTrustRewrite(n, nr, pg);
      54                 :    3741975 : }
      55                 :            : 
      56                 :    1588688 : TrustRewriteResponse TheoryRewriter::postRewriteWithProof(TNode node)
      57                 :            : {
      58                 :    1588688 :   RewriteResponse response = postRewrite(node);
      59                 :            :   // by default, we return a trust rewrite response with no proof generator
      60                 :            :   return TrustRewriteResponse(
      61                 :    3177376 :       response.d_status, node, response.d_node, nullptr);
      62                 :    1588688 : }
      63                 :            : 
      64                 :    2153287 : TrustRewriteResponse TheoryRewriter::preRewriteWithProof(TNode node)
      65                 :            : {
      66                 :    2153287 :   RewriteResponse response = preRewrite(node);
      67                 :            :   // by default, we return a trust rewrite response with no proof generator
      68                 :            :   return TrustRewriteResponse(
      69                 :    4306574 :       response.d_status, node, response.d_node, nullptr);
      70                 :    2153287 : }
      71                 :            : 
      72                 :         60 : Node TheoryRewriter::rewriteEqualityExt(Node node) { return node; }
      73                 :            : 
      74                 :        856 : TrustNode TheoryRewriter::rewriteEqualityExtWithProof(Node node)
      75                 :            : {
      76                 :        856 :   Node nodeRew = rewriteEqualityExt(node);
      77         [ +  - ]:        856 :   if (nodeRew != node)
      78                 :            :   {
      79                 :            :     // by default, we return a trust rewrite response with no proof generator
      80                 :        856 :     return TrustNode::mkTrustRewrite(node, nodeRew, nullptr);
      81                 :            :   }
      82                 :            :   // no rewrite
      83                 :          0 :   return TrustNode::null();
      84                 :        856 : }
      85                 :            : 
      86                 :     146857 : Node TheoryRewriter::expandDefinition(CVC5_UNUSED Node node)
      87                 :            : {
      88                 :            :   // no expansion
      89                 :     146857 :   return Node::null();
      90                 :            : }
      91                 :            : 
      92                 :          0 : Node TheoryRewriter::rewriteViaRule(CVC5_UNUSED ProofRewriteRule pr,
      93                 :            :                                     const Node& n)
      94                 :            : {
      95                 :          0 :   return n;
      96                 :            : }
      97                 :            : 
      98                 :    1169617 : ProofRewriteRule TheoryRewriter::findRule(const Node& a,
      99                 :            :                                           const Node& b,
     100                 :            :                                           TheoryRewriteCtx ctx)
     101                 :            : {
     102                 :    1169617 :   std::vector<ProofRewriteRule>& rules = d_pfTheoryRewrites[ctx];
     103         [ +  + ]:    3260690 :   for (ProofRewriteRule r : rules)
     104                 :            :   {
     105         [ +  + ]:    2140468 :     if (rewriteViaRule(r, a) == b)
     106                 :            :     {
     107                 :      49395 :       return r;
     108                 :            :     }
     109                 :            :   }
     110                 :    1120222 :   return ProofRewriteRule::NONE;
     111                 :            : }
     112                 :            : 
     113                 :    5165249 : void TheoryRewriter::registerProofRewriteRule(ProofRewriteRule id,
     114                 :            :                                               TheoryRewriteCtx ctx)
     115                 :            : {
     116                 :    5165249 :   std::vector<ProofRewriteRule>& rules = d_pfTheoryRewrites[ctx];
     117                 :    5165249 :   rules.push_back(id);
     118                 :            :   // theory rewrites marked DSL_SUBCALL are also tried at PRE_DSL effort.
     119         [ +  + ]:    5165249 :   if (ctx == TheoryRewriteCtx::DSL_SUBCALL)
     120                 :            :   {
     121                 :     424511 :     d_pfTheoryRewrites[TheoryRewriteCtx::PRE_DSL].push_back(id);
     122                 :            :   }
     123                 :    5165249 : }
     124                 :            : 
     125                 :   60436591 : NodeManager* TheoryRewriter::nodeManager() const { return d_nm; }
     126                 :            : 
     127                 :         20 : NoOpTheoryRewriter::NoOpTheoryRewriter(NodeManager* nm, TheoryId tid)
     128                 :         20 :     : TheoryRewriter(nm), d_tid(tid)
     129                 :            : {
     130                 :         20 : }
     131                 :            : 
     132                 :          0 : RewriteResponse NoOpTheoryRewriter::postRewrite(TNode node)
     133                 :            : {
     134                 :          0 :   return RewriteResponse(REWRITE_DONE, node);
     135                 :            : }
     136                 :          0 : RewriteResponse NoOpTheoryRewriter::preRewrite(TNode node)
     137                 :            : {
     138                 :          0 :   std::stringstream ss;
     139                 :          0 :   ss << "The theory " << d_tid
     140                 :            :      << " is disabled in this configuration, but got a constraint in that "
     141                 :          0 :         "theory.";
     142                 :            :   // suggested options only in non-safe builds
     143                 :            : #if !defined(CVC5_SAFE_MODE) && !defined(CVC5_STABLE_MODE)
     144                 :            :   // hardcoded, for better error messages.
     145 [ -  - ][ -  - ]:          0 :   switch (d_tid)
                    [ - ]
     146                 :            :   {
     147                 :          0 :     case THEORY_FF: ss << " Try --ff."; break;
     148                 :          0 :     case THEORY_FP: ss << " Try --fp."; break;
     149                 :          0 :     case THEORY_BAGS: ss << " Try --bags."; break;
     150                 :          0 :     case THEORY_SEP: ss << " Try --sep."; break;
     151                 :          0 :     default: break;
     152                 :            :   }
     153                 :            : #endif
     154                 :          0 :   throw SafeLogicException(ss.str());
     155                 :            :   return RewriteResponse(REWRITE_DONE, node);
     156                 :          0 : }
     157                 :            : 
     158                 :            : }  // namespace theory
     159                 :            : }  // namespace cvc5::internal