NonlinWork: Nonlin Real division is no longer supported

Author: BritikovKI

src/api/MainSolver.cc

@@ -337,7 +337,7 @@ sstat MainSolver::check() {
     sstat rval;
     try {
         rval = simplifyFormulas();
-    } catch (opensmt::NonLinException const & error) {
+    } catch (NonLinException const & error) {
         reasonUnknown = error.what();
         return s_Undef;
     }
@@ -347,7 +347,7 @@ sstat MainSolver::check() {
     if (rval == s_Undef) {
         try {
             rval = solve();
-        } catch (std::overflow_error const & error) { rval = s_Error; } catch (opensmt::NonLinException const & error) {
+        } catch (std::overflow_error const & error) { rval = s_Error; } catch (NonLinException const & error) {
             reasonUnknown = error.what();
             return s_Undef;
         }

src/logics/ArithLogic.cc

@@ -2,6 +2,7 @@
 
 #include <common/ApiException.h>
 #include <common/InternalException.h>
+#include <common/NonLinException.h>
 #include <common/StringConv.h>
 #include <common/TreeOps.h>
 #include <pterms/PtStore.h>
@@ -680,8 +681,7 @@ PTRef ArithLogic::mkTimes(vec<PTRef> && args) {
     if (!isTimes(s_new)) return mkFun(s_new, std::move(args));
     PTRef coef = PTRef_Undef;
     std::vector<PTRef> vars;
-    //    return mkFun(s_new, std::move(args));
-    // Splitting Multiplication into constant and variable subterms
+    // Splitting Multiplication into constant and monomial subterms
     for (int i = 0; i < args.size(); i++) {
         if (isConstant(args[i])) {
             assert(coef == PTRef_Undef);
@@ -863,7 +863,9 @@ PTRef ArithLogic::mkRealDiv(vec<PTRef> && args) {
     vec<PTRef> args_new;
     SymRef s_new;
     simp.simplify(get_sym_Real_DIV(), args, s_new, args_new);
-    if (isRealDiv(s_new) && (isNumTerm(args_new[0]) || isPlus(args_new[0])) && isConstant(args_new[1])) {
+    // TODO: Currently creation of nonlinear Real divison is not supported
+    if (isRealDiv(s_new) && (isNumTerm(args_new[0]) || isPlus(args_new[0]))) {
+        if (!isConstant(args_new[1])) throw NonLinException(pp(args[0]) + "/" + pp(args[1]));
         args_new[1] = mkRealConst(getNumConst(args_new[1]).inverse()); // mkConst(1/getRealConst(args_new[1]));
         return mkTimes(args_new);
     }

src/tsolvers/lasolver/LASolver.cc

@@ -92,7 +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.isTimesLinOrNonlin(sum) || logic.isRealDiv(sum));
+    assert(logic.isNumVar(sum) || logic.isPlus(sum) || logic.isTimesLinOrNonlin(sum));
     (void) cons; (void)sum;
 }
 
@@ -243,7 +243,7 @@ LVRef LASolver::getVarForLeq(PTRef ref) const {
 }
 
 LVRef LASolver::getLAVar_single(PTRef expr_in) {
-    if (logic.isTimesNonlin(expr_in) || logic.isRealDiv(expr_in)) throw NonLinException(logic.pp(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();
 

test/regression/base/arithmetic/miniexample1.smt2

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