1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
|
/********************* */
/*! \file sygus_print_callback.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Haniel Barbosa, Mathias Preiner
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 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_public.h"
#ifndef CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H
#define CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H
#include <vector>
#include "expr/datatype.h"
#include "expr/expr.h"
namespace CVC4 {
namespace printer {
/** sygus expression constructor printer
*
* This class is used for printing sygus datatype constructor terms whose top
* symbol is an expression, such as a custom defined lambda. For example, for
* sygus grammar:
* A -> (+ x A B) | x | y
* B -> 0 | 1
* The first constructor, call it C_f for A takes two arguments (A, B) and has
* sygus operator
* (lambda ((z Int) (w Int)) (+ x z w))
* For this operator, we set a print callback that prints, e.g. the term
* C_f( t1, t2 )
* is printed as:
* "(+ x [out1] [out2])"
* where out1 is the result of p->toStreamSygus(out,t1) and
* out2 is the result of p->toStreamSygus(out,t2).
*/
class CVC4_PUBLIC SygusExprPrintCallback : public SygusPrintCallback
{
public:
SygusExprPrintCallback(Expr body, const std::vector<Expr>& args);
~SygusExprPrintCallback() {}
/** print sygus term e on output out using printer p */
virtual void toStreamSygus(const Printer* p,
std::ostream& out,
Expr e) const override;
protected:
/** body of the sygus term */
Expr d_body;
/** arguments */
std::vector<Expr> d_args;
/** body argument */
int d_body_argument;
/** 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 CVC4_PUBLIC SygusNamedPrintCallback : public SygusPrintCallback
{
public:
SygusNamedPrintCallback(std::string name);
~SygusNamedPrintCallback() {}
/** 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 CVC4_PUBLIC SygusEmptyPrintCallback : public SygusPrintCallback
{
public:
SygusEmptyPrintCallback() {}
~SygusEmptyPrintCallback() {}
/** print sygus term e on output out using printer p */
virtual void toStreamSygus(const Printer* p,
std::ostream& out,
Expr e) const override;
/* Retrieves empty callback pointer */
static inline std::shared_ptr<SygusEmptyPrintCallback> getEmptyPC()
{
if (!d_empty_pc)
{
d_empty_pc = std::make_shared<SygusEmptyPrintCallback>();
}
return d_empty_pc;
}
private:
/* empty callback object */
static std::shared_ptr<SygusEmptyPrintCallback> d_empty_pc;
};
} /* CVC4::printer namespace */
} /* CVC4 namespace */
#endif /* CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H */
|
