logic_or_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_LOGIC_OR_CLAUSE
#define D_LOGIC_OR_CLAUSE
#ifndef STD_NS
#define STD_NS
using namespace std;
#endif

#include <string>
#include <list>

class Logic_literal;
class CNF_clause;

class Logic_or_clause {
public:
	/** creates a new, empty Logic_or_clause */
	Logic_or_clause(bool val = true);

	Logic_or_clause * clone();

	~Logic_or_clause();

	const list < Logic_literal * > * get_literals() const {
		return & literals;
	}


	/** adds a Logic_literal (semantic: logic or of existing
	 * literals and the new one) */
	void add_literal(Logic_literal * l);

	/** simplifies if two literals refer to the same symbol */
	void simplify();

	/** returns true iff there are no literals in the clause
	 * you may want to call simplify before always_true */
	bool is_constant() const;

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

	/** add all elements of c2 */
	void merge(Logic_or_clause * c2);

	/** returns true iff all Literals in 'this' are also in greater
	 * thus, greater -> 'this' */
	bool is_subsum(const Logic_or_clause * greater) const;

	/** invert the clause using ~(A1||A2||..||An)=~A1 && ~A2 &&...&& ~An */
	CNF_clause * comp_inverse() const;


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


private:
	bool const_value;

	list < Logic_literal * > literals;
	typedef list < Logic_literal * >::iterator literals_iter;
	typedef list < Logic_literal * >::const_iterator const_literals_iter;
};
#endif //D_LOGIC_OR_CLAUSE