Improve CLI and parser, update SMT grammar, add command framework

paultristanwagner · Oct 26, 2023 · 8be935c · 8be935c
2 parents bb1b11f + 75c5a32
commit 8be935c
Show file tree

Hide file tree

Showing 51 changed files with 1,417 additions and 890 deletions.
diff --git a/README.md b/README.md
@@ -23,38 +23,36 @@ A SAT solver is implemented that can
 employ [DPLL+CDCL](https://en.wikipedia.org/wiki/Conflict-driven_clause_learning), [DPLL](https://en.wikipedia.org/wiki/DPLL_algorithm)
 as well as simple enumeration to solve propositional logic problems.
 
-### Example
-
 Input can be given in conjunctive normal form in the following way.
 
-<img src="images/cnf-input-sat.png" alt="How to input in CNF" width="350" /> <br>
-<img src="images/cnf-input-unsat.png" alt="How to input in CNF" width="350" /> <br>
+<img src="images/cnf-input-sat.png" alt="How to input in CNF"/> <br>
+<img src="images/cnf-input-unsat.png" alt="How to input in CNF"/> <br>
 
 # Tseitin's transformation
 
 The Tseitin transformation is implemented for propositional logic.
 It can be used to transform a formula into an equi-satisfiable formula in conjunctive normal form.
 The logical operators '~', '&', '|', '->', '<->' as well as parentheses are supported.
 
-<img src="images/tseitin.png" alt="Tseitin transformation for proving 'modus ponens'" width="700" /> <br>
+<img src="images/tseitin.png" alt="Tseitin transformation for proving 'modus ponens'"/> <br>
 
 # SMT solver
 
 An SMT solver is implemented for linear real arithmetic (QF_LRA), linear integer arithmetic (QF_LIA), equality logic (
 QF_EQ) and equality logic with
 uninterpreted functions (QF_EQUF).
 
-<img src="images/smt-qflra-sat.png" alt="Satisfiable SMT example of linear real arithmetic" width="450" /> <br>
-<img src="images/smt-qflra-unsat.png" alt="Unsatisfiable SMT example of linear real arithmetic" width="450" /> <br>
+<img src="images/smt-qflra-sat.png" alt="Satisfiable SMT example of linear real arithmetic"/> <br>
+<img src="images/smt-qflra-unsat.png" alt="Unsatisfiable SMT example of linear real arithmetic"/> <br>
 
-<img src="images/smt-qflia-sat.png" alt="Satisfiable SMT example of linear integer arithmetic" width="450" /> <br>
-<img src="images/smt-qflia-unsat.png" alt="Unsatisfiable SMT example of linear integer arithmetic" width="450" /> <br>
+<img src="images/smt-qflia-sat.png" alt="Satisfiable SMT example of linear integer arithmetic"/> <br>
+<img src="images/smt-qflia-unsat.png" alt="Unsatisfiable SMT example of linear integer arithmetic"/> <br>
 
-<img src="images/smt-qfeq-sat.png" alt="Satisfiable SMT example of equality logic" width="450" /> <br>
-<img src="images/smt-qfeq-unsat.png" alt="Unsatisfiable SMT example of equality logic" width="450" /> <br>
+<img src="images/smt-qfeq-sat.png" alt="Satisfiable SMT example of equality logic"/> <br>
+<img src="images/smt-qfeq-unsat.png" alt="Unsatisfiable SMT example of equality logic"/> <br>
 
-<img src="images/smt-qfequf-sat.png" alt="Satisfiable SMT example of equality logic with uninterpreted functions" width="500" /> <br>
-<img src="images/smt-qfequf-unsat.png" alt="Unsatisfiable SMT example of equality logic with uninterpreted functions" width="500" /> <br>
+<img src="images/smt-qfequf-sat.png" alt="Satisfiable SMT example of equality logic with uninterpreted functions"/> <br>
+<img src="images/smt-qfequf-unsat.png" alt="Unsatisfiable SMT example of equality logic with uninterpreted functions"/> <br>
 
 # Theory solvers
 
@@ -68,10 +66,10 @@ Currently, the program supports decimal coefficients which will be handled via f
 
 ### Examples
 
-<img src="images/simplex-sat.png" alt="Satisfiable Simplex example" width="350" /> <br>
-<img src="images/simplex-unsat.png" alt="Unsatisfiable Simplex example" width="350" /> <br>
+<img src="images/simplex-sat.png" alt="Satisfiable Simplex example"/> <br>
+<img src="images/simplex-unsat.png" alt="Unsatisfiable Simplex example"/> <br>
 
 An optional objective function can be given to maximize or minimize the value of a linear expression.
 
-<img src="images/simplex-optimal.png" alt="Optimal Simplex example" width="450" /> <br>
-<img src="images/simplex-unbounded.png" alt="Unbounded Simplex example" width="350" /> <br>
+<img src="images/simplex-optimal.png" alt="Optimal Simplex example"/> <br>
+<img src="images/simplex-unbounded.png" alt="Unbounded Simplex example"/> <br>
diff --git a/images/cnf-input-sat.png b/images/cnf-input-sat.png
diff --git a/images/cnf-input-unsat.png b/images/cnf-input-unsat.png
diff --git a/images/simplex-optimal.png b/images/simplex-optimal.png
diff --git a/images/simplex-sat.png b/images/simplex-sat.png
diff --git a/images/simplex-unbounded.png b/images/simplex-unbounded.png
diff --git a/images/simplex-unsat.png b/images/simplex-unsat.png
diff --git a/images/smt-qfeq-sat.png b/images/smt-qfeq-sat.png
diff --git a/images/smt-qfeq-unsat.png b/images/smt-qfeq-unsat.png
diff --git a/images/smt-qfequf-sat.png b/images/smt-qfequf-sat.png
diff --git a/images/smt-qfequf-unsat.png b/images/smt-qfequf-unsat.png
diff --git a/images/smt-qflia-sat.png b/images/smt-qflia-sat.png
diff --git a/images/smt-qflia-unsat.png b/images/smt-qflia-unsat.png
diff --git a/images/smt-qflra-sat.png b/images/smt-qflra-sat.png
diff --git a/images/smt-qflra-unsat.png b/images/smt-qflra-unsat.png
diff --git a/images/tseitin.png b/images/tseitin.png
diff --git a/pom.xml b/pom.xml
@@ -31,7 +31,17 @@
         <dependency>
             <groupId>com.google.guava</groupId>
             <artifactId>guava</artifactId>
-            <version>31.1-jre</version>
+            <version>32.1.3-jre</version>
+        </dependency>
+        <dependency>
+            <groupId>org.jline</groupId>
+            <artifactId>jline</artifactId>
+            <version>3.23.0</version>
+        </dependency>
+        <dependency>
+            <groupId>org.jline</groupId>
+            <artifactId>jline-terminal-jansi</artifactId>
+            <version>3.23.0</version>
         </dependency>
     </dependencies>
 
@@ -67,7 +77,7 @@
                             <transformers>
                                 <transformer
                                         implementation="org.apache.maven.plugins.shade.resource.ManifestResourceTransformer">
-                                    <mainClass>me.paultristanwagner.satchecking.CLI</mainClass>
+                                    <mainClass>me.paultristanwagner.satchecking.Main</mainClass>
                                 </transformer>
                             </transformers>
                         </configuration>

diff --git a/src/main/java/me/paultristanwagner/satchecking/CLI.java b/src/main/java/me/paultristanwagner/satchecking/CLI.java