diff --git a/doc/Hstring.H.html b/doc/Hstring.H.html deleted file mode 100644 index 5161eb26..00000000 --- a/doc/Hstring.H.html +++ /dev/null @@ -1,25 +0,0 @@ - - - - - - - - - - - - - - -Hstring.H - - -
 Up - Next -
-

Module Hstring.H

-
-
module H: Hashtbl.S  with type key = t
Hash-tables indexed by hash-consed strings
-
- \ No newline at end of file diff --git a/doc/Hstring.HMap.html b/doc/Hstring.HMap.html deleted file mode 100644 index f2cc7f21..00000000 --- a/doc/Hstring.HMap.html +++ /dev/null @@ -1,25 +0,0 @@ - - - - - - - - - - - - - - -Hstring.HMap - - -
Previous - Up - 
-

Module Hstring.HMap

-
-
module HMap: Map.S  with type key = t
Maps indexed by hash-consed strings
-
- \ No newline at end of file diff --git a/doc/Hstring.HSet.html b/doc/Hstring.HSet.html deleted file mode 100644 index 7cd6a12a..00000000 --- a/doc/Hstring.HSet.html +++ /dev/null @@ -1,27 +0,0 @@ - - - - - - - - - - - - - - - -Hstring.HSet - - -
Previous - Up - Next -
-

Module Hstring.HSet

-
-
module HSet: Set.S  with type elt = t
Sets of hash-consed strings
-
- \ No newline at end of file diff --git a/doc/Hstring.html b/doc/Hstring.html deleted file mode 100644 index c107def9..00000000 --- a/doc/Hstring.html +++ /dev/null @@ -1,90 +0,0 @@ - - - - - - - - - - - - - - -Hstring - - -
Previous - Up - 
-

Module Hstring

-
-
module Hstring: sig .. end
Hash-consed strings -

- - Hash-consing is a technique to share values that are structurally - equal. More details on - Wikipedia and - here. -

- - This module provides an easy way to use hash-consing for strings.
-

