[SMTChecker] Add option divModWithSlacks #11738
Conversation
leonardoalt
force-pushed
the
smt_div_mod_slacks
branch
from
8a067b2 to
137529a
Compare
|
The effect this has is that if |
leonardoalt
force-pushed
the
smt_div_mod_slacks
branch
from
137529a to
8f6b400
Compare
|
@hrkrshnn tiny one 😬 |
|
Actually missing command line JSON tests |
test/cmdlineTests/model_checker_divModSlacks_default_all/input.sol
Outdated
Show resolved
Hide resolved
leonardoalt
force-pushed
the
smt_div_mod_slacks
branch
from
8f6b400 to
a105948
Compare
|
@cameel see the |
|
Oh, so it looks like instead of simply cutting out all messages we should be inserting I'll try to fix that and submit a PR. |
|
Here's a PR that fixes the warning stripping + adds pragmas and SPDX comments to tests that were missing them: #11751. |
leonardoalt
force-pushed
the
smt_div_mod_slacks
branch
2 times, most recently
from
b9d0bcd to
b1a4d62
Compare
|
Updated the comments, added JSON tests and put the license lines back after rebasing over @cameel 's PR that fixed the script. |
| @@ -0,0 +1 @@ | |||
|
|
|||
There was a problem hiding this comment.
You don't need these files when they are empty. I've just removed a bunch of empty ones in the PR that fixed the checks for empty output :P
We should really modify cmdlineTests.sh to just not create them.
There was a problem hiding this comment.
Yea.. I didn't create them, I just ran the script and committed whatever files I had for convenience
There was a problem hiding this comment.
Right. I think it just accepts the test without the file but if you ask it to update, it always creates it. I'll create an issue to clean this up eventually.
There was a problem hiding this comment.
I just removed this and other empty files from this PR.
| @@ -0,0 +1,49 @@ | |||
| {"auxiliaryInputRequested":{"smtlib2queries":{"0x10763dfdad96614fe8fcaf54161ed2be500bbaa57bda8e2d706b675f1290f13b":"(set-option :produce-models true) | |||
There was a problem hiding this comment.
A few remarks not completely related to this PR:
auxiliaryInputRequested- The field is not documented as a part of Standard JSON output in
Using the compiler. - CLI does not produce this output. Why?
- I see that CHC does not produce this output either. Why?
- The field is not documented as a part of Standard JSON output in
solversoption added in [SMTChecker] Solver option #11421 is not listed in Standard JSON input either. It's only on the page about SMT.
There was a problem hiding this comment.
BTW, if any of this needs fixing, it does not necessarily have to be done in this PR (unless it's this PR that broke it).
There was a problem hiding this comment.
Right, this auxiliaryInputRequested is a bit of legacy that I'm not sure was ever used. Back when we didn't have emscripten z3 embedded into the compiler, we used this double run where you run the compiler once, get the queries like this, run a local solver, and input the results back into another compiler run via auxiliaryInput, using the same query hashes.
CLI doesn't produce it because the feature is only available via JSON.
CHC does produce it as well, when it can't prove a property.
There was a problem hiding this comment.
Ah ok, solver option should be there, so will open another PR fixing that later.
There was a problem hiding this comment.
OK, that explains it. What are your plans for auxiliaryInputRequested? Are you going to eventually remove it or can it be still useful in some rare cases?
There was a problem hiding this comment.
We talked about removing it in a call, but didn't reach consensus. Maybe we should just remove it
leonardoalt
force-pushed
the
smt_div_mod_slacks
branch
from
b1a4d62 to
08c065e
Compare
Currently we encode division and modulo as the constraint
a = b * d + mwhered = a / bandm = a % bbecause Spacer doesn't like syntactic/andmodinside Horn rules. However, other solvers (like Eldarica) might prefer the actual precise operations. This PR adds an option for that.