Add CVC5 Parsing Support

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

@@ -9,9 +9,9 @@
 package org.sosy_lab.java_smt.solvers.cvc5;
 
 import static com.google.common.base.Preconditions.checkArgument;
+import static com.google.common.base.Preconditions.checkNotNull;
 import static com.google.common.base.Preconditions.checkState;
 
-import com.google.common.base.Preconditions;
 import com.google.common.base.Splitter;
 import com.google.common.collect.FluentIterable;
 import com.google.common.collect.HashBasedTable;
@@ -32,10 +32,14 @@
 import io.github.cvc5.Term;
 import io.github.cvc5.TermManager;
 import java.math.BigInteger;
+import java.util.ArrayDeque;
 import java.util.ArrayList;
+import java.util.Deque;
 import java.util.HashMap;
+import java.util.HashSet;
 import java.util.List;
 import java.util.Map;
+import java.util.Set;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.common.rationals.Rational;
 import org.sosy_lab.java_smt.api.ArrayFormula;
@@ -48,11 +52,13 @@
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType;
 import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
+import org.sosy_lab.java_smt.api.FunctionDeclaration;
 import org.sosy_lab.java_smt.api.FunctionDeclarationKind;
 import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier;
 import org.sosy_lab.java_smt.api.RegexFormula;
 import org.sosy_lab.java_smt.api.StringFormula;
 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;
 import org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl;
 import org.sosy_lab.java_smt.solvers.cvc5.CVC5Formula.CVC5ArrayFormula;
@@ -76,8 +82,9 @@ public class CVC5FormulaCreator extends FormulaCreator<Term, Sort, TermManager,
 
   // <Name, Sort.toString, Term> because CVC5 returns distinct pointers for types, while the
   // String representation is equal (and they are equal)
-  private final Table<String, String, Term> variablesCache = HashBasedTable.create();
-  private final Map<String, Term> functionsCache = new HashMap<>();
+  protected final Table<String, String, Term> variablesCache = HashBasedTable.create();
+  protected final Map<String, Term> functionsCache = new HashMap<>();
+  protected boolean registerUnknownBoundVariables = false;
   private final TermManager termManager;
   private final Solver solver;
 
