src/printer/sygus_print_callback.cpp

   1 /*********************                                                        */
   2 /*! \file sygus_print_callback.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Haniel Barbosa
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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.\endverbatim
  11  **
  12  ** \brief Implementation of sygus print callbacks
  13  **/
  14
  15 #include "printer/sygus_print_callback.h"
  16
  17 #include "expr/node.h"
  18 #include "printer/printer.h"
  19
  20 using namespace CVC4::kind;
  21 using namespace std;
  22
  23 namespace CVC4 {
  24 namespace printer {
  25
  26 SygusExprPrintCallback::SygusExprPrintCallback(Expr body,
  27                                                const std::vector<Expr>& args)
  28     : d_body(body), d_body_argument(-1)
  29 {
  30   d_args.insert(d_args.end(), args.begin(), args.end());
  31   for (unsigned i = 0, size = d_args.size(); i < size; i++)
  32   {
  33     if (d_args[i] == d_body)
  34     {
  35       d_body_argument = static_cast<int>(i);
  36     }
  37   }
  38 }
  39
  40 void SygusExprPrintCallback::doStrReplace(std::string& str,
  41                                           const std::string& oldStr,
  42                                           const std::string& newStr) const
  43 {
  44   size_t pos = 0;
  45   while ((pos = str.find(oldStr, pos)) != std::string::npos)
  46   {
  47     str.replace(pos, oldStr.length(), newStr);
  48     pos += newStr.length();
  49   }
  50 }
  51
  52 void SygusExprPrintCallback::toStreamSygus(const Printer* p,
  53                                            std::ostream& out,
  54                                            Expr e) const
  55 {
  56   // optimization: if body is equal to an argument, then just print that one
  57   if (d_body_argument >= 0)
  58   {
  59     p->toStreamSygus(out, Node::fromExpr(e[d_body_argument]));
  60   }
  61   else
  62   {
  63     // make substitution
  64     std::vector<Node> vars;
  65     std::vector<Node> subs;
  66     for (unsigned i = 0, size = d_args.size(); i < size; i++)
  67     {
  68       vars.push_back(Node::fromExpr(d_args[i]));
  69       std::stringstream ss;
  70       ss << "_setpc_var_" << i;
  71       Node lv = NodeManager::currentNM()->mkBoundVar(
  72           ss.str(), TypeNode::fromType(d_args[i].getType()));
  73       subs.push_back(lv);
  74     }
  75
  76     // the substituted body should be a non-sygus term
  77     Node sbody = Node::fromExpr(d_body);
  78     sbody =
  79         sbody.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
  80
  81     // print to stream without letification
  82     std::stringstream body_out;
  83     p->toStream(body_out, sbody, -1, false, 0);
  84
  85     // do string substitution
  86     Assert(e.getNumChildren() == d_args.size());
  87     std::string str_body = body_out.str();
  88     for (unsigned i = 0, size = d_args.size(); i < size; i++)
  89     {
  90       std::stringstream old_str;
  91       old_str << subs[i];
  92       std::stringstream new_str;
  93       p->toStreamSygus(new_str, Node::fromExpr(e[i]));
  94       doStrReplace(str_body, old_str.str().c_str(), new_str.str().c_str());
  95     }
  96     out << str_body;
  97   }
  98 }
  99
 100 SygusNamedPrintCallback::SygusNamedPrintCallback(std::string name)
 101     : d_name(name)
 102 {
 103 }
 104
 105 void SygusNamedPrintCallback::toStreamSygus(const Printer* p,
 106                                             std::ostream& out,
 107                                             Expr e) const
 108 {
 109   if (e.getNumChildren() > 0)
 110   {
 111     out << "(";
 112   }
 113   out << d_name;
 114   if (e.getNumChildren() > 0)
 115   {
 116     for (Expr ec : e)
 117     {
 118       out << " ";
 119       p->toStreamSygus(out, ec);
 120     }
 121     out << ")";
 122   }
 123 }
 124
 125 void SygusEmptyPrintCallback::toStreamSygus(const Printer* p,
 126                                             std::ostream& out,
 127                                             Expr e) const
 128 {
 129   if (e.getNumChildren() == 1)
 130   {
 131     p->toStreamSygus(out, e[0]);
 132   }
 133   else
 134   {
 135     Assert(false);
 136   }
 137 }
 138
 139 std::shared_ptr<SygusEmptyPrintCallback> SygusEmptyPrintCallback::d_empty_pc = nullptr;
 140
 141 } /* CVC4::printer namespace */
 142 } /* CVC4 namespace */