Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/HOL/Tools/Nitpick/   (Beweissystem Isabelle Version 2025-1©)  Datei vom 16.11.2025 mit Größe 40 kB image not shown  

Quelle  kodkod.ML   Sprache: SML

 
(*  Title:      HOL/Tools/Nitpick/kodkod.ML
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2008-2014

ML interface for Kodkod.
*)

signature KODKOD =
sig
  type n_ary_index = int * int
  type setting = string * string

  datatype tuple =
    Tuple of int list |
    TupleIndex of n_ary_index |
    TupleReg of n_ary_index

  datatype tuple_set =
    TupleUnion of tuple_set * tuple_set |
    TupleDifference of tuple_set * tuple_set |
    TupleIntersect of tuple_set * tuple_set |
    TupleProduct of tuple_set * tuple_set |
    TupleProject of tuple_set * int |
    TupleSet of tuple list |
    TupleRange of tuple * tuple |
    TupleArea of tuple * tuple |
    TupleAtomSeq of int * int |
    TupleSetReg of n_ary_index

  datatype tuple_assign =
    AssignTuple of n_ary_index * tuple |
    AssignTupleSet of n_ary_index * tuple_set

  type bound = (n_ary_index * string) list * tuple_set list
  type int_bound = int option * tuple_set list

  datatype formula =
    All of decl list * formula |
    Exist of decl list * formula |
    FormulaLet of expr_assign list * formula |
    FormulaIf of formula * formula * formula |
    Or of formula * formula |
    Iff of formula * formula |
    Implies of formula * formula |
    And of formula * formula |
    Not of formula |
    Acyclic of n_ary_index |
    Function of n_ary_index * rel_expr * rel_expr |
    Functional of n_ary_index * rel_expr * rel_expr |
    TotalOrdering of n_ary_index * rel_expr * rel_expr * rel_expr |
    Subset of rel_expr * rel_expr |
    RelEq of rel_expr * rel_expr |
    IntEq of int_expr * int_expr |
    LT of int_expr * int_expr |
    LE of int_expr * int_expr |
    No of rel_expr |
    Lone of rel_expr |
    One of rel_expr |
    Some of rel_expr |
    False |
    True |
    FormulaReg of int
  and rel_expr =
    RelLet of expr_assign list * rel_expr |
    RelIf of formula * rel_expr * rel_expr |
    Union of rel_expr * rel_expr |
    Difference of rel_expr * rel_expr |
    Override of rel_expr * rel_expr |
    Intersect of rel_expr * rel_expr |
    Product of rel_expr * rel_expr |
    IfNo of rel_expr * rel_expr |
    Project of rel_expr * int_expr list |
    Join of rel_expr * rel_expr |
    Closure of rel_expr |
    ReflexiveClosure of rel_expr |
    Transpose of rel_expr |
    Comprehension of decl list * formula |
    Bits of int_expr |
    Int of int_expr |
    Iden |
    Ints |
    None |
    Univ |
    Atom of int |
    AtomSeq of int * int |
    Rel of n_ary_index |
    Var of n_ary_index |
    RelReg of n_ary_index
  and int_expr =
    Sum of decl list * int_expr |
    IntLet of expr_assign list * int_expr |
    IntIf of formula * int_expr * int_expr |
    SHL of int_expr * int_expr |
    SHA of int_expr * int_expr |
    SHR of int_expr * int_expr |
    Add of int_expr * int_expr |
    Sub of int_expr * int_expr |
    Mult of int_expr * int_expr |
    Div of int_expr * int_expr |
    Mod of int_expr * int_expr |
    Cardinality of rel_expr |
    SetSum of rel_expr |
    BitOr of int_expr * int_expr |
    BitXor of int_expr * int_expr |
    BitAnd of int_expr * int_expr |
    BitNot of int_expr |
    Neg of int_expr |
    Absolute of int_expr |
    Signum of int_expr |
    Num of int |
    IntReg of int
  and decl =
    DeclNo of n_ary_index * rel_expr |
    DeclLone of n_ary_index * rel_expr |
    DeclOne of n_ary_index * rel_expr |
    DeclSome of n_ary_index * rel_expr |
    DeclSet of n_ary_index * rel_expr
  and expr_assign =
    AssignFormulaReg of int * formula |
    AssignRelReg of n_ary_index * rel_expr |
    AssignIntReg of int * int_expr

  type 'a fold_expr_funcs =
    {formula_func: formula -> 'a -> 'a,
     rel_expr_func: rel_expr -> 'a -> 'a,
     int_expr_func: int_expr -> 'a -> 'a}

  val fold_formula : 'a fold_expr_funcs -> formula -> 'a -> 'a
  val fold_rel_expr : 'a fold_expr_funcs -> rel_expr -> 'a -> 'a
  val fold_int_expr : 'a fold_expr_funcs -> int_expr -> 'a -> 'a
  val fold_decl : 'a fold_expr_funcs -> decl -> 'a -> 'a
  val fold_expr_assign : 'a fold_expr_funcs -> expr_assign -> 'a -> 'a

  type 'a fold_tuple_funcs =
    {tuple_func: tuple -> 'a -> 'a,
     tuple_set_func: tuple_set -> 'a -> 'a}

  val fold_tuple : 'a fold_tuple_funcs -> tuple -> 'a -> 'a
  val fold_tuple_set : 'a fold_tuple_funcs -> tuple_set -> 'a -> 'a
  val fold_tuple_assign : 'a fold_tuple_funcs -> tuple_assign -> 'a -> 'a
  val fold_bound :
      'a fold_expr_funcs -> 'a fold_tuple_funcs -> bound -> 'a -> 'a
  val fold_int_bound : 'a fold_tuple_funcs -> int_bound -> 'a -> 'a

  type problem =
    {comment: string,
     settings: setting list,
     univ_card: int,
     tuple_assigns: tuple_assign list,
     bounds: bound list,
     int_bounds: int_bound list,
     expr_assigns: expr_assign list,
     formula: formula}

  type raw_bound = n_ary_index * int list list

  datatype outcome =
    Normal of (int * raw_bound list) list * int list * string |
    TimedOut of int list |
    Error of string * int list

  exception SYNTAX of string * string

  val max_arity : int -> int
  val arity_of_rel_expr : rel_expr -> int
  val is_problem_trivially_false : problem -> bool
  val problems_equivalent : problem * problem -> bool
  val solve_any_problem :
    bool -> bool -> bool -> Time.time -> int -> int -> problem list -> outcome
  val kodkod_scala : bool Config.T
