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

test variants for seq_solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-05-30 18:15:10 -07:00
parent f03032bd09
commit 39acd3594a
4 changed files with 23 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/ast/ast.cpp
View file

@ -1575,19 +1575,6 @@ bool ast_manager::are_equal(expr * a, expr * b) const {
return false;
}
void ast_manager::inc_ref(ast * n) {
if (n) {
n->inc_ref();
}
}
void ast_manager::dec_ref(ast* n) {
if (n) {
n->dec_ref();
if (n->get_ref_count() == 0)
delete_node(n);
}
}
bool ast_manager::are_distinct(expr* a, expr* b) const {
if (is_app(a) && is_app(b)) {

16
src/ast/ast.h
View file

@ -1571,9 +1571,19 @@ public:
void debug_ref_count() { m_debug_ref_count = true; }
void inc_ref(ast * n);
void dec_ref(ast * n);
void inc_ref(ast * n) {
if (n) {
n->inc_ref();
}
}
void dec_ref(ast* n) {
if (n) {
n->dec_ref();
if (n->get_ref_count() == 0)
delete_node(n);
}
}
template<typename T>
void inc_array_ref(unsigned sz, T * const * a) {

6
src/cmd_context/basic_cmds.cpp
View file

@ -28,6 +28,7 @@ Notes:
#include"eval_cmd.h"
#include"gparams.h"
#include"env_params.h"
#include"well_sorted.h"
class help_cmd : public cmd {
svector<symbol> m_cmds;
@ -156,11 +157,16 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", {
pr = ctx.get_check_sat_result()->get_proof();
if (pr == 0)
throw cmd_exception("proof is not available");
if (ctx.well_sorted_check_enabled() && !is_well_sorted(ctx.m(), pr)) {
throw cmd_exception("proof is not well sorted");
}
// TODO: reimplement a new SMT2 pretty printer
ast_smt_pp pp(ctx.m());
cmd_is_declared isd(ctx);
pp.set_is_declared(&isd);
pp.set_logic(ctx.get_logic());
// ctx.regular_stream() << mk_pp(pr, ctx.m()) << "\n";
pp.display_smt2(ctx.regular_stream(), pr);
ctx.regular_stream() << std::endl;
});

8
src/smt/theory_seq.cpp
View file

@ -242,6 +242,7 @@ void theory_seq::init(context* ctx) {
}
final_check_status theory_seq::final_check_eh() {
m_new_propagation = false;
TRACE("seq", display(tout << "level: " << get_context().get_scope_level() << "\n"););
if (simplify_and_solve_eqs()) {
++m_stats.m_solve_eqs;
@ -1436,7 +1437,7 @@ bool theory_seq::solve_eqs(unsigned i) {
change = true;
}
}
return change || ctx.inconsistent();
return change || m_new_propagation || ctx.inconsistent();
}
bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* deps) {
@ -1831,8 +1832,6 @@ bool theory_seq::solve_ne(unsigned idx) {
continue;
}
else {
if (!updated) {
for (unsigned j = 0; j < i; ++j) {
new_ls.push_back(n.ls(j));
@ -2120,7 +2119,6 @@ bool theory_seq::explain_empty(expr_ref_vector& es, dependency*& dep) {
bool theory_seq::simplify_and_solve_eqs() {
context & ctx = get_context();
m_new_propagation = false;
m_new_solution = true;
while (m_new_solution && !ctx.inconsistent()) {
m_new_solution = false;
@ -2639,6 +2637,7 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
else if (m_util.str.is_itos(e, e1)) {
rational val;
if (get_value(e1, val)) {
TRACE("seq", tout << mk_pp(e, m) << " -> " << val << "\n";);
expr_ref num(m), res(m);
num = m_autil.mk_numeral(val, true);
if (!ctx.e_internalized(num)) {
@ -2652,6 +2651,7 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(n1, n2)));
}
else {
TRACE("seq", tout << "add axiom\n";);
add_axiom(~mk_eq(num, e1, false), mk_eq(e, res, false));
add_axiom(mk_eq(num, e1, false), ~mk_eq(e, res, false));
result = e;