item.cc

由matlab开发的hybrid系统的描述语言

/*
	HYSDEL
	Copyright (C) 1999-2002  Fabio D. Torrisi

	This file is part of HYSDEL.
    
	HYSDEL 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 of the License, or (at your option) any later version.

	HYSDEL 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 this library; if not, write to the Free Software
	Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA

	CONTACT INFORMATION
	===================
	Fabio D. Torrisi
	ETH Zentrum
	Physikstrasse. 3 ETL,
	CH-8032 Zurich
	Switzerland
	mailto:[e-mail] (preferred)
*/

#include "Item.h"
#include "CNF_clause.h"
#include "MLD_representation.h"
#include <list>
#include <string>
#include <stdio.h>
#include "Logic_or_clause.h"
#include "Logic_literal.h"
#include "Number_expr.h"
#include "Not_expr.h"
#include "Affine_func.h"
#include "Affine_addend.h"
#include "Var_symbol.h"
#include "Neg_expr.h"
#include "Min_max_eps.h"
#include "Param_symbol.h"
#include "Plus_expr.h"
#include "Symbol_table.h"
#include "Variable_expr.h"
#include "Parameter_expr.h"
#include "Cmd_options.h"
#include "Linear_item.h"
#include "Row_information.h"
#include "Counter.h"
#include "Real_number.h"
#include <stdio.h>
#include "Globals.h"
#include "Problem.h"
#include "Problem_handler.h"

class MLD_representation;


Item::Item(const Globals * glob) {
	globals = glob;
	group = -1;
	subgroup = -1;
	unrolled_from = NULL;
	section=NULL;
}

/*
Item::~Item()
{
required.clear();
}
*/

void Item::comp_group_numbers() {
	if (group != -1) // already set
			return;
	if (unrolled_from) {
		assert(unrolled_from->group != -1); //fine
		group = unrolled_from->group;
		subgroup = unrolled_from->subgroup + 1;
		source = unrolled_from->source;
		source_line = unrolled_from->source_line;
	} else {
		group = globals->counter->get_cnt();
		subgroup = 0;
	}
}


string Item::to_string() const {
	string res;

	res += "item defined at line ";
	res += source_line;
	res += ": ";
	res += source;
	res += "\n";
	return res;
}


void Item::cnf_to_mld(const CNF_clause * cnf, MLD_representation * mld,
	int * subind_cnt) const {
		Row_information * info;
		int ineq, clause_cnt;
		list < Logic_or_clause * >::const_iterator clauses;
		list < Logic_literal * >::const_iterator literals;

		clause_cnt = 0;
		for (clauses = cnf->get_or_clauses()->begin();
			clauses != cnf->get_or_clauses()->end(); clauses++) {
				int neg_cnt = 0;
				ineq = mld->new_ineq();
				clause_cnt++;
				info = new Row_information(this, * subind_cnt);
				(* subind_cnt) ++;
				mld->set_info_ineq(ineq, info);
				for (literals = (* clauses)->get_literals()->begin();
					literals != (* clauses)->get_literals()->end();
					literals++) {
						Expr * e;
						if ((* literals)->get_neg()) {
							e = new Number_expr(1.0, globals);
							neg_cnt++;
						} else {
							e = new Number_expr(-1.0, globals);
						}
						mld->set_coeff_ineq_less(ineq,
							(* literals)->get_variable(), e);
				}
				mld->set_coeff_ineq(ineq, NULL,
					new Number_expr(neg_cnt
					- 1.0, globals));
		}
}

void Item::aff_leq_zero_to_mld(const Affine_func * aff,
	MLD_representation * mld, int * subind_cnt) const {
		int ineq;
		list < Affine_addend * >::const_iterator iter;
		Row_information * info;

		ineq = mld->new_ineq();
		info = new Row_information(this, * subind_cnt);
		(* subind_cnt) ++;
		mld->set_info_ineq(ineq, info);
		for (iter = aff->get_addends()->begin();
			iter != aff->get_addends()->end(); iter++) {
				mld->set_coeff_ineq_less(ineq, (* iter)->get_var(),
					(* iter)->get_coeff()->clone());
		}
}


