path: root/src/lfsc/tosmtcoq.ml

(**************************************************************************)
(*                                                                        *)
(*     SMTCoq                                                             *)
(*     Copyright (C) 2011 - 2022                                          *)
(*                                                                        *)
(*     See file "AUTHORS" for the list of authors                         *)
(*                                                                        *)
(*   This file is distributed under the terms of the CeCILL-C licence     *)
(*                                                                        *)
(**************************************************************************)


open SmtAtom
open SmtForm
open Ast
open Builtin
open Format
open Translator_sig
open SmtBtype

let ra = Atom.create ()
let rf = Form.create ()

type lit = SmtAtom.Form.t

type clause = lit list

let lit_of_atom_form_lit rf af = Form.lit_of_atom_form_lit rf (true, af)

let show_veritproof =
  try ignore (Sys.getenv "DONTSHOWVERIT"); false
  with Not_found -> true


module HS = Hstring.H
(* module HT = Hashtbl.Make (Term) *)
module HCl = Hashtbl

module HT = struct
  module M = Map.Make (Term)
  let create _ = ref M.empty
  let add h k v = h := M.add k v !h
  let find h k = M.find k !h
  let clear h = h := M.empty
  (* let iter f h = M.iter f !h *)
end



let clauses_ids = HCl.create 201
let ids_clauses = Hashtbl.create 201
let propvars = HT.create 201
let inputs : int HS.t = HS.create 13
let alias_tbl = HS.create 17
let memo_terms = HT.create 31
(* let termalias_tbl = HT.create 17 *)

let cl_cpt = ref 0


let get_rule = function
  | Reso -> VeritSyntax.Reso
  | Weak -> VeritSyntax.Weak
  | Or -> VeritSyntax.Or
  | Orp -> VeritSyntax.Orp
  | Imp -> VeritSyntax.Imp
  | Impp -> VeritSyntax.Impp
  | Nand -> VeritSyntax.Nand
  | Andn -> VeritSyntax.Andn
  | Nimp1 -> VeritSyntax.Nimp1
  | Nimp2 -> VeritSyntax.Nimp2
  | Impn1 -> VeritSyntax.Impn1
  | Impn2 -> VeritSyntax.Impn2
  | Nor -> VeritSyntax.Nor
  | Orn -> VeritSyntax.Orn
  | And -> VeritSyntax.And
  | Andp -> VeritSyntax.Andp
  | Equ1 -> VeritSyntax.Equ1
  | Equ2 -> VeritSyntax.Equ2
  | Nequ1 -> VeritSyntax.Nequ1
  | Nequ2 -> VeritSyntax.Nequ2
  | Equp1 -> VeritSyntax.Equp1
  | Equp2 -> VeritSyntax.Equp2
  | Equn1 -> VeritSyntax.Equn1
  | Equn2 -> VeritSyntax.Equn2
  | Xor1 -> VeritSyntax.Xor1
  | Xor2 -> VeritSyntax.Xor2
  | Xorp1 -> VeritSyntax.Xorp1
  | Xorp2 -> VeritSyntax.Xorp2
  | Xorn1 -> VeritSyntax.Xorn1
  | Xorn2 -> VeritSyntax.Xorn2
  | Nxor1 -> VeritSyntax.Nxor1
  | Nxor2 -> VeritSyntax.Nxor2
  | Itep1 -> VeritSyntax.Itep1
  | Itep2 -> VeritSyntax.Itep2
  | Iten1 -> VeritSyntax.Iten1
  | Iten2 -> VeritSyntax.Iten2
  | Ite1 -> VeritSyntax.Ite1
  | Ite2 -> VeritSyntax.Ite2
  | Nite1 -> VeritSyntax.Nite1
  | Nite2 -> VeritSyntax.Nite2
  | Eqtr -> VeritSyntax.Eqtr
  | Eqcp -> VeritSyntax.Eqcp
  | Eqco -> VeritSyntax.Eqco
  | Eqre -> VeritSyntax.Eqre
  | Lage -> VeritSyntax.Lage
  | Flat -> VeritSyntax.Flat
  | Hole -> VeritSyntax.Hole
  | True -> VeritSyntax.True
  | Fals -> VeritSyntax.Fals
  | Bbva -> VeritSyntax.Bbva
  | Bbconst -> VeritSyntax.Bbconst
  | Bbeq -> VeritSyntax.Bbeq
  | Bbdis -> VeritSyntax.Bbdis
  | Bbop -> VeritSyntax.Bbop
  | Bbadd -> VeritSyntax.Bbadd
  | Bbmul -> VeritSyntax.Bbmul
  | Bbult -> VeritSyntax.Bbult
  | Bbslt -> VeritSyntax.Bbslt
  | Bbshl -> VeritSyntax.Bbshl
  | Bbshr -> VeritSyntax.Bbshr
  | Bbnot -> VeritSyntax.Bbnot
  | Bbneg -> VeritSyntax.Bbneg
  | Bbconc -> VeritSyntax.Bbconc
  | Bbextr -> VeritSyntax.Bbextr
  | Bbzext -> VeritSyntax.Bbzext
  | Bbsext -> VeritSyntax.Bbsext
  | Row1 -> VeritSyntax.Row1
  | Row2 -> VeritSyntax.Row2
  | Exte -> VeritSyntax.Exte

