Nlsat simplify

README.md

@@ -226,7 +226,7 @@ to Z3's C API. For more information, see [MachineArithmetic/README.md](https://g
 * Default input format is [SMTLIB2](http://smtlib.cs.uiowa.edu)
 
 * Other native foreign function interfaces:
-* [C++ API](https://z3prover.github.io/api/html/group__cppapi.html)
+* [C++ API](https://z3prover.github.io/api/html/namespacez3.html)
 * [.NET API](https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html)
 * [Java API](https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html)
 * [Python API](https://z3prover.github.io/api/html/namespacez3py.html) (also available in [pydoc format](https://z3prover.github.io/api/html/z3.html))

src/api/api_arith.cpp

@@ -123,6 +123,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+    MK_UNARY(Z3_mk_abs, mk_c(c)->get_arith_fid(), OP_ABS, SKIP);
     MK_UNARY(Z3_mk_int2real, mk_c(c)->get_arith_fid(), OP_TO_REAL, SKIP);
     MK_UNARY(Z3_mk_real2int, mk_c(c)->get_arith_fid(), OP_TO_INT, SKIP);
     MK_UNARY(Z3_mk_is_int,   mk_c(c)->get_arith_fid(), OP_IS_INT, SKIP);

src/api/api_ast.cpp

@@ -1152,6 +1152,7 @@ extern "C" {
             case OP_REM: return Z3_OP_REM;
             case OP_MOD: return Z3_OP_MOD;
             case OP_POWER: return Z3_OP_POWER;
+            case OP_ABS: return Z3_OP_ABS;
             case OP_TO_REAL: return Z3_OP_TO_REAL;
             case OP_TO_INT: return Z3_OP_TO_INT;
             case OP_IS_INT: return Z3_OP_IS_INT;
@@ -1310,6 +1311,10 @@ extern "C" {
             case OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX;
             case OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE;
             case OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE;
+            case OP_SEQ_MAP: return Z3_OP_SEQ_MAP;
+            case OP_SEQ_MAPI: return Z3_OP_SEQ_MAPI;
+            case OP_SEQ_FOLDL: return Z3_OP_SEQ_FOLDL;
+            case OP_SEQ_FOLDLI: return Z3_OP_SEQ_FOLDLI;
 
             case _OP_STRING_STRREPL: return Z3_OP_SEQ_REPLACE;
             case _OP_STRING_CONCAT: return Z3_OP_SEQ_CONCAT;

src/api/api_seq.cpp

@@ -348,5 +348,10 @@ extern "C" {
     MK_UNARY(Z3_mk_char_from_bv, mk_c(c)->get_char_fid(), OP_CHAR_FROM_BV, SKIP);
     MK_UNARY(Z3_mk_char_is_digit, mk_c(c)->get_char_fid(), OP_CHAR_IS_DIGIT, SKIP);
 
+    MK_BINARY(Z3_mk_seq_map, mk_c(c)->get_seq_fid(), OP_SEQ_MAP, SKIP); 
+    MK_TERNARY(Z3_mk_seq_mapi, mk_c(c)->get_seq_fid(), OP_SEQ_MAPI, SKIP);
+    MK_TERNARY(Z3_mk_seq_foldl, mk_c(c)->get_seq_fid(), OP_SEQ_FOLDL, SKIP);
+    MK_FOURARY(Z3_mk_seq_foldli, mk_c(c)->get_seq_fid(), OP_SEQ_FOLDLI, SKIP);
+
 
 };

src/api/api_util.h

@@ -147,6 +147,9 @@ Z3_ast Z3_API NAME(Z3_context c, Z3_ast n1, Z3_ast n2) {        \
     Z3_TRY;                                                     \
     RESET_ERROR_CODE();                                         \
     EXTRA_CODE;                                                 \
+    CHECK_IS_EXPR(n1, nullptr);                                 \
+    CHECK_IS_EXPR(n2, nullptr);                                 \
+    CHECK_IS_EXPR(n3, nullptr);                                 \
     expr * args[3] = { to_expr(n1), to_expr(n2), to_expr(n3) }; \
     ast* a = mk_c(c)->m().mk_app(FID, OP, 0, 0, 3, args);       \
     mk_c(c)->save_ast_trail(a);                                 \
@@ -160,6 +163,27 @@ Z3_ast Z3_API NAME(Z3_context c, Z3_ast n1, Z3_ast n2) {        \
     MK_TERNARY_BODY(NAME, FID, OP, EXTRA_CODE);                          \
 }
 
+#define MK_FOURARY_BODY(NAME, FID, OP, EXTRA_CODE)               \
+    Z3_TRY;                                                     \
+    RESET_ERROR_CODE();                                         \
+    EXTRA_CODE;                                                 \
+    CHECK_IS_EXPR(n1, nullptr);                                 \
+    CHECK_IS_EXPR(n2, nullptr);                                 \
+    CHECK_IS_EXPR(n3, nullptr);                                 \
+    CHECK_IS_EXPR(n4, nullptr);                                 \
+    expr * args[4] = { to_expr(n1), to_expr(n2), to_expr(n3), to_expr(n4) }; \
+    ast* a = mk_c(c)->m().mk_app(FID, OP, 0, 0, 4, args);       \
+    mk_c(c)->save_ast_trail(a);                                 \
+    check_sorts(c, a);                                          \
+    RETURN_Z3(of_ast(a));                                       \
+    Z3_CATCH_RETURN(0);
+
+#define MK_FOURARY(NAME, FID, OP, EXTRA_CODE)                            \
+    Z3_ast Z3_API NAME(Z3_context c, Z3_ast n1, Z3_ast n2, Z3_ast n3, Z3_ast n4) { \
+    LOG_ ## NAME(c, n1, n2, n3, n4);                                        \
+    MK_FOURARY_BODY(NAME, FID, OP, EXTRA_CODE);                          \
+}
+
 #define MK_NARY(NAME, FID, OP, EXTRA_CODE)                              \
 Z3_ast Z3_API NAME(Z3_context c, unsigned num_args, Z3_ast const* args) { \
     Z3_TRY;                                                             \

src/api/c++/z3++.h

@@ -2497,6 +2497,34 @@ namespace z3 {
         return expr(ctx, r);
     }
 
+    inline expr map(expr const& f, expr const& list) {
+        context& ctx = f.ctx();
+        Z3_ast r = Z3_mk_seq_map(ctx, f, list);
+        ctx.check_error();
+        return expr(ctx, r);
+    }
+
+    inline expr mapi(expr const& f, expr const& i, expr const& list) {
+        context& ctx = f.ctx();
+        Z3_ast r = Z3_mk_seq_mapi(ctx, f, i, list);
+        ctx.check_error();
+        return expr(ctx, r);
+    }
+
+    inline expr foldl(expr const& f, expr const& a, expr const& list) {
+        context& ctx = f.ctx();
+        Z3_ast r = Z3_mk_seq_foldl(ctx, f, a, list);
+        ctx.check_error();
+        return expr(ctx, r);
+    }
+
+    inline expr foldli(expr const& f, expr const& i, expr const& a, expr const& list) {
+        context& ctx = f.ctx();
+        Z3_ast r = Z3_mk_seq_foldli(ctx, f, i, a, list);
+        ctx.check_error();
+        return expr(ctx, r);
+    }
+
     inline expr mk_or(expr_vector const& args) {
         array<Z3_ast> _args(args);
         Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());

src/api/python/z3/z3.py

@@ -11210,6 +11210,32 @@ def Length(s):
     s = _coerce_seq(s)
     return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx)
 
+def SeqMap(f, s):
+    """Map function 'f' over sequence 's'"""
+    ctx = _get_ctx2(f, s)
+    s = _coerce_seq(s, ctx)
+    return _to_expr_ref(Z3_mk_seq_map(s.ctx_ref(), f.as_ast(), s.as_ast()), ctx)
+
+def SeqMapI(f, i, s):
+    """Map function 'f' over sequence 's' at index 'i'"""
+    ctx = _get_ctx(f, s)
+    s = _coerce_seq(s, ctx)
+    if not is_expr(i):
+        i = _py2expr(i)
+    return _to_expr_ref(Z3_mk_seq_mapi(s.ctx_ref(), f.as_ast(), i.as_ast(), s.as_ast()), ctx)
+
+def SeqFoldLeft(f, a, s):
+    ctx = _get_ctx2(f, s)
+    s = _coerce_seq(s, ctx)
+    a = _py2expr(a)
+    return _to_expr_ref(Z3_mk_seq_foldl(s.ctx_ref(), f.as_ast(), a.as_ast(), s.as_ast()), ctx)
+
+def SeqFoldLeftI(f, i, a, s):
+    ctx = _get_ctx2(f, s)
+    s = _coerce_seq(s, ctx)
+    a = _py2expr(a)
+    i = _py2epxr(i)
+    return _to_expr_ref(Z3_mk_seq_foldli(s.ctx_ref(), f.as_ast(), i.as_ast(), a.as_ast(), s.as_ast()), ctx)
 
 def StrToInt(s):
     """Convert string expression to integer

src/api/z3_api.h

@@ -1023,6 +1023,7 @@ typedef enum {
     Z3_OP_TO_INT,
     Z3_OP_IS_INT,
     Z3_OP_POWER,
+    Z3_OP_ABS,
 
     // Arrays & Sets
     Z3_OP_STORE = 0x300,
@@ -1193,6 +1194,10 @@ typedef enum {
     Z3_OP_SEQ_LAST_INDEX,
     Z3_OP_SEQ_TO_RE,
     Z3_OP_SEQ_IN_RE,
+    Z3_OP_SEQ_MAP,            
+    Z3_OP_SEQ_MAPI,           
+    Z3_OP_SEQ_FOLDL,          
+    Z3_OP_SEQ_FOLDLI,         
 
     // strings
     Z3_OP_STR_TO_INT,
@@ -2544,6 +2549,13 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2);
 
+    /**
+       \brief Take the absolute value of an integer
+
+       def_API('Z3_mk_abs', AST, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_abs(Z3_context c, Z3_ast arg);
+
     /**
         \brief Create less than.
 
@@ -3798,6 +3810,30 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast s, Z3_ast substr);
 
+    /**
+      \brief Create a map of the function \c f over the sequence \c s.
+      def_API('Z3_mk_seq_map', AST ,(_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_seq_map(Z3_context c, Z3_ast f, Z3_ast s);
+
+    /**
+     \brief Create a map of the function \c f over the sequence \c s starting at index \c i.
+     def_API('Z3_mk_seq_mapi', AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_seq_mapi(Z3_context c, Z3_ast f, Z3_ast i, Z3_ast s);
+
+    /**
+      \brief Create a fold of the function \c f over the sequence \c s with accumulator a.
+      def_API('Z3_mk_seq_foldl', AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_seq_foldl(Z3_context c, Z3_ast f, Z3_ast a, Z3_ast s);
+
+    /**
+       \brief Create a fold with index tracking of the function \c f over the sequence \c s with accumulator \c a starting at index \c i.
+       def_API('Z3_mk_seq_foldli', AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_seq_foldli(Z3_context c, Z3_ast f, Z3_ast i, Z3_ast a, Z3_ast s);
+
     /**
        \brief Convert string to integer.
 

src/math/lp/lp_settings.h

@@ -128,8 +128,12 @@ struct statistics {
     unsigned m_grobner_conflicts;
     unsigned m_offset_eqs;
     unsigned m_fixed_eqs;
+    ::statistics m_st;
     statistics() { reset(); }
-    void reset() { memset(this, 0, sizeof(*this)); }
+    void reset() {
+        memset(this, 0, sizeof(*this));
+        m_st.reset();
+    }
     void collect_statistics(::statistics& st) const {
         st.update("arith-factorizations", m_num_factorizations);
         st.update("arith-make-feasible", m_make_feasible);
@@ -157,7 +161,7 @@ struct statistics {
         st.update("arith-nla-lemmas", m_nla_lemmas);
         st.update("arith-nra-calls", m_nra_calls);   
         st.update("arith-bounds-improvements", m_nla_bounds_improvements);
-
+        st.copy(m_st);
     }
 };
 

src/math/lp/nra_solver.cpp

@@ -34,7 +34,7 @@ struct solver::imp {
     scoped_ptr<scoped_anum_vector>   m_values; // values provided by LRA solver
     scoped_ptr<scoped_anum> m_tmp1, m_tmp2;
     nla::core&                m_nla_core;
-
+    
     imp(lp::lar_solver& s, reslimit& lim, params_ref const& p, nla::core& nla_core): 
         lra(s), 
         m_limit(lim),
@@ -180,6 +180,7 @@ struct solver::imp {
         }
 
         lbool r = l_undef;
+        statistics& st = m_nla_core.lp_settings().stats().m_st;
         try {
             r = m_nlsat->check();
         }
@@ -188,9 +189,11 @@ struct solver::imp {
                 r = l_undef;
             }
             else {
+                m_nlsat->collect_statistics(st);
                 throw;
             }
         }
+        m_nlsat->collect_statistics(st);
         TRACE("nra",
               m_nlsat->display(tout << r << "\n");
               display(tout);
@@ -234,6 +237,7 @@ struct solver::imp {
         return r;
     }   
 
+
     void add_monic_eq_bound(mon_eq const& m) {
         if (!lra.column_has_lower_bound(m.var()) && 
             !lra.column_has_upper_bound(m.var()))
@@ -374,6 +378,7 @@ struct solver::imp {
         }
 
         lbool r = l_undef;
+        statistics& st = m_nla_core.lp_settings().stats().m_st;
         try {
             r = m_nlsat->check();
         }
@@ -382,9 +387,11 @@ struct solver::imp {
                 r = l_undef;
             }
             else {
+                m_nlsat->collect_statistics(st);
                 throw;
             }
         }
+        m_nlsat->collect_statistics(st);
 
         switch (r) {
         case l_true:
@@ -665,7 +672,7 @@ nlsat::anum_manager& solver::am() {
 scoped_anum& solver::tmp1() { return m_imp->tmp1(); }
 
 scoped_anum& solver::tmp2() { return m_imp->tmp2(); }
-
+ 
 
 void solver::updt_params(params_ref& p) {
     m_imp->updt_params(p);

src/math/polynomial/algebraic_numbers.cpp

@@ -2594,27 +2594,28 @@ namespace algebraic_numbers {
 
         void int_lt(numeral const & a, numeral & b) {
             scoped_mpz v(qm());
+            if (!a.is_basic())
+                refine_until_prec(const_cast<numeral&>(a), 1);
             if (a.is_basic()) {
                 qm().floor(basic_value(a), v);
                 qm().dec(v);
             }
-            else {
-                refine_until_prec(const_cast<numeral&>(a), 1);
-                bqm().floor(qm(), lower(a.to_algebraic()), v);
-            }
+            else                 
+                bqm().floor(qm(), lower(a.to_algebraic()), v);            
             m_wrapper.set(b, v);
         }
 
         void int_gt(numeral const & a, numeral & b) {
             scoped_mpz v(qm());
+            if (!a.is_basic()) 
+                refine_until_prec(const_cast<numeral&>(a), 1);
             if (a.is_basic()) {
                 qm().ceil(basic_value(a), v);
                 qm().inc(v);
             }
-            else {
-                refine_until_prec(const_cast<numeral&>(a), 1);
+            else                
                 bqm().ceil(qm(), upper(a.to_algebraic()), v);
-            }
+
             m_wrapper.set(b, v);
         }