Sls

.gitignore

@@ -6,6 +6,7 @@ rebase.cmd
 callgrind.out.*
 # .hpp files are automatically generated
 *.hpp
+.env
 .z3-trace
 .env
 .genaiscript
@@ -28,6 +29,8 @@ ocamlz3
 # Emacs temp files
 \#*\#
 # Directories with generated code and documentation
+node_modules/*
+.genaiscript/*
 release/*
 build/*
 trace/*
@@ -105,3 +108,4 @@ CMakeSettings.json
 .DS_Store
 dbg/**
 *.wsp
+CppProperties.json

scripts/mk_project.py

@@ -28,19 +28,19 @@ def init_project_def():
     add_lib('parser_util', ['ast'], 'parsers/util')
     add_lib('euf', ['ast'], 'ast/euf')
     add_lib('grobner', ['ast', 'dd', 'simplex'], 'math/grobner')    
-    add_lib('sat', ['params', 'util', 'dd', 'grobner'])    
-    add_lib('nlsat', ['polynomial', 'sat'])
-    add_lib('lp', ['util', 'nlsat', 'grobner', 'interval', 'smt_params'], 'math/lp')
     add_lib('rewriter', ['ast', 'polynomial', 'interval', 'automata', 'params'], 'ast/rewriter')
-    add_lib('bit_blaster',  ['rewriter'], 'ast/rewriter/bit_blaster')
     add_lib('normal_forms', ['rewriter'], 'ast/normal_forms')
-    add_lib('substitution', ['rewriter'], 'ast/substitution')
-    add_lib('proofs', ['rewriter'], 'ast/proofs')
     add_lib('macros', ['rewriter'], 'ast/macros')
     add_lib('model',  ['macros'])
     add_lib('converters', ['model'], 'ast/converters')
+    add_lib('ast_sls', ['ast','normal_forms','converters','smt_params','euf'], 'ast/sls')
+    add_lib('sat', ['params', 'util', 'dd', 'ast_sls', 'grobner'])    
+    add_lib('nlsat', ['polynomial', 'sat'])
+    add_lib('lp', ['util', 'nlsat', 'grobner', 'interval', 'smt_params'], 'math/lp')
+    add_lib('bit_blaster',  ['rewriter'], 'ast/rewriter/bit_blaster')
+    add_lib('substitution', ['rewriter'], 'ast/substitution')
+    add_lib('proofs', ['rewriter'], 'ast/proofs')
     add_lib('simplifiers', ['euf', 'normal_forms', 'bit_blaster', 'converters', 'substitution'], 'ast/simplifiers')
-    add_lib('ast_sls', ['ast','normal_forms','converters'], 'ast/sls')
     add_lib('tactic', ['simplifiers'])
     add_lib('mbp', ['model', 'simplex'], 'qe/mbp')
     add_lib('qe_lite', ['tactic', 'mbp'], 'qe/lite')

src/CMakeLists.txt

@@ -54,7 +54,6 @@ add_subdirectory(ast/euf)
 add_subdirectory(ast/converters)
 add_subdirectory(ast/substitution)
 add_subdirectory(ast/simplifiers)
-add_subdirectory(ast/sls)
 add_subdirectory(tactic)
 add_subdirectory(qe/mbp)
 add_subdirectory(qe/lite)
@@ -74,6 +73,7 @@ add_subdirectory(parsers/smt2)
 add_subdirectory(solver/assertions)
 add_subdirectory(ast/pattern)
 add_subdirectory(math/lp)
+add_subdirectory(ast/sls)
 add_subdirectory(sat/smt)
 add_subdirectory(sat/tactic)
 add_subdirectory(nlsat/tactic)

src/ast/arith_decl_plugin.h

@@ -365,6 +365,7 @@ class arith_recognizers {
     MATCH_BINARY(is_div0);
     MATCH_BINARY(is_idiv0);
     MATCH_BINARY(is_power);
+    MATCH_BINARY(is_power0);
 
     MATCH_UNARY(is_sin);
     MATCH_UNARY(is_asin);

src/ast/ast.cpp

@@ -1714,7 +1714,7 @@ ast * ast_manager::register_node_core(ast * n) {
 
     n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();        
 
-//    track_id(*this, n, 77);
+  //  track_id(*this, n, 9213);
 
 //    TRACE("ast", tout << (s_count++) << " Object " << n->m_id << " was created.\n";);
     TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);

src/ast/bv_decl_plugin.cpp

@@ -932,13 +932,13 @@ unsigned bv_util::get_int2bv_size(parameter const& p) {
     return static_cast<unsigned>(sz);
 }
 
-app * bv_util::mk_bv2int(expr* e) {
+app * bv_util::mk_bv2int(expr* e) const {
     sort* s = m_manager.mk_sort(m_manager.mk_family_id("arith"), INT_SORT);
     parameter p(s);
     return m_manager.mk_app(get_fid(), OP_BV2INT, 1, &p, 1, &e);
 }
 
-app* bv_util::mk_int2bv(unsigned sz, expr* e) {
+app* bv_util::mk_int2bv(unsigned sz, expr* e) const {
     parameter p(sz);
     return m_manager.mk_app(get_fid(), OP_INT2BV, 1, &p, 1, &e);
 }

src/ast/bv_decl_plugin.h

@@ -549,8 +549,8 @@ class bv_util : public bv_recognizers {
     app * mk_bv_ashr(expr* arg1, expr* arg2) { return m_manager.mk_app(get_fid(), OP_BASHR, arg1, arg2); }
     app * mk_bv_lshr(expr* arg1, expr* arg2) { return m_manager.mk_app(get_fid(), OP_BLSHR, arg1, arg2); }
 
-    app * mk_bv2int(expr* e);
-    app * mk_int2bv(unsigned sz, expr* e);
+    app * mk_bv2int(expr* e) const;
+    app * mk_int2bv(unsigned sz, expr* e) const;
 
     app* mk_bv_rotate_left(expr* arg1, expr* arg2) { return m_manager.mk_app(get_fid(), OP_EXT_ROTATE_LEFT, arg1, arg2); }
     app* mk_bv_rotate_right(expr* arg1, expr* arg2) { return m_manager.mk_app(get_fid(), OP_EXT_ROTATE_RIGHT, arg1, arg2); }

src/ast/datatype_decl_plugin.h

@@ -341,8 +341,10 @@ namespace datatype {
         ast_manager & get_manager() const { return m; }
         // sort * mk_datatype_sort(symbol const& name, unsigned n, sort* const* params); 
         bool is_datatype(sort const* s) const { return is_sort_of(s, fid(), DATATYPE_SORT); }
+        bool is_datatype(expr* e) const { return is_datatype(e->get_sort()); }
         bool is_enum_sort(sort* s);
         bool is_recursive(sort * ty);
+        bool is_recursive(expr* e) { return is_recursive(e->get_sort()); }
         bool is_recursive_nested(sort * ty);
         bool is_constructor(func_decl * f) const { return is_decl_of(f, fid(), OP_DT_CONSTRUCTOR); }
         bool is_recognizer(func_decl * f) const { return is_recognizer0(f) || is_is(f); }

src/ast/euf/euf_egraph.cpp

@@ -82,8 +82,11 @@ namespace euf {
 
     void egraph::reinsert_equality(enode* p) {
         SASSERT(p->is_equality());        
-        if (p->value() != l_true && p->get_arg(0)->get_root() == p->get_arg(1)->get_root()) 
+        if (p->value() != l_true && p->get_arg(0)->get_root() == p->get_arg(1)->get_root()) {
             queue_literal(p, nullptr);
+            if (p->value() == l_false && !m_on_propagate_literal) 
+                set_conflict(p->get_arg(0), p->get_arg(1), p->m_lit_justification);
+        }
     }
 
     void egraph::queue_literal(enode* p, enode* ante) {        
@@ -201,6 +204,18 @@ namespace euf {
         }
     }
 
+    void egraph::new_diseq(enode* n, void* reason) {
+        force_push();
+        SASSERT(m.is_eq(n->get_expr()));
+        auto j = justification::external(reason);
+        auto a = n->get_arg(0), b = n->get_arg(1);
+        auto r1 = a->get_root(), r2 = b->get_root();
+        if (r1 == r2)
+            set_conflict(a, b, j);
+        else 
+            set_value(n, l_false, j);                
+    }
+
     void egraph::new_diseq(enode* n) {
         SASSERT(n->is_equality());
         SASSERT(n->value() == l_false);

src/ast/euf/euf_egraph.h

@@ -278,10 +278,11 @@ namespace euf {
          */
         void merge(enode* n1, enode* n2, void* reason) { merge(n1, n2, justification::external(reason)); }        
         void new_diseq(enode* n);
