src/Tools/Argo/argo_term.ML

new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic

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

Internal language of the Argo solver.

Terms are fully-shared via hash-consing. Alpha-equivalent terms have the same identifier.
*)

signature ARGO_TERM =
sig
  (* data types *)
  type meta
  datatype term = T of meta * Argo_Expr.kind * term list

  (* term operations *)
  val id_of: term -> int
  val expr_of: term -> Argo_Expr.expr
  val type_of: term -> Argo_Expr.typ
  val eq_term: term * term -> bool
  val term_ord: term * term -> order

  (* context *)
  type context
  val context: context

  (* identifying expressions *)
  datatype item = Expr of Argo_Expr.expr | Term of term
  datatype identified = New of term | Known of term
  val identify_item: item -> context -> identified * context
end

structure Argo_Term: ARGO_TERM =
struct

(* data types *)

(*
  The type meta is intentionally hidden to prevent that functions outside of this structure
  are able to build terms. Meta stores the identifier of the term as well as the complete
  expression underlying the term.
*)

datatype meta = M of int * Argo_Expr.expr
datatype term = T of meta * Argo_Expr.kind * term list


(* term operations *)

fun id_of (T (M (id, _), _, _)) = id
fun expr_of (T (M (_, e), _, _)) = e
fun type_of t = Argo_Expr.type_of (expr_of t)

(*
  Comparing terms is fast as only the identifiers are compared. No expressions need to
  be taken into account.
*)

fun eq_term (t1, t2) = (id_of t1 = id_of t2)
fun term_ord (t1, t2) = int_ord (id_of t1, id_of t2)


(* sharing of terms *)

(*
  Kinds are short representation of expressions. Constants and numbers carry additional
  information and have no arguments. Their kind is hence similar to them. All other expressions
  are stored in a flat way with identifiers of shared terms as arguments instead of expression
  as arguments.
*)

datatype kind =
  Con of string * Argo_Expr.typ |
  Num of Rat.rat |
  Exp of int list

fun kind_of (Argo_Expr.E (Argo_Expr.Con c, _)) _ = Con c
  | kind_of (Argo_Expr.E (Argo_Expr.Num n, _)) _ = Num n
  | kind_of (Argo_Expr.E (k, _)) is = Exp (Argo_Expr.int_of_kind k :: is)

fun int_of_kind (Con _) = 1
  | int_of_kind (Num _) = 2
  | int_of_kind (Exp _) = 3

fun kind_ord (Con c1, Con c2) = Argo_Expr.con_ord (c1, c2)
  | kind_ord (Num n1, Num n2) = Rat.ord (n1, n2)
  | kind_ord (Exp is1, Exp is2) = dict_ord int_ord (is1, is2)
  | kind_ord (k1, k2) = int_ord (int_of_kind k1, int_of_kind k2)

structure Kindtab = Table(type key = kind val ord = kind_ord)

(*
  The context keeps track of the next unused identifier as well as all shared terms,
  which are indexed by their unique kind. For each term, a boolean marker flag is stored.
  When set to true on an atom, the atom is already asserted to the solver core. When set to
  true on an if-then-else term, the term has already been lifted.

  Zero is intentionally avoided as identifier, since literals use term identifiers
  with a sign as literal identifiers.
*)

type context = {
  next_id: int,
  terms: (term * bool) Kindtab.table}

fun mk_context next_id terms: context = {next_id=next_id, terms=terms}

val context = mk_context 1 Kindtab.empty

fun note_atom true kind (t, false) ({next_id, terms}: context) =
      mk_context next_id (Kindtab.update (kind, (t, true)) terms)
  | note_atom _ _ _ cx = cx

fun with_unique_id kind is_atom (e as Argo_Expr.E (k, _)) ts ({next_id, terms}: context) =
  let val t = T (M (next_id, e), k, ts)
  in ((t, false), mk_context (next_id + 1) (Kindtab.update (kind, (t, is_atom)) terms)) end

fun unique kind is_atom e ts (cx as {terms, ...}: context) =
  (case Kindtab.lookup terms kind of
    SOME tp => (tp, note_atom is_atom kind tp cx)
  | NONE => with_unique_id kind is_atom e ts cx)


(* identifying expressions *)

(*
  Only atoms, i.e., boolean propositons, and if-then-else expressions need to be identified.
  Other terms are identified implicitly. The identification process works bottom-up.

  The solver core needs to know whether an atom has already been added. Likewise, the clausifier
  needs to know whether an if-then-else expression has already been lifted. Therefore,
  the identified term is marked as either "new" when identified for the first time or
  "known" when it has already been identified before.
*)

datatype item = Expr of Argo_Expr.expr | Term of term
datatype identified = New of term | Known of term

fun identify_head is_atom e (ts, cx) = unique (kind_of e (map id_of ts)) is_atom e ts cx

fun identify is_atom (e as Argo_Expr.E (_, es)) cx =
  identify_head is_atom e (fold_map (apfst fst oo identify false) es cx)

fun identified (t, true) = Known t
  | identified (t, false) = New t

fun identify_item (Expr e) cx = identify true e cx |>> identified
  | identify_item (Term (t as T (_, _, ts))) cx =
      identify_head true (expr_of t) (ts, cx) |>> identified

end

structure Argo_Termtab = Table(type key = Argo_Term.term val ord = Argo_Term.term_ord)