From 4f0c743e2bcc68192a1e39f81e9a0ce52cc52671 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 12 Oct 2020 11:24:08 -0700 Subject: [PATCH] add stubs for arithmetic --- src/sat/smt/CMakeLists.txt | 4 ++ src/sat/smt/arith_axioms.cpp | 34 +++++++++++++ src/sat/smt/arith_diagnostics.cpp | 30 +++++++++++ src/sat/smt/arith_internalize.cpp | 34 +++++++++++++ src/sat/smt/arith_solver.cpp | 40 +++++++++++++++ src/sat/smt/arith_solver.h | 82 +++++++++++++++++++++++++++++++ src/sat/smt/sat_th.cpp | 5 ++ src/sat/smt/sat_th.h | 2 + 8 files changed, 231 insertions(+) create mode 100644 src/sat/smt/arith_axioms.cpp create mode 100644 src/sat/smt/arith_diagnostics.cpp create mode 100644 src/sat/smt/arith_internalize.cpp create mode 100644 src/sat/smt/arith_solver.cpp create mode 100644 src/sat/smt/arith_solver.h diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index 0b00b4f5a..51a65c0f2 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/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 diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp new file mode 100644 index 000000000..ce8fc3e9d --- /dev/null +++ b/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); + } + + +} diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp new file mode 100644 index 000000000..0b83f4ee2 --- /dev/null +++ b/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 {} +} diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp new file mode 100644 index 000000000..5259d18bc --- /dev/null +++ b/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) {} + +} diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp new file mode 100644 index 000000000..12d234ad6 --- /dev/null +++ b/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& dep) {} +} diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h new file mode 100644 index 000000000..44cd0702b --- /dev/null +++ b/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 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& 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; + }; +} diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index a9ddaa7d7..31fa24078 100644 --- a/src/sat/smt/sat_th.cpp +++ b/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)); + } + + } diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 48c80a8d3..2a1f04912 100644 --- a/src/sat/smt/sat_th.h +++ 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);