/*

  Copyright (c) 1992, 1993
	Regents of the University of California
  All rights reserved.

  Use and copying of this software and preparation of derivative works
  based upon this software are permitted.  However, any distribution of
  this software or derivative works must include the above copyright
  notice.

  This software is made available AS IS, and neither the Electronics
  Research Laboratory or the Universify of California make any
  warranty about the software, its performance or its conformity to
  any specification.

  Author: Szu-Tsung Cheng, stcheng@ic.Berkeley.EDU
	  10/92
	  10/93

  $Header: /projects/development/hsv/CVSRepository/vl2mv/src/parser/vl_resolution.c,v 1.2 2009/03/09 20:25:58 fabio Exp $


*/

#include <stdio.h>
#include <math.h>
#include "util.h"
#include "array.h"
#include "list.h"
#include "st.h"
#include "set.h"
#include "vl_types.h"
#include "vl_defs.h"
#include "vlr_int.h"
#include "vl_fg_defs.h"
#include "vl_create.h"
#include "vl_write.h"
#include "vl_write_util.h"
#include "vl_vardecl.h"

extern int set_notation;
extern int smartEvent;
extern vl_desc *mod_list;
extern int noBus;

FILE *null_file;


void create_mvar_nondeterminism(FILE *file,
				st_table *resultant_vars,
				char *var_name,
				vl_id_range *id_sym,
				int lo, int hi,
				array_t *controls,
				array_t *vars_array)
{
    vl_term *nond_out, *ctrl_i;
    char buf[MAXSTRLEN], buf_new[MAXSTRLEN], buf_old[MAXSTRLEN], *cp, *t;
    var_info *cur_var;
    st_table *vars;
    int i, j, k;
    int idx, idx_lo, idx_hi;
    lsList domain;
    lsGen enum_gen;
    lsHandle enum_handle;
    vl_enumerator *enum_elt;
    array_t *val_array;

    nond_out = new_term(id_sym->range, lo, hi);
    nond_out->flag |= MVar;
    nond_out->term_type = id_sym->id_type;
    domain = id_sym->id_type->specifier->u.enum_type->domain_list;
    write_var_decl(file, nond_out);


    st_insert(resultant_vars, var_name,
	      (char*)create_var_info(vl_copy_id_range(id_sym), nond_out));
    st_lookup(resultant_vars, var_name, (char**)&cur_var);
    cur_var->extra = (void*)controls;

    if (id_sym->range) {
	idx_lo = vl_eval_expr(id_sym->range->left);
	if (id_sym->range->right)
	    idx_hi = vl_eval_expr(id_sym->range->right);
	else
	    idx_hi = idx_lo;
    } else {
	idx_lo = idx_hi = 0;
    }

    for (idx=idx_lo; idx<=idx_hi; idx++) {
	int control_is_tautology;

	control_is_tautology = 0;

	val_array = array_alloc(char*, 0);

	cp = buf; *cp = '\0';
	cp = strappend(cp, ".names ");
	for (i=0; i<array_n(controls); i++) {
	    char tmp_buf[MAXSTRLEN];
	    ctrl_i = array_fetch(vl_term*, controls, i);
	    if (ctrl_i) {
		if (ctrl_i->flag & TautologyTrue)
		    control_is_tautology = 1;

		vars = array_fetch(st_table*, vars_array, i);
		st_lookup(vars, var_name, (char**)&cur_var);
		cp = strappendS(cp, ctrl_i->name->name);
		if (id_sym->range) {
		    sprintf(tmp_buf, "%s%s%d%s",
			    cur_var->current_terminal->name->name,
			    SEP_LARRAY, idx, SEP_RARRAY);
		} else {
		    sprintf(tmp_buf, "%s",
			    cur_var->current_terminal->name->name);
		}
		cp = strappendS(cp, tmp_buf);
		array_insert_last(char*, val_array, vlStrdup(tmp_buf));
	    } else {

		t = WRT_BLIF_MV_DC(null_file,
				   id_sym->id_type->specifier->
				       u.enum_type->domain_list);
		array_insert_last(char*, val_array, vlStrdup(t));
	    }
	}

	if (!control_is_tautology) {

	    strcpy(buf_old, id_sym->name);
	    strip_char(buf_old, SEP_LATCH);
	    if (id_sym->range) {
		sprintf(buf_new, "%s%s%d%s",
			buf_old, SEP_LARRAY, idx, SEP_RARRAY);
	    } else {
		strcpy(buf_new, buf_old);
	    }
	    cp = strappendS(cp, buf_new);
	}

	if (id_sym->range) {
	    sprintf(buf_new, "%s%s%d%s",
		    nond_out->name->name, SEP_LARRAY, idx, SEP_RARRAY);
	    cp = strappendS(cp, buf_new);
	} else {
	    strcpy(buf_new, nond_out->name->name);
	    cp = strappendS(cp, buf_new);
	}

	fprintf(file, "%s\n", buf);

	if (control_is_tautology ||
	    ((id_sym->flags & EventVar) && smartEvent)) {
	    vl_enumerator *enum_elt;

	    lsFirstItem(id_sym->id_type->specifier->u.enum_type->domain_list,
			(lsGeneric*)&enum_elt, 0);
	    fprintf(file, "%s %s\n", HSIS_DEFAULT, enum_elt->name);
	}

	if (set_notation) {

	    for (i=0; i<array_n(controls); i++) {
		ctrl_i = array_fetch(vl_term*, controls, i);
		if (ctrl_i) {
		    for (k=0; k<i; k++) {
			ctrl_i = array_fetch(vl_term*, controls, k);
			if (ctrl_i) fprintf(file,"- - ");
		    }
		    fprintf(file, "1 - ");
		    for (k=i+1; k<array_n(controls); k++) {
			ctrl_i = array_fetch(vl_term*, controls, k);
			if (ctrl_i) fprintf(file, "- - ");
		    }
		    if (!control_is_tautology)
			fprintf(file, "- %s%s\n",
				HSIS_EQUAL,
				array_fetch(char*, val_array, i));
		    else
			fprintf(file, "%s%s\n",
				HSIS_EQUAL,
				array_fetch(char*, val_array, i));
		}
	    }


	    if (!control_is_tautology) {
		for (j=0; j<array_n(controls); j++) {
		    ctrl_i = array_fetch(vl_term*, controls, j);
		    if (ctrl_i) fprintf(file, "0 - ");
		}
		if (id_sym->range) {
		    char id_buf[MAXSTRLEN];
		    sprintf(id_buf, "%s%s%d%s",
			    id_sym->name, SEP_LARRAY, idx, SEP_RARRAY);
		    fprintf(file, "- %s%s\n", HSIS_EQUAL, id_buf);
		} else {
		    fprintf(file, "- %s%s\n", HSIS_EQUAL, id_sym->name);
		}
	    }

	    for (i=0; i<array_n(val_array); i++)
		vl_chk_free(array_fetch(char*, val_array, i));
	} else {

	    for (i=0; i<array_n(controls); i++) {
		for (enum_gen=lsStart(domain);
		     lsNext(enum_gen,
			    (lsGeneric*)&enum_elt,&enum_handle)!=LS_NOMORE;) {
		    ctrl_i = array_fetch(vl_term*, controls, i);
		    if (ctrl_i) {
			for (k=0; k<i; k++) {
			    ctrl_i = array_fetch(vl_term*, controls, k);
			    if (ctrl_i) fprintf(file,"- - ");
			}
			fprintf(file, "1 %s ", enum_elt->name);
			for (k=i+1; k<array_n(controls); k++) {
			    ctrl_i = array_fetch(vl_term*, controls, k);
			    if (ctrl_i) fprintf(file, "- - ");
			}
			fprintf(file, "- %s\n", enum_elt->name);
		    }
		}
		lsFinish(enum_gen);
	    }

	    for (enum_gen=lsStart(domain);
		 lsNext(enum_gen,(lsGeneric*)&enum_elt,&enum_handle)!=
		     LS_NOMORE;) {
		for (j=0; j<array_n(controls); j++) {
		    ctrl_i = array_fetch(vl_term*, controls, j);
		    if (ctrl_i) fprintf(file, "0 - ");
		}
		fprintf(file, "%s %s\n", enum_elt->name, enum_elt->name);
	    }
	    lsFinish(enum_gen);
	}
	array_free(val_array);
    }
}


