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>
@@ -333,14 +334,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

@@ -310,6 +310,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

@@ -24,5 +24,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,23 @@
+/*
+*  Copyright (c) 2024, Konstantin Britikov <[email protected]>
+*
+*  SPDX-License-Identifier: MIT
+*/
+
+#ifndef OPENSMT_NONLINEXCEPTION_H
+#define OPENSMT_NONLINEXCEPTION_H
+
+namespace opensmt {
+class NonLinException : public std::runtime_error {
+public:
+    NonLinException(std::string_view const reason_) : runtime_error(std::string(reason_)) {
+        msg = "Term " + std::string(reason_) + " is non-linear";
+    }
+    virtual char const * what() const noexcept override { return msg.c_str(); }
+
+private:
+    std::string msg;
+};
+}
+
+#endif // OPENSMT_NONLINEXCEPTION_H

src/logics/ArithLogic.h

@@ -8,16 +8,6 @@
 #include <numeric>
 
 namespace opensmt {
-class LANonLinearException : public std::runtime_error {
-public:
-    LANonLinearException(char const * reason_) : runtime_error(reason_) {
-        msg = "Term " + std::string(reason_) + " is non-linear";
-    }
-    virtual char const * what() const noexcept override { return msg.c_str(); }
-
-private:
-    std::string msg;
-};
 
 class ArithDivisionByZeroException : public std::runtime_error {
 public:
@@ -105,6 +95,10 @@ class ArithLogic : public Logic {
 
     SymRef get_sym_Int_TIMES() const { return sym_Int_TIMES; }
     SymRef get_sym_Real_TIMES() const { return sym_Real_TIMES; }
+    SymRef get_sym_Int_TIMES_LIN() const { return sym_Int_TIMES_LIN; }
+    SymRef get_sym_Real_TIMES_LIN() const { return sym_Real_TIMES_LIN; }
+    SymRef get_sym_Int_TIMES_NONLIN() const { return sym_Int_TIMES_NONLIN; }
+    SymRef get_sym_Real_TIMES_NONLIN() const { return sym_Real_TIMES_NONLIN; }
     SymRef get_sym_Int_DIV() const { return sym_Int_DIV; }
     SymRef get_sym_Int_MOD() const { return sym_Int_MOD; }
     SymRef get_sym_Real_DIV() const { return sym_Real_DIV; }
@@ -170,10 +164,22 @@ class ArithLogic : public Logic {
     bool isIntNeg(SymRef sr) const { return sr == sym_Int_NEG; }
     bool isRealNeg(SymRef sr) const { return sr == sym_Real_NEG; }
 
-    bool isTimes(SymRef sr) const { return isIntTimes(sr) or isRealTimes(sr); }
+    bool isTimes(SymRef sr) const { return isTimesLin(sr) or isTimesNonlin(sr) or isIntTimes(sr) or isRealTimes(sr); };
+    bool isTimesLinOrNonlin(SymRef sr) const { return isTimesLin(sr) or isTimesNonlin(sr); };
+    bool isTimesLin(SymRef sr) const { return isIntTimesLin(sr) or isRealTimesLin(sr); }
+    bool isTimesNonlin(SymRef sr) const { return isIntTimesNonlin(sr) or isRealTimesNonlin(sr); }
     bool isTimes(PTRef tr) const { return isTimes(getPterm(tr).symb()); }
-    bool isIntTimes(PTRef tr) const { return isIntTimes(getPterm(tr).symb()); }
-    bool isRealTimes(PTRef tr) const { return isRealTimes(getPterm(tr).symb()); }
+    bool isTimesLinOrNonlin(PTRef tr) const { return isTimesLinOrNonlin(getPterm(tr).symb()); };
+    bool isTimesLin(PTRef tr) const { return isTimesLin(getPterm(tr).symb()); }
+    bool isTimesNonlin(PTRef tr) const { return isTimesNonlin(getPterm(tr).symb()); }
+    bool isIntTimesLin(PTRef tr) const { return isIntTimesLin(getPterm(tr).symb()); }
+    bool isIntTimesNonlin(PTRef tr) const { return isIntTimesNonlin(getPterm(tr).symb()); }
+    bool isRealTimesLin(PTRef tr) const { return isRealTimesLin(getPterm(tr).symb()); }
+    bool isRealTimesNonlin(PTRef tr) const { return isRealTimesNonlin(getPterm(tr).symb()); }
+    bool isIntTimesLin(SymRef sr) const { return sr == sym_Int_TIMES_LIN; }
+    bool isIntTimesNonlin(SymRef sr) const { return sr == sym_Int_TIMES_NONLIN; }
+    bool isRealTimesLin(SymRef sr) const { return sr == sym_Real_TIMES_LIN; }
+    bool isRealTimesNonlin(SymRef sr) const { return sr == sym_Real_TIMES_NONLIN; }
     bool isIntTimes(SymRef sr) const { return sr == sym_Int_TIMES; }
     bool isRealTimes(SymRef sr) const { return sr == sym_Real_TIMES; }
 
@@ -222,10 +228,10 @@ class ArithLogic : public Logic {
 
     bool isNumVar(SymRef sr) const { return isVar(sr) and (yieldsSortInt(sr) or yieldsSortReal(sr)); }
     bool isNumVar(PTRef tr) const { return isNumVar(getPterm(tr).symb()); }
-    bool isNumVarLike(SymRef sr) const {
-        return yieldsSortNum(sr) and not isPlus(sr) and not isTimes(sr) and not isNumConst(sr);
+    bool isMonomial(PTRef tr) const {
+        SymRef sr = getPterm(tr).symb();
+        return yieldsSortNum(sr) and not isPlus(sr) and not isTimesLin(sr) and not isNumConst(sr);
     }
-    bool isNumVarLike(PTRef tr) const { return isNumVarLike(getPterm(tr).symb()); }
 
     bool isZero(SymRef sr) const { return isIntZero(sr) or isRealZero(sr); }
     bool isZero(PTRef tr) const { return isZero(getSymRef(tr)); }
@@ -267,7 +273,8 @@ class ArithLogic : public Logic {
     }
 
     SymRef getPlusForSort(SRef sort) const;
-    SymRef getTimesForSort(SRef sort) const;
+    SymRef getTimesLinForSort(SRef sort) const;
+    SymRef getTimesNonlinForSort(SRef sort) const;
     SymRef getMinusForSort(SRef sort) const;
 
     PTRef getZeroForSort(SRef sort) const;
@@ -346,7 +353,8 @@ class ArithLogic : public Logic {
     bool isLinearTerm(PTRef tr) const;
     bool isLinearFactor(PTRef tr) const;
     pair<Number, vec<PTRef>> getConstantAndFactors(PTRef sum) const;
-    pair<PTRef, PTRef> splitTermToVarAndConst(PTRef term) const;
+    // Given a term `t` is splits the term into monomial and its coefficient
+    pair<PTRef, PTRef> splitPolyTerm(PTRef term) const;
     PTRef normalizeMul(PTRef mul);
     // Given a sum term 't' returns a normalized inequality 'c <= s' equivalent to '0 <= t'
     PTRef sumToNormalizedInequality(PTRef sum);
@@ -380,6 +388,9 @@ class ArithLogic : public Logic {
     PTRef mkBinaryGeq(PTRef lhs, PTRef rhs) { return mkBinaryLeq(rhs, lhs); }
     PTRef mkBinaryLt(PTRef lhs, PTRef rhs) { return mkNot(mkBinaryGeq(lhs, rhs)); }
     PTRef mkBinaryGt(PTRef lhs, PTRef rhs) { return mkNot(mkBinaryLeq(lhs, rhs)); }
+    SymRef declareFun_Multiplication_LinNonlin(std::string const & s, SRef rsort, vec<SRef> const & args) {
+        return sym_store.newInternalSymb(s.c_str(), rsort, args, SymConf::CommutativeNoScopingLeftAssoc);
+    }
     PTRef mkBinaryEq(PTRef lhs, PTRef rhs) override;
     pair<Number, PTRef> sumToNormalizedPair(PTRef sum);
     pair<Number, PTRef> sumToNormalizedIntPair(PTRef sum);
@@ -431,6 +442,8 @@ class ArithLogic : public Logic {
     SymRef sym_Real_MINUS;
     SymRef sym_Real_PLUS;
     SymRef sym_Real_TIMES;
+    SymRef sym_Real_TIMES_LIN;
+    SymRef sym_Real_TIMES_NONLIN;
     SymRef sym_Real_DIV;
     SymRef sym_Real_EQ;
     SymRef sym_Real_LEQ;
@@ -451,6 +464,8 @@ class ArithLogic : public Logic {
     SymRef sym_Int_MINUS;
     SymRef sym_Int_PLUS;
     SymRef sym_Int_TIMES;
+    SymRef sym_Int_TIMES_LIN;
+    SymRef sym_Int_TIMES_NONLIN;
     SymRef sym_Int_DIV;
     SymRef sym_Int_MOD;
     SymRef sym_Int_EQ;

src/rewriters/DivModRewriter.h

@@ -11,6 +11,7 @@
 #include "Rewriter.h"
 
 #include <common/InternalException.h>
+#include <common/NonLinException.h>
 #include <logics/ArithLogic.h>
 
 namespace opensmt {
@@ -36,6 +37,7 @@ class DivModConfig : public DefaultRewriterConfig {
             PTRef modVar = divMod.mod;
             PTRef rewritten = logic.isIntDiv(symRef) ? divVar : modVar;
             if (not inCache) {
+                if (!logic.isConstant(divisor)) throw NonLinException(logic.pp(term));
                 // collect the definitions to add
                 assert(logic.isConstant(divisor));
                 auto divisorVal = logic.getNumConst(divisor);

src/simplifiers/LA.cc

@@ -57,14 +57,14 @@ void LAExpression::initialize(PTRef e, bool do_canonize) {
         } else if (logic.isTimes(t)) {
             // If it is times, then one side must be constant, other
             // is enqueued with a new constant
-            auto [var, constant] = logic.splitTermToVarAndConst(t);
+            auto [var, constant] = logic.splitPolyTerm(t);
             Real new_c = logic.getNumConst(constant);
             new_c *= c;
             curr_term.emplace_back(var);
             curr_const.emplace_back(std::move(new_c));
         } else {
-            // Otherwise it is a variable, Ite, UF or constant
-            assert(logic.isNumVarLike(t) || logic.isConstant(t) || logic.isUF(t));
+            // Otherwise it is a monomial or constant
+            assert(logic.isMonomial(t) || logic.isConstant(t));
             if (logic.isConstant(t)) {
                 const Real tval = logic.getNumConst(t);
                 polynome[PTRef_Undef] += tval * c;

src/symbols/SymStore.cc

@@ -39,11 +39,12 @@ SymStore::~SymStore() {
         free(idToName[i]);
 }
 
-SymRef SymStore::newSymb(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig) {
+SymRef SymStore::newSymb(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig,
+                         bool subSymb) {
     // Check if there already is a term called fname with same number of arguments of the same sort
     auto * symrefs = getRefOrNull(fname);
 
-    if (symrefs) {
+    if (symrefs && !subSymb) {
         vec<SymRef> const & trs = *symrefs;
         for (SymRef symref : trs) {
             auto const & symbol = ta[symref];
@@ -67,7 +68,7 @@ SymRef SymStore::newSymb(char const * fname, SRef rsort, vec<SRef> const & args,
         vec<SymRef> trs;
         trs.push(tr);
         symbolTable.insert(tmp_name, trs);
-    } else {
+    } else if (!subSymb) {
         symbolTable[tmp_name].push(tr); // Map the name to term reference (why not id?), used in parsing
     }
     return tr;

src/symbols/SymStore.h

@@ -40,9 +40,15 @@ class SymStore {
     SymStore(SymStore &&) = default;
     SymStore & operator=(SymStore &&) = default;
     // Constructs a new symbol.
-    SymRef newSymb(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig);
+
+    SymRef newSymb(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig) {
+        return newSymb(fname, rsort, args, symConfig, false);
+    };
     SymRef newSymb(char const * fname, SRef rsort, vec<SRef> const & args) {
-        return newSymb(fname, rsort, args, SymConf::Default);
+        return newSymb(fname, rsort, args, SymConf::Default, false);
+    }
+    SymRef newInternalSymb(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig) {
+        return newSymb(fname, rsort, args, symConfig, true);
     }
     bool contains(char const * fname) const { return symbolTable.has(fname); }
     vec<SymRef> const & nameToRef(char const * s) const { return symbolTable[s]; }
@@ -73,6 +79,9 @@ class SymStore {
     vec<SymRef> symbols;
     SymbolAllocator ta{1024};
     vec<char *> idToName;
+
+    SymRef newSymb(char const * fname, SRef rsort, vec<SRef> const & args, SymbolConfig const & symConfig,
+                   bool subSymb);
 };
 } // namespace opensmt
 

src/tsolvers/lasolver/LASolver.cc

@@ -11,6 +11,7 @@
 #include "CutCreator.h"
 
 #include <common/Random.h>
+#include <common/NonLinException.h>
 #include <models/ModelBuilder.h>
 #include <simplifiers/LA.h>
 
@@ -91,9 +92,7 @@ void LASolver::isProperLeq(PTRef tr)
     assert(logic.isLeq(tr));
     auto [cons, sum] = logic.leqToConstantAndTerm(tr);
     assert(logic.isConstant(cons));
-    assert(logic.isNumVar(sum) || logic.isPlus(sum) || logic.isTimes(sum));
-    assert(!logic.isTimes(sum) || ((logic.isNumVar(logic.getPterm(sum)[0]) && logic.isOne(logic.mkNeg(logic.getPterm(sum)[1]))) ||
-                                   (logic.isNumVar(logic.getPterm(sum)[1]) && logic.isOne(logic.mkNeg(logic.getPterm(sum)[0])))));
+    assert(logic.isNumVar(sum) || logic.isPlus(sum) || logic.isTimesLinOrNonlin(sum));
     (void) cons; (void)sum;
 }
 
@@ -244,7 +243,7 @@ LVRef LASolver::getVarForLeq(PTRef ref) const {
 }
 
 LVRef LASolver::getLAVar_single(PTRef expr_in) {
-
+    if (logic.isTimesNonlin(expr_in)) throw NonLinException(logic.pp(expr_in));
     assert(logic.isLinearTerm(expr_in));
     PTId id = logic.getPterm(expr_in).getId();
 
@@ -262,7 +261,7 @@ std::unique_ptr<Tableau::Polynomial> LASolver::expressionToLVarPoly(PTRef term)
     auto poly = std::make_unique<Tableau::Polynomial>();
     bool negated = laVarMapper.isNegated(term);
     for (int i = 0; i < logic.getPterm(term).size(); i++) {
-        auto [v,c] = logic.splitTermToVarAndConst(logic.getPterm(term)[i]);
+        auto [v,c] = logic.splitPolyTerm(logic.getPterm(term)[i]);
         LVRef var = getLAVar_single(v);
         Real coeff = getNum(c);
         if (negated) {
@@ -296,11 +295,11 @@ LVRef LASolver::registerArithmeticTerm(PTRef expr) {
         }
     }
 
-    if (logic.isNumVar(expr) || logic.isTimes(expr)) {
+    if (logic.isNumVar(expr) || logic.isTimesLin(expr)) {
         // Case (1), (2a), and (2b)
-        auto [v,c] = logic.splitTermToVarAndConst(expr);
-        assert(logic.isNumVar(v) || (laVarMapper.isNegated(v) && logic.isNumVar(logic.mkNeg(v))));
+        auto [v,c] = logic.splitPolyTerm(expr);
         x = getLAVar_single(v);
+        assert(logic.isNumVar(v) || (laVarMapper.isNegated(v) && logic.isNumVar(logic.mkNeg(v))));
         simplex.newNonbasicVar(x);
         notifyVar(x);
     }
@@ -847,7 +846,7 @@ std::pair<SparseLinearSystem,std::vector<PTRef>> linearSystemFromConstraints(std
         PTRef poly = defConstraint.lhs;
         fillTerms(poly, terms);
         for (PTRef arg : terms) {
-            auto [var, constant] = logic.splitTermToVarAndConst(arg);
+            auto [var, constant] = logic.splitPolyTerm(arg);
             assert(var != PTRef_Undef);
             if (varIndices.find(var) == varIndices.end()) {
                 varIndices.insert({var, columns++});
@@ -866,7 +865,7 @@ std::pair<SparseLinearSystem,std::vector<PTRef>> linearSystemFromConstraints(std
         PTRef poly = constraints[row].lhs;
         fillTerms(poly, terms);
         for (PTRef arg : terms) {
-            auto [var, constant] = logic.splitTermToVarAndConst(arg);
+            auto [var, constant] = logic.splitPolyTerm(arg);
             auto col = varIndices[var];
             columnPolynomials[col].addTerm(IndexType{row}, logic.getNumConst(constant));
         }

src/tsolvers/lasolver/LAVarMapper.cc

@@ -58,7 +58,7 @@ bool LAVarMapper::isNegated(PTRef tr) const {
         return false; // Case (1a)
     if (logic.isTimes(tr)) {
         // Cases (2)
-        auto [v,c] = logic.splitTermToVarAndConst(tr);
+        auto [v,c] = logic.splitPolyTerm(tr);
         return isNegated(c);
     }
     if (logic.isIte(tr)) {

test/regression/base/arithmetic/miniexample.smt2

@@ -0,0 +1,5 @@
+(set-logic QF_LIA)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (* a b))
+(assert (= (uninterp_mul 1 2) 2))
+(check-sat)
+(exit)

test/regression/base/arithmetic/miniexample.smt2.expected.out

@@ -0,0 +1 @@
+sat

test/regression/base/arithmetic/miniexample1.smt2

@@ -0,0 +1,5 @@
+(set-logic QF_LRA)
+(define-fun uninterp_div ((a Real) (b Real)) Real (* a b))
+(assert (= (uninterp_div 0.25 2) 0.5))
+(check-sat)
+(exit)

test/regression/base/arithmetic/miniexample1.smt2.expected.out

@@ -0,0 +1 @@
+sat

test/regression/base/arithmetic/miniexample10.smt2

@@ -0,0 +1,7 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (* 2 a b))
+(assert (= (uninterp_mul 5 x) 10))
+(check-sat)
+(get-model)
+(exit)

test/regression/base/arithmetic/miniexample10.smt2.expected.out

@@ -0,0 +1,5 @@
+sat
+(
+  (define-fun x () Int
+    1)
+)

test/regression/base/arithmetic/miniexample2.smt2

@@ -0,0 +1,7 @@
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(define-fun uninterp_mul ((a Int) (b Int)) Int (* a b))
+(assert (= (uninterp_mul 2 x) (+ x x)))
+(check-sat)
+(get-model)
+(exit)

test/regression/base/arithmetic/miniexample2.smt2.expected.out

@@ -0,0 +1,5 @@
+sat
+(
+  (define-fun x () Int
+    0)
+)