CVC5: Add parser support

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

@@ -34,9 +34,7 @@
 import java.lang.reflect.Array;
 import java.math.BigInteger;
 import java.util.ArrayList;
-import java.util.HashMap;
 import java.util.List;
-import java.util.Map;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.common.rationals.Rational;
 import org.sosy_lab.java_smt.api.ArrayFormula;
@@ -72,13 +70,9 @@ public class CVC5FormulaCreator extends FormulaCreator<Term, Sort, TermManager,
   /** CVC5 does not allow using some key-functions from SMTLIB2 as identifiers. */
   private static final ImmutableSet<String> UNSUPPORTED_IDENTIFIERS = ImmutableSet.of("let");
 
-  // private static final Pattern FLOATING_POINT_PATTERN = Pattern.compile("^\\(fp #b(?<sign>\\d)
-  // #b(?<exp>\\d+) #b(?<mant>\\d+)$");
+  /** We use a variable cache to keep track of variables/Ufs that have already been defined. */
+  private final Table<String, Sort, Term> variablesCache = HashBasedTable.create();
 
-  // <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<>();
   private final TermManager termManager;
   private final Solver solver;
 
@@ -98,9 +92,13 @@ public Solver getSolver() {
     return solver;
   }
 
+  Table<String, Sort, Term> getDeclaredVariables() {
+    return variablesCache;
+  }
+
   @Override
   public Term makeVariable(Sort sort, String name) {
-    Term existingVar = variablesCache.get(name, sort.toString());
+    Term existingVar = variablesCache.get(name, sort);
     if (existingVar != null) {
       return existingVar;
     }
@@ -124,7 +122,7 @@ public Term makeVariable(Sort sort, String name) {
                   .getKey());
     }
     Term newVar = termManager.mkConst(sort, name);
-    variablesCache.put(name, sort.toString(), newVar);
+    variablesCache.put(name, sort, newVar);
     return newVar;
   }
 
@@ -426,21 +424,14 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Term f) {
                 getFormulaType(f),
                 f.getKind()));
 
-      } else if (f.getKind() == Kind.VARIABLE) {
-        // 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);
-        return visitor.visitBoundVariable(encapsulate(originalVar), 0);
-
       } else if (f.getKind() == Kind.FORALL || f.getKind() == Kind.EXISTS) {
         // QUANTIFIER: replace bound variable with free variable for visitation
         assert f.getNumChildren() == 2;
         Term body = f.getChild(1);
         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 = makeVariable(boundVar.getSort(), name);
           body = body.substitute(boundVar, freeVar);
           freeVars.add(encapsulate(freeVar));
         }
