Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.mli @ 1d36cd07

History | View | Annotate | Download (1.07 KB)

1
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
2
    @author Florian Widmann
3
 *)
4

    
5

    
6
type sortTable = (CoAlgMisc.functors * int list) array
7

    
8
type nomTable = string -> CoAlgFormula.sort option
9

    
10
type assumptions = CoAlgFormula.sortedFormula list
11

    
12
type input = sortTable * nomTable * assumptions * CoAlgFormula.sortedFormula
13

    
14
exception ReasonerError of string
15

    
16
val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> sortTable
17
            -> (string -> CoAlgFormula.sort option) ->
18
            CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool
19

    
20

    
21
val initReasoner : CoAlgMisc.fragment_spec -> sortTable
22
                   -> (string -> CoAlgFormula.sort option) ->
23
                   CoAlgFormula.sortedFormula list
24
                   -> CoAlgFormula.sortedFormula -> unit
25

    
26
(** Run a single step of the reasoner. That is: Expand one node and perform sat
27
    propagation.
28

    
29
    This is used in the debugger.
30
  *)
31
val runReasonerStep : unit -> unit
32

    
33
val reasonerFinished : unit -> bool
34
val isRootSat : unit -> bool option
35

    
36
(* vim: set et sw=2 sts=2 ts=8 : *)