void create_bin_scalar_nondeterminism(FILE *file,
				      st_table *resultant_vars,
				      char *var_name,
				      vl_id_range *id_sym,
				      array_t *controls,
				      array_t *vars_array)
{
    vl_term *nond_out, *ctrl_i;
    char buf[MAXSTRLEN], buf_new[MAXSTRLEN], buf_old[MAXSTRLEN], *cp;
    var_info *cur_var;
    st_table *vars;
    int i, j, k;
    int idx, idx_lo, idx_hi;

    nond_out = new_term(NIL(vl_range), 0, -1);

    st_insert(resultant_vars, var_name,
	      (char*)create_var_info(vl_copy_id_range(id_sym), nond_out));
    st_lookup(resultant_vars, var_name, (char**)&cur_var);
    nond_out->name->range = id_sym->range;
    nond_out->name->unintType = id_sym->unintType;
    cur_var->extra = (void*)controls;

    if (id_sym->range) {
	idx_lo = vl_eval_expr(id_sym->range->left);
	if (id_sym->range->right)
	    idx_hi = vl_eval_expr(id_sym->range->right);
	else
	    idx_hi = idx_lo;
    } else {
	idx_lo = idx_hi = 0;
    }

    write_var_decl(file, nond_out);

    for (idx=idx_lo; idx<=idx_hi; idx++) {
	int control_is_tautology;

	control_is_tautology = 0;

	cp = buf; *cp = '\0';
	cp = strappend(cp, ".names ");
	for (i=0; i<array_n(controls); i++) {
	    char tmp_buf[MAXSTRLEN];
	    ctrl_i = array_fetch(vl_term*, controls, i);
	    if (ctrl_i) {
		if (!(ctrl_i->flag & ConflictFalse)) {
		    if (ctrl_i->flag & TautologyTrue)
			control_is_tautology = 1;

		    vars = array_fetch(st_table*, vars_array, i);
		    st_lookup(vars, var_name, (char**)&cur_var);
		    cp = strappendS(cp, ctrl_i->name->name);
		    if (id_sym->range) {
			sprintf(tmp_buf, "%s%s%d%s",
				cur_var->current_terminal->name->name,
				SEP_LARRAY, idx, SEP_RARRAY);
			cp = strappendS(cp, tmp_buf);
		    } else {
			sprintf(tmp_buf, "%s",
				cur_var->current_terminal->name->name);
			cp = strappendS(cp, tmp_buf);
		    }
		}
	    } else {

		cp = cp;

	    }
	}

	if (!control_is_tautology &&
	    (!(id_sym->flags & EventVar) || !smartEvent)) {
	    strcpy(buf_old, id_sym->name);
	    strip_char(buf_old, SEP_LATCH);
	    if (id_sym->range) {
		sprintf(buf_new, "%s%s%d%s",
			buf_old, SEP_LARRAY, idx, SEP_RARRAY);
		cp = strappendS(cp, buf_new);
	    } else {
		strcpy(buf_new, buf_old);
		cp = strappendS(cp, buf_new);
	    }
	}

	if (id_sym->range) {
	    sprintf(buf_new, "%s%s%d%s",
		    nond_out->name->name,
		    SEP_LARRAY, idx, SEP_RARRAY);
	    cp = strappendS(cp, buf_new);
	} else {
	    strcpy(buf_new, nond_out->name->name);
	    cp = strappendS(cp, buf_new);
	}

	fprintf(file, "%s\n", buf);

	if (control_is_tautology ||
	    ((id_sym->flags & EventVar) && smartEvent)) {
	    fprintf(file, "%s %d\n", HSIS_DEFAULT, 0);
	}


	for (i=0; i<array_n(controls); i++) {
	    ctrl_i = array_fetch(vl_term*, controls, i);
	    if (ctrl_i) {
		if (!(ctrl_i->flag & ConflictFalse)) {

		    for (j=0; j<= 1; j++) {
			for (k=0; k<i; k++) {
			    ctrl_i = array_fetch(vl_term*, controls, k);
			    if (ctrl_i)
				fprintf(file,"- - ");
			}
			fprintf(file, "1 %d ", j);
			for (k=i+1; k<array_n(controls); k++) {
			    ctrl_i = array_fetch(vl_term*, controls, k);
			    if (ctrl_i)
				fprintf(file, "- - ");
			}
			if (!control_is_tautology &&
			    (!(id_sym->flags & EventVar) ||
			     !smartEvent))
			    fprintf(file, "- %d\n", j);
			else
			    fprintf(file, "%d\n", j);
		    }
		}
	    }
	}

	if (!control_is_tautology) {
	    if (!(id_sym->flags & EventVar) || !smartEvent) {

		for (i=0; i<=1; i++) {
		    for (j=0; j<array_n(controls); j++) {
			ctrl_i = array_fetch(vl_term*, controls, j);
			if (ctrl_i)
			    fprintf(file, "0 - ");
		    }
		    fprintf(file, "%d %d\n", i, i);
		}
	    } else {

		for (j=0; j<array_n(controls); j++) {
		    ctrl_i = array_fetch(vl_term*, controls, j);
		    if (ctrl_i) fprintf(file, "0 - ");
		}
		fprintf(file, "%d\n", 0);
	    }
	}
    }
}