end;

structure Kodkod : KODKOD =
struct

type n_ary_index = int * int

type setting = string * string

datatype tuple =
  Tuple of int list |
  TupleIndex of n_ary_index |
  TupleReg of n_ary_index

datatype tuple_set =
  TupleUnion of tuple_set * tuple_set |
  TupleDifference of tuple_set * tuple_set |
  TupleIntersect of tuple_set * tuple_set |
  TupleProduct of tuple_set * tuple_set |
  TupleProject of tuple_set * int |
  TupleSet of tuple list |
  TupleRange of tuple * tuple |
  TupleArea of tuple * tuple |
  TupleAtomSeq of int * int |
  TupleSetReg of n_ary_index

datatype tuple_assign =
  AssignTuple of n_ary_index * tuple |
  AssignTupleSet of n_ary_index * tuple_set

type bound = (n_ary_index * string) list * tuple_set list
type int_bound = int option * tuple_set list

datatype formula =
  All of decl list * formula |
  Exist of decl list * formula |
  FormulaLet of expr_assign list * formula |
  FormulaIf of formula * formula * formula |
  Or of formula * formula |
  Iff of formula * formula |
  Implies of formula * formula |
  And of formula * formula |
  Not of formula |
  Acyclic of n_ary_index |
  Function of n_ary_index * rel_expr * rel_expr |
  Functional of n_ary_index * rel_expr * rel_expr |
  TotalOrdering of n_ary_index * rel_expr * rel_expr * rel_expr |
  Subset of rel_expr * rel_expr |
  RelEq of rel_expr * rel_expr |
  IntEq of int_expr * int_expr |
  LT of int_expr * int_expr |
  LE of int_expr * int_expr |
  No of rel_expr |
  Lone of rel_expr |
  One of rel_expr |
  Some of rel_expr |
  False |
  True |
  FormulaReg of int
and rel_expr =
  RelLet of expr_assign list * rel_expr |
  RelIf of formula * rel_expr * rel_expr |
  Union of rel_expr * rel_expr |
  Difference of rel_expr * rel_expr |
  Override of rel_expr * rel_expr |
  Intersect of rel_expr * rel_expr |
  Product of rel_expr * rel_expr |
  IfNo of rel_expr * rel_expr |
  Project of rel_expr * int_expr list |
  Join of rel_expr * rel_expr |
  Closure of rel_expr |
  ReflexiveClosure of rel_expr |
  Transpose of rel_expr |
  Comprehension of decl list * formula |
  Bits of int_expr |
  Int of int_expr |
  Iden |
  Ints |
  None |
  Univ |
  Atom of int |
  AtomSeq of int * int |
  Rel of n_ary_index |
  Var of n_ary_index |
  RelReg of n_ary_index
and int_expr =
  Sum of decl list * int_expr |
  IntLet of expr_assign list * int_expr |
  IntIf of formula * int_expr * int_expr |
  SHL of int_expr * int_expr |
  SHA of int_expr * int_expr |
  SHR of int_expr * int_expr |
  Add of int_expr * int_expr |
  Sub of int_expr * int_expr |
  Mult of int_expr * int_expr |
  Div of int_expr * int_expr |
  Mod of int_expr * int_expr |
  Cardinality of rel_expr |
  SetSum of rel_expr |
  BitOr of int_expr * int_expr |
  BitXor of int_expr * int_expr |
  BitAnd of int_expr * int_expr |
  BitNot of int_expr |
  Neg of int_expr |
  Absolute of int_expr |
  Signum of int_expr |
  Num of int |
  IntReg of int
and decl =
  DeclNo of n_ary_index * rel_expr |
  DeclLone of n_ary_index * rel_expr |
  DeclOne of n_ary_index * rel_expr |
  DeclSome of n_ary_index * rel_expr |
  DeclSet of n_ary_index * rel_expr
and expr_assign =
  AssignFormulaReg of int * formula |
  AssignRelReg of n_ary_index * rel_expr |
  AssignIntReg of int * int_expr

type problem =
  {comment: string,
   settings: setting list,
   univ_card: int,
   tuple_assigns: tuple_assign list,
   bounds: bound list,
   int_bounds: int_bound list,
   expr_assigns: expr_assign list,
   formula: formula}

type raw_bound = n_ary_index * int list list

datatype outcome =
  Normal of (int * raw_bound list) list * int list * string |
  TimedOut of int list |
  Error of string * int list

exception SYNTAX of string * string

type 'a fold_expr_funcs =
  {formula_func: formula -> 'a -> 'a,
   rel_expr_func: rel_expr -> 'a -> 'a,
   int_expr_func: int_expr -> 'a -> 'a}


(** Auxiliary functions on Kodkod problems **)

