Branch data     Line data    Source code

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