1 /*
2
3 This file is part of the Maude 2 interpreter.
4
5 Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA.
6
7 This program is free software; you can redistribute it and/or modify
8 it under the terms of the GNU General Public License as published by
9 the Free Software Foundation; either version 2 of the License, or
10 (at your option) any later version.
11
12 This program is distributed in the hope that it will be useful,
13 but WITHOUT ANY WARRANTY; without even the implied warranty of
14 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 GNU General Public License for more details.
16
17 You should have received a copy of the GNU General Public License
18 along with this program; if not, write to the Free Software
19 Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.
20
21 */
22
23 //
24 // Class for formulae in some propositional logic.
25 //
26 #ifndef _logicFormula_hh_
27 #define _logicFormula_hh_
28
29 class LogicFormula
30 {
31 public:
32 enum Op
33 {
34 //
35 // Primitive
36 //
37 PROPOSITION,
38 LTL_TRUE,
39 LTL_FALSE,
40 //
41 // Unary
42 //
43 NOT,
44 NEXT,
45 //
46 // Binary
47 //
48 AND,
49 OR,
50 UNTIL,
51 RELEASE
52 };
53
54 int makeProp(int propIndex);
55 int makeOp(Op op, int firstArg = NONE, int secondArg = NONE);
56
57 int getProp(int nodeNr) const;
58 Op getOp(int nodeNr) const;
59 int getArg(int nodeNr, int argNr = 0) const;
60 bool isPropositional(int nodeNr) const;
61 /*
62 bool structuallyImplies(const NatSet& now, const NatSet& next, int candidate) const;
63 bool structuallyContradicts(const NatSet& now, const NatSet& next, int candidate) const;
64 bool containsNegation(const NatSet& indexSet, int formulaIndex) const;
65 bool isNegation(int f1, int f2) const;
66 */
67 void dump(ostream& s);
68
69 private:
70 struct Node
71 {
72 short op;
73 Bool propositional;
74 int args[2];
75 };
76
77 Vector<Node> nodes;
78 };
79
80 inline LogicFormula::Op
getOp(int nodeNr) const81 LogicFormula::getOp(int nodeNr) const
82 {
83 return static_cast<Op>(nodes[nodeNr].op);
84 }
85
86 inline int
getProp(int nodeNr) const87 LogicFormula::getProp(int nodeNr) const
88 {
89 return nodes[nodeNr].args[0];
90 }
91
92 inline int
getArg(int nodeNr,int argNr) const93 LogicFormula::getArg(int nodeNr, int argNr) const
94 {
95 return nodes[nodeNr].args[argNr];
96 }
97
98 inline bool
isPropositional(int nodeNr) const99 LogicFormula::isPropositional(int nodeNr) const
100 {
101 return nodes[nodeNr].propositional;
102 }
103
104 #endif
105