Fixed lone multiplicity with fields

CVC4 · May 9, 2019 · 753f1af · 753f1af
1 parent 0090719
commit 753f1af
Show file tree

Hide file tree

Showing 3 changed files with 40 additions and 54 deletions.
diff --git a/alloy2smt/src/main/java/edu/uiowa/alloy2smt/translators/ExprBinaryTranslator.java b/alloy2smt/src/main/java/edu/uiowa/alloy2smt/translators/ExprBinaryTranslator.java
@@ -245,7 +245,7 @@ private Expression translateComparison(ExprBinary expr, BinaryExpression.Op op,
                         existentialBdVarExprs.add(bdVar.getVariable());
                     }        
 
-                    Expression distElementsExpr = TranslatorUtils.mkDistinctExpr(existentialBdVarExprs);
+                    Expression distElementsExpr = TranslatorUtils.makeDistinct(existentialBdVarExprs);
 
                     exprTranslator.translator.existentialBdVars.addAll(existentialBdVars);        
                     if(exprTranslator.translator.auxExpr != null)
@@ -294,7 +294,7 @@ private Expression translateComparison(ExprBinary expr, BinaryExpression.Op op,
                     }        
 
                     // (distinct e1 e2 e3 ....)
-                    Expression distElementsExpr = TranslatorUtils.mkDistinctExpr(existentialBdVarExprs);
+                    Expression distElementsExpr = TranslatorUtils.makeDistinct(existentialBdVarExprs);
 
                     exprTranslator.translator.existentialBdVars.addAll(existentialBdVars);        
                     if(exprTranslator.translator.auxExpr != null)
@@ -343,7 +343,7 @@ private Expression translateComparison(ExprBinary expr, BinaryExpression.Op op,
                     }        
 
                     // (distinct e1 e2 e3 ....)
-                    Expression distElementsExpr = TranslatorUtils.mkDistinctExpr(existentialBdVarExprs);
+                    Expression distElementsExpr = TranslatorUtils.makeDistinct(existentialBdVarExprs);
 
                     exprTranslator.translator.existentialBdVars.addAll(existentialBdVars);        
                     if(exprTranslator.translator.auxExpr != null)
@@ -392,7 +392,7 @@ private Expression translateComparison(ExprBinary expr, BinaryExpression.Op op,
                     }        
 
                     // (distinct e1 e2 e3 ....)
-                    Expression distElementsExpr = TranslatorUtils.mkDistinctExpr(existentialBdVarExprs);
+                    Expression distElementsExpr = TranslatorUtils.makeDistinct(existentialBdVarExprs);
 
                     exprTranslator.translator.existentialBdVars.addAll(existentialBdVars);        
                     if(exprTranslator.translator.auxExpr != null)
@@ -456,7 +456,7 @@ else if((expr.right instanceof ExprUnary) && ((ExprUnary)expr.right).op == ExprU
                         existentialBdVarExprs.add(bdVar.getVariable());
                     }        
 
-                    Expression distElementsExpr = TranslatorUtils.mkDistinctExpr(existentialBdVarExprs);
+                    Expression distElementsExpr = TranslatorUtils.makeDistinct(existentialBdVarExprs);
 
                     exprTranslator.translator.existentialBdVars.addAll(existentialBdVars);        
                     if(exprTranslator.translator.auxExpr != null)
@@ -505,7 +505,7 @@ else if((expr.right instanceof ExprUnary) && ((ExprUnary)expr.right).op == ExprU
                     }        
 
                     // (distinct e1 e2 e3 ....)
-                    Expression distElementsExpr = TranslatorUtils.mkDistinctExpr(existentialBdVarExprs);
+                    Expression distElementsExpr = TranslatorUtils.makeDistinct(existentialBdVarExprs);
 
                     exprTranslator.translator.existentialBdVars.addAll(existentialBdVars);        
                     if(exprTranslator.translator.auxExpr != null)
@@ -554,7 +554,7 @@ else if((expr.right instanceof ExprUnary) && ((ExprUnary)expr.right).op == ExprU
                     }        
 
                     // (distinct e1 e2 e3 ....)
-                    Expression distElementsExpr = TranslatorUtils.mkDistinctExpr(existentialBdVarExprs);
+                    Expression distElementsExpr = TranslatorUtils.makeDistinct(existentialBdVarExprs);
 
                     exprTranslator.translator.existentialBdVars.addAll(existentialBdVars);        
                     if(exprTranslator.translator.auxExpr != null)
@@ -603,7 +603,7 @@ else if((expr.right instanceof ExprUnary) && ((ExprUnary)expr.right).op == ExprU
                     }        
 
                     // (distinct e1 e2 e3 ....)
-                    Expression distElementsExpr = TranslatorUtils.mkDistinctExpr(existentialBdVarExprs);
+                    Expression distElementsExpr = TranslatorUtils.makeDistinct(existentialBdVarExprs);
 
                     exprTranslator.translator.existentialBdVars.addAll(existentialBdVars);        
                     if(exprTranslator.translator.auxExpr != null)