diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-15 16:48:26 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-15 16:48:26 -0600 |
commit | 9bff14c12c34fea0e6ba0649a3e8f7e8f48b5646 (patch) | |
tree | ea7c7ccd91be5ea728e798d8ec8df4b2fec78820 /src/printer/sygus_print_callback.cpp | |
parent | 39ec2fb797623bd1556f81b963ace1997c74e920 (diff) |
Sygus print callbacks (#1348)
* Initial infrastructure for sygus printing.
* Minor
* Minor improvements
* Format
* Minor
* Empty constructor printer.
* Format
* Minor
* Format
* Address.
Diffstat (limited to 'src/printer/sygus_print_callback.cpp')
-rw-r--r-- | src/printer/sygus_print_callback.cpp | 144 |
1 files changed, 144 insertions, 0 deletions
diff --git a/src/printer/sygus_print_callback.cpp b/src/printer/sygus_print_callback.cpp new file mode 100644 index 000000000..c956c32de --- /dev/null +++ b/src/printer/sygus_print_callback.cpp @@ -0,0 +1,144 @@ +/********************* */ +/*! \file sygus_print_callback.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of sygus print callbacks + **/ + +#include "printer/sygus_print_callback.h" + +using namespace CVC4::kind; +using namespace std; + +namespace CVC4 { +namespace printer { + +SygusLetExpressionPrinter::SygusLetExpressionPrinter( + Node let_body, std::vector<Node>& let_args, unsigned ninput_args) +{ +} + +void SygusLetExpressionConstructorPrinter::doStrReplace( + std::string& str, const std::string& oldStr, const std::string& newStr) +{ + size_t pos = 0; + while ((pos = str.find(oldStr, pos)) != std::string::npos) + { + str.replace(pos, oldStr.length(), newStr); + pos += newStr.length(); + } +} + +void SygusLetExpressionConstructorPrinter::toStreamSygus(Printer* p, + std::ostream& out, + Expr e) +{ + std::stringstream let_out; + // print as let term + if (d_sygus_num_let_input_args > 0) + { + let_out << "(let ("; + } + std::vector<Node> subs_lvs; + std::vector<Node> new_lvs; + for (unsigned i = 0; i < d_sygus_let_args.size(); i++) + { + Node v = d_sygus_let_args[i]; + subs_lvs.push_back(v); + std::stringstream ss; + ss << "_l_" << new_lvs.size(); + Node lv = NodeManager::currentNM()->mkBoundVar(ss.str(), v.getType()); + new_lvs.push_back(lv); + // map free variables to proper terms + if (i < d_sygus_num_let_input_args) + { + // it should be printed as a let argument + let_out << "("; + let_out << lv << " " << lv.getType() << " "; + p->toStreamSygus(let_out, e[i]); + let_out << ")"; + } + } + if (d_sygus_num_let_input_args > 0) + { + let_out << ") "; + } + // print the body + Node slet_body = d_let_body.substitute( + subs_lvs.begin(), subs_lvs.end(), new_lvs.begin(), new_lvs.end()); + new_lvs.insert(new_lvs.end(), lvs.begin(), lvs.end()); + p->toStreamSygus(let_out, slet_body); + if (d_sygus_num_let_input_args > 0) + { + let_out << ")"; + } + // do variable substitutions since + // ASSUMING : let_vars are interpreted literally and do not represent a class + // of variables + std::string lbody = let_out.str(); + for (unsigned i = 0; i < d_sygus_let_args.size(); i++) + { + std::stringstream old_str; + old_str << new_lvs[i]; + std::stringstream new_str; + if (i >= d_sygus_num_let_input_args) + { + p->toStreamSygus(new_str, Node::fromExpr(e[i])); + } + else + { + new_str << d_sygus_let_args[i]; + } + doStrReplace(lbody, old_str.str().c_str(), new_str.str().c_str()); + } + out << lbody; +} + +SygusNamedConstructorPrinter::SygusNamedConstructorPrinter(std::string name) + : d_name(name) +{ +} + +void SygusNamedConstructorPrinter::toStreamSygus(Printer* p, + std::ostream& out, + Expr e) +{ + if (e.getNumChildren() > 0) + { + out << "("; + } + out << d_name; + if (e.getNumChildren() > 0) + { + for (Expr ec : e) + { + out << " "; + p->toStreamSygus(out, ec); + } + out << ")"; + } +} + +void SygusEmptyConstructorPrinter::toStreamSygus(const Printer* p, + std::ostream& out, + Expr e) +{ + if (e.getNumChildren() == 1) + { + p->toStreamSygus(out, e[0]); + } + else + { + Assert(false); + } +} + +} /* CVC4::printer namespace */ +} /* CVC4 namespace */ |