mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix build errors on ubuntu and gcc

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-05-01 02:35:57 -07:00
parent 5098089ee1
commit 7cb9e7381d
13 changed files with 38 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/muz_qe/dl_rule.cpp
View file

@ -85,8 +85,6 @@ namespace datalog {
return BR_FAILED;
}
template class rewriter_tpl<rule_manager::remove_label_cfg>;
void rule_manager::remove_labels(expr_ref& fml, proof_ref& pr) {
expr_ref tmp(m);
@ -1121,3 +1119,5 @@ namespace datalog {
};
template class rewriter_tpl<datalog::rule_manager::remove_label_cfg>;

1
src/muz_qe/fixedpoint_params.pyg
View file

@ -60,6 +60,7 @@ def_module_params('fixedpoint',
('print_answer', BOOL, False, 'print answer instance(s) to query'),
('print_certificate', BOOL, False, 'print certificate for reachability or non-reachability'),
('print_statistics', BOOL, False, 'print statistics'),
('use_utvpi', BOOL, False, 'experimental use UTVPI strategy'),
('tab_selection', SYMBOL, 'weight', 'selection method for tabular strategy: weight (default), first, var-use'),
))

1
src/muz_qe/hnf.cpp
View file

@ -186,6 +186,7 @@ private:
void mk_horn(expr_ref& fml, proof_ref& premise) {
SASSERT(!premise || fml == m.get_fact(premise));
expr* e1, *e2;
expr_ref fml0(m), fml1(m), fml2(m), head(m);
proof_ref p(m);

16
src/muz_qe/pdr_context.cpp
View file

@ -1441,11 +1441,7 @@ namespace pdr {
}
}
m_is_dl = is_difference_logic(m, forms.size(), forms.c_ptr());
#if 0
if (!m_is_dl) {
m_is_utvpi = is_utvpi_logic(m, forms.size(), forms.c_ptr());
}
#endif
m_is_utvpi = m_is_dl || is_utvpi_logic(m, forms.size(), forms.c_ptr());
}
}
@ -1565,15 +1561,15 @@ namespace pdr {
m_fparams.m_arith_auto_config_simplex = true;
m_fparams.m_arith_propagate_eqs = false;
m_fparams.m_arith_eager_eq_axioms = false;
if (classify.is_dl()) {
m_fparams.m_arith_mode = AS_DIFF_LOGIC;
m_fparams.m_arith_expand_eqs = true;
}
else if (classify.is_utvpi()) {
if (classify.is_utvpi() && m_params.use_utvpi()) {
IF_VERBOSE(1, verbose_stream() << "UTVPI\n";);
m_fparams.m_arith_mode = AS_UTVPI;
m_fparams.m_arith_expand_eqs = true;
}
else if (classify.is_dl()) {
m_fparams.m_arith_mode = AS_DIFF_LOGIC;
m_fparams.m_arith_expand_eqs = true;
}
}
if (!use_mc && m_params.use_inductive_generalizer()) {
m_core_generalizers.push_back(alloc(core_bool_inductive_generalizer, *this, 0));

2
src/muz_qe/pdr_prop_solver.cpp
View file

@ -391,7 +391,7 @@ namespace pdr {
!is_utvpi_logic(m, lemmas.size(), lemmas.c_ptr()));
if (outside_of_logic) {
IF_VERBOSE(1,
IF_VERBOSE(2,
verbose_stream() << "not diff\n";
for (unsigned i = 0; i < lemmas.size(); ++i) {
verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n";

6
src/muz_qe/pdr_util.cpp
View file

@ -1248,7 +1248,11 @@ namespace pdr {
}
if (!m_is_dl) {
IF_VERBOSE(1, verbose_stream() << "non-diff: " << mk_pp(e, m) << "\n";);
char const* msg = "non-diff: ";
if (m_test_for_utvpi) {
msg = "non-utvpi: ";
}
IF_VERBOSE(1, verbose_stream() << msg << mk_pp(e, m) << "\n";);
}
}

7
src/smt/diff_logic.h
View file

@ -264,13 +264,6 @@ class dl_graph {
m_assignment[e.get_target()] - m_assignment[e.get_source()] <= e.get_weight();
}
bool is_tight(edge_id e) const {
edge const& edge = m_edges[e];
return edge.is_enabled() &&
m_assignment[edge.get_target()] - m_assignment[e.get_source()] == e.get_weight();
}
public:
// An assignment is feasible if all edges are feasible.
bool is_feasible() const {

3
src/smt/theory_diff_logic.h
View file

@ -46,7 +46,6 @@ namespace smt {
unsigned m_num_conflicts;
unsigned m_num_assertions;
unsigned m_num_th2core_eqs;
unsigned m_num_th2core_prop;
unsigned m_num_core2th_eqs;
unsigned m_num_core2th_diseqs;
@ -260,7 +259,7 @@ namespace smt {
m_arith_eq_adapter.restart_eh();
}
virtual void relevant_eh(app* e);
virtual void relevant_eh(app* e) {}
virtual void init_search_eh() {
m_arith_eq_adapter.init_search_eh();

7
src/smt/theory_diff_logic_def.h
View file

@ -310,9 +310,9 @@ void theory_diff_logic<Ext>::assign_eh(bool_var v, bool is_true) {
template<typename Ext>
void theory_diff_logic<Ext>::collect_statistics(::statistics & st) const {
st.update("dl conflicts", m_stats.m_num_conflicts);
st.update("dl propagations", m_stats.m_num_th2core_prop);
st.update("dl asserts", m_stats.m_num_assertions);
st.update("core->dl eqs", m_stats.m_num_core2th_eqs);
st.update("core->dl diseqs", m_stats.m_num_core2th_diseqs);
m_arith_eq_adapter.collect_statistics(st);
m_graph.collect_statistics(st);
}
@ -598,7 +598,6 @@ void theory_diff_logic<Ext>::set_neg_cycle_conflict() {
literal_vector const& lits = m_nc_functor.get_lits();
context & ctx = get_context();
TRACE("arith_conflict",
//display(tout);
tout << "conflict: ";
for (unsigned i = 0; i < lits.size(); ++i) {
ctx.display_literal_info(tout, lits[i]);
@ -971,10 +970,6 @@ void theory_diff_logic<Ext>::new_diseq_eh(theory_var v1, theory_var v2) {
}
template<typename Ext>
void theory_diff_logic<Ext>::relevant_eh(app* e) {
}
struct imp_functor {
conflict_resolution & m_cr;

1
src/smt/theory_horn_ineq.h
View file

@ -85,6 +85,7 @@ namespace smt {
class theory_horn_ineq : public theory, private Ext {
typedef typename Ext::numeral numeral;
typedef typename Ext::inf_numeral inf_numeral;
typedef literal explanation;
typedef theory_var th_var;
typedef svector<th_var> th_var_vector;

12
src/smt/theory_horn_ineq_def.h
View file

@ -797,10 +797,10 @@ namespace smt {
template<typename Ext>
typename theory_horn_ineq<Ext>::numeral theory_horn_ineq<Ext>::mk_weight(bool is_real, bool is_strict, rational const& w) const {
if (is_strict) {
return numeral(Ext::inf_numeral(w)) + (is_real?Ext::m_epsilon:numeral(1));
return numeral(inf_numeral(w)) + (is_real?Ext::m_epsilon:numeral(1));
}
else {
return numeral(Ext::inf_numeral(w));
return numeral(inf_numeral(w));
}
}
@ -1001,9 +1001,9 @@ namespace smt {
th_var target = mk_var(ctx.mk_enode(n, false, false, true));
coeffs.push_back(std::make_pair(target, rational(-1)));
VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(Ext::inf_numeral(w)), null_literal)));
VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(w)), null_literal)));
negate(coeffs, w);
VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(Ext::inf_numeral(w)), null_literal)));
VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(w)), null_literal)));
return target;
}
@ -1024,9 +1024,9 @@ namespace smt {
// v = k: v <= k k <= v
coeffs coeffs;
coeffs.push_back(std::make_pair(v, rational(1)));
VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(Ext::inf_numeral(r)), null_literal)));
VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(r)), null_literal)));
coeffs.back().second.neg();
VERIFY (m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(Ext::inf_numeral(-r)), null_literal)));
VERIFY (m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(-r)), null_literal)));
}
return v;
}

