src/Tools/Argo/argo_lit.ML
author boehmes
Thu Sep 29 20:54:44 2016 +0200 (2016-09-29)
changeset 63960 3daf02070be5
permissions -rw-r--r--
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes@63960
     1
(*  Title:      Tools/Argo/argo_lit.ML
boehmes@63960
     2
    Author:     Sascha Boehme
boehmes@63960
     3
boehmes@63960
     4
Representation of literals. Literals are terms with a polarity, either positive or negative.
boehmes@63960
     5
A literal for term t with positive polarity is equivalent to t.
boehmes@63960
     6
A literal for term t with negative polarity is equivalent to the propositional negation of t.
boehmes@63960
     7
*)
boehmes@63960
     8
boehmes@63960
     9
signature ARGO_LIT =
boehmes@63960
    10
sig
boehmes@63960
    11
  datatype literal = Pos of Argo_Term.term | Neg of Argo_Term.term
boehmes@63960
    12
  val literal: Argo_Term.term -> bool -> literal
boehmes@63960
    13
  val dest: literal -> Argo_Term.term * bool
boehmes@63960
    14
  val term_of: literal -> Argo_Term.term
boehmes@63960
    15
  val signed_id_of: literal -> int
boehmes@63960
    16
  val signed_expr_of: literal -> Argo_Expr.expr
boehmes@63960
    17
  val negate: literal -> literal
boehmes@63960
    18
  val eq_id: literal * literal -> bool
boehmes@63960
    19
  val eq_lit: literal * literal -> bool
boehmes@63960
    20
  val dual_lit: literal * literal -> bool
boehmes@63960
    21
end
boehmes@63960
    22
boehmes@63960
    23
structure Argo_Lit: ARGO_LIT =
boehmes@63960
    24
struct
boehmes@63960
    25
boehmes@63960
    26
(* data type *)
boehmes@63960
    27
boehmes@63960
    28
datatype literal = Pos of Argo_Term.term | Neg of Argo_Term.term
boehmes@63960
    29
boehmes@63960
    30
boehmes@63960
    31
(* operations *)
boehmes@63960
    32
boehmes@63960
    33
fun literal t true = Pos t
boehmes@63960
    34
  | literal t false = Neg t
boehmes@63960
    35
boehmes@63960
    36
fun dest (Pos t) = (t, true)
boehmes@63960
    37
  | dest (Neg t) = (t, false)
boehmes@63960
    38
boehmes@63960
    39
fun term_of (Pos t) = t
boehmes@63960
    40
  | term_of (Neg t) = t
boehmes@63960
    41
boehmes@63960
    42
fun signed_id_of (Pos t) = Argo_Term.id_of t
boehmes@63960
    43
  | signed_id_of (Neg t) = ~(Argo_Term.id_of t)
boehmes@63960
    44
boehmes@63960
    45
fun signed_expr_of (Pos t) = Argo_Term.expr_of t
boehmes@63960
    46
  | signed_expr_of (Neg t) = Argo_Expr.mk_not (Argo_Term.expr_of t)
boehmes@63960
    47
boehmes@63960
    48
fun id_of (Pos t) = Argo_Term.id_of t
boehmes@63960
    49
  | id_of (Neg t) = Argo_Term.id_of t
boehmes@63960
    50
boehmes@63960
    51
fun negate (Pos t) = Neg t
boehmes@63960
    52
  | negate (Neg t) = Pos t
boehmes@63960
    53
boehmes@63960
    54
fun eq_id (lit1, lit2) = (id_of lit1 = id_of lit2)
boehmes@63960
    55
boehmes@63960
    56
fun eq_lit (Pos t1, Pos t2) = Argo_Term.eq_term (t1, t2)
boehmes@63960
    57
  | eq_lit (Neg t1, Neg t2) = Argo_Term.eq_term (t1, t2)
boehmes@63960
    58
  | eq_lit _ = false
boehmes@63960
    59
boehmes@63960
    60
fun dual_lit (Pos t1, Neg t2) = Argo_Term.eq_term (t1, t2)
boehmes@63960
    61
  | dual_lit (Neg t1, Pos t2) = Argo_Term.eq_term (t1, t2)
boehmes@63960
    62
  | dual_lit _ = false
boehmes@63960
    63
boehmes@63960
    64
end