Merge pull request #638 from vprover/signature-optimization

Signature optimization
vprover · Jan 8, 2025 · 1f3a308 · 1f3a308
2 parents 18c72e7 + 743ab47
commit 1f3a308
Show file tree

Hide file tree

Showing 18 changed files with 245 additions and 491 deletions.
diff --git a/Inferences/Instantiation.cpp b/Inferences/Instantiation.cpp
@@ -182,27 +182,21 @@ Term* Instantiation::tryGetDifferentValue(Term* t)
 {
   TermList sort = SortHelper::getResultSort(t);
 
-  try {
-        if(sort == AtomicSort::intSort()){
-              IntegerConstantType constant;
-              if(theory->tryInterpretConstant(t,constant)){
-                return theory->representConstant(constant+1);
-              }
-        } else if(sort == AtomicSort::rationalSort()){
-              RationalConstantType constant;
-              RationalConstantType one(1,1);
-              if(theory->tryInterpretConstant(t,constant)){
-                return theory->representConstant(constant+one);
-              }
-        } else if(sort == AtomicSort::realSort()){
-              RealConstantType constant;
-              RealConstantType one(RationalConstantType(1,1));
-              if(theory->tryInterpretConstant(t,constant)){
-                return theory->representConstant(constant+one);
-              }
-        }
-  } catch (ArithmeticException&) {
-    // return 0 as well
+  if(sort == AtomicSort::intSort()){
+    IntegerConstantType constant;
+    if(theory->tryInterpretConstant(t,constant)){
+      return theory->representConstant(constant+1);
+    }
+  } else if(sort == AtomicSort::rationalSort()){
+    RationalConstantType constant;
+    if(theory->tryInterpretConstant(t,constant)){
+      return theory->representConstant(constant + 1);
+    }
+  } else if(sort == AtomicSort::realSort()){
+    RealConstantType constant;
+    if(theory->tryInterpretConstant(t,constant)){
+      return theory->representConstant(constant + 1);
+    }
   }
 
   return 0;

diff --git a/Inferences/PolynomialEvaluation.cpp b/Inferences/PolynomialEvaluation.cpp
@@ -283,7 +283,8 @@ Polynom<Number> simplifyPoly(Polynom<Number> const& in, PolyNf* simplifiedArgs)
     auto poly = Polynom(std::move(out));
     poly.integrity();
     return poly;
-  } catch (ArithmeticException&) { 
+  } catch (DivByZeroException&) { 
+    // TODO can we remove this?
     return in.replaceTerms(simplifiedArgs);
   }
 }

diff --git a/Kernel/InterpretedLiteralEvaluator.cpp b/Kernel/InterpretedLiteralEvaluator.cpp
@@ -401,7 +401,7 @@ class InterpretedLiteralEvaluator::ConversionEvaluator
 	ASSERTION_VIOLATION;
       }
     }
-    catch(ArithmeticException&)
+    catch(DivByZeroException&)
     {
       return false;
     }
@@ -534,9 +534,8 @@ class InterpretedLiteralEvaluator::TypedEvaluator : public Evaluator
       res = TermList(theory->representConstant(resNum));
       return true;
     }
-    catch(ArithmeticException&)
+    catch(DivByZeroException&)
     {
-       DEBUG( "ArithmeticException" );
       return false;
     }
   }
@@ -571,7 +570,7 @@ class InterpretedLiteralEvaluator::TypedEvaluator : public Evaluator
       }
       return PredEvalResult::trivial(res);
     }
-    catch(ArithmeticException&)
+    catch(DivByZeroException&)
     {
       return PredEvalResult::nop();
     }