Back translation for Princess rewrites

src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java

@@ -33,9 +33,11 @@
 import org.sosy_lab.common.collect.PathCopyingPersistentTreeMap;
 import org.sosy_lab.common.collect.PersistentMap;
 import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.Model;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
 import org.sosy_lab.java_smt.api.SolverException;
+import org.sosy_lab.java_smt.api.visitors.FormulaTransformationVisitor;
 import org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat;
 import org.sosy_lab.java_smt.basicimpl.CachingModel;
 import scala.Enumeration.Value;
@@ -100,8 +102,20 @@ protected int addConstraint0(BooleanFormula constraint) {
     partitions.push(partitions.pop().putAndCopy(formulaId, constraint));
     api.setPartitionNumber(formulaId);
 
-    final IFormula t = (IFormula) mgr.extractInfo(constraint);
-    api.addAssertion(api.abbrevSharedExpressions(t, creator.getEnv().getMinAtomsForAbbreviation()));
+    var abbrev =
+        api.abbrevSharedExpressions(
+            (IFormula) mgr.extractInfo(constraint), creator.getEnv().getMinAtomsForAbbreviation());
+    var rebuild =
+        mgr.transformRecursively(
+            creator.encapsulateBoolean(abbrev),
+            new FormulaTransformationVisitor(mgr) {
+              @Override
+              public Formula visitFreeVariable(Formula f, String name) {
+                // Add abbrev symbols to variable cache
+                return mgr.makeVariable(creator.getFormulaType(f), name);
+              }
+            });
+    api.addAssertion((IFormula) mgr.extractInfo(rebuild));
 
     return formulaId;
   }

src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java

@@ -13,11 +13,10 @@
 import ap.parser.ITerm;
 import ap.theories.bitvectors.ModuloArithmetic$;
 import ap.types.Sort;
-import ap.types.Sort$;
-import com.google.common.base.Preconditions;
+import com.google.common.collect.ImmutableList;
 import java.math.BigInteger;
 import org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager;
-import scala.Option;
+import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessBitvectorToIntegerDeclaration;
 
 class PrincessBitvectorFormulaManager
     extends AbstractBitvectorFormulaManager<
