diff --git a/scripts/out/Microsoft.Z3.x64.4.8.9.nupkg b/scripts/out/Microsoft.Z3.x64.4.8.9.nupkg
new file mode 100644
index 000000000..9b4c02a06
Binary files /dev/null and b/scripts/out/Microsoft.Z3.x64.4.8.9.nupkg differ
diff --git a/scripts/out/Microsoft.Z3.x64.4.8.9.nupkg.zip b/scripts/out/Microsoft.Z3.x64.4.8.9.nupkg.zip
new file mode 100644
index 000000000..9b4c02a06
Binary files /dev/null and b/scripts/out/Microsoft.Z3.x64.4.8.9.nupkg.zip differ
diff --git a/scripts/out/Microsoft.Z3.x64.nuspec b/scripts/out/Microsoft.Z3.x64.nuspec
new file mode 100644
index 000000000..196157132
--- /dev/null
+++ b/scripts/out/Microsoft.Z3.x64.nuspec
@@ -0,0 +1,27 @@
+
+
+
+ Microsoft.Z3.x64
+ 4.8.9
+ Microsoft
+
+Z3 is a satisfiability modulo theories solver from Microsoft Research.
+
+Linux Dependencies:
+ libgomp.so.1 installed
+
+ © Microsoft Corporation. All rights reserved.
+ smt constraint solver theorem prover
+ https://raw.githubusercontent.com/Z3Prover/z3/79734f26aee55309077de1f26e9b6f50ecd99ceb/resources/icon.jpg
+ https://github.com/Z3Prover/z3
+ https://raw.githubusercontent.com/Z3Prover/z3/79734f26aee55309077de1f26e9b6f50ecd99ceb/LICENSE.txt
+
+ true
+ en
+
+
\ No newline at end of file
diff --git a/scripts/out/build/Microsoft.Z3.targets b/scripts/out/build/Microsoft.Z3.targets
new file mode 100644
index 000000000..bf2ca2dc7
--- /dev/null
+++ b/scripts/out/build/Microsoft.Z3.targets
@@ -0,0 +1,10 @@
+
+
+
+
+ false
+ libz3.dll
+ PreserveNewest
+
+
+
diff --git a/scripts/out/lib/netstandard1.4/Microsoft.Z3.dll b/scripts/out/lib/netstandard1.4/Microsoft.Z3.dll
new file mode 100644
index 000000000..db7c360d5
Binary files /dev/null and b/scripts/out/lib/netstandard1.4/Microsoft.Z3.dll differ
diff --git a/scripts/out/runtimes/macos/native/libz3.dylib b/scripts/out/runtimes/macos/native/libz3.dylib
new file mode 100644
index 000000000..cfda8f18f
Binary files /dev/null and b/scripts/out/runtimes/macos/native/libz3.dylib differ
diff --git a/scripts/out/runtimes/ubuntu-x64/native/libz3.so b/scripts/out/runtimes/ubuntu-x64/native/libz3.so
new file mode 100644
index 000000000..d4417086f
Binary files /dev/null and b/scripts/out/runtimes/ubuntu-x64/native/libz3.so differ
diff --git a/scripts/out/runtimes/win-x64/native/libz3.dll b/scripts/out/runtimes/win-x64/native/libz3.dll
new file mode 100644
index 000000000..df6bd8d1a
Binary files /dev/null and b/scripts/out/runtimes/win-x64/native/libz3.dll differ
diff --git a/src/sat/smt/ar_solver.h b/src/sat/smt/ar_solver.h
new file mode 100644
index 000000000..8769b4431
--- /dev/null
+++ b/src/sat/smt/ar_solver.h
@@ -0,0 +1,297 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+ ar_solver.h
+
+Abstract:
+
+ Theory plugin for arrays
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2020-09-08
+
+--*/
+#pragma once
+
+#include "sat/smt/sat_th.h"
+#include "ast/array_decl_plugin.h"
+
+namespace euf {
+ class solver;
+}
+
+namespace array {
+
+ class solver : public euf::th_euf_solver {
+ typedef rational numeral;
+ 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 svector vars;
+ typedef std::pair value_sort_pair;
+ typedef pair_hash, unsigned_hash> value_sort_pair_hash;
+ typedef map > value2var;
+ typedef union_find bv_union_find;
+ typedef std::pair var_pos;
+
+ friend class ackerman;
+
+ struct stats {
+ unsigned m_num_diseq_static, m_num_diseq_dynamic, m_num_bit2core, m_num_th2core_eq, m_num_conflicts;
+ unsigned m_ackerman;
+ void reset() { memset(this, 0, sizeof(stats)); }
+ stats() { reset(); }
+ };
+
+ struct bv_justification {
+ enum kind_t { eq2bit, bit2eq };
+ kind_t m_kind;
+ theory_var m_v1;
+ theory_var m_v2;
+ sat::literal m_consequent;
+ sat::literal m_antecedent;
+ bv_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a) :
+ m_kind(kind_t::eq2bit), m_v1(v1), m_v2(v2), m_consequent(c), m_antecedent(a) {}
+ bv_justification(theory_var v1, theory_var v2):
+ m_kind(kind_t::bit2eq), m_v1(v1), m_v2(v2) {}
+ sat::ext_constraint_idx to_index() const {
+ return sat::constraint_base::mem2base(this);
+ }
+ static bv_justification& from_index(size_t idx) {
+ return *reinterpret_cast(sat::constraint_base::from_index(idx)->mem());
+ }
+ static size_t get_obj_size() { return sat::constraint_base::obj_size(sizeof(bv_justification)); }
+ };
+
+ sat::justification mk_eq2bit_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a);
+ sat::ext_justification_idx mk_bit2eq_justification(theory_var v1, theory_var v2);
+ void log_drat(bv_justification const& c);
+
+
+ /**
+ \brief Structure used to store the position of a bitvector variable that
+ contains the true_literal/false_literal.
+
+ Remark: the implementation assumes that bitvector variables containing
+ complementary bits are never merged. I assert a disequality (not (= x y))
+ whenever x and y contain complementary bits. However, this is too expensive
+ when the bit is the true_literal or false_literal. The number of disequalities
+ is too big. To avoid this problem, each equivalence class has a set
+ of its true_literal and false_literal bits in the form of svector.
+
+ Before merging two classes we just check if the merge is valid by traversing these
+ vectors.
+ */
+ struct zero_one_bit {
+ theory_var m_owner; //!< variable that owns the bit: useful for backtracking
+ unsigned m_idx:31;
+ unsigned m_is_true:1;
+ zero_one_bit(theory_var v = euf::null_theory_var, unsigned idx = UINT_MAX, bool is_true = false):
+ m_owner(v), m_idx(idx), m_is_true(is_true) {}
+ };
+
+ typedef svector zero_one_bits;
+
+ struct bit_atom;
+ struct def_atom;
+ class atom {
+ public:
+ virtual ~atom() {}
+ virtual bool is_bit() const = 0;
+ bit_atom& to_bit();
+ def_atom& to_def();
+ };
+
+ struct var_pos_occ {
+ var_pos m_vp;
+ var_pos_occ * m_next;
+ var_pos_occ(theory_var v = euf::null_theory_var, unsigned idx = 0, var_pos_occ * next = nullptr):m_vp(v, idx), m_next(next) {}
+ };
+
+ class var_pos_it {
+ var_pos_occ* m_first;
+ public:
+ var_pos_it(var_pos_occ* c) : m_first(c) {}
+ var_pos operator*() { return m_first->m_vp; }
+ var_pos_it& operator++() { m_first = m_first->m_next; return *this; }
+ var_pos_it operator++(int) { var_pos_it tmp = *this; ++* this; return tmp; }
+ bool operator==(var_pos_it const& other) const { return m_first == other.m_first; }
+ bool operator!=(var_pos_it const& other) const { return !(*this == other); }
+ };
+
+ struct bit_atom : public atom {
+ var_pos_occ * m_occs;
+ bit_atom():m_occs(nullptr) {}
+ ~bit_atom() override {}
+ bool is_bit() const override { return true; }
+ var_pos_it begin() const { return var_pos_it(m_occs); }
+ var_pos_it end() const { return var_pos_it(nullptr); }
+ };
+
+ struct def_atom : public atom {
+ literal m_var;
+ literal m_def;
+ def_atom(literal v, literal d):m_var(v), m_def(d) {}
+ ~def_atom() override {}
+ bool is_bit() const override { return false; }
+ };
+
+ class bit_trail;
+ class add_var_pos_trail;
+ class mk_atom_trail;
+ typedef ptr_vector bool_var2atom;
+
+ bv_util bv;
+ arith_util m_autil;
+ stats m_stats;
+ ackerman m_ackerman;
+ bit_blaster m_bb;
+ bv_union_find m_find;
+ vector m_bits; // per var, the bits of a given variable.
+ unsigned_vector m_wpos; // per var, watch position for fixed variable detection.
+ vector m_zero_one_bits; // per var, see comment in the struct zero_one_bit
+ bool_var2atom m_bool_var2atom;
+ value2var m_fixed_var_table;
+ mutable vector m_power2;
+ literal_vector m_tmp_literals;
+ svector m_prop_queue;
+ unsigned_vector m_prop_queue_lim;
+ unsigned m_prop_queue_head { 0 };
+
+
+ sat::solver* m_solver;
+ sat::solver& s() { return *m_solver; }
+
+ // internalize
+ void insert_bv2a(bool_var bv, atom * a) { m_bool_var2atom.setx(bv, a, 0); }
+ void erase_bv2a(bool_var bv) { m_bool_var2atom[bv] = 0; }
+ atom * get_bv2a(bool_var bv) const { return m_bool_var2atom.get(bv, 0); }
+ bool visit(expr* e) override;
+ bool visited(expr* e) override;
+ bool post_visit(expr* e, bool sign, bool root) override;
+ unsigned get_bv_size(euf::enode* n);
+ unsigned get_bv_size(theory_var v);
+ theory_var get_var(euf::enode* n);
+ euf::enode* get_arg(euf::enode* n, unsigned idx);
+ inline theory_var get_arg_var(euf::enode* n, unsigned idx);
+ void get_bits(theory_var v, expr_ref_vector& r);
+ void get_bits(euf::enode* n, expr_ref_vector& r);
+ void get_arg_bits(app* n, unsigned idx, expr_ref_vector& r);
+ void fixed_var_eh(theory_var v);
+ bool is_bv(theory_var v) const { return bv.is_bv(var2expr(v)); }
+ sat::status status() const { return sat::status::th(m_is_redundant, get_id()); }
+ void register_true_false_bit(theory_var v, unsigned i);
+ void add_bit(theory_var v, sat::literal lit);
+ void set_bit_eh(theory_var v, literal l, unsigned idx);
+ void init_bits(expr* e, expr_ref_vector const & bits);
+ void mk_bits(theory_var v);
+ void add_def(sat::literal def, sat::literal l);
+ void internalize_unary(app* n, std::function& fn);
+ void internalize_binary(app* n, std::function& fn);
+ void internalize_ac_binary(app* n, std::function& fn);
+ void internalize_par_unary(app* n, std::function& fn);
+ void internalize_novfl(app* n, std::function& fn);
+ void internalize_num(app * n, theory_var v);
+ void internalize_concat(app * n);
+ void internalize_bv2int(app* n);
+ void internalize_int2bv(app* n);
+ void internalize_mkbv(app* n);
+ void internalize_xor3(app* n);
+ void internalize_carry(app* n);
+ void internalize_sub(app* n);
+ void internalize_extract(app* n);
+ void internalize_bit2bool(app* n);
+ template
+ void internalize_le(app* n);
+ void assert_bv2int_axiom(app * n);
+ void assert_int2bv_axiom(app* n);
+ void assert_ackerman(theory_var v1, theory_var v2);
+
+ // solving
+ theory_var find(theory_var v) const { return m_find.find(v); }
+ void find_wpos(theory_var v);
+ void find_new_diseq_axioms(bit_atom& a, theory_var v, unsigned idx);
+ void mk_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx);
+ bool get_fixed_value(theory_var v, numeral& result) const;
+ void add_fixed_eq(theory_var v1, theory_var v2);
+ svector m_merge_aux[2]; //!< auxiliary vector used in merge_zero_one_bits
+ bool merge_zero_one_bits(theory_var r1, theory_var r2);
+ void assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc);
+ void propagate_bits(var_pos entry);
+ numeral const& power2(unsigned i) const;
+
+ // invariants
+ bool check_zero_one_bits(theory_var v);
+
+ public:
+ solver(euf::solver& ctx, theory_id id);
+ ~solver() override {}
+ void set_solver(sat::solver* s) override { m_solver = s; }
+ void set_lookahead(sat::lookahead* s) override { }
+ void init_search() override {}
+ double get_reward(literal l, sat::ext_constraint_idx idx, sat::literal_occs_fun& occs) const override;
+ bool is_extended_binary(sat::ext_justification_idx idx, literal_vector& r) override;
+ bool is_external(bool_var v) override;
+ bool propagate(literal l, sat::ext_constraint_idx idx) override;
+ 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;
+ void push() override;
+ void pop(unsigned n) override;
+ void pre_simplify() override;
+ void simplify() override;
+ bool set_root(literal l, literal r) override;
+ void flush_roots() override;
+ void clauses_modifed() override;
+ lbool get_phase(bool_var v) 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;
+ extension* copy(sat::solver* s) override;
+ void find_mutexes(literal_vector& lits, vector & mutexes) override {}
+ void gc() override {}
+ void pop_reinit() override;
+ bool validate() override;
+ void init_use_list(sat::ext_use_list& ul) override;
+ bool is_blocked(literal l, sat::ext_constraint_idx) override;
+ bool check_model(sat::model const& m) const override;
+ unsigned max_var(unsigned w) const override;
+
+ void new_eq_eh(euf::th_eq const& eq) override;
+ bool unit_propagate() override;
+
+ void add_value(euf::enode* n, expr_ref_vector& values) override;
+
+ bool extract_pb(std::function& card,
+ std::function& pb) override { return false; }
+
+ bool to_formulas(std::function& l2e, expr_ref_vector& fmls) override { return false; }
+ 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;
+
+
+ void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2);
+ void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { SASSERT(check_zero_one_bits(r1)); }
+ void unmerge_eh(theory_var v1, theory_var v2);
+ trail_stack& get_trail_stack();
+
+ // disagnostics
+ std::ostream& display(std::ostream& out, theory_var v) const;
+ typedef std::pair pp_var;
+ pp_var pp(theory_var v) const { return pp_var(this, v); }
+
+ };
+
+ inline std::ostream& operator<<(std::ostream& out, solver::pp_var const& p) { return p.first->display(out, p.second); }
+
+
+}
diff --git a/src/sat/smt/bv_delay_internalize.cpp b/src/sat/smt/bv_delay_internalize.cpp
index 6bc299063..0b6ff6838 100644
--- a/src/sat/smt/bv_delay_internalize.cpp
+++ b/src/sat/smt/bv_delay_internalize.cpp
@@ -169,7 +169,6 @@ namespace bv {
bool solver::check_mul_zero(app* n, expr_ref_vector const& arg_values, expr* mul_value, expr* arg_value) {
SASSERT(mul_value != arg_value);
SASSERT(!(bv.is_zero(mul_value) && bv.is_zero(arg_value)));
-
if (bv.is_zero(arg_value)) {
unsigned sz = n->get_num_args();
expr_ref_vector args(m, sz, n->get_args());
@@ -180,6 +179,7 @@ namespace bv {
set_delay_internalize(r, internalize_mode::init_bits_only_i); // do not bit-blast this multiplier.
expr_ref eq(m.mk_eq(r, arg_value), m);
args[i] = n->get_arg(i);
+ std::cout << eq << "@" << s().scope_lvl() << "\n";
add_unit(b_internalize(eq));
}
return false;
@@ -298,6 +298,8 @@ namespace bv {
set_delay_internalize(rhs, internalize_mode::no_delay_i);
expr_ref eq(m.mk_eq(lhs, rhs), m);
add_unit(b_internalize(eq));
+ TRACE("bv", tout << "low-bits: " << eq << "\n";);
+ std::cout << "low bits\n";
return false;
}
diff --git a/src/util/compressed_limit_trail.h b/src/util/compressed_limit_trail.h
new file mode 100644
index 000000000..6ad17ef1f
--- /dev/null
+++ b/src/util/compressed_limit_trail.h
@@ -0,0 +1,36 @@
+
+#include "util/vector.h"
+
+#pragma once
+
+class compressed_limit_trail {
+ unsigned_vector m_lim;
+ unsigned m_scopes{ 0 };
+ unsigned m_last{ 0 };
+ public:
+
+ void push(unsigned n) {
+ if (m_last == n)
+ m_scopes++;
+ else {
+ for (; m_scopes > 0; --m_scopes)
+ m_lim.push_back(m_last);
+ m_last = n;
+ }
+ }
+ unsigned pop(unsigned n) {
+ SASSERT(n > 0);
+ SASSERT(m_scopes + m_lim.size() >= n);
+ if (n <= m_scopes) {
+ m_scopes -= n;
+ return m_last;
+ }
+ else {
+ n -= m_scopes;
+ m_scopes = 0;
+ m_last = m_lim[m_lim.size() - n];
+ m_lim.shrink(m_lim.size() - n);
+ return m_last;
+ }
+ }
+};