Add support for SMT-LIB function definitions

[cbarrettfb]

This PR adds support for a function attribute ":define". Adding this attribute to a function generates a SMT-LIB "define-fun" command instead of a definition via universal quantification. Note that the function must not be recursive.

Example in Test/functiondefine.

[zvonimir]

This looks like a great addition! I do have a quick question though: how is this better/different than the :inline attribute that already exists?
I guess I understand how it is different at the level of the VC, but I am curious if solvers somehow handle define-fun more efficiently internally?
Thanks!

[cbarrettfb]

Good question Zvonimir. At the level of the VC, using :inline eagerly substitutes the function everywhere in the SMT formula. Using :define creates a define-fun and lets the solver decide how to handle things. Somewhat surprisingly, Z3 slows down quite a bit (3-4X) in some cases when using :inline, but the same examples are the same or even faster with :define. I'm not sure exactly why - I suspect Z3 may be doing some lazy definition expansion, but in any case, using definitions seems to give the solver more flexibility.

[shazqadeer]

It seems we are creating an axiom even when the programmer is indicating a function definition using :define. Is there some peculiarity of Boogie that is forcing this design?

[cbarrettfb]

Yes. At first, I tried an implementation that just stores the function definition as a special field in the Function class. However, such functions must ultimately be translated to VCExprs.
This requires adding a new type of VCExpr for function definitions. While conceptually clean, this ends up being a very heavy and error-prone change, as it requires changing all of the VCExpr visitors (there are like 10-20 of them). I thought it was maybe not worth it when I could instead recover the function from the axiom quite easily and not have to touch the VCExpr class heirarchy. I'm open to ideas if you think there is a better way.

[shazqadeer]

@RustanLeino : It would be helpful if you could take a look at this PR. @cbarrettfb is adding a very useful Boogie feature.

[bkragl]

Hi @cbarrettfb, this looks like a very nice addition to Boogie! I have a few suggestions that would be nice to apply before merging.

First, let me try to summarize what is going on to see if my understanding is correct. When a function is decorated with {:define} there is still a quantified axiom generated as for "regular" functions. However, the quantifier expression (not the axiom) is marked as a function definition, such that it can be treated differently (and actually not be emitted as quantified formula to the SMT solver) in the VC generation.

1. My first thought was that it would be nice if no axiom is generated for function definitions (what @shazqadeer also noted above), but now I think it is actually good because there could be prover backends that do not support function definitions. However, what is the reason that the quantifier expression has to be marked and not the axiom? In class Axiom I see the field isFunctionDefinition, but it is unused. Can it be removed?

2. I think it would be better if isFunctionDefinition would not be a field of QuantifierExpr and thus appear as optional parameter in all the constructors of it and ForallExpr. Instead, can we have a set that stores all ForallExpr objects related to function definitions, such that Boogie2VCExprTranslator.GenerateQuantifierInfos can query it? @shazqadeer, what would be a good place to keep such a set?

3. Parameter isFuncDef of VCExpressionGenerator.Forall (twice) and VCExpressionGenerator.Exists can be removed.

Finally, could you please pull in the current state of the master branch? This will help us ensure that all regression tests pass.

[shazqadeer]

If the summary provided by @bkragl is correct, wouldn't it be better to have the field isFunctionDefinition in the axiom?

[RustanLeino]

I'm thinking that it would be better to check for the attribute :define during the VC generation stages, rather than having the parser look for it and using another boolean in the AST. Was such a design rejected for some reason?

Please document :define in the /attrHelp flag.

[RustanLeino]

I suggest considering the design of this feature from the Boogie perspective. Is the following a good way to present it to the Boogie user?

• If a function is declared without a body, it is just an uninterpreted function. Of course, you can add axioms about it if you wish.

