Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: g_indfun.mlg Sprache: SML

Original von: Isabelle^©

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

Representation of literals. Literals are terms with a polarity, either positive or negative.
A literal for term t with positive polarity is equivalent to t.
A literal for term t with negative polarity is equivalent to the propositional negation of t.
*)

signature ARGO_LIT =
sig
  datatype literal = Pos of Argo_Term.term | Neg of Argo_Term.term
  val literal: Argo_Term.term -> bool -> literal
  val dest: literal -> Argo_Term.term * bool
  val term_of: literal -> Argo_Term.term
  val signed_id_of: literal -> int
  val signed_expr_of: literal -> Argo_Expr.expr
  val negate: literal -> literal
  val eq_id: literal * literal -> bool
  val eq_lit: literal * literal -> bool
  val dual_lit: literal * literal -> bool
end

structure Argo_Lit: ARGO_LIT =
struct

(* data type *)

datatype literal = Pos of Argo_Term.term | Neg of Argo_Term.term

(* operations *)

fun literal t true = Pos t
  | literal t false = Neg t

fun dest (Pos t) = (t, true)
  | dest (Neg t) = (t, false)

fun term_of (Pos t) = t
  | term_of (Neg t) = t

fun signed_id_of (Pos t) = Argo_Term.id_of t
  | signed_id_of (Neg t) = ~(Argo_Term.id_of t)

fun signed_expr_of (Pos t) = Argo_Term.expr_of t
  | signed_expr_of (Neg t) = Argo_Expr.mk_not (Argo_Term.expr_of t)

fun id_of (Pos t) = Argo_Term.id_of t
  | id_of (Neg t) = Argo_Term.id_of t

fun negate (Pos t) = Neg t
  | negate (Neg t) = Pos t

fun eq_id (lit1, lit2) = (id_of lit1 = id_of lit2)

fun eq_lit (Pos t1, Pos t2) = Argo_Term.eq_term (t1, t2)
  | eq_lit (Neg t1, Neg t2) = Argo_Term.eq_term (t1, t2)
  | eq_lit _ = false

fun dual_lit (Pos t1, Neg t2) = Argo_Term.eq_term (t1, t2)
  | dual_lit (Neg t1, Pos t2) = Argo_Term.eq_term (t1, t2)
  | dual_lit _ = false

end

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.