5
src/smt/theory_utvpi.h
View file

@ -201,6 +201,7 @@ namespace smt {
virtual void assign_eh(bool_var v, bool is_true);
virtual void new_eq_eh(th_var v1, th_var v2) {
m_stats.m_num_core2th_eqs++;
m_arith_eq_adapter.new_eq_eh(v1, v2);
}
@ -322,10 +323,6 @@ namespace smt {
return v | 0x1;
}
th_var not(th_var v) const {
return v ^ 0x1;
}
};

16
src/smt/theory_utvpi_def.h
View file

@ -264,7 +264,7 @@ namespace smt {
template<typename Ext>
typename theory_utvpi<Ext>::numeral theory_utvpi<Ext>::mk_weight(bool is_real, bool is_strict, rational const& w) const {
if (is_strict) {
return numeral(w) + (is_real?m_epsilon:numeral(1));
return numeral(w) + (is_real?Ext::m_epsilon:numeral(1));
}
else {
return numeral(w);
@ -435,6 +435,7 @@ namespace smt {
m_nc_functor.reset();
VERIFY(m_graph.find_shortest_zero_edge_path(v1, v2, UINT_MAX, m_nc_functor));
VERIFY(m_graph.find_shortest_zero_edge_path(v2, v1, UINT_MAX, m_nc_functor));
IF_VERBOSE(1, verbose_stream() << "parity conflict " << mk_pp(e->get_owner(), get_manager()) << "\n";);
set_conflict();
return false;
@ -453,7 +454,9 @@ namespace smt {
template<typename Ext>
void theory_utvpi<Ext>::collect_statistics(::statistics& st) const {
st.update("utvpi conflicts", m_stats.m_num_conflicts);
st.update("utvpi assignments", m_stats.m_num_assertions);
st.update("utvpi asserts", m_stats.m_num_assertions);
st.update("core->utvpi eqs", m_stats.m_num_core2th_eqs);
st.update("core->utvpi diseqs", m_stats.m_num_core2th_diseqs);
m_arith_eq_adapter.collect_statistics(st);
m_graph.collect_statistics(st);
}
@ -669,6 +672,9 @@ namespace smt {
unsigned sz = m_atoms.size();
for (unsigned i = 0; i < sz; ++i) {
bool_var b = m_atoms[i].get_bool_var();
if (!ctx.is_relevant(b)) {
continue;
}
bool ok = true;
expr* e = ctx.bool_var2expr(b);
switch(ctx.get_assignment(b)) {
@ -681,7 +687,9 @@ namespace smt {
default:
break;
}
CTRACE("utvpi", !ok, tout << "validation failed: " << mk_pp(e, get_manager()) << "\n";);
CTRACE("utvpi", !ok, tout << "validation failed: " << mk_pp(e, get_manager()) << "\n";);
// CTRACE("utvpi", ok, tout << "validation success: " << mk_pp(e, get_manager()) << "\n";);
SASSERT(ok);
}
}
@ -748,6 +756,7 @@ namespace smt {
numeral val = val1 - val2;
rational num = val.get_rational() + (m_delta * val.get_infinitesimal().to_rational());
num = num/rational(2);
num = floor(num);
return num;
}
@ -755,7 +764,6 @@ namespace smt {
model_value_proc * theory_utvpi<Ext>::mk_value(enode * n, model_generator & mg) {
theory_var v = n->get_th_var(get_id());
rational num = mk_value(v);
num = ceil(num);
TRACE("utvpi", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";);
return alloc(expr_wrapper_proc, m_factory->mk_value(num, a.is_int(n->get_owner())));
}