From 631e18e1f4b677695f42a30ac0e1fd483e90ce30 Mon Sep 17 00:00:00 2001
From: Benedikt Becker <benedikt.becker@inria.fr>
Date: Mon, 24 Feb 2020 14:20:04 +0100
Subject: [PATCH] fixup! Clean interface for module Colis

---
 src/colis.ml  | 18 ++++++++++--------
 src/colis.mli |  7 +++++--
 2 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/src/colis.ml b/src/colis.ml
index ec403c5e..1b46bc1f 100644
--- a/src/colis.ml
+++ b/src/colis.ml
@@ -115,11 +115,13 @@ end
 
 module FilesystemSpec = FilesystemSpec
 
+module Constraints = Colis_constraints
+
 module SymbolicConstraints = struct
-  open SymbolicUtility
-  open SymbolicUtility.Constraints
+  include SymbolicUtility.Constraints
 
   let () =
+    let open SymbolicUtility in
     List.iter Mixed.register [
       (module Basics.True) ;
       (module Basics.Colon) ;
@@ -146,7 +148,7 @@ module SymbolicConstraints = struct
 
   let add_fs_spec_to_clause root clause fs_spec =
     let fs_clause = FilesystemSpec.compile root fs_spec in
-    Colis_constraints.Clause.add_to_sat_conj fs_clause clause
+    Constraints.Clause.add_to_sat_conj fs_clause clause
 
   let to_state ~prune_init_state ~root clause : state =
     let open SymbolicUtility.Constraints in
@@ -171,13 +173,13 @@ module SymbolicConstraints = struct
         let stack_size = Finite (Z.of_int stack_size) in
         { loop_limit; stack_size } in
       Input.({ argument0; config; under_condition=false }) in
-    Mixed.interp_program_constraints inp stas' program
+    SymbolicUtility.Mixed.interp_program_constraints inp stas' program
 
   let print_dot filename id clause =
     let ch = open_out filename in
     try
       let fmt = formatter_of_out_channel ch in
-      Colis_constraints.Clause.pp_sat_conj_as_dot ~name:id fmt clause;
+      Constraints.Clause.pp_sat_conj_as_dot ~name:id fmt clause;
       close_out ch
     with e ->
       close_out ch;
@@ -190,7 +192,7 @@ module SymbolicConstraints = struct
   }
 
   let print_filesystem fmt fs =
-    let open Colis_constraints in
+    let open Constraints in
     let open SymbolicUtility.Constraints in
     fprintf fmt "root: %a@\n" Var.pp fs.root;
     fprintf fmt "clause: %a@\n" Clause.pp_sat_conj fs.clause
@@ -265,8 +267,8 @@ module SymbolicConstraints = struct
       exit 0
 
   let run config fs_spec ~argument0 ?(arguments=[]) ?(vars=[]) colis =
-    let root = Colis_constraints.Var.fresh ~hint:"r" () in
-    let disj = add_fs_spec_to_clause root Colis_constraints.Clause.true_sat_conj fs_spec in
+    let root = Constraints.Var.fresh ~hint:"r" () in
+    let disj = add_fs_spec_to_clause root Constraints.Clause.true_sat_conj fs_spec in
     let stas = List.map (to_state ~prune_init_state:config.prune_init_state ~root) disj in
     let stas' = List.map (to_symbolic_state ~vars ~arguments) stas in
     let results =
diff --git a/src/colis.mli b/src/colis.mli
index f2d89b02..07285505 100644
--- a/src/colis.mli
+++ b/src/colis.mli
@@ -96,10 +96,13 @@ end
 (** Specification of the initial filesystem *)
 module FilesystemSpec = FilesystemSpec
 
+module Constraints = Colis_constraints
+
 (** The symbolic interpreter using constraints *)
 module SymbolicConstraints : sig
-  open Colis_constraints
-  open SymbolicUtility.Constraints
+  open Constraints
+
+  include module type of SymbolicUtility.Constraints
 
   (** [compile_fs_spec root conj fs_spec] creates a disjunction that represents the conjunction [conj] with constraints representing the filesystem specified by [fs_spec] *)
   val add_fs_spec_to_clause : Var.t -> Clause.sat_conj -> FilesystemSpec.t -> Clause.sat_conj list