Dafny as a SAT-QBF solver is not giving right results

Question

I am trying to get the habit to use Dafny as a friendly SAT-QBF solver for some simple formulae, since doing it in, for instance, Z3 is too uncomfortable.

The context for this is that I have implemented Cooper's algorithm for quantifier elimination and, when all the variables are bounded, it can be used as a decision procedure: therefore, I want to know which is the result that I should get before executing it.

However, I encountered a problem in Dafny.

Let us raise, for instance, this formula (written in Dafny):

  assert forall x_1: int :: exists y_1: int :: forall x_2: int :: exists y_2 : int
    :: (y_2<y_1) && (x_2<y_2) && (x_1<x_2);

In my Cooper, it returns False, while Dafny returns assertion violation (along with the typical triggerswarnings), which I interpret as False too. Okay, so no problem with this.

But if I raise:

  assert exists x_1: int :: exists y_1: int :: exists x_2: int :: exists y_2 : int
    :: (y_2<y_1) && (x_2<y_2) && (x_1<x_2);

In my Cooper, it returns True, while Dafny also returns assertion violation. I have done a manual Cooper execution (pencil and paper) and I think the True is right one.

Any idea of what is going on?

PS: I have not tried it in Z3, yet, because I am doing first other attempts with other theories.

EDIT

Trigger warnings can be avoided using a simple trick to instantiate the quantified variables: creating an uninterpreted function.

method Main() {
 assert exists x_1 : int {:trigger P(x_1)} :: exists y_1: int {:trigger P(y_1)} 
    :: exists x_2: int {:trigger P(x_2)} :: exists y_2 : int {:trigger P(y_2)}
        :: (y_2<y_1) && (x_2<y_2) && (x_1<x_2);
}


predicate P(a: int)
{
   true
}

Answer 1

You cannot do this with Dafny. While Dafny supports quantifiers, booleans, arithmetic, and many other things (recursive functions, sets, sequences, objects and references, multi-dimensional arrays, induction, inductive and coinductive datatypes, bitvectors, greatest and least fixpoints of monotonic functions, etc.), it is not suitable for SAT-QBF (or QBF + artihmetic) benchmarks.

Dafny's errors, including the assertion violation, tell you that the verifier was not able to do the proof. It may be that the property still holds, but you'll need to supply more of the proof yourself. In other words, you should interpret the assertion violation as a "don't know" answer. Stated differently, you cannot decide (only semi-decide) formulas with Dafny.

Dafny uses quantifiers in the SMT solvers via matching patterns, aka triggers. When a quantifier has no good triggers, which is what Dafny's "no trigger" warning is telling you, you may see bad performance, unstable verifications, and so-called butterfly effects (where a small and seemingly unrelated part of the program causes a change in the automatic construction of other proofs). Triggers are driven by uninterpreted function symbols, which your example doesn't have at all.

If you want a readable syntax, you may be able to do what you're trying through Boogie. I have not tried that, but you could try putting Boogie in its monomorphic mode and then supplying prover options to ask for the SAT-QBF or something similar (see Boogie's /help). Otherwise, if you're interested in deciding these problems, then going directly to SMT solver is the way to go.