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                 :            :  * Print channels for LFSC proofs.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "proof/lfsc/lfsc_print_channel.h"
      14                 :            : 
      15                 :            : #include <sstream>
      16                 :            : 
      17                 :            : #include "proof/lfsc/lfsc_util.h"
      18                 :            : #include "rewriter/rewrite_proof_rule.h"
      19                 :            : 
      20                 :            : using namespace cvc5::internal::rewriter;
      21                 :            : 
      22                 :            : namespace cvc5::internal {
      23                 :            : namespace proof {
      24                 :            : 
      25                 :       1707 : LfscPrintChannelOut::LfscPrintChannelOut(std::ostream& out) : d_out(out) {}
      26                 :    3720470 : void LfscPrintChannelOut::printNode(TNode n)
      27                 :            : {
      28                 :    3720470 :   d_out << " ";
      29                 :    3720470 :   printNodeInternal(d_out, n);
      30                 :    3720470 : }
      31                 :            : 
      32                 :      20633 : void LfscPrintChannelOut::printTypeNode(TypeNode tn)
      33                 :            : {
      34                 :      20633 :   d_out << " ";
      35                 :      20633 :   printTypeNodeInternal(d_out, tn);
      36                 :      20633 : }
      37                 :            : 
      38                 :   20668239 : void LfscPrintChannelOut::printHole() { d_out << " _ "; }
      39                 :     608254 : void LfscPrintChannelOut::printTrust(TNode res, ProofRule src)
      40                 :            : {
      41                 :     608254 :   d_out << std::endl << "(trust ";
      42                 :     608254 :   printNodeInternal(d_out, res);
      43                 :     608254 :   d_out << ") ; from " << src << std::endl;
      44                 :     608254 : }
      45                 :            : 
      46                 :    7810244 : void LfscPrintChannelOut::printOpenRule(const ProofNode* pn)
      47                 :            : {
      48                 :    7810244 :   d_out << std::endl << "(";
      49                 :    7810244 :   printRule(d_out, pn);
      50                 :    7810244 : }
      51                 :            : 
      52                 :    1595276 : void LfscPrintChannelOut::printOpenLfscRule(LfscRule lr)
      53                 :            : {
      54                 :    1595276 :   d_out << std::endl << "(" << lr;
      55                 :    1595276 : }
      56                 :            : 
      57                 :    8628246 : void LfscPrintChannelOut::printCloseRule(size_t nparen)
      58                 :            : {
      59         [ +  + ]:   18033766 :   for (size_t i = 0; i < nparen; i++)
      60                 :            :   {
      61                 :    9405520 :     d_out << ")";
      62                 :            :   }
      63                 :    8628246 : }
      64                 :            : 
      65                 :    3780712 : void LfscPrintChannelOut::printId(size_t id, const std::string& prefix)
      66                 :            : {
      67                 :    3780712 :   d_out << " ";
      68                 :    3780712 :   printId(d_out, id, prefix);
      69                 :    3780712 : }
      70                 :            : 
      71                 :    1619309 : void LfscPrintChannelOut::printEndLine() { d_out << std::endl; }
      72                 :            : 
      73                 :    4791313 : void LfscPrintChannelOut::printNodeInternal(std::ostream& out, Node n)
      74                 :            : {
      75                 :            :   // due to use of special names in the node converter, we must clean symbols
      76                 :    4791313 :   std::stringstream ss;
      77                 :    4791313 :   options::ioutils::applyOutputLanguage(ss, Language::LANG_SMTLIB_V2_6);
      78                 :    4791313 :   n.toStream(ss);
      79                 :    4791313 :   std::string s = ss.str();
      80                 :    4791313 :   cleanSymbols(s);
      81                 :    4791313 :   out << s;
      82                 :    4791313 : }
      83                 :            : 
      84                 :      37824 : void LfscPrintChannelOut::printTypeNodeInternal(std::ostream& out, TypeNode tn)
      85                 :            : {
      86                 :            :   // due to use of special names in the node converter, we must clean symbols
      87                 :      37824 :   std::stringstream ss;
      88                 :      37824 :   options::ioutils::applyOutputLanguage(ss, Language::LANG_SMTLIB_V2_6);
      89                 :      37824 :   tn.toStream(ss);
      90                 :      37824 :   std::string s = ss.str();
      91                 :      37824 :   cleanSymbols(s);
      92                 :      37824 :   out << s;
      93                 :      37824 : }
      94                 :            : 
      95                 :    7810244 : void LfscPrintChannelOut::printRule(std::ostream& out, const ProofNode* pn)
      96                 :            : {
      97         [ +  + ]:    7810244 :   if (pn->getRule() == ProofRule::LFSC_RULE)
      98                 :            :   {
      99                 :    4203424 :     const std::vector<Node>& args = pn->getArguments();
     100                 :    4203424 :     out << getLfscRule(args[0]);
     101                 :    4203428 :     return;
     102                 :            :   }
     103         [ +  + ]:    3606820 :   else if (pn->getRule() == ProofRule::DSL_REWRITE)
     104                 :            :   {
     105                 :          4 :     const std::vector<Node>& args = pn->getArguments();
     106                 :            :     ProofRewriteRule di;
     107         [ +  - ]:          4 :     if (rewriter::getRewriteRule(args[0], di))
     108                 :            :     {
     109                 :          4 :       printProofRewriteRule(out, di);
     110                 :            :     }
     111                 :            :     else
     112                 :            :     {
     113                 :          0 :       Unreachable();
     114                 :            :     }
     115                 :          4 :     return;
     116                 :            :   }
     117                 :            :   // Otherwise, convert to lower case
     118                 :    3606816 :   std::stringstream ss;
     119                 :    3606816 :   ss << pn->getRule();
     120                 :    3606816 :   std::string rname = ss.str();
     121                 :    3606816 :   std::transform(
     122                 :   21343533 :       rname.begin(), rname.end(), rname.begin(), [](unsigned char c) {
     123                 :   21343533 :         return std::tolower(c);
     124                 :            :       });
     125                 :    3606816 :   out << rname;
     126                 :    3606816 : }
     127                 :            : 
     128                 :    4658825 : void LfscPrintChannelOut::printId(std::ostream& out,
     129                 :            :                                   size_t id,
     130                 :            :                                   const std::string& prefix)
     131                 :            : {
     132                 :    4658825 :   out << prefix << id;
     133                 :    4658825 : }
     134                 :            : 
     135                 :          6 : void LfscPrintChannelOut::printProofRewriteRule(std::ostream& out,
     136                 :            :                                                 ProofRewriteRule id)
     137                 :            : {
     138                 :          6 :   out << "dsl." << id;
     139                 :          6 : }
     140                 :            : 
     141                 :    4829137 : void LfscPrintChannelOut::cleanSymbols(std::string& s)
     142                 :            : {
     143                 :    4829137 :   size_t start_pos = 0;
     144         [ +  + ]:    4830645 :   while ((start_pos = s.find("(_ ", start_pos)) != std::string::npos)
     145                 :            :   {
     146                 :       1508 :     s.replace(start_pos, 3, "(");
     147                 :       1508 :     start_pos += 1;
     148                 :            :   }
     149                 :    4829137 :   start_pos = 0;
     150         [ +  + ]:    4833695 :   while ((start_pos = s.find("__LFSC_TMP", start_pos)) != std::string::npos)
     151                 :            :   {
     152                 :       4558 :     s.replace(start_pos, 10, "");
     153                 :            :   }
     154                 :    4829137 : }
     155                 :            : 
     156                 :       1707 : LfscPrintChannelPre::LfscPrintChannelPre(LetBinding& lbind) : d_lbind(lbind) {}
     157                 :            : 
     158                 :    3720470 : void LfscPrintChannelPre::printNode(TNode n) { d_lbind.process(n); }
     159                 :     608254 : void LfscPrintChannelPre::printTrust(TNode res, CVC5_UNUSED ProofRule src)
     160                 :            : {
     161                 :     608254 :   d_lbind.process(res);
     162                 :     608254 : }
     163                 :            : 
     164                 :    7810244 : void LfscPrintChannelPre::printOpenRule(const ProofNode* pn)
     165                 :            : {
     166                 :            :   // if its a DSL rule, remember it
     167         [ +  + ]:    7810244 :   if (pn->getRule() == ProofRule::DSL_REWRITE)
     168                 :            :   {
     169                 :          4 :     Node idn = pn->getArguments()[0];
     170                 :            :     ProofRewriteRule di;
     171         [ +  - ]:          4 :     if (rewriter::getRewriteRule(idn, di))
     172                 :            :     {
     173                 :          4 :       d_dprs.insert(di);
     174                 :            :     }
     175                 :            :     else
     176                 :            :     {
     177                 :          0 :       Unhandled();
     178                 :            :     }
     179                 :          4 :   }
     180                 :    7810244 : }
     181                 :            : 
     182                 :            : const std::unordered_set<ProofRewriteRule>&
     183                 :       1707 : LfscPrintChannelPre::getDslRewrites() const
     184                 :            : {
     185                 :       1707 :   return d_dprs;
     186                 :            : }
     187                 :            : 
     188                 :            : }  // namespace proof
     189                 :            : }  // namespace cvc5::internal