alt-ergo/src/lib/reasoners/th_util.ml at 1924184c50b9f1aaac01ce611f8b8d7d9e8e87c9 · OCamlPro/alt-ergo · GitHub

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
(**************************************************************************)
(*                                                                        *)
(*     Alt-Ergo: The SMT Solver For Software Verification                 *)
(*     Copyright (C) 2013-2023 --- OCamlPro SAS                           *)
(*                                                                        *)
(*     This file is distributed under the terms of OCamlPro               *)
(*     Non-Commercial Purpose License, version 1.                         *)
(*                                                                        *)
(*     As an exception, Alt-Ergo Club members at the Gold level can       *)
(*     use this file under the terms of the Apache Software License       *)
(*     version 2.0.                                                       *)
(*                                                                        *)
(*     ---------------------------------------------------------------    *)
(*                                                                        *)
(*     The Alt-Ergo theorem prover                                        *)
(*                                                                        *)
(*     Sylvain Conchon, Evelyne Contejean, Francois Bobot                 *)
(*     Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout              *)
(*                                                                        *)
(*     CNRS - INRIA - Universite Paris Sud                                *)
(*                                                                        *)
(*     Until 2013, some parts of this code were released under            *)
(*     the Apache Software License version 2.0.                           *)
(*                                                                        *)
(*     ---------------------------------------------------------------    *)
(*                                                                        *)
(*     More details can be found in the directory licenses/               *)
(*                                                                        *)
(**************************************************************************)

type answer = (Explanation.t * Expr.Set.t list) option

type theory =
  | Th_arith
  | Th_sum
  | Th_adt
  | Th_arrays
  | Th_UF

let pp_theory fmt t = Fmt.string fmt @@ match t with
  | Th_arith -> "Th_arith"
  | Th_sum -> "Th_sum"
  | Th_adt -> "Th_adt"
  | Th_arrays -> "Th_arrays"
  | Th_UF -> "Th_UF"

type limit_kind =
  | Above
  | Below

type 'a optimized_split_value =
  | Minfinity
  | Pinfinity
  | Value of 'a
  | Limit of limit_kind * 'a
  | Unknown

type lit_origin =
  | Subst
  | CS of theory * Numbers.Q.t
  | NCS of theory * Numbers.Q.t
  | Other

(* TODO: use a record to document this type. *)
type case_split = Shostak.Combine.r Xliteral.view * bool * lit_origin

type optimized_split = {
  r : Shostak.Combine.r;
  e : Expr.t;
  value : Expr.t optimized_split_value;
  case_split : case_split option;
  is_max : bool;
  (** For linear arithmetic: is_max <-> (opt = maximize). *)

  order : int
  (** Ordering assigned by the user for this variable. *)
}