Question about choose satisifiability

[romac]

In this gist, I'm wondering why Stainless is able to find a counter-example for:

def noSolution(state: State): Boolean = {
  state.exec(prog).reg(Rbx) != 22
} holds

ie:

state: State -> State({Rbx() -> Some[Int](10), Rax() -> Some[Int](0), * -> Some[Int](0)})

but fails to satisfy this choose:

def solution: State = {
  choose { (state: State) =>
    state.exec(prog).reg(Rbx) == 22
  }
}

It seems to me that if Stainless can find a counter-example for the proposition Ɐ x:A. !P(x) then it should be able to find a satisfying assignment for ∃ x:A. P(x), or am I misunderstand how choose works/stands for?

[romac]

Oops, the counter-example should have read:

state: State -> State({Rbx() -> Some[Int](10), Rax() -> Some[Int](0), * -> Some[Int](0)})

I updated the post above.

[romac]

Closed the issue by mistake, sorry about that.

[samarion]

Stainless only invokes Inox for validity checks, namely each VC corresponds to a satisfiability check where UNSAT is expected. In your specific example, it would be possible for Stainless/Inox to handle the outermost forall with no free variables as a negated existential (and vice-versa) where SAT is expected and then flipping the result but this optimization is only valid under these very restrictive conditions. Basically, you could add

def solveIfForall(expr: Expr) = expr match {
  case Forall(args, body) if variablesOf(expr).isEmpty =>
    // actually you also need some other conditions checking that there aren't any
    // chooses in the bodies of the functions called in the forall...
    solve(Not(body)) match {
      case Sat(model) => Unsat
      case Unsat => Sat(Model.empty)
    }
  case _ => solve(expr)
}

In most cases of choose satisfiability, we'll have a quantifier alternation and then considering the contra-positive won't help much.

[samarion]

Chooses in Stainless are mostly an internal feature so I won't be changing the proof obligation generation for now. If we someday port synthesis from Leon, we can address this issue at that time. Closing until then.