let string_of_rule = function
  | Reso -> "resolution"
  | Weak -> "weaken"
  | Or -> "or"
  | Orp -> "or_pos"
  | Imp -> "implies"
  | Impp -> "implies_pos"
  | Nand -> "not_and"
  | Andn -> "and_neg"
  | Nimp1 -> "not_implies1"
  | Nimp2 -> "not_implies2"
  | Impn1 -> "implies_neg1"
  | Impn2 -> "implies_neg2"
  | Nor -> "not_or"
  | Orn -> "or_neg"
  | And -> "and"
  | Andp -> "and_pos"
  | Equ1 -> "equiv1"
  | Equ2 -> "equiv2"
  | Nequ1 -> "not_equiv1"
  | Nequ2 -> "not_equiv2"
  | Equp1 -> "equiv_pos1"
  | Equp2 -> "equiv_pos2"
  | Equn1 -> "equiv_neg1"
  | Equn2 -> "equiv_neg2"
  | Xor1 -> "xor1"
  | Xor2 -> "xor2"
  | Xorp1 -> "xor_pos1"
  | Xorp2 -> "xor_pos2"
  | Xorn1 -> "xor_neg1"
  | Xorn2 -> "xor_neg2"
  | Nxor1 -> "not_xor1"
  | Nxor2 -> "not_xor2"
  | Itep1 -> "ite_pos1"
  | Itep2 -> "ite_pos2"
  | Iten1 -> "ite_neg1"
  | Iten2 -> "ite_neg2"
  | Ite1 -> "ite1"
  | Ite2 -> "ite2"
  | Nite1 -> "not_ite1"
  | Nite2 -> "not_ite2"
  | Eqtr -> "eq_transitive"
  | Eqcp -> "eq_congruent_pred"
  | Eqco -> "eq_congruent"
  | Eqre -> "eq_reflexive"
  | Lage -> "la_generic"
  | Flat -> "flatten"
  | Hole -> "hole"
  | True -> "true"
  | Fals -> "false"
  | Bbva -> "bbvar"
  | Bbconst -> "bbconst"
  | Bbeq -> "bbeq"
  | Bbdis -> "bv_const_neq"
  | Bbop -> "bbop"
  | Bbadd -> "bbadd"
  | Bbmul -> "bbmul"
  | Bbult -> "bbult"
  | Bbslt -> "bbslt"
  | Bbshl -> "bbshl"
  | Bbshr -> "bbshr"
  | Bbnot -> "bbnot"
  | Bbneg -> "bbneg"
  | Bbconc -> "bbconcat"
  | Bbextr -> "bbextract"
  | Bbzext -> "bbzextend"
  | Bbsext -> "bbsextend"
  | Row1 -> "row1"
  | Row2 -> "row2" 
  | Exte -> "ext" 


let bit_to_bool t = match name t with
  | Some n when n == H.b0 -> false
  | Some n when n == H.b1 -> true
  | _ -> assert false

let rec const_bv_aux acc t = match name t with
  | Some n when n == H.bvn -> acc
  | _ ->
    match app_name t with
    | Some (n, [b; t]) when n == H.bvc -> const_bv_aux (bit_to_bool b :: acc) t
    | _ -> assert false

let const_bv t =
  let bv_list = const_bv_aux [] t in
  Form.Atom (Atom.mk_bvconst ra bv_list)


