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.h | |
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.h')
-rw-r--r-- | src/printer/sygus_print_callback.h | 129 |
1 files changed, 129 insertions, 0 deletions
diff --git a/src/printer/sygus_print_callback.h b/src/printer/sygus_print_callback.h new file mode 100644 index 000000000..cdeec32f0 --- /dev/null +++ b/src/printer/sygus_print_callback.h @@ -0,0 +1,129 @@ +/********************* */ +/*! \file sygus_print_callback.h + ** \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 sygus print callback functions + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H +#define __CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H + +#include <vector> + +#include "expr/node.h" + +namespace CVC4 { +namespace printer { + +/** sygus let expression constructor printer + * + * This class is used for printing sygus + * datatype constructor terms whose top symbol + * is a let expression. + * For example, for grammar: + * A -> (let ((x B)) (+ A 1)) | x | (+ A A) | 0 + * B -> 0 | 1 + * the first constructor for A takes as arguments + * (B,A) and has operator + * (lambda ((y B) (z A)) (+ z 1)) + * CVC4's support for let expressions in grammars + * is highly limited, since notice that the + * argument y : B is unused. + * + * For the above constructor, we have that + * d_let_body is (+ z 1), + * d_sygus_let_args is { y, z }, + * d_sygus_num_let_input_args is 1, since + * y is an original input argument of the + * let expression, but z is not. + */ +class SygusLetExpressionConstructorPrinter + : public SygusDatatypeConstructorPrinter +{ + public: + SygusLetExpressionPrinter(Node let_body, + std::vector<Node>& let_args, + unsigned ninput_args); + ~SygusLetExpressionPrinter() {} + /** print sygus term e on output out using printer p */ + virtual void toStreamSygus(const Printer* p, + std::ostream& out, + Expr e) const override; + + private: + /** let body of the sygus term */ + Node d_sygus_let_body; + /** let arguments */ + std::vector<Node> d_sygus_let_args; + /** number of arguments that are interpreted as input arguments */ + unsigned d_sygus_num_let_input_args; + /** do string replace + * Replaces all occurrences of oldStr with newStr in str. + */ + void doStrReplace(std::string& str, + const std::string& oldStr, + const std::string& newStr) const; +}; + +/** sygus named constructor printer + * + * This callback is used for explicitly naming + * the builtin term that a sygus datatype constructor + * should be printed as. This is used for printing + * terms in sygus grammars that involve defined + * functions. For example, for grammar : + * A -> f( A ) | 0 + * where f is defined as: + * (define-fun ((x Int)) Int (+ x 1)) + * this class can be used as a callback for printing + * the first sygus datatype constructor f, where we use + * analog operator (lambda (x) (+ x 1)). + */ +class SygusNamedConstructorPrinter : public SygusDatatypeConstructorPrinter +{ + public: + SygusNamedConstructorPrinter(std::string name); + ~SygusNamedConstructorPrinter() {} + /** print sygus term e on output out using printer p */ + virtual void toStreamSygus(const Printer* p, + std::ostream& out, + Expr e) const override; + + private: + /** the defined function name */ + std::string d_name; +}; + +/** sygus empty printer + * + * This callback is used for printing constructors whose operators are + * implicit, such as identity functions. For example, for grammar : + * A -> B + * B -> x | 0 | 1 + * The first constructor of A, call it cons, has sygus operator (lambda (x) x). + * Call toStreamSygus on cons( t ) should call toStreamSygus on t directly. + */ +class SygusEmptyConstructorPrinter : public SygusDatatypeConstructorPrinter +{ + public: + SygusEmptyConstructorPrinter(std::string name); + ~SygusEmptyConstructorPrinter() {} + /** print sygus term e on output out using printer p */ + virtual void toStreamSygus(const Printer* p, + std::ostream& out, + Expr e) const override; +}; + +} /* CVC4::printer namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H */ |