%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  This is a rough approximation to the algorithm presented in:
%
%	"An Algorithm for NAND Decomposition Under Network Constraints,"
%	IEEE Trans. Comp., vol C-18, no. 12, Dec. 1969, p. 1098
%	by E. S. Davidson.
%
%  Written by Bruce Holmer
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  I have used the paper's terminology for names used in the program.
%
%  The data structure for representing functions and variables is
%		function(FunctionNumber, TrueSet, FalseSet,
%			ConceivableInputs,
%			ImmediatePredecessors, ImmediateSuccessors,
%			Predecessors, Successors)
%
%
%  Common names used in the program:
%
%	NumVars		number of variables (signal inputs)
%	NumGs		current number of variables and functions
%	Gs		list of variable and function data
%	Gi,Gj,Gk,Gl	individual variable or function--letter corresponds to
%			the subscript in the paper (most of the time)
%	Vector,V	vector from a function's true set
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

main :- main(0).

main(N) :-
	init_state(N, NumVars, NumGs, Gs),
	add_necessary_functions(NumVars, NumGs, Gs, NumGs2, Gs2),
	test_bounds(NumVars, NumGs2, Gs2),
	search(NumVars, NumGs2, Gs2).
main(_) :-
	write('Search completed'), nl.

%  Test input
%  init_state(circuit(NumInputs, NumOutputs, FunctionList))
init_state(0, 2, 3, [		% 2 input xor
		function(2, [1,2], [0,3], [], [], [], [], []),
		function(1, [2,3], [0,1], [], [], [], [], []),
		function(0, [1,3], [0,2], [], [], [], [], [])
		]) :-
	update_bounds(_, 100, _).
init_state(1, 3, 4, [		% carry circuit
		function(3, [3,5,6,7], [0,1,2,4], [], [], [], [], []),
		function(2, [4,5,6,7], [0,1,2,3], [], [], [], [], []),
		function(1, [2,3,6,7], [0,1,4,5], [], [], [], [], []),
		function(0, [1,3,5,7], [0,2,4,6], [], [], [], [], [])
		]) :-
	update_bounds(_, 100, _).
init_state(2, 3, 4, [		% example in paper
		function(3, [1,2,4,6,7], [0,3,5], [], [], [], [], []),
		function(2, [4,5,6,7], [0,1,2,3], [], [], [], [], []),
		function(1, [2,3,6,7], [0,1,4,5], [], [], [], [], []),
		function(0, [1,3,5,7], [0,2,4,6], [], [], [], [], [])
		]) :-
	update_bounds(_, 100, _).
init_state(3, 3, 4, [		% sum (3 input xor)
		function(3, [1,2,4,7], [0,3,5,6], [], [], [], [], []),
		function(2, [4,5,6,7], [0,1,2,3], [], [], [], [], []),
		function(1, [2,3,6,7], [0,1,4,5], [], [], [], [], []),
		function(0, [1,3,5,7], [0,2,4,6], [], [], [], [], [])
		]) :-
	update_bounds(_, 100, _).
init_state(4, 3, 5, [		% do sum and carry together
		function(4, [3,5,6,7], [0,1,2,4], [], [], [], [], []),
		function(3, [1,2,4,7], [0,3,5,6], [], [], [], [], []),
		function(2, [4,5,6,7], [0,1,2,3], [], [], [], [], []),
		function(1, [2,3,6,7], [0,1,4,5], [], [], [], [], []),
		function(0, [1,3,5,7], [0,2,4,6], [], [], [], [], [])
		]) :-
	update_bounds(_, 100, _).
