logic_or_clause.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 "Logic_or_clause.h"
#include "Logic_literal.h"
#include "CNF_clause.h"
#include "Var_symbol.h"


Logic_or_clause::Logic_or_clause(bool val = true) {
	const_value = val;
}

Logic_or_clause::~Logic_or_clause() {
	for (literals_iter iter = literals.begin(); iter != literals.end();
		iter++)delete(* iter);
	literals.clear();
}

Logic_or_clause * Logic_or_clause::clone() {
	Logic_or_clause * res;

	res = new Logic_or_clause();
	res->const_value = const_value;
	for (literals_iter iter = literals.begin(); iter != literals.end();
		iter++)res->literals.push_back((* iter)->clone());
	return res;
}


void Logic_or_clause::add_literal(Logic_literal * l) {
	literals.push_back(l);
}

bool Logic_or_clause::is_subsum(const Logic_or_clause * greater) const {
	const_literals_iter this_iter, greater_iter;
	bool found;

	//cout << "checking subsum " << to_string() << " <= " <<
	// greater->to_string() << " ?";

	for (this_iter = literals.begin(); this_iter != literals.end();
		this_iter++) {
			found = false;
			for (greater_iter = greater->literals.begin();
				greater_iter != greater->literals.end();
				greater_iter++) {
					if ((* this_iter)->is_equal(*
						greater_iter)) {
							found = true;
							break;
					}
			}
			if (!found) {
				//cout << "no" << endl;
				return false;
			}
	}
	//cout << "yes" << endl;
	return true;
}


void Logic_or_clause::simplify() {
	literals_iter iter1, iter2;

	for (iter1 = literals.begin(); iter1 != literals.end(); iter1++)
		for (iter2 = iter1, iter2++; iter2 != literals.end(); )
			if ((* iter1)->get_variable() ==
				(* iter2)->get_variable()) {
					if ((* iter1)->get_neg() ==
						(* iter2)->get_neg()) { //literals
							// identical, remove one
							delete(* iter2);
							iter2 = literals.erase(iter2);
					} else {
						// a || ~a   is always true
						for (literals_iter iter
							= literals.begin();
							iter != literals.end();
							iter++) delete(* iter);
						literals.clear();
						const_value = true;
						return;
					}
			} else iter2++;
}


bool Logic_or_clause::is_constant() const {
	return literals.empty();
}

bool Logic_or_clause::get_const_value() const {
	assert(is_constant()); //fine
	assert(const_value); //??? I don't see a reason for const_value to be false
	return const_value;
}


CNF_clause * Logic_or_clause::comp_inverse() const {
	CNF_clause * res;
	Logic_or_clause * lit_as_clause;
	Logic_literal * lit;
	const_literals_iter iter;

	res = new CNF_clause();
	for (iter = literals.begin(); iter != literals.end(); iter++) {
		lit = (* iter)->clone();
		lit->negate();
		lit_as_clause = new Logic_or_clause();
		lit_as_clause->add_literal(lit);
		res->add_or_clause(lit_as_clause);
	}
	return res;
}


void Logic_or_clause::merge(Logic_or_clause * c2) {
	literals.insert(literals.end(), c2->literals.begin(),
		c2->literals.end()); // add all of c2	
}


string Logic_or_clause::to_string() const {
	string res;
	const_literals_iter iter, tmp;

	res += "{";
	for (iter = literals.begin(); iter != literals.end(); iter++) {
		res += (* iter)->to_string();
		tmp = iter;
		tmp++;
		if (tmp != literals.end()) res += ",";
	}
	res += "}";
	return res;
}