let rec term_smtcoq_old t =
  match value t with
  | Const {sname=Name n} when n == H.ttrue -> Form.Form Form.pform_true
  | Const {sname=Name n} when n == H.tfalse -> Form.Form Form.pform_false
  | Const {sname=Name n} when n == H.bvn -> const_bv t
  | Const {sname=Name n} ->
    begin
      try
        term_smtcoq  (HS.find alias_tbl n)
      with Not_found ->
        Form.Atom (Atom.get ra (Aapp (SmtMaps.get_fun (Hstring.view n),[||])))
    end
  | Int bi -> Form.Atom (Atom.hatom_Z_of_bigint ra bi)
  | App _ ->
    begin match app_name t with
      | Some (n, [f]) when n == H.not_ ->
        Form.Lit (Form.neg (lit_of_atom_form_lit rf (term_smtcoq f)))
      | Some (n, args) when n == H.and_ -> Form.Form (Fapp (Fand, args_smtcoq args))
      | Some (n, args) when n == H.or_ -> Form.Form (Fapp (For, args_smtcoq args))
      | Some (n, args) when n == H.impl_ -> Form.Form (Fapp (Fimp, args_smtcoq args))
      | Some (n, args) when n == H.xor_ -> Form.Form (Fapp (Fxor, args_smtcoq args))
      | Some (n, args) when n == H.ite || n == H.ifte_ ->
        Form.Form (Fapp (Fite, args_smtcoq args))
      | Some (n, args) when n == H.iff -> Form.Form (Fapp (Fiff, args_smtcoq args))
      | Some (n, [_; a; b]) when n == H.eq ->
        let h1, h2 = term_smtcoq_atom a, term_smtcoq_atom b in
        Form.Atom (Atom.mk_eq_sym ra (Atom.type_of h1) h1 h2)
      | Some (n, _) when n == H.apply -> uncurry [] t
      | Some (n, [p]) when n == H.p_app -> term_smtcoq p
      | Some (n, [{value = Int bi}]) when n == H.a_int ->
        Form.Atom (Atom.hatom_Z_of_bigint ra bi)
      | Some (n, [ni]) when n == H.a_int ->
        begin match app_name ni with
          | Some (n, [{value = Int bi}]) when n == H.uminus ->
            Form.Atom (Atom.hatom_Z_of_bigint ra (Big_int.minus_big_int bi))
          | _ -> assert false
        end
      | Some (n, [_; v]) when n == H.a_var_bv -> term_smtcoq v
      | Some (n, _) when n == H.bvc -> const_bv t
      | Some (n, [_; v]) when n == H.a_bv -> term_smtcoq v
      | Some (b, [a; {value = Int n}]) when b == H.bitof ->
         (let ha = term_smtcoq_atom a in
          match Atom.type_of ha with
            | TBV s -> Form.Atom (Atom.mk_bitof ra s (Big_int.int_of_big_int n) ha)
            | _ -> assert false)
      | Some (n, [_; a; bb]) when n == H.bblast_term ->
        Form.Form (FbbT ((term_smtcoq_atom a), bblt_lits [] bb))
      | Some (n, [_; a]) when n == H.bvnot ->
         (let ha = term_smtcoq_atom a in
          match Atom.type_of ha with
            | TBV s -> Form.Atom (Atom.mk_bvnot ra s ha)
            | _ -> assert false)
      | Some (n, [_; a]) when n == H.bvneg ->
         (let ha = term_smtcoq_atom a in
          match Atom.type_of ha with
            | TBV s -> Form.Atom (Atom.mk_bvneg ra s ha)
            | _ -> assert false)
      | Some (n, [_; a; b]) when n == H.bvand ->
         (let ha = term_smtcoq_atom a in
          let hb = term_smtcoq_atom b in
          match Atom.type_of ha with
            | TBV s -> Form.Atom (Atom.mk_bvand ra s ha hb)
            | _ -> assert false)
      | Some (n, [_; a; b]) when n == H.bvor ->
         (let ha = term_smtcoq_atom a in
          let hb = term_smtcoq_atom b in
          match Atom.type_of ha with
            | TBV s -> Form.Atom (Atom.mk_bvor ra s ha hb)
            | _ -> assert false)
      | Some (n, [_; a; b]) when n == H.bvxor ->
         (let ha = term_smtcoq_atom a in
          let hb = term_smtcoq_atom b in
          match Atom.type_of ha with
            | TBV s -> Form.Atom (Atom.mk_bvxor ra s ha hb)
            | _ -> assert false)
      | Some (n, [_; a; b]) when n == H.bvadd ->
         (let ha = term_smtcoq_atom a in
          let hb = term_smtcoq_atom b in
          match Atom.type_of ha with
            | TBV s -> Form.Atom (Atom.mk_bvadd ra s ha hb)
            | _ -> assert false)
      | Some (n, [_; a; b]) when n == H.bvmul ->
         (let ha = term_smtcoq_atom a in
          let hb = term_smtcoq_atom b in
          match Atom.type_of ha with
            | TBV s -> Form.Atom (Atom.mk_bvmult ra s ha hb)
            | _ -> assert false)
      | Some (n, [_; a; b]) when n == H.bvult ->
         (let ha = term_smtcoq_atom a in
          let hb = term_smtcoq_atom b in
          match Atom.type_of ha with
            | TBV s -> Form.Atom (Atom.mk_bvult ra s ha hb)
            | _ -> assert false)
      | Some (n, [_; a; b]) when n == H.bvslt ->
         (let ha = term_smtcoq_atom a in
          let hb = term_smtcoq_atom b in
          match Atom.type_of ha with
            | TBV s -> Form.Atom (Atom.mk_bvslt ra s ha hb)
            | _ -> assert false)
      | Some (n, [_; a; b]) when n == H.bvule ->
        (let ha = term_smtcoq_atom a in
         let hb = term_smtcoq_atom b in
         match Atom.type_of ha with
         | TBV s ->
           let a = Form.Atom (Atom.mk_bvult ra s hb ha) in
           Form.Lit (Form.neg (lit_of_atom_form_lit rf a))
         | _ -> assert false)
      | Some (n, [_; a; b]) when n == H.bvsle ->
        (let ha = term_smtcoq_atom a in
         let hb = term_smtcoq_atom b in
         match Atom.type_of ha with
         | TBV s ->
           let a = Form.Atom (Atom.mk_bvslt ra s hb ha) in
           Form.Lit (Form.neg (lit_of_atom_form_lit rf a))
         | _ -> assert false)         
      | Some (n, [_; _; _; a; b]) when n == H.concat ->
         (let ha = term_smtcoq_atom a in
          let hb = term_smtcoq_atom b in
          match Atom.type_of ha, Atom.type_of hb with
            | TBV s1, TBV s2 -> Form.Atom (Atom.mk_bvconcat ra s1 s2 ha hb)
            | _ -> assert false)
      | Some (n, [_; {value = Int bj}; {value = Int bi}; _; a])
        when n == H.extract ->
        (let ha = term_smtcoq_atom a in
         let i = Big_int.int_of_big_int bi in
         let j = Big_int.int_of_big_int bj in
          match Atom.type_of ha with
            | TBV s -> Form.Atom (Atom.mk_bvextr ra ~s ~i ~n:(j-i+1) ha)
            | _ -> assert false)
      | Some (n, [_; {value = Int bi}; _; a])
        when n == H.zero_extend ->
        (let ha = term_smtcoq_atom a in
         let n = Big_int.int_of_big_int bi in
          match Atom.type_of ha with
            | TBV s -> Form.Atom (Atom.mk_bvzextn ra ~s ~n ha)
            | _ -> assert false)
      | Some (n, [_; {value = Int bi}; _; a])
        when n == H.sign_extend ->
        (let ha = term_smtcoq_atom a in
         let n = Big_int.int_of_big_int bi in
          match Atom.type_of ha with
            | TBV s -> Form.Atom (Atom.mk_bvsextn ra ~s ~n ha)
            | _ -> assert false)
      | Some (n, [_; a; b]) when n == H.bvshl ->
         (let ha = term_smtcoq_atom a in
          let hb = term_smtcoq_atom b in
          match Atom.type_of ha with
            | TBV s -> Form.Atom (Atom.mk_bvshl ra s ha hb)
            | _ -> assert false)
      | Some (n, [_; a; b]) when n == H.bvlshr ->
         (let ha = term_smtcoq_atom a in
          let hb = term_smtcoq_atom b in
          match Atom.type_of ha with
            | TBV s -> Form.Atom (Atom.mk_bvshr ra s ha hb)
            | _ -> assert false)

      | Some (n, [a; b]) when n == H.lt_Int ->
        Form.Atom (Atom.mk_lt ra (term_smtcoq_atom a) (term_smtcoq_atom b))
      | Some (n, [a; b]) when n == H.le_Int ->
        Form.Atom (Atom.mk_le ra (term_smtcoq_atom a) (term_smtcoq_atom b))
      | Some (n, [a; b]) when n == H.gt_Int ->
        Form.Atom (Atom.mk_gt ra (term_smtcoq_atom a) (term_smtcoq_atom b))
      | Some (n, [a; b]) when n == H.ge_Int ->
        Form.Atom (Atom.mk_ge ra (term_smtcoq_atom a) (term_smtcoq_atom b))
      | Some (n, [a; b]) when n == H.plus_Int ->
        Form.Atom (Atom.mk_plus ra (term_smtcoq_atom a) (term_smtcoq_atom b))
      | Some (n, [a; b]) when n == H.minus_Int ->
        Form.Atom (Atom.mk_minus ra (term_smtcoq_atom a) (term_smtcoq_atom b))
      | Some (n, [a; b]) when n == H.times_Int ->
        Form.Atom (Atom.mk_mult ra (term_smtcoq_atom a) (term_smtcoq_atom b))
      | Some (n, [a]) when n == H.uminus_Int ->
        Form.Atom (Atom.mk_opp ra (term_smtcoq_atom a))
      | Some (n, _) ->
        Format.eprintf "\nTerm: %a\n@." print_term t;
        failwith ("LFSC function symbol "^Hstring.view n^" not supported.")
      | _ -> assert false
    end

  | Rat _ -> failwith ("LFSC rationals not supported")
  | Type -> failwith ("LFSC Type not supported")
  | Kind -> failwith ("LFSC Kind not supported")
  | Mpz -> failwith ("LFSC mpz not supported")
  | Mpq -> failwith ("LFSC mpq not supported")
  | Pi _ -> failwith ("LFSC pi abstractions not supported")
  | Lambda _ -> failwith ("LFSC lambda abstractions not supported")
  | Hole _ -> failwith ("LFSC holes not supported")
  | Ptr _ -> failwith ("LFSC Ptr not supported")
  | SideCond _ -> failwith ("LFSC side conditions not supported")
  | _ -> assert false


and term_smtcoq t =
  try HT.find memo_terms t
  with Not_found ->
    let v = term_smtcoq_old t in
    HT.add memo_terms t v;
    v


and term_smtcoq_atom a = match term_smtcoq a with
  | Form.Atom h -> h
  | _ ->  assert false

and args_smtcoq args =
  List.map (fun t -> lit_of_atom_form_lit rf (term_smtcoq t)) args
  |> Array.of_list

and uncurry acc t = match app_name t, acc with
  | Some (n, [_; _; f; a]), _ when n == H.apply ->
    uncurry (term_smtcoq_atom a :: acc) f
  | Some (n, [_; _]) , [h1; h2] when n == H.read ->
    (match Atom.type_of h1 with
     | TFArray (ti,te) -> Form.Atom (Atom.mk_select ra ti te h1 h2)
     | _ -> assert false)
  | Some (n, [_; _]) , [h1; h2; h3] when n == H.write ->
    (match Atom.type_of h1 with
     | TFArray (ti,te) -> Form.Atom (Atom.mk_store ra ti te h1 h2 h3)
     | _ -> assert false)
  | Some (n, [_; _]) , [h1; h2] when n == H.diff ->
    (match Atom.type_of h1 with
     | TFArray (ti,te) -> Form.Atom (Atom.mk_diffarray ra ti te h1 h2)
     | _ -> assert false)
  | None, _ ->
    (match name t with
     | Some n ->
       let args = Array.of_list acc in
       Form.Atom (Atom.get ra (Aapp (SmtMaps.get_fun (Hstring.view n), args)))
     | _ -> assert false)
  | _ ->
    eprintf "uncurry fail: %a@." Ast.print_term t;
    assert false