+        void new_diseq(enode* n, void* reason);
 
 
         /**
-           \brief propagate set of merges. 
+           \brief propagate set of merges.           
            This call may detect an inconsistency. Then inconsistent() is true.
            Use then explain() to extract an explanation for the conflict.
 

src/ast/rewriter/CMakeLists.txt

@@ -4,6 +4,7 @@ z3_add_component(rewriter
     array_rewriter.cpp
     ast_counter.cpp
     bit2int.cpp
+    bv2int_translator.cpp
     bool_rewriter.cpp
     bv_bounds.cpp
     bv_elim.cpp

src/ast/rewriter/arith_rewriter.cpp

@@ -515,6 +515,129 @@ br_status arith_rewriter::reduce_power(expr * arg1, expr * arg2, op_kind kind, e
     }
 }
 
+bool arith_rewriter::is_mul_factor(expr* s, expr* t) {
+    if (m_util.is_mul(t))
+        return any_of(*to_app(t), [&](expr* m) { return is_mul_factor(s, m); });
+    return s == t;
+}
+
+bool arith_rewriter::is_add_factor(expr* s, expr* t) {
+    if (m_util.is_add(t))
+        return all_of(*to_app(t), [&](expr* f) { return is_add_factor(s, f); });
+    return is_mul_factor(s, t);
+}
+
+expr_ref arith_rewriter::remove_factor(expr* s, expr* t) {
+
+    if (m_util.is_mul(t)) {
+        ptr_buffer<expr> r;
+        r.push_back(t);
+        for (unsigned i = 0; i < r.size(); ++i) {
+            expr* arg = r[i];
+            if (m_util.is_mul(arg)) {
+                r.append(to_app(arg)->get_num_args(), to_app(arg)->get_args());
+                r[i] = r.back();
+                r.pop_back();
+                --i;
+                continue;
+            }
+            if (s == arg) {
+                r[i] = r.back();
+                r.pop_back();
+                break;
+            }
+        }
+        switch (r.size()) {
+        case 0:
+            return expr_ref(m_util.mk_numeral(rational(1), m_util.is_int(t)), m);
+        case 1:
+            return expr_ref(r[0], m);
+        default:
+            return expr_ref(m_util.mk_mul(r.size(), r.data()), m);
+        }
+    }
+    if (m_util.is_add(t)) {
+        expr_ref_vector sum(m);
+        sum.push_back(t);
+        for (unsigned i = 0; i < sum.size(); ++i) {
+            expr* arg = sum.get(i);
+            if (m_util.is_add(arg)) {
+                sum.append(to_app(arg)->get_num_args(), to_app(arg)->get_args());
+                sum[i] = sum.back();
+                sum.pop_back();
+                --i;
+                continue;
+            }
+            sum[i] = remove_factor(s, arg);
+        }
+        if (sum.size() == 1)
+            return expr_ref(sum.get(0), m);
+        else
+            return expr_ref(m_util.mk_add(sum.size(), sum.data()), m);
+    }
+    else {
+        SASSERT(s == t);
+        return expr_ref(m_util.mk_numeral(rational(1), m_util.is_int(t)), m);
+    }
+}
+
+
+void arith_rewriter::get_nl_muls(expr* t, ptr_buffer<expr>& muls) {
+    if (m_util.is_mul(t)) {
+        for (expr* arg : *to_app(t))
+            get_nl_muls(arg, muls);
+    }
+    else if (!m_util.is_numeral(t))
+        muls.push_back(t);    
+}
+
+expr* arith_rewriter::find_nl_factor(expr* t) {
+    ptr_buffer<expr> sum, muls;
+    sum.push_back(t);
+
+    for (unsigned i = 0; i < sum.size(); ++i) {
+        expr* arg = sum[i];
+        if (m_util.is_add(arg)) 
+            sum.append(to_app(arg)->get_num_args(), to_app(arg)->get_args());        
+        else if (m_util.is_mul(arg)) {
+            muls.reset();
+            get_nl_muls(arg, muls);
+            if (muls.size() <= 1)
+                continue;
+            for (auto m : muls) {
+                if (is_add_factor(m, t))
+                    return m;
+            }
+            return nullptr;
+        }
+    }
+    return nullptr;
+}
+
+br_status arith_rewriter::factor_le_ge_eq(expr * arg1, expr * arg2, op_kind kind, expr_ref & result) {
+
+    if (is_zero(arg2)) {
+        expr* f = find_nl_factor(arg1);
+        if (!f)
+            return BR_FAILED;
+        expr_ref f2 = remove_factor(f, arg1);
+        expr* z = m_util.mk_numeral(rational(0), m_util.is_int(arg1));
+        result = m.mk_or(m_util.mk_eq(f, z), m_util.mk_eq(f2, z));
+        switch (kind) {
+        case EQ: 
+            break;
+        case GE:
+            result = m.mk_or(m.mk_iff(m_util.mk_ge(f, z), m_util.mk_ge(f2, z)), result);
+            break;
+        case LE:
+            result = m.mk_or(m.mk_not(m.mk_iff(m_util.mk_ge(f, z), m_util.mk_ge(f2, z))), result);
+            break;            
+        }
+        return BR_REWRITE3;                    
+    }
+    return BR_FAILED;
+}
+
 br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kind, expr_ref & result) {
     expr *orig_arg1 = arg1, *orig_arg2 = arg2;
     expr_ref new_arg1(m);
@@ -655,7 +778,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
         default: result = m.mk_eq(arg1, arg2); return BR_DONE;
         }
     }
-    return BR_FAILED;
+    return factor_le_ge_eq(arg1, arg2, kind, result);
 }
 
 

src/ast/rewriter/arith_rewriter.h

@@ -73,6 +73,12 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
     br_status is_separated(expr * arg1, expr * arg2, op_kind kind, expr_ref & result);
     bool is_non_negative(expr* e);
     br_status mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kind, expr_ref & result);
+    bool is_add_factor(expr* s, expr* t);
+    bool is_mul_factor(expr* s, expr* t);
+    expr* find_nl_factor(expr* t);
+    void get_nl_muls(expr* t, ptr_buffer<expr>& muls);
+    expr_ref remove_factor(expr* s, expr* t);
+    br_status factor_le_ge_eq(expr * arg1, expr * arg2, op_kind kind, expr_ref & result);
 
     bool elim_to_real_var(expr * var, expr_ref & new_var);
     bool elim_to_real_mon(expr * monomial, expr_ref & new_monomial);