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
|
#include "print_smt2.h"
#ifdef PRINT_SMT2
void print_smt2( Expr* p, std::ostream& s, short mode )
{
switch( p->getclass() )
{
case CEXPR:
{
switch( p->getop() )
{
case APP:
{
std::vector<Expr *> args;
Expr *head = p->collect_args(args, false);
short newMode = get_mode( head );
if( is_smt2_poly_formula( head ) )
{
s << "(";
head->print( s );
s << " ";
print_smt2( args[1], s, newMode );
s << " ";
print_smt2( args[2], s, newMode );
s << ")";
}
else if( ( mode==2 || mode==3 ) && mode==newMode )
{
print_smt2( args[0], s, newMode );
s << " ";
print_smt2( args[1], s, newMode );
}
else if( newMode==1 )
{
if( mode!=1 || newMode!=mode ){
s << "(";
}
print_smt2( args[2], s, newMode );
s << " ";
print_smt2( args[3], s, 0 );
if( mode!=1 || newMode!=mode ){
s << ")";
}
}
else
{
s << "(";
switch( newMode )
{
case 4: s << "=>";break;
default: head->print( s );break;
}
s << " ";
for( int a=0; a<(int)args.size(); a++ ){
print_smt2( args[a], s, newMode );
if( a!=args.size()-1 )
s << " ";
}
s << ")";
}
}
break;
default:
std::cout << "Unhandled op " << p->getop() << std::endl;
break;
}
}
break;
case HOLE_EXPR:
{
HoleExpr *e = (HoleExpr *)p;
if( e->val ){
print_smt2( e->val, s, mode );
}else{
s << "_";
}
}
break;
case SYMS_EXPR:
case SYM_EXPR:
if( ((SymExpr*)p)->val )
print_smt2( ((SymExpr*)p)->val, s, mode );
else
p->print( s );
break;
default:
std::cout << "Unhandled class " << p->getclass() << std::endl;
break;
}
}
bool is_smt2_poly_formula( Expr* e )
{
if( e->getclass()==SYMS_EXPR )
{
SymSExpr* s = (SymSExpr*)e;
static std::string eq("=");
static std::string distinct("distinct");
return s->s==eq || s->s==distinct;
}else{
return false;
}
}
short get_mode( Expr* e )
{
if( e->getclass()==SYMS_EXPR ){
SymSExpr* s = (SymSExpr*)e;
static std::string applys("apply");
if ( s->s==applys ) return 1;
static std::string ands("and");
if ( s->s==ands ) return 2;
static std::string ors("or");
if ( s->s==ors ) return 3;
static std::string impls("impl");
if ( s->s==impls ) return 4;
}
return 0;
}
#endif
|