• If the function is given a body, then Boogie gives you three options:

  • Macro: The definition can be inlined in each place the function occurs, like a macro. This is illegal to do for recursively defined functions. Because the function definition is inlined, the function symbol itself is not part of the VC; this means that any use of the function in a trigger will also be replaced by the definition (which may produce an illegal trigger, where the function form looked okay as a trigger).

  • Axiom: The definition can be turned into a universally quantified axiom. By giving the definition in this way, it looks nice and localized in the Boogie program, and it saves you the trouble of generating the parameters once for the function and once for the axiom.

  • Lazy Expansion: If the underlying prover supports it, then the responsibility of equating a use of a function with its definition can be done during proving. This is similar to Axiom, but allows the prover to use different heuristics for when to bring the function definition into play. Like Macro, this option is illegal for recursively defined functions. (Does the function symbol stay around? In particular, what happens with a Lazy Expanded function that's used in a trigger?)

What is the best way for a Boogie user to select between these options? Currently, we have the {:inline} attribute, the new {:define} attribute, and probably the former also looks at some command-line options. It would be nice to have a clean and understandable story here.

[shazqadeer]

• Axiom: The definition can be turned into a universally quantified axiom. By giving the definition in this way, it looks nice and localized in the Boogie program, and it saves you the trouble of generating the parameters once for the function and once for the axiom.

@RustanLeino : If the function definition is recursive and this axiom option is applied, it seems to me that it is possible for an inconsistent axiom to be generated. Have you considered outlawing recursion altogether in function definitions, at least until termination check for functions has been implemented in Boogie?

[cbarrettfb]

@bkragl

First, let me try to summarize what is going on to see if my understanding is correct. When a function is decorated with {:define} there is still a quantified axiom generated as for "regular" functions. However, the quantifier expression (not the axiom) is marked as a function definition, such that it can be treated differently (and actually not be emitted as quantified formula to the SMT solver) in the VC generation.

Yes, that is correct.

1. My first thought was that it would be nice if no axiom is generated for function definitions (what @shazqadeer also noted above), but now I think it is actually good because there could be prover backends that do not support function definitions. However, what is the reason that the quantifier expression has to be marked and not the axiom? In class Axiom I see the field isFunctionDefinition, but it is unused. Can it be removed?

That is a potential benefit I did not consider, yes. The main reason is what I said in my response to Shaz. Adding another VCExpr subclass seems unnecessarily complicated and error-prone. Ah - you are right - it is not used in Axiom. Removed.

2. I think it would be better if isFunctionDefinition would not be a field of QuantifierExpr and thus appear as optional parameter in all the constructors of it and ForallExpr. Instead, can we have a set that stores all ForallExpr objects related to function definitions, such that Boogie2VCExprTranslator.GenerateQuantifierInfos can query it? @shazqadeer, what would be a good place to keep such a set?

I've removed it from the constructors where it is not needed. I suppose that such a set would be another possible implementation, though it may be a bit more cumbersome to ensure that both the AST and the translator have access to it. What is the rationale? Is it that we don't want to take up unnecessary space in the AST? It seems to me that one flag is not too bad, but I'm open to changing it.

3. Parameter isFuncDef of VCExpressionGenerator.Forall (twice) and VCExpressionGenerator.Exists can be removed.

OK I think I've removed this where possible.

Finally, could you please pull in the current state of the master branch? This will help us ensure that all regression tests pass.

Done.

[cbarrettfb]

@shazqadeer

If the summary provided by @bkragl is correct, wouldn't it be better to have the field isFunctionDefinition in the axiom?

Right - that was my initial thought also. The problem is that the translator doesn't have access to the Axiom object, only to the QuantifierExpr object. So we need a flag in the AST node, we need to check it in the translator, and we need a flag in the VCExpr - the quantifier info seemed like a convenient place to put the flag as we already store other flags there and it required changing the least amount of code. But we only have access to the QuantifierExpr object when creating the quantifier infos in the translator.

[cbarrettfb]

@RustanLeino

I'm thinking that it would be better to check for the attribute :define during the VC generation stages, rather than having the parser look for it and using another boolean in the AST. Was such a design rejected for some reason?

Hmm...how would that work exactly? Maybe i'm missing something, but right now, it seems that functions are either inlined or converted into axioms, so there's no translation done on a function directly during the translation stage. I'm not sure how I could check a quantified axiom to see whether it is a function definition without having some flag there. There is no back pointer from the axiom to the function it was created from. I'm definitely open to suggestions, but I didn't see a simpler way to do this. I'm a noob when it comes to Boogie though so feel free to let me know if I'm missing something!

Please document :define in the /attrHelp flag.

Done.

[cbarrettfb]

I suggest considering the design of this feature from the Boogie perspective. Is the following a good way to present it to the Boogie user?

• If a function is declared without a body, it is just an uninterpreted function. Of course, you can add axioms about it if you wish.

• If the function is given a body, then Boogie gives you three options:

  • Macro: The definition can be inlined in each place the function occurs, like a macro. This is illegal to do for recursively defined functions. Because the function definition is inlined, the function symbol itself is not part of the VC; this means that any use of the function in a trigger will also be replaced by the definition (which may produce an illegal trigger, where the function form looked okay as a trigger).
  • Axiom: The definition can be turned into a universally quantified axiom. By giving the definition in this way, it looks nice and localized in the Boogie program, and it saves you the trouble of generating the parameters once for the function and once for the axiom.
  • Lazy Expansion: If the underlying prover supports it, then the responsibility of equating a use of a function with its definition can be done during proving. This is similar to Axiom, but allows the prover to use different heuristics for when to bring the function definition into play. Like Macro, this option is illegal for recursively defined functions. (Does the function symbol stay around? In particular, what happens with a Lazy Expanded function that's used in a trigger?)

What is the best way for a Boogie user to select between these options? Currently, we have the {:inline} attribute, the new {:define} attribute, and probably the former also looks at some command-line options. It would be nice to have a clean and understandable story here.

Yes, I think this is an accurate picture after adding this feature. I might say it a slightly different way. With the first two options (macro, axiom), Boogie takes responsibility for how the function will be encoded. It's either inlined or turned into a quantified expression. In the third case (using :define), the solver is responsible for it. The solver can choose to inline or not and can choose to use quantifier-like heuristics or not. The question about whether the function symbol stays around is probably solver-dependent. I don't know what would happen if you use it in a trigger, but my guess is that it will probably behave similar to the first option (Macro).

As for the question of how a Boogie user should select between the options, that's a bit tricky. I would have guessed that {:inline} and {:define} would behave similarly, but I found that on our examples, {:define} is often much more efficient. But this may be different on other examples.

For me, it really comes down to having more fine-grained control over the generated SMT file. I always prefer using quantifier-free encodings if possible, so for me the {:define} route is a nice clean way to do that, and it's what I would personally recommend, but again I suspect others may take a different view.

[zvonimir]

This pull request is subsumed by #236 and so I am closing this one.

[RustanLeino]

I'm trying to figure out if the "Axiom" mode is still supported. In the experiments I've tried, it seems that a function with a body (and without the {:define} attribute) always causes the function's body to be inlined (whether or not {:inline} is explicitly part of the input). Am I missing something or is the "Axiom" functionality not supported?

[shazqadeer]

I just tried Boogie master version on the following program:

function foo(x: int): int {
    3
}

procedure A() {
    assert foo(0) == 3;
}

The generated SMTLIB2 file was the following:

(set-option :print-success false)
(set-info :smt-lib-version 2.6)
(set-option :smt.mbqi false)
(set-option :model.compact false)
(set-option :model.v2 true)
(set-option :pp.bv_literals false)
; done setting options


(declare-fun tickleBool (Bool) Bool)
(assert (and (tickleBool true) (tickleBool false)))
(declare-fun foo (Int) Int)
(assert (forall ((x Int) ) (! (= (foo x) 3)
 :qid |blahbpl.1:14|
 :skolemid |0|
 :pattern ( (foo x))
)))
(declare-fun ControlFlow (Int Int) Int)
(push 1)
(set-info :boogie-vc-id A)
(set-option :timeout 0)
(set-option :rlimit 0)
(assert (not
 (=> (= (ControlFlow 0 0) 66) (let ((anon0_correct  (=> (= (ControlFlow 0 41) (- 0 67)) (= (foo 0) 3))))
(let ((PreconditionGeneratedEntry_correct  (=> (= (ControlFlow 0 66) 41) anon0_correct)))
PreconditionGeneratedEntry_correct)))
))
(check-sat)
(pop 1)
; Valid

As you can see, the axiom is being generated.

[RustanLeino]

Oh, thank you! I now see my problem. I'm using the API and wanted to have the effect of the foo in your example. I had set the .Body field, but that's not the way to do it. (There's even a comment next to that field in the Boogie sources that tells me .Body is to be used only with {:inline}.) To me delight, I see there's a method Function.CreateDefinitionAxiom that I should call instead of setting the .Body. Thanks for setting me straight.