Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.mli @ de84f40d

History | View | Annotate | Download (794 Bytes)

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 -> sortTable -> (string -> CoAlgFormula.sort option) ->
17
  CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool
18

    
19

    
20
val initReasoner : sortTable -> (string -> CoAlgFormula.sort option) ->
21
  CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> unit
22

    
23
val runReasonerStep : unit -> unit
24
val reasonerFinished : unit -> bool
25
val isRootSat : unit -> bool option