void Item::aff_to_mld_eq(const Var_symbol * lhs, const Affine_func * aff,
	MLD_representation * mld, int * subind_cnt) const {
		list < Affine_addend * >::const_iterator iter;
		Row_information * info;

		info = new Row_information(this, * subind_cnt);
		(* subind_cnt) ++;
		mld->set_info_eq(lhs, info);
		for (iter = aff->get_addends()->begin();
			iter != aff->get_addends()->end(); iter++) {
				mld->set_coeff_eq(lhs, (* iter)->get_var(),
					(* iter)->get_coeff());
		}

}


Min_max_eps * Item::compute_mme_from_aff(const Affine_func * aff) const {
	list < Affine_addend * >::const_iterator iter;
	Expr * min, * max, * eps;
	const Param_symbol * eps_sym;
	const Symbol * eps_found;

	min = new Number_expr(0.0, globals);
	max = new Number_expr(0.0, globals);
	for (iter = aff->get_addends()->begin(); iter != aff->get_addends()->end();
		iter++) {
			min = new Plus_expr(min, (* iter)->find_min(this));
			max = new Plus_expr(max, (* iter)->find_max(this));
	}
	eps_found = globals->symbol_table->find_symbol(MLD_EPSILON_NAME);
	if (!eps_found->is_param_symbol()) {
		string msg;
		char buf[20];
		sprintf(buf, "line %d: ", get_source_line());
		msg = buf;
		msg += string("MLD_epsilon required but is not a parameter");
		globals->problem_handler->process(new Problem(ERROR, msg));
	}
	eps_sym = (const Param_symbol *) eps_found;
	eps = eps_sym->get_value();
	return new Min_max_eps(min, max, eps, globals);
}


void Item::check_mme_tight(const Min_max_eps * user_mme,
	const Min_max_eps * auto_mme) const {
		Expr * amin, * amax, * umin, * umax;
		Real_number * ar, * ur;
		string msg;
		char buf[100];

		amin = auto_mme->get_min();
		amax = auto_mme->get_max();
		umin = user_mme->get_min();
		umax = user_mme->get_max();
		if (amin->is_number() && umin->is_number()) {
			ar = (Real_number *) (amin->compute_number());
			ur = (Real_number *) (umin->compute_number());
			if (ar->get_double() > ur->get_double()) {
				sprintf(buf, "line %d: ", get_source_line());
				msg = buf;
				msg += string("Lower bound not tight (is ") +
					umin->get_source() +
					string(" = ") + ur->to_matlab() +
					string(", could be ") +
					ar->to_matlab() + string(")");
				globals->problem_handler->process(
					new Problem(WARNING, msg,
					BOUND_NOT_TIGHT));
			}
			delete ar;
			delete ur;
		}
		if (amax->is_number() && umax->is_number()) {
			ar = (Real_number *) (amax->compute_number());
			ur = (Real_number *) (umax->compute_number());
			if (ar->get_double() < ur->get_double()) {
				sprintf(buf, "line %d: ", get_source_line());
				msg = buf;
				msg += string("Upper bound not tight (is ") +
					umax->get_source() +
					string(" = ") + ur->to_matlab() +
					string(", could be ") +
					ar->to_matlab() + string(")");
				globals->problem_handler->process(
					new Problem(WARNING, msg,
					BOUND_NOT_TIGHT));
			}
			delete ar;
			delete ur;
		}
		delete amin;
		delete amax;
		delete umin;
		delete umax;
}


/** we distinguish the following cases:
 * 1) it is neither a constant nor simply a variable: unroll as logic
if it is a negated variable and B5D5: set -1 in variable, 1 in const
 * 2) it is just a variable: do not unroll, set a 1 in the MLD matrix
 * 4) it is a constant and false: create a row of zeros
 * 5) it is a constant and true: a) if consts_in_eq_as_B5D5: set a 1 in B5/D5
 * b) if consts_in_eq_as_auxVar: do as if in case 1
 * c) if consts_in_eq_as_error: report error */
