Branch data     Line data    Source code

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