new files

src/sat/smt/arith_value.cpp

@@ -0,0 +1,145 @@
+/*++
+Copyright (c) 2018 Microsoft Corporation
+
+Module Name:
+
+    smt_arith_value.cpp
+
+Abstract:
+
+    Utility to extract arithmetic values from context.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2018-12-08.
+
+Revision History:
+
+--*/
+
+#include "ast/ast_pp.h"
+#include "sat/smt/arith_value.h"
+#include "sat/smt/euf_solver.h"
+#include "sat/smt/arith_solver.h"
+
+namespace arith {
+
+    arith_value::arith_value(euf::solver& s) :
+        s(s), m(s.get_manager()), a(m) {}
+
+    void arith_value::init() {
+        if (!as)
+            as = dynamic_cast<arith::solver*>(s.fid2solver(a.get_family_id()));
+    }
+
+    bool arith_value::get_value(expr* e, rational& val) {
+        auto n = s.get_enode(e);
+        expr_ref _val(m);
+        init();
+        return n && as->get_value(n, _val) && a.is_numeral(_val, val);
+    }
+
+#if 0
+    bool arith_value::get_lo_equiv(expr* e, rational& lo, bool& is_strict) {
+        if (!s.get_enode(e))
+            return false;
+        init();
+        is_strict = false;
+        bool found = false;
+        bool is_strict1;
+        rational lo1;
+        for (auto sib : euf::enode_class(s.get_enode(e))) {
+            if (!as->get_lower(sib, lo1, is_strict1))
+                continue;
+            if (!found || lo1 > lo || lo == lo1 && is_strict1)
+                lo = lo1, is_strict = is_strict1;
+            found = true;
+        }
+        CTRACE("arith_value", !found, tout << "value not found for " << mk_pp(e, m) << "\n";);
+        return found;
+    }
+
+    bool arith_value::get_up_equiv(expr* e, rational& hi, bool& is_strict) {
+        if (!s.get_enode(e))
+            return false;
+        init();
+        is_strict = false;
+        bool found = false;
+        bool is_strict1;
+        rational hi1;
+        for (auto sib : euf::enode_class(s.get_enode(e))) {
+            if (!as->get_upper(sib, hi1, is_strict1))
+                continue;
+            if (!found || hi1 < hi || hi == hi1 && is_strict1)
+                hi = hi1, is_strict = is_strict1;
+            found = true;
+        }
+        CTRACE("arith_value", !found, tout << "value not found for " << mk_pp(e, m) << "\n";);
+        return found;
+    }
+
+    bool arith_value::get_up(expr* e, rational& up, bool& is_strict) const {
+        init();
+        enode* n = s.get_enode(e);
+        is_strict = false;
+        return n && as->get_upper(n, up, is_strict);
+    }
+
+    bool arith_value::get_lo(expr* e, rational& lo, bool& is_strict) const {
+        init();
+        enode* n = s.get_enode(e);
+        is_strict = false;
+        return n && as->get_lower(n, lo, is_strict);
+    }
+
+#endif
+
+
+#if 0
+
+
+    bool arith_value::get_value_equiv(expr* e, rational& val) const {
+        if (!m_ctx->e_internalized(e)) return false;
+        expr_ref _val(m);
+        enode* next = m_ctx->get_enode(e), * n = next;
+        do {
+            e = next->get_expr();
+            if (m_tha && m_tha->get_value(next, _val) && a.is_numeral(_val, val)) return true;
+            if (m_thi && m_thi->get_value(next, _val) && a.is_numeral(_val, val)) return true;
+            if (m_thr && m_thr->get_value(next, val)) return true;
+            next = next->get_next();
+        } while (next != n);
+        TRACE("arith_value", tout << "value not found for " << mk_pp(e, m_ctx->get_manager()) << "\n";);
+        return false;
+    }
+
+    expr_ref arith_value::get_lo(expr* e) const {
+        rational lo;
+        bool s = false;
+        if ((a.is_int_real(e) || b.is_bv(e)) && get_lo(e, lo, s) && !s) {
+            return expr_ref(a.mk_numeral(lo, e->get_sort()), m);
+        }
+        return expr_ref(e, m);
+    }
+
+    expr_ref arith_value::get_up(expr* e) const {
+        rational up;
+        bool s = false;
+        if ((a.is_int_real(e) || b.is_bv(e)) && get_up(e, up, s) && !s) {
+            return expr_ref(a.mk_numeral(up, e->get_sort()), m);
+        }
+        return expr_ref(e, m);
+    }
+
+    expr_ref arith_value::get_fixed(expr* e) const {
+        rational lo, up;
+        bool s = false;
+        if (a.is_int_real(e) && get_lo(e, lo, s) && !s && get_up(e, up, s) && !s && lo == up) {
+            return expr_ref(a.mk_numeral(lo, e->get_sort()), m);
+        }
+        return expr_ref(e, m);
+    }
+
+#endif
+
+};