(* Endianness dependant: LFSC big endian -> SMTCoq little endian *)
and bblt_lits acc t = match name t with
  | Some n when n == H.bbltn -> acc
  | _ -> match app_name t with
    | Some (n, [f; r]) when n == H.bbltc ->
      bblt_lits (lit_of_atom_form_lit rf (term_smtcoq f) :: acc) r
    | _ -> assert false


let term_smtcoq t =
  (* eprintf "translate term %a@." Ast.print_term t; *)
  lit_of_atom_form_lit rf (term_smtcoq t)


let rec clause_smtcoq acc t = match name t with
  | Some n when n == H.cln || n == H.tfalse -> acc
  | Some _ -> term_smtcoq t :: acc
  | None ->
    match app_name t with
    | Some (n, [v]) when n == H.pos ->
      let t = HT.find propvars (deref v) in
      term_smtcoq t :: acc
    | Some (n, [v]) when n == H.neg ->
      let t = HT.find propvars (deref v) in
      Form.neg (term_smtcoq t) :: acc
    | Some (n, [a; cl]) when n == H.clc ->
      clause_smtcoq (clause_smtcoq acc a) cl
    | Some (n, [a; b]) when n == H.or_ -> clause_smtcoq (clause_smtcoq acc a) b
    | _ -> term_smtcoq t :: acc


