Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.mli @ de84f40d

History | View | Annotate | Download (794 Bytes)

1 4fd28192 Thorsten Wißmann
(** 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 c78c1ce0 Thorsten Wißmann
type nomTable = string -> CoAlgFormula.sort option
9
10
type assumptions = CoAlgFormula.sortedFormula list
11
12
type input = sortTable * nomTable * assumptions * CoAlgFormula.sortedFormula
13 4fd28192 Thorsten Wißmann
14 f335015f Thorsten Wißmann
exception ReasonerError of string
15
16 4fd28192 Thorsten Wißmann
val isSat : ?verbose:bool -> sortTable -> (string -> CoAlgFormula.sort option) ->
17
  CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool
18 c2cc0c2e Thorsten Wißmann
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