QuantifiedFormulaManager: disallow an empty variable list for quantification.

Most solvers already enforced a non-empty list of variables for quantification.
This step unifies the precondition check and improves the error message.

Author: kfriedberger

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

@@ -8,6 +8,8 @@
 
 package org.sosy_lab.java_smt.basicimpl;
 
+import static com.google.common.base.Preconditions.checkArgument;
+
 import com.google.common.collect.Lists;
 import java.util.List;
 import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -41,6 +43,8 @@ protected abstract TFormulaInfo eliminateQuantifiers(TFormulaInfo pExtractInfo)
   @Override
   public BooleanFormula mkQuantifier(
       Quantifier q, List<? extends Formula> pVariables, BooleanFormula pBody) {
+    checkArgument(
+        !pVariables.isEmpty(), "Missing variables for quantifier '%s' and body '%s'.", q, pBody);
     return wrap(
         mkQuantifier(q, Lists.transform(pVariables, this::extractInfo), extractInfo(pBody)));
   }

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4QuantifiedFormulaManager.java

@@ -8,6 +8,8 @@
 
 package org.sosy_lab.java_smt.solvers.cvc4;
 
+import static com.google.common.base.Preconditions.checkArgument;
+
 import edu.stanford.CVC4.Expr;
 import edu.stanford.CVC4.ExprManager;
 import edu.stanford.CVC4.Kind;
@@ -72,23 +74,22 @@ protected Expr eliminateQuantifiers(Expr pExtractInfo)
    */
   @Override
   public Expr mkQuantifier(Quantifier pQ, List<Expr> pVars, Expr pBody) {
-    if (pVars.isEmpty()) {
-      throw new IllegalArgumentException("Empty variable list for quantifier.");
-    } else {
-      // CVC4 uses its own lists for quantifier that may only have bound vars
-      vectorExpr vec = new vectorExpr();
-      Expr substBody = pBody;
-      // every free needs a bound copy. As the internal Id is different for every variable, even
-      // with the same name, this is fine.
-      for (Expr var : pVars) {
-        Expr boundCopy = ((CVC4FormulaCreator) formulaCreator).makeBoundCopy(var);
-        vec.add(boundCopy);
-        substBody = substBody.substitute(var, boundCopy);
-      }
-      Expr quantifiedVars = exprManager.mkExpr(Kind.BOUND_VAR_LIST, vec);
+    checkArgument(
+        !pVars.isEmpty(), "Missing variables for quantifier '%s' and body '%s'.", pQ, pBody);
 
-      Kind quant = pQ == Quantifier.EXISTS ? Kind.EXISTS : Kind.FORALL;
-      return exprManager.mkExpr(quant, quantifiedVars, substBody);
+    // CVC4 uses its own lists for quantifier that may only have bound vars
+    vectorExpr vec = new vectorExpr();
+    Expr substBody = pBody;
+    // every free needs a bound copy. As the internal Id is different for every variable, even
+    // with the same name, this is fine.
+    for (Expr var : pVars) {
+      Expr boundCopy = ((CVC4FormulaCreator) formulaCreator).makeBoundCopy(var);
+      vec.add(boundCopy);
+      substBody = substBody.substitute(var, boundCopy);
     }
+    Expr quantifiedVars = exprManager.mkExpr(Kind.BOUND_VAR_LIST, vec);
+
+    Kind quant = pQ == Quantifier.EXISTS ? Kind.EXISTS : Kind.FORALL;
+    return exprManager.mkExpr(quant, quantifiedVars, substBody);
   }
 }

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5QuantifiedFormulaManager.java

@@ -8,6 +8,8 @@
 
 package org.sosy_lab.java_smt.solvers.cvc5;
 
+import static com.google.common.base.Preconditions.checkArgument;
+
 import io.github.cvc5.Kind;
 import io.github.cvc5.Solver;
 import io.github.cvc5.Sort;
@@ -63,22 +65,21 @@ protected Term eliminateQuantifiers(Term input) throws SolverException, Interrup
    */
   @Override
   public Term mkQuantifier(Quantifier pQ, List<Term> pVars, Term pBody) {
-    if (pVars.isEmpty()) {
-      throw new IllegalArgumentException("Empty variable list for quantifier.");
-    } else {
-      List<Term> boundVars = new ArrayList<>();
-      Term substBody = pBody;
-      // every free needs a bound copy. As the internal Id is different for every variable, even
-      // with the same name, this is fine.
-      for (Term var : pVars) {
-        Term boundCopy = ((CVC5FormulaCreator) formulaCreator).makeBoundCopy(var);
-        boundVars.add(boundCopy);
-        substBody = substBody.substitute(var, boundCopy);
-      }
+    checkArgument(
+        !pVars.isEmpty(), "Missing variables for quantifier '%s' and body '%s'.", pQ, pBody);
 
-      Kind quant = pQ == Quantifier.EXISTS ? Kind.EXISTS : Kind.FORALL;
-      Term boundVarsList = termManager.mkTerm(Kind.VARIABLE_LIST, boundVars.toArray(new Term[0]));
-      return termManager.mkTerm(quant, boundVarsList, substBody);
+    List<Term> boundVars = new ArrayList<>();
+    Term substBody = pBody;
+    // every free needs a bound copy. As the internal Id is different for every variable, even
+    // with the same name, this is fine.
+    for (Term var : pVars) {
+      Term boundCopy = ((CVC5FormulaCreator) formulaCreator).makeBoundCopy(var);
+      boundVars.add(boundCopy);
+      substBody = substBody.substitute(var, boundCopy);
     }
+
+    Kind quant = pQ == Quantifier.EXISTS ? Kind.EXISTS : Kind.FORALL;
+    Term boundVarsList = termManager.mkTerm(Kind.VARIABLE_LIST, boundVars.toArray(new Term[0]));
+    return termManager.mkTerm(quant, boundVarsList, substBody);
   }
 }

src/org/sosy_lab/java_smt/solvers/z3/Z3QuantifiedFormulaManager.java

@@ -29,7 +29,12 @@ class Z3QuantifiedFormulaManager extends AbstractQuantifiedFormulaManager<Long,
 
   @Override
   public Long mkQuantifier(Quantifier q, List<Long> pVariables, Long pBody) {
-    checkArgument(!pVariables.isEmpty(), "List of quantified variables can not be empty");
+    checkArgument(
+        !pVariables.isEmpty(),
+        "Missing variables for quantifier '%s' and body '%s'.",
+        q,
+        Native.astToString(z3context, pBody));
+
     return Native.mkQuantifierConst(
         z3context,
         q == Quantifier.FORALL,