Conversation
src/engine/bmc/bmc_engine.cpp
Outdated
| // Transition formula | ||
| expr::term_ref transition_formula = ts->get_transition_relation(); | ||
|
|
||
| // Invariant formula |
There was a problem hiding this comment.
Invariants were actually never implemented before. Transition systems had methods for adding invariants, but these were never used nor accessed. This change (and to the other engines) actually implements invariants properly.
The only caveat is that I didn't implement them for the pdkind engine, so I will take a look at that.
src/engine/kind/kind_engine.cpp
Outdated
| // Transition formula | ||
| expr::term_ref transition_formula = ts->get_transition_relation(); | ||
|
|
||
| // Invariant formula |
There was a problem hiding this comment.
why this change?
Was there a bug before?
There was a problem hiding this comment.
See comment on bmc_engine
src/engine/simulator/simulator.cpp
Outdated
| // Transition formula | ||
| expr::term_ref transition_formula = ts->get_transition_relation(); | ||
|
|
||
| // Invariant formula |
There was a problem hiding this comment.
See comment on bmc_engine
src/parser/btor/btor_state.cpp
Outdated
| bad_children.push_back(bad); | ||
| } | ||
| // FIXME: Don't think this works for more than one child -- | ||
| // 'property' is a bool, but then the next line compares it to bv 0 |
There was a problem hiding this comment.
I think that this might because there is no Boolean type in BTOR. Instead a BV of 1 bit is used for true/false.
There was a problem hiding this comment.
I think this is incorrect though, because property is of type Boolean (since it's an OR), but then is compared to the bit-vector zero (so there is a type mismatch). I would need to test this out to see what happens though.
src/system/context.cpp
Outdated
| } | ||
| d_transition_systems.get_entry(id)->add_invariant(sf); | ||
| } | ||
| // void context::add_invariant_to(std::string id, state_formula* sf) { |
There was a problem hiding this comment.
This was not used by any module -- I can remove this since now the invariant is just a single formula.
|
I'll add invariant support to the pdkind engine. |
|
@ahmed-irfan This should be ready to review/merge |
ahmed-irfan
left a comment
ahmed-irfan
left a comment
There was a problem hiding this comment.
Left one comment.
Rest LGTM
2 participants
Adds a BTOR2 frontend using the btor2tools parsing library.