--- a/src/Tools/Metis/src/Formula.sig Mon Sep 13 16:44:20 2010 +0200
+++ b/src/Tools/Metis/src/Formula.sig Mon Sep 13 21:24:10 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC FORMULAS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Formula =
@@ -34,6 +34,10 @@
val isBoolean : formula -> bool
+val isTrue : formula -> bool
+
+val isFalse : formula -> bool
+
(* Functions *)
val functions : formula -> NameAritySet.set
@@ -92,6 +96,8 @@
val listMkForall : Term.var list * formula -> formula
+val setMkForall : NameSet.set * formula -> formula
+
val stripForall : formula -> Term.var list * formula
(* Existential quantification *)
@@ -102,6 +108,8 @@
val listMkExists : Term.var list * formula -> formula
+val setMkExists : NameSet.set * formula -> formula
+
val stripExists : formula -> Term.var list * formula
(* ------------------------------------------------------------------------- *)
@@ -116,6 +124,8 @@
val compare : formula * formula -> order
+val equal : formula -> formula -> bool
+
(* ------------------------------------------------------------------------- *)
(* Free variables. *)
(* ------------------------------------------------------------------------- *)
@@ -124,6 +134,8 @@
val freeVars : formula -> NameSet.set
+val freeVarsList : formula list -> NameSet.set
+
val specialize : formula -> formula
val generalize : formula -> formula
@@ -163,12 +175,18 @@
val rhs : formula -> Term.term
(* ------------------------------------------------------------------------- *)
+(* Splitting goals. *)
+(* ------------------------------------------------------------------------- *)
+
+val splitGoal : formula -> formula list
+
+(* ------------------------------------------------------------------------- *)
(* Parsing and pretty-printing. *)
(* ------------------------------------------------------------------------- *)
-type quotation = formula Parser.quotation
+type quotation = formula Parse.quotation
-val pp : formula Parser.pp
+val pp : formula Print.pp
val toString : formula -> string