cnf_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 "CNF_clause.h"
#include "Logic_or_clause.h"

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

CNF_clause::~CNF_clause() {
	for (clauses_iter iter = clauses.begin(); iter != clauses.end(); iter++)
		delete(* iter);
	clauses.clear();
}

CNF_clause * CNF_clause::clone() {
	CNF_clause * res = new CNF_clause(const_value);
	for (clauses_iter iter = clauses.begin(); iter != clauses.end();
		iter++) {
			res->clauses.push_back((* iter)->clone());
	}
	return res;
}


void CNF_clause::add_or_clause(Logic_or_clause * or_clause) {
	clauses.push_back(or_clause);
}


bool CNF_clause::get_const_value() const {
	assert(clauses.empty()); //fine
	return const_value;
}


void CNF_clause::log_and(CNF_clause * c2) {
	const_value = const_value && c2->const_value;

	clauses.insert(clauses.end(), c2->clauses.begin(), c2->clauses.end()); //add all of c2
	c2->clauses.clear();
	delete c2;
}


/** note: (A1&&A2&&...&&An)||(B1&&B2&&...&&Bm) =
 * (A1||B1) && (A1||B2) && ... && (A1||Bm) && (A2||B1) && ... && (An||Bm) */
void CNF_clause::log_or(CNF_clause * c2) {
	clauses_iter i1, i2;
	list < Logic_or_clause * > tmp;

	if (is_constant()) {
		if (get_const_value()) {
			delete c2;
		} else // copy c2
		{
			const_value = c2->const_value;
			for (clauses_iter iter = clauses.begin();
				iter != clauses.end(); iter++) delete(* iter);
			clauses.clear();
			clauses = c2->clauses;
			c2->clauses.clear();
			delete c2;
		}
		return;
	}
	if (c2->is_constant()) {
		if (c2->get_const_value()) {
			for (clauses_iter iter = clauses.begin();
				iter != clauses.end(); iter++) delete(* iter);
			clauses.clear();
			const_value = true;
			delete c2;
		} else delete c2;
		return;
	}

	tmp = clauses;
	clauses.clear();
	Logic_or_clause * i1entry;
	for (i1 = tmp.begin(); i1 != tmp.end(); i1++) {
		for (i2 = c2->clauses.begin(); i2 != c2->clauses.end(); i2++) {
			i1entry = (* i1)->clone();
			i1entry->merge((* i2)->clone());
			add_or_clause(i1entry);
		}
	}
	for (clauses_iter iter = tmp.begin(); iter != tmp.end(); iter++)
		delete(* iter);
	tmp.clear();
	delete c2;

	simplify();
}


/** invert using ~(C1 && C2 && .. && Cn) = ~C1 || ~C2 || .. || ~Cn */
void CNF_clause::log_not() {
	CNF_clause * not_clause;
	clauses_iter iter;
	list < Logic_or_clause * > tmp;

	//cout << "CNF_clause::NOT(" << c->to_string() << ")"; cout.flush();

	if (is_constant()) {
		const_value = !const_value;
		return;
	}

	const_value = false;
	tmp = clauses;
	clauses.clear();
	for (iter = tmp.begin(); iter != tmp.end(); iter++) {
		not_clause = (* iter)->comp_inverse();
		delete(* iter);
		log_or(not_clause);
	}
	tmp.clear();
	//cout << " ==> " << res->to_string() << endl; cout.flush();
}


void CNF_clause::simplify() {
	clauses_iter iter, iter2;


	//cout << "before simplify: "<< to_string() << endl; cout.flush();

	// simplify all clauses seperately
	for (iter = clauses.begin(); iter != clauses.end(); ) { // had to move iter++ outside
		(* iter)->simplify();
		if ((* iter)->is_constant()) { // clause is always true -> remove
			assert((* iter)->get_const_value()); //???
			delete(* iter);
			iter = clauses.erase(iter); // performs iter++			
		} else iter++;
	}

	//cout << "after step 1:" << to_string() << endl; cout.flush();

	// look for and remove superclauses
	for (iter = clauses.begin(); iter != clauses.end(); iter++) {
		for (iter2 = clauses.begin(); iter2 != clauses.end(); ) {
			if ((iter != iter2) && (* iter)->is_subsum(* iter2)) {
				delete(* iter2);
				iter2 = clauses.erase(iter2);
			} else iter2++;

		}
	}

	//cout << "after step 2:" << to_string() << endl; cout.flush();
}


string CNF_clause::to_string() const {
	string res;
	const_clauses_iter iter, tmp;

	if (is_constant()) {
		if (!get_const_value()) return "FALSE"; else return "TRUE";
	}
	res += "{";
	for (iter = clauses.begin(); iter != clauses.end(); iter++) {
		res += (* iter)->to_string();
		tmp = iter;
		tmp++;
		if (tmp != clauses.end()) res += ", ";
	}
	res += "}";
	return res;
}