Use FormulaUtils where appropriate

src/main/java/org/variantsync/diffdetective/analysis/logic/SAT.java

@@ -9,6 +9,7 @@
 import java.util.HashMap;
 
 import static org.variantsync.diffdetective.util.fide.FormulaUtils.negate;
+import static org.variantsync.diffdetective.util.fide.FormulaUtils.and;
 
 /**
  * Class with static functions for satisfiability solving, potentially with some optimizations.
@@ -123,7 +124,7 @@ public static boolean implies(final Node left, final Node right) {
         /// = TAUT(!left || right)
         /// = !SAT(!(!left || right))
         /// = !SAT(left && !right))
-        return !isSatisfiable(new And(left, negate(right)));
+        return !isSatisfiable(and(left, negate(right)));
     }
 
     /**
@@ -134,6 +135,6 @@ public static boolean implies(final Node left, final Node right) {
      * @return True iff <code>left</code> &lt;=&gt; <code>right</code> is a tautology.
      */
     public static boolean equivalent(final Node left, final Node right) {
-        return isTautology(new Equals(left, right));
+        return isTautology(FormulaUtils.equivalent(left, right));
     }
-}
+}

src/main/java/org/variantsync/diffdetective/feature/cpp/ControllingCExpressionVisitor.java

@@ -4,17 +4,17 @@
 import org.antlr.v4.runtime.tree.AbstractParseTreeVisitor;
 import org.antlr.v4.runtime.tree.ParseTree;
 import org.antlr.v4.runtime.tree.ParseTreeVisitor;
-import org.prop4j.And;
-import org.prop4j.Literal;
 import org.prop4j.Node;
-import org.prop4j.Not;
-import org.prop4j.Or;
 import org.variantsync.diffdetective.feature.antlr.CExpressionParser;
 import org.variantsync.diffdetective.feature.antlr.CExpressionVisitor;
+import org.variantsync.diffdetective.util.fide.FormulaUtils;
 
 import java.util.List;
 import java.util.function.Function;
 
