Project

General

Profile

Statistics
| Branch: | Revision:

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

History | View | Annotate | Download (1.07 KB)

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 f24367c4 Hans-Peter Deifel
val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> sortTable
17
            -> (string -> CoAlgFormula.sort option) ->
18
            CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool
19 c2cc0c2e Thorsten Wißmann
20
21 f24367c4 Hans-Peter Deifel
val initReasoner : CoAlgMisc.fragment_spec -> sortTable
22
                   -> (string -> CoAlgFormula.sort option) ->
23
                   CoAlgFormula.sortedFormula list
24
                   -> CoAlgFormula.sortedFormula -> unit
25 c2cc0c2e Thorsten Wißmann
26 371cb823 Hans-Peter Deifel
(** Run a single step of the reasoner. That is: Expand one node and perform sat
27 7198f96f Hans-Peter Deifel
    propagation.
28
29
    This is used in the debugger.
30 371cb823 Hans-Peter Deifel
  *)
31 c2cc0c2e Thorsten Wißmann
val runReasonerStep : unit -> unit
32 371cb823 Hans-Peter Deifel
33 c2cc0c2e Thorsten Wißmann
val reasonerFinished : unit -> bool
34
val isRootSat : unit -> bool option
35 a57eb439 Hans-Peter Deifel
36
(* vim: set et sw=2 sts=2 ts=8 : *)