Make (p.universo.2.7.doc.universo.solving.Solving.Solver.Make)

Parameters

module S : Utils.SMTSOLVER

Signature

Sourceval parse : Common.Files.path -> unit

parse file parses the constraint associated to file

val print_model : 
  Solving.Utils.M.cfg ->
  Utils.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.

Sourceval solve : Utils.env -> int * Utils.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.