z3 hangs on query involving maps and bitvectors #7484
Comments
…no quantifiers, #7484 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
These should use relevancy=0. It helps for second case. The first is solved by sat.smt=true, which is a different solver. |
|
Doing solver comparison for the first case, I found that the cvc5 (1.2.0) reports every problem is UNSAT. Based on Ranjit's description, it seems UNSAT is the expected result. |
|
This is what I get: C:\z3\release>z3 z3-slow-2.smt2.txt sat.smt=true C:\z3\release>z3 z3-slow-1.smt2.txt sat.smt=true what benchmarks are you using? |
|
Does this declaration mean that you are effectively introducing a definition of a tuple type? There appears to be two alternate definitions depending on scopes. |
|
@NikolajBjorner In my comment above I was testing both benchmarks that Ranjit attached. This is z3 4.13.3 on Linux: On macOS arm64, I was able to test both 4.13.3 and 4.13.4. Z3 reports different results for both of Ranjit's benchmarks on these two versions: |
|
Yes, bugs were fixed for 13.4. The tactic for removing unconstrained sub-terms was buggy. |
I went ahead and introduced a single tuple variable rather than building one from a1..a9 and it does seem to make a huge difference (solved almost instantly). Thanks for that tip! For the other one, If so, I'm assuming the patch is to use |
It uses an entirely different backend solver. It is not generally tuned as the legacy solver and I often find performance gaps. |
…no quantifiers, Z3Prover#7484 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
… been allocated. Instances, such as #7484 can be solved faster by either having authors rewrite benchmarks or by using incremental pre-processing. You can add incremental pre-processing to the SMT solver by using the command ``` (set-simplifier (then simplify propagate-values solve-eqs elim-unconstrained simplify)) ``` This command can be invoked any time prior to push or adding assertions. The effect of the command is that it adds an incremental pre-processing pass to check-sat invocations that is potentially more powerful than the default pre-processing. The default pre-processing functionality is not touched mainly to avoid instability against functionality that is already built around its behavior.
* add prd Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * missing text Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #7647 * fix #7647 - with respect to scope level * initial stab at randomizer Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Create prd.yml * missing text Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Update prd.yml * allows setting simplifier factory independently of whether solver has been allocated. Instances, such as #7484 can be solved faster by either having authors rewrite benchmarks or by using incremental pre-processing. You can add incremental pre-processing to the SMT solver by using the command ``` (set-simplifier (then simplify propagate-values solve-eqs elim-unconstrained simplify)) ``` This command can be invoked any time prior to push or adding assertions. The effect of the command is that it adds an incremental pre-processing pass to check-sat invocations that is potentially more powerful than the default pre-processing. The default pre-processing functionality is not touched mainly to avoid instability against functionality that is already built around its behavior. * remove experiment from pr --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
See commit message: you can use set-simplifier to tease out incremental behavior with the solver. |
Uh oh!
There was an error while loading. Please reload this page.
Hi z3 team -- my student @vrindisbacher came across the following two SMTLIB queries that seem to finish instantaneously with
cvc5but seem to makez3hang indefinitely. I will ask John Regehr's help with usingc-reduceto minimize the tests -- but maybe you have some idea?There are two files.
The first test
z3-slow-1.smt2.txtshould work just by pure equality/congruence.There is a lot of junk in it but we're just checking a VC of the form.
(a = b) => (a = b)except that that the
aandbare blown out into gigantic terms involving map-setand bitvector operations, with some additional booleans recording the equality...
The second is not so trivial, but both seem to finish swiftly with CVC5.
Any ideas on what might be happening?
z3-slow-1.smt2.txt
z3-slow-2.smt2.txt
The text was updated successfully, but these errors were encountered: