simplify value conversion for the model across several solvers.

Move common code upwards.
sosy-lab · Nov 19, 2021 · ce41852 · ce41852
1 parent 2d57c51
commit ce41852
Show file tree

Hide file tree

Showing 5 changed files with 7 additions and 26 deletions.
diff --git a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java
@@ -423,7 +423,11 @@ public TFuncDecl getBooleanVarDeclaration(BooleanFormula var) {
    *
    * @param pF the formula to be converted.
    */
-  public abstract Object convertValue(TFormulaInfo pF);
+  public Object convertValue(TFormulaInfo pF) {
+    throw new UnsupportedOperationException(
+        "This SMT solver needs a second term to determine a correct type. "
+            + "Please use the other method 'convertValue(formula, formula)'.");
+  }
 
   /**
    * Convert the formula into a Java object as far as possible, i.e., try to match a primitive or
@@ -432,7 +436,7 @@ public TFuncDecl getBooleanVarDeclaration(BooleanFormula var) {
    * @param pAdditionalF an additonal formula where the type can be received from.
    * @param pF the formula to be converted.
    */
-  // TODO only Mathsat5 needs the second (first) parameter, other solvers ignore it. Avoid it?
+  // only some solvers require the additional (first) parameter, other solvers ignore it.
   public Object convertValue(
       @SuppressWarnings("unused") TFormulaInfo pAdditionalF, TFormulaInfo pF) {
     return convertValue(pF);

diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaCreator.java
@@ -243,7 +243,7 @@ public Long declareUFImpl(String name, Long pReturnType, List<Long> pArgTypes) {
   }
 
   @Override
-  public Object convertValue(Long key, Long term) {
+  public Object convertValue(Long term) {
     String value;
     if (BtorJNI.boolector_is_array(getEnv(), term)) {
       value = BtorJNI.boolector_bv_assignment(getEnv(), term);
@@ -327,11 +327,6 @@ String getName(long pKey) {
     return BtorJNI.boolector_get_symbol(getEnv(), pKey);
   }
 
-  @Override
-  public Object convertValue(Long pF) {
-    throw new UnsupportedOperationException("Please use the other method.");
-  }
-
   @Override
   protected Long getBooleanVarDeclarationImpl(Long pTFormulaInfo) {
     // declaration of constant or fun

diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java
@@ -478,12 +478,6 @@ public Expr declareUFImpl(String pName, Type pReturnType, List<Type> pArgTypes)
     return exp;
   }
 
-  @Override
-  public Object convertValue(Expr pF) {
-    throw new UnsupportedOperationException(
-        "CVC4 needs a second term to determine a correct type. Please use the other method.");
-  }
-
   @Override
   public Object convertValue(Expr expForType, Expr value) {
     final Type type = expForType.getType();

diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java
@@ -504,12 +504,6 @@ private FunctionDeclarationKind getDeclarationKind(long pF) {
     }
   }
 
-  @Override
-  public Object convertValue(Long key) {
-    throw new UnsupportedOperationException(
-        "Mathsat needs a second term to determine a correct type. Please use the other method.");
-  }
-
   @Override
   public Object convertValue(Long key, Long term) {
 

diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java
@@ -732,12 +732,6 @@ private BigInteger parseBitvector(int pF) {
     }
   }
 
-  @Override
-  public Object convertValue(Integer key) {
-    throw new UnsupportedOperationException(
-        "Yices needs a second term to determine a correct type. Please use the other method.");
-  }
-
   @Override
   public Object convertValue(Integer typeKey, Integer pF) {
     FormulaType<?> type = getFormulaType(typeKey);