Skip to content

Commit

Permalink
Update simple_smt, fix SMT counterexample production
Browse files Browse the repository at this point in the history
Credit to @klausnat in #318
  • Loading branch information
NatKarmios committed Dec 3, 2024
1 parent 8e95e0c commit 6532631
Show file tree
Hide file tree
Showing 4 changed files with 16 additions and 7 deletions.
8 changes: 7 additions & 1 deletion GillianCore/engine/FOLogic/FOSolver.ml
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,13 @@ let check_satisfiability_with_model (fs : Formula.t list) (gamma : Type_env.t) :
try
Smt.lift_model model (Type_env.as_hashtbl gamma) update smt_vars;
Some subst
with _ -> None)
with e ->
let () =
L.verbose (fun m ->
m "Error when attempting to get SMT model: %s"
(Printexc.to_string e))
in
None)

let check_satisfiability
?(matching = false)
Expand Down
11 changes: 7 additions & 4 deletions GillianCore/smt/smt.ml
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ exception SMT_unknown

let pp_sexp = Sexplib.Sexp.pp_hum
let init_decls : sexp list ref = ref []
let builtin_funcs : sexp list ref = ref []

let sanitize_identifier =
let pattern = Str.regexp "#" in
Expand Down Expand Up @@ -159,7 +160,7 @@ let mk_datatype name type_params (variants : (module Variant.S) list) =

let mk_fun_decl name param_types result_type =
let decl = declare_fun name param_types result_type in
let () = init_decls := decl :: !init_decls in
let () = builtin_funcs := decl :: !builtin_funcs in
atom name

module Type_operations = struct
Expand Down Expand Up @@ -989,7 +990,8 @@ let exec_sat' (fs : Formula.Set.t) (gamma : typenv) : sexp option =
in
let encoded_assertions = encode_assertions fs gamma in
let () = if !Config.dump_smt then Dump.dump fs gamma encoded_assertions in
let () = encoded_assertions |> List.iter (fun a -> cmd a) in
let () = List.iter cmd !builtin_funcs in
let () = List.iter cmd encoded_assertions in
L.verbose (fun fmt -> fmt "Reached SMT.");
let result = check solver in
L.verbose (fun m ->
Expand Down Expand Up @@ -1061,12 +1063,13 @@ let lift_model
(gamma : typenv)
(subst_update : string -> Expr.t -> unit)
(target_vars : Expr.Set.t) : unit =
let model_eval = (model_eval z3 model).eval [] in
let () = reset_solver () in
let model_eval = (model_eval' solver model).eval [] in

let get_val x =
try
let x = x |> sanitize_identifier |> atom in
model_eval (atom "get-value" <| x) |> Option.some
model_eval x |> Option.some
with UnexpectedSolverResponse _ -> None
in

Expand Down
2 changes: 1 addition & 1 deletion gillian.opam
Original file line number Diff line number Diff line change
Expand Up @@ -44,5 +44,5 @@ build: [
]
dev-repo: "git+https://github.com/GillianPlatform/Gillian.git"
pin-depends: [
"simple_smt.~dev" "git+https://github.com/NatKarmios/simple-smt-ocaml#b88c4b0685f6ec989e8b4c911e296c4087768db8"
"simple_smt.~dev" "git+https://github.com/NatKarmios/simple-smt-ocaml#94a891e7fb552ecaff57bbe5b9f4e4e5c1aed145"
]
2 changes: 1 addition & 1 deletion gillian.opam.template
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
pin-depends: [
"simple_smt.~dev" "git+https://github.com/NatKarmios/simple-smt-ocaml#b88c4b0685f6ec989e8b4c911e296c4087768db8"
"simple_smt.~dev" "git+https://github.com/NatKarmios/simple-smt-ocaml#94a891e7fb552ecaff57bbe5b9f4e4e5c1aed145"
]

0 comments on commit 6532631

Please sign in to comment.