blob: 8b2ee349ed989298b7af8caebd8ea0062b6faac3 (
plain) (
tree)
|
|
open Ast
open Formula
module type ENVIRONMENT_DOMAIN = sig
type t
(* construction *)
val init : t
val bottom : t
val is_bot : t -> bool
(* variable management *)
val addvar : t -> id -> bool -> t (* integer or float variable ? *)
val forgetvar : t -> id -> t (* remove var from constraints *)
val rmvar : t -> id -> t
val vars : t -> (id * bool) list
val vbottom : t -> t (* bottom value with same environment *)
(* set-theoretic operations *)
val join : t -> t -> t (* union *)
val meet : t -> t -> t (* intersection *)
val widen : t -> t -> t
(* order *)
val subset : t -> t -> bool
val eq : t -> t -> bool
(* abstract operation *)
val apply_f : t -> bool_expr -> t
val apply_cl : t -> conslist -> t
val assign : t -> (id * num_expr) list -> t
(* pretty-printing *)
val print_vars : Format.formatter -> t -> id list -> unit
val print_all : Format.formatter -> t -> unit
end
|