+import static org.variantsync.diffdetective.util.fide.FormulaUtils.negate;
+import static org.variantsync.diffdetective.util.fide.FormulaUtils.var;
+
 /**
  * Visitor that controls how formulas given as an ANTLR parse tree are abstracted.
  * To this end, the visitor traverses the parse tree, searching for subtrees that should be abstracted.
@@ -73,7 +73,7 @@ public Node visitPrimaryExpression(CExpressionParser.PrimaryExpressionContext ct
             // Negation can be modeled in the formula.
             // All other unary operators need to be abstracted.
             if (ctx.unaryOperator().getText().equals("!")) {
-                return new Not(ctx.primaryExpression().accept(this));
+                return negate(ctx.primaryExpression().accept(this));
             } else {
                 return abstractToLiteral(ctx);
             }
@@ -250,15 +250,15 @@ public Node visitInclusiveOrExpression(CExpressionParser.InclusiveOrExpressionCo
     //    ;
     @Override
     public Node visitLogicalAndExpression(CExpressionParser.LogicalAndExpressionContext ctx) {
-        return visitLogicalExpression(ctx, And::new);
+        return visitLogicalExpression(ctx, FormulaUtils::and);
     }
 
     // logicalOrExpression
     //    :   logicalAndExpression ( '||' logicalAndExpression)*
     //    ;
     @Override
     public Node visitLogicalOrExpression(CExpressionParser.LogicalOrExpressionContext ctx) {
-        return visitLogicalExpression(ctx, Or::new);
+        return visitLogicalExpression(ctx, FormulaUtils::or);
     }
 
     // logicalOperand
@@ -302,6 +302,6 @@ private Node recurseOnSingleChild(ParserRuleContext ctx) {
     }
 
     private Node abstractToLiteral(ParserRuleContext ctx) {
-        return new Literal(ctx.accept(abstractingVisitor).toString());
+        return var(ctx.accept(abstractingVisitor).toString());
     }
 }

src/main/java/org/variantsync/diffdetective/feature/jpp/ControllingJPPExpressionVisitor.java

@@ -3,16 +3,17 @@
 import org.antlr.v4.runtime.ParserRuleContext;
 import org.antlr.v4.runtime.tree.AbstractParseTreeVisitor;
 import org.antlr.v4.runtime.tree.ParseTree;
-import org.prop4j.And;
-import org.prop4j.Literal;
 import org.prop4j.Node;
-import org.prop4j.Or;
 import org.variantsync.diffdetective.feature.antlr.JPPExpressionParser;
 import org.variantsync.diffdetective.feature.antlr.JPPExpressionVisitor;
+import org.variantsync.diffdetective.util.fide.FormulaUtils;
 
 import java.util.List;
 import java.util.function.Function;
 
+import static org.variantsync.diffdetective.util.fide.FormulaUtils.negate;
+import static org.variantsync.diffdetective.util.fide.FormulaUtils.var;
+
 /**
  * Transform a parse tree into a {@link org.prop4j.Node formula}.
  * Non-boolean sub-expressions are abstracted using
@@ -33,15 +34,15 @@ public Node visitExpression(JPPExpressionParser.ExpressionContext ctx) {
     //    ;
     @Override
     public Node visitLogicalOrExpression(JPPExpressionParser.LogicalOrExpressionContext ctx) {
-        return visitLogicalExpression(ctx, Or::new);
+        return visitLogicalExpression(ctx, FormulaUtils::or);
     }
 
     // logicalAndExpression
     //    :   primaryExpression (AND primaryExpression)*
     //    ;
     @Override
     public Node visitLogicalAndExpression(JPPExpressionParser.LogicalAndExpressionContext ctx) {
-        return visitLogicalExpression(ctx, And::new);
+        return visitLogicalExpression(ctx, FormulaUtils::and);
     }
 
     // primaryExpression
@@ -68,7 +69,7 @@ public Node visitPrimaryExpression(JPPExpressionParser.PrimaryExpressionContext
     //    ;
     @Override
     public Node visitComparisonExpression(JPPExpressionParser.ComparisonExpressionContext ctx) {
-        return new Literal(ctx.getText());
+        return var(ctx.getText());
     }
 
     // operand
@@ -79,23 +80,23 @@ public Node visitComparisonExpression(JPPExpressionParser.ComparisonExpressionCo
     //    ;
     @Override
     public Node visitOperand(JPPExpressionParser.OperandContext ctx) {
-        return new Literal(ctx.getText());
+        return var(ctx.getText());
     }
 
     // definedExpression
     //    :   'defined' '(' Identifier ')'
     //    ;
     @Override
     public Node visitDefinedExpression(JPPExpressionParser.DefinedExpressionContext ctx) {
-        return new Literal(String.format("defined(%s)", ctx.Identifier().getText()));
+        return var(String.format("defined(%s)", ctx.Identifier().getText()));
     }
 
     // undefinedExpression
     //    :   NOT 'defined' '(' Identifier ')'
     //    ;
     @Override
     public Node visitUndefinedExpression(JPPExpressionParser.UndefinedExpressionContext ctx) {
-        return new Literal(String.format("defined(%s)", ctx.Identifier().getText()), false);
+        return negate(var(String.format("defined(%s)", ctx.Identifier().getText())));
     }
 
     // propertyExpression

src/main/java/org/variantsync/diffdetective/util/fide/FormulaUtils.java

@@ -1,9 +1,12 @@
 package org.variantsync.diffdetective.util.fide;
 
 import org.prop4j.And;
+import org.prop4j.Equals;
+import org.prop4j.Implies;
 import org.prop4j.Literal;
 import org.prop4j.Node;
 import org.prop4j.Not;
+import org.prop4j.Or;
 import org.variantsync.diffdetective.analysis.logic.SAT;
 import org.variantsync.diffdetective.util.Assert;
 import org.variantsync.functjonal.Cast;
@@ -45,6 +48,18 @@ public static And and(Node... nodes) {
         return new And(nodes);
     }
 
+    public static Or or(Node... nodes) {
+        return new Or(nodes);
+    }
+
+    public static Implies implies(Node a, Node b) {
+        return new Implies(a, b);
+    }
+
+    public static Equals equivalent(Node a, Node b) {
+        return new Equals(a, b);
+    }
+
     /** Recursively counts the number of instances of {@link Literal} in {@code formula}. */
     public static int numberOfLiterals(final Node formula) {
         if (formula instanceof Literal) {