simplify example.
Instead of interleaved parsing and classifying,
we can first parse all formulas and then classify them.
@@ -77,22 +77,27 @@ public class FormulaClassifier {
// we need a solver that supports all theories, at least for parsing.
try (SolverContext context =
SolverContextFactory.createSolverContext(config, logger, notifier, solver)) {
- FormulaClassifier fc = new FormulaClassifier(context);
List<BooleanFormula> formulas = new ArrayList<>();
+
+ // read all formulas from the file
List<String> definitions = new ArrayList<>();
for (String line : Files.readAllLines(path)) {
// we assume a line-based content
if (line.startsWith(";;") || line.startsWith("(push ") || line.startsWith("(pop ")) {
continue;
} else if (line.startsWith("(assert ")) {
- BooleanFormula bf = fc.parse(Joiner.on("").join(definitions) + line);
- fc.visit(bf);
+ BooleanFormula bf =
+ context.getFormulaManager().parse(Joiner.on("").join(definitions) + line);
formulas.add(bf);
} else {
// it is a definition
definitions.add(line);
}
}
+
+ // classify the formulas
+ FormulaClassifier fc = new FormulaClassifier(context);
+ formulas.forEach(fc::visit);
System.out.println(fc + ", checked formulas: " + formulas.size());
} catch (InvalidConfigurationException | UnsatisfiedLinkError e) {
@@ -115,10 +120,6 @@ public class FormulaClassifier {
mgr = context.getFormulaManager();
}
- private BooleanFormula parse(String s) {
- return mgr.parse(s);
- }
-
public void visit(BooleanFormula f) {
// first split formula into atoms to avoid repeated analysis of common subtrees.
AtomCollector atomCollector = new AtomCollector();
