I am interested in solving QF_BV + QF_IDL formulas where QF_BV encodes data-flow and QF_IDL encodes scheduling constraints.
However, according to the Yices2 documentation the Floyd-Warshall solver is only usable for pure QF_IDL and cannot be combined with other theories. I am wondering where this restriction comes from? In my case, there are no mixed-theory atoms; the theories only loosely interact via a boolean structure.
For Z3, just enabling Floyd-Warshall could make verification 4-8x times faster (see Z3Prover/z3#8940).
I was wondering if Yices2 could gain a similar speed-up for our SMT queries if we could use Floyd-Warshall.
This is particularly interesting for us because Yices2 is already substantially faster than Z3 and often outperforms it, even if Z3 uses Floyd-Warshall!
Does Yices2 eagerly bit-blast QF_BV (we don't use MCSAT)? If so, maybe it would be easy to allow the user to enable Floyd-Warshall in cases where bit-blasting brings the formula into QF_IDL?
I am interested in solving
QF_BV + QF_IDLformulas whereQF_BVencodes data-flow andQF_IDLencodes scheduling constraints.However, according to the Yices2 documentation the Floyd-Warshall solver is only usable for pure
QF_IDLand cannot be combined with other theories. I am wondering where this restriction comes from? In my case, there are no mixed-theory atoms; the theories only loosely interact via a boolean structure.For Z3, just enabling Floyd-Warshall could make verification 4-8x times faster (see Z3Prover/z3#8940).
I was wondering if Yices2 could gain a similar speed-up for our SMT queries if we could use Floyd-Warshall.
This is particularly interesting for us because Yices2 is already substantially faster than Z3 and often outperforms it, even if Z3 uses Floyd-Warshall!
Does Yices2 eagerly bit-blast
QF_BV(we don't use MCSAT)? If so, maybe it would be easy to allow the user to enable Floyd-Warshall in cases where bit-blasting brings the formula intoQF_IDL?