@@ -520,7 +511,7 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Term f) {
    * back to a common one.
    */
   private Term normalize(Term operator) {
-    Term function = functionsCache.get(getName(operator));
+    Term function = variablesCache.get(getName(operator), operator.getSort());
     if (function != null) {
       checkState(
           function.getId() == operator.getId(),
@@ -766,20 +757,19 @@ private void checkSymbol(String symbol) {
   public Term declareUFImpl(String pName, Sort pReturnType, List<Sort> pArgTypes) {
     checkSymbol(pName);
 
-    Term exp = functionsCache.get(pName);
+    // Ufs in CVC5 can't have 0 arity. We just use a variable as a workaround.
+    Sort termSort =
+        pArgTypes.isEmpty()
+            ? pReturnType
+            : environment.mkFunctionSort(pArgTypes.toArray(new Sort[0]), pReturnType);
+    Term exp = variablesCache.get(pName, termSort);
 
     if (exp == null) {
-      // Ufs in CVC5 can't have 0 arity. We just use a variable as a workaround.
-      Sort sort =
-          pArgTypes.isEmpty()
-              ? pReturnType
-              : termManager.mkFunctionSort(pArgTypes.toArray(new Sort[0]), pReturnType);
-      exp = termManager.mkConst(sort, pName);
-      functionsCache.put(pName, exp);
-
+      exp = termManager.mkConst(termSort, pName);
+      variablesCache.put(pName, exp.getSort(), exp);
     } else {
       Preconditions.checkArgument(
-          exp.getSort().equals(exp.getSort()),
+          pReturnType.equals(exp.getSort().getFunctionCodomainSort()),
           "Symbol %s already in use for different return type %s",
           exp,
           exp.getSort());
@@ -801,6 +791,11 @@ public Term declareUFImpl(String pName, Sort pReturnType, List<Sort> pArgTypes)
     return exp;
   }
 
+  @Override
+  public Object convertValue(Term pValue) {
+    return convertValue(pValue, pValue);
+  }
+
   @Override
   public Object convertValue(Term expForType, Term value) {
     final Sort type = expForType.getSort();
@@ -857,28 +852,4 @@ private FloatingPointNumber convertFloatingPoint(Term value) throws CVC5ApiExcep
     final var bits = bvValue.getBitVectorValue();
     return FloatingPointNumber.of(bits, expWidth, mantWidth);
   }
-
-  private Term accessVariablesCache(String name, Sort sort) {
-    Term existingVar = variablesCache.get(name, sort.toString());
-    if (existingVar == null) {
-      throw new IllegalArgumentException(
-          "Symbol "
-              + name
-              + " requested with type "
-              + sort
-              + ", but "
-              + "already "
-              + "used "
-              + "with "
-              + "type"
-              + variablesCache
-                  .rowMap()
-                  .get(name)
-                  .entrySet()
-                  .toArray((java.util.Map.Entry[]) Array.newInstance(java.util.Map.Entry.class, 0))[
-                  0]
-                  .getKey());
-    }
-    return existingVar;
-  }
 }

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

@@ -9,18 +9,30 @@
 package org.sosy_lab.java_smt.solvers.cvc5;
 
 import com.google.common.base.Joiner;
+import com.google.common.base.Preconditions;
+import com.google.common.collect.ImmutableList;
 import com.google.common.collect.Iterables;
+import com.google.common.collect.Table;
+import com.google.common.collect.Table.Cell;
 import de.uni_freiburg.informatik.ultimate.logic.PrintTerm;
 import io.github.cvc5.CVC5ApiException;
+import io.github.cvc5.Command;
+import io.github.cvc5.InputParser;
 import io.github.cvc5.Kind;
+import io.github.cvc5.Solver;
 import io.github.cvc5.Sort;
+import io.github.cvc5.SymbolManager;
 import io.github.cvc5.Term;
 import io.github.cvc5.TermManager;
+import io.github.cvc5.modes.InputLanguage;
+import java.util.HashMap;
 import java.util.LinkedHashMap;
+import java.util.List;
 import java.util.Map;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager;
+import org.sosy_lab.java_smt.basicimpl.Tokenizer;
 
 class CVC5FormulaManager extends AbstractFormulaManager<Term, Sort, TermManager, Term> {
 
@@ -66,7 +78,138 @@ static Term getCVC5Term(Formula pT) {
 
   @Override
   public Term parseImpl(String formulaStr) throws IllegalArgumentException {
-    throw new UnsupportedOperationException();
+    // Split the input string into a list of SMT-LIB2 commands
+    List<String> tokens = Tokenizer.tokenize(formulaStr);
+
+    Table<String, Sort, Term> cache = creator.getDeclaredVariables();
+
+    // Process the declarations
+    Map<String, Sort> localSymbols = new HashMap<>();
+    ImmutableList.Builder<String> processed = ImmutableList.builder();
+    for (String token : tokens) {
+      if (Tokenizer.isDeclarationToken(token)) {
+        // Parse the variable/UF declaration to get a name
+        Solver solver = new Solver(getEnvironment());
+        InputParser parser = new InputParser(solver);
+        SymbolManager symbolManager = new SymbolManager(getEnvironment());
+        parser.setStringInput(InputLanguage.SMT_LIB_2_6, "(set-logic ALL)" + token, "");
+        parser.nextCommand().invoke(solver, symbolManager);
+        parser.nextCommand().invoke(solver, symbolManager);
+
+        Term parsed = symbolManager.getDeclaredTerms()[0];
+
+        String symbol = parsed.getSymbol();
+        if (symbol.startsWith("|") && symbol.endsWith("|")) {
+          // Strip quotes from the name
+          symbol = symbol.substring(1, symbol.length() - 1);
+        }
+        Sort sort = parsed.getSort();
+
+        // Check if the symbol is already defined in the variable cache
+        if (cache.containsRow(symbol)) {
+          Sort typeDefinition = cache.row(symbol).keySet().toArray(new Sort[0])[0];
+          Preconditions.checkArgument(
+              cache.contains(symbol, sort),
+              "Symbol '%s' is already used by the solver with a different type. The new type is "
+                  + "%s, but we already have a definition with type %s.",
+              symbol,
+              sort,
+              typeDefinition);
+          continue; // Skip if it's a redefinition
+        }
+
+        // Check if it collides with a definition that was parsed earlier
+        Preconditions.checkArgument(
+            !localSymbols.containsKey(symbol) || localSymbols.get(symbol).equals(sort),
+            "Symbol '%s' has already been defined by this script with a different type. The new "
+                + "type is %s, but we have already a definition with type %s.",
+            symbol,
+            sort,
+            localSymbols.get(symbol));
+
+        // Add the symbol to the local definitions for this parse
+        localSymbols.put(symbol, sort);
+      }
+      // Otherwise, keep the command
+      processed.add(token);
+    }
+
+    // Build SMT-LIB2 declarations for all variables in the cache
+    ImmutableList.Builder<String> builder = ImmutableList.builder();
+    for (Cell<String, Sort, Term> c : cache.cellSet()) {
+      String symbol = c.getValue().toString();
+      List<Sort> args = ImmutableList.of();
+      Sort sort = c.getValue().getSort();
+
+      if (sort.isFunction()) {
+        args = List.of(sort.getFunctionDomainSorts());
+        sort = sort.getFunctionCodomainSort();
+      }
+      StringBuilder decl = new StringBuilder();
+      decl.append("(declare-fun").append(" ");
+      decl.append(symbol).append(" ");
+      decl.append("(");
+      for (Sort p : args) {
+        decl.append(p).append(" ");
+      }
+      decl.append(")").append(" ");
+      decl.append(sort);
+      decl.append(")");
+
+      builder.add(decl.toString());
+    }
+
+    String decls = String.join("\n", builder.build());
+    String input = String.join("\n", processed.build());
+
+    // Add the declarations to the input and parse everything
+    Solver solver = new Solver(getEnvironment());
+    InputParser parser = new InputParser(solver);
+    SymbolManager symbolManager = parser.getSymbolManager();
+    parser.setStringInput(InputLanguage.SMT_LIB_2_6, "(set-logic ALL)" + decls + input, "");
+
+    Command cmd = parser.nextCommand();
+    while (!cmd.isNull()) {
+      try {
+        Preconditions.checkArgument(
+            ImmutableList.of("set-logic", "declare-fun", "declare-const", "define-fun", "assert")
+                .contains(cmd.getCommandName()),
+            "Command %s is not supported",
+            cmd.getCommandName());
+        cmd.invoke(solver, symbolManager);
+        cmd = parser.nextCommand();
+      } catch (Throwable e) {
+        throw new IllegalArgumentException(e);
+      }
+    }
+
+    // Get the assertions from the input
+    Term[] asserted = solver.getAssertions();
+    Term result = asserted.length == 1 ? asserted[0] : getEnvironment().mkTerm(Kind.AND, asserted);
+
+    // Now get all declared symbols
+    Term[] declared = symbolManager.getDeclaredTerms();
+
+    // Process the symbols from the parser
+    Map<Term, Term> subst = new HashMap<>();
+    for (Term term : declared) {
+      String symbol = term.getSymbol();
+      if (symbol.startsWith("|") && symbol.endsWith("|")) {
+        // Strip quotes from the name
+        symbol = symbol.substring(1, symbol.length() - 1);
+      }
+      if (cache.containsRow(symbol)) {
+        // Symbol is from the context: add the original term to the substitution map
+        subst.put(term, cache.get(symbol, term.getSort()));
+      } else {
+        // Symbol is new, add it to the context
+        cache.put(symbol, term.getSort(), term);
+      }
+    }
+
+    // Substitute all symbols from the context with their original terms
+    return result.substitute(
+        subst.keySet().toArray(new Term[0]), subst.values().toArray(new Term[0]));
   }
 
   @Override