Source file `smtSolve.ml`

1
2
3
4
5
6
7
8
# 1 "src/lib/yices2/smtSolveDummy.ml"
(** {b Requires [yices2]} Process an evaluated AST in order to solve
    it with Yices2. *)

let ast_to_yices _ = failwith "Yices2 not available, recompile with Yices2"
let string_of_model ?value_sep _ _ = failwith "Yices2 not available, recompile with Yices2"
let solve _ _ = failwith "Yices2 not available, recompile with Yices2"
let logic_supported _ = failwith "Yices2 not available, recompile with Yices2"
let enabled = false