mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-25 01:55:32 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-03-09 21:33:16 -08:00
commit 2354e747bf
10 changed files with 166 additions and 110 deletions
Download patch file Download diff file Expand all files Collapse all files

97
src/tactic/core/collect_occs.cpp Normal file
View file

@ -0,0 +1,97 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
collect_cccs.cpp
Abstract:
Collect variables by occurrences.
Author:
Leonardo (leonardo) 2011-10-22
Notes:
--*/
#include "ast.h"
#include "goal.h"
#include "hashtable.h"
#include "collect_occs.h"
bool collect_occs::visit(expr * t) {
if (m_visited.is_marked(t)) {
if (is_uninterp_const(t))
m_more_than_once.mark(t);
return true;
}
m_visited.mark(t);
if (is_uninterp_const(t)) {
m_vars.push_back(to_app(t));
return true;
}
if (is_var(t))
return true;
if (is_app(t) && to_app(t)->get_num_args() == 0)
return true;
m_stack.push_back(frame(t, 0));
return false;
}
void collect_occs::process(expr * t) {
SASSERT(m_stack.empty());
if (visit(t))
return;
SASSERT(!m_stack.empty());
unsigned num;
expr * child;
while (!m_stack.empty()) {
start:
frame & fr = m_stack.back();
expr * t = fr.first;
switch (t->get_kind()) {
case AST_APP:
num = to_app(t)->get_num_args();
while (fr.second < num) {
child = to_app(t)->get_arg(fr.second);
fr.second++;
if (!visit(child))
goto start;
}
m_stack.pop_back();
break;
case AST_QUANTIFIER:
// don't need to visit patterns
child = to_quantifier(t)->get_expr();
fr.second++;
if (!visit(child))
goto start;
m_stack.pop_back();
break;
default:
UNREACHABLE();
}
}
}
void collect_occs::operator()(goal const & g, obj_hashtable<expr> & r) {
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++) {
expr * t = g.form(i);
process(t);
}
ptr_vector<app>::const_iterator it = m_vars.begin();
ptr_vector<app>::const_iterator end = m_vars.end();
for (; it != end; ++it) {
if (m_more_than_once.is_marked(*it))
continue;
r.insert(*it);
}
m_visited.reset();
m_more_than_once.reset();
}

38
src/tactic/core/collect_occs.h Normal file
View file

@ -0,0 +1,38 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
collect_cccs.h
Abstract:
Collect variables by occurrences.
Author:
Leonardo (leonardo) 2011-10-22
Notes:
--*/
#ifndef COLLECT_OCCS_H_
#define COLLECT_OCCS_H_
class collect_occs {
expr_fast_mark1 m_visited;
expr_fast_mark2 m_more_than_once;
typedef std::pair<expr *, unsigned> frame;
svector<frame> m_stack;
ptr_vector<app> m_vars;
bool visit(expr * t);
void process(expr * t);
public:
void operator()(goal const & g, obj_hashtable<expr> & r);
};
#endif

85
src/tactic/core/elim_uncnstr_tactic.cpp
View file

