mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

fix #2509, fix issue with model inheritance exposed by #2483

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-08-27 10:48:22 -03:00
parent 271cd2ac6b
commit 2e6908bd9e
7 changed files with 61 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/nlsat/nlsat_explain.cpp
View file

@ -1467,10 +1467,7 @@ namespace nlsat {
m_result = &result;
svector<literal> lits;
TRACE("nlsat", tout << "project x" << x << "\n";
for (unsigned i = 0; i < num; ++i) {
m_solver.display(tout, ls[i]) << " ";
}
tout << "\n";
m_solver.display(tout, num, ls);
m_solver.display(tout););
DEBUG_CODE(
@ -1514,12 +1511,7 @@ namespace nlsat {
result.set(i, ~result[i]);
}
DEBUG_CODE(
TRACE("nlsat",
for (literal l : result) {
m_solver.display(tout << " ", l);
}
tout << "\n";
);
TRACE("nlsat", m_solver.display(tout, result.size(), result.c_ptr()); );
for (literal l : result) {
CTRACE("nlsat", l_true != m_solver.value(l), m_solver.display(tout, l) << " " << m_solver.value(l) << "\n";);
SASSERT(l_true == m_solver.value(l));

10
src/nlsat/nlsat_solver.cpp
View file

@ -3282,6 +3282,12 @@ namespace nlsat {
m_imp->m_bvalues.reset();
m_imp->m_bvalues.append(vs);
m_imp->m_bvalues.resize(m_imp->m_atoms.size(), l_undef);
for (unsigned i = 0; i < m_imp->m_atoms.size(); ++i) {
atom* a = m_imp->m_atoms[i];
if (a) {
m_imp->m_bvalues[i] = to_lbool(m_imp->m_evaluator.eval(a, false));
}
}
TRACE("nlsat", display(tout););
}
@ -3329,6 +3335,10 @@ namespace nlsat {
return out;
}
std::ostream& solver::display(std::ostream & out, literal_vector const& ls) const {
return display(out, ls.size(), ls.c_ptr());
}
std::ostream& solver::display(std::ostream & out, var x) const {
return m_imp->m_display_var(out, x);
}

2
src/nlsat/nlsat_solver.h
View file

@ -241,6 +241,8 @@ namespace nlsat {
std::ostream& display(std::ostream & out, unsigned n, literal const* ls) const;
std::ostream& display(std::ostream & out, literal_vector const& ls) const;
std::ostream& display(std::ostream & out, atom const& a) const;
/**

15
src/qe/nlqsat.cpp
View file

@ -25,6 +25,7 @@ Revision History:
#include "ast/ast_pp.h"
#include "ast/for_each_expr.h"
#include "ast/rewriter/rewriter.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/rewriter/quant_hoist.h"
#include "qe/nlqsat.h"
@ -617,7 +618,7 @@ namespace qe {
*/
void ackermanize_div(expr_ref& fml) {
void ackermanize_div(expr_ref& fml, expr_ref_vector& paxioms) {
is_pure_proc is_pure(*this);
{
expr_fast_mark1 visited;
@ -626,10 +627,8 @@ namespace qe {
if (is_pure.has_divs()) {
arith_util arith(m);
proof_ref pr(m);
expr_ref_vector paxioms(m);
div_rewriter_star rw(*this);
rw(fml, fml, pr);
paxioms.push_back(fml);
vector<div> const& divs = rw.divs();
for (unsigned i = 0; i < divs.size(); ++i) {
expr_ref den_is0(m.mk_eq(divs[i].den, arith.mk_real(0)), m);
@ -640,7 +639,6 @@ namespace qe {
m.mk_eq(divs[i].name, divs[j].name)));
}
}
fml = mk_and(paxioms);
}
}
@ -669,14 +667,16 @@ namespace qe {
// expr -> nlsat::solver
void hoist(expr_ref& fml) {
ackermanize_div(fml);
expr_ref_vector paxioms(m);
ackermanize_div(fml, paxioms);
quantifier_hoister hoist(m);
vector<app_ref_vector> qvars;
app_ref_vector vars(m);
bool is_forall = false;
pred_abs abs(m);
abs.get_free_vars(fml, vars);
expr_ref fml_a(m.mk_and(fml, mk_and(paxioms)), m);
abs.get_free_vars(fml_a, vars);
insert_set(m_free_vars, vars);
qvars.push_back(vars);
vars.reset();
@ -706,6 +706,9 @@ namespace qe {
fml = m.mk_iff(is_true, fml);
goal_ref g = alloc(goal, m);
g->assert_expr(fml);
for (expr* f : paxioms) {
g->assert_expr(f);
}
expr_dependency_ref core(m);
goal_ref_buffer result;
(*m_nftactic)(g, result);

35
src/smt/theory_seq.cpp
View file

@ -2338,6 +2338,13 @@ bool theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) {
display_deps(tout, dep);
);
TRACE("seq",
tout << "assert: "
<< mk_bounded_pp(n1->get_owner(), m) << " = " << mk_bounded_pp(n2->get_owner(), m) << " <-\n"
<< lits << "\n";
);
justification* js = ctx.mk_justification(
ext_theory_eq_propagation_justification(
get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2));
@ -2473,7 +2480,24 @@ bool theory_seq::solve_itos(expr_ref_vector const& ls, expr_ref_vector const& rs
return false;
}
bool theory_seq::solve_nth_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep) {
bool theory_seq::solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps) {
rational n;
expr* s = nullptr, *idx = nullptr;
if (ls.size() == 1 && m_util.str.is_nth_i(ls[0], s, idx)) {
expr_ref lhs(m_util.str.mk_at(s, idx), m);
expr_ref rhs(m_util.str.mk_concat(rs.size(), rs.c_ptr()), m);
expr_ref_vector ls1(m); ls1.push_back(lhs);
expr_ref_vector rs1(m); rs1.push_back(m_util.str.mk_unit(rhs));
m_eqs.push_back(eq(m_eq_id++, ls1, rs1, deps));
return true;
}
return false;
}
bool theory_seq::solve_nth_eq1(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep) {
if (solve_nth_eq2(ls, rs, dep)) {
return true;
}
if (ls.size() != 1 || rs.size() <= 1) {
return false;
}
@ -2649,10 +2673,10 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de
TRACE("seq", tout << "binary\n";);
return true;
}
if (!ctx.inconsistent() && solve_nth_eq(ls, rs, deps)) {
if (!ctx.inconsistent() && solve_nth_eq1(ls, rs, deps)) {
return true;
}
if (!ctx.inconsistent() && solve_nth_eq(rs, ls, deps)) {
if (!ctx.inconsistent() && solve_nth_eq1(rs, ls, deps)) {
return true;
}
if (!ctx.inconsistent() && solve_itos(rs, ls, deps)) {
@ -5557,6 +5581,11 @@ bool theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
TRACE("seq_verbose",
tout << "assert: " << mk_pp(e1, m) << " = " << mk_pp(e2, m) << " <- \n";
if (!lits.empty()) { ctx.display_literals_verbose(tout, lits) << "\n"; });
TRACE("seq",
tout << "assert: " << mk_bounded_pp(e1, m) << " = " << mk_bounded_pp(e2, m) << " <- \n";
tout << lits << "\n";);
justification* js =
ctx.mk_justification(
ext_theory_eq_propagation_justification(

3
src/smt/theory_seq.h
View file

@ -488,7 +488,8 @@ namespace smt {
bool lift_ite(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
bool solve_unit_eq(expr* l, expr* r, dependency* dep);
bool solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
bool solve_nth_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
bool solve_nth_eq1(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
bool solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
bool solve_itos(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
bool is_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, expr_ref& x, ptr_vector<expr>& xunits, ptr_vector<expr>& yunits, expr_ref& y);
bool is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x1, expr_ref_vector& xs, expr_ref& x2, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2);

4
src/tactic/core/tseitin_cnf_tactic.cpp
View file

@ -49,6 +49,7 @@ Author:
Notes:
--*/
#include "ast/ast_pp.h"
#include "tactic/tactical.h"
#include "tactic/goal_shared_occs.h"
#include "tactic/generic_model_converter.h"
@ -268,6 +269,7 @@ class tseitin_cnf_tactic : public tactic {
!m.is_or(c1, c1, c2))
return false;
SASSERT(to_app(n)->get_num_args() == 3);
swap_if_gt(a1, a2);
swap_if_gt(b1, b2);
swap_if_gt(c1, c2);
@ -834,6 +836,8 @@ class tseitin_cnf_tactic : public tactic {
m_produce_models = g->models_enabled();
m_produce_unsat_cores = g->unsat_core_enabled();
TRACE("tseitin_cnf", g->display(tout););
m_occs(*g);
reset_cache();
m_deps.reset();