cnf_clause.h

由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)
*/

#ifndef D_CNF_CLAUSE
#define D_CNF_CLAUSE
#ifndef STD_NS
#define STD_NS
using namespace std;
#endif
#include<list>
#include<string>
class Logic_or_clause;

/** representation of a logic expression in CNF (conjunctive normal form) */
class CNF_clause {
	typedef list < Logic_or_clause * >::iterator clauses_iter;
	typedef list < Logic_or_clause * >::const_iterator const_clauses_iter;

public:
	const list < Logic_or_clause * > * get_or_clauses() const {
		return & clauses;
	}

	/** creates a new, empty CNF_clause with const_value val */
	CNF_clause(bool val = true);

	~CNF_clause();

	CNF_clause * clone();

	/** adds a Logic_or_clause (semantic: logic and of existing
	 * clauses and the new one) */
	void add_or_clause(Logic_or_clause * or_clause);

	/** returns true iff the CNF is constant, i.e. always
	 * true or always false */
	bool is_constant() const { return clauses.empty(); }

	/** if is_constant, get_const_value returns the value of the CNF */
	bool get_const_value() const;


	/** create the logic and of two CNF_clause's */
	void log_and(CNF_clause * c2);

	/** create the logic or of two CNF_clause's */
	void log_or(CNF_clause * c2);

	/** create the logic not of a CNF_clause */
	void log_not();

	/** simplify the CNF */
	void simplify();


	/** output in human-readable form, for debug only */
	string to_string() const;

private:

	/** if the boolean expr is a constant (indicated by
	 * clauses==NULL), then const_value stores this constant */
	bool const_value;

	/** if clauses==NULL, the CNF is a constant (given by const_value) */
	list < Logic_or_clause * > clauses;

	void invert_clause();
};
#endif //D_CNF_CLAUSE