let to_clause = clause_smtcoq [] 


let print_clause fmt cl =
  fprintf fmt "(";
  List.iter (fprintf fmt "%a " (Form.to_smt ~debug:false)) cl;
  fprintf fmt ")"



type clause_res_id = NewCl of int | OldCl of int


let register_clause_id cl id =
  HCl.add clauses_ids cl id;
  Hashtbl.add ids_clauses id cl


(* let register_termclause_id t id =
 *   register_clause_id (to_clause t) id *)


let new_clause_id ?(reuse=true) cl =
  try
    if not reuse then raise Not_found;
    OldCl (HCl.find clauses_ids cl)
  with Not_found ->
    incr cl_cpt;
    let id = !cl_cpt in
    register_clause_id cl id;
    NewCl id


let mk_clause ?(reuse=true) rule cl args =
  match new_clause_id ~reuse cl with
  | NewCl id ->
    if show_veritproof then
      eprintf "%d:(%s %a %a)@." id (string_of_rule rule)
        print_clause cl
        (fun fmt -> List.iter (fprintf fmt " %d")) args;
    VeritSyntax.mk_clause (id, (get_rule rule), cl, args)
  | OldCl id ->
    (* Format.eprintf "old_clause %d@." id; *)
    id


let mk_clause_cl ?(reuse=true) rule cl args =
  mk_clause ~reuse rule (List.map term_smtcoq cl) args


let mk_input name formula =
  let cl = [term_smtcoq formula] in
  match new_clause_id cl with
   | NewCl id ->
     register_clause_id cl id;
     HS.add inputs name id;
     if show_veritproof then eprintf "%d:input  %a@." id print_clause cl;
     VeritSyntax.mk_clause (id, VeritSyntax.Inpu, cl, []) |> ignore
   | OldCl _ -> ()


let mk_admit_preproc name formula =
  let cl = [term_smtcoq formula] in
  match new_clause_id cl with
   | NewCl id ->
     register_clause_id cl id;
     HS.add inputs name id;
     if show_veritproof then eprintf "%d:hole  %a@." id print_clause cl;
     VeritSyntax.mk_clause (id, VeritSyntax.Hole, cl, []) |> ignore
   | OldCl _ -> ()


let register_prop_abstr vt formula = HT.add propvars vt formula


let register_alias name_index t = HS.add alias_tbl name_index t


(* let register_termalias a t = HT.add termalias_tbl a t *)


let get_clause_id cl =
  try HCl.find clauses_ids cl with Not_found -> assert false


let get_input_id h = HS.find inputs h


let register_decl name formula =
  let cl = [term_smtcoq formula] in
  match new_clause_id cl with
  | NewCl id | OldCl id ->
    (* eprintf "register decl %d@." id; *)
    HS.add inputs name id

let register_decl_id name id =
  (* eprintf "register_decl %s : %d@." name id; *)
  HS.add inputs name id



let clear () =
  Atom.clear ra;
  Form.clear rf;
  HCl.clear clauses_ids;
  Hashtbl.clear ids_clauses;
  HT.clear propvars;
  HS.clear inputs;
  HS.clear alias_tbl;
  HT.clear memo_terms;
  (* HT.clear termalias_tbl; *)
  cl_cpt := 0