module Prop_logic: sig .. end
Methods for working with propositional logic
type
the general concrete Syntax for formulas
type
the type of models for propositional logic
val empty : model
the empty models without any assignments
type model -> model
type for assignments of variables
exception Var_unbound
exception that is raised when a unbound variable is looked up
val lookup : var:string -> model -> bool
lookup an assignment for a variable in a model.
Raises Var_unbound when the variable is not bound in the model
val assign : var:string -> bool -> assignment
assign a value to a variable in a model
val combine : assignment -> assignment -> assignment
combine two assingments into one
val create : assignment list -> model
create a model from a list of assignments
val solve : formula -> model -> bool
solve a formula in a given model.
Raises Var_unbound when a variable is not bound in the model
val find_vars : formula -> string list
finds all variables that occur in a formula
val print_bool : bool -> unit
prints a single bool to stdout
val print_model : model -> unit
prints a complete model to stdout
val is_solvable : formula -> model option
Tries to find a model that satisfies the formula.
Returns Some model if there is a solution and None if there is none
val find_models : formula -> model list
Tries to find all modules in which the formula is true.
Returns a list of all models that will solve this formula