void create_bin_vector_nondeterminism(FILE *file,
				      st_table *resultant_vars,
				      char *var_name,
				      vl_id_range *id_sym,
				      int lo, int hi,
				      array_t *controls,
				      array_t *vars_array)
{
    vl_term *nond_out, *ctrl_i;
    char buf[MAXSTRLEN];
    char buf_tmp[MAXSTRLEN];
    char *cp;
    var_info *cur_var;
    st_table *vars;
    int h, i, j, k;
    int idx, idx_lo, idx_hi;
    char ctrl_terms_buf[MAXSTRLEN], *ctrl_terms_cp;
    char val_terms_buf[MAXSTRLEN], *val_terms_cp;

    nond_out = new_term(id_sym->range, lo, hi);
    write_var_decl(file, nond_out);

    st_insert(resultant_vars, vlStrdup(var_name),
	      (char*)create_var_info(vl_copy_id_range(id_sym), nond_out));
    st_lookup(resultant_vars, var_name, (char**)&cur_var);
    cur_var->extra = (void*)controls;

    if (id_sym->range) {
	idx_lo = vl_eval_expr(id_sym->range->left);
	if (id_sym->range->right)
	    idx_hi = vl_eval_expr(id_sym->range->right);
	else
	    idx_hi = idx_lo;
    } else {
	idx_lo = idx_hi = 0;
    }

    for (idx=idx_lo; idx<=idx_hi; idx++) {
	if (set_notation && !(array_n(controls) <= 1 && noBus)) {
	    char buf_ctrl[MAXSTRLEN], buf_var[MAXSTRLEN];
	    int control_is_tautology;

	    control_is_tautology = 0;

	    cp = buf; *cp = '\0';
	    ctrl_terms_cp = ctrl_terms_buf;  *ctrl_terms_cp = '\0';
	    val_terms_cp = val_terms_buf;  *val_terms_cp = '\0';
	    cp = strappend(cp, ".names ");
	    for (i=0; i<array_n(controls); i++) {
		ctrl_i = array_fetch(vl_term*, controls, i);
		if (ctrl_i) {
		    if (!(ctrl_i->flag & ConflictFalse)) {
			if (ctrl_i->flag & TautologyTrue)
			    control_is_tautology = 1;

			vars = array_fetch(st_table*, vars_array, i);
			st_lookup(vars, var_name, (char**)&cur_var);
			sprintf(buf_ctrl, "%s", ctrl_i->name->name);

			cp = strappendS(cp, buf_ctrl);
			ctrl_terms_cp =
			    strappendS(ctrl_terms_cp, buf_ctrl);
			for (h=lo; h<=hi; h++) {
			    if (!id_sym->range) {
				sprintf(buf_var, "%s%s%d%s",
					cur_var->current_terminal->
					name->name,
					SEP_LBITSELECT, h, SEP_RBITSELECT);
			    } else {
				sprintf(buf_var, "%s%s%d%s%s%d%s",
					cur_var->current_terminal->
					name->name,
					SEP_LARRAY, idx, SEP_RARRAY,
					SEP_LBITSELECT, h, SEP_RBITSELECT);
			    }
			    cp = strappendS(cp, buf_var);
			}
		    }
		} else {

		    cp = cp;

		}
	    }

	    if (!control_is_tautology) {
		for (h=lo; h<=hi; h++) {
		    if (id_sym->range) {
			sprintf(buf_tmp, "%s%s%d%s%s%d%s",
				strip_char(vlStrdup(id_sym->name),SEP_LATCH),
				SEP_LARRAY, idx, SEP_RARRAY,
				SEP_LBITSELECT, h, SEP_RBITSELECT);
		    } else {
			sprintf(buf_tmp, "%s%s%d%s",
				strip_char(vlStrdup(id_sym->name),SEP_LATCH),
				SEP_LBITSELECT, h, SEP_RBITSELECT);
		    }
		    cp = strappendS(cp, buf_tmp);
		}
	    }

	    cp = strappendS(cp, HSIS_ARROW);
	    for (h=lo; h<=hi; h++) {
		if (id_sym->range) {
		    sprintf(buf_tmp, "%s%s%d%s%s%d%s",
			    nond_out->name->name,
			    SEP_LARRAY, idx, SEP_RARRAY,
			    SEP_LBITSELECT, h, SEP_RBITSELECT);
		} else {
		    sprintf(buf_tmp, "%s%s%d%s",
			    nond_out->name->name,
			    SEP_LBITSELECT, h, SEP_RBITSELECT);
		}
		cp = strappendS(cp, buf_tmp);
	    }
	    fprintf(file, "%s\n", buf);

	    if (control_is_tautology ||
		((id_sym->flags & EventVar) && smartEvent)) {
		fprintf(file, "%s", HSIS_DEFAULT);
		for (h=lo; h<=hi; h++)
		    fprintf(file, " %d", 0);
		fprintf(file, "\n");
	    }

	    for (i=0; i<array_n(controls); i++) {
		ctrl_i = array_fetch(vl_term*, controls, i);
		if (ctrl_i) {
		    if (!(ctrl_i->flag & ConflictFalse)) {
			for (k=0; k<i; k++) {
			    ctrl_i = array_fetch(vl_term*,controls,k);
			    if (ctrl_i) {
				fprintf(file,"- ");
				for (h=lo; h<=hi; h++) fprintf(file,"- ");
			    }
			}
			fprintf(file, "1 ");
			for (h=lo; h<=hi; h++) fprintf(file, "- ");
			for (k=i+1; k<array_n(controls); k++) {
			    ctrl_i = array_fetch(vl_term*,controls,k);
			    if (ctrl_i) {
				if (!(ctrl_i->flag & ConflictFalse)) {
				    fprintf(file,"- ");
				    for (h=lo; h<=hi; h++)
					fprintf(file,"- ");
				}
			    }
			}

			if (!control_is_tautology) {
			    for (h=lo; h<=hi; h++) fprintf(file, "- ");
			}

			for (h=lo; h<=hi; h++) {
			    vars = array_fetch(st_table*, vars_array, i);
			    st_lookup(vars, var_name, (char**)&cur_var);
			    if (!id_sym->range) {
				sprintf(buf_var, "%s%s%d%s",
					cur_var->current_terminal->
					name->name,
					SEP_LBITSELECT, h, SEP_RBITSELECT);
			    } else {
				sprintf(buf_var, "%s%s%d%s%s%d%s",
					cur_var->current_terminal->
					name->name,
					SEP_LARRAY, idx, SEP_RARRAY,
					SEP_LBITSELECT, h, SEP_RBITSELECT);
			    }
			    fprintf(file, "%s%s ", HSIS_EQUAL, buf_var);
			}
			fprintf(file, "\n");
		    }
		}
	    }

	    if (!control_is_tautology) {
		for (j=0; j<array_n(controls); j++) {
		    ctrl_i = array_fetch(vl_term*, controls, j);
		    if (ctrl_i) {
			if (!(ctrl_i->flag & ConflictFalse)) {
			    fprintf(file, "0 ");
			    for (h=lo; h<=hi; h++) fprintf(file, "- ");
			}
		    }
		}

		for (h=lo; h<=hi; h++) fprintf(file, "- ");
		for (h=lo; h<=hi; h++) {
		    if (!id_sym->range) {
			sprintf(buf_var, "%s%s%d%s",
				strip_char(vlStrdup(id_sym->name),SEP_LATCH),
				SEP_LBITSELECT, h, SEP_RBITSELECT);
		    } else {
			sprintf(buf_var, "%s%s%d%s%s%d%s",
				strip_char(vlStrdup(id_sym->name),SEP_LATCH),
				SEP_LARRAY, idx, SEP_RARRAY,
				SEP_LBITSELECT, h, SEP_RBITSELECT);
		    }
		    fprintf(file, "%s%s ", HSIS_EQUAL, buf_var);
		}
		fprintf(file, "\n");
	    }
	} else {
	    for (h=lo; h<=hi; h++) {

		cp = buf; *cp = '\0';
		cp = strappend(cp, ".names ");
		for (i=0; i<array_n(controls); i++) {
		    ctrl_i = array_fetch(vl_term*, controls, i);
		    if (ctrl_i) {
			if (!(ctrl_i->flag & ConflictFalse)) {
			    char buf_ctrl[MAXSTRLEN], buf_var[MAXSTRLEN];

			    vars = array_fetch(st_table*, vars_array, i);
			    st_lookup(vars, var_name, (char**)&cur_var);
			    sprintf(buf_ctrl, "%s", ctrl_i->name->name);

			    if (!id_sym->range) {
				sprintf(buf_var, "%s%s%d%s",
					cur_var->current_terminal->
					name->name,
					SEP_LBITSELECT, h, SEP_RBITSELECT);
			    } else {
				sprintf(buf_var, "%s%s%d%s%s%d%s",
					cur_var->current_terminal->
					name->name,
					SEP_LARRAY, idx, SEP_RARRAY,
					SEP_LBITSELECT, h, SEP_RBITSELECT);
			    }
			    cp = strappendS(cp, buf_ctrl);
			    cp = strappendS(cp, buf_var);
			}
		    } else {

			cp = cp;

		    }
		}
		if (id_sym->range) {
		    sprintf(buf_tmp, "%s%s%d%s%s%d%s %s%s%d%s%s%d%s",
			    strip_char(vlStrdup(id_sym->name),SEP_LATCH),
			    SEP_LARRAY, idx, SEP_RARRAY,
			    SEP_LBITSELECT, h, SEP_RBITSELECT,
			    nond_out->name->name,
			    SEP_LARRAY, idx, SEP_RARRAY,
			    SEP_LBITSELECT, h, SEP_RBITSELECT);
		} else {
		    sprintf(buf_tmp, "%s%s%d%s %s%s%d%s",
			    strip_char(vlStrdup(id_sym->name),SEP_LATCH),
			    SEP_LBITSELECT, h, SEP_RBITSELECT,
			    nond_out->name->name,
			    SEP_LBITSELECT, h, SEP_RBITSELECT);
		}
		cp = strappendS(cp, buf_tmp);
		fprintf(file, "%s\n", buf);

		for (i=0; i<array_n(controls); i++) {
		    ctrl_i = array_fetch(vl_term*, controls, i);
		    if (ctrl_i) {
			if (!(ctrl_i->flag & ConflictFalse)) {
			    for (j=0; j<= 1; j++) {
				for (k=0; k<i; k++) {
				    ctrl_i =
					array_fetch(vl_term*,controls,k);
				    if (ctrl_i)
					if (!(ctrl_i->flag&ConflictFalse))
					    fprintf(file,"- - ");
				}
				fprintf(file, "1 %d ", j);
				for (k=i+1; k<array_n(controls); k++) {
				    ctrl_i =
					array_fetch(vl_term*,controls,k);
				    if (ctrl_i)
					if (!(ctrl_i->flag&ConflictFalse))
					    fprintf(file, "- - ");
				}
				fprintf(file, "- %d\n", j);
			    }
			}
		    }
		}

		for (i=0; i<=1; i++) {
		    for (j=0; j<array_n(controls); j++) {
			ctrl_i = array_fetch(vl_term*, controls, j);
			if (ctrl_i)
			    if (!(ctrl_i->flag & ConflictFalse))
				fprintf(file, "0 - ");
		    }
		    fprintf(file, "%d %d\n", i, i);
		}
	    }
	}
    }
}