Counterexample Generation with Function Invocation

[DavePearce]

Currently, counterexample generation in the presence of function invocation fails. A minimal example would be this:

function f() -> (int r)

assert "postcondition not satisfied":
    forall(int i):
        if:
            i == 0
        then:
            f() > 0

This is not a surprise as we have the following comment in Interpreter.resolve(Expr.Invoke):

// What we need to do here is look at the return type and return
// something sensible. Or we could preiterate all function
// invocations beforehand.
throw new RuntimeException("UNKNOWN");

This is the error reported. I'm not sure why it doesn't go through and pull out the right one. What would happen if it did this?

[DavePearce]

What we probably need to do here is add the following method:

Iterable<Environment> Environment.declare(Decl.Named.Function fun, Object... arguments)

This needs to allow for iteration over possible return values whilst remembering specific parameter values as well. That way, it is forced to return the same value for the same argument set (that is, implement a proper function).

[DavePearce]

Right, that doesn't work exactly. The problem is that we really need a top-level iterator over functions which are used within a given assertion.