[WIP] [Model] Handle definition of constants in smt2 file

[bobot]

Fixes some errors found by @jhoenicke

• Definition in smt2 file should be handled differently than in response file.

[Gbury]

I'm not sure I see what problem exactly is fixed by the different handling of definitions (the tests added already pass without the changes).

[Gbury]

On the other hand, there can be issues when a problem files does something along the following lines: declare-const a; define-const b = a + 1, and we need to wait for the definition of a in the response/model file before we can evaluate b. This particular case would be solved by your patch, but if the response file tries to define a constant using the value of a constant defined in the problem file, then the code with your patch will generate an error. I think I see how to solve that, and i'll implement the proper solution this week.

[bobot]

declare-const a; define-const b = a + 1

I think def2.smt2 is exactly this case with a instead of a+1

but if the response file tries to define a constant using the value of a constant defined in the problem file

I think it should not be accepted. Accepting more would put too much burden on tools that also parses models. I think the terms that can define a model should be precisely defined (constants, or specific builtin function like store and const). In no case symbol definition from the problem.

[Gbury]

You're correct: define-sorts indeed cause an error whereas they shouldn't, and we need to record the definitions from the problem file after all the definitions form the model. I'll fix that asap, ^^

[jhoenicke]

but if the response file tries to define a constant using the value of a constant defined in the problem file

My feeling is that a model should not use any benchmark-defined/declared functions. For real constants it should just give the value directly, for uninterpreted sorts it should give model values, and for function definitions it should only use theory-defined symbols (ite, <, =, +, *, etc).

Following that logic, the model should also not use benchmark-defined sorts and instead use their underlying definition in the model. At least Bitwuzla and cvc5 do this for the benchmarks containing define-sort.

This way it's correct to first parse the model (after setting the logic) and then parse the benchmark skipping the declared functions. If the model could refer to the benchmark-declared functions, one would need to parse the benchmark and when there is a declare-fun search for the definition in the model and then parse that definition (and complain about cyclic dependencies).

For datatypes we may later run into problems, as these are declared in the benchmark and the model needs to use constructors and match terms. But for now, the smt-comp's model-validation track doesn't run on datatype logics.

[Gbury]

These changes (albeit a bit adjusted) are now included in the model branch, see 419ad7a and 187b479

[Gbury]

My feeling is that a model should not use any benchmark-defined/declared functions. For real constants it should just give the value directly, for uninterpreted sorts it should give model values, and for function definitions it should only use theory-defined symbols (ite, <, =, +, *, etc).

Following that logic, the model should also not use benchmark-defined sorts and instead use their underlying definition in the model. At least Bitwuzla and cvc5 do this for the benchmarks containing define-sort.

Indeed, the model definitions should only map constants to values, and therefore, we can evaluate them, and then evaluate the definitions from the original problem file (which may use the values defined by the model).

This way it's correct to first parse the model (after setting the logic) and then parse the benchmark skipping the declared functions. If the model could refer to the benchmark-declared functions, one would need to parse the benchmark and when there is a declare-fun search for the definition in the model and then parse that definition (and complain about cyclic dependencies).

For datatypes we may later run into problems, as these are declared in the benchmark and the model needs to use constructors and match terms. But for now, the smt-comp's model-validation track doesn't run on datatype logics.

Dolmen already supports algebraic datatype in model verification. It can do so because the way things work is: parse and type the problem file, record all the definition/assertions, parse and type the model file, evaluate the definition from the model, and then evaluate the definitions from the problem file, and then evaluate the assertions.