Add a translation layer to automatically escape/unescape variable and Uf names. This is work in progress and will eventually allow us to support arbitrary names for variables.

Author: daniel-raffler

src/org/sosy_lab/java_smt/basicimpl/AbstractArrayFormulaManager.java

@@ -8,7 +8,7 @@
 
 package org.sosy_lab.java_smt.basicimpl;
 
-import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName;
+import static org.sosy_lab.java_smt.basicimpl.FormulaCreator.escapeName;
 
 import org.sosy_lab.java_smt.api.ArrayFormula;
 import org.sosy_lab.java_smt.api.ArrayFormulaManager;
@@ -65,8 +65,8 @@ protected abstract TFormulaInfo store(
           FTI extends FormulaType<TI>,
           FTE extends FormulaType<TE>>
       ArrayFormula<TI, TE> makeArray(String pName, FTI pIndexType, FTE pElementType) {
-    checkVariableName(pName);
-    final TFormulaInfo namedArrayFormula = internalMakeArray(pName, pIndexType, pElementType);
+    final TFormulaInfo namedArrayFormula =
+        internalMakeArray(escapeName(pName), pIndexType, pElementType);
     return getFormulaCreator().encapsulateArray(namedArrayFormula, pIndexType, pElementType);
   }
 

src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java

@@ -9,7 +9,6 @@
 package org.sosy_lab.java_smt.basicimpl;
 
 import static com.google.common.base.Preconditions.checkArgument;
-import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName;
 
 import com.google.common.base.Preconditions;
 import com.google.common.collect.Lists;
@@ -294,8 +293,7 @@ public BitvectorFormula makeVariable(BitvectorType type, String pVar) {
 
   @Override
   public BitvectorFormula makeVariable(int pLength, String pVar) {
-    checkVariableName(pVar);
-    return wrap(makeVariableImpl(pLength, pVar));
+    return wrap(makeVariableImpl(pLength, FormulaCreator.escapeName(pVar)));
   }
 
   protected abstract TFormulaInfo makeVariableImpl(int pLength, String pVar);

src/org/sosy_lab/java_smt/basicimpl/AbstractBooleanFormulaManager.java

@@ -10,7 +10,6 @@
 
 import static com.google.common.base.Preconditions.checkArgument;
 import static com.google.common.base.Preconditions.checkState;
-import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName;
 
 import com.google.common.collect.Collections2;
 import com.google.common.collect.ImmutableList;
@@ -40,6 +39,7 @@
 import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor;
 import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
 import org.sosy_lab.java_smt.api.visitors.TraversalProcess;
+import org.sosy_lab.java_smt.basicimpl.FormulaCreator.SymbolViewVisitor;
 
 @SuppressWarnings("ClassTypeParameterName")
 public abstract class AbstractBooleanFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl>
@@ -60,8 +60,7 @@ private BooleanFormula wrap(TFormulaInfo formulaInfo) {
 
   @Override
   public BooleanFormula makeVariable(String pVar) {
-    checkVariableName(pVar);
-    return wrap(makeVariableImpl(pVar));
+    return wrap(makeVariableImpl(FormulaCreator.escapeName(pVar)));
   }
 
   protected abstract TFormulaInfo makeVariableImpl(String pVar);
@@ -279,21 +278,26 @@ public final <T extends Formula> T ifThenElse(BooleanFormula pBits, T f1, T f2)
 
   @Override
   public <R> R visit(BooleanFormula pFormula, BooleanFormulaVisitor<R> visitor) {
-    return formulaCreator.visit(pFormula, new DelegatingFormulaVisitor<>(visitor));
+    return formulaCreator.visit(
+        pFormula, new SymbolViewVisitor<>(new DelegatingFormulaVisitor<>(visitor)));
   }
 
   @Override
   public void visitRecursively(
       BooleanFormula pF, BooleanFormulaVisitor<TraversalProcess> pFormulaVisitor) {
     formulaCreator.visitRecursively(
-        new DelegatingFormulaVisitor<>(pFormulaVisitor), pF, p -> p instanceof BooleanFormula);
+        new SymbolViewVisitor<>(new DelegatingFormulaVisitor<>(pFormulaVisitor)),
+        pF,
+        p -> p instanceof BooleanFormula);
   }
 
   @Override
   public BooleanFormula transformRecursively(
       BooleanFormula f, BooleanFormulaTransformationVisitor pVisitor) {
     return formulaCreator.transformRecursively(
-        new DelegatingFormulaVisitor<>(pVisitor), f, p -> p instanceof BooleanFormula);
+        new SymbolViewVisitor<>(new DelegatingFormulaVisitor<>(pVisitor)),
+        f,
+        p -> p instanceof BooleanFormula);
   }
 
   private class DelegatingFormulaVisitor<R> implements FormulaVisitor<R> {

src/org/sosy_lab/java_smt/basicimpl/AbstractEnumerationFormulaManager.java

@@ -10,10 +10,12 @@
 
 import static com.google.common.base.Preconditions.checkArgument;
 import static com.google.common.base.Preconditions.checkNotNull;
-import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName;
+import static org.sosy_lab.java_smt.basicimpl.FormulaCreator.escapeName;
 
 import com.google.common.base.Preconditions;
 import com.google.common.collect.ImmutableMap;
+import com.google.common.collect.ImmutableSet;
+import com.google.common.collect.Iterables;
 import java.util.LinkedHashMap;
 import java.util.Map;
 import java.util.Set;
@@ -77,8 +79,9 @@ private void checkSameEnumerationType(EnumerationFormula pF1, EnumerationFormula
 
   @Override
   public EnumerationFormulaType declareEnumeration(String pName, Set<String> pElementNames) {
-    checkVariableName(pName);
-    return declareEnumerationImpl(pName, pElementNames);
+    return declareEnumerationImpl(
+        escapeName(pName),
+        ImmutableSet.copyOf(Iterables.transform(pElementNames, FormulaCreator::escapeName)));
   }
 
   protected EnumerationFormulaType declareEnumerationImpl(String pName, Set<String> pElementNames) {
@@ -114,8 +117,7 @@ protected TFormulaInfo makeConstantImpl(String pName, EnumerationFormulaType pTy
 
   @Override
   public EnumerationFormula makeVariable(String pVar, EnumerationFormulaType pType) {
-    checkVariableName(pVar);
-    return wrap(makeVariableImpl(pVar, pType));
+    return wrap(makeVariableImpl(escapeName(pVar), pType));
   }
 
   protected TFormulaInfo makeVariableImpl(String pVar, EnumerationFormulaType pType) {

src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java

@@ -8,7 +8,7 @@
 
 package org.sosy_lab.java_smt.basicimpl;
 
-import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName;
+import static org.sosy_lab.java_smt.basicimpl.FormulaCreator.escapeName;
 
 import com.google.common.base.Preconditions;
 import java.math.BigDecimal;
@@ -153,8 +153,7 @@ protected abstract TFormulaInfo makeNumberAndRound(
 
   @Override
   public FloatingPointFormula makeVariable(String pVar, FormulaType.FloatingPointType pType) {
-    checkVariableName(pVar);
-    return wrap(makeVariableImpl(pVar, pType));
+    return wrap(makeVariableImpl(escapeName(pVar), pType));
   }
 
   protected abstract TFormulaInfo makeVariableImpl(