boolector / btor2tools Goto Github PK
View Code? Open in Web Editor NEWA generic parser and tool package for the BTOR2 format.
License: Other
btor2tools's Issues
Partial register initialization
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?
btorsim: missing implementation for `BTOR2_tag_rol`, `BTOR2_tag_ror`, and `BTOR2_tag_smod`
Btorsim is missing an implementation of the rotation operations rol, ror, and smod
btorsim: incorrect implementation for `BTOR2_tag_sra`
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
.
case 'l' in btor2parser.c
Hi, in btor2parser.c, line 1434 writes: "case 'l': PARSE (state, input); break;"
Is it supposed for some keyword starting with 'l'?
Parse error for `init`: state id must be greater than id of second operand
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!
Build with btor2aiger fails
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
Negative node ids?
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!
Negating an array with the minus sign
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.
[btor2parser] memory allocation failed
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.
btorsim: `BTOR2_tag_iff` not marked as implemented
Btorsim is missing an implementation of the iff operation.
Semantics of negated signals with the minus sign
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!
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.