equivalence_expr.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 "Equivalence_expr.h"
#include "CNF_clause.h"
#include "Bool_number.h"
#include "Globals.h"
#include "Cmd_options.h"

/** A<->B  is equal to  (A && B) || (~A && ~B) */
CNF_clause * Equivalence_expr::compute_CNF() const {
	CNF_clause * l, * r, * notl, * notr;

	l = left->compute_CNF();
	r = right->compute_CNF();

	notl = l->clone();
	notl->log_not();
	notr = r->clone();
	notr->log_not();

	l->log_and(r);
	notl->log_and(notr);
	l->log_or(notl);
	return l;
}

void Equivalence_expr::semantic_checks() {
	left->semantic_checks();
	assert(left->is_logic()); //fine
	right->semantic_checks();
	assert(right->is_logic()); //fine
}

bool Equivalence_expr::is_number() const {
	return left->is_number() && right->is_number();
}

Number * Equivalence_expr::compute_number() const {
	Bool_number * l, * r;

	l = (Bool_number *) left->compute_number();
	r = (Bool_number *) right->compute_number();
	l->equivalence(r);
	return l;
}

string Equivalence_expr::to_matlab() const {
	string s;

	if (globals->cmd_options->all_params_symbolic() || !is_number() ) {
	  s += "~(";
	  s += left->to_matlab();
	  s +=")";
	  s += string(" xor ");
	  s +="(";
	  s += right->to_matlab();
	  s += ")";
	} else {
	  Number *n;
	  n=compute_number();
	  s += n->to_matlab();
	  delete n;
	}

	return s;
}