package universo

  1. Overview
  2. Docs

Generic solver for Universo

val parse : Common.Files.path -> unit

parse file parses the constraint associated to file

val print_model : M.cfg -> model -> Common.Files.path list -> unit

print_model meta model file prints the model into the solution file associated to file. Universes are translated to terms via the meta rules.

val solve : env -> int * model

solve env solves all the files parsed and returns a model as long as i, the number of universes needed. As postconditions, i >= env.minimum && i <= maximum. Moreover forall j < i, the solver did not found a solution.