-
Notifications
You must be signed in to change notification settings - Fork 1
/
smtlib.py
106 lines (88 loc) · 4.34 KB
/
smtlib.py
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
#!/usr/bin/env python3
##############################################################################
## ##
## FP_TEST_GENERATOR ##
## ##
## Copyright (C) 2020, Florian Schanda ##
## ##
## This file is part of FP_Test_Generator. ##
## ##
## FP_Test_Generator is free software: you can redistribute it and/or ##
## modify it under the terms of the GNU General Public License as ##
## published by the Free Software Foundation, either version 3 of the ##
## License, or (at your option) any later version. ##
## ##
## FP_Test_Generator is distributed in the hope that it will be useful, ##
## but WITHOUT ANY WARRANTY; without even the implied warranty of ##
## MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the ##
## GNU General Public License for more details. ##
## ##
## You should have received a copy of the GNU General Public License ##
## along with FP_Test_Generator. If not, see ##
## <http://www.gnu.org/licenses/>. ##
## ##
##############################################################################
def write_header(fd, seed, validators):
fd.write(";; Random floating-point test generated by fp_test_generator\n")
fd.write(";;\n")
fd.write(";; Seed information:\n")
for key in sorted(seed.keys):
fd.write(";; %s = %s\n" % (key, seed.keys[key]))
fd.write(";;\n")
fd.write(";; Test oracle(s) for this test:\n")
for oracle in sorted(validators):
fd.write(";; * %s\n" % oracle)
fd.write("\n")
set_info(fd, "smt-lib-version", "2.6")
set_info(fd, "license", "https://www.gnu.org/licenses/gpl-3.0.html")
set_info(fd, "category", "random")
set_info(fd,
"source",
"https://github.com/florianschanda/fp_test_generator")
def write_footer(fd):
fd.write("\n")
fd.write("(check-sat)\n")
fd.write("(exit)\n")
def set_info(fd, key, value):
if ":" in value:
fd.write("(set-info :%s |%s|)\n" % (key, value))
else:
fd.write("(set-info :%s %s)\n" % (key, value))
def set_logic(fd, logic):
fd.write("(set-logic %s)\n" % logic)
def set_status(fd, status):
assert status in ("sat", "unsat")
set_info(fd, "status", status)
def define_fp_const(fd, name, value):
fd.write("\n")
fd.write("(define-const %s %s %s)\n" % (name,
value.smtlib_sort(),
value.smtlib_literal()))
if value.isFinite():
str_val = value.to_python_string()
if len(str_val) < 20:
fd.write(";; should be %s\n" % str_val)
fd.write(";; isZero : %s\n" % value.isZero())
fd.write(";; isSubnormal : %s\n" % value.isSubnormal())
fd.write(";; isNormal : %s\n" % value.isNormal())
fd.write(";; isInfinite : %s\n" % value.isInfinite())
fd.write(";; isNan : %s\n" % value.isNaN())
fd.write(";; isNegative : %s\n" % value.isNegative())
fd.write(";; isPositive : %s\n" % value.isPositive())
fd.write(";; isFinite : %s\n" % value.isFinite())
fd.write(";; isIntegral : %s\n" % value.isIntegral())
def define_const(fd, name, sort, value):
fd.write("\n")
fd.write("(define-const %s %s %s)\n" % (name,
sort,
value))
def goal_eq(fd, a, b, expecting_unsat):
fd.write("\n")
if expecting_unsat:
fd.write(";; goal\n")
fd.write("(assert (not (= %s %s)))\n" % (a, b))
else:
fd.write(";; goal\n")
fd.write("(assert (= %s %s))\n" % (a, b))
def comment(fd, c):
fd.write(";; %s\n" % c)