Stufen

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

Angebot Produkte Projekt Beratung

in der Quellcodebibliothek suchen Parameter fehlt Codequalität: Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/trig/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 540 B

Quellcode-Bibliothek argo_cls.ML Sprache: SML

(*  Title:      Tools/Argo/argo_cls.ML
    Author:     Sascha Boehme

Representation of clauses. Clauses are disjunctions of literals with a proof that explains
why the disjunction holds.
*)

signature ARGO_CLS =
sig
  type clause = Argo_Lit.literal list * Argo_Proof.proof
  val eq_clause: clause * clause -> bool

  (* two-literal watches for clauses *)
  type table
  val table: table
  val put_watches: clause -> Argo_Lit.literal * Argo_Lit.literal -> table -> table
  val get_watches: table -> clause -> Argo_Lit.literal * Argo_Lit.literal
end

structure Argo_Cls: ARGO_CLS =
struct

type clause = Argo_Lit.literal list * Argo_Proof.proof

fun eq_clause ((_, p1), (_, p2)) = Argo_Proof.eq_proof_id (apply2 Argo_Proof.id_of (p1, p2))
fun clause_ord ((_, p1), (_, p2)) = Argo_Proof.proof_id_ord (apply2 Argo_Proof.id_of (p1, p2))

(* two-literal watches for clauses *)

(*
  The CDCL solver keeps a mapping of some literals to clauses. Exactly two literals
  of a clause are used to index the clause.
*)

structure Clstab = Table(type key = clause val ord = clause_ord)

type table = (Argo_Lit.literal * Argo_Lit.literal) Clstab.table

val table: table = Clstab.empty

fun put_watches cls lp table = Clstab.update (cls, lp) table
fun get_watches table cls = the (Clstab.lookup table cls)

end

quality100%

¤ 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.0.12Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.