-
Notifications
You must be signed in to change notification settings - Fork 0
/
Control.java
55 lines (43 loc) · 1.37 KB
/
Control.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
/*
* To change this license header, choose License Headers in Project Properties.
* To change this template file, choose Tools | Templates
* and open the template in the editor.
*/
package MainPackage;
import java.util.Iterator;
import java.util.TreeSet;
/**
*
* @author marcomatarese
*/
public class Control{
public static Formula form = new Formula();
/**
* The program's kernel.
*/
public static void goToDpp(){
TreeSet<Clausola> ex = null, ris = null;
//The loop stops when the Formula has 0 or 1 Clausola.
while(form.listOfC.size() > 1){
form.deleteAllTautologies();
form.emptyClauseControl();
Letterale p = form.takePivot();
ex = form.identifyExonerated(p);
ris = form.calculateResolvents(p);
form.listOfC = form.formulasUnion(ex, ris);
}
}
/**
* Cleans all the used memory.
*/
public static void cleanAll(){
Iterator<Clausola> itC = form.listOfC.iterator();
Clausola tmpC;
while(itC.hasNext()){
tmpC = itC.next();
tmpC.listOfL.removeAll(tmpC.listOfL);
}
form.listOfC.removeAll(form.listOfC);
form = new Formula();
}
}