@@ -132,34 +131,17 @@ protected IExpression makeBitvectorImpl(int pLength, BigInteger pI) {
 
   @Override
   protected IExpression makeBitvectorImpl(int pLength, IExpression pIntegerFormula) {
-    return ModuloArithmetic$.MODULE$.cast2UnsignedBV(pLength, (ITerm) pIntegerFormula);
+    return new PrincessFunctionDeclaration.PrincessBitvectorFromIntegerDeclaration(pLength)
+        .makeApp(getFormulaCreator().getEnv(), ImmutableList.of(pIntegerFormula));
   }
 
   @Override
   protected IExpression toIntegerFormulaImpl(IExpression pBVFormula, boolean signed) {
-    final Sort sort = Sort$.MODULE$.sortOf((ITerm) pBVFormula);
-    final Option<Object> bitWidth = PrincessEnvironment.getBitWidth(sort);
-    Preconditions.checkArgument(bitWidth.isDefined());
-    final int size = (Integer) bitWidth.get();
-
-    // compute range for integer value,
-    // example: bitWidth=4 => signed_range=[-8;7] and unsigned_range=[0;15]
-    final BigInteger min;
-    final BigInteger max;
-    if (signed) {
-      min = BigInteger.ONE.shiftLeft(size - 1).negate();
-      max = BigInteger.ONE.shiftLeft(size - 1).subtract(BigInteger.ONE);
-    } else {
-      min = BigInteger.ZERO;
-      max = BigInteger.ONE.shiftLeft(size).subtract(BigInteger.ONE);
-    }
-
-    ITerm bvInRange =
-        ModuloArithmetic$.MODULE$.cast2Interval(
-            IdealInt.apply(min), IdealInt.apply(max), (ITerm) pBVFormula);
-
-    // Princess can not directly convert from BV to INT. However, adding zero helps. Ugly.
-    return IExpression.i(0).$plus(bvInRange);
+    var decl =
+        signed
+            ? PrincessBitvectorToIntegerDeclaration.SIGNED
+            : PrincessBitvectorToIntegerDeclaration.UNSIGNED;
+    return decl.makeApp(getFormulaCreator().getEnv(), ImmutableList.of(pBVFormula));
   }
 
   @Override
@@ -194,10 +176,8 @@ protected IExpression extract(IExpression pNumber, int pMsb, int pLsb) {
 
   @Override
   protected IExpression extend(IExpression pNumber, int pExtensionBits, boolean pSigned) {
-    if (pSigned) {
-      return ModuloArithmetic$.MODULE$.sign_extend(pExtensionBits, (ITerm) pNumber);
-    } else {
-      return ModuloArithmetic$.MODULE$.zero_extend(pExtensionBits, (ITerm) pNumber);
-    }
+    return new PrincessFunctionDeclaration.PrincessBitvectorExtendDeclaration(
+            pExtensionBits, pSigned)
+        .makeApp(getFormulaCreator().getEnv(), ImmutableList.of(pNumber));
   }
 }

src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java

@@ -12,6 +12,7 @@
 import static scala.collection.JavaConverters.collectionAsScalaIterableConverter;
 
 import ap.api.SimpleAPI;
+import ap.basetypes.IdealInt;
 import ap.parameters.GlobalSettings;
 import ap.parser.BooleanCompactifier;
 import ap.parser.Environment.EnvironmentException;
@@ -22,6 +23,8 @@
 import ap.parser.IFunApp;
 import ap.parser.IFunction;
 import ap.parser.IIntFormula;
+import ap.parser.IIntLit;
+import ap.parser.IIntRelation;
 import ap.parser.ITerm;
 import ap.parser.Parser2InputAbsy.TranslationException;
 import ap.parser.PartialEvaluator;
@@ -30,7 +33,6 @@
 import ap.parser.SMTTypes.SMTType;
 import ap.terfor.ConstantTerm;
 import ap.terfor.preds.Predicate;
-import ap.theories.arrays.ExtArray;
 import ap.theories.arrays.ExtArray.ArraySort;
 import ap.theories.bitvectors.ModuloArithmetic;
 import ap.theories.rationals.Rationals$;
@@ -50,8 +52,6 @@
 import java.io.File;
 import java.io.IOException;
 import java.io.StringReader;
-import java.lang.reflect.InvocationTargetException;
-import java.lang.reflect.Method;
 import java.nio.file.Path;
 import java.util.ArrayDeque;
 import java.util.ArrayList;
@@ -173,6 +173,8 @@ class PrincessEnvironment {
 
   private final Map<String, IFunction> functionsCache = new HashMap<>();
 
+  private final Map<FormulaType<?>, Map<ITerm, ITerm>> constArrayCache = new HashMap<>();
+
   private final int randomSeed;
   private final @Nullable PathCounterTemplate basicLogfile;
   private final ShutdownNotifier shutdownNotifier;
@@ -334,6 +336,15 @@ public List<? extends IExpression> parseStringToTerms(String s, PrincessFormulaC
         IFunction fun = ((IFunApp) var).fun();
         functionsCache.put(fun.name(), fun);
         addFunction(fun);
+      } else if (var instanceof IIntFormula
+          && ((IIntFormula) var).rel().equals(IIntRelation.EqZero())
+          && ((IIntFormula) var).apply(0) instanceof IFunApp) {
+        // Functions with return type Bool are wrapped in a predicate as (=0 (uf ...))
+        IFunction fun = ((IFunApp) var.apply(0)).fun();
+        functionsCache.put(fun.name(), fun);
+        addFunction(fun);
+      } else {
+        throw new IllegalArgumentException();
       }
     }
     return formulas;
@@ -562,6 +573,18 @@ private static String getName(IExpression var) {
   static FormulaType<?> getFormulaType(IExpression pFormula) {
     if (pFormula instanceof IFormula) {
       return FormulaType.BooleanType;
+    } else if (pFormula instanceof IFunApp
+        && ((IFunApp) pFormula).fun().equals(ModuloArithmetic.bv_extract())) {
+      IIntLit upper = (IIntLit) pFormula.apply(0);
+      IIntLit lower = (IIntLit) pFormula.apply(1);
+      IdealInt bwResult = upper.value().$minus(lower.value()).$plus(IdealInt.ONE());
+      return FormulaType.getBitvectorTypeWithSize(bwResult.intValue());
+    } else if (pFormula instanceof IFunApp
+        && ((IFunApp) pFormula).fun().equals(ModuloArithmetic.bv_concat())) {
+      IIntLit upper = (IIntLit) pFormula.apply(0);
+      IIntLit lower = (IIntLit) pFormula.apply(1);
+      IdealInt bwResult = upper.value().$plus(lower.value());
+      return FormulaType.getBitvectorTypeWithSize(bwResult.intValue());
     } else {
       final Sort sort = Sort.sortOf((ITerm) pFormula);
       try {
@@ -631,7 +654,14 @@ public IExpression makeVariable(Sort type, String varname) {
       }
     } else {
       if (sortedVariablesCache.containsKey(varname)) {
-        return sortedVariablesCache.get(varname);
+        ITerm found = sortedVariablesCache.get(varname);
+        Preconditions.checkArgument(
+            getFormulaType(found).equals(getFormulaTypeFromSort(type)),
+            "Can't declare variable \"%s\" with type %s. It has already been declared with type %s",
+            varname,
+            getFormulaTypeFromSort(type),
+            getFormulaType(found));
+        return found;
       } else {
         ITerm var = api.createConstant(varname, type);
         addSymbol(var);
@@ -644,6 +674,7 @@ public IExpression makeVariable(Sort type, String varname) {
   /** This function declares a new functionSymbol with the given argument types and result. */
   public IFunction declareFun(String name, Sort returnType, List<Sort> args) {
     if (functionsCache.containsKey(name)) {
+      // FIXME Check that the old declaration has the right type
       return functionsCache.get(name);
     } else {
       IFunction funcDecl =
@@ -667,20 +698,32 @@ public ITerm makeStore(ITerm array, ITerm index, ITerm value) {
     return new IFunApp(arraySort.theory().store(), toSeq(args));
   }
 
-  public ITerm makeConstArray(ArraySort arraySort, ITerm elseTerm) {
-    // return new IFunApp(arraySort.theory().const(), elseTerm); // I love Scala! So simple! ;-)
-
-    // Scala uses keywords that are illegal in Java. Thus, we use reflection to access the method.
-    // TODO we should contact the developers of Princess and ask for a renaming.
-    final IFunction constArrayOp;
-    try {
-      Method constMethod = ExtArray.class.getMethod("const");
-      constArrayOp = (IFunction) constMethod.invoke(arraySort.theory());
-    } catch (IllegalAccessException | NoSuchMethodException | InvocationTargetException exception) {
-      throw new RuntimeException(exception);
-    }
+  void cacheConstArray(ArraySort arraySort, ITerm elseTerm, ITerm constArray) {
+    constArrayCache.compute(
+        getFormulaTypeFromSort(arraySort),
+        (sort, maps) -> {
+          if (maps == null) {
+            maps = new HashMap<>();
+          }
+          maps.putIfAbsent(elseTerm, constArray);
+          return maps;
+        });
+  }
 
-    return new IFunApp(constArrayOp, toSeq(ImmutableList.of(elseTerm)));
+  public ITerm makeConstArray(ArraySort arraySort, ITerm elseTerm) {
+    constArrayCache.compute(
+        getFormulaTypeFromSort(arraySort),
+        (sort, maps) -> {
+          if (maps == null) {
+            maps = new HashMap<>();
+          }
+          maps.computeIfAbsent(
+              elseTerm,
+              term ->
+                  new IFunApp(arraySort.theory().constArray(), toSeq(ImmutableList.of(elseTerm))));
+          return maps;
+        });
+    return constArrayCache.get(getFormulaTypeFromSort(arraySort)).get(elseTerm);
   }
 
   public boolean hasArrayType(IExpression exp) {