Simplify before add

RipplB · Feb 25, 2024 · 0e22535 · 0e22535
1 parent de80e66
commit 0e22535
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/...olver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java b/...olver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java
@@ -84,13 +84,14 @@ public SmtLibSolver(
 
     @Override
     public void add(Expr<BoolType> assertion) {
-        final var consts = ExprUtils.getConstants(assertion);
+        final var simplifiedAssertion = ExprUtils.simplify(assertion);
+        final var consts = ExprUtils.getConstants(simplifiedAssertion);
         consts.removeAll(declarationStack.toCollection());
         declarationStack.add(consts);
 
-        final var term = transformationManager.toTerm(assertion);
+        final var term = transformationManager.toTerm(simplifiedAssertion);
 
-        assertions.add(assertion);
+        assertions.add(simplifiedAssertion);
         declareDatatypes((Collection<Type>) consts.stream().map(ConstDecl::getType).toList());
         consts.stream().map(symbolTable::getDeclaration).forEach(this::issueGeneralCommand);
         issueGeneralCommand(String.format("(assert %s)", term));