@@ -103,7 +110,7 @@ public Term makeVariable(Sort sort, String name) {
     if (existingVar != null) {
       return existingVar;
     }
-    Preconditions.checkArgument(
+    checkArgument(
         !variablesCache.containsRow(name),
         "Symbol %s requested with type %s, but already used with type %s",
         name,
@@ -417,7 +424,7 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Term f) {
         // BOUND vars are used for all vars that are bound to a quantifier in CVC5.
         // We resubstitute them back to the original free.
         // CVC5 doesn't give you the de-brujin index
-        Term originalVar = accessVariablesCache(formula.toString(), sort);
+        Term originalVar = getFreeVariableFromCache(formula.toString(), sort, visitor);
         return visitor.visitBoundVariable(encapsulate(originalVar), 0);
 
       } else if (f.getKind() == Kind.FORALL || f.getKind() == Kind.EXISTS) {
@@ -427,7 +434,7 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Term f) {
         List<Formula> freeVars = new ArrayList<>();
         for (Term boundVar : f.getChild(0)) { // unpack grand-children of f.
           String name = getName(boundVar);
-          Term freeVar = Preconditions.checkNotNull(accessVariablesCache(name, boundVar.getSort()));
+          Term freeVar = getFreeVariableFromCache(name, boundVar.getSort(), visitor);
           body = body.substitute(boundVar, freeVar);
           freeVars.add(encapsulate(freeVar));
         }
@@ -439,7 +446,7 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Term f) {
         return visitor.visitFreeVariable(formula, dequote(f.toString()));
 
       } else if (f.getKind() == Kind.APPLY_CONSTRUCTOR) {
-        Preconditions.checkState(
+        checkState(
             f.getNumChildren() == 1, "Unexpected formula '%s' with sort '%s'", f, f.getSort());
         return visitor.visitConstant(formula, f.getChild(0).getSymbol());
 
@@ -768,15 +775,15 @@ public Term declareUFImpl(String pName, Sort pReturnType, List<Sort> pArgTypes)
       functionsCache.put(pName, exp);
 
     } else {
-      Preconditions.checkArgument(
+      checkArgument(
           exp.getSort().equals(exp.getSort()),
           "Symbol %s already in use for different return type %s",
           exp,
           exp.getSort());
       for (int i = 1; i < exp.getNumChildren(); i++) {
         // CVC5s first argument in a function/Uf is the declaration, we don't need that here
         try {
-          Preconditions.checkArgument(
+          checkArgument(
               pArgTypes.get(i).equals(exp.getChild(i).getSort()),
               "Argument %s with type %s does not match expected type %s",
               i - 1,
@@ -843,19 +850,111 @@ private FloatingPointNumber convertFloatingPoint(Term value) throws CVC5ApiExcep
     final var expWidth = Ints.checkedCast(fpValue.first);
     final var mantWidth = Ints.checkedCast(fpValue.second - 1); // without sign bit
     final var bvValue = fpValue.third;
-    Preconditions.checkState(bvValue.isBitVectorValue());
+    checkState(bvValue.isBitVectorValue());
     final var bits = bvValue.getBitVectorValue();
     return FloatingPointNumber.of(bits, expWidth, mantWidth);
   }
 
-  private Term accessVariablesCache(String name, Sort sort) {
+  /**
+   * Returns the free variable for the given name and sort of a bound variable from the variables
+   * cache. Will throw a {@link NullPointerException} if no variable is known for the input!
+   */
+  private Term getFreeVariableFromCache(String name, Sort sort, FormulaVisitor<?> visitor) {
+    if (visitor instanceof BoundVariablesRegisteringRecursiveVisitor) {
+      ((BoundVariablesRegisteringRecursiveVisitor) visitor).registerBoundVariable(name, sort);
+    }
     Term existingVar = variablesCache.get(name, sort.toString());
-    Preconditions.checkNotNull(
+    return checkNotNull(
         existingVar,
-        "Symbol %s requested with type %s, but already used with type %s",
+        "Symbol %s requested with type %s, but %s",
         name,
         sort,
-        variablesCache.row(name).keySet());
-    return existingVar;
+        variablesCache.containsRow(name)
+            ? "the used symbol is already registered with type " + variablesCache.row(name).keySet()
+            : "the used symbol is unknown to the variables cache");
+  }
+
+  /**
+   * Caches all bound variables nested in the boolean input term that are unknown to the variable
+   * cache with a free variable copy in it.
+   */
+  protected void registerBoundVariablesWithVisitor(Term input) {
+    checkArgument(
+        input.getSort().isBoolean(),
+        "Only boolean terms can be used to register " + "bound variables as free variables!");
+
+    BoundVariablesRegisteringRecursiveVisitor boundVariablesRegisteringRecursiveVisitor =
+        new BoundVariablesRegisteringRecursiveVisitor(this);
+
+    boundVariablesRegisteringRecursiveVisitor.addToQueue(encapsulateBoolean(input));
+    while (!boundVariablesRegisteringRecursiveVisitor.isQueueEmpty()) {
+      Formula tt = boundVariablesRegisteringRecursiveVisitor.pop();
+      TraversalProcess process = visit(tt, boundVariablesRegisteringRecursiveVisitor);
+      if (process == TraversalProcess.ABORT) {
+        return;
+      }
+    }
+  }
+
+  private static final class BoundVariablesRegisteringRecursiveVisitor
+      implements FormulaVisitor<TraversalProcess> {
+
+    private final Set<Formula> seen = new HashSet<>();
+    private final Deque<Formula> toVisit = new ArrayDeque<>();
+
+    private final CVC5FormulaCreator usedCreator;
+
+    BoundVariablesRegisteringRecursiveVisitor(CVC5FormulaCreator pCreator) {
+      usedCreator = checkNotNull(pCreator);
+    }
+
+    private void registerBoundVariable(String boundVariableName, Sort boundVarSort) {
+      String boundSort = boundVarSort.toString();
+      Term existingVar = usedCreator.variablesCache.get(boundVariableName, boundSort);
+      if (existingVar == null) {
+        existingVar = usedCreator.makeVariable(boundVarSort, boundVariableName);
+        usedCreator.variablesCache.put(boundVariableName, boundSort, existingVar);
+      }
+    }
+
+    void addToQueue(Formula f) {
+      if (seen.add(f)) {
+        toVisit.push(f);
+      }
+    }
+
+    boolean isQueueEmpty() {
+      return toVisit.isEmpty();
+    }
+
+    Formula pop() {
+      return toVisit.pop();
+    }
+
+    @Override
+    public TraversalProcess visitFreeVariable(Formula pF, String pName) {
+      return TraversalProcess.CONTINUE;
+    }
+
+    @Override
+    public TraversalProcess visitConstant(Formula pF, Object pValue) {
+      return TraversalProcess.CONTINUE;
+    }
+
+    @Override
+    public TraversalProcess visitFunction(
+        Formula pF, List<Formula> pArgs, FunctionDeclaration<?> pFunctionDeclaration) {
+      for (Formula f : pArgs) {
+        addToQueue(f);
+      }
+      return TraversalProcess.CONTINUE;
+    }
+
+    @Override
+    public TraversalProcess visitQuantifier(
+        BooleanFormula pF, Quantifier pQuantifier, List<Formula> boundVars, BooleanFormula pBody) {
+      addToQueue(pBody);
+      return TraversalProcess.CONTINUE;
+    }
   }
 }