External SMT solver bare "or" crashes #359
Description
When running received error
Running external solver boolector
boolector: <stdin>:154:26: expected expression
Uncaught exception:
Upon investigation it appears Z3 is printing smtlib differently in the new version. Here is a snippet of the problem
(let ((a!10 (=> a!1
(=> (ite or true a!9)
(= (bvadd #x00000003 #x00000002) #x00000005)))))
(=> a!10 false))))))))
The bare or is presumably representing false but is not accepted by boolector.
A quick hacky fix is to change line 267 of z3_utils.ml to
let check_external
(solver : Z3.Solver.solver)
(solver_path : string)
(ctx : Z3.context)
(declsyms : (Z3.FuncDecl.func_decl * Z3.Symbol.symbol) list) : Z3.Solver.status =
let smt_string = Z3.Solver.to_string solver in
(* Valid uses of `or` are preceded by "(", Even if I'm wrong, false is not an operator, so should fail (false x y) for example will fail *)
let smt_string = String.substr_replace_all smt_string ~pattern:" or" ~with_:" false" inBut something more elegant may be desirable.
I note that parsing the smtlib and doing to substitution over Sexp.t is not as straightforward as one might like. It is inefficient (who cares actually though), more importantly you have to deal with the escaping issues earlier. Such a fix still does not really get at the deeper issue of why these or are being generated anyway. Nevertheless, here's what I think such a transformation might look like
(** [remove_lone_or] removes "or" appearing as an atom without parens around it.
Latest Z3 version is outputting this. I am guessing that "or" is an empty or clause,
which represents `false` (the identity element of or)
*)
let rec remove_lone_or (s : Sexp.t) : Sexp.t =
match s with
| List (Atom "or" :: s) -> List (Atom "or" :: List.map ~f:remove_lone_or s)
| Atom "or" -> Atom "false"
| List sexps -> List (List.map sexps ~f:remove_lone_or)
| Atom _ -> s