Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/Matrix_LP/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 5 kB

Quelle CplexMatrixConverter.ML Sprache: SML

(*  Title:      HOL/Matrix_LP/CplexMatrixConverter.ML
    Author:     Steven Obua
*)

signature MATRIX_BUILDER =
sig
    type vector
    type matrix

    val empty_vector : vector
    val empty_matrix : matrix

    exception Nat_expected of int
    val set_elem : vector -> int -> string -> vector
    val set_vector : matrix -> int -> vector -> matrix
end;

signature CPLEX_MATRIX_CONVERTER =
sig
    structure cplex : CPLEX
    structure matrix_builder : MATRIX_BUILDER
    type vector = matrix_builder.vector
    type matrix = matrix_builder.matrix
    type naming = int * (int -> string) * (string -> int)

    exception Converter of string

    (* program must fulfill is_normed_cplexProg and must be an element of the image of elim_nonfree_bounds *)
    (* convert_prog maximize c A b naming *)
    val convert_prog : cplex.cplexProg -> bool * vector * matrix * vector * naming

    (* results must be optimal, converts_results returns the optimal value as string and the solution as vector *)
    (* convert_results results name2index *)
    val convert_results : cplex.cplexResult -> (string -> int) -> string * vector
end;

functor MAKE_CPLEX_MATRIX_CONVERTER (structure cplex: CPLEX and matrix_builder: MATRIX_BUILDER) : CPLEX_MATRIX_CONVERTER =
struct

structure cplex = cplex
structure matrix_builder = matrix_builder
type matrix = matrix_builder.matrix
type vector = matrix_builder.vector
type naming = int * (int -> string) * (string -> int)

open matrix_builder
open cplex

exception Converter of string;

fun neg_term (cplexNeg t) = t
  | neg_term (cplexSum ts) = cplexSum (map neg_term ts)
  | neg_term t = cplexNeg t

fun convert_prog (cplexProg (_, goal, constrs, bounds)) =
    let
        fun build_naming index i2s s2i [] = (index, i2s, s2i)
          | build_naming index i2s s2i (cplexBounds (cplexNeg cplexInf, cplexLeq, cplexVar v, cplexLeq, cplexInf)::bounds)
            = build_naming (index+1) (Inttab.update (index, v) i2s) (Symtab.update_new (v, index) s2i) bounds
          | build_naming _ _ _ _ = raise (Converter "nonfree bound")

        val (varcount, i2s_tab, s2i_tab) = build_naming 0 Inttab.empty Symtab.empty bounds

        fun i2s i = case Inttab.lookup i2s_tab i of NONE => raise (Converter "index not found")
                                                     | SOME n => n
        fun s2i s = case Symtab.lookup s2i_tab s of NONE => raise (Converter ("name not found: "^s))
                                                     | SOME i => i
        fun num2str positive (cplexNeg t) = num2str (not positive) t
          | num2str positive (cplexNum num) = if positive then num else "-"^num
          | num2str _ _ = raise (Converter "term is not a (possibly signed) number")

        fun setprod vec positive (cplexNeg t) = setprod vec (not positive) t
          | setprod vec positive (cplexVar v) = set_elem vec (s2i v) (if positive then "1" else "-1")
          | setprod vec positive (cplexProd (cplexNum num, cplexVar v)) =
            set_elem vec (s2i v) (if positive then num else "-"^num)
          | setprod _ _ _ = raise (Converter "term is not a normed product")

        fun sum2vec (cplexSum ts) = fold (fn t => fn vec => setprod vec true t) ts empty_vector
          | sum2vec t = setprod empty_vector true t

        fun constrs2Ab j A b [] = (A, b)
          | constrs2Ab j A b ((_, cplexConstr (cplexLeq, (t1,t2)))::cs) =
            constrs2Ab (j+1) (set_vector A j (sum2vec t1)) (set_elem b j (num2str true t2)) cs
          | constrs2Ab j A b ((_, cplexConstr (cplexGeq, (t1,t2)))::cs) =
            constrs2Ab (j+1) (set_vector A j (sum2vec (neg_term t1))) (set_elem b j (num2str true (neg_term t2))) cs
          | constrs2Ab j A b ((_, cplexConstr (cplexEq, (t1,t2)))::cs) =
            constrs2Ab j A b ((NONE, cplexConstr (cplexLeq, (t1,t2)))::
                              (NONE, cplexConstr (cplexGeq, (t1, t2)))::cs)
          | constrs2Ab _ _ _ _ = raise (Converter "no strict constraints allowed")

        val (A, b) = constrs2Ab 0 empty_matrix empty_vector constrs

        val (goal_maximize, goal_term) =
            case goal of
                (cplexMaximize t) => (true, t)
              | (cplexMinimize t) => (false, t)
    in
        (goal_maximize, sum2vec goal_term, A, b, (varcount, i2s, s2i))
    end

fun convert_results (cplex.Optimal (opt, entries)) name2index =
    let
        fun setv (name, value) v = matrix_builder.set_elem v (name2index name) value
    in
        (opt, fold setv entries (matrix_builder.empty_vector))
    end
  | convert_results _ _ = raise (Converter "No optimal result")

end;

structure SimpleMatrixBuilder : MATRIX_BUILDER =
struct
type vector = (int * string) list
type matrix = (int * vector) list

val empty_matrix = []
val empty_vector = []

exception Nat_expected of int;

fun set_elem v i s = v @ [(i, s)]

fun set_vector m i v = m @ [(i, v)]

end;

structure SimpleCplexMatrixConverter =
  MAKE_CPLEX_MATRIX_CONVERTER(structure cplex = Cplex and matrix_builder = SimpleMatrixBuilder);

quality100%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.