This repository has been archived by the owner on Jan 15, 2023. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 0
/
PropositionalFormula.java
201 lines (176 loc) · 6.13 KB
/
PropositionalFormula.java
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
import java.util.Arrays;
import java.lang.IllegalArgumentException;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
import java.util.ArrayList;
import java.util.List;
import java.util.ListIterator;
import java.util.HashMap;
class PropositionalFormula extends SyntacticallyValidFormula {
public String formula;
private List<String> clauseSet;
private String CNF = "";
public PropositionalFormula(String syntacticallyValidFormula){
super(syntacticallyValidFormula);
trimParentheses(syntacticallyValidFormula);
if(!(isPropositional(syntacticallyValidFormula))){
throw new IllegalArgumentException("Supplied argument is not a syntactically valid propositional formula.");
} else {
this.formula = syntacticallyValidFormula;
}
}
private boolean isPropositional(String syntacticallyValidFormula){
String[] approvedWords = {"and", "or", "implies", "equivalent", "not"};
return containsWord(syntacticallyValidFormula, approvedWords, true);
}
private void toCNF(){
/* Algorithm:
To convert first-order logic to CNF:
1 Convert to Negation normal form.
1 Eliminate implications: convert x → y to ¬ x ∨ y
2 Move NOTs inwards.
2 Standardize variables
3 Skolemize the statement
4 Drop universal quantifiers
5 Distribute ANDs over ORs.
*/
}
public String getCNF(){
if (this.CNF.equals("")){
return null;
}
return this.CNF;
}
public boolean isCNF(){
if (this.CNF.equals("")){
return isCNF(this.formula);
}
return true;
}
public List<String> getClauseSet(){
return this.clauseSet;
}
public void setClauseSet(List<String> cs){
this.clauseSet = new ArrayList<String>(cs);
}
public PropositionalFormula clone(){
PropositionalFormula ny = new PropositionalFormula(this.formula);
ny.isCNF();
ny.setClauseSet(this.clauseSet);
return ny;
}
private boolean isCNF(String formula){
boolean isCNF = true;
if (containsWord(formula, new String[]{"implies"}, false)){
System.out.printf("Formula '%s' is not in CNF as it contains an implication.\n", formula);
isCNF = false;
}
if (containsWord(formula, new String[]{"equivalent"}, false)) {
System.out.printf("Formula '%s' is not in CNF as it contains an equivalence.\n", formula);
isCNF = false;
}
//Get clauses between ANDs
List<String> clauses = new ArrayList<>();
String regexClauses = "\\(([^)]+)\\)";
Matcher m = Pattern.compile(regexClauses).matcher(formula);
while(m.find()){
//System.out.println(m.group(1));
clauses.add(m.group(1));
}
String regexConjunctions = "\\)([^)]+)\\(";
m = Pattern.compile(regexConjunctions).matcher(formula);
while(m.find()){
if(containsWord(m.group(1), new String[]{"or"}, false)){
System.out.printf("Formula '%s' is not in CNF as it contains operator 'or'-operator between clauses.\n", formula);
isCNF = false;
}
}
//Check for disallowed words between parantheses
String[] disallowedWords = {"and", "implies", "equivalent"};
if(containsWord(clauses, disallowedWords, false)){
System.out.printf("Formula '%s' is not in CNF as it contains a clause which is not a disjunction.\n", formula);
isCNF = false;
}
//Check for disallowed NOTs, and add allowed atomos and negated atoms to clauses
String[] split = formula.split(" ");
for (int i = 0; i < split.length; i++){
// I cant remember why some of these are needed..
// Changed the first condition quite heftly, because it saved clauses wrong.
// Update: they are there for getting unit clauses and single literals!
if (split[0].length() == 1 && i == 0){
clauses.add(split[0]);
}
if((split[i].length() == 1) && (i > 0) && (!(split[i-1].equals("not")) && (!(split[i-1].equals("or"))) && (!(split[i-1].equals("(not"))))){
clauses.add(split[i]);
continue;
}
if(split[i].equals("not")){
if (i == (split.length - 1)){
System.out.printf("Formula '%s' ends with an invalid 'not'-operator.\n", formula);
isCNF = false;
continue;
}
if (!(split[i+1].length() == 1) && !(split[i+1].length() == 2 && split[i+1].charAt(1) == ')')){
System.out.printf("Formula '%s' is not in CNF as it contains a non-atomic term '%s' after a 'not'-operator.\n", formula, split[i+1]);
isCNF = false;
continue;
}
if (i == 0){
clauses.add("not " + split[i+1]);
continue;
}
if(!(split[i-1].equals("or"))){
clauses.add("not " + split[i+1]);
}
}
}
//If in CNF, write the clauses to the objects CNF-string.
this.clauseSet = new ArrayList<>();
if (isCNF){
ListIterator<String> iterator = clauses.listIterator();
while(iterator.hasNext()){
String s = iterator.next();
s = s.replaceAll("not ", "-");
s = s.replaceAll(" or ", "");
this.clauseSet.add(s);
this.CNF = this.CNF.concat("{" + s + "}, ");
}
//Remove trailing comma
this.CNF = this.CNF.substring(0, this.CNF.length()-2);
}
return isCNF;
}
private boolean containsWord(List<String> formulas, String[] words, boolean shouldContain){
boolean found = false;
ListIterator<String> iterator = formulas.listIterator();
while(iterator.hasNext()){
if (containsWord(iterator.next(), words, shouldContain)){
found = true;
}
}
return found;
}
private boolean containsWord(String formula, String[] words, boolean shouldContain){
//charAt goes to shit if you get a ' ' in the split.
String[] split;
if (formula.charAt(0) == ' '){
split = formula.substring(1).split(" ");
}
else {
split = formula.split(" ");
}
boolean contains = false;
for (String s : split){
if (s.charAt(0) == '('){
s = s.substring(1);
}
if (Arrays.stream(words).anyMatch(s::equals)){
if (!shouldContain){
//System.out.println("Disallowed word: " + s);
}
contains = true;
}
}
return contains;
}
}