00001 /* 00002 00003 Copyright (C) 2000, 2001 Silicon Graphics, Inc. All Rights Reserved. 00004 00005 This program is free software; you can redistribute it and/or modify it 00006 under the terms of version 2 of the GNU General Public License as 00007 published by the Free Software Foundation. 00008 00009 This program is distributed in the hope that it would be useful, but 00010 WITHOUT ANY WARRANTY; without even the implied warranty of 00011 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. 00012 00013 Further, this software is distributed without any warranty that it is 00014 free of the rightful claim of any third person regarding infringement 00015 or the like. Any license provided herein, whether implied or 00016 otherwise, applies only to this software file. Patent licenses, if 00017 any, provided herein do not apply to combinations of this program with 00018 other software, or any other product whatsoever. 00019 00020 You should have received a copy of the GNU General Public License along 00021 with this program; if not, write the Free Software Foundation, Inc., 59 00022 Temple Place - Suite 330, Boston MA 02111-1307, USA. 00023 00024 Contact information: Silicon Graphics, Inc., 1600 Amphitheatre Pky, 00025 Mountain View, CA 94043, or: 00026 00027 http://www.sgi.com 00028 00029 For further information regarding this notice, see: 00030 00031 http://oss.sgi.com/projects/GenInfo/NoticeExplan 00032 00033 */ 00034 00035 00036 // This is really -*- C++ -*- 00037 00038 #ifndef dnf_INCLUDED 00039 #define dnf_INCLUDED "dnf.h" 00040 00041 #include <sys/types.h> 00042 #include <stdio.h> 00043 #include <assert.h> 00044 00045 #include "defs.h" 00046 #include "cxx_memory.h" 00047 #include "mat.h" 00048 #include "infin.h" 00049 #include "lnoutils.h" 00050 #include "soe.h" 00051 00052 enum CLAUSE_TYPE {CLAUSE_DISJ, CLAUSE_ATOM}; 00053 00054 /* The nice thing about soe's is that they represent a conjunct. So, 00055 they can be the building blocks of our disjunctive general 00056 clauses. A clause is either an soe (i.e. a atom-clause clause, 00057 or it can be the a disj of clauses. Note that nothing at this 00058 stage forces the conjunct of two conjuncts to be represented 00059 as a single conjunct. That will be imposed by a normalization 00060 phase to be performed at the discretion of a user later */ 00061 00062 class LINEAR_CLAUSE { 00063 private: 00064 CLAUSE_TYPE _t; 00065 MEM_POOL *_m; 00066 union { 00067 SYSTEM_OF_EQUATIONS *_atom; 00068 struct { 00069 INT32 _nconj; 00070 SYSTEM_OF_EQUATIONS **_conj; 00071 } _disj; 00072 } _u; 00073 friend LINEAR_CLAUSE * 00074 _xcombine_atom_with_disj(LINEAR_CLAUSE *l1, LINEAR_CLAUSE *l2); 00075 friend LINEAR_CLAUSE * 00076 _xcombine_disj_with_disj(LINEAR_CLAUSE *l1, LINEAR_CLAUSE *l2); 00077 enum CLAUSE_TYPE CLAUSE_type() { 00078 return _t; 00079 } 00080 SYSTEM_OF_EQUATIONS *CLAUSE_atom() { 00081 assert (_t == CLAUSE_ATOM); 00082 return _u._atom; 00083 } 00084 INT32 CLAUSE_nconj () { 00085 assert (_t == CLAUSE_DISJ); 00086 return _u._disj._nconj; 00087 } 00088 SYSTEM_OF_EQUATIONS **CLAUSE_conj() { 00089 assert (_t == CLAUSE_DISJ); 00090 return _u._disj._conj; 00091 } 00092 SYSTEM_OF_EQUATIONS *CLAUSE_conj_ith(INT32 i) { 00093 return _u._disj._conj[i]; 00094 } 00095 MEM_POOL *CLAUSE_mem_pool() { 00096 return _m; 00097 } 00098 public: 00099 LINEAR_CLAUSE (SYSTEM_OF_EQUATIONS *soe, MEM_POOL *pool); 00100 LINEAR_CLAUSE (SYSTEM_OF_EQUATIONS **soe_list, 00101 INT32 count, MEM_POOL *pool); 00102 friend LINEAR_CLAUSE * 00103 combine_clauses (LINEAR_CLAUSE *l1, LINEAR_CLAUSE *l2); 00104 BOOL Is_Consistent(); 00105 void Print (FILE *fp) const; 00106 }; 00107 00108 #endif
1.5.6