24/09/2020 : le runner partagé est actuellement indisponible.

constraint.ml 2.36 KB
Newer Older
1
(*-----------------------------------------------------------------------
2
** Copyright (C) 2002 - Verimag.
3 4 5 6 7 8 9 10 11 12
** This file may only be copied under the terms of the GNU Library General
** Public License 
**-----------------------------------------------------------------------
**
** File: constraint.ml
** Main author: jahier@imag.fr
*)


(* exported *)
13
type ineq = 
14 15
  | GZ      of Ne.t (** expr >  0 *)
  | GeqZ    of Ne.t (** expr >= 0 *)
16 17 18 19 20 21

(* exported *)
type t = 
  | Bv      of string (** booleans  *)
  | EqZ     of Ne.t   (** expr  = 0 *)
  | Ineq    of ineq   (** > or >= *)
22 23


24 25 26 27 28 29
(* exported *)
let (dimension_ineq : ineq -> int) =
  fun cstr -> 
    match cstr with
	GZ(ne) -> Ne.dimension ne
      | GeqZ(ne) -> Ne.dimension ne
30 31

(* exported *)
32 33 34 35
let (dimension : t -> int) =
  fun cstr -> 
    match cstr with
	Bv(_) -> 1
36
      | Ineq(ineq) -> dimension_ineq ineq
37
      | EqZ(ne) -> Ne.dimension ne
38

39 40

(* exported *)
41
let (neg_ineq : ineq -> ineq) =
42 43
  fun cstr -> 
    match cstr with
44
	GZ(ne) -> GeqZ(Ne.neg_nexpr ne)
45 46 47
      | GeqZ(ne) -> GZ(Ne.neg_nexpr ne)

(* exported *)
48
let (opp_ineq : ineq -> ineq) =
49 50
  fun cstr -> 
    match cstr with
51
	GZ(ne) -> GZ(Ne.neg_nexpr ne)
52 53 54
      | GeqZ(ne) -> GeqZ(Ne.neg_nexpr ne)


55 56 57 58 59 60 61
(* exported *)
let (apply_subst_ineq : Ne.subst -> ineq -> ineq) =
  fun s cstr -> 
    match cstr with
	GZ(ne)   -> GZ(Ne.apply_subst ne s)
      | GeqZ(ne) -> GeqZ(Ne.apply_subst ne s)

62 63 64 65 66
(* exported *)
let (apply_subst : Ne.subst -> t -> t) =
  fun s cstr -> 
    match cstr with
	Bv(_)    -> cstr
67
      | Ineq(ineq)   -> Ineq(apply_subst_ineq s ineq)
68 69
      | EqZ(ne)  -> EqZ(Ne.apply_subst ne s)

70 71 72 73 74 75 76
(* exported *)
let (apply_substl_ineq : Ne.subst list -> ineq -> ineq) =
  fun s cstr -> 
    match cstr with
	GZ(ne)   -> GZ(Ne.apply_substl s ne)
      | GeqZ(ne) -> GeqZ(Ne.apply_substl s ne)

77 78 79 80 81
(* exported *)
let (apply_substl : Ne.subst list -> t -> t) =
  fun s cstr -> 
    match cstr with
	Bv(_)    -> cstr
82
      | Ineq(ineq)   -> Ineq(apply_substl_ineq s ineq)
83 84 85
      | EqZ(ne)  -> EqZ(Ne.apply_substl s ne)


86

87
(* exported *)
88
let (ineq_to_string : ineq -> string) =
89 90 91 92
  fun f -> 
    match f with
      | GZ(ne)   -> ((Ne.to_string ne)  ^ " >  0 ")
      | GeqZ(ne) -> ((Ne.to_string ne)  ^ " >= 0 ")
93 94 95 96 97 98 99

(* exported *)
let (to_string : t -> string) =
  fun f -> 
    match f with
      | Bv(str)  -> str
      | Ineq(ineq)   -> ineq_to_string ineq
100
      | EqZ(ne)  -> ((Ne.to_string ne) ^  " = 0 ")
101