mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 04:38:53 +00:00
Code Activity

fix build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-27 10:10:13 -07:00
parent 24a9ca3226
commit 9dd8ebb474
3 changed files with 23 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/ast/rewriter/arith_rewriter.cpp
View file

@ -22,6 +22,13 @@ Notes:
#include "math/polynomial/algebraic_numbers.h" #include "math/polynomial/algebraic_numbers.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
seq_util& arith_rewriter_core::seq() {
if (!m_seq) {
m_seq = alloc(seq_util, m());
}
return *m_seq;
}
void arith_rewriter::updt_local_params(params_ref const & _p) { void arith_rewriter::updt_local_params(params_ref const & _p) {
arith_rewriter_params p(_p); arith_rewriter_params p(_p);
m_arith_lhs = p.arith_lhs(); m_arith_lhs = p.arith_lhs();
@ -247,10 +254,10 @@ bool arith_rewriter::is_non_negative(expr* e) {
unsigned pu; unsigned pu;
return m_util.is_power(e, n, p) && m_util.is_unsigned(p, pu) && (pu % 2 == 0); return m_util.is_power(e, n, p) && m_util.is_unsigned(p, pu) && (pu % 2 == 0);
}; };
if (m_seq.str.is_length(e))
return true;
if (is_even_power(e)) if (is_even_power(e))
return true; return true;
if (seq().str.is_length(e))
return true;
if (!m_util.is_mul(e)) if (!m_util.is_mul(e))
return false; return false;
expr_mark mark; expr_mark mark;
@ -260,7 +267,7 @@ bool arith_rewriter::is_non_negative(expr* e) {
for (expr* arg : args) { for (expr* arg : args) {
if (is_even_power(arg)) if (is_even_power(arg))
continue; continue;
if (m_seq.str.is_length(e)) if (seq().str.is_length(e))
continue; continue;
if (m_util.is_numeral(arg, r)) { if (m_util.is_numeral(arg, r)) {
if (r.is_neg()) if (r.is_neg())

5
src/ast/rewriter/arith_rewriter.h
View file

@ -27,13 +27,14 @@ class arith_rewriter_core {
protected: protected:
typedef rational numeral; typedef rational numeral;
arith_util m_util; arith_util m_util;
seq_util m_seq; scoped_ptr<seq_util> m_seq;
bool m_expand_power; bool m_expand_power;
bool m_mul2power; bool m_mul2power;
bool m_expand_tan; bool m_expand_tan;
ast_manager & m() const { return m_util.get_manager(); } ast_manager & m() const { return m_util.get_manager(); }
family_id get_fid() const { return m_util.get_family_id(); } family_id get_fid() const { return m_util.get_family_id(); }
seq_util& seq();
bool is_numeral(expr * n) const { return m_util.is_numeral(n); } bool is_numeral(expr * n) const { return m_util.is_numeral(n); }
bool is_numeral(expr * n, numeral & r) const { return m_util.is_numeral(n, r); } bool is_numeral(expr * n, numeral & r) const { return m_util.is_numeral(n, r); }
@ -45,7 +46,7 @@ protected:
bool use_power() const { return m_mul2power && !m_expand_power; } bool use_power() const { return m_mul2power && !m_expand_power; }
decl_kind power_decl_kind() const { return OP_POWER; } decl_kind power_decl_kind() const { return OP_POWER; }
public: public:
arith_rewriter_core(ast_manager & m):m_util(m), m_seq(m) {} arith_rewriter_core(ast_manager & m):m_util(m) {}
bool is_zero(expr * n) const { return m_util.is_zero(n); } bool is_zero(expr * n) const { return m_util.is_zero(n); }
}; };

26
src/smt/seq_regex.cpp
View file

@ -309,7 +309,7 @@ namespace smt {
/** /**
* is_non_empty(r, u) => nullable or not c_i or is_non_empty(r_i, u union r) * is_non_empty(r, u) => nullable or not c_i or is_non_empty(r_i, u union r)
* *
* for each (c_i, r_i) in cofactors * for each (c_i, r_i) in cofactors (min-terms)
* *
* is_non_empty(r_i, u union r) := false if r_i in u * is_non_empty(r_i, u union r) := false if r_i in u
* *
@ -327,24 +327,23 @@ namespace smt {
if (!d) if (!d)
throw default_exception("derivative was not defined"); throw default_exception("derivative was not defined");
literal_vector lits; literal_vector lits;
lits.push_back(~lit);
if (null_lit != false_literal)
lits.push_back(null_lit);
expr_ref_pair_vector cofactors(m); expr_ref_pair_vector cofactors(m);
seq_rw().get_cofactors(d, cofactors); seq_rw().get_cofactors(d, cofactors);
for (auto const& p : cofactors) { for (auto const& p : cofactors) {
if (is_member(p.second, u))
continue;
expr_ref cond(p.first, m); expr_ref cond(p.first, m);
seq_rw().elim_condition(hd, cond); seq_rw().elim_condition(hd, cond);
rewrite(cond); rewrite(cond);
if (m.is_false(cond)) if (m.is_false(cond))
continue; continue;
lits.reset(); expr_ref next_non_empty = sk().mk_is_non_empty(p.second, re().mk_union(u, r));
lits.push_back(~lit); lits.push_back(th.mk_literal(next_non_empty));
if (!m.is_true(cond))
lits.push_back(~th.mk_literal(cond));
if (null_lit != false_literal)
lits.push_back(null_lit);
if (!is_member(p.second, u))
lits.push_back(th.mk_literal(sk().mk_is_non_empty(p.second, re().mk_union(u, r))));
th.add_axiom(lits);
} }
th.add_axiom(lits);
} }
@ -384,15 +383,10 @@ namespace smt {
continue; continue;
lits.reset(); lits.reset();
lits.push_back(~lit); lits.push_back(~lit);
expr_ref is_empty1 = sk().mk_is_non_empty(p.second, re().mk_union(u, r));
// TBD: triple check soundness here.
// elim_condition(x, x = 'a') = true
// forall x . x = 'a' => is_empty(r, u)
// <=>
// is_empty(r, u)
if (!m.is_true(cond)) { if (!m.is_true(cond)) {
lits.push_back(th.mk_literal(mk_forall(m, hd, mk_not(m, cond)))); lits.push_back(th.mk_literal(mk_forall(m, hd, mk_not(m, cond))));
} }
expr_ref is_empty1 = sk().mk_is_non_empty(p.second, re().mk_union(u, r));
lits.push_back(th.mk_literal(is_empty1)); lits.push_back(th.mk_literal(is_empty1));
th.add_axiom(lits); th.add_axiom(lits);
} }