Comments (3)
I had another look at the Btor2 paper and discovered that the example in Fig 3
also has a negative node id.
Do I interpret this correctly as inverting a boolean (i.e. 1-bit bitvector)? Can this be used anywhere a 1-bit signal is used? What happens if a multi-bit signal is refereed to with a negative node id? Do all bits get inverted?
from btor2tools.
A negative node id is a shorthand for bitwise negation, which can be used for any Boolean or bit-vector term.
from btor2tools.
A negative node id is a shorthand for bitwise negation, which can be used for any Boolean or bit-vector term.
Thanks for the confirmation!
I fixed it in my implementation: ucb-bar/maltese-smt@c953052
from btor2tools.
Related Issues (11)
- [btor2parser] memory allocation failed HOT 1
- Parse error for `init`: state id must be greater than id of second operand HOT 2
- Semantics of negated signals with the minus sign HOT 2
- Negating an array with the minus sign HOT 1
- Partial register initialization HOT 3
- btorsim: `BTOR2_tag_iff` not marked as implemented HOT 3
- btorsim: missing implementation for `BTOR2_tag_rol`, `BTOR2_tag_ror`, and `BTOR2_tag_smod` HOT 1
- btorsim: incorrect implementation for `BTOR2_tag_sra`
- case 'l' in btor2parser.c
- Build with btor2aiger fails HOT 3
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.
from btor2tools.