Remove Boolector Quantifiers

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java

@@ -22,7 +22,6 @@ final class BoolectorFormulaManager extends AbstractFormulaManager<Long, Long, L
       BoolectorUFManager pFunctionManager,
       BoolectorBooleanFormulaManager pBooleanManager,
       BoolectorBitvectorFormulaManager pBitvectorManager,
-      BoolectorQuantifiedFormulaManager pQuantifierManager,
       BoolectorArrayFormulaManager pArrayManager) {
     super(
         pFormulaCreator,
@@ -32,7 +31,7 @@ final class BoolectorFormulaManager extends AbstractFormulaManager<Long, Long, L
         null,
         pBitvectorManager,
         null,
-        pQuantifierManager,
+        null,
         pArrayManager,
         null,
         null,

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java

@@ -94,12 +94,10 @@ public static BoolectorSolverContext create(
     BoolectorBooleanFormulaManager booleanTheory = new BoolectorBooleanFormulaManager(creator);
     BoolectorBitvectorFormulaManager bitvectorTheory =
         new BoolectorBitvectorFormulaManager(creator, booleanTheory);
-    BoolectorQuantifiedFormulaManager quantifierTheory =
-        new BoolectorQuantifiedFormulaManager(creator);
     BoolectorArrayFormulaManager arrayTheory = new BoolectorArrayFormulaManager(creator);
     BoolectorFormulaManager manager =
         new BoolectorFormulaManager(
-            creator, functionTheory, booleanTheory, bitvectorTheory, quantifierTheory, arrayTheory);
+            creator, functionTheory, booleanTheory, bitvectorTheory, arrayTheory);
     return new BoolectorSolverContext(manager, creator, pShutdownNotifier);
   }
 

src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java

@@ -35,6 +35,7 @@
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_DIVIDES_ATOM;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_EQ_TERM;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_FLOOR;
+import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_FORALL_TERM;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_IDIV;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_IMOD;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_IS_INT_ATOM;
@@ -81,6 +82,7 @@
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_eq;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_floor;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_function_type;
+import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_get_term_by_name;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_get_term_name;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_idiv;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_imod;
@@ -89,7 +91,8 @@
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_is_int_atom;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_ite;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_mul;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_named_variable;
+import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_new_uninterpreted_term;
+import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_new_variable;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_not;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_or;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_parse_rational;
@@ -100,6 +103,7 @@
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_proj_index;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_rational_const_value;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_real_type;
+import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_set_term_name;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_sum;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_sum_component;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_bitsize;
@@ -120,9 +124,11 @@
 import com.google.common.base.Joiner;
 import com.google.common.base.Preconditions;
 import com.google.common.collect.Collections2;
+import com.google.common.collect.HashBasedTable;
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableSet;
 import com.google.common.collect.Lists;
+import com.google.common.collect.Table;
 import com.google.common.primitives.Ints;
 import java.math.BigInteger;
 import java.util.ArrayList;
@@ -135,6 +141,7 @@
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
 import org.sosy_lab.java_smt.api.FunctionDeclarationKind;
+import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier;
 import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
 import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
 import org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl;
@@ -153,6 +160,12 @@ public class Yices2FormulaCreator extends FormulaCreator<Integer, Integer, Long,
           YICES_VARIABLE,
           YICES_UNINTERPRETED_TERM);
 
+  /**
+   * Maps a name and a free variable or function type to a concrete formula node. We allow only 1
+   * type per var name, meaning there is only 1 column per row!
+   */
+  private final Table<String, Integer, Integer> formulaCache = HashBasedTable.create();
+
   protected Yices2FormulaCreator() {
     super(null, yices_bool_type(), yices_int_type(), yices_real_type(), null, null);
   }
@@ -174,7 +187,7 @@ public Integer getArrayType(Integer pIndexType, Integer pElementType) {
 
   @Override
   public Integer makeVariable(Integer pType, String pVarName) {
-    return yices_named_variable(pType, pVarName);
+    return createNamedVariable(pType, pVarName);
   }
 
   @Override
@@ -246,6 +259,60 @@ public FormulaType<?> getFormulaType(Integer pFormula) {
             yices_type_to_string(yices_type_of_term(pFormula)), yices_term_to_string(pFormula)));
   }
 