-
type t = string Hashcons.hash_consed
-
-The type of Hash-consed string
-
- -
val make : string -> t
-make s builds ans returns a hash-consed string from s.
-
-
val view : t -> string
-view hs returns the string corresponding to hs.
-
-
val equal : t -> t -> bool
-equal x y returns true if x and y are the same hash-consed string - (constant time).
-
-
val compare : t -> t -> int
-compares x y returns 0 if x and y are equal, and is unspecified - otherwise but provides a total ordering on hash-consed strings.
-
-
val hash : t -> int
-hash x returns the integer (hash) associated to x.
-
-
val empty : t
-the empty ("") hash-consed string.
-
-
val list_assoc : t -> (t * 'a) list -> 'a
-list_assoc x l returns the element associated with x in the list of - pairs l.
-Raises Not_found if there is no value associated with x in the list l.
-
-
val list_mem_assoc : t -> (t * 'a) list -> bool
-Same as Hstring.list_assoc, but simply returns true if a binding exists, and - false if no bindings exist for the given key.
-
-
val list_mem : t -> t list -> bool
-list_mem x l is true if and only if x is equal to an element of l.
-
-
val list_mem_couple : t * t -> (t * t) list -> bool
-list_mem_couple (x,y) l is true if and only if (x,y) is equal to an - element of l.
-
-
val compare_list : t list -> t list -> int
-compare_list l1 l2 returns 0 if and only if l1 is equal to l2.
-
-
val print : Format.formatter -> t -> unit
-Prints a list of hash-consed strings on a formatter.
-
-
module H: Hashtbl.S  with type key = t
-Hash-tables indexed by hash-consed strings -
-
module HSet: Set.S  with type elt = t
-Sets of hash-consed strings -
-
module HMap: Map.S  with type key = t
-Maps indexed by hash-consed strings -
- \ No newline at end of file diff --git a/doc/Smt.Formula.html b/doc/Smt.Formula.html deleted file mode 100644 index 3fe0f295..00000000 --- a/doc/Smt.Formula.html +++ /dev/null @@ -1,135 +0,0 @@ - - - - - - - - - - - - - - - -Smt.Formula - - -
Previous - Up - Next -
-

Module Smt.Formula

-
-
module Formula: sig .. end
-
type comparator = - - - - - - - - - - - - - - - - - - - -
-| -Eq(*equality (=)*)
-| -Neq(*disequality (<>)*)
-| -Le(*inequality (<=)*)
-| -Lt(*strict inequality (<)*)
- -
-The type of comparators:
-
- -
type combinator = - - - - - - - - - - - - - - - - - - - -
-| -And(*conjunction*)
-| -Or(*disjunction*)
-| -Imp(*implication*)
-| -Not(*negation*)
- -
-The type of operators
-
- -
type t = - - - - - - - - - -
-| -Lit of Literal.LT.t
-| -Comb of combinator * t list
- -
-The type of ground formulas
-
- -
val f_true : t
-The formula which represents true
-
-
val f_false : t
-The formula which represents false
-
-
val make_lit : comparator -> Smt.Term.t list -> t
-make_lit cmp [t1; t2] creates the literal (t1 <cmp> t2).
-
-
val make : combinator -> t list -> t
-make cmb [f_1; ...; f_n] creates the formula - (f_1 <cmb> ... <cmb> f_n).
-
-
val make_cnf : t -> Literal.LT.t list list
-make_cnf f returns a conjunctive normal form of f under the form: a - list (which is a conjunction) of lists (which are disjunctions) of - literals.
-
-
val print : Format.formatter -> t -> unit
-print fmt f prints the formula on the formatter fmt.
-
- \ No newline at end of file diff --git a/doc/Smt.Make.html b/doc/Smt.Make.html deleted file mode 100644 index 3a7a58a9..00000000 --- a/doc/Smt.Make.html +++ /dev/null @@ -1,105 +0,0 @@ - - - - - - - - - - - - - - - - -Smt.Make - - -
Previous - Up - 
-

Functor Smt.Make

-
-
module Make: 
functor (Dummy : sig
end) -> Solver
Functor to create several instances of the solver
- - - - - -
Parameters: - - - - -
-Dummy:sig end -
-
-
-
-This SMT solver is imperative in the sense that it maintains a global - context. To create different instances of Alt-Ergo Zero use the - functor Smt.Make. -

- - A typical use of this solver is to do the following :

      clear ();
-      assume f_1;
-      ...
-      assume f_n;
-      check ();

-
type state
-
-The type of the internal state of the solver (see Smt.Solver.save_state and - Smt.Solver.restore_state).
-
- -
-

Profiling functions


-
val get_time : unit -> float
-get_time () returns the cumulated time spent in the solver in seconds.
-
-
val get_calls : unit -> int
-get_calls () returns the cumulated number of calls to Smt.Solver.check.
-
-
-

Main API of the solver


-
val clear : unit -> unit
-clear () clears the context of the solver. Use this after Smt.Solver.check - raised Smt.Unsat or if you want to restart the solver.
-
-
val assume : ?profiling:bool -> id:int -> Smt.Formula.t -> unit
-assume ~profiling:b f id adds the formula f to the context of the - solver with idetifier id. - This function only performs unit propagation.
-
-
profiling : if set to true then profiling information (time) will - be computed (expensive because of system calls). -

- - Raises Smt.Unsat if the context becomes inconsistent after unit - propagation.

-
val check : ?profiling:bool -> unit -> unit
-check () runs Alt-Ergo Zero on its context. If () is - returned then the context is satifiable.
-
-
profiling : if set to true then profiling information (time) will - be computed (expensive because of system calls). -

- - Raises Smt.Unsat [id_1; ...; id_n] if the context is unsatisfiable. - id_1, ..., id_n is the unsat core (returned as the identifiers of the - formulas given to the solver).

-
val save_state : unit -> state
-save_state () returns a copy of the current state of the solver.
-
-
val restore_state : state -> unit
-restore_state s restores a previously saved state s.
-
-
val entails : ?profiling:bool -> id:int -> Smt.Formula.t -> bool
-entails ~id f returns true if the context of the solver entails - the formula f. It doesn't modify the context of the solver (the state - is saved when this function is called and restored on exit).
-
- \ No newline at end of file diff --git a/doc/Smt.Solver.html b/doc/Smt.Solver.html deleted file mode 100644 index ec9ceb5e..00000000 --- a/doc/Smt.Solver.html +++ /dev/null @@ -1,88 +0,0 @@ - - - - - - - - - - - - - - - -Smt.Solver - - -
 Up - 
-

Module type Smt.Solver

-
-
module type Solver = sig .. end
-
-This SMT solver is imperative in the sense that it maintains a global - context. To create different instances of Alt-Ergo Zero use the - functor Smt.Make. -

- - A typical use of this solver is to do the following :

      clear ();
-      assume f_1;
-      ...
-      assume f_n;
-      check ();

-
type state
-
-The type of the internal state of the solver (see Smt.Solver.save_state and - Smt.Solver.restore_state).
-
- -
-

Profiling functions


-
val get_time : unit -> float
-get_time () returns the cumulated time spent in the solver in seconds.
-
-
val get_calls : unit -> int
-get_calls () returns the cumulated number of calls to Smt.Solver.check.
-
-
-

Main API of the solver


-
val clear : unit -> unit
-clear () clears the context of the solver. Use this after Smt.Solver.check - raised Smt.Unsat or if you want to restart the solver.
-
-
val assume : ?profiling:bool -> id:int -> Smt.Formula.t -> unit
-assume ~profiling:b f id adds the formula f to the context of the - solver with idetifier id. - This function only performs unit propagation.
-
-
profiling : if set to true then profiling information (time) will - be computed (expensive because of system calls). -

- - Raises Smt.Unsat if the context becomes inconsistent after unit - propagation.

-
val check : ?profiling:bool -> unit -> unit
-check () runs Alt-Ergo Zero on its context. If () is - returned then the context is satifiable.
-
-
profiling : if set to true then profiling information (time) will - be computed (expensive because of system calls). -

- - Raises Smt.Unsat [id_1; ...; id_n] if the context is unsatisfiable. - id_1, ..., id_n is the unsat core (returned as the identifiers of the - formulas given to the solver).

-
val save_state : unit -> state
-save_state () returns a copy of the current state of the solver.
-
-
val restore_state : state -> unit
-restore_state s restores a previously saved state s.
-
-
val entails : ?profiling:bool -> id:int -> Smt.Formula.t -> bool
-entails ~id f returns true if the context of the solver entails - the formula f. It doesn't modify the context of the solver (the state - is saved when this function is called and restored on exit).
-
- \ No newline at end of file diff --git a/doc/Smt.Symbol.html b/doc/Smt.Symbol.html deleted file mode 100644 index 64eea377..00000000 --- a/doc/Smt.Symbol.html +++ /dev/null @@ -1,49 +0,0 @@ - - - - - - - - - - - - - - - -Smt.Symbol - - -
Previous - Up - Next -
-

Module Smt.Symbol

-
-
module Symbol: sig .. end

Function symbols


-
-
type t = Hstring.t
-
-The type of function symbols
-
- -
val declare : Hstring.t -> Smt.Type.t list -> Smt.Type.t -> unit
-declare s [arg_1; ... ; arg_n] out declares a new function - symbol with type (arg_1, ... , arg_n) -> out
-
-
val type_of : t -> Smt.Type.t list * Smt.Type.t
-type_of x returns the type of x.
-
-
val has_abstract_type : t -> bool
-has_abstract_type x is true if the type of x is abstract.
-
-
val has_type_proc : t -> bool
-has_type_proc x is true if x has the type of a process - identifier.
-
-
val declared : t -> bool
-declared x is true if x is already declared.
-
- \ No newline at end of file diff --git a/doc/Smt.Term.html b/doc/Smt.Term.html deleted file mode 100644 index 974b7ccf..00000000 --- a/doc/Smt.Term.html +++ /dev/null @@ -1,100 +0,0 @@ - - - - - - - - - - - - - - - -Smt.Term - - -
Previous - Up - Next -
-

Module Smt.Term

-
-
module Term: sig .. end
-
type t
-
-The type of terms
-
- -
type operator = - - - - - - - - - - - - - - - - - - - - - - - - -
-| -Plus(*+*)
-| -Minus(*-*)
-| -Mult(***)
-| -Div(*/*)
-| -Modulo(*mod*)
- -
-The type of operators
-
- -
val make_int : Num.num -> t
-make_int n creates an integer constant of value n.
-
-
val make_real : Num.num -> t
-make_real n creates an real constant of value n.
-
-
val make_app : Smt.Symbol.t -> t list -> t
-make_app f l creates the application of function symbol f to a list - of terms l.
-
-
val make_arith : operator -> t -> t -> t
-make_arith op t1 t2 creates the term t1 <op> t2.
-
-
val make_ite : Smt.Formula.t -> t -> t -> t
-make_ite f t1 t2 creates the term if f then t1 else t2.
-
-
val is_int : t -> bool
-is_int x is true if the term x has type int
-
-
val is_real : t -> bool
-is_real x is true if the term x has type real
-
-
val t_true : t
-t_true is the boolean term true
-
-
val t_false : t
-t_false is the boolean term false
-
- \ No newline at end of file diff --git a/doc/Smt.Type.html b/doc/Smt.Type.html deleted file mode 100644 index 5236b200..00000000 --- a/doc/Smt.Type.html +++ /dev/null @@ -1,63 +0,0 @@ - - - - - - - - - - - - - - - - -Smt.Type - - -
 Up - Next -
-

Module Smt.Type

-
-
module Type: sig .. end

Typing


-
-
type t = Hstring.t
-
-The type of types in Alt-Ergo Zero
-
- -
-

Builtin types


-
val type_int : t
-The type of integers
-
-
val type_real : t
-The type of reals
-
-
val type_bool : t
-The type of booleans
-
-
val type_proc : t
-The type processes (identifiers)
-
-
-

Declaring new types


-
val declare : Hstring.t -> Hstring.t list -> unit
- -
-
-
val all_constructors : unit -> Hstring.t list
-all_constructors () returns a list of all the defined constructors.
-
-
val constructors : t -> Hstring.t list
-constructors ty returns the list of constructors of ty when type is - an enumerated data-type, otherwise returns [].
-
- \ No newline at end of file diff --git a/doc/Smt.Variant.html b/doc/Smt.Variant.html deleted file mode 100644 index 2f1b3f33..00000000 --- a/doc/Smt.Variant.html +++ /dev/null @@ -1,62 +0,0 @@ - - - - - - - - - - - - - - - -Smt.Variant - - -
Previous - Up - Next -
-

Module Smt.Variant

-
-
module Variant: sig .. end

Variants

 -

- - The types of symbols (when they are enumerated data types) can be refined - to substypes of their original type (i.e. a subset of their constructors).
-

-
val init : (Smt.Symbol.t * Smt.Type.t) list -> unit
-init l where l is a list of pairs (s, ty) initializes the - type (and associated constructors) of each s to its original type ty. -

- - This function must be called with a list of all symbols before - attempting to refine the types.
-

-
val close : unit -> unit
-close () will compute the smallest type possible for each symbol. -

- - This function must be called when all information has been added.
-

-
val assign_constr : Smt.Symbol.t -> Hstring.t -> unit
-assign_constr s cstr will add the constraint that the constructor - cstr must be in the type of s
-
-
val assign_var : Smt.Symbol.t -> Smt.Symbol.t -> unit
-assign_var x y will add the constraint that the type of y is a - subtype of x (use this function when x := y appear in your - program
-
-
val print : unit -> unit
-print () will output the computed refined types on std_err. This - function is here only for debugging purposes. Use it afer close ().
-
-
val get_variants : Smt.Symbol.t -> Hstring.HSet.t
-get_variants s returns a set of constructors, which is the refined - type of s.
-
- \ No newline at end of file diff --git a/doc/Smt.html b/doc/Smt.html deleted file mode 100644 index 33bee2c1..00000000 --- a/doc/Smt.html +++ /dev/null @@ -1,105 +0,0 @@ - - - - - - - - - - - - - - - - - - - -Smt - - -
 Up - Next -
-

Module Smt

-
-
module Smt: sig .. end
The Alt-Ergo Zero SMT library -

- - This SMT solver is derived from Alt-Ergo. It - uses an efficient SAT solver and supports the following quantifier free - theories:

- - This API makes heavy use of hash-consed strings. Please take a moment to - look at Hstring.
-
-
-

Error handling


-
type error = - - - - - - - - - - - - - - - - - - - -
-| -DuplicateTypeName of Hstring.t(*raised when a type is already declared*)
-| -DuplicateSymb of Hstring.t(*raised when a symbol is already declared*)
-| -UnknownType of Hstring.t(*raised when the given type is not declared*)
-| -UnknownSymb of Hstring.t(*raised when the given symbol is not declared*)
- - -
exception Error of error
-
-

Typing


-
module Type: sig .. end
-Typing -
-
module Symbol: sig .. end
-Function symbols -
-
module Variant: sig .. end
-Variants -
-
-

Building terms


-
module Term: sig .. end

-

Building formulas


-
module Formula: sig .. end

-

The SMT solver


-
exception Unsat of int list
-
-The exception raised by Smt.Solver.check and Smt.Solver.assume when - the formula is unsatisfiable.
-
-
val set_cc : bool -> unit
-set_cc false deactivates congruence closure algorithm - (true by default).
-
-
module type Solver = sig .. end
module Make: 
functor (Dummy : sig
end) -> Solver
-Functor to create several instances of the solver -
- \ No newline at end of file diff --git a/doc/index.html b/doc/index.html deleted file mode 100644 index d1837d7b..00000000 --- a/doc/index.html +++ /dev/null @@ -1,34 +0,0 @@ - - - - - - - - - - - - - - - -

-Index of types
-Index of exceptions
-Index of values
-Index of modules
-Index of module types
-

- - - -
Smt
-The Alt-Ergo Zero SMT library -
-
Hstring
-Hash-consed strings -
-
- - \ No newline at end of file diff --git a/doc/index_attributes.html b/doc/index_attributes.html deleted file mode 100644 index fb4af8f6..00000000 --- a/doc/index_attributes.html +++ /dev/null @@ -1,19 +0,0 @@ - - - - - - - - - - - -Index of class attributes - - -

Index of class attributes

- -

- - \ No newline at end of file diff --git a/doc/index_class_types.html b/doc/index_class_types.html deleted file mode 100644 index c58c17bb..00000000 --- a/doc/index_class_types.html +++ /dev/null @@ -1,19 +0,0 @@ - - - - - - - - - - - -Index of class types - - -

Index of class types

- -

- - \ No newline at end of file diff --git a/doc/index_classes.html b/doc/index_classes.html deleted file mode 100644 index 30fe9b57..00000000 --- a/doc/index_classes.html +++ /dev/null @@ -1,19 +0,0 @@ - - - - - - - - - - - -Index of classes - - -

Index of classes

- -

- - \ No newline at end of file diff --git a/doc/index_exceptions.html b/doc/index_exceptions.html deleted file mode 100644 index 50e8c67c..00000000 --- a/doc/index_exceptions.html +++ /dev/null @@ -1,29 +0,0 @@ - - - - - - - - - - - -Index of exceptions - - -

Index of exceptions

- - - - - - - -

E
Error [Smt]

U
Unsat [Smt]
-The exception raised by Smt.Solver.check and Smt.Solver.assume when - the formula is unsatisfiable. -
-

- - \ No newline at end of file diff --git a/doc/index_methods.html b/doc/index_methods.html deleted file mode 100644 index 1d9642bd..00000000 --- a/doc/index_methods.html +++ /dev/null @@ -1,19 +0,0 @@ - - - - - - - - - - - -Index of class methods - - -

Index of class methods

- -

- - \ No newline at end of file diff --git a/doc/index_module_types.html b/doc/index_module_types.html deleted file mode 100644 index 41684149..00000000 --- a/doc/index_module_types.html +++ /dev/null @@ -1,22 +0,0 @@ - - - - - - - - - - - -Index of module types - - -

Index of module types

- - - - -

S
Solver [Smt]

- - \ No newline at end of file diff --git a/doc/index_modules.html b/doc/index_modules.html deleted file mode 100644 index 27b6af52..00000000 --- a/doc/index_modules.html +++ /dev/null @@ -1,74 +0,0 @@ - - - - - - - - - - - -Index of modules - - -

Index of modules

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

F
Formula [Smt]

H
H [Hstring]
-Hash-tables indexed by hash-consed strings -
-
HMap [Hstring]
-Maps indexed by hash-consed strings -
-
HSet [Hstring]
-Sets of hash-consed strings -
-
Hstring
-Hash-consed strings -
-

M
Make [Smt]
-Functor to create several instances of the solver -
-

S
Smt
-The Alt-Ergo Zero SMT library -
-
Symbol [Smt]
-Function symbols -
-

T
Term [Smt]
Type [Smt]
-Typing -
-

V
Variant [Smt]
-Variants -
-

- - \ No newline at end of file diff --git a/doc/index_types.html b/doc/index_types.html deleted file mode 100644 index 162aa5b0..00000000 --- a/doc/index_types.html +++ /dev/null @@ -1,72 +0,0 @@ - - - - - - - - - - - -Index of types - - -

Index of types

- - - - - - - - - - - - - - - - - - - - - - - - - - -

C
combinator [Smt.Formula]
-The type of operators -
-
comparator [Smt.Formula]
-The type of comparators: -
-

E
error [Smt]

O
operator [Smt.Term]
-The type of operators -
-

S
state [Smt.Solver]
-The type of the internal state of the solver (see Smt.Solver.save_state and - Smt.Solver.restore_state). -
-

T
t [Hstring]
-The type of Hash-consed string -
-
t [Smt.Formula]
-The type of ground formulas -
-
t [Smt.Term]
-The type of terms -
-
t [Smt.Symbol]
-The type of function symbols -
-
t [Smt.Type]
-The type of types in Alt-Ergo Zero -
-

- - \ No newline at end of file diff --git a/doc/index_values.html b/doc/index_values.html deleted file mode 100644 index 4db77440..00000000 --- a/doc/index_values.html +++ /dev/null @@ -1,325 +0,0 @@ - - - - - - - - - - - -Index of values - - -

Index of values

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

A
all_constructors [Smt.Type]
-all_constructors () returns a list of all the defined constructors. -
-
assign_constr [Smt.Variant]
-assign_constr s cstr will add the constraint that the constructor - cstr must be in the type of s -
-
assign_var [Smt.Variant]
-assign_var x y will add the constraint that the type of y is a - subtype of x (use this function when x := y appear in your - program -
-
assume [Smt.Solver]
-assume ~profiling:b f id adds the formula f to the context of the - solver with idetifier id. -
-

C
check [Smt.Solver]
-check () runs Alt-Ergo Zero on its context. -
-
clear [Smt.Solver]
-clear () clears the context of the solver. -
-
close [Smt.Variant]
-close () will compute the smallest type possible for each symbol. -
-
compare [Hstring]
-compares x y returns 0 if x and y are equal, and is unspecified - otherwise but provides a total ordering on hash-consed strings. -
-
compare_list [Hstring]
-compare_list l1 l2 returns 0 if and only if l1 is equal to l2. -
-
constructors [Smt.Type]
-constructors ty returns the list of constructors of ty when type is - an enumerated data-type, otherwise returns []. -
-

D
declare [Smt.Symbol]
-declare s [arg_1; ... ; arg_n] out declares a new function - symbol with type (arg_1, ... , arg_n) -> out -
-
declare [Smt.Type]
- declare n cstrs declares a new enumerated data-type with - name n and constructors cstrs., declare n [] declares a new abstract type with name n. -
-
declared [Smt.Symbol]
-declared x is true if x is already declared. -
-

E
empty [Hstring]
-the empty ("") hash-consed string. -
-
entails [Smt.Solver]
-entails ~id f returns true if the context of the solver entails - the formula f. -
-
equal [Hstring]
-equal x y returns true if x and y are the same hash-consed string - (constant time). -
-

F
f_false [Smt.Formula]
-The formula which represents false -
-
f_true [Smt.Formula]
-The formula which represents true -
-

G
get_calls [Smt.Solver]
-get_calls () returns the cumulated number of calls to Smt.Solver.check. -
-
get_time [Smt.Solver]
-get_time () returns the cumulated time spent in the solver in seconds. -
-
get_variants [Smt.Variant]
-get_variants s returns a set of constructors, which is the refined - type of s. -
-

H
has_abstract_type [Smt.Symbol]
-has_abstract_type x is true if the type of x is abstract. -
-
has_type_proc [Smt.Symbol]
-has_type_proc x is true if x has the type of a process - identifier. -
-
hash [Hstring]
-hash x returns the integer (hash) associated to x. -
-

I
init [Smt.Variant]
-init l where l is a list of pairs (s, ty) initializes the - type (and associated constructors) of each s to its original type ty. -
-
is_int [Smt.Term]
-is_int x is true if the term x has type int -
-
is_real [Smt.Term]
-is_real x is true if the term x has type real -
-

L
list_assoc [Hstring]
-list_assoc x l returns the element associated with x in the list of - pairs l. -
-
list_mem [Hstring]
-list_mem x l is true if and only if x is equal to an element of l. -
-
list_mem_assoc [Hstring]
-Same as Hstring.list_assoc, but simply returns true if a binding exists, and - false if no bindings exist for the given key. -
-
list_mem_couple [Hstring]
-list_mem_couple (x,y) l is true if and only if (x,y) is equal to an - element of l. -
-

M
make [Hstring]
-make s builds ans returns a hash-consed string from s. -
-
make [Smt.Formula]
-make cmb [f_1; ...; f_n] creates the formula - (f_1 <cmb> ... <cmb> f_n). -
-
make_app [Smt.Term]
-make_app f l creates the application of function symbol f to a list - of terms l. -
-
make_arith [Smt.Term]
-make_arith op t1 t2 creates the term t1 <op> t2. -
-
make_cnf [Smt.Formula]
-make_cnf f returns a conjunctive normal form of f under the form: a - list (which is a conjunction) of lists (which are disjunctions) of - literals. -
-
make_int [Smt.Term]
-make_int n creates an integer constant of value n. -
-
make_ite [Smt.Term]
-make_ite f t1 t2 creates the term if f then t1 else t2. -
-
make_lit [Smt.Formula]
-make_lit cmp [t1; t2] creates the literal (t1 <cmp> t2). -
-
make_real [Smt.Term]
-make_real n creates an real constant of value n. -
-

P
print [Hstring]
-Prints a list of hash-consed strings on a formatter. -
-
print [Smt.Formula]
-print fmt f prints the formula on the formatter fmt. -
-
print [Smt.Variant]
-print () will output the computed refined types on std_err. -
-

R
restore_state [Smt.Solver]
-restore_state s restores a previously saved state s. -
-

S
save_state [Smt.Solver]
-save_state () returns a copy of the current state of the solver. -
-
set_cc [Smt]
-set_cc false deactivates congruence closure algorithm - (true by default). -
-

T
t_false [Smt.Term]
-t_false is the boolean term false -
-
t_true [Smt.Term]
-t_true is the boolean term true -
-
type_bool [Smt.Type]
-The type of booleans -
-
type_int [Smt.Type]
-The type of integers -
-
type_of [Smt.Symbol]
-type_of x returns the type of x. -
-
type_proc [Smt.Type]
-The type processes (identifiers) -
-
type_real [Smt.Type]
-The type of reals -
-

V
view [Hstring]
-view hs returns the string corresponding to hs. -
-

- - \ No newline at end of file diff --git a/doc/style.css b/doc/style.css deleted file mode 100644 index 9c84d311..00000000 --- a/doc/style.css +++ /dev/null @@ -1,34 +0,0 @@ -a:visited {color : #416DFF; text-decoration : none; } -a:link {color : #416DFF; text-decoration : none;} -a:hover {color : Red; text-decoration : none; background-color: #5FFF88} -a:active {color : Red; text-decoration : underline; } -.keyword { font-weight : bold ; color : Red } -.keywordsign { color : #C04600 } -.superscript { font-size : 4 } -.subscript { font-size : 4 } -.comment { color : Green } -.constructor { color : Blue } -.type { color : #5C6585 } -.string { color : Maroon } -.warning { color : Red ; font-weight : bold } -.info { margin-left : 3em; margin-right : 3em } -.param_info { margin-top: 4px; margin-left : 3em; margin-right : 3em } -.code { color : #465F91 ; } -h1 { font-size : 20pt ; text-align: center; } -h2 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90BDFF ;padding: 2px; } -h3 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90DDFF ;padding: 2px; } -h4 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90EDFF ;padding: 2px; } -h5 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90FDFF ;padding: 2px; } -h6 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #C0FFFF ; padding: 2px; } -div.h7 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #E0FFFF ; padding: 2px; } -div.h8 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #F0FFFF ; padding: 2px; } -div.h9 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #FFFFFF ; padding: 2px; } -.typetable { border-style : hidden } -.indextable { border-style : hidden } -.paramstable { border-style : hidden ; padding: 5pt 5pt} -body { background-color : White } -tr { background-color : White } -td.typefieldcomment { background-color : #FFFFFF ; font-size: smaller ;} -pre { margin-bottom: 4px } -div.sig_block {margin-left: 2em} -*:target { background: yellow; } \ No newline at end of file diff --git a/doc/type_Hstring.H.html b/doc/type_Hstring.H.html deleted file mode 100644 index e75ee543..00000000 --- a/doc/type_Hstring.H.html +++ /dev/null @@ -1,29 +0,0 @@ - - - - - - - - - - -Hstring.H - - -sig
-  type key = t
-  type 'a t
-  val create : int -> 'a t
-  val clear : 'a t -> unit
-  val copy : 'a t -> 'a t
-  val add : 'a t -> key -> 'a -> unit
-  val remove : 'a t -> key -> unit
-  val find : 'a t -> key -> 'a
-  val find_all : 'a t -> key -> 'a list
-  val replace : 'a t -> key -> 'a -> unit
-  val mem : 'a t -> key -> bool
-  val iter : (key -> 'a -> unit) -> 'a t -> unit
-  val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
-  val length : 'a t -> int
-end \ No newline at end of file diff --git a/doc/type_Hstring.HMap.html b/doc/type_Hstring.HMap.html deleted file mode 100644 index 11e8dbe1..00000000 --- a/doc/type_Hstring.HMap.html +++ /dev/null @@ -1,42 +0,0 @@ - - - - - - - - - - -Hstring.HMap - - -sig
-  type key = t
-  type +'a t
-  val empty : 'a t
-  val is_empty : 'a t -> bool
-  val mem : key -> 'a t -> bool
-  val add : key -> 'a -> 'a t -> 'a t
-  val singleton : key -> 'a -> 'a t
-  val remove : key -> 'a t -> 'a t
-  val merge :
-    (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
-  val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
-  val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
-  val iter : (key -> 'a -> unit) -> 'a t -> unit
-  val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
-  val for_all : (key -> 'a -> bool) -> 'a t -> bool
-  val exists : (key -> 'a -> bool) -> 'a t -> bool
-  val filter : (key -> 'a -> bool) -> 'a t -> 'a t
-  val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
-  val cardinal : 'a t -> int
-  val bindings : 'a t -> (key * 'a) list
-  val min_binding : 'a t -> key * 'a
-  val max_binding : 'a t -> key * 'a
-  val choose : 'a t -> key * 'a
-  val split : key -> 'a t -> 'a t * 'a option * 'a t
-  val find : key -> 'a t -> 'a
-  val map : ('a -> 'b) -> 'a t -> 'b t
-  val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
-end \ No newline at end of file diff --git a/doc/type_Hstring.HSet.html b/doc/type_Hstring.HSet.html deleted file mode 100644 index 5b36f864..00000000 --- a/doc/type_Hstring.HSet.html +++ /dev/null @@ -1,41 +0,0 @@ - - - - - - - - - - -Hstring.HSet - - -sig
-  type elt = t
-  type t
-  val empty : t
-  val is_empty : t -> bool
-  val mem : elt -> t -> bool
-  val add : elt -> t -> t
-  val singleton : elt -> t
-  val remove : elt -> t -> t
-  val union : t -> t -> t
-  val inter : t -> t -> t
-  val diff : t -> t -> t
-  val compare : t -> t -> int
-  val equal : t -> t -> bool
-  val subset : t -> t -> bool
-  val iter : (elt -> unit) -> t -> unit
-  val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
-  val for_all : (elt -> bool) -> t -> bool
-  val exists : (elt -> bool) -> t -> bool
-  val filter : (elt -> bool) -> t -> t
-  val partition : (elt -> bool) -> t -> t * t
-  val cardinal : t -> int
-  val elements : t -> elt list
-  val min_elt : t -> elt
-  val max_elt : t -> elt
-  val choose : t -> elt
-  val split : elt -> t -> t * bool * t
-end \ No newline at end of file diff --git a/doc/type_Hstring.html b/doc/type_Hstring.html deleted file mode 100644 index ec254215..00000000 --- a/doc/type_Hstring.html +++ /dev/null @@ -1,105 +0,0 @@ - - - - - - - - - - -Hstring - - -sig
-  type t = string Hashcons.hash_consed
-  val make : string -> Hstring.t
-  val view : Hstring.t -> string
-  val equal : Hstring.t -> Hstring.t -> bool
-  val compare : Hstring.t -> Hstring.t -> int
-  val hash : Hstring.t -> int
-  val empty : Hstring.t
-  val list_assoc : Hstring.t -> (Hstring.t * 'a) list -> 'a
-  val list_mem_assoc : Hstring.t -> (Hstring.t * 'a) list -> bool
-  val list_mem : Hstring.t -> Hstring.t list -> bool
-  val list_mem_couple :
-    Hstring.t * Hstring.t -> (Hstring.t * Hstring.t) list -> bool
-  val compare_list : Hstring.t list -> Hstring.t list -> int
-  val print : Format.formatter -> Hstring.t -> unit
-  module H :
-    sig
-      type key = t
-      type 'a t
-      val create : int -> 'a t
-      val clear : 'a t -> unit
-      val copy : 'a t -> 'a t
-      val add : 'a t -> key -> 'a -> unit
-      val remove : 'a t -> key -> unit
-      val find : 'a t -> key -> 'a
-      val find_all : 'a t -> key -> 'a list
-      val replace : 'a t -> key -> 'a -> unit
-      val mem : 'a t -> key -> bool
-      val iter : (key -> 'a -> unit) -> 'a t -> unit
-      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
-      val length : 'a t -> int
-    end
-  module HSet :
-    sig
-      type elt = t
-      type t
-      val empty : t
-      val is_empty : t -> bool
-      val mem : elt -> t -> bool
-      val add : elt -> t -> t
-      val singleton : elt -> t
-      val remove : elt -> t -> t
-      val union : t -> t -> t
-      val inter : t -> t -> t
-      val diff : t -> t -> t
-      val compare : t -> t -> int
-      val equal : t -> t -> bool
-      val subset : t -> t -> bool
-      val iter : (elt -> unit) -> t -> unit
-      val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
-      val for_all : (elt -> bool) -> t -> bool
-      val exists : (elt -> bool) -> t -> bool
-      val filter : (elt -> bool) -> t -> t
-      val partition : (elt -> bool) -> t -> t * t
-      val cardinal : t -> int
-      val elements : t -> elt list
-      val min_elt : t -> elt
-      val max_elt : t -> elt
-      val choose : t -> elt
-      val split : elt -> t -> t * bool * t
-    end
-  module HMap :
-    sig
-      type key = t
-      type +'a t
-      val empty : 'a t
-      val is_empty : 'a t -> bool
-      val mem : key -> 'a t -> bool
-      val add : key -> 'a -> 'a t -> 'a t
-      val singleton : key -> 'a -> 'a t
-      val remove : key -> 'a t -> 'a t
-      val merge :
-        (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
-      val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
-      val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
-      val iter : (key -> 'a -> unit) -> 'a t -> unit
-      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
-      val for_all : (key -> 'a -> bool) -> 'a t -> bool
-      val exists : (key -> 'a -> bool) -> 'a t -> bool
-      val filter : (key -> 'a -> bool) -> 'a t -> 'a t
-      val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
-      val cardinal : 'a t -> int
-      val bindings : 'a t -> (key * 'a) list
-      val min_binding : 'a t -> key * 'a
-      val max_binding : 'a t -> key * 'a
-      val choose : 'a t -> key * 'a
-      val split : key -> 'a t -> 'a t * 'a option * 'a t
-      val find : key -> 'a t -> 'a
-      val map : ('a -> 'b) -> 'a t -> 'b t
-      val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
-    end
-end \ No newline at end of file diff --git a/doc/type_Smt.Formula.html b/doc/type_Smt.Formula.html deleted file mode 100644 index 8a6e6004..00000000 --- a/doc/type_Smt.Formula.html +++ /dev/null @@ -1,26 +0,0 @@ - - - - - - - - - - -Smt.Formula - - -sig
-  type comparator = Eq | Neq | Le | Lt
-  type combinator = And | Or | Imp | Not
-  type t =
-      Lit of Literal.LT.t
-    | Comb of Smt.Formula.combinator * Smt.Formula.t list
-  val f_true : Smt.Formula.t
-  val f_false : Smt.Formula.t
-  val make_lit : Smt.Formula.comparator -> Smt.Term.t list -> Smt.Formula.t
-  val make : Smt.Formula.combinator -> Smt.Formula.t list -> Smt.Formula.t
-  val make_cnf : Smt.Formula.t -> Literal.LT.t list list
-  val print : Format.formatter -> Smt.Formula.t -> unit
-end \ No newline at end of file diff --git a/doc/type_Smt.Make.html b/doc/type_Smt.Make.html deleted file mode 100644 index 0d7c496d..00000000 --- a/doc/type_Smt.Make.html +++ /dev/null @@ -1,14 +0,0 @@ - - - - - - - - - - -Smt.Make - - -functor (Dummy : sig  end) -> Solver \ No newline at end of file diff --git a/doc/type_Smt.Solver.html b/doc/type_Smt.Solver.html deleted file mode 100644 index 26a75e1a..00000000 --- a/doc/type_Smt.Solver.html +++ /dev/null @@ -1,24 +0,0 @@ - - - - - - - - - - -Smt.Solver - - -sig
-  type state
-  val get_time : unit -> float
-  val get_calls : unit -> int
-  val clear : unit -> unit
-  val assume : ?profiling:bool -> id:int -> Smt.Formula.t -> unit
-  val check : ?profiling:bool -> unit -> unit
-  val save_state : unit -> Smt.Solver.state
-  val restore_state : Smt.Solver.state -> unit
-  val entails : ?profiling:bool -> id:int -> Smt.Formula.t -> bool
-end \ No newline at end of file diff --git a/doc/type_Smt.Symbol.html b/doc/type_Smt.Symbol.html deleted file mode 100644 index dcd06375..00000000 --- a/doc/type_Smt.Symbol.html +++ /dev/null @@ -1,21 +0,0 @@ - - - - - - - - - - -Smt.Symbol - - -sig
-  type t = Hstring.t
-  val declare : Hstring.t -> Smt.Type.t list -> Smt.Type.t -> unit
-  val type_of : Smt.Symbol.t -> Smt.Type.t list * Smt.Type.t
-  val has_abstract_type : Smt.Symbol.t -> bool
-  val has_type_proc : Smt.Symbol.t -> bool
-  val declared : Smt.Symbol.t -> bool
-end \ No newline at end of file diff --git a/doc/type_Smt.Term.html b/doc/type_Smt.Term.html deleted file mode 100644 index e6a41971..00000000 --- a/doc/type_Smt.Term.html +++ /dev/null @@ -1,27 +0,0 @@ - - - - - - - - - - -Smt.Term - - -sig
-  type t
-  type operator = Plus | Minus | Mult | Div | Modulo
-  val make_int : Num.num -> Smt.Term.t
-  val make_real : Num.num -> Smt.Term.t
-  val make_app : Smt.Symbol.t -> Smt.Term.t list -> Smt.Term.t
-  val make_arith :
-    Smt.Term.operator -> Smt.Term.t -> Smt.Term.t -> Smt.Term.t
-  val make_ite : Smt.Formula.t -> Smt.Term.t -> Smt.Term.t -> Smt.Term.t
-  val is_int : Smt.Term.t -> bool
-  val is_real : Smt.Term.t -> bool
-  val t_true : Smt.Term.t
-  val t_false : Smt.Term.t
-end \ No newline at end of file diff --git a/doc/type_Smt.Type.html b/doc/type_Smt.Type.html deleted file mode 100644 index d14a5a63..00000000 --- a/doc/type_Smt.Type.html +++ /dev/null @@ -1,23 +0,0 @@ - - - - - - - - - - -Smt.Type - - -sig
-  type t = Hstring.t
-  val type_int : Smt.Type.t
-  val type_real : Smt.Type.t
-  val type_bool : Smt.Type.t
-  val type_proc : Smt.Type.t
-  val declare : Hstring.t -> Hstring.t list -> unit
-  val all_constructors : unit -> Hstring.t list
-  val constructors : Smt.Type.t -> Hstring.t list
-end \ No newline at end of file diff --git a/doc/type_Smt.Variant.html b/doc/type_Smt.Variant.html deleted file mode 100644 index 5736af72..00000000 --- a/doc/type_Smt.Variant.html +++ /dev/null @@ -1,21 +0,0 @@ - - - - - - - - - - -Smt.Variant - - -sig
-  val init : (Smt.Symbol.t * Smt.Type.t) list -> unit
-  val close : unit -> unit
-  val assign_constr : Smt.Symbol.t -> Hstring.t -> unit
-  val assign_var : Smt.Symbol.t -> Smt.Symbol.t -> unit
-  val print : unit -> unit
-  val get_variants : Smt.Symbol.t -> Hstring.HSet.t
-end \ No newline at end of file diff --git a/doc/type_Smt.html b/doc/type_Smt.html deleted file mode 100644 index 3b6f4362..00000000 --- a/doc/type_Smt.html +++ /dev/null @@ -1,96 +0,0 @@ - - - - - - - - - - -Smt - - -sig
-  type error =
-      DuplicateTypeName of Hstring.t
-    | DuplicateSymb of Hstring.t
-    | UnknownType of Hstring.t
-    | UnknownSymb of Hstring.t
-  exception Error of Smt.error
-  module Type :
-    sig
-      type t = Hstring.t
-      val type_int : Smt.Type.t
-      val type_real : Smt.Type.t
-      val type_bool : Smt.Type.t
-      val type_proc : Smt.Type.t
-      val declare : Hstring.t -> Hstring.t list -> unit
-      val all_constructors : unit -> Hstring.t list
-      val constructors : Smt.Type.t -> Hstring.t list
-    end
-  module Symbol :
-    sig
-      type t = Hstring.t
-      val declare : Hstring.t -> Smt.Type.t list -> Smt.Type.t -> unit
-      val type_of : Smt.Symbol.t -> Smt.Type.t list * Smt.Type.t
-      val has_abstract_type : Smt.Symbol.t -> bool
-      val has_type_proc : Smt.Symbol.t -> bool
-      val declared : Smt.Symbol.t -> bool
-    end
-  module Variant :
-    sig
-      val init : (Smt.Symbol.t * Smt.Type.t) list -> unit
-      val close : unit -> unit
-      val assign_constr : Smt.Symbol.t -> Hstring.t -> unit
-      val assign_var : Smt.Symbol.t -> Smt.Symbol.t -> unit
-      val print : unit -> unit
-      val get_variants : Smt.Symbol.t -> Hstring.HSet.t
-    end
-  module rec Term :
-    sig
-      type t
-      type operator = Plus | Minus | Mult | Div | Modulo
-      val make_int : Num.num -> Smt.Term.t
-      val make_real : Num.num -> Smt.Term.t
-      val make_app : Smt.Symbol.t -> Smt.Term.t list -> Smt.Term.t
-      val make_arith :
-        Smt.Term.operator -> Smt.Term.t -> Smt.Term.t -> Smt.Term.t
-      val make_ite : Smt.Formula.t -> Smt.Term.t -> Smt.Term.t -> Smt.Term.t
-      val is_int : Smt.Term.t -> bool
-      val is_real : Smt.Term.t -> bool
-      val t_true : Smt.Term.t
-      val t_false : Smt.Term.t
-    end
-  and Formula :
-    sig
-      type comparator = Eq | Neq | Le | Lt
-      type combinator = And | Or | Imp | Not
-      type t =
-          Lit of Literal.LT.t
-        | Comb of Smt.Formula.combinator * Smt.Formula.t list
-      val f_true : Smt.Formula.t
-      val f_false : Smt.Formula.t
-      val make_lit :
-        Smt.Formula.comparator -> Smt.Term.t list -> Smt.Formula.t
-      val make :
-        Smt.Formula.combinator -> Smt.Formula.t list -> Smt.Formula.t
-      val make_cnf : Smt.Formula.t -> Literal.LT.t list list
-      val print : Format.formatter -> Smt.Formula.t -> unit
-    end
-  exception Unsat of int list
-  val set_cc : bool -> unit
-  module type Solver =
-    sig
-      type state
-      val get_time : unit -> float
-      val get_calls : unit -> int
-      val clear : unit -> unit
-      val assume : ?profiling:bool -> id:int -> Smt.Formula.t -> unit
-      val check : ?profiling:bool -> unit -> unit
-      val save_state : unit -> Smt.Solver.state
-      val restore_state : Smt.Solver.state -> unit
-      val entails : ?profiling:bool -> id:int -> Smt.Formula.t -> bool
-    end
-  module Make : functor (Dummy : sig  end) -> Solver
-end \ No newline at end of file diff --git a/msat.mlpack b/msat.mlpack index b4591901..54b4d70b 100644 --- a/msat.mlpack +++ b/msat.mlpack @@ -3,3 +3,20 @@ Formula_intf Solver Solver_types Theory_intf + +#Arith +#Cc +#Combine +#Exception +#Fm +#Intervals +#Literal +#Polynome +#Smt +#Sum +#Symbols +#Term +#Ty +#Uf +#Use + diff --git a/msat.odocl b/msat.odocl index 87ca5a83..22b5db30 100644 --- a/msat.odocl +++ b/msat.odocl @@ -4,19 +4,19 @@ sat/Solver sat/Solver_types sat/Theory_intf -smt/Arith -smt/Cc -smt/Combine -smt/Exception -smt/Fm -smt/Intervals -smt/Literal -smt/Polynome -smt/Smt -smt/Sum -smt/Symbols -smt/Term -smt/Ty -smt/Uf -smt/Use +#smt/Arith +#smt/Cc +#smt/Combine +#smt/Exception +#smt/Fm +#smt/Intervals +#smt/Literal +#smt/Polynome +#smt/Smt +#smt/Sum +#smt/Symbols +#smt/Term +#smt/Ty +#smt/Uf +#smt/Use