boolector / btor2tools Goto Github PK
View Code? Open in Web Editor NEWA generic parser and tool package for the BTOR2 format.
License: Other
A generic parser and tool package for the BTOR2 format.
License: Other
In Btor2, both registers (states of bit-vector sort) and memories (states of array sort)
are initialized randomly unless init
is used to explicitly initialize their values.
The allows the partial initialization of a register by
applying a bit-mask to an uninitialized register.
For example, consider the Btor2 circuit:
1 sort bitvec 3
2 const 1 001
3 state 1
4 const 1 100
5 and 1 3 4
6 state 1
7 init 1 6 5
The register at line 6 is initialized to ?00
(?
indicates a random Boolean value).
If we append the following line to initialize the register at line 3:
8 init 1 3 2
What will the register at line 6 be initialized to in this case?
Will it now become 000
(001
& 100
) or remain as ?00
?
Consider the following BTOR2 file:
1 sort bitvec 3
2 sort bitvec 24
3 sort array 1 2
4 state 3
5 input 1
6 read 2 -4 5
Although line 6 negates an array with -
(which should be invalid), catbtor
does not complain about it.
However, if 7 not 3 4
is appended to the file, catbtor
reports:
*** catbtor: parse error in 'array_not.btor2' line 7: expected bitvec sort for not
It would be better if catbtor
could detect the error of the negated array at line 6.
Hello -
We are using the vmt2btor.py to create a btor2 file. However, when we call btor tools on such files, we always encounter the [btor2parser] memory allocation failed
problem. Did we miss something? Thanks.
For example, we start from this example given by the AVR model checker: https://github.com/aman-goel/avr/blob/master/examples/vmt/simple.c.vmt
(set-info :source |printed by MathSAT|)
(declare-fun .PC.0 () Bool)
(declare-fun .PC.1 () Bool)
(declare-fun .PC.2 () Bool)
(declare-fun x__1$main () (_ BitVec 32))
(declare-fun __RET__$main.next () (_ BitVec 32))
(declare-fun .PC.0.next () Bool)
(declare-fun .PC.1.next () Bool)
(declare-fun __RET__$main () (_ BitVec 32))
(declare-fun .PC.2.next () Bool)
(declare-fun |__NONDET_INLINE_INIT__4__3$main#0| () (_ BitVec 32))
(declare-fun n__3$main.next () (_ BitVec 32))
(declare-fun x__1$main.next () (_ BitVec 32))
(declare-fun n__3$main () (_ BitVec 32))
(define-fun .def_13 () Bool (! .PC.0 :next |.PC.0.next|))
(define-fun .def_14 () Bool (not .def_13))
(define-fun .def_11 () Bool (! .PC.1 :next |.PC.1.next|))
(define-fun .def_12 () Bool (not .def_11))
(define-fun .def_15 () Bool (and .def_12 .def_14))
(define-fun .def_9 () Bool (! .PC.2 :next |.PC.2.next|))
(define-fun .def_10 () Bool (not .def_9))
(define-fun .def_16 () Bool (! (and .def_10 .def_15) :init true))
(define-fun .def_72 () Bool (= n__3$main.next |__NONDET_INLINE_INIT__4__3$main#0|))
(define-fun .def_70 () Bool (= x__1$main.next (_ bv0 32)))
(define-fun .def_73 () Bool (and .def_70 .def_72))
(define-fun .def_67 () Bool (bvslt n__3$main.next (_ bv1 32)))
(define-fun .def_68 () Bool (not .def_67))
(define-fun .def_74 () Bool (and .def_68 .def_73))
(define-fun .def_29 () (_ BitVec 32) (! __RET__$main :next |__RET__$main.next|))
(define-fun .def_31 () Bool (= .def_29 __RET__$main.next))
(define-fun .def_75 () Bool (and .def_31 .def_74))
(define-fun .def_42 () Bool (not .PC.2.next))
(define-fun .def_18 () Bool (not .PC.1.next))
(define-fun .def_41 () Bool (and .def_18 .PC.0.next))
(define-fun .def_43 () Bool (and .def_41 .def_42))
(define-fun .def_76 () Bool (and .def_43 .def_75))
(define-fun .def_77 () Bool (and .def_16 .def_76))
(define-fun .def_34 () (_ BitVec 32) (! x__1$main :next |x__1$main.next|))
(define-fun .def_27 () (_ BitVec 32) (! n__3$main :next |n__3$main.next|))
(define-fun .def_60 () Bool (bvslt .def_27 .def_34))
(define-fun .def_45 () (_ BitVec 32) (bvadd (_ bv4294967295 32) .def_27))
(define-fun .def_46 () Bool (bvslt .def_45 .def_34))
(define-fun .def_61 () Bool (and .def_46 .def_60))
(define-fun .def_28 () Bool (= n__3$main.next .def_27))
(define-fun .def_62 () Bool (and .def_28 .def_61))
(define-fun .def_63 () Bool (and .def_31 .def_62))
(define-fun .def_35 () Bool (= x__1$main.next .def_34))
(define-fun .def_64 () Bool (and .def_35 .def_63))
(define-fun .def_20 () Bool (not .PC.0.next))
(define-fun .def_58 () Bool (and .PC.1.next .def_20))
(define-fun .def_59 () Bool (and .def_42 .def_58))
(define-fun .def_65 () Bool (and .def_59 .def_64))
(define-fun .def_55 () Bool (and .def_12 .def_13))
(define-fun .def_56 () Bool (and .def_10 .def_55))
(define-fun .def_66 () Bool (and .def_56 .def_65))
(define-fun .def_78 () Bool (or .def_66 .def_77))
(define-fun .def_49 () (_ BitVec 32) (bvadd (_ bv1 32) .def_34))
(define-fun .def_50 () Bool (= x__1$main.next .def_49))
(define-fun .def_47 () Bool (not .def_46))
(define-fun .def_51 () Bool (and .def_47 .def_50))
(define-fun .def_52 () Bool (and .def_28 .def_51))
(define-fun .def_53 () Bool (and .def_31 .def_52))
(define-fun .def_54 () Bool (and .def_43 .def_53))
(define-fun .def_57 () Bool (and .def_54 .def_56))
(define-fun .def_79 () Bool (or .def_57 .def_78))
(define-fun .def_38 () Bool (and .def_11 .def_14))
(define-fun .def_39 () Bool (and .def_10 .def_38))
(define-fun .def_32 () Bool (and .def_28 .def_31))
(define-fun .def_36 () Bool (and .def_32 .def_35))
(define-fun .def_21 () Bool (and .def_18 .def_20))
(define-fun .def_23 () Bool (and .def_21 .PC.2.next))
(define-fun .def_37 () Bool (and .def_23 .def_36))
(define-fun .def_40 () Bool (and .def_37 .def_39))
(define-fun .def_80 () Bool (or .def_40 .def_79))
(define-fun .def_24 () Bool (and .def_9 .def_15))
(define-fun .def_25 () Bool (and .def_23 .def_24))
(define-fun .def_81 () Bool (! (or .def_25 .def_80) :trans true))
(define-fun .def_82 () Bool (! (not .def_24) :invar-property 0))
(assert true)
Then we use vmt2btor.py in the recent version of vmt-lib tools for conversion: https://vmt-lib.fbk.eu/
; generated by vmt2btor.py on Wed May 11 17:04:41 2022
1 sort bitvec 1
2 sort bitvec 32
3 constd 1 1
4 state 1 .PC.0
5 state 1 .PC.1
6 state 1 .PC.2
7 input 2 n__3$main.next
8 input 2 __NONDET_INLINE_INIT__4__3$main#0
9 input 2 x__1$main.next
10 state 2 __RET__$main
11 input 2 __RET__$main.next
12 input 1 .PC.2.next
13 input 1 .PC.1.next
14 input 1 .PC.0.next
15 state 2 x__1$main
16 state 2 n__3$main
17 next 1 4 14
18 next 1 5 13
19 next 1 6 12
20 next 2 10 11
21 next 2 15 9
22 next 2 16 7
; init
23 not 1 14
24 not 1 13
25 and 1 24 23
26 not 1 12
27 and 1 26 25
; trans
28 not 1 5
29 not 1 4
30 and 1 29 28
31 and 1 30 6
32 and 1 12 25
33 and 1 32 31
34 eq 1 7 16
35 eq 1 10 11
36 and 1 35 34
37 eq 1 9 15
38 and 1 37 36
39 and 1 38 32
40 and 1 29 5
41 not 1 6
42 and 1 41 40
43 and 1 42 39
44 constd 2 4294967295
45 add 2 44 16
46 slt 1 45 15
47 not 1 46
48 constd 2 1
49 add 2 48 15
50 eq 1 9 49
51 and 1 50 47
52 and 1 34 51
53 and 1 35 52
54 and 1 24 14
55 and 1 26 54
56 and 1 55 53
57 and 1 4 28
58 and 1 41 57
59 and 1 58 56
60 and 1 13 23
61 and 1 26 60
62 slt 1 16 15
63 and 1 62 46
64 and 1 63 34
65 and 1 35 64
66 and 1 65 37
67 and 1 66 61
68 and 1 67 58
69 slt 1 7 48
70 not 1 69
71 constd 2 0
72 eq 1 9 71
73 eq 1 7 8
74 and 1 73 72
75 and 1 74 70
76 and 1 75 35
77 and 1 76 55
78 and 1 30 41
79 and 1 78 77
80 or 1 79 68
81 or 1 80 59
82 or 1 81 43
83 or 1 82 33
; reset sequence
84 state 1 model-reset0
85 init 1 84 -3
86 next 1 84 3
87 state 1 model-reset1
88 init 1 87 -3
89 next 1 87 84
90 and 1 84 -87
; model var
91 state 1 model-valid
92 init 1 91 -3
94 and 1 91 83
93 ite 1 90 27 94
95 ite 1 84 93 -3
96 next 1 91 95
; property 0
97 not 1 31
98 and 1 91 -97
99 bad 98
Then we call btorsim and encounter this issue.
Hi,
I am trying to understand the BTOR2 format.
I ran catbtor
(built at b8456dd) with the BTOR2 model program.btor2
of the example program in the CAV 2018 paper.
1 sort bitvec 1
2 sort bitvec 32
3 input 1 turn
4 state 2 a
5 state 2 b
6 zero 2
7 init 2 4 6
8 init 2 5 6
9 one 2
10 add 2 4 9
11 add 2 5 9
12 ite 2 3 4 10
13 ite 2 -3 5 11
14 next 2 4 12
15 next 2 5 13
16 constd 2 3
17 eq 1 4 16
18 eq 1 5 16
19 and 1 17 18
20 bad 19
However, I received a parse error:
*** catbtor: parse error in 'program.btor2' line 7: state id must be greater than id of second operand
Is this an intended behavior of the parser?
I could not find information on such restrictions in the CAV paper.
(The file can be successfully parsed if the line 6 zero 2
gets an nid
smaller than a's and b's.)
Thanks!
I encountered a btor file in your examples that contains a negative node id:
Looking at the spec it isn't clear to me what a negative node id means. According to the grammar (nid) := (num)
and num
is defined as a positive unsigned integer.
I would appreciate any explanation what the meaning of a negative node id is. Thanks!
Btorsim's implementation for sra
(shift arithmetic right) is wrong for negative inputs. It doesn't correctly check the sign bit of the left operand to determine whether to shift in zeros or ones.
Testcase:
;; -----------------------------------------------------------------------------
;; manually written btor file for testing binary operators
;; -----------------------------------------------------------------------------
1 sort bitvec 1
2 sort bitvec 8
;; -----------------------------------------------------------------------------
;; arithmetic shift right negative
;; -----------------------------------------------------------------------------
3 constd 2 4
4 const 2 10110110
5 const 2 11111011
6 sra 2 4 3
7 eq 1 5 6
8 bad 7 sra-negative
Witness:
#0
@0
.
Btorsim is missing an implementation of the rotation operations rol
, ror
, and smod
Btorsim is missing an implementation of the iff
operation.
The following commands to build with btor2aiger produce an error (Ubuntu 18.04.4, commit 9831f99):
git clone https://github.com/Boolector/btor2tools.git
cd btor2tools/
./setup-deps.sh
Error: *** configure.sh: invalid option '-fPIC' (try '-h')
The error occurs when running script deps/boolector/contrib/setup-btor2tools.sh
, which is called in ./setup-deps.sh
.
The patch below fixes the above error, but the installation flow still fails as follows:
cp: cannot stat 'build/libbtor2parser.a': No such file or directory
diff --git a/setup-deps.sh b/setup-deps.sh
index 4450d4c..b661a5c 100755
--- a/setup-deps.sh
+++ b/setup-deps.sh
@@ -18,6 +18,8 @@ git clone https://github.com/boolector/boolector deps/boolector
cd deps/boolector
git checkout bitblast-api
+sed "s/-fPIC//g" -i ./contrib/setup-btor2tools.sh
+sed "/configure/a cd build" -i ./contrib/setup-btor2tools.sh
./contrib/setup-btor2tools.sh
./contrib/setup-lingeling.sh
./configure.sh --prefix $(pwd)/../install
Hello,
I noticed that there are negated signals in some BTOR2 files, e.g., hwmcc20/bv/2019/beem/blocks.4.prop1-back-serstep.btor2
.
57 and 1 47 -49
However, I could not find the definition of the minus sign in the 2018 CAV paper.
Is the semantics of the minus sign bitwise inversion, i.e., not
?
Can we use the minus sign with a bitvec signal with more than one bit?
Many thanks!
Hi, in btor2parser.c
, line 1434 writes: "case 'l': PARSE (state, input); break;"
Is it supposed for some keyword starting with 'l'?
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.