@ -24,6 +24,7 @@ Notes:
#include"bv_decl_plugin.h"
#include"array_decl_plugin.h"
#include"datatype_decl_plugin.h"
#include"collect_occs.h"
#include"cooperate.h"
#include"ast_smt2_pp.h"
#include"ast_ll_pp.h"
@ -32,86 +33,6 @@ class elim_uncnstr_tactic : public tactic {
struct imp {
// unconstrained vars collector
struct collect {
expr_fast_mark1 m_visited;
expr_fast_mark2 m_more_than_once;
typedef std::pair<expr *, unsigned> frame;
svector<frame> m_stack;
ptr_vector<app> m_vars;
bool visit(expr * t) {
if (m_visited.is_marked(t)) {
if (is_uninterp_const(t))
m_more_than_once.mark(t);
return true;
}
m_visited.mark(t);
if (is_uninterp_const(t)) {
m_vars.push_back(to_app(t));
return true;
}
if (is_var(t))
return true;
if (is_app(t) && to_app(t)->get_num_args() == 0)
return true;
m_stack.push_back(frame(t, 0));
return false;
}
void process(expr * t) {
SASSERT(m_stack.empty());
if (visit(t))
return;
SASSERT(!m_stack.empty());
unsigned num;
expr * child;
while (!m_stack.empty()) {
start:
frame & fr = m_stack.back();
expr * t = fr.first;
switch (t->get_kind()) {
case AST_APP:
num = to_app(t)->get_num_args();
while (fr.second < num) {
child = to_app(t)->get_arg(fr.second);
fr.second++;
if (!visit(child))
goto start;
}
m_stack.pop_back();
break;
case AST_QUANTIFIER:
// don't need to visit patterns
child = to_quantifier(t)->get_expr();
fr.second++;
if (!visit(child))
goto start;
m_stack.pop_back();
break;
default:
UNREACHABLE();
}
}
}
void operator()(goal const & g, obj_hashtable<expr> & r) {
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++) {
expr * t = g.form(i);
process(t);
}
ptr_vector<app>::const_iterator it = m_vars.begin();
ptr_vector<app>::const_iterator end = m_vars.end();
for (; it != end; ++it) {
if (m_more_than_once.is_marked(*it))
continue;
r.insert(*it);
}
m_visited.reset();
m_more_than_once.reset();
}
};
typedef extension_model_converter mc;
@ -910,7 +831,7 @@ class elim_uncnstr_tactic : public tactic {
TRACE("elim_uncnstr_bug", g->display(tout););
tactic_report report("elim-uncnstr-vars", *g);
m_vars.reset();
collect p;
collect_occs p;
p(*g, m_vars);
if (m_vars.empty()) {
result.push_back(g.get());
@ -977,7 +898,7 @@ class elim_uncnstr_tactic : public tactic {
m_rw->reset(); // reset cache
m_vars.reset();
{
collect p;
collect_occs p;
p(*g, m_vars);
}
if (m_vars.empty())

24
src/tactic/smtlogics/qfbv_tactic.cpp
View file

@ -35,9 +35,9 @@ Notes:
tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
params_ref solve_eq_p;
// conservative guassian elimination.
solve_eq_p.set_uint("solve_eqs_max_occs", 2);
// conservative guassian elimination.
solve_eq_p.set_uint("solve_eqs_max_occs", 2);
params_ref simp2_p = p;
simp2_p.set_bool("som", true);
simp2_p.set_bool("pull_cheap_ite", true);
@ -61,13 +61,13 @@ tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
using_params(mk_simplify_tactic(m), simp2_p),
//
// Z3 can solve a couple of extra benchmarks by using hoist_mul
// but the timeout in SMT-COMP is too small.
// but the timeout in SMT-COMP is too small.
// Moreover, it impacted negatively some easy benchmarks.
// We should decide later, if we keep it or not.
//
using_params(mk_simplify_tactic(m), hoist_p),
mk_max_bv_sharing_tactic(m),
mk_ackermannize_bv_tactic(m,p)
if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_tactic(m,p)))
);
}
@ -80,14 +80,14 @@ static tactic * main_p(tactic* t) {
}
tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tactic* smt) {
tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tactic* smt) {
params_ref local_ctx_p = p;
local_ctx_p.set_bool("local_ctx", true);
params_ref solver_p;
solver_p.set_bool("preprocess", false); // preprocessor of smt::context is not needed.
params_ref no_flat_p;
no_flat_p.set_bool("flat", false);
@ -98,7 +98,7 @@ tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tacti
params_ref big_aig_p;
big_aig_p.set_bool("aig_per_assertion", false);
tactic* preamble_st = mk_qfbv_preamble(m, p);
tactic * st = main_p(and_then(preamble_st,
// If the user sets HI_DIV0=false, then the formula may contain uninterpreted function
@ -119,10 +119,10 @@ tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tacti
big_aig_p))))),
sat),
smt))));
st->updt_params(p);
return st;
}
@ -131,9 +131,7 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
tactic * new_sat = cond(mk_produce_proofs_probe(),
and_then(mk_simplify_tactic(m), mk_smt_tactic()),
mk_sat_tactic(m));
return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic());
}