Skip to content

Commit 0032260

Browse files
ChronosymbolicChronosymbolic
committed
add missing files
1 parent 429dd62 commit 0032260

8 files changed

Lines changed: 230 additions & 2 deletions

File tree

‎.gitignore‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,6 @@ lib64/
3838
parts/
3939
sdist/
4040
var/
41-
tests/
4241
wheels/
4342
pip-wheel-metadata/
4443
share/python-wheels/

‎README.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ Python (3.7.0 or higher recommended, and [Anaconda](https://www.anaconda.com/) r
4444

4545
- Adjust timeout using `-t TIMEOUT`, only effective in directory mode
4646

47-
- Specify the result summary log file using `-o FILE_NAME`; Export an additional result summary CSV `FILE_NAME_prefix.csv` (with success and timing statistics, and `is_correct` column shows the satisfiability of the CHC system if solved) using `-a`; The summary is only available when running multiple instances (directory mode or file list mode)
47+
- Specify the result summary log file using `-o FILE_NAME`; Export an additional result summary CSV `FILE_NAME_prefix.csv` (with success and timing statistics, and `is_correct` column shows the satisfiability of the CHC system *if successfully solved* (`is_successful=1`)) using `-a`; The summary is only available when running multiple instances (directory mode or file list mode)
4848

4949
- Start solving from the file index `K` in the folder `-s K` (`K` is the index starting from zero)
5050

‎requirements.txt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ ordered-set
66
colorlog
77
eventlet
88
scikit-learn
9+
pandas

‎tests/README.md‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
# Test Suites
2+
## safe
3+
Safe instances
4+
5+
## unsafe
6+
Unsafe instances
7+
8+
## multiple_pred
9+
Instances with multiple predicates
10+
11+
## simple_smt
12+
Simple instances just for testing functionality (In examples, `dt_visualizer.ipynb` visualizes the instance `10000.smt2`)

‎tests/simple_smt/10000.smt2‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
(set-logic HORN)
2+
(declare-rel itp (Int Int Int))
3+
(declare-rel simple!!query ())
4+
(declare-var A Int)
5+
(declare-var B Int)
6+
(declare-var C Int)
7+
(declare-var D Int)
8+
(declare-var E Int)
9+
(declare-var F Int)
10+
(rule (=> (and (= A 0) (= B 0) (= C 0)) (itp A B C)))
11+
(rule (=> (and (itp A B C) (= D (+ A 1)) (= E (+ B 1)) (= F (+ C 1))) (itp D E F)))
12+
(rule (=> (and (itp A B C) (>= A 10000) (not (= B C))) simple!!query))
13+
(query simple!!query)

‎tests/simple_smt/1000_loop.smt2‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
(set-logic HORN)
2+
(declare-rel itp (Int))
3+
(declare-rel simple!!query ())
4+
(declare-var A Int)
5+
(declare-var B Int)
6+
(declare-var C Int)
7+
(rule (=> (= A 0) (itp A)))
8+
(rule (=> (and (itp A) (< A C) (= B (+ A 1))) (itp B)))
9+
(rule (=> (and (itp A) (>= A C) (<= A 1000)) simple!!query))
10+
(query simple!!query)

‎tests/simple_smt/1000_seahorn.smt2‎

Lines changed: 179 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,179 @@
1+
(set-info :original "/tmp/sea-nsu6mg/100.pp.ms.o.bc")
2+
(set-info :authors "SeaHorn v.0.1.0-rc3")
3+
(declare-rel verifier.error (Bool Bool Bool ))
4+
(declare-rel main@entry (Int ))
5+
(declare-rel main@.lr.ph (Int Int Int Int ))
6+
(declare-rel main@verifier.error.split ())
7+
(declare-var main@%_9_0 Bool )
8+
(declare-var main@%or.cond.i_0 Bool )
9+
(declare-var main@%_10_0 Bool )
10+
(declare-var main@%_11_0 Bool )
11+
(declare-var main@%_6_0 Int )
12+
(declare-var main@%_7_0 Int )
13+
(declare-var main@%_8_0 Bool )
14+
(declare-var main@%.lcssa11_1 Int )
15+
(declare-var main@%.lcssa10_1 Int )
16+
(declare-var main@%.lcssa_1 Int )
17+
(declare-var main@%c.0.i3_2 Int )
18+
(declare-var main@%a.0.i2_2 Int )
19+
(declare-var main@%b.0.i1_2 Int )
20+
(declare-var main@%_0_0 Int )
21+
(declare-var main@%_1_0 Int )
22+
(declare-var main@%_2_0 Bool )
23+
(declare-var @unknown_0 Int )
24+
(declare-var main@entry_0 Bool )
25+
(declare-var main@.lr.ph.preheader_0 Bool )
26+
(declare-var main@.lr.ph_0 Bool )
27+
(declare-var main@%c.0.i3_0 Int )
28+
(declare-var main@%a.0.i2_0 Int )
29+
(declare-var main@%b.0.i1_0 Int )
30+
(declare-var main@%c.0.i3_1 Int )
31+
(declare-var main@%a.0.i2_1 Int )
32+
(declare-var main@%b.0.i1_1 Int )
33+
(declare-var main@verifier.error_0 Bool )
34+
(declare-var main@%c.0.i.lcssa_0 Int )
35+
(declare-var main@%a.0.i.lcssa_0 Bool )
36+
(declare-var main@%b.0.i.lcssa_0 Int )
37+
(declare-var main@%c.0.i.lcssa_1 Int )
38+
(declare-var main@%a.0.i.lcssa_1 Bool )
39+
(declare-var main@%b.0.i.lcssa_1 Int )
40+
(declare-var main@verifier.error.split_0 Bool )
41+
(declare-var main@%_3_0 Int )
42+
(declare-var main@%_4_0 Int )
43+
(declare-var main@%_5_0 Int )
44+
(declare-var main@.lr.ph_1 Bool )
45+
(declare-var main@.verifier.error_crit_edge_0 Bool )
46+
(declare-var main@%.lcssa11_0 Int )
47+
(declare-var main@%.lcssa10_0 Int )
48+
(declare-var main@%.lcssa_0 Int )
49+
(declare-var main@%phitmp_0 Bool )
50+
(rule (verifier.error false false false))
51+
(rule (verifier.error false true true))
52+
(rule (verifier.error true false true))
53+
(rule (verifier.error true true true))
54+
(rule (main@entry @unknown_0))
55+
(rule (=> (and (main@entry @unknown_0)
56+
true
57+
(= main@%_0_0 @unknown_0)
58+
(= main@%_2_0 (= main@%_1_0 0))
59+
(=> main@.lr.ph.preheader_0 (and main@.lr.ph.preheader_0 main@entry_0))
60+
(=> (and main@.lr.ph.preheader_0 main@entry_0) (not main@%_2_0))
61+
(=> main@.lr.ph_0 (and main@.lr.ph_0 main@.lr.ph.preheader_0))
62+
main@.lr.ph_0
63+
(=> (and main@.lr.ph_0 main@.lr.ph.preheader_0) (= main@%c.0.i3_0 0))
64+
(=> (and main@.lr.ph_0 main@.lr.ph.preheader_0) (= main@%a.0.i2_0 0))
65+
(=> (and main@.lr.ph_0 main@.lr.ph.preheader_0) (= main@%b.0.i1_0 0))
66+
(=> (and main@.lr.ph_0 main@.lr.ph.preheader_0)
67+
(= main@%c.0.i3_1 main@%c.0.i3_0))
68+
(=> (and main@.lr.ph_0 main@.lr.ph.preheader_0)
69+
(= main@%a.0.i2_1 main@%a.0.i2_0))
70+
(=> (and main@.lr.ph_0 main@.lr.ph.preheader_0)
71+
(= main@%b.0.i1_1 main@%b.0.i1_0)))
72+
(main@.lr.ph main@%a.0.i2_1 main@%b.0.i1_1 main@%c.0.i3_1 @unknown_0)))
73+
(rule (let ((a!1 (and (main@entry @unknown_0)
74+
true
75+
(= main@%_0_0 @unknown_0)
76+
(= main@%_2_0 (= main@%_1_0 0))
77+
(=> main@verifier.error_0
78+
(and main@verifier.error_0 main@entry_0))
79+
(=> (and main@verifier.error_0 main@entry_0) main@%_2_0)
80+
(=> (and main@verifier.error_0 main@entry_0)
81+
(= main@%c.0.i.lcssa_0 0))
82+
(=> (and main@verifier.error_0 main@entry_0)
83+
(= main@%a.0.i.lcssa_0 true))
84+
(=> (and main@verifier.error_0 main@entry_0)
85+
(= main@%b.0.i.lcssa_0 0))
86+
(=> (and main@verifier.error_0 main@entry_0)
87+
(= main@%c.0.i.lcssa_1 main@%c.0.i.lcssa_0))
88+
(=> (and main@verifier.error_0 main@entry_0)
89+
(= main@%a.0.i.lcssa_1 main@%a.0.i.lcssa_0))
90+
(=> (and main@verifier.error_0 main@entry_0)
91+
(= main@%b.0.i.lcssa_1 main@%b.0.i.lcssa_0))
92+
(=> main@verifier.error_0
93+
(= main@%_9_0 (= main@%b.0.i.lcssa_1 main@%c.0.i.lcssa_1)))
94+
(=> main@verifier.error_0
95+
(= main@%or.cond.i_0 (or main@%a.0.i.lcssa_1 main@%_9_0)))
96+
(=> main@verifier.error_0 (not main@%or.cond.i_0))
97+
(=> main@verifier.error_0
98+
(= main@%_10_0 (xor main@%a.0.i.lcssa_1 true)))
99+
(=> main@verifier.error_0 (= main@%_11_0 (xor main@%_9_0 true)))
100+
(=> main@verifier.error.split_0
101+
(and main@verifier.error.split_0 main@verifier.error_0))
102+
main@verifier.error.split_0)))
103+
(=> a!1 main@verifier.error.split)))
104+
(rule (=> (and (main@.lr.ph main@%a.0.i2_0 main@%b.0.i1_0 main@%c.0.i3_0 @unknown_0)
105+
true
106+
(= main@%_3_0 (+ main@%a.0.i2_0 1))
107+
(= main@%_4_0 (+ main@%b.0.i1_0 1))
108+
(= main@%_5_0 (+ main@%c.0.i3_0 1))
109+
(= main@%_6_0 @unknown_0)
110+
(= main@%_8_0 (= main@%_7_0 0))
111+
(=> main@.lr.ph_1 (and main@.lr.ph_1 main@.lr.ph_0))
112+
main@.lr.ph_1
113+
(=> (and main@.lr.ph_1 main@.lr.ph_0) (not main@%_8_0))
114+
(=> (and main@.lr.ph_1 main@.lr.ph_0) (= main@%c.0.i3_1 main@%_5_0))
115+
(=> (and main@.lr.ph_1 main@.lr.ph_0) (= main@%a.0.i2_1 main@%_3_0))
116+
(=> (and main@.lr.ph_1 main@.lr.ph_0) (= main@%b.0.i1_1 main@%_4_0))
117+
(=> (and main@.lr.ph_1 main@.lr.ph_0)
118+
(= main@%c.0.i3_2 main@%c.0.i3_1))
119+
(=> (and main@.lr.ph_1 main@.lr.ph_0)
120+
(= main@%a.0.i2_2 main@%a.0.i2_1))
121+
(=> (and main@.lr.ph_1 main@.lr.ph_0)
122+
(= main@%b.0.i1_2 main@%b.0.i1_1)))
123+
(main@.lr.ph main@%a.0.i2_2 main@%b.0.i1_2 main@%c.0.i3_2 @unknown_0)))
124+
(rule (let ((a!1 (and (main@.lr.ph main@%a.0.i2_0
125+
main@%b.0.i1_0
126+
main@%c.0.i3_0
127+
@unknown_0)
128+
true
129+
(= main@%_3_0 (+ main@%a.0.i2_0 1))
130+
(= main@%_4_0 (+ main@%b.0.i1_0 1))
131+
(= main@%_5_0 (+ main@%c.0.i3_0 1))
132+
(= main@%_6_0 @unknown_0)
133+
(= main@%_8_0 (= main@%_7_0 0))
134+
(=> main@.verifier.error_crit_edge_0
135+
(and main@.verifier.error_crit_edge_0 main@.lr.ph_0))
136+
(=> (and main@.verifier.error_crit_edge_0 main@.lr.ph_0)
137+
main@%_8_0)
138+
(=> (and main@.verifier.error_crit_edge_0 main@.lr.ph_0)
139+
(= main@%.lcssa11_0 main@%_5_0))
140+
(=> (and main@.verifier.error_crit_edge_0 main@.lr.ph_0)
141+
(= main@%.lcssa10_0 main@%_4_0))
142+
(=> (and main@.verifier.error_crit_edge_0 main@.lr.ph_0)
143+
(= main@%.lcssa_0 main@%_3_0))
144+
(=> (and main@.verifier.error_crit_edge_0 main@.lr.ph_0)
145+
(= main@%.lcssa11_1 main@%.lcssa11_0))
146+
(=> (and main@.verifier.error_crit_edge_0 main@.lr.ph_0)
147+
(= main@%.lcssa10_1 main@%.lcssa10_0))
148+
(=> (and main@.verifier.error_crit_edge_0 main@.lr.ph_0)
149+
(= main@%.lcssa_1 main@%.lcssa_0))
150+
(=> main@.verifier.error_crit_edge_0
151+
(= main@%phitmp_0 (< main@%.lcssa_1 1000)))
152+
(=> main@verifier.error_0
153+
(and main@verifier.error_0 main@.verifier.error_crit_edge_0))
154+
(=> (and main@verifier.error_0 main@.verifier.error_crit_edge_0)
155+
(= main@%c.0.i.lcssa_0 main@%.lcssa11_1))
156+
(=> (and main@verifier.error_0 main@.verifier.error_crit_edge_0)
157+
(= main@%a.0.i.lcssa_0 main@%phitmp_0))
158+
(=> (and main@verifier.error_0 main@.verifier.error_crit_edge_0)
159+
(= main@%b.0.i.lcssa_0 main@%.lcssa10_1))
160+
(=> (and main@verifier.error_0 main@.verifier.error_crit_edge_0)
161+
(= main@%c.0.i.lcssa_1 main@%c.0.i.lcssa_0))
162+
(=> (and main@verifier.error_0 main@.verifier.error_crit_edge_0)
163+
(= main@%a.0.i.lcssa_1 main@%a.0.i.lcssa_0))
164+
(=> (and main@verifier.error_0 main@.verifier.error_crit_edge_0)
165+
(= main@%b.0.i.lcssa_1 main@%b.0.i.lcssa_0))
166+
(=> main@verifier.error_0
167+
(= main@%_9_0 (= main@%b.0.i.lcssa_1 main@%c.0.i.lcssa_1)))
168+
(=> main@verifier.error_0
169+
(= main@%or.cond.i_0 (or main@%a.0.i.lcssa_1 main@%_9_0)))
170+
(=> main@verifier.error_0 (not main@%or.cond.i_0))
171+
(=> main@verifier.error_0
172+
(= main@%_10_0 (xor main@%a.0.i.lcssa_1 true)))
173+
(=> main@verifier.error_0 (= main@%_11_0 (xor main@%_9_0 true)))
174+
(=> main@verifier.error.split_0
175+
(and main@verifier.error.split_0 main@verifier.error_0))
176+
main@verifier.error.split_0)))
177+
(=> a!1 main@verifier.error.split)))
178+
(query main@verifier.error.split)
179+

‎tests/simple_smt/simple_test.smt2‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
; annotation
2+
(set-logic ALL)
3+
;(set-option :produce-proofs true)
4+
(declare-rel itp (Int Int))
5+
;(declare-rel simple!!query ())
6+
(declare-rel sq ())
7+
(declare-var A Int)
8+
(declare-var B Int)
9+
(declare-var C Int)
10+
(declare-var D Int)
11+
(rule (=> (and (< A 100) (> A 0)(= B A)) (itp A B)))
12+
(rule (=> (and (itp A B) (= D (+ A 0)) (= C (+ A 0))) (itp C D)))
13+
(rule (=> (and (itp A B) (not (= A B))) sq))
14+
(query sq :print-certificate true)

0 commit comments

Comments
 (0)