search

ghulette / ocaml-smtlib

An OCaml API for working with SMTLIB2
MIT License
0 stars 0 forks source link

Add support for reading functions returned via `get-model` #2

Closed ghulette closed 4 years ago

ghulette commented 4 years ago 
open Easy_smt.Smtlib
open Smtlib_test

let test solv =
  declare_fun solv (Id "int_of_bool") [bool_sort] int_sort;
  assert_ solv (equals (App (Id "int_of_bool", [bool_to_term false])) (int_to_term 0));
  assert_ solv (equals (App (Id "int_of_bool", [bool_to_term true])) (int_to_term 1))

let () =
  run_test test

Right now the parser cannot parse the result from Z3, which looks like

sat
(model 
  (define-fun int_of_bool ((x!0 Bool)) Int
    (ite (= x!0 true) 1
      0))
  (define-fun bool_of_int ((x!0 Int)) Bool
    (= x!0 0))
)