simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

add todo

Browse source
This commit is contained in:
Simon Cruanes 2022-10-23 20:58:25 -04:00
parent 651f2c1150
commit f5ccbb476b
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smtlib/Driver.ml
View file

@ -69,7 +69,10 @@ let decl_fun (self : t) f args ret const : unit =
let build_model (self : t) (sat : Solver.sat_result) : Model.t = let build_model (self : t) (sat : Solver.sat_result) : Model.t =
Build_model.build self.build_model sat Build_model.build self.build_model sat
let check_model (self : t) (m : Model.t) : unit = assert false (* FIXME *)
let check_model (_self : t) (_m : Model.t) : unit =
Log.debugf 0 (fun k -> k "; TODO: check model");
()
(* call the solver to check satisfiability *) (* call the solver to check satisfiability *)
let solve (self : t) ~assumptions () : Solver.res = let solve (self : t) ~assumptions () : Solver.res =