init_state(5, 5, 8, [		% 2 bit full adder
		function(7,		% A2 (output)
			[1,3,4,6,9,11,12,14,16,18,21,23,24,26,29,31],
			[0,2,5,7,8,10,13,15,17,19,20,22,25,27,28,30],
			[], [], [], [], []),
		function(6,		% B2 (output)
			[2,3,5,6,8,9,12,15,17,18,20,21,24,27,30,31],
			[0,1,4,7,10,11,13,14,16,19,22,23,25,26,28,29],
			[], [], [], [], []),
		function(5,		% carry-out (output)
			[7,10,11,13,14,15,19,22,23,25,26,27,28,29,30,31],
			[0,1,2,3,4,5,6,8,9,12,16,17,18,20,21,24],
			[], [], [], [], []),
		function(4,		% carry-in
			[16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31],
			[0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15],
			[], [], [], [], []),
		function(3,		% B1 input
			[8,9,10,11,12,13,14,15,24,25,26,27,28,29,30,31],
			[0,1,2,3,4,5,6,7,16,17,18,19,20,21,22,23],
			[], [], [], [], []),
		function(2,		% B0 input
			[4,5,6,7,12,13,14,15,20,21,22,23,28,29,30,31],
			[0,1,2,3,8,9,10,11,16,17,18,19,24,25,26,27],
			[], [], [], [], []),
		function(1, 		% A1 input
			[2,3,6,7,10,11,14,15,18,19,22,23,26,27,30,31],
			[0,1,4,5,8,9,12,13,16,17,20,21,24,25,28,29],
			[], [], [], [], []),
		function(0,		% A0 input
			[1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31],
			[0,2,4,6,8,10,12,14,16,18,20,22,24,26,28,30],
			[], [], [], [], [])
		]) :-
	update_bounds(_, 21, _).


%  Iterate over all the TRUE vectors that need to be covered.
%  If no vectors remain to be covered (select_vector fails), then
%  the circuit is complete (printout results, update bounds, and
%  continue search for a lower cost circuit).
search(NumVars, NumGsIn, GsIn) :-
	select_vector(NumVars, NumGsIn, GsIn, Gj, Vector), !,
	cover_vector(NumVars, NumGsIn, GsIn, Gj, Vector, NumGs, Gs),
	add_necessary_functions(NumVars, NumGs, Gs, NumGsOut, GsOut),
	test_bounds(NumVars, NumGsOut, GsOut),
	search(NumVars, NumGsOut, GsOut).
search(NumVars, NumGs, Gs) :-
	output_results(NumVars, NumGs, Gs),
	update_bounds(NumVars, NumGs, Gs),
	fail.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Given the current solution, pick the best uncovered TRUE vector
%  for covering next.
%  The selected vector is specified by its vector number and function.
%  Select_vector fails if all TRUE vectors are covered.
%  Select_vector is determinant (gives only one solution).
select_vector(NumVars, NumGs, Gs, Gj, Vector) :-
	select_vector(Gs, NumVars, NumGs, Gs,
		dummy, 0, nf, 999, Gj, Vector, Type, _), !,
	\+ Type = cov,
	\+ Type = nf.

% loop over functions
select_vector([Gk|_], NumVars, _, _, Gj, V, Type, N, Gj, V, Type, N) :-
	function_number(Gk, K),
	K < NumVars.
select_vector([Gk|Gks], NumVars, NumGs, Gs,
		GjIn, Vin, TypeIn, Nin, GjOut, Vout, TypeOut, Nout) :-
	function_number(Gk, K),
	K >= NumVars,
	true_set(Gk, Tk),
	select_vector(Tk, Gk, NumVars, NumGs, Gs,
		GjIn, Vin, TypeIn, Nin, Gj, V, Type, N),
	select_vector(Gks, NumVars, NumGs, Gs,
		Gj, V, Type, N, GjOut, Vout, TypeOut, Nout).
	
% loop over vectors
select_vector([], _, _, _, _, Gj, V, Type, N, Gj, V, Type, N).
select_vector([V|Vs], Gk, NumVars, NumGs, Gs,
		GjIn, Vin, TypeIn, Nin, GjOut, Vout, TypeOut, Nout) :-
	vector_cover_type(NumVars, Gs, Gk, V, Type, N),
	best_vector(GjIn, Vin, TypeIn, Nin,
			Gk, V, Type, N,
			Gj2, V2, Type2, N2),
	select_vector(Vs, Gk, NumVars, NumGs, Gs,
		Gj2, V2, Type2, N2, GjOut, Vout, TypeOut, Nout).

vector_cover_type(NumVars, Gs, Gj, Vector, Type, NumCovers) :-
	immediate_predecessors(Gj, IPs),
	conceivable_inputs(Gj, CIs),
	false_set(Gj, Fj),
	cover_type1(IPs, Gs, Vector, nf, 0, T, N),
	cover_type2(CIs, Gs, NumVars, Fj, Vector, T, N, Type, NumCovers).

cover_type1([], _, _, T, N, T, N).
cover_type1([I|IPs], Gs, V, TypeIn, Nin, TypeOut, Nout) :-
	function(I, Gs, Gi),
	true_set(Gi, Ti),
	\+ set_member(V, Ti), !,
	false_set(Gi, Fi),
	(set_member(V, Fi) ->
		max_type(TypeIn, cov, Type);
		max_type(TypeIn, exp, Type)),
	N is Nin + 1,
	cover_type1(IPs, Gs, V, Type, N, TypeOut, Nout).
