mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-03 20:20:33 -07:00
parent f4472927c0
commit 31e16c7d60
2 changed files with 48 additions and 79 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

123
src/smt/theory_utvpi_def.h
View file

@ -47,8 +47,7 @@ Revision History:
--*/ --*/
#ifndef THEORY_UTVPI_DEF_H_ #pragma once
#define THEORY_UTVPI_DEF_H_
#include "smt/theory_utvpi.h" #include "smt/theory_utvpi.h"
#include "util/heap.h" #include "util/heap.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
@ -59,20 +58,20 @@ namespace smt {
template<typename Ext> template<typename Ext>
theory_utvpi<Ext>::theory_utvpi(ast_manager& m): theory_utvpi<Ext>::theory_utvpi(ast_manager& m):
theory(m.mk_family_id("arith")), theory(m.mk_family_id("arith")),
a(m), a(m),
m_arith_eq_adapter(*this, m_params, a), m_arith_eq_adapter(*this, m_params, a),
m_izero(null_theory_var), m_izero(null_theory_var),
m_rzero(null_theory_var), m_rzero(null_theory_var),
m_nc_functor(*this), m_nc_functor(*this),
m_asserted_qhead(0), m_asserted_qhead(0),
m_agility(0.5), m_agility(0.5),
m_lia(false), m_lia(false),
m_lra(false), m_lra(false),
m_non_utvpi_exprs(false), m_non_utvpi_exprs(false),
m_test(m), m_test(m),
m_factory(nullptr) { m_factory(nullptr) {
} }
template<typename Ext> template<typename Ext>
theory_utvpi<Ext>::~theory_utvpi() { theory_utvpi<Ext>::~theory_utvpi() {
@ -150,7 +149,7 @@ namespace smt {
template<typename Ext> template<typename Ext>
void theory_utvpi<Ext>::new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just) { void theory_utvpi<Ext>::new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just) {
rational k; rational k(0);
th_var s = expand(true, v1, k); th_var s = expand(true, v1, k);
th_var t = expand(false, v2, k); th_var t = expand(false, v2, k);
context& ctx = get_context(); context& ctx = get_context();
@ -168,26 +167,23 @@ namespace smt {
// Create equality ast, internalize_atom // Create equality ast, internalize_atom
// assign the corresponding equality literal. // assign the corresponding equality literal.
// //
// t1 - s1 = k
//
app_ref eq(m), s2(m), t2(m); app_ref eq(m), s2(m), t2(m);
app* s1 = get_enode(s)->get_owner(); app* s1 = get_enode(s)->get_owner();
app* t1 = get_enode(t)->get_owner(); app* t1 = get_enode(t)->get_owner();
s2 = a.mk_sub(t1, s1); s2 = a.mk_sub(t1, s1);
t2 = a.mk_numeral(k, m.get_sort(s2.get())); t2 = a.mk_numeral(k, m.get_sort(s2.get()));
// t1 - s1 = k
eq = m.mk_eq(s2.get(), t2.get()); eq = m.mk_eq(s2.get(), t2.get());
TRACE("utvpi", TRACE("utvpi", tout << v1 << " .. " << v2 << "\n" << eq << "\n";);
tout << v1 << " .. " << v2 << "\n";
tout << mk_pp(eq.get(), m) <<"\n";);
if (!internalize_atom(eq.get(), false)) { VERIFY (internalize_atom(eq.get(), false));
UNREACHABLE();
}
literal l(ctx.get_literal(eq.get())); literal l(ctx.get_literal(eq.get()));
if (!is_eq) { if (!is_eq) {
l = ~l; l.neg();
} }
ctx.assign(l, b_justification(&eq_just), false); ctx.assign(l, b_justification(&eq_just), false);
} }
@ -207,22 +203,8 @@ namespace smt {
inc_conflicts(); inc_conflicts();
literal_vector const& lits = m_nc_functor.get_lits(); literal_vector const& lits = m_nc_functor.get_lits();
context & ctx = get_context(); context & ctx = get_context();
IF_VERBOSE(2, IF_VERBOSE(2, ctx.display_literals_smt2(verbose_stream() << "conflict:\n", lits));
verbose_stream() << "conflict:\n"; TRACE("utvpi", ctx.display_literals_smt2(tout << "conflict:\n", lits););
for (unsigned i = 0; i < lits.size(); ++i) {
ast_manager& m = get_manager();
expr_ref e(m);
ctx.literal2expr(lits[i], e);
verbose_stream() << mk_pp(e, m) << "\n";
}
verbose_stream() << "\n";);
TRACE("utvpi",
tout << "conflict: ";
for (unsigned i = 0; i < lits.size(); ++i) {
ctx.display_literal_info(tout, lits[i]);
}
tout << "\n";
);
if (m_params.m_arith_dump_lemmas) { if (m_params.m_arith_dump_lemmas) {
symbol logic(m_lra ? (m_lia?"QF_LIRA":"QF_LRA") : "QF_LIA"); symbol logic(m_lra ? (m_lia?"QF_LIRA":"QF_LRA") : "QF_LIA");
@ -248,14 +230,15 @@ namespace smt {
template<typename Ext> template<typename Ext>
void theory_utvpi<Ext>::found_non_utvpi_expr(expr* n) { void theory_utvpi<Ext>::found_non_utvpi_expr(expr* n) {
if (!m_non_utvpi_exprs) { if (m_non_utvpi_exprs) {
std::stringstream msg; return;
msg << "found non utvpi logic expression:\n" << mk_pp(n, get_manager()) << "\n";
TRACE("utvpi", tout << msg.str(););
warning_msg("%s", msg.str().c_str());
get_context().push_trail(value_trail<context, bool>(m_non_utvpi_exprs));
m_non_utvpi_exprs = true;
} }
std::stringstream msg;
msg << "found non utvpi logic expression:\n" << mk_pp(n, get_manager()) << "\n";
TRACE("utvpi", tout << msg.str(););
warning_msg("%s", msg.str().c_str());
get_context().push_trail(value_trail<context, bool>(m_non_utvpi_exprs));
m_non_utvpi_exprs = true;
} }
template<typename Ext> template<typename Ext>
@ -283,8 +266,8 @@ namespace smt {
*/ */
template<typename Ext> template<typename Ext>
void theory_utvpi<Ext>::negate(coeffs& coeffs, rational& weight) { void theory_utvpi<Ext>::negate(coeffs& coeffs, rational& weight) {
for (unsigned i = 0; i < coeffs.size(); ++i) { for (auto& c : coeffs) {
coeffs[i].second.neg(); c.second.neg();
} }
weight.neg(); weight.neg();
} }
@ -303,8 +286,8 @@ namespace smt {
void theory_utvpi<Ext>::mk_coeffs(vector<std::pair<expr*,rational> > const& terms, coeffs& coeffs, rational& w) { void theory_utvpi<Ext>::mk_coeffs(vector<std::pair<expr*,rational> > const& terms, coeffs& coeffs, rational& w) {
coeffs.reset(); coeffs.reset();
w = m_test.get_weight(); w = m_test.get_weight();
for (unsigned i = 0; i < terms.size(); ++i) { for (auto const& t : terms) {
coeffs.push_back(std::make_pair(mk_var(terms[i].first), terms[i].second)); coeffs.push_back(std::make_pair(mk_var(t.first), t.second));
} }
} }
@ -475,8 +458,8 @@ namespace smt {
template<typename Ext> template<typename Ext>
void theory_utvpi<Ext>::display(std::ostream& out) const { void theory_utvpi<Ext>::display(std::ostream& out) const {
for (unsigned i = 0; i < m_atoms.size(); ++i) { for (auto const& a : m_atoms) {
m_atoms[i].display(*this, out); out << "\n"; a.display(*this, out); out << "\n";
} }
m_graph.display(out); m_graph.display(out);
} }
@ -775,12 +758,9 @@ namespace smt {
TRACE("utvpi", TRACE("utvpi",
tout << "Disparity: " << v1 << "\n"; tout << "Disparity: " << v1 << "\n";
for (auto v : zero_v) { tout << "decrement: " << zero_v << "\n";
tout << "decrement: " << v << "\n";
}
display(tout); display(tout);
); );
SASSERT(m_graph.is_feasible());
for (auto v : zero_v) { for (auto v : zero_v) {
m_graph.inc_assignment(v, numeral(-1)); m_graph.inc_assignment(v, numeral(-1));
@ -788,8 +768,9 @@ namespace smt {
if (!is_parity_ok(k)) { if (!is_parity_ok(k)) {
todo.push_back(k); todo.push_back(k);
} }
} }
TRACE("utvpi", display(tout);); TRACE("utvpi", display(tout););
SASSERT(m_graph.is_feasible());
} }
DEBUG_CODE( DEBUG_CODE(
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
@ -820,8 +801,8 @@ namespace smt {
void theory_utvpi<Ext>::model_validate() { void theory_utvpi<Ext>::model_validate() {
context& ctx = get_context(); context& ctx = get_context();
unsigned sz = m_atoms.size(); unsigned sz = m_atoms.size();
for (unsigned i = 0; i < sz; ++i) { for (auto const& a : m_atoms) {
bool_var b = m_atoms[i].get_bool_var(); bool_var b = a.get_bool_var();
if (!ctx.is_relevant(b)) { if (!ctx.is_relevant(b)) {
continue; continue;
} }
@ -841,20 +822,11 @@ namespace smt {
CTRACE("utvpi", !ok, CTRACE("utvpi", !ok,
tout << "validation failed:\n"; tout << "validation failed:\n";
tout << "Assignment: " << assign << "\n"; tout << "Assignment: " << assign << "\n";
m_atoms[i].display(*this, tout); a.display(*this, tout);
tout << "\n"; tout << "\n";
display(tout); display(tout);
m_graph.display_agl(tout); m_graph.display_agl(tout);
); );
if (!ok) {
std::cout << "validation failed:\n";
std::cout << "Assignment: " << assign << "\n";
m_atoms[i].display(*this, std::cout);
std::cout << "\n";
display(std::cout);
m_graph.display_agl(std::cout);
}
// CTRACE("utvpi", ok, tout << "validation success: " << mk_pp(e, get_manager()) << "\n";); // CTRACE("utvpi", ok, tout << "validation success: " << mk_pp(e, get_manager()) << "\n";);
SASSERT(ok); SASSERT(ok);
} }
@ -888,16 +860,12 @@ namespace smt {
} }
if (a.is_add(e)) { if (a.is_add(e)) {
r.reset(); r.reset();
for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) { for (expr* arg : *to_app(e)) r+= eval_num(arg);
r += eval_num(to_app(e)->get_arg(i));
}
return r; return r;
} }
if (a.is_mul(e)) { if (a.is_mul(e)) {
r = rational(1); r = rational(1);
for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) { for (expr* arg : *to_app(e)) r*= eval_num(arg);
r *= eval_num(to_app(e)->get_arg(i));
}
return r; return r;
} }
if (a.is_uminus(e, e1)) { if (a.is_uminus(e, e1)) {
@ -986,5 +954,4 @@ namespace smt {
}; };
#endif

4
src/util/vector.h
View file

@ -32,11 +32,13 @@ using char_vector = old_svector<char>;
using signed_char_vector = old_svector<signed char>; using signed_char_vector = old_svector<signed char>;
using double_vector = old_svector<double>; using double_vector = old_svector<double>;
inline std::ostream& operator<<(std::ostream& out, unsigned_vector const& v) { template<typename T>
inline std::ostream& operator<<(std::ostream& out, old_svector<T> const& v) {
for (unsigned u : v) out << u << " "; for (unsigned u : v) out << u << " ";
return out; return out;
} }
template<typename Hash, typename Vec> template<typename Hash, typename Vec>
struct vector_hash_tpl { struct vector_hash_tpl {
Hash m_hash; Hash m_hash;