ctl/wrapper_ctl.mli

   1 (*
   2  * Copyright 2012, INRIA
   3  * Julia Lawall, Gilles Muller
   4  * Copyright 2010-2011, INRIA, University of Copenhagen
   5  * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
   6  * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
   7  * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
   8  * This file is part of Coccinelle.
   9  *
  10  * Coccinelle is free software: you can redistribute it and/or modify
  11  * it under the terms of the GNU General Public License as published by
  12  * the Free Software Foundation, according to version 2 of the License.
  13  *
  14  * Coccinelle is distributed in the hope that it will be useful,
  15  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  16  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  17  * GNU General Public License for more details.
  18  *
  19  * You should have received a copy of the GNU General Public License
  20  * along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
  21  *
  22  * The authors reserve the right to distribute this or future versions of
  23  * Coccinelle under other licenses.
  24  *)
  25
  26
  27 type info = int
  28
  29 type ('pred, 'mvar) wrapped_ctl =
  30     ('pred * 'mvar Ast_ctl.modif,  'mvar, info) Ast_ctl.generic_ctl
  31
  32 type ('a, 'b) wrapped_binding =
  33     ClassicVal of 'a
  34   | PredVal of 'b Ast_ctl.modif
  35
  36 type ('pred,'state,'mvar,'value) labelfunc =
  37     'pred ->
  38       ('state * ('pred * ('mvar, 'value) Ast_ctl.generic_substitution))  list
  39
  40 module CTL_ENGINE_BIS :
  41   functor (SUB : Ctl_engine.SUBST) ->
  42     functor (G : Ctl_engine.GRAPH) ->
  43       functor(P : Ctl_engine.PREDICATE) ->
  44   sig
  45
  46     type predicate = P.t
  47     module WRAPPER_ENV :
  48         sig
  49           type mvar = SUB.mvar
  50           type value = (SUB.value, predicate) wrapped_binding
  51         end
  52     module WRAPPER_PRED :
  53         sig
  54           type t = P.t * SUB.mvar Ast_ctl.modif
  55         end
  56     module WRAPPER_ENGINE :
  57         sig
  58           type substitution =
  59               (WRAPPER_ENV.mvar, WRAPPER_ENV.value) Ast_ctl.generic_subst list
  60           type ('a, 'b) witness =
  61               (G.node, substitution,
  62                ('a, WRAPPER_ENV.mvar, 'b) Ast_ctl.generic_ctl list)
  63                 Ast_ctl.generic_witnesstree
  64           type ('a, 'b) triples =
  65               (G.node * substitution * ('a, 'b) witness list) list
  66         end
  67
  68
  69     val satbis_noclean :
  70         G.cfg *
  71         (predicate, G.node, WRAPPER_ENV.mvar, SUB.value) labelfunc *
  72         G.node list ->
  73           ((WRAPPER_PRED.t, WRAPPER_ENV.mvar, int) Ast_ctl.generic_ctl *
  74              (WRAPPER_PRED.t list list)) ->
  75                (WRAPPER_PRED.t, 'a) WRAPPER_ENGINE.triples
  76
  77     val satbis :
  78         G.cfg *
  79          (predicate,G.node,SUB.mvar,SUB.value) labelfunc *
  80          G.node list ->
  81            ((predicate,SUB.mvar) wrapped_ctl *
  82               (WRAPPER_PRED.t list list)) ->
  83                 (WRAPPER_ENV.mvar list * (SUB.mvar * SUB.value) list) ->
  84                   ((WRAPPER_PRED.t, 'a) WRAPPER_ENGINE.triples *
  85                      ((G.node * (SUB.mvar * SUB.value) list * predicate)
  86                         list list *
  87                         bool *
  88                         (WRAPPER_ENV.mvar * SUB.value) list list))
  89
  90     val print_bench : unit -> unit
  91 end