Nonlin LA preds

src/api/MainSolver.cc

@@ -9,6 +9,7 @@
 #include "MainSolver.h"
 
 #include <common/ApiException.h>
+#include <common/NonLinException.h>
 #include <itehandler/IteHandler.h>
 #include <logics/ArrayTheory.h>
 #include <logics/LATheory.h>
@@ -347,14 +348,23 @@ sstat MainSolver::check() {
         StopWatch sw(query_timer);
     }
     if (isLastFrameUnsat()) { return s_False; }
-    sstat rval = simplifyFormulas();
+    sstat rval;
+    try {
+        rval = simplifyFormulas();
+    } catch (NonLinException const & error) {
+        reasonUnknown = error.what();
+        return s_Undef;
+    }
 
     if (config.dump_query()) printCurrentAssertionsAsQuery();
 
     if (rval == s_Undef) {
         try {
             rval = solve();
-        } catch (std::overflow_error const & error) { rval = s_Error; }
+        } catch (std::overflow_error const & error) { rval = s_Error; } catch (NonLinException const & error) {
+            reasonUnknown = error.what();
+            return s_Undef;
+        }
         if (rval == s_False) {
             assert(not smt_solver->isOK());
             rememberUnsatFrame(smt_solver->getConflictFrame());

src/api/MainSolver.h

@@ -324,6 +324,7 @@ class MainSolver {
     vec<PTRef> frameTerms;
     std::size_t firstNotSimplifiedFrame = 0;
     unsigned int insertedFormulasCount = 0;
+    std::string reasonUnknown;
 };
 
 bool MainSolver::trackPartitions() const {

src/common/CMakeLists.txt

@@ -25,5 +25,5 @@ include(numbers/CMakeLists.txt)
 install(FILES
         StringMap.h Timer.h inttypes.h IColor.h
         TreeOps.h FlaPartitionMap.h PartitionInfo.h Partitions.h ApiException.h TypeUtils.h
-        NatSet.h ScopedVector.h TermNames.h
+        NatSet.h ScopedVector.h TermNames.h NonLinException.h
 DESTINATION ${INSTALL_HEADERS_DIR}/common)

src/common/NonLinException.h

@@ -0,0 +1,19 @@
+/*
+*  Copyright (c) 2024, Konstantin Britikov <britikovki@gmail.com>
+*
+*  SPDX-License-Identifier: MIT
+*/
+
+#ifndef OPENSMT_NONLINEXCEPTION_H
+#define OPENSMT_NONLINEXCEPTION_H
+
+#include <stdexcept>
+
+namespace opensmt {
+class NonLinException : public std::runtime_error {
+public:
+    NonLinException(std::string_view const reason_) : runtime_error("Term " + std::string(reason_) + " is non-linear"){}
+};
+}
+
+#endif // OPENSMT_NONLINEXCEPTION_H

src/common/polynomials/Translations.cc

@@ -16,12 +16,12 @@ LAPoly ptrefToPoly(PTRef const op, ArithLogic & logic) {
     PTRef const polyTerm = lhs == logic.getZeroForSort(logic.getSortRef(lhs)) ? rhs : logic.mkMinus(rhs, lhs);
     assert(logic.isLinearTerm(polyTerm));
     if (logic.isLinearFactor(polyTerm)) {
-        auto [var, c] = logic.splitTermToVarAndConst(polyTerm);
+        auto [var, c] = logic.splitPolyTerm(polyTerm);
         poly.addTerm(var, logic.getNumConst(c));
     } else {
         assert(logic.isPlus(polyTerm));
         for (PTRef const factor : logic.getPterm(polyTerm)) {
-            auto [var, c] = logic.splitTermToVarAndConst(factor);
+            auto [var, c] = logic.splitPolyTerm(factor);
             poly.addTerm(var, logic.getNumConst(c));
         }
     }