Disabled flexible Farkas itps for integers

usi-verification-and-security · Nov 23, 2024 · 5173223 · 5173223
1 parent 71b7042
commit 5173223
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 4 deletions.
diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc
@@ -776,7 +776,7 @@ PTRef LASolver::interpolateUsingEngine(FarkasInterpolator & interpolator) const
     auto itpAlgorithm = config.getLRAInterpolationAlgorithm();
     if (itpAlgorithm == itp_lra_alg_strong) { return interpolator.getFarkasInterpolant(); }
     else if (itpAlgorithm == itp_lra_alg_weak) { return interpolator.getDualFarkasInterpolant(); }
-    else if (itpAlgorithm == itp_lra_alg_factor) { return interpolator.getFlexibleInterpolant(Real(config.getLRAStrengthFactor())); }
+    else if (itpAlgorithm == itp_lra_alg_factor) { assert(not logic.hasIntegers()); return interpolator.getFlexibleInterpolant(Real(config.getLRAStrengthFactor())); }
     else if (itpAlgorithm == itp_lra_alg_decomposing_strong) { return interpolator.getDecomposedInterpolant(); }
     else if (itpAlgorithm == itp_lra_alg_decomposing_weak) { return interpolator.getDualDecomposedInterpolant(); }
     else {

diff --git a/src/tsolvers/lasolver/LIAInterpolator.h b/src/tsolvers/lasolver/LIAInterpolator.h
@@ -22,6 +22,9 @@ struct LAExplanations {
 class LIAInterpolator : public FarkasInterpolator {
 public:
     LIAInterpolator(ArithLogic & logic, LAExplanations liaExplanations);
+
+    // not implemented for integers
+    PTRef getFlexibleInterpolant(Real strengthFactor) = delete;
 };
 } // namespace opensmt
 

diff --git a/test/unit/test_LIAInterpolation.cc b/test/unit/test_LIAInterpolation.cc
@@ -52,9 +52,10 @@ TEST_F(LIAInterpolationTest, test_InterpolationLRASat){
     PTRef dualFarkasItp = interpolator.getDualFarkasInterpolant();
     std::cout << logic.pp(dualFarkasItp) << std::endl;
     EXPECT_TRUE(verifyInterpolant(leq1, leq2, dualFarkasItp));
-    PTRef halfFarkasItp = interpolator.getFlexibleInterpolant(Number(1,2));
-    std::cout << logic.pp(halfFarkasItp) << std::endl;
-    EXPECT_TRUE(verifyInterpolant(leq1, leq2, halfFarkasItp));
+    // not implemented for integers
+    // PTRef halfFarkasItp = interpolator.getFlexibleInterpolant(Number(1,2));
+    // std::cout << logic.pp(halfFarkasItp) << std::endl;
+    // EXPECT_TRUE(verifyInterpolant(leq1, leq2, halfFarkasItp));
 }
 
 TEST_F(LIAInterpolationTest, test_DecompositionInLIA){