Up – Package index » universo » Library universo.solving » Solving » Z3cfg

Module `Solving.Z3cfg`Source

module type Z3LOGIC =
  Utils.LOGIC
    with type t = Z3.Expr.expr
     and type smt_model = Z3.Model.model
     and type ctx = Z3.context

Sourcemodule Make (ZL : Z3LOGIC) : Utils.SMTSOLVER

Sourcemodule Syn : Z3LOGIC

Sourcemodule Arith (S : Common.Logic.LRA_SPECIFICATION) : Z3LOGIC