package alt-ergo-lib

  1. Overview
  2. Docs

Source file sat_solver.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
(******************************************************************************)
(*                                                                            *)
(*     Alt-Ergo: The SMT Solver For Software Verification                     *)
(*     Copyright (C) 2013-2018 --- OCamlPro SAS                               *)
(*                                                                            *)
(*     This file is distributed under the terms of the license indicated      *)
(*     in the file 'License.OCamlPro'. If 'License.OCamlPro' is not           *)
(*     present, please contact us to clarify licensing.                       *)
(*                                                                            *)
(******************************************************************************)

let get_current () =
  match Options.sat_solver () with
  | Util.Tableaux | Util.Tableaux_CDCL ->
    if Options.verbose() then
      Format.eprintf "[bool reasoning] use Tableaux-like solver@.";
    (module Fun_sat : Sat_solver_sig.SatContainer)
  | Util.CDCL | Util.CDCL_Tableaux ->
    if Options.verbose() then
      Format.eprintf "[bool reasoning] use CDCL solver@.";
    (module Satml_frontend : Sat_solver_sig.SatContainer)

(*
(*+ no dynamic loading of SAT solvers anymore +*)

open Options
open Format

let current = ref (module Fun_sat : Sat_solver_sig.S)

let initialized = ref false

let set_current sat =
  if use_satml() then
    current := sat

let load_current_sat () =
  match sat_plugin () with
  | "" ->
    if debug_sat () then eprintf "[Dynlink] Using Fun_sat solver@."

  | path ->
    if debug_sat () then
      eprintf "[Dynlink] Loading the SAT-solver in %s ...@." path;
    try
      MyDynlink.loadfile path;
      if debug_sat () then  eprintf "Success !@.@."
    with
    | MyDynlink.Error m1 ->
      if debug_sat() then begin
        eprintf
          "[Dynlink] Loading the SAT-solver in plugin \"%s\" failed!@."
          path;
        Format.eprintf ">> Failure message: %s@.@."
                             (MyDynlink.error_message m1);
      end;
      let prefixed_path = sprintf "%s/%s" Config.pluginsdir path in
      if debug_sat () then
        eprintf "[Dynlink] Loading the SAT-solver in %s ... with prefix %s@."
          path Config.pluginsdir;
      try
        MyDynlink.loadfile prefixed_path;
        if debug_sat () then  eprintf "Success !@.@."
      with
      | MyDynlink.Error m2 ->
        if not (debug_sat()) then begin
          eprintf
            "[Dynlink] Loading the SAT-solver in plugin \"%s\" failed!@."
            path;
          Format.eprintf ">> Failure message: %s@.@."
            (MyDynlink.error_message m1);
        end;
        eprintf
          "[Dynlink] Trying to load the plugin from \"%s\" failed too!@."
          prefixed_path;
        Format.eprintf ">> Failure message: %s@.@."
                             (MyDynlink.error_message m2);
        exit 1

let get_current () =
  if not !initialized then
    begin
      load_current_sat ();
      initialized := true;
    end;
  !current
 *)