mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-18 21:40:27 +00:00
Code Activity

trying new build infrastructure on linux

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-23 13:10:41 -07:00
parent efff6db567
commit 1d795e9a5e
9 changed files with 41 additions and 72 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/muz_qe/pdr_context.cpp
View file

@ -712,14 +712,14 @@ namespace pdr {
pred_transformer& p = pt();
ast_manager& m = p.get_manager();
manager& pm = p.get_pdr_manager();
TRACE("pdr", model_v2_pp(tout, model()););
TRACE("pdr", model_v2_pp(tout, get_model()););
func_decl* f = p.head();
unsigned arity = f->get_arity();
expr_ref_vector args(m);
func_decl_ref v(m);
for (unsigned i = 0; i < arity; ++i) {
v = pm.o2n(p.sig(i),0);
expr* e = model().get_const_interp(v);
expr* e = get_model().get_const_interp(v);
if (e) {
args.push_back(e);
}

2
src/muz_qe/pdr_context.h
View file

@ -196,7 +196,7 @@ namespace pdr {
pred_transformer& pt() const { return m_pt; }
model_node* parent() const { return m_parent; }
model* model_ptr() const { return m_model.get(); }
model const& model() const { return *m_model; }
model const& get_model() const { return *m_model; }
unsigned index() const;
bool is_closed() const { return m_closed; }

4
src/muz_qe/pdr_quantifiers.cpp
View file

@ -418,10 +418,10 @@ namespace pdr {
// nodes from leaves that are repeated
// inside the search tree don't have models.
//
if (!(&node.model())) {
if (!(&node.get_model())) {
return;
}
m_current_rule = &pt.find_rule(node.model());
m_current_rule = &pt.find_rule(node.get_model());
m_current_pt = &pt;
m_current_node = &node;
if (!m_current_rule) {

8
src/muz_qe/pdr_util.cpp
View file

@ -908,9 +908,6 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
m_cfg(m, p) {}
};
template class rewriter_tpl<ite_hoister_cfg>;
void hoist_non_bool_if(expr_ref& fml) {
ast_manager& m = fml.get_manager();
datalog::scoped_no_proof _sp(m);
@ -1039,3 +1036,8 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
}
}
template class rewriter_tpl<pdr::ite_hoister_cfg>;

2
src/muz_qe/qe_lite.cpp
View file

@ -498,7 +498,7 @@ public:
unsigned j = 0;
for (unsigned i = 0; i < vars.size(); ++i) {
if (used.contains(vars.size()-i-1)) {
vars[j] = vars[i];
vars.set(j, vars.get(i));
++j;
}
}