Princess: improve visiting quantified formulas.

The user should never come across a situation without variables,
and internally, we avoid this, too.

Author: kfriedberger

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

@@ -14,6 +14,7 @@
 import static org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.toSeq;
 import static scala.collection.JavaConverters.asJava;
 import static scala.collection.JavaConverters.asJavaCollection;
+import static scala.collection.JavaConverters.asScala;
 
 import ap.basetypes.IdealInt;
 import ap.parser.IAtom;
@@ -38,7 +39,6 @@
 import ap.parser.ITermITE;
 import ap.parser.ITimes;
 import ap.parser.IVariable;
-import ap.terfor.conjunctions.Quantifier;
 import ap.terfor.preds.Predicate;
 import ap.theories.arrays.ExtArray;
 import ap.theories.bitvectors.ModuloArithmetic;
@@ -53,11 +53,11 @@
 import com.google.common.collect.ImmutableSet;
 import com.google.common.collect.Table;
 import java.lang.reflect.InvocationTargetException;
-import java.util.ArrayList;
 import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
 import java.util.Set;
+import org.sosy_lab.common.UniqueIdGenerator;
 import org.sosy_lab.common.rationals.Rational;
 import org.sosy_lab.java_smt.api.ArrayFormula;
 import org.sosy_lab.java_smt.api.BitvectorFormula;
@@ -66,6 +66,7 @@
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.FunctionDeclarationKind;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
+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;
@@ -184,6 +185,9 @@ class PrincessFormulaCreator
    */
   private final Table<Sort, Sort, Sort> arraySortCache = HashBasedTable.create();
 
+  // Keeps track of the bound/free variables created when visiting quantified terms.
+  private final UniqueIdGenerator boundVariablesId = new UniqueIdGenerator();
+
   PrincessFormulaCreator(PrincessEnvironment pEnv) {
     super(
         pEnv,
@@ -398,19 +402,7 @@ public <R> R visit(FormulaVisitor<R> visitor, final Formula f, final IExpression
       return visitor.visitConstant(f, convertValue(input));
 
     } else if (input instanceof IQuantified) {
-      // this is a quantifier
-
-      BooleanFormula body = encapsulateBoolean(((IQuantified) input).subformula());
-      return visitor.visitQuantifier(
-          (BooleanFormula) f,
-          ((IQuantified) input).quan().equals(Quantifier.apply(true)) ? FORALL : EXISTS,
-
-          // Princess does not hold any metadata about bound variables,
-          // so we can't get meaningful list here.
-          // HOWEVER, passing this list to QuantifiedFormulaManager#mkQuantifier
-          // works as expected.
-          new ArrayList<>(),
-          body);
+      return visitQuantifier(visitor, (BooleanFormula) f, (IQuantified) input);
 
     } else if (input instanceof IVariable) {
       // variable bound by a quantifier
@@ -539,6 +531,29 @@ public <R> R visit(FormulaVisitor<R> visitor, final Formula f, final IExpression
             getName(input), kind, argTypes.build(), getFormulaType(f), solverDeclaration));
   }
 
+  private <R> R visitQuantifier(FormulaVisitor<R> visitor, BooleanFormula f, IQuantified input) {
+    Quantifier quantifier =
+        input.quan().equals(ap.terfor.conjunctions.Quantifier.apply(true)) ? FORALL : EXISTS;
+    IFormula body = input.subformula();
+
+    // Princess uses de-Bruijn indices, so we have index 0 here for the most outer quantified scope
+    IVariable boundVariable = input.sort().boundVariable(0);
+    String boundVariableName = "__JAVASMT__BOUND_VARIABLE_" + boundVariablesId.getFreshId();
+    // Currently, Princess supports only non-boolean bound variables, so we can cast to ITerm.
+    ITerm substitutionVariable = (ITerm) makeVariable(boundVariable.sort(), boundVariableName);
+
+    // substitute the bound variable with a new variable,
+    // and un-shift the remaining de-Bruijn indices.
+    IFormula substitutedBody =
+        IFormula.subst(body, asScala(List.of(substitutionVariable)).toList(), -1);
+
+    return visitor.visitQuantifier(
+        f,
+        quantifier,
+        List.of(encapsulateWithTypeOf(substitutionVariable)),
+        encapsulateBoolean(substitutedBody));
+  }
+
   private boolean isBitvectorOperationWithAdditionalArgument(FunctionDeclarationKind kind) {
     switch (kind) {
       case BV_NOT:

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

@@ -14,12 +14,11 @@
 import ap.parser.IConstant;
 import ap.parser.IExpression;
 import ap.parser.IFormula;
-import ap.parser.ISortedQuantified;
 import ap.terfor.ConstantTerm;
 import ap.terfor.conjunctions.Quantifier.ALL$;
 import ap.terfor.conjunctions.Quantifier.EX$;
 import ap.types.Sort;
-import java.util.ArrayList;
+import com.google.common.collect.Lists;
 import java.util.List;
 import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.basicimpl.AbstractQuantifiedFormulaManager;
@@ -40,24 +39,17 @@ class PrincessQuantifiedFormulaManager
 
   @Override
   public IExpression mkQuantifier(Quantifier q, List<IExpression> vars, IExpression body) {
+    checkArgument(!vars.isEmpty(), "Missing variables for quantifier '%s' and body '%s'.", q, body);
+
     checkArgument(body instanceof IFormula);
     ap.terfor.conjunctions.Quantifier pq = (q == Quantifier.FORALL) ? ALL$.MODULE$ : EX$.MODULE$;
-    if (vars.isEmpty()) {
 
-      // Body already contains bound variables.
-      return new ISortedQuantified(pq, PrincessEnvironment.INTEGER_SORT, (IFormula) body);
-    } else {
-      // TODO: add support for boolean quantification!
-      return IExpression.quanConsts(pq, asScala(toConstantTerm(vars)), (IFormula) body);
-    }
+    // TODO: add support for boolean quantification!
+    return IExpression.quanConsts(pq, asScala(toConstantTerms(vars)), (IFormula) body);
   }
 
-  private List<ConstantTerm> toConstantTerm(List<IExpression> lst) {
-    List<ConstantTerm> retVal = new ArrayList<>(lst.size());
-    for (IExpression f : lst) {
-      retVal.add(((IConstant) f).c());
-    }
-    return retVal;
+  private List<ConstantTerm> toConstantTerms(List<IExpression> lst) {
+    return Lists.transform(lst, f -> ((IConstant) f).c());
   }
 
   @Override

src/org/sosy_lab/java_smt/test/FormulaClassifierTest.java

@@ -136,6 +136,27 @@ public void test_LRA() {
     assertThat(classifier.toString()).isEqualTo("LRA");
   }
 
+  @Test
+  public void test_LRA_2() {
+    requireParser();
+    requireRationals();
+    requireQuantifiers();
+    requireRationals();
+    String query =
+        NUMERAL_VARS
+            + "(assert (and "
+            + "(exists ((a Real) (b Real)) (= (+ y y) (+ a b))) "
+            + "(exists ((a Real) (b Real)) (= (+ y y) (- a b))) "
+            + "))";
+    classifier.visit(mgr.parse(query));
+    if (solverToUse() == Solvers.PRINCESS) {
+      // Princess rewrites the formula and uses '-1' for the negation -> Integer arithmetic
+      assertThat(classifier.toString()).isEqualTo("LIRA");
+    } else {
+      assertThat(classifier.toString()).isEqualTo("LRA");
+    }
+  }
+
   @Test
   public void test_ABVIRA() {
     requireParser();