Support (or correct use) of QF_UF/app?

[remigerme]

Hi,

I'm trying to play a bit with Smt.ml. I've written the following snippet:

open Smtml

module AltErgo = Solver.Batch (Altergo_mappings)
module Bitwuzla = Solver.Batch (Bitwuzla_mappings)

let solver_ae = AltErgo.create ()
let solver_bitwuzla = Bitwuzla.create ()

let f = Symbol.make Ty.Ty_app "f"
let x = Expr.symbol (Symbol.make Ty.Ty_bool "x")
let cond = Expr.app f [ x ]

let () =
  let res_ae =
    match AltErgo.check solver_ae [ cond ] with
    | `Sat -> "sat"
    | `Unsat -> "unsat"
    | `Unknown -> "unknown"
  in
  print_endline res_ae

let () =
  let res_bitwuzla =
    match Bitwuzla.check solver_bitwuzla [ cond ] with
    | `Sat -> "sat"
    | `Unsat -> "unsat"
    | `Unknown -> "unknown"
  in
  print_endline res_bitwuzla

Unfortunately, both solvers fail with an error Failure("Unsupported theory: app\n") which surprised me as QF_UF is usually supported. Note that I couldn't try with Z3 as I have problems installing it via opam.

• Am I missing something on how to use Smt.ml?
  Especially, I feel weird not specifying the expected type of f (Ty_bool -> Ty_bool in my head).
• If this is a currently missing feature of Smt.ml, is support for it planned?

Thanks!

[filipeom]

Hi! Thanks for using Smt.ml! Uninterpreted functions are still a quite recent addition, so the API is indeed a bit rough. To fix your example, you need to define the symbol `f` with its return type (in this case, `Ty_bool`), rather than `Ty_app`. The library then infers the full function signature based on the arguments you pass to `Expr.app`. Here is the corrected snippet: ```ocaml let f = Symbol.make Ty.Ty_bool "f" (* Make 'f' boolean so the App has bool return *) let x = Expr.symbol (Symbol.make Ty.Ty_bool "x") let cond = Expr.app f [ x ] (* Because 'x' and 'f' are bools. This app gets the inferred signature: bool -> bool *) ``` All uninterpreted functions take the type of the symbol passed as the first argument to `Expr.app` as their return value. The input types are derived automatically from the argument list. Regarding the backends: AltErgo was very recently added to Smt.ml, so while this fix solves the `Unsupported theory: app` error generally, let me know if you run into specific issues with AE.

- If this is a currently missing feature of Smt.ml, is support for it planned?

We actually have a prototype for typechecking the construction of expressions at compile-time. However, `Apps` are not currently included in that check. We are actively working to extend this and improve the API for expression construction. Let me know if you have any other questions!

[remigerme]

Thank you for the explanations!

I implemented your proposed fix. Two things:

1. I indeed encountered an error using AE - let me know if I should open a separate issue for this. Here is the stack trace:

   Fatal error: exception Not_found
   Raised at Stdlib__Hashtbl.MakeSeeded.find in file "hashtbl.ml", line 391, characters 17-32
   Called from AltErgoLib__D_cnf.Cache.find_sy in file "src/lib/frontend/d_cnf.ml", line 78, characters 4-28
   Called from AltErgoLib__D_cnf.make.aux in file "src/lib/frontend/d_cnf.ml", line 1887, characters 14-48
   Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
   Called from AltErgoLib__D_cnf.make.aux in file "src/lib/frontend/d_cnf.ml", lines 1767-1777, characters 8-18
   Called from Smtml__Altergo_mappings.M.Make.Solver.mk_cmds in file "src/smtml/altergo_mappings.default.ml", line 114, characters 21-60
   Called from Smtml__Altergo_mappings.M.Make.Solver.check in file "src/smtml/altergo_mappings.default.ml", line 202, characters 25-67
   Called from Smtml__Utils.run_and_time_call in file "src/smtml/utils.ml", line 7, characters 15-19
   Called from Smtml__Solver.Batch.check in file "src/smtml/solver.ml" (inlined), line 125, characters 41-68
   Called from Dune__exe__Example in file "bin/example.ml", line 48, characters 10-42 // Line 48 is the call to AltErgo.check
   

2. With Bitwuzla, I no longer have an error and the solver returns sat with the following model, which does not mention f:

    (model
    	(x bool false))

   I was rather expecting something like this (returned by Bitwuzla using the same condition expressed in SMT2):

   (
       (define-fun f ((@bzla.var_6 Bool)) Bool (ite (= @bzla.var_6 false) true false))
       (define-fun x () Bool false)
    )

   More annoying, I tested the following:

    let f = Symbol.make Ty.Ty_bool "f"
    let f_false_true = Expr.app f [ Expr.value Value.False ] (* Meaning that f(false) must be true *)
    let f_false_false = Expr.unop Ty.Ty_bool Ty.Unop.Not f_false_true (* Meaning that f(false) must be false *)

   When checked, the Bitwuzla solver returns sat which is unsound (at least, if I correctly wrote what I wanted to write, that is (assert (f false)) (assert (not (f false)))). It successfully returns unsat if considering a variable x and its negation not(x) instead of f(x) and not(f(x)). Any insight on this?

Thanks again.

[remigerme]

Hi @filipeom, any update regarding my reply above? Let me know if I should open separate issues on these two problems (especially if the unsoundness problem is indeed a problem and not just me being the problem by misusing the library) if that's more convenient.

[filipeom]

Hi @remigerme sorry for the slow response. This slipped my inbox.

I was rather expecting something like this (returned by Bitwuzla using the same condition expressed in SMT2):

Unfortunately we have yet to implemented model completion for uninterpreted functions. We're going to do it eventually. But, that is the reason you don't see a model for f yet.

When checked, the Bitwuzla solver returns sat which is unsound (at least, if I correctly wrote what I wanted to write, that is (assert (f false)) (assert (not (f false)))). It successfully returns unsat if considering a variable x and its negation not(x) instead of f(x) and not(f(x)). Any insight on this?

I tested it with bitwuzla and z3 (see code below) and it seems z3 correctly returns unsat. So it seems there is an issue in our bitwuzla mappings. I'm going to open an issue to track this.

open Smtml

module Z3 = Solver.Batch (Z3_mappings)

let solver_z3 = Z3.create ()

let f = Symbol.make Ty.Ty_bool "f"
 let f_false_true = Expr.app f [ Expr.value Value.False ]
 let f_false_false = Expr.unop Ty.Ty_bool Ty.Unop.Not f_false_true

let () =
  let res_z3 =
    match Z3.check solver_z3 [ f_false_true; f_false_false ] with
    | `Sat -> "sat"
    | `Unsat -> "unsat"
    | `Unknown -> "unknown"
  in
  print_endline res_z3

Thanks for bringing this to our attention!

[remigerme]

Hi, no worries at all about the delay.

Unfortunately we have yet to implemented model completion for uninterpreted functions. We're going to do it eventually. But, that is the reason you don't see a model for f yet.

Okay I see.

I'm going to open an issue to track this.

Just saw it, thanks.

Thanks again for your explanations/support!