cover_type1([_|IPs], Gs, V, TypeIn, Nin, TypeOut, Nout) :-
	cover_type1(IPs, Gs, V, TypeIn, Nin, TypeOut, Nout).

cover_type2([], _, _, _, _, T, N, T, N).
cover_type2([I|CIs], Gs, NumVars, Fj, V, TypeIn, Nin, TypeOut, Nout) :-
	I < NumVars,
	function(I, Gs, Gi),
	false_set(Gi, Fi),
	set_member(V, Fi), !,
	max_type(TypeIn, var, Type),
	N is Nin + 1,
	cover_type2(CIs, Gs, NumVars, Fj, V, Type, N, TypeOut, Nout).
cover_type2([I|CIs], Gs, NumVars, Fj, V, TypeIn, Nin, TypeOut, Nout) :-
	I >= NumVars,
	function(I, Gs, Gi),
	true_set(Gi, Ti),
	\+ set_member(V, Ti), !,
	false_set(Gi, Fi),
	(set_member(V, Fi) ->
		(set_subset(Fj, Ti) ->
			max_type(TypeIn, fcn, Type);
			max_type(TypeIn, mcf, Type));
		(set_subset(Fj, Ti) ->
			max_type(TypeIn, exf, Type);
			max_type(TypeIn, exmcf, Type))),
	N is Nin + 1,
	cover_type2(CIs, Gs, NumVars, Fj, V, Type, N, TypeOut, Nout).
cover_type2([_|CIs], Gs, NumVars, Fj, V, TypeIn, Nin, TypeOut, Nout) :-
	cover_type2(CIs, Gs, NumVars, Fj, V, TypeIn, Nin, TypeOut, Nout).

%  The best vector to cover is the one with worst type, or, if types
%  are equal, with the least number of possible covers.
best_vector(dummy, _, _, _, Gj2, V2, Type2, N2, Gj2, V2, Type2, N2) :- !.
best_vector(Gj1, V1, Type1, N1, dummy, _, _, _, Gj1, V1, Type1, N1) :- !.
best_vector(Gj1, V1, Type, N1, Gj2, _, Type, N2, Gj1, V1, Type, N1) :-
	function_number(Gj1, J), function_number(Gj2, J),
	N1 < N2, !.
best_vector(Gj1, _, Type, N1, Gj2, V2, Type, N2, Gj2, V2, Type, N2) :-
	function_number(Gj1, J), function_number(Gj2, J),
	N1 >= N2, !.
best_vector(Gj1, V1, Type, N1, Gj2, _, Type, _, Gj1, V1, Type, N1) :-
	(Type = exp ; Type = var),
	function_number(Gj1, J1), function_number(Gj2, J2),
	J1 > J2, !.
best_vector(Gj1, _, Type, _, Gj2, V2, Type, N2, Gj2, V2, Type, N2) :-
	(Type = exp ; Type = var),
	function_number(Gj1, J1), function_number(Gj2, J2),
	J1 < J2, !.
best_vector(Gj1, V1, Type, N1, Gj2, _, Type, _, Gj1, V1, Type, N1) :-
	\+ (Type = exp ; Type = var),
	function_number(Gj1, J1), function_number(Gj2, J2),
	J1 < J2, !.
best_vector(Gj1, _, Type, _, Gj2, V2, Type, N2, Gj2, V2, Type, N2) :-
	\+ (Type = exp ; Type = var),
	function_number(Gj1, J1), function_number(Gj2, J2),
	J1 > J2, !.
best_vector(Gj1, V1, Type1, N1, _, _, Type2, _, Gj1, V1, Type1, N1) :-
	type_order(Type2, Type1), !.
best_vector(_, _, Type1, _, Gj2, V2, Type2, N2, Gj2, V2, Type2, N2) :-
	type_order(Type1, Type2), !.

max_type(T1, T2, T1) :- type_order(T1, T2), !.
max_type(T1, T2, T2) :- \+ type_order(T1, T2), !.

%  Order of types