void // ptr to const Symbol*
	Item::construct_logic_eq(const Expr * logic, const Symbol * * upd_var,
	Expr * * upd_var_assign, bool * const_value,
	Symbol_table * sym_tab) const {

		CNF_clause * cnf;

		assert(logic->is_logic()); //fine

		if (logic->is_variable_expr()) {
			* upd_var = ((Variable_expr *) logic)->get_value();
			* upd_var_assign = NULL;
			*const_value=true;
			return;
		}
		
		if (logic->is_not_expr() && globals->cmd_options->consts_in_eq_as_B5D5()) {
		  const Expr *child=((Not_expr*)logic)->get_child();
		  if (child->is_variable_expr()) {
		    *upd_var=((const Variable_expr*)child)->get_value();
		    *upd_var_assign = NULL;
		    *const_value=false;
		    return;
		  }
		}
		
		cnf = logic->compute_CNF();
		if (!cnf->is_constant() ||
			(cnf->is_constant() && cnf->get_const_value() &&
			globals->cmd_options->consts_in_eq_as_auxvar())) {
				* upd_var = sym_tab->create_additional(AUX_KIND, BOOL_TYPE);
				* upd_var_assign = logic->clone();
				*const_value=true;
				return;
		}
		// it is a constant
		* upd_var_assign = NULL;
		if (cnf->get_const_value()) {
			if (globals->cmd_options->consts_in_eq_as_error()) {
				string msg;
				char buf[20];
				sprintf(buf, "line %d: ", get_source_line());
				msg = buf;
				msg += string("Logic expression in equality is always true, resulting in a constant term");
				globals->problem_handler->process(
					new Problem(ERROR, msg));
			}
			if (globals->cmd_options->consts_in_eq_as_B5D5()) {
				* upd_var = NULL;
				* const_value = true;
			}
		} else {
			* upd_var = NULL;
			* const_value = false;
		}
}


Linear_item * Item::extract_const_from_aff(const Expr * affine_expr,
	Expr * * lin_expr) const {
		Linear_item * cnst_item = NULL;
		Expr * lin_part;
		Affine_func * aff;
		Affine_addend * cnst_add;
		Var_symbol * add_var;

		aff = affine_expr->compute_affine();
		cnst_add = aff->remove_const();
		if (cnst_add) {
			add_var = (Var_symbol *)
				globals->symbol_table->create_additional(
				AUX_KIND, REAL_TYPE);
			cnst_item = new Linear_item(add_var, cnst_add->to_expr(),
				globals);
			delete cnst_add;
			lin_part = aff->to_expr();
			delete aff;
			// was a bug: I modified local pointer
			* lin_expr = new
				Plus_expr(lin_part,
				new Variable_expr(add_var, globals));
		} else {
		  *lin_expr = affine_expr->clone();
		}
		return cnst_item;
}


list < Item * > Item::unroll() {
	return list < Item * > ();
}


void Item::add_required(list < const Var_symbol * > & required,
	const Expr * e) {
		const Var_symbol * s = NULL;

		if (e->is_variable_expr())
			s = ((const Variable_expr *) e)->get_value();
		//	if (e->is_parameter_expr())
		//		s=((const Parameter_expr*)e)->get_value();
		if (s) {
			if (!is_required(required, s)) required.push_back(s);
		}
		if (e->is_unary_expr())
			add_required(required,
				((const Unary_expr *) e)->get_child());
		if (e->is_binary_expr()) {
			add_required(required,
				((const Binary_expr *) e)->get_left());
			add_required(required,
				((const Binary_expr *) e)->get_right());
		}
}

void Item::add_required(list < const Var_symbol * > & required,
	const Min_max_eps * mme) {
		const Expr * e;
		if (mme) {
			e = mme->get_min();
			if (e) add_required(required, e);
			e = mme->get_max();
			if (e) add_required(required, e);
			e = mme->get_eps();
			if (e) add_required(required, e);
		}
}

bool Item::is_required_simu(const Var_symbol * s) const {
	list < const Var_symbol * > required;
	required = get_required_simu();
	return is_required(required, s);
}


bool Item::is_required(list < const Var_symbol * > required,
	const Var_symbol * s) {
		for (list < const Var_symbol * >::const_iterator iter =
			required.begin(); iter != required.end(); iter++) {
				if ((* iter) == s) return true;
		}
		return false;
}

string Item::get_source_line_str() const
{
  char buf[20];
  sprintf(buf, "%d", source_line);
  return string(buf);
}

void Item::set_unrolled_from(Item * i) 
{ 
  source=i->source;
  source_line=i->source_line;
  section=i->section;
  unrolled_from = i; 
}