(* MACE model finding.
   Copyright (C) 2004 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

   h1 is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   h1 is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with h1; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*)

open "mace_h";

datatype mace_var = MACE_F_VAR of string * int * (int * int) set
       | MACE_P_VAR of string * int set;

(* MACE_F_VAR (f, i, bv):
 Each function f : D^k -> D, where |D| = 2^p is encoded through
 k functions fi : D^k -> Bool, i.e., through k subsets fi of D^k.
 Elements of D^k are bit vectors of length kp, i.e., subsets bv
 of {1, ..., k} * {1, ..., p}.

 MACE_P_VAR (P, bv):
 Each predicate P : D -> Bool is just a subset of D, elements
 are bit vectors of length p, i.e., subsets of {1, ..., p}.
 *)

exception MaceTerm;

fun mace_term (p : int, hs : mace_var horn_set,
	       rho : ''var -m> int set,
	       output : int -m> mace_var) : unit =
    (* Assume truevar is a variable that will always be true in hs,
     and falsevar will always be false in hs;
     rho maps each variable to an element of D = 2^p, i.e., a subset of {1, ..., p}.
     output_var is a p-tuple of variables representing the output of the
     evaluation of the input term. *)
    let val one_to_p = 1 to p
	fun m_term (V x) =
	    (iterate
	       add_horn_clause (hs, SOME (?output bit))
	     | bit in set ?rho x
	     end handle MapGet => raise MaceTerm)
	    else raise MaceTerm
	  | m_term (f $ l) =
	    let val ir = ref 0
	    in
	    end
    in
	m_term
    end;