type_order(cov, exp).
type_order(cov, var).
type_order(cov, fcn).
type_order(cov, mcf).
type_order(cov, exf).
type_order(cov, exmcf).
type_order(cov, nf).
type_order(exp, var).
type_order(exp, fcn).
type_order(exp, mcf).
type_order(exp, exf).
type_order(exp, exmcf).
type_order(exp, nf).
type_order(var, fcn).
type_order(var, mcf).
type_order(var, exf).
type_order(var, exmcf).
type_order(var, nf).
type_order(fcn, mcf).
type_order(fcn, exf).
type_order(fcn, exmcf).
type_order(fcn, nf).
type_order(mcf, exf).
type_order(mcf, exmcf).
type_order(mcf, nf).
type_order(exf, exmcf).
type_order(exf, nf).
type_order(exmcf, nf).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%  Cover_vector will cover the specified vector and
%  generate new circuit information.
%  Using backtracking, all possible coverings are generated.
%  The ordering of the possible coverings is approximately that
%  given in Davidson's paper, but has been simplified.

cover_vector(NumVars, NumGsIn, GsIn, Gj, Vector, NumGsOut, GsOut) :-
	immediate_predecessors(Gj, IPs),
	conceivable_inputs(Gj, CIs),
	vector_types(Type),
	cover_vector(Type, IPs, CIs, Gj, Vector, NumVars, NumGsIn, GsIn,
		NumGsOut, GsOut).
	
vector_types(var).
vector_types(exp).
vector_types(fcn).
vector_types(mcf).
vector_types(exf).
vector_types(exmcf).
vector_types(nf).

cover_vector(exp, [I|_], _, Gj, V, _, NumGs, GsIn, NumGs, GsOut) :-
	function(I, GsIn, Gi),
	true_set(Gi, Ti),
	\+ set_member(V, Ti),
	update_circuit(GsIn, Gi, Gj, V, GsIn, GsOut).
