mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 20:50:50 +00:00
Code Activity

fix #3751

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-04 23:01:30 -07:00
parent 7ae9734db2
commit e419565239
2 changed files with 11 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/tactic/ufbv/ufbv_rewriter.cpp
View file

@ -49,7 +49,7 @@ ufbv_rewriter::~ufbv_rewriter() {
} }
} }
bool ufbv_rewriter::is_demodulator(expr * e, expr_ref & large, expr_ref & small) const { bool ufbv_rewriter::is_demodulator(expr * e, app_ref & large, expr_ref & small) const {
if (!is_forall(e)) { if (!is_forall(e)) {
return false; return false;
} }
@ -65,13 +65,13 @@ bool ufbv_rewriter::is_demodulator(expr * e, expr_ref & large, expr_ref & small)
// We only track uninterpreted functions, everything else is likely too expensive. // We only track uninterpreted functions, everything else is likely too expensive.
if ((subset == +1 || subset == +2) && smaller == +1) { if ((subset == +1 || subset == +2) && smaller == +1) {
if (is_uninterp(rhs)) { if (is_uninterp(rhs)) {
large = rhs; large = to_app(rhs);
small = lhs; small = lhs;
return true; return true;
} }
// lhs = (not rhs) --> (not lhs) = rhs // lhs = (not rhs) --> (not lhs) = rhs
if (m.is_not(rhs, n) && is_uninterp(n)) { if (m.is_not(rhs, n) && is_uninterp(n)) {
large = n; large = to_app(n);
small = m.mk_not(lhs); small = m.mk_not(lhs);
return true; return true;
} }
@ -79,21 +79,21 @@ bool ufbv_rewriter::is_demodulator(expr * e, expr_ref & large, expr_ref & small)
if ((subset == -1 || subset == +2) && smaller == -1) { if ((subset == -1 || subset == +2) && smaller == -1) {
if (is_uninterp(lhs)) { if (is_uninterp(lhs)) {
large = lhs; large = to_app(lhs);
small = rhs; small = rhs;
return true; return true;
} }
// (not lhs) = rhs --> lhs = (not rhs) // (not lhs) = rhs --> lhs = (not rhs)
if (m.is_not(lhs, n) && is_uninterp(n)) { if (m.is_not(lhs, n) && is_uninterp(n)) {
large = n; large = to_app(n);
small = m.mk_not(rhs); small = m.mk_not(rhs);
return true; return true;
} }
} }
} }
else if (m.is_not(qe, n)) { else if (m.is_not(qe, n) && is_app(n)) {
// this is like (not (f ... )) --> (= (f ...) false) // this is like (not (f ... )) --> (= (f ...) false)
large = n; large = to_app(n);
small = m.mk_false(); small = m.mk_false();
return true; return true;
} }
@ -649,7 +649,8 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const *
// SASSERT(rewrite(np)==np); // SASSERT(rewrite(np)==np);
// if (n' is not a demodulator) { // if (n' is not a demodulator) {
expr_ref large(m), small(m); app_ref large(m);
expr_ref small(m);
if (!is_demodulator(np, large, small)) { if (!is_demodulator(np, large, small)) {
// insert n' into m_processed // insert n' into m_processed
m_processed.insert(np); m_processed.insert(np);
@ -672,8 +673,7 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const *
tout << mk_pp(small.get(), m) << std::endl; ); tout << mk_pp(small.get(), m) << std::endl; );
// let f be the top symbol of n' // let f be the top symbol of n'
SASSERT(is_app(large)); func_decl * f = large->get_decl();
func_decl * f = to_app(large)->get_decl();
reschedule_processed(f); reschedule_processed(f);
reschedule_demodulators(f, large); reschedule_demodulators(f, large);

2
src/tactic/ufbv/ufbv_rewriter.h
View file

@ -175,7 +175,7 @@ class ufbv_rewriter {
void remove_fwd_idx(func_decl * f, quantifier * demodulator); void remove_fwd_idx(func_decl * f, quantifier * demodulator);
bool check_fwd_idx_consistency(); bool check_fwd_idx_consistency();
void show_fwd_idx(std::ostream & out); void show_fwd_idx(std::ostream & out);
bool is_demodulator(expr * e, expr_ref & large, expr_ref & small) const; bool is_demodulator(expr * e, app_ref & large, expr_ref & small) const;
bool can_rewrite(expr * n, expr * lhs); bool can_rewrite(expr * n, expr * lhs);
expr * rewrite(expr * n); expr * rewrite(expr * n);