fun fold_formula (F : 'a fold_expr_funcs) formula =
  case formula of
    All (ds, f) => fold (fold_decl F) ds #> fold_formula F f
  | Exist (ds, f) => fold (fold_decl F) ds #> fold_formula F f
  | FormulaLet (bs, f) => fold (fold_expr_assign F) bs #> fold_formula F f
  | FormulaIf (f, f1, f2) =>
    fold_formula F f #> fold_formula F f1 #> fold_formula F f2
  | Or (f1, f2) => fold_formula F f1 #> fold_formula F f2
  | Iff (f1, f2) => fold_formula F f1 #> fold_formula F f2
  | Implies (f1, f2) => fold_formula F f1 #> fold_formula F f2
  | And (f1, f2) => fold_formula F f1 #> fold_formula F f2
  | Not f => fold_formula F f
  | Acyclic x => fold_rel_expr F (Rel x)
  | Function (x, r1, r2) =>
    fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2
  | Functional (x, r1, r2) =>
    fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2
  | TotalOrdering (x, r1, r2, r3) =>
    fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2
    #> fold_rel_expr F r3
  | Subset (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
  | RelEq (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
  | IntEq (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | LT (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | LE (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | No r => fold_rel_expr F r
  | Lone r => fold_rel_expr F r
  | One r => fold_rel_expr F r
  | Some r => fold_rel_expr F r
  | False => #formula_func F formula
  | True => #formula_func F formula
  | FormulaReg _ => #formula_func F formula
and fold_rel_expr F rel_expr =
  case rel_expr of
    RelLet (bs, r) => fold (fold_expr_assign F) bs #> fold_rel_expr F r
  | RelIf (f, r1, r2) =>
    fold_formula F f #> fold_rel_expr F r1 #> fold_rel_expr F r2
  | Union (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
  | Difference (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
  | Override (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
  | Intersect (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
  | Product (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
  | IfNo (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
  | Project (r1, is) => fold_rel_expr F r1 #> fold (fold_int_expr F) is
  | Join (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
  | Closure r => fold_rel_expr F r
  | ReflexiveClosure r => fold_rel_expr F r
  | Transpose r => fold_rel_expr F r
  | Comprehension (ds, f) => fold (fold_decl F) ds #> fold_formula F f
  | Bits i => fold_int_expr F i
  | Int i => fold_int_expr F i
  | Iden => #rel_expr_func F rel_expr
  | Ints => #rel_expr_func F rel_expr
  | None => #rel_expr_func F rel_expr
  | Univ => #rel_expr_func F rel_expr
  | Atom _ => #rel_expr_func F rel_expr
  | AtomSeq _ => #rel_expr_func F rel_expr
  | Rel _ => #rel_expr_func F rel_expr
  | Var _ => #rel_expr_func F rel_expr
  | RelReg _ => #rel_expr_func F rel_expr
and fold_int_expr F int_expr =
  case int_expr of
    Sum (ds, i) => fold (fold_decl F) ds #> fold_int_expr F i
  | IntLet (bs, i) => fold (fold_expr_assign F) bs #> fold_int_expr F i
  | IntIf (f, i1, i2) =>
    fold_formula F f #> fold_int_expr F i1 #> fold_int_expr F i2
  | SHL (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | SHA (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | SHR (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | Add (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | Sub (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | Mult (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | Div (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | Mod (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | Cardinality r => fold_rel_expr F r
  | SetSum r => fold_rel_expr F r
  | BitOr (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | BitXor (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | BitAnd (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | BitNot i => fold_int_expr F i
  | Neg i => fold_int_expr F i
  | Absolute i => fold_int_expr F i
  | Signum i => fold_int_expr F i
  | Num _ => #int_expr_func F int_expr
  | IntReg _ => #int_expr_func F int_expr
and fold_decl F decl =
  case decl of
    DeclNo (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
  | DeclLone (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
  | DeclOne (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
  | DeclSome (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
  | DeclSet (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
and fold_expr_assign F assign =
  case assign of
    AssignFormulaReg (x, f) => fold_formula F (FormulaReg x) #> fold_formula F f
  | AssignRelReg (x, r) => fold_rel_expr F (RelReg x) #> fold_rel_expr F r
  | AssignIntReg (x, i) => fold_int_expr F (IntReg x) #> fold_int_expr F i

type 'a fold_tuple_funcs =
  {tuple_func: tuple -> 'a -> 'a,
   tuple_set_func: tuple_set -> 'a -> 'a}

fun fold_tuple (F : 'a fold_tuple_funcs) = #tuple_func F

fun fold_tuple_set F tuple_set =
  case tuple_set of
    TupleUnion (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
  | TupleDifference (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
  | TupleIntersect (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
  | TupleProduct (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
  | TupleProject (ts, _) => fold_tuple_set F ts
  | TupleSet ts => fold (fold_tuple F) ts
  | TupleRange (t1, t2) => fold_tuple F t1 #> fold_tuple F t2
  | TupleArea (t1, t2) => fold_tuple F t1 #> fold_tuple F t2
  | TupleAtomSeq _ => #tuple_set_func F tuple_set
  | TupleSetReg _ => #tuple_set_func F tuple_set

fun fold_tuple_assign F assign =
  case assign of
    AssignTuple (x, t) => fold_tuple F (TupleReg x) #> fold_tuple F t
  | AssignTupleSet (x, ts) =>
    fold_tuple_set F (TupleSetReg x) #> fold_tuple_set F ts

fun fold_bound expr_F tuple_F (zs, tss) =
  fold (fold_rel_expr expr_F) (map (Rel o fst) zs)
  #> fold (fold_tuple_set tuple_F) tss

fun fold_int_bound F (_, tss) = fold (fold_tuple_set F) tss

fun max_arity univ_card = floor (Math.ln 2147483647.0
                                 / Math.ln (Real.fromInt univ_card))

fun arity_of_rel_expr (RelLet (_, r)) = arity_of_rel_expr r
  | arity_of_rel_expr (RelIf (_, r1, _)) = arity_of_rel_expr r1
  | arity_of_rel_expr (Union (r1, _)) = arity_of_rel_expr r1
  | arity_of_rel_expr (Difference (r1, _)) = arity_of_rel_expr r1
  | arity_of_rel_expr (Override (r1, _)) = arity_of_rel_expr r1
  | arity_of_rel_expr (Intersect (r1, _)) = arity_of_rel_expr r1
  | arity_of_rel_expr (Product (r1, r2)) = sum_arities_of_rel_exprs r1 r2
  | arity_of_rel_expr (IfNo (r1, _)) = arity_of_rel_expr r1
  | arity_of_rel_expr (Project (_, is)) = length is
  | arity_of_rel_expr (Join (r1, r2)) = sum_arities_of_rel_exprs r1 r2 - 2
  | arity_of_rel_expr (Closure _) = 2
  | arity_of_rel_expr (ReflexiveClosure _) = 2
  | arity_of_rel_expr (Transpose _) = 2
  | arity_of_rel_expr (Comprehension (ds, _)) =
    fold (curry op + o arity_of_decl) ds 0
  | arity_of_rel_expr (Bits _) = 1
  | arity_of_rel_expr (Int _) = 1
  | arity_of_rel_expr Iden = 2
  | arity_of_rel_expr Ints = 1
  | arity_of_rel_expr None = 1
  | arity_of_rel_expr Univ = 1
  | arity_of_rel_expr (Atom _) = 1
  | arity_of_rel_expr (AtomSeq _) = 1
  | arity_of_rel_expr (Rel (n, _)) = n
  | arity_of_rel_expr (Var (n, _)) = n
  | arity_of_rel_expr (RelReg (n, _)) = n
and sum_arities_of_rel_exprs r1 r2 = arity_of_rel_expr r1 + arity_of_rel_expr r2
and arity_of_decl (DeclNo ((n, _), _)) = n
  | arity_of_decl (DeclLone ((n, _), _)) = n
  | arity_of_decl (DeclOne ((n, _), _)) = n
  | arity_of_decl (DeclSome ((n, _), _)) = n
  | arity_of_decl (DeclSet ((n, _), _)) = n

fun is_problem_trivially_false ({formula = False, ...} : problem) = true
  | is_problem_trivially_false _ = false

val chop_solver = take 2 o space_explode ","

fun settings_equivalent ([], []) = true
  | settings_equivalent ((key1, value1) :: settings1,
                         (key2, value2) :: settings2) =
    key1 = key2 andalso
    (value1 = value2 orelse key1 = "delay" orelse
     (key1 = "solver" andalso chop_solver value1 = chop_solver value2)) andalso
    settings_equivalent (settings1, settings2)
  | settings_equivalent _ = false

fun problems_equivalent (p1 : problem, p2 : problem) =
  #univ_card p1 = #univ_card p2 andalso
  #formula p1 = #formula p2 andalso
  #bounds p1 = #bounds p2 andalso
  #expr_assigns p1 = #expr_assigns p2 andalso
  #tuple_assigns p1 = #tuple_assigns p2 andalso
  #int_bounds p1 = #int_bounds p2 andalso
  settings_equivalent (#settings p1, #settings p2)

(** Serialization of problem **)

fun base_name j =
  if j < 0 then string_of_int (~j - 1) ^ "'" else string_of_int j

fun n_ary_name (1, j) prefix _ _ = prefix ^ base_name j
  | n_ary_name (2, j) _ prefix _ = prefix ^ base_name j
  | n_ary_name (n, j) _ _ prefix = prefix ^ string_of_int n ^ "_" ^ base_name j

fun atom_name j = "A" ^ base_name j
fun atom_seq_name (k, 0) = "u" ^ base_name k
  | atom_seq_name (k, j0) = "u" ^ base_name k ^ "@" ^ base_name j0
fun formula_reg_name j = "$f" ^ base_name j
fun rel_reg_name j = "$e" ^ base_name j
fun int_reg_name j = "$i" ^ base_name j

fun tuple_name x = n_ary_name x "A" "P" "T"
fun rel_name x = n_ary_name x "s" "r" "m"
fun var_name x = n_ary_name x "S" "R" "M"
fun tuple_reg_name x = n_ary_name x "$A" "$P" "$T"
fun tuple_set_reg_name x = n_ary_name x "$a" "$p" "$t"

fun inline_comment "" = ""
  | inline_comment comment =
    " /* " ^ translate_string (fn "\n" => " " | "*" => "* " | s => s) comment ^
    " */"

fun block_comment "" = ""
  | block_comment comment = prefix_lines "// " comment ^ "\n"

fun commented_rel_name (x, s) = rel_name x ^ inline_comment s

fun string_for_tuple (Tuple js) = "[" ^ commas (map atom_name js) ^ "]"
  | string_for_tuple (TupleIndex x) = tuple_name x
  | string_for_tuple (TupleReg x) = tuple_reg_name x

val no_prec = 100
val prec_TupleUnion = 1
val prec_TupleIntersect = 2
val prec_TupleProduct = 3
val prec_TupleProject = 4

fun precedence_ts (TupleUnion _) = prec_TupleUnion
  | precedence_ts (TupleDifference _) = prec_TupleUnion
  | precedence_ts (TupleIntersect _) = prec_TupleIntersect
  | precedence_ts (TupleProduct _) = prec_TupleProduct
  | precedence_ts (TupleProject _) = prec_TupleProject
  | precedence_ts _ = no_prec

fun string_for_tuple_set tuple_set =
  let
    fun sub tuple_set outer_prec =
      let
        val prec = precedence_ts tuple_set
        val need_parens = (prec < outer_prec)
      in
        (if need_parens then "(" else "") ^
        (case tuple_set of
           TupleUnion (ts1, ts2) => sub ts1 prec ^ " + " ^ sub ts2 (prec + 1)
         | TupleDifference (ts1, ts2) =>
           sub ts1 prec ^ " - " ^ sub ts2 (prec + 1)
         | TupleIntersect (ts1, ts2) => sub ts1 prec ^ " & " ^ sub ts2 prec
         | TupleProduct (ts1, ts2) => sub ts1 prec ^ "->" ^ sub ts2 prec
         | TupleProject (ts, c) => sub ts prec ^ "[" ^ string_of_int c ^ "]"
         | TupleSet ts => "{" ^ commas (map string_for_tuple ts) ^ "}"
         | TupleRange (t1, t2) =>
           "{" ^ string_for_tuple t1 ^
           (if t1 = t2 then "" else " .. " ^ string_for_tuple t2) ^ "}"
         | TupleArea (t1, t2) =>
           "{" ^ string_for_tuple t1 ^ " # " ^ string_for_tuple t2 ^ "}"
         | TupleAtomSeq x => atom_seq_name x
         | TupleSetReg x => tuple_set_reg_name x) ^
        (if need_parens then ")" else "")
      end
  in sub tuple_set 0 end

fun string_for_tuple_assign (AssignTuple (x, t)) =
    tuple_reg_name x ^ " := " ^ string_for_tuple t ^ "\n"
  | string_for_tuple_assign (AssignTupleSet (x, ts)) =
    tuple_set_reg_name x ^ " := " ^ string_for_tuple_set ts ^ "\n"

fun string_for_bound (zs, tss) =
  "bounds " ^ commas (map commented_rel_name zs) ^ ": " ^
  (if length tss = 1 then "" else "[") ^ commas (map string_for_tuple_set tss) ^
  (if length tss = 1 then "" else "]") ^ "\n"

fun int_string_for_bound (opt_n, tss) =
  (case opt_n of
     SOME n => signed_string_of_int n ^ ": "
   | NONE => "") ^ "[" ^ commas (map string_for_tuple_set tss) ^ "]"

val prec_All = 1
val prec_Or = 2
val prec_Iff = 3
val prec_Implies = 4
val prec_And = 5
val prec_Not = 6
val prec_Eq = 7
val prec_Some = 8
val prec_SHL = 9
val prec_Add = 10
val prec_Mult = 11
val prec_Override = 12
val prec_Intersect = 13
val prec_Product = 14
val prec_IfNo = 15
val prec_Project = 17
val prec_Join = 18
val prec_BitNot = 19

fun precedence_f (All _) = prec_All
  | precedence_f (Exist _) = prec_All
  | precedence_f (FormulaLet _) = prec_All
  | precedence_f (FormulaIf _) = prec_All
  | precedence_f (Or _) = prec_Or
  | precedence_f (Iff _) = prec_Iff
  | precedence_f (Implies _) = prec_Implies
  | precedence_f (And _) = prec_And
  | precedence_f (Not _) = prec_Not
  | precedence_f (Acyclic _) = no_prec
  | precedence_f (Function _) = no_prec
  | precedence_f (Functional _) = no_prec
  | precedence_f (TotalOrdering _) = no_prec
  | precedence_f (Subset _) = prec_Eq
  | precedence_f (RelEq _) = prec_Eq
  | precedence_f (IntEq _) = prec_Eq
  | precedence_f (LT _) = prec_Eq
  | precedence_f (LE _) = prec_Eq
  | precedence_f (No _) = prec_Some
  | precedence_f (Lone _) = prec_Some
  | precedence_f (One _) = prec_Some
  | precedence_f (Some _) = prec_Some
  | precedence_f False = no_prec
  | precedence_f True = no_prec
  | precedence_f (FormulaReg _) = no_prec
and precedence_r (RelLet _) = prec_All
  | precedence_r (RelIf _) = prec_All
  | precedence_r (Union _) = prec_Add
  | precedence_r (Difference _) = prec_Add
  | precedence_r (Override _) = prec_Override
  | precedence_r (Intersect _) = prec_Intersect
  | precedence_r (Product _) = prec_Product
  | precedence_r (IfNo _) = prec_IfNo
  | precedence_r (Project _) = prec_Project
  | precedence_r (Join _) = prec_Join
  | precedence_r (Closure _) = prec_BitNot
  | precedence_r (ReflexiveClosure _) = prec_BitNot
  | precedence_r (Transpose _) = prec_BitNot
  | precedence_r (Comprehension _) = no_prec
  | precedence_r (Bits _) = no_prec
  | precedence_r (Int _) = no_prec
  | precedence_r Iden = no_prec
  | precedence_r Ints = no_prec
  | precedence_r None = no_prec
  | precedence_r Univ = no_prec
  | precedence_r (Atom _) = no_prec
  | precedence_r (AtomSeq _) = no_prec
  | precedence_r (Rel _) = no_prec
  | precedence_r (Var _) = no_prec
  | precedence_r (RelReg _) = no_prec
and precedence_i (Sum _) = prec_All
  | precedence_i (IntLet _) = prec_All
  | precedence_i (IntIf _) = prec_All
  | precedence_i (SHL _) = prec_SHL
  | precedence_i (SHA _) = prec_SHL
  | precedence_i (SHR _) = prec_SHL
  | precedence_i (Add _) = prec_Add
  | precedence_i (Sub _) = prec_Add
  | precedence_i (Mult _) = prec_Mult
  | precedence_i (Div _) = prec_Mult
  | precedence_i (Mod _) = prec_Mult
  | precedence_i (Cardinality _) = no_prec
  | precedence_i (SetSum _) = no_prec
  | precedence_i (BitOr _) = prec_Intersect
  | precedence_i (BitXor _) = prec_Intersect
  | precedence_i (BitAnd _) = prec_Intersect
  | precedence_i (BitNot _) = prec_BitNot
  | precedence_i (Neg _) = prec_BitNot
  | precedence_i (Absolute _) = prec_BitNot
  | precedence_i (Signum _) = prec_BitNot
  | precedence_i (Num _) = no_prec
  | precedence_i (IntReg _) = no_prec

fun write_problem out problems =
  let
    fun out_outmost_f (And (f1, f2)) =
        (out_outmost_f f1; out "\n && "; out_outmost_f f2)
      | out_outmost_f f = out_f f prec_And
    and out_f formula outer_prec =
      let
        val prec = precedence_f formula
        val need_parens = (prec < outer_prec)
      in
        (if need_parens then out "(" else ());
        (case formula of
           All (ds, f) => (out "all ["; out_decls ds; out "] | "; out_f f prec)
         | Exist (ds, f) =>
           (out "some ["; out_decls ds; out "] | "; out_f f prec)
         | FormulaLet (bs, f) =>
           (out "let ["; out_assigns bs; out "] | "; out_f f prec)
         | FormulaIf (f, f1, f2) =>
           (out "if "; out_f f prec; out " then "; out_f f1 prec; out " else ";
            out_f f2 prec)
         | Or (f1, f2) => (out_f f1 prec; out " || "; out_f f2 prec)
         | Iff (f1, f2) => (out_f f1 prec; out " <=> "; out_f f2 prec)
         | Implies (f1, f2) => (out_f f1 (prec + 1); out " => "; out_f f2 prec)
         | And (f1, f2) => (out_f f1 prec; out " && "; out_f f2 prec)
         | Not f => (out "! "; out_f f prec)
         | Acyclic x => out ("ACYCLIC(" ^ rel_name x ^ ")")
         | Function (x, r1, r2) =>
           (out ("FUNCTION(" ^ rel_name x ^ ", "); out_r r1 0; out " -> one ";
            out_r r2 0; out ")")
         | Functional (x, r1, r2) =>
           (out ("FUNCTION(" ^ rel_name x ^ ", "); out_r r1 0; out " -> lone ";
            out_r r2 0; out ")")
         | TotalOrdering (x, r1, r2, r3) =>
           (out ("TOTAL_ORDERING(" ^ rel_name x ^ ", "); out_r r1 0; out ", ";
            out_r r2 0; out ", "; out_r r3 0; out ")")
         | Subset (r1, r2) => (out_r r1 prec; out " in "; out_r r2 prec)
         | RelEq (r1, r2) => (out_r r1 prec; out " = "; out_r r2 prec)
         | IntEq (i1, i2) => (out_i i1 prec; out " = "; out_i i2 prec)
         | LT (i1, i2) => (out_i i1 prec; out " < "; out_i i2 prec)
         | LE (i1, i2) => (out_i i1 prec; out " <= "; out_i i2 prec)
         | No r => (out "no "; out_r r prec)
         | Lone r => (out "lone "; out_r r prec)
         | One r => (out "one "; out_r r prec)
         | Some r => (out "some "; out_r r prec)
         | False => out "false"
         | True => out "true"
         | FormulaReg j => out (formula_reg_name j));
        (if need_parens then out ")" else ())
      end
    and out_r rel_expr outer_prec =
      let
        val prec = precedence_r rel_expr
        val need_parens = (prec < outer_prec)
      in
        (if need_parens then out "(" else ());
        (case rel_expr of
           RelLet (bs, r) =>
           (out "let ["; out_assigns bs; out "] | "; out_r r prec)
         | RelIf (f, r1, r2) =>
           (out "if "; out_f f prec; out " then "; out_r r1 prec;
            out " else "; out_r r2 prec)
         | Union (r1, r2) => (out_r r1 prec; out " + "; out_r r2 (prec + 1))
         | Difference (r1, r2) =>
           (out_r r1 prec; out " - "; out_r r2 (prec + 1))
         | Override (r1, r2) => (out_r r1 prec; out " ++ "; out_r r2 prec)
         | Intersect (r1, r2) => (out_r r1 prec; out " & "; out_r r2 prec)
         | Product (r1, r2) => (out_r r1 prec; out "->"; out_r r2 prec)
         | IfNo (r1, r2) => (out_r r1 prec; out "\\"; out_r r2 prec)
         | Project (r1, is) => (out_r r1 prec; out "["; out_columns is; out "]")
         | Join (r1, r2) => (out_r r1 prec; out "."; out_r r2 (prec + 1))
         | Closure r => (out "^"; out_r r prec)
         | ReflexiveClosure r => (out "*"; out_r r prec)
         | Transpose r => (out "~"; out_r r prec)
         | Comprehension (ds, f) =>
           (out "{["; out_decls ds; out "] | "; out_f f 0; out "}")
         | Bits i => (out "Bits["; out_i i 0; out "]")
         | Int i => (out "Int["; out_i i 0; out "]")
         | Iden => out "iden"
         | Ints => out "ints"
         | None => out "none"
         | Univ => out "univ"
         | Atom j => out (atom_name j)
         | AtomSeq x => out (atom_seq_name x)
         | Rel x => out (rel_name x)
         | Var x => out (var_name x)
         | RelReg (_, j) => out (rel_reg_name j));
        (if need_parens then out ")" else ())
      end
    and out_i int_expr outer_prec =
      let
        val prec = precedence_i int_expr
        val need_parens = (prec < outer_prec)
      in
        (if need_parens then out "(" else ());
        (case int_expr of
           Sum (ds, i) => (out "sum ["; out_decls ds; out "] | "; out_i i prec)
         | IntLet (bs, i) =>
           (out "let ["; out_assigns bs; out "] | "; out_i i prec)
         | IntIf (f, i1, i2) =>
           (out "if "; out_f f prec; out " then "; out_i i1 prec;
            out " else "; out_i i2 prec)
         | SHL (i1, i2) => (out_i i1 prec; out " << "; out_i i2 (prec + 1))
         | SHA (i1, i2) => (out_i i1 prec; out " >> "; out_i i2 (prec + 1))
         | SHR (i1, i2) => (out_i i1 prec; out " >>> "; out_i i2 (prec + 1))
         | Add (i1, i2) => (out_i i1 prec; out " + "; out_i i2 (prec + 1))
         | Sub (i1, i2) => (out_i i1 prec; out " - "; out_i i2 (prec + 1))
         | Mult (i1, i2) => (out_i i1 prec; out " * "; out_i i2 (prec + 1))
         | Div (i1, i2) => (out_i i1 prec; out " / "; out_i i2 (prec + 1))
         | Mod (i1, i2) => (out_i i1 prec; out " % "; out_i i2 (prec + 1))
         | Cardinality r => (out "#("; out_r r 0; out ")")
         | SetSum r => (out "sum("; out_r r 0; out ")")
         | BitOr (i1, i2) => (out_i i1 prec; out " | "; out_i i2 prec)
         | BitXor (i1, i2) => (out_i i1 prec; out " ^ "; out_i i2 prec)
         | BitAnd (i1, i2) => (out_i i1 prec; out " & "; out_i i2 prec)
         | BitNot i => (out "~"; out_i i prec)
         | Neg i => (out "-"; out_i i prec)
         | Absolute i => (out "abs "; out_i i prec)
         | Signum i => (out "sgn "; out_i i prec)
         | Num k => out (signed_string_of_int k)
         | IntReg j => out (int_reg_name j));
        (if need_parens then out ")" else ())
      end
    and out_decls [] = ()
      | out_decls [d] = out_decl d
      | out_decls (d :: ds) = (out_decl d; out ", "; out_decls ds)
    and out_decl (DeclNo (x, r)) =
        (out (var_name x); out " : no "; out_r r 0)
      | out_decl (DeclLone (x, r)) =
        (out (var_name x); out " : lone "; out_r r 0)
      | out_decl (DeclOne (x, r)) =
        (out (var_name x); out " : one "; out_r r 0)
      | out_decl (DeclSome (x, r)) =
        (out (var_name x); out " : some "; out_r r 0)
      | out_decl (DeclSet (x, r)) =
        (out (var_name x); out " : set "; out_r r 0)
    and out_assigns [] = ()
      | out_assigns [b] = out_assign b
      | out_assigns (b :: bs) = (out_assign b; out ", "; out_assigns bs)
    and out_assign (AssignFormulaReg (j, f)) =
        (out (formula_reg_name j); out " := "; out_f f 0)
      | out_assign (AssignRelReg ((_, j), r)) =
        (out (rel_reg_name j); out " := "; out_r r 0)
      | out_assign (AssignIntReg (j, i)) =
        (out (int_reg_name j); out " := "; out_i i 0)
    and out_columns [] = ()
      | out_columns [i] = out_i i 0
      | out_columns (i :: is) = (out_i i 0; out ", "; out_columns is)
    and out_problem {comment, settings, univ_card, tuple_assigns, bounds,
                     int_bounds, expr_assigns, formula} =
        (out ("\n" ^ block_comment comment ^
              implode (map (fn (key, value) => key ^ ": " ^ value ^ "\n")
                            settings) ^
              "univ: " ^ atom_seq_name (univ_card, 0) ^ "\n" ^
              implode (map string_for_tuple_assign tuple_assigns) ^
              implode (map string_for_bound bounds) ^
              (if int_bounds = [] then
                 ""
               else
                 "int_bounds: " ^
                 commas (map int_string_for_bound int_bounds) ^ "\n"));
         List.app (fn b => (out_assign b; out ";")) expr_assigns;
         out "solve "; out_outmost_f formula; out ";\n")
  in
    out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^
         "// " ^ ATP_Util.timestamp () ^ "\n");
    List.app out_problem problems
  end

(** Parsing of solution **)

fun is_ident_char s =
  Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse
  s = "_" orelse s = "'" orelse s = "$"

fun strip_blanks [] = []
  | strip_blanks (" " :: ss) = strip_blanks ss
  | strip_blanks [s1, " "] = [s1]
  | strip_blanks (s1 :: " " :: s2 :: ss) =
    if is_ident_char s1 andalso is_ident_char s2 then
      s1 :: " " :: strip_blanks (s2 :: ss)
    else
      strip_blanks (s1 :: s2 :: ss)
  | strip_blanks (s :: ss) = s :: strip_blanks ss

val scan_nat =
  Scan.repeat1 (Scan.one Symbol.is_ascii_digit)
  >> (the o Int.fromString o implode)
val scan_rel_name =
  ($$ "s" |-- scan_nat >> pair 1
   || $$ "r" |-- scan_nat >> pair 2
   || ($$ "m" |-- scan_nat --| $$ "_") -- scan_nat) -- Scan.option ($$ "'")
  >> (fn ((n, j), SOME _) => (n, ~j - 1)
       | ((n, j), NONE) => (n, j))
val scan_atom = $$ "A" |-- scan_nat
fun parse_non_empty_list scan = scan ::: Scan.repeat ($$ "," |-- scan)
fun parse_list scan = parse_non_empty_list scan || Scan.succeed []
val parse_tuple = $$ "[" |-- parse_list scan_atom --| $$ "]"
val parse_tuple_set = $$ "[" |-- parse_list parse_tuple --| $$ "]"
val parse_assignment = (scan_rel_name --| $$ "=") -- parse_tuple_set
val parse_instance =
  Scan.this_string "relations:"
  |-- $$ "{" |-- parse_list parse_assignment --| $$ "}"

val extract_instance =
  fst o Scan.finite Symbol.stopper
            (Scan.error (!! (fn _ =>
                                raise SYNTAX ("Kodkod.extract_instance",
                                              "ill-formed Kodkodi output"))
                            parse_instance))
  o strip_blanks o raw_explode

val problem_marker = "*** PROBLEM "
val outcome_marker = "---OUTCOME---\n"
val instance_marker = "---INSTANCE---\n"

fun read_section_body marker =
  Substring.string o fst o Substring.position "\n\n"
  o Substring.triml (size marker)

fun read_next_instance s =
  let val s = Substring.position instance_marker s |> snd in
    if Substring.isEmpty s then
      raise SYNTAX ("Kodkod.read_next_instance", "expected \"INSTANCE\" marker")
    else
      read_section_body instance_marker s |> extract_instance
  end

fun read_next_outcomes j (s, ps, js) =
  let val (s1, s2) = Substring.position outcome_marker s in
    if Substring.isEmpty s2 orelse
       not (Substring.isEmpty (Substring.position problem_marker s1
                               |> snd)) then
      (s, ps, js)
    else
      let
        val outcome = read_section_body outcome_marker s2
        val s = Substring.triml (size outcome_marker) s2
      in
        if String.isSuffix "UNSATISFIABLE" outcome then
          read_next_outcomes j (s, ps, j :: js)
        else if String.isSuffix "SATISFIABLE" outcome then
          read_next_outcomes j (s, (j, read_next_instance s2) :: ps, js)
        else
          raise SYNTAX ("Kodkod.read_next_outcomes",
                        "unknown outcome " ^ quote outcome)
      end
  end

fun read_next_problems (s, ps, js) =
  let val s = Substring.position problem_marker s |> snd in
    if Substring.isEmpty s then
      (ps, js)
    else
      let
        val s = Substring.triml (size problem_marker) s
        val j_plus_1 = s |> Substring.takel (not_equal #" ") |> Substring.string
                         |> Int.fromString |> the
        val j = j_plus_1 - 1
      in read_next_problems (read_next_outcomes j (s, ps, js)) end
  end
  handle Option.Option => raise SYNTAX ("Kodkod.read_next_problems",
                                        "expected number after \"PROBLEM\"")


(** Main Kodkod entry point **)

fun serial_string_and_temporary_dir overlord =
  if overlord then ("", getenv "ISABELLE_HOME_USER")
  else (serial_string (), getenv "ISABELLE_TMP")

(* The fudge term below is to account for Kodkodi's slow start-up time, which
   is partly due to the JVM and partly due to the ML "bash" function. *)
val fudge_ms = 250

fun uncached_solve_any_problem kodkod_scala overlord deadline max_threads0 max_solutions problems =
  let
    val j = find_index (curry (op =) True o #formula) problems
    val indexed_problems = if j >= 0 then
                             [(j, nth problems j)]
                           else
                             filter_out (is_problem_trivially_false o snd)
                                        (0 upto length problems - 1 ~~ problems)
    val triv_js = filter_out (AList.defined (op =) indexed_problems)
                             (0 upto length problems - 1)
    val reindex = fst o nth indexed_problems

    val max_threads =
      if max_threads0 = 0
      then Options.default_int \<^system_option>\<open>kodkod_max_threads\<close>
      else max_threads0

    val external_process = not kodkod_scala orelse overlord
    val timeout0 = Time.toMilliseconds (deadline - Time.now ())
    val timeout = if external_process then timeout0 - fudge_ms else timeout0

    val solve_all = max_solutions > 1
  in
    if null indexed_problems then
      Normal ([], triv_js, "")
    else if timeout <= 0 then TimedOut triv_js
    else
      let
        val kki =
          let
            val buf = Unsynchronized.ref Buffer.empty
            fun out s = Unsynchronized.change buf (Buffer.add s)
            val _ = write_problem out (map snd indexed_problems)
          in Buffer.content (! buf) end
        val (rc, out, err) =
          if external_process then
            let
              val (serial_str, temp_dir) = serial_string_and_temporary_dir overlord
              fun path_for suf = Path.explode (temp_dir ^ "/kodkodi" ^ serial_str ^ "." ^ suf)
              val kki_path = path_for "kki"
              val out_path = path_for "out"
              val err_path = path_for "err"

              fun remove_temporary_files () =
                if overlord then ()
                else List.app (ignore o try File.rm) [kki_path, out_path, err_path]
            in
              \<^try>\<open>
                let
                  val _ = File.write kki_path kki
                  val rc =
                    Isabelle_System.bash ("cd " ^ Bash.string temp_dir ^ ";\n\
                      \\"$KODKODI/bin/kodkodi\"" ^
                      (" -max-msecs " ^ string_of_int timeout) ^
                      (if solve_all then " -solve-all" else "") ^
                      " -max-solutions " ^ string_of_int max_solutions ^
                      (if max_threads > 0 then " -max-threads " ^ string_of_int max_threads else "") ^
                      " < " ^ File.bash_path kki_path ^
                      " > " ^ File.bash_path out_path ^
                      " 2> " ^ File.bash_path err_path)
                  val out = File.read out_path
                  val err = File.read err_path
                  val _ = remove_temporary_files ()
                in (rc, out, err) end
                finally remove_temporary_files ()
              \<close>
            end
          else
            (timeout, (solve_all, (max_solutions, (max_threads, kki))))
            |> let open XML.Encode in pair int (pair bool (pair int (pair int string))) end
            |> YXML.string_of_body
            |> \<^scala>\<open>kodkod\<close>
            |> YXML.parse_body
            |> let open XML.Decode in triple int string string end

        val (ps, nontriv_js) =
          read_next_problems (Substring.full out, [], [])
          |>> rev ||> rev
          |> apfst (map (apfst reindex)) |> apsnd (map reindex)
        val js = triv_js @ nontriv_js

        val first_error =
          trim_split_lines err
          |> map
           (perhaps (try (unsuffix ".")) #>
            perhaps (try (unprefix "Solve error: ")) #>
            perhaps (try (unprefix "Error: ")))
          |> find_first (fn line => line <> "" andalso line <> "EXIT")
          |> the_default ""
      in
        if not (null ps) orelse rc = 0 then Normal (ps, js, first_error)
        else if rc = 2 then TimedOut js
        else if rc = 130 then Isabelle_Thread.raise_interrupt ()
        else Error (if first_error = "" then "Unknown error" else first_error, js)
      end
  end

val cached_outcome =
  Synchronized.var "Kodkod.cached_outcome"
                   (NONE : ((int * problem list) * outcome) option)

fun solve_any_problem kodkod_scala debug overlord deadline max_threads max_solutions
                      problems =
  let
    fun do_solve () =
      uncached_solve_any_problem kodkod_scala overlord deadline max_threads max_solutions
                                 problems
  in
    if debug orelse overlord then
      do_solve ()
    else
      case AList.lookup (fn ((max1, ps1), (max2, ps2)) =>
                            max1 = max2 andalso length ps1 = length ps2 andalso
                            forall problems_equivalent (ps1 ~~ ps2))
                        (the_list (Synchronized.value cached_outcome))
                        (max_solutions, problems) of
        SOME outcome => outcome
      | NONE =>
        let val outcome = do_solve () in
          (case outcome of
             Normal (_, _, "") =>
             Synchronized.change cached_outcome
                                 (K (SOME ((max_solutions, problems), outcome)))
           | _ => ());
          outcome
        end
  end

val kodkod_scala = Attrib.setup_option_bool (\<^system_option>\<open>kodkod_scala\<close>, \<^here>)

end;

99%


¤ Dauer der Verarbeitung: 0.25 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.