src/Tools/Metis/src/Active.sig
author wenzelm
Wed, 04 Oct 2017 12:00:53 +0200
changeset 66787 64b47495676d
parent 39502 cffceed8e7fa
child 72004 913162a47d9f
permissions -rw-r--r--
obsolete;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     1
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     2
(* THE ACTIVE SET OF CLAUSES                                                 *)
39502
cffceed8e7fa fix license
blanchet
parents: 39501
diff changeset
     3
(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License            *)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     4
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     5
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     6
signature Active =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     7
sig
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     8
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     9
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    10
(* A type of active clause sets.                                             *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    11
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    12
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    13
type simplify =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    14
     {subsume : bool,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    15
      reduce : bool,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    16
      rewrite : bool}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    17
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    18
type parameters =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    19
     {clause : Clause.parameters,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    20
      prefactor : simplify,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    21
      postfactor : simplify}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    22
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    23
type active
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    24
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    25
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    26
(* Basic operations.                                                         *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    27
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    28
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    29
val default : parameters
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    30
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    31
val size : active -> int
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    32
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    33
val saturation : active -> Clause.clause list
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    34
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    35
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    36
(* Create a new active clause set and initialize clauses.                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    37
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    38
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    39
val new :
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    40
    parameters -> {axioms : Thm.thm list, conjecture : Thm.thm list} ->
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    41
    active * {axioms : Clause.clause list, conjecture : Clause.clause list}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    42
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    43
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    44
(* Add a clause into the active set and deduce all consequences.             *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    45
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    46
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    47
val add : active -> Clause.clause -> active * Clause.clause list
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    48
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    49
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    50
(* Pretty printing.                                                          *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    51
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    52
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    53
val pp : active Print.pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    54
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    55
end