src/sat/smt/arith_value.h

@@ -0,0 +1,52 @@
+
+/*++
+Copyright (c) 2018 Microsoft Corporation
+
+Module Name:
+
+    arith_value.h
+
+Abstract:
+
+    Utility to extract arithmetic values from context.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2018-12-08.
+
+Revision History:
+
+--*/
+#pragma once
+
+#include "ast/arith_decl_plugin.h"
+
+namespace euf {
+    class solver;
+}
+namespace arith {
+
+    class solver;
+
+    class arith_value {
+        euf::solver& s;
+        ast_manager& m;
+        arith_util a;
+        solver* as = nullptr;
+        void init();
+    public:
+        arith_value(euf::solver& s);
+        bool get_value(expr* e, rational& value);
+
+#if 0
+        bool get_lo_equiv(expr* e, rational& lo, bool& strict);
+        bool get_up_equiv(expr* e, rational& up, bool& strict);
+        bool get_lo(expr* e, rational& lo, bool& strict);
+        bool get_up(expr* e, rational& up, bool& strict);
+        bool get_value_equiv(expr* e, rational& value);
+        expr_ref get_lo(expr* e);
+        expr_ref get_up(expr* e);
+        expr_ref get_fixed(expr* e);
+#endif
+    };
+};

src/sat/smt/polysat/saturation.h

@@ -0,0 +1,241 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    Polysat core saturation
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-6
+
+--*/
+#pragma once
+
+#include "math/polysat/constraints.h"
+
+namespace polysat {
+
+    struct bilinear {
+        rational a, b, c, d;
+
+        rational eval(rational const& x, rational const& y) const {
+            return a*x*y + b*x + c*y + d;
+        }
+
+        bilinear operator-() const {
+            bilinear r(*this);
+            r.a = -r.a;
+            r.b = -r.b;
+            r.c = -r.c;
+            r.d = -r.d;
+            return r;
+        }
+
+        bilinear operator-(bilinear const& other) const {
+            bilinear r(*this);
+            r.a -= other.a;
+            r.b -= other.b;
+            r.c -= other.c;
+            r.d -= other.d;
+            return r;
+        }
+
+        bilinear operator+(rational const& d) const {
+            bilinear r(*this);
+            r.d += d;
+            return r;
+        }
+        
+        bilinear operator-(rational const& d) const {
+            bilinear r(*this);
+            r.d -= d;
+            return r;
+        }
+
+        bilinear operator-(int d) const {
+            bilinear r(*this);
+            r.d -= d;
+            return r;
+        }
+};
+
+    inline std::ostream& operator<<(std::ostream& out, bilinear const& b) {
+        return out << b.a << "*x*y + " << b.b << "*x + " << b.c << "*y + " << b.d;
+    }
+
+    /**
+     * Introduce lemmas that derive new (simpler) constraints from the current conflict and partial model.
+     */
+    class saturation {
+
+        core& c;
+        constraints& C;
+        char const* m_rule = nullptr;
+        
+#if 0
+        parity_tracker m_parity_tracker;
+        unsigned_vector m_occ;
+        unsigned_vector m_occ_cnt;
+
+        void set_rule(char const* r) { m_rule = r; }
+
+        bool is_non_overflow(pdd const& x, pdd const& y, signed_constraint& c);
+        signed_constraint ineq(bool strict, pdd const& lhs, pdd const& rhs);
+
+        void log_lemma(pvar v, conflict& core);
+        bool propagate(pvar v, conflict& core, signed_constraint crit1, signed_constraint c);
+        bool propagate(pvar v, conflict& core, inequality const& crit1, signed_constraint c);
+        bool propagate(pvar v, conflict& core, signed_constraint c);
+        bool add_conflict(pvar v, conflict& core, inequality const& crit1, signed_constraint c);
+        bool add_conflict(pvar v, conflict& core, inequality const& crit1, inequality const& crit2, signed_constraint c);
+
+        bool try_ugt_x(pvar v, conflict& core, inequality const& c);
+
+        bool try_ugt_y(pvar v, conflict& core, inequality const& c);
+        bool try_ugt_y(pvar v, conflict& core, inequality const& l_y, inequality const& yx_l_zx, pdd const& x, pdd const& z);
+
+        bool try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& c);
+        bool try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& x_l_z, inequality const& y_l_ax, pdd const& a, pdd const& y);
+
+        bool try_ugt_z(pvar z, conflict& core, inequality const& c);
+        bool try_ugt_z(pvar z, conflict& core, inequality const& x_l_z0, inequality const& yz_l_xz, pdd const& y, pdd const& x);
+
+        bool try_parity(pvar x, conflict& core, inequality const& axb_l_y);
+        bool try_parity_diseq(pvar x, conflict& core, inequality const& axb_l_y);
+        bool try_mul_bounds(pvar x, conflict& core, inequality const& axb_l_y);
+        bool try_factor_equality(pvar x, conflict& core, inequality const& a_l_b);
+        bool try_infer_equality(pvar x, conflict& core, inequality const& a_l_b);
+        bool try_mul_eq_1(pvar x, conflict& core, inequality const& axb_l_y);
+        bool try_mul_odd(pvar x, conflict& core, inequality const& axb_l_y);
+        bool try_mul_eq_bound(pvar x, conflict& core, inequality const& axb_l_y);
+        bool try_transitivity(pvar x, conflict& core, inequality const& axb_l_y);
+        bool try_tangent(pvar v, conflict& core, inequality const& c);
+        bool try_add_overflow_bound(pvar x, conflict& core, inequality const& axb_l_y);
+        bool try_add_mul_bound(pvar x, conflict& core, inequality const& axb_l_y);
+        bool try_infer_parity_equality(pvar x, conflict& core, inequality const& a_l_b);
+        bool try_div_monotonicity(conflict& core);
+
+        bool try_nonzero_upper_extract(pvar v, conflict& core, inequality const& i);
+        bool try_congruence(pvar v, conflict& core, inequality const& i);
+
+
+        rational round(rational const& M, rational const& x);
+        bool eval_round(rational const& M, pdd const& p, rational& r);
+        bool extract_linear_form(pdd const& q, pvar& y, rational& a, rational& b);
+        bool extract_bilinear_form(pvar x, pdd const& p, pvar& y, bilinear& b);
+        bool adjust_bound(rational const& x_min, rational const& x_max, rational const& y0, rational const& M,
+                          bilinear& b, rational& x_split);
+        bool update_min(rational& y_min, rational const& x_min, rational const& x_max,
+                        bilinear const& b);
+        bool update_max(rational& y_max, rational const& x_min, rational const& x_max,
+                        bilinear const& b);
+        bool update_bounds_for_xs(rational const& x_min, rational const& x_max, rational& y_min, rational& y_max,
+                                  rational const& y0, bilinear b1, bilinear b2,
+                                  rational const& M, inequality const& a_l_b);
+        void fix_values(pvar x, pvar y, pdd const& p);
+        void fix_values(pvar y, pdd const& p);
+        
+        // c := lhs ~ v
+        //  where ~ is < or <=
+        bool is_l_v(pvar v, inequality const& c);
+
+        // c := v ~ rhs
+        bool is_g_v(pvar v, inequality const& c);
+
+        // c := x ~ Y
+        bool is_x_l_Y(pvar x, inequality const& i, pdd& y);
+
+        // c := Y ~ x
+        bool is_Y_l_x(pvar x, inequality const& i, pdd& y);
+
+        // c := X*y ~ X*Z
+        bool is_Xy_l_XZ(pvar y, inequality const& c, pdd& x, pdd& z);
+        bool verify_Xy_l_XZ(pvar y, inequality const& c, pdd const& x, pdd const& z);
+
+        // c := Y ~ Ax
+        bool is_Y_l_Ax(pvar x, inequality const& c, pdd& a, pdd& y);
+        bool verify_Y_l_Ax(pvar x, inequality const& c, pdd const& a, pdd const& y);
+
+        // c := Ax ~ Y
+        bool is_Ax_l_Y(pvar x, inequality const& c, pdd& a, pdd& y);
+        bool verify_Ax_l_Y(pvar x, inequality const& c, pdd const& a, pdd const& y);
+
+        // c := Ax + B ~ Y
+        bool is_AxB_l_Y(pvar x, inequality const& c, pdd& a, pdd& b, pdd& y);
+        bool verify_AxB_l_Y(pvar x, inequality const& c, pdd const& a, pdd const& b, pdd const& y);
+
+        // c := Y ~ Ax + B
+        bool is_Y_l_AxB(pvar x, inequality const& c, pdd& y, pdd& a, pdd& b);
+        bool verify_Y_l_AxB(pvar x, inequality const& c, pdd const& y, pdd const& a, pdd& b);
+
+        // c := Ax + B ~ Y, val(Y) = 0
+        bool is_AxB_eq_0(pvar x, inequality const& c, pdd& a, pdd& b, pdd& y);
+        bool verify_AxB_eq_0(pvar x, inequality const& c, pdd const& a, pdd const& b, pdd const& y);
+
+        // c := Ax + B != Y, val(Y) = 0
+        bool is_AxB_diseq_0(pvar x, inequality const& c, pdd& a, pdd& b, pdd& y);
+
+        // c := Y*X ~ z*X
+        bool is_YX_l_zX(pvar z, inequality const& c, pdd& x, pdd& y);
+        bool verify_YX_l_zX(pvar z, inequality const& c, pdd const& x, pdd const& y);
+
+        // c := xY <= xZ
+        bool is_xY_l_xZ(pvar x, inequality const& c, pdd& y, pdd& z);
+
+        // xy := x * Y
+        bool is_xY(pvar x, pdd const& xy, pdd& y);
+
+        // a * b does not overflow
+        bool is_non_overflow(pdd const& a, pdd const& b);
+
+        // p := coeff*x*y where coeff_x = coeff*x, x a variable
+        bool is_coeffxY(pdd const& coeff_x, pdd const& p, pdd& y);
+
+        bool is_add_overflow(pvar x, inequality const& i, pdd& y, bool& is_minus);
+
+        bool has_upper_bound(pvar x, conflict& core, rational& bound, vector<signed_constraint>& x_ge_bound);
+
+        bool has_lower_bound(pvar x, conflict& core, rational& bound, vector<signed_constraint>& x_le_bound);
+
+        // inequality i implies x != 0
+        bool is_nonzero_by(pvar x, inequality const& i);
+
+        // determine min/max parity of polynomial
+        unsigned min_parity(pdd const& p, vector<signed_constraint>& explain);
+        unsigned max_parity(pdd const& p, vector<signed_constraint>& explain);
+        unsigned min_parity(pdd const& p) { vector<signed_constraint> ex; return min_parity(p, ex); }
+        unsigned max_parity(pdd const& p) { vector<signed_constraint> ex; return max_parity(p, ex); }
+
+        lbool get_multiple(const pdd& p1, const pdd& p2, pdd& out);
+        
+        bool is_forced_eq(pdd const& p, rational const& val);
+        bool is_forced_eq(pdd const& p, int i) { return is_forced_eq(p, rational(i)); }
+        
+        bool is_forced_diseq(pdd const& p, rational const& val, signed_constraint& c);
+        bool is_forced_diseq(pdd const& p, int i, signed_constraint& c) { return is_forced_diseq(p, rational(i), c); }
+
+        bool is_forced_odd(pdd const& p, signed_constraint& c);
+
+        bool is_forced_false(signed_constraint const& sc);
+
+        bool is_forced_true(signed_constraint const& sc);
+
+        bool try_inequality(pvar v, inequality const& i);
+
+        bool try_umul_ovfl(pvar v, signed_constraint c);
+        bool try_umul_ovfl_noovfl(pvar v, signed_constraint c);
+        bool try_umul_noovfl_lo(pvar v, signed_constraint c);
+        bool try_umul_noovfl_bounds(pvar v, signed_constraint c);
+        bool try_umul_ovfl_bounds(pvar v, signed_constraint c);
+
+        bool try_op(pvar v, signed_constraint c);
+#endif
+
+    public:
+        saturation(core& c);
+        void perform(pvar v);
+        bool perform(pvar v, signed_constraint sc);
+    };
+}