+  /** Creates a named, free variable. Might retrieve it from the cache if created prior. */
+  protected int createNamedVariable(int type, String name) {
+    Integer maybeFormula = formulaCache.get(name, type);
+    if (maybeFormula != null) {
+      return maybeFormula;
+    }
+    if (formulaCache.containsRow(name)) {
+      throw new IllegalArgumentException(
+          "Symbol " + name + " already used for a variable of type " + formulaCache.row(name));
+    }
+    int var = yices_new_uninterpreted_term(type);
+    // Names in Yices2 behave like a stack. The last variable named is retrieved when asking for
+    // a term with a specific name. Since we substitute free vars with bound for quantifiers,
+    // this sometimes mixes them up, hence we track them ourselves.
+    yices_set_term_name(var, name);
+    formulaCache.put(name, type, var);
+    return var;
+  }
+
+  protected int createBoundVariableFromFreeVariable(int unboundVar) {
+    int type = yices_type_of_term(unboundVar);
+    String name = yices_get_term_name(unboundVar);
+
+    int termFromName = yices_get_term_by_name(name);
+    if (termFromName != -1) {
+      int termFromNameType = yices_type_of_term(termFromName);
+      if (type == termFromNameType) {
+        int constructor = yices_term_constructor(termFromName);
+        if (constructor == YICES_VARIABLE) {
+          // Already a bound var
+          return termFromName;
+        }
+      } else {
+        throw new IllegalArgumentException(
+            String.format(
+                "Can't create variable with name '%s' and type '%s' "
+                    + "as it would omit a variable with type '%s'",
+                name, yices_type_to_string(type), yices_type_to_string(termFromNameType)));
+      }
+    }
+    // reset term name binding
+    // TODO: add yices_remove_term_name();
+    int bound = yices_new_variable(type);
+    // Names in Yices2 behave like a stack. The last variable named is retrieved when asking for
+    // a term with a specific name. Since we substitute free vars with bound for quantifiers,
+    // this sometimes mixes them up, hence we track them ourselves.
+    // This overrides the naming, but the old is cached.
+    // Meaning that if we remove the new name, the old term gets its name back.
+    // Since we just want to retrieve the same var for the quantifier we are currently building,
+    // this is fine.
+    yices_set_term_name(bound, name);
+    return bound;
+  }
+
   @Override
   public <R> R visit(FormulaVisitor<R> pVisitor, Formula pFormula, Integer pF) {
     int constructor = yices_term_constructor(pF);
@@ -258,6 +325,22 @@ public <R> R visit(FormulaVisitor<R> pVisitor, Formula pFormula, Integer pF) {
         return pVisitor.visitConstant(pFormula, convertValue(pF, pF));
       case YICES_UNINTERPRETED_TERM:
         return pVisitor.visitFreeVariable(pFormula, yices_get_term_name(pF));
+      case YICES_VARIABLE:
+        return pVisitor.visitBoundVariable(pFormula, 0);
+      case YICES_FORALL_TERM:
+        int children = yices_term_num_children(pF);
+        ImmutableList.Builder<Formula> boundVars = ImmutableList.builder();
+        for (int i = 0; i < children - 1; i++) {
+          int boundVar = yices_term_child(pF, i);
+          boundVars.add(encapsulateWithTypeOf(boundVar));
+        }
+        BooleanFormula body = encapsulateBoolean(yices_term_child(pF, children - 1));
+        Quantifier quant = Quantifier.EXISTS;
+        if (yices_term_to_string(pF).startsWith("(forall")) {
+          // TODO: this is stupid, but i could not find a way of discerning between the quantifiers
+          quant = Quantifier.FORALL;
+        }
+        return pVisitor.visitQuantifier((BooleanFormula) pFormula, quant, boundVars.build(), body);
       default:
         return visitFunctionApplication(pVisitor, pFormula, pF, constructor);
     }
@@ -696,7 +779,7 @@ public Integer declareUFImpl(String pName, Integer pReturnType, List<Integer> pA
     } else {
       yicesFuncType = yices_function_type(size, argTypeArray, pReturnType);
     }
-    int uf = yices_named_variable(yicesFuncType, pName);
+    int uf = createNamedVariable(yicesFuncType, pName);
     return uf;
   }
 

src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java

@@ -48,7 +48,8 @@ protected Yices2FormulaManager(
       Yices2BooleanFormulaManager pBooleanManager,
       Yices2IntegerFormulaManager pIntegerManager,
       Yices2RationalFormulaManager pRationalManager,
-      Yices2BitvectorFormulaManager pBitvectorManager) {
+      Yices2BitvectorFormulaManager pBitvectorManager,
+      Yices2QuantifiedFormulaManager pQuantifiedFormulaManager) {
     super(
         pFormulaCreator,
         pFunctionManager,
@@ -57,7 +58,7 @@ protected Yices2FormulaManager(
         pRationalManager,
         pBitvectorManager,
         null,
-        null,
+        pQuantifiedFormulaManager,
         null,
         null,
         null,

src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java

@@ -783,25 +783,6 @@ public static String yices_model_to_string(long m) {
 
   public static native int yices_subst_term(int size, int[] from, int[] to, int t);
 
-  public static int yices_named_variable(int type, String name) {
-    int termFromName = yices_get_term_by_name(name);
-    if (termFromName != -1) {
-      int termFromNameType = yices_type_of_term(termFromName);
-      if (type == termFromNameType) {
-        return termFromName;
-      } else {
-        throw new IllegalArgumentException(
-            String.format(
-                "Can't create variable with name '%s' and type '%s' "
-                    + "as it would omit a variable with type '%s'",
-                name, yices_type_to_string(type), yices_type_to_string(termFromNameType)));
-      }
-    }
-    int var = yices_new_uninterpreted_term(type);
-    yices_set_term_name(var, name);
-    return var;
-  }
-
   /**
    * @return int 1 if the Yices2-lib is compiled thread-safe and 0 otherwise
    */