Add conversion of incremental smt2 data structures to string #6240
Conversation
Because the bit vector theory defined in SMT2 does not allow for bit vectors of 0 bits.
So that they can be sent to an SMT2 solver using a string based interface.
thomasspriggs
requested review from
NlightNFotis,
TGWDB,
chrisr-diffblue,
kroening,
peterschrammel and
tautschnig
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #6240 +/- ##
===========================================
+ Coverage 76.18% 76.22% +0.03%
===========================================
Files 1478 1482 +4
Lines 161669 161833 +164
===========================================
+ Hits 123165 123353 +188
+ Misses 38504 38480 -24
Continue to review full report at Codecov.
|
|
|
||
| void visit(const smt_logic_quantifier_free_bit_vectorst &) override | ||
| { | ||
| os << "QF_BV"; |
There was a problem hiding this comment.
This is not the logic we currently use and this can cause errors later (we currently use QF_AUFBV explicitly, or for z3 we don't specify and let z3 assume ALL).
There was a problem hiding this comment.
Is QF_BV enough for our first slice of functionality? I plan to add more different logics in a follow up PR, but I was deliberately limiting the scope of this and the preceding PR, in order to keep things more easily reviewable.
There was a problem hiding this comment.
We need at least UF for free function symbols:
tgw@DB0907:~$ z3 -smt2 -in
(set-logic QF_BV)
(declare-fun |f| ((_ BitVec 32) (_ BitVec 33)) (_ BitVec 31))
(error "line 2 column 60: logic does not support uninterpreted functions")
as above QF_BV alone will fail, but QF_UFBV below is ok:
tgw@DB0907:~$ z3 -smt2 -in
(set-logic QF_UFBV)
(declare-fun |f| ((_ BitVec 32) (_ BitVec 33)) (_ BitVec 31))
(define-fun |f| ((|g| (_ BitVec 32)) (|h| (_ BitVec 32))) Bool (|=| |g| |h|))
(check-sat)
sat
So that they can be sent to an SMT2 solver using a string based interface.
For uniformity with `smt_declare_function_commandt` and ease of correctly escaping the identifer when converting to string.
So that they can be sent to an SMT2 solver using a string based interface.
Some of the outputs can currently be safely captured by value. However there is the potential for accidentally introducing dangling reference type bugs from changes elsewhere in the term to string conversion code. Therefore this change will reduce the likelyhood of bugs being introduced in future and should have minimal performance impact due to the copy-on-write properties of ireps.
thomasspriggs
force-pushed
the
tas/smt2_data_structures_to_string
branch
from
e0d089e to
aacc171
Compare
| return os; | ||
| } | ||
|
|
||
| std::string smt_to_string(const smt_logict &logic) |
There was a problem hiding this comment.
Should we make the naming here (and in the class/file name) a little more explicit? e.g. smt_to_smt2_string ? Otherwise its not explicitly clear what sort of 'string' is being returned.
There was a problem hiding this comment.
I am fine with making that change if you think it would make things clearer. I can't think of many other kinds of string which we could be converting to, but that is probably because I've been busy writing this one.
In order to make the kind of string being converted to clearer.
In order to make the kind of string being converted to clearer.
In order to be clear about the kind of strings which should be generated.
4 participants
Add conversion of incremental smt2 data structures to string. So that they can be converted and sent to a solver. Visitors are used for this implementation, so that the conversion code can be kept separate from the data structures.
My commit message includes data points confirming performance improvements (if claimed).