-
Notifications
You must be signed in to change notification settings - Fork 54
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Missformed SMT source, Unknown SMT term of class: class smtlib.trees.Terms$FunctionApplication #1549
Comments
The error is apparently not in the generation of the SMT2 file, but rather in reading the SMTLIB model into Inox terms (In Inox: SMTLIBParser.scala:226). It starts here while reading function definitions from the model. This seems to be caused by the fact that cvc5 is outputting a model where the model for one function uses the generated model for another function (but is returning them in the opposite order). Illustrated here: Definitions: (declare-fun lt () State)
(declare-fun r (State Action) Option) And the model: (define-fun lt () State (valueOf (r [...]) ; trimmed
(define-fun r ((arg1 State) (arg2 Action)) Option None) (cleaned up a bit for readability) There is also a Inox doesn't seem to expect this usage of functions and thus returns it as an unknown symbol. I'm checking if this is unexpected behaviour from the solver, or a failure to read it from Inox's end because of the order they are returned in. z3 does not have this behaviour on this example, at least. Its model does not use other functions at all, only lets and ADT constructors. |
I suspected this and tried to use
--check-models=false
but that turns off only our execution base validation. Can we make it turn
off reconstruction of the model as well, so it only gets a boolean answer?
…On Fri, 2 Aug 2024, 08:46 Sankalp Gambhir, ***@***.***> wrote:
The error is apparently not in the generation of the SMT2 file, but rather
in reading the SMTLIB model into Inox terms (In Inox:
SMTLIBParser.scala:226
<https://github.com/epfl-lara/inox/blob/3f5bd759182f1c07ac1da2c48ed75c759bfe95ba/src/main/scala/inox/solvers/smtlib/SMTLIBParser.scala#L226>).
It starts here while reading function definitions from the model
<https://github.com/epfl-lara/inox/blob/3f5bd759182f1c07ac1da2c48ed75c759bfe95ba/src/main/scala/inox/solvers/smtlib/SMTLIBSolver.scala#L81>
.
This seems to be caused by the fact that cvc5 is outputting a model where
the model for one function *uses* the generated model for another
function. Illustrated here:
Definitions:
(declare-fun lt () State)
(declare-fun r (State Action) Option)
And the model:
(define-fun lt () State (valueOf (r [...]) ; trimmed
(define-fun r ((arg1 State) (arg2 Action)) Option None)
(cleanup up a bit for readability)
There is also a valueOf None expression, which as far as I can tell, is
assigned some unique value while testing for satisfiability (and is not
returned).
Inox doesn't seem to expect this usage of functions within each other. I'm
checking if this is expected behaviour from the solver, or a failure to
read it from Inox's end. z3 does not have this behaviour on this example,
at least.
—
Reply to this email directly, view it on GitHub
<#1549 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AA5CDN23IKKNGJZQAJRC4XTZPMTLTAVCNFSM6AAAAABLZF7N7WVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDENRUGY3TSNBUHA>
.
You are receiving this because you authored the thread.Message ID:
***@***.***>
|
That's correct, the "check model" option is only checked after retrieval and construction of the model in the unrolling solver. The requirement of a model is encoded in the types and API as well ( After that it's a matter of changing the one-line |
Would you prefer to make this part of the |
Regarding the original issue: the order of definitions returned is not an issue, that is accounted for. Inox does also allow seeing some (marked) constants reused, but it never expects actual functions with parameters. The function |
I also wanted to remove model reconstruction when using |
With Can I move this issue to Inox instead? |
You can move the issue as desired. |
The snack dispenser example, https://github.com/epfl-lara/bolts/blob/main/tutorials/dispenser/Dispenser.scala
fails with smt-cvc5 with error messages apparently during Inox's preparation of the SMT-LIB file.
(Note: the benchmark only works with a substantial timeout with 43 seconds on my laptop to check exampleTrace postcondition; something that was likely not happening before.)
The text was updated successfully, but these errors were encountered: