add stubs for arithmetic

src/sat/smt/CMakeLists.txt

@@ -1,5 +1,9 @@
 z3_add_component(sat_smt
   SOURCES
+    arith_axioms.cpp
+    arith_diagnostics.cpp
+    arith_internalize.cpp
+    arith_solver.cpp
     array_axioms.cpp
     array_internalize.cpp
     array_model.cpp

src/sat/smt/arith_axioms.cpp

@@ -0,0 +1,34 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    arith_axioms.cpp
+
+Abstract:
+
+    Theory plugin for arithmetic
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-08
+
+--*/
+#pragma once
+
+#include "sat/smt/euf_solver.h"
+#include "sat/smt/arith_solver.h"
+
+
+namespace arith {
+
+    // q = 0 or q * (p div q) = p
+    void solver::mk_div_axiom(expr* p, expr* q) {
+        if (a.is_zero(q)) return;
+        literal eqz = eq_internalize(q, a.mk_real(0));
+        literal eq  = eq_internalize(a.mk_mul(q, a.mk_div(p, q)), p);
+        add_clause(eqz, eq);
+    }
+
+
+}

src/sat/smt/arith_diagnostics.cpp

@@ -0,0 +1,30 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    arith_diagnostics.cpp
+
+Abstract:
+
+    Theory plugin for arithmetic
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-08
+
+--*/
+#pragma once
+
+#include "sat/smt/euf_solver.h"
+#include "sat/smt/arith_solver.h"
+
+
+namespace arith {
+
+    
+    std::ostream& solver::display(std::ostream& out) const { return out; }
+    std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const { return out;}
+    std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const { return out;}
+    void solver::collect_statistics(statistics& st) const {}
+}

src/sat/smt/arith_internalize.cpp

@@ -0,0 +1,34 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    arith_internalize.cpp
+
+Abstract:
+
+    Theory plugin for arithmetic
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-08
+
+--*/
+#pragma once
+
+#include "sat/smt/euf_solver.h"
+#include "sat/smt/arith_solver.h"
+
+namespace arith {
+
+    bool solver::visit(expr* e) { return false; }
+    bool solver::visited(expr* e) { return false; }
+    bool solver::post_visit(expr* e, bool sign, bool root) { return false; }
+    void solver::ensure_var(euf::enode* n) {}
+    sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) { return sat::null_literal; }
+    void solver::internalize(expr* e, bool redundant) {}
+    euf::theory_var solver::mk_var(euf::enode* n) { return euf::null_theory_var; }
+    bool solver::is_shared(theory_var v) const { return false; }   
+    void solver::pop_core(unsigned n) {}
+        
+}

src/sat/smt/arith_solver.cpp

@@ -0,0 +1,40 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    arith_solver.cpp
+
+Abstract:
+
+    Theory plugin for arithmetic
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-08
+
+--*/
+#pragma once
+
+#include "sat/smt/euf_solver.h"
+#include "sat/smt/arith_solver.h"
+
+
+namespace arith {
+
+    solver::solver(euf::solver& ctx, theory_id id):
+        th_euf_solver(ctx, symbol("arith"), id),
+        a(m)
+    {}
+
+    solver::~solver() {}
+
+    void solver::asserted(literal l) {}
+    sat::check_result solver::check() { return sat::check_result::CR_DONE; }
+    
+    euf::th_solver* solver::clone(sat::solver* s, euf::solver& ctx) { return nullptr;}
+    void solver::new_eq_eh(euf::th_eq const& eq) {}
+    bool solver::unit_propagate() { return false; }
+    void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {}
+    void solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {}
+}

src/sat/smt/arith_solver.h

@@ -0,0 +1,82 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    arith_solver.h
+
+Abstract:
+
+    Theory plugin for arithmetic
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-08
+
+--*/
+#pragma once
+
+#include "ast/ast_trail.h"
+#include "sat/smt/sat_th.h"
+#include "ast/arith_decl_plugin.h"
+
+namespace euf {
+    class solver;
+}
+
+namespace arith {
+
+    class solver : public euf::th_euf_solver {
+        typedef euf::theory_var theory_var;
+        typedef euf::theory_id theory_id;
+        typedef sat::literal literal;
+        typedef sat::bool_var bool_var;
+        typedef sat::literal_vector literal_vector;
+        typedef union_find<solver, euf::solver>  array_union_find;
+
+
+        struct stats {
+            void reset() { memset(this, 0, sizeof(*this)); }
+            stats() { reset(); }
+        };
+
+
+        arith_util        a;
+        stats             m_stats;
+
+        // internalize
+        bool visit(expr* e) override;
+        bool visited(expr* e) override;
+        bool post_visit(expr* e, bool sign, bool root) override;
+        void ensure_var(euf::enode* n);
+
+        // axioms
+        void mk_div_axiom(expr* p, expr* q);
+
+        void pop_core(unsigned n) override;
+        
+    public:
+        solver(euf::solver& ctx, theory_id id);
+        ~solver() override;
+        bool is_external(bool_var v) override { return false; }
+        bool propagate(literal l, sat::ext_constraint_idx idx) override { UNREACHABLE(); return false; }
+        void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) override {}
+        void asserted(literal l) override;
+        sat::check_result check() override;
+
+        std::ostream& display(std::ostream& out) const override;
+        std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
+        std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
+        void collect_statistics(statistics& st) const override;
+        euf::th_solver* clone(sat::solver* s, euf::solver& ctx) override;
+        void new_eq_eh(euf::th_eq const& eq) override;
+        bool unit_propagate() override;
+        void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
+        void add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
+        sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
+        void internalize(expr* e, bool redundant) override;
+        euf::theory_var mk_var(euf::enode* n) override;
+        void apply_sort_cnstr(euf::enode* n, sort* s) override {}
+        bool is_shared(theory_var v) const override;
+    };
+}

src/sat/smt/sat_th.cpp

@@ -200,4 +200,9 @@ namespace euf {
         return ctx.mk_eq(e1, e2); 
     }
 
+    sat::literal th_euf_solver::eq_internalize(expr* a, expr* b) { 
+        return b_internalize(ctx.mk_eq(a, b)); 
+    }
+
+
 }

src/sat/smt/sat_th.h

@@ -143,6 +143,8 @@ namespace euf {
         bool is_true(sat::literal a, sat::literal b, sat::literal c) { return is_true(a) || is_true(b, c); }
         bool is_true(sat::literal a, sat::literal b, sat::literal c, sat::literal d) { return is_true(a) || is_true(b, c, c); }
 
+        sat::literal eq_internalize(expr* a, expr* b);
+
         euf::enode* e_internalize(expr* e) { internalize(e, m_is_redundant); return expr2enode(e); }
         euf::enode* mk_enode(expr* e, bool suppress_args);
         expr_ref mk_eq(expr* e1, expr* e2);