cover_vector(exp, [_|IPs], _, Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	cover_vector(exp, IPs, _, Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut).
cover_vector(var, _, [I|_], Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	I < NumVars,
	function(I, GsIn, Gi),
	false_set(Gi, Fi),
	set_member(V, Fi),
	update_circuit(GsIn, Gi, Gj, V, GsIn, GsOut).
cover_vector(var, _, [_|CIs], Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	cover_vector(var, _, CIs, Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut).
cover_vector(fcn, _, [I|_], Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	I >= NumVars,
	function(I, GsIn, Gi),
	false_set(Gi, Fi),
	set_member(V, Fi),
	true_set(Gi, Ti),
	false_set(Gj, Fj),
	set_subset(Fj, Ti),
	update_circuit(GsIn, Gi, Gj, V, GsIn, GsOut).
cover_vector(fcn, _, [_|CIs], Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	cover_vector(fcn, _, CIs, Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut).
cover_vector(mcf, _, [I|_], Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	I >= NumVars,
	function(I, GsIn, Gi),
	false_set(Gi, Fi),
	set_member(V, Fi),
	true_set(Gi, Ti),
	false_set(Gj, Fj),
	\+ set_subset(Fj, Ti),
	update_circuit(GsIn, Gi, Gj, V, GsIn, GsOut).
cover_vector(mcf, _, [_|CIs], Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	cover_vector(mcf, _, CIs, Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut).
cover_vector(exf, _, [I|_], Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	I >= NumVars,
	function(I, GsIn, Gi),
	false_set(Gi, Fi),
	\+ set_member(V, Fi),
	true_set(Gi, Ti),
	\+ set_member(V, Ti),
	false_set(Gj, Fj),
	set_subset(Fj, Ti),
	update_circuit(GsIn, Gi, Gj, V, GsIn, GsOut).
cover_vector(exf, _, [_|CIs], Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	cover_vector(exf, _, CIs, Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut).
cover_vector(exmcf, _, [I|_], Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	I >= NumVars,
	function(I, GsIn, Gi),
	false_set(Gi, Fi),
	\+ set_member(V, Fi),
	true_set(Gi, Ti),
	\+ set_member(V, Ti),
	false_set(Gj, Fj),
	\+ set_subset(Fj, Ti),
	update_circuit(GsIn, Gi, Gj, V, GsIn, GsOut).
cover_vector(exmcf, _, [_|CIs], Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut) :-
	cover_vector(exmcf, _, CIs, Gj, V, NumVars, NumGs, GsIn, NumGs, GsOut).
cover_vector(nf, _, _, Gj, V, NumVars, NumGsIn, GsIn, NumGsOut, GsOut) :-
	NumGsOut is NumGsIn + 1,
	false_set(Gj, Fj),
	new_function_CIs(GsIn,
		function(NumGsIn,Fj,[V],[],[],[],[],[]),
		NumVars, Gs, Gi),
	update_circuit(Gs, Gi, Gj, V, Gs, GsOut).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

update_circuit([], _, _, _, _, []).
update_circuit([function(K,Tk,Fk,CIk,IPk,ISk,Pk,Sk)|GsIn],
		Gi, Gj, V, Gs,
		[function(K,Tko,Fko,CIko,IPko,ISko,Pko,Sko)|GsOut]) :-
	Gi = function(I,_,Fi,_,IPi,ISi,Pi,_),
	Gj = function(J,_,Fj,_,_,_,_,Sj),
	set_union([I], Pi, PiI),
	set_union([J], Sj, SjJ),
	(K = J ->
		set_union(Tk, Fi, Tk2);
		Tk2 = Tk),
	(K = I ->
		set_union(Tk2, Fj, Tk3);
		Tk3 = Tk2),
	((set_member(K, IPi); set_member(K, ISi)) ->
		set_union(Tk3, [V], Tko);
		Tko = Tk3),
	(K = I ->
		set_union(Fk, [V], Fko);
		Fko = Fk),
	((set_member(K, Pi); K = I) ->
		set_difference(CIk, SjJ, CIk2);
		CIk2 = CIk),
	((set_member(I, CIk), set_member(V, Fk)) ->
		set_difference(CIk2, [I], CIk3);
		CIk3 = CIk2),
	(K = I ->
		exclude_if_vector_in_false_set(CIk3, Gs, V, CIk4);
		CIk4 = CIk3),
	(K = J ->
		set_difference(CIk4, [I], CIko);
		CIko = CIk4),
	(K = J ->
		set_union(IPk, [I], IPko);
		IPko = IPk),
	(K = I ->
		set_union(ISk, [J], ISko);
		ISko = ISk),
	(set_member(K, SjJ) ->
		set_union(Pk, PiI, Pko);
		Pko = Pk),
	(set_member(K, PiI) ->
		set_union(Sk, SjJ, Sko);
		Sko = Sk),
	update_circuit(GsIn, Gi, Gj, V, Gs, GsOut).

exclude_if_vector_in_false_set([], _, _, []).
exclude_if_vector_in_false_set([K|CIsIn], Gs, V, CIsOut) :-
	function(K, Gs, Gk),
	false_set(Gk, Fk),
	set_member(V, Fk), !,
	exclude_if_vector_in_false_set(CIsIn, Gs, V, CIsOut).
exclude_if_vector_in_false_set([K|CIsIn], Gs, V, [K|CIsOut]) :-
	exclude_if_vector_in_false_set(CIsIn, Gs, V, CIsOut).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

add_necessary_functions(NumVars, NumGsIn, GsIn, NumGsOut, GsOut) :-
	add_necessary_functions(NumVars, NumVars, NumGsIn, GsIn,
					NumGsOut, GsOut).

add_necessary_functions(NumGs, _, NumGs, Gs, NumGs, Gs) :- !.
add_necessary_functions(K, NumVars, NumGsIn, GsIn, NumGsOut, GsOut) :-
	function(K, GsIn, Gk),
	function_type(NumVars, NumGsIn, GsIn, Gk, nf, V), !,
	false_set(Gk, Fk),
	new_function_CIs(GsIn,
		function(NumGsIn,Fk,[V],[],[],[],[],[]),
		NumVars, Gs, Gl),
	function(K, Gs, Gk1),
	update_circuit(Gs, Gl, Gk1, V, Gs, Gs1),
	NumGs1 is NumGsIn + 1,
	K1 is K + 1,
	add_necessary_functions(K1, NumVars, NumGs1, Gs1, NumGsOut, GsOut).
add_necessary_functions(K, NumVars, NumGsIn, GsIn, NumGsOut, GsOut) :-
	K1 is K + 1,
	add_necessary_functions(K1, NumVars, NumGsIn, GsIn, NumGsOut, GsOut).

new_function_CIs(GsIn, function(L,Tl,Fl,_,IPl,ISl,Pl,Sl), NumVars,
		[GlOut|GsOut], GlOut) :-
	new_function_CIs(GsIn, L, Fl, NumVars, GsOut, [], CIlo),
	GlOut = function(L,Tl,Fl,CIlo,IPl,ISl,Pl,Sl).
	
new_function_CIs([], _, _, _, [], CIl, CIl).
new_function_CIs([function(K,Tk,Fk,CIk,IPk,ISk,Pk,Sk)|GsIn], L, Fl, NumVars,
		[function(K,Tk,Fk,CIko,IPk,ISk,Pk,Sk)|GsOut], CIlIn, CIlOut) :-
	set_intersection(Fl, Fk, []), !,
	(K >= NumVars ->
		set_union(CIk, [L], CIko);
		CIko = CIk),
	new_function_CIs(GsIn, L, Fl, NumVars, GsOut, [K|CIlIn], CIlOut).
new_function_CIs([Gk|GsIn], L, Fl, NumVars, [Gk|GsOut], CIlIn, CIlOut) :-
	new_function_CIs(GsIn, L, Fl, NumVars, GsOut, CIlIn, CIlOut).

function_type(NumVars, NumGs, Gs, Gk, Type, Vector) :-
	true_set(Gk, Tk),
	select_vector(Tk, Gk, NumVars, NumGs, Gs,
		dummy, 0, nf, 999, _, Vector, Type, _).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Cost and constraint predicates:

% very simple bound for now

test_bounds(_, NumGs, _) :-
	access(bound, Bound),
	NumGs < Bound.

update_bounds(_, NumGs, _) :-
	set(bound, NumGs).

% set and access for systems that don't support them
set(N, A) :-
	(recorded(N, _, Ref) -> erase(Ref) ; true),
	recorda(N, A, _).

access(N, A) :-
	recorded(N, A, _).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Output predicates:

%  for now just dump everything

output_results(NumVars, NumGs, Gs) :-
	NumGates is NumGs - NumVars,
	write(NumGates), write(' gates'), nl,
	write_gates(Gs), nl,
	write('searching for a better solution...'), nl, nl.

write_gates([]).
write_gates([Gi|Gs]) :-
	function_number(Gi, I),
	write('gate #'), write(I), write(' inputs:   '),
	immediate_predecessors(Gi, IPi),
	write(IPi), nl,
	write_gates(Gs).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%  Retrieve the specified function from the function list.
%  function(FunctionNumber, FunctionList, Function).
function(I, [Gi|_], Gi) :- function_number(Gi, I), !.
function(I, [_|Gs], Gi) :- function(I, Gs, Gi).

function_number(        function(I,_,_,_,_,_,_,_), I).
true_set(               function(_,T,_,_,_,_,_,_), T).
false_set(              function(_,_,F,_,_,_,_,_), F).
conceivable_inputs(     function(_,_,_,CI,_,_,_,_), CI).
immediate_predecessors( function(_,_,_,_,IP,_,_,_), IP).
immediate_successors(   function(_,_,_,_,_,IS,_,_), IS).
predecessors(           function(_,_,_,_,_,_,P,_), P).
successors(             function(_,_,_,_,_,_,_,S), S).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Set operations assume that the sets are represented by an ordered list
%  of integers.

set_union([],     [],     []).
set_union([],     [X|L2], [X|L2]).
set_union([X|L1], [],     [X|L1]).
set_union([X|L1], [X|L2], [X|L3]) :-        set_union(L1, L2,     L3).
set_union([X|L1], [Y|L2], [X|L3]) :- X < Y, set_union(L1, [Y|L2], L3).
set_union([X|L1], [Y|L2], [Y|L3]) :- X > Y, set_union([X|L1], L2, L3).

set_intersection([],     [],     []).
set_intersection([],     [_|_],  []).
set_intersection([_|_],  [],     []).
set_intersection([X|L1], [X|L2], [X|L3]) :-    set_intersection(L1, L2,     L3).
set_intersection([X|L1], [Y|L2], L3) :- X < Y, set_intersection(L1, [Y|L2], L3).
set_intersection([X|L1], [Y|L2], L3) :- X > Y, set_intersection([X|L1], L2, L3).

set_difference([],     [],     []).
set_difference([],     [_|_],  []).
set_difference([X|L1], [],     [X|L1]).
set_difference([X|L1], [X|L2], L3) :-            set_difference(L1, L2,     L3).
set_difference([X|L1], [Y|L2], [X|L3]) :- X < Y, set_difference(L1, [Y|L2], L3).
set_difference([X|L1], [Y|L2], L3) :-     X > Y, set_difference([X|L1], L2, L3).

set_subset([],     _).
set_subset([X|L1], [X|L2]) :-        set_subset(L1, L2).
set_subset([X|L1], [Y|L2]) :- X > Y, set_subset([X|L1], L2).

set_member(X, [X|_]).
set_member(X, [Y|T]) :- X > Y, set_member(X, T).