mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 19:53:34 +00:00
Code Activity

enable neat vs. less neat pretty priting as an option

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-09 16:25:41 -07:00
parent f7e1ad5277
commit f151879c0b
9 changed files with 98 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/python/z3printer.py
View file

@ -842,6 +842,8 @@ class Formatter:
return self.pp_seq(a.assertions(), 0, [])
elif isinstance(a, z3.Fixedpoint):
return a.sexpr()
elif isinstance(a, z3.Optimize):
return a.sexpr()
elif isinstance(a, z3.ApplyResult):
return self.pp_seq_seq(a, 0, [])
elif isinstance(a, z3.ModelRef):

9
src/opt/opt_context.cpp
View file

@ -38,6 +38,7 @@ Notes:
#include "inc_sat_solver.h"
#include "bv_decl_plugin.h"
#include "pb_decl_plugin.h"
#include "ast_smt_pp.h"
namespace opt {
@ -122,7 +123,8 @@ namespace opt {
m_fm(m),
m_objective_refs(m),
m_enable_sat(false),
m_enable_sls(false)
m_enable_sls(false),
m_pp_neat(false)
{
params_ref p;
p.set_bool("model", true);
@ -1063,6 +1065,7 @@ namespace opt {
m_enable_sat = _p.enable_sat();
m_enable_sls = _p.enable_sls();
m_maxsat_engine = _p.maxsat_engine();
m_pp_neat = _p.pp_neat();
}
typedef obj_hashtable<func_decl> func_decl_set;
@ -1095,9 +1098,11 @@ namespace opt {
std::string context::to_string() const {
smt2_pp_environment_dbg env(m);
ast_smt_pp ll_smt2_pp(m);
free_func_visitor visitor(m);
std::ostringstream out;
#define PP(_e_) ast_smt2_pp(out, _e_, env);
#define PPE(_e_) if (m_pp_neat) ast_smt2_pp(out, _e_, env); else ll_smt2_pp.display_expr_smt2(out, _e_);
for (unsigned i = 0; i < m_scoped_state.m_hard.size(); ++i) {
visitor.collect(m_scoped_state.m_hard[i]);
}
@ -1132,7 +1137,7 @@ namespace opt {
}
for (unsigned i = 0; i < m_scoped_state.m_hard.size(); ++i) {
out << "(assert ";
PP(m_scoped_state.m_hard[i]);
PPE(m_scoped_state.m_hard[i]);
out << ")\n";
}
for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) {

1
src/opt/opt_context.h
View file

@ -127,6 +127,7 @@ namespace opt {
tactic_ref m_simplify;
bool m_enable_sat;
bool m_enable_sls;
bool m_pp_neat;
symbol m_maxsat_engine;
symbol m_logic;
public:

1
src/opt/opt_params.pyg
View file

@ -10,6 +10,7 @@ def_module_params('opt',
('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'),
('enable_sat', BOOL, False, 'enable the new SAT core for propositional constraints'),
('elim_01', BOOL, True, 'eliminate 01 variables'),
('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'),
('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)'),
('maxres.hill_climb', BOOL, True, 'give preference for large weight cores'),
('maxres.add_upper_bound_block', BOOL, False, 'restict upper bound with constraint'),

2
src/smt/smt_internalizer.cpp
View file

@ -814,7 +814,7 @@ namespace smt {
*/
bool_var context::mk_bool_var(expr * n) {
SASSERT(!b_internalized(n));
SASSERT(!m_manager.is_not(n));
//SASSERT(!m_manager.is_not(n));
unsigned id = n->get_id();
bool_var v = m_b_internalized_stack.size();
#ifndef _EXTERNAL_RELEASE

14
src/smt/smt_setup.cpp
View file

@ -411,6 +411,15 @@ namespace smt {
return;
}
}
#if 0
switch (m_params.m_arith_mode) {
case AS_DIFF_LOGIC:
case AS_DENSE_DIFF_LOGIC:
case AS_UTVPI:
setup_arith();
return;
}
#endif
m_params.m_arith_eq_bounds = true;
m_params.m_phase_selection = PS_ALWAYS_FALSE;
m_params.m_restart_strategy = RS_GEOMETRIC;
@ -420,7 +429,7 @@ namespace smt {
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
}
// else if (st.m_arith_k_sum < rational(INT_MAX / 8))
// m_context.register_plugin(alloc(smt::theory_si_arith, m_manager, m_params));
// m_context.register_plugin(alloc(smt::theory_dense_si, m_manager, m_params));
else
m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
}
@ -703,6 +712,7 @@ namespace smt {
m_context.register_plugin(alloc(smt::theory_dummy, m_manager.mk_family_id("arith"), "no arithmetic"));
break;
case AS_DIFF_LOGIC:
m_params.m_arith_expand_eqs = true;
if (m_params.m_arith_fixnum) {
if (m_params.m_arith_int_only)
m_context.register_plugin(alloc(smt::theory_fidl, m_manager, m_params));
@ -717,6 +727,7 @@ namespace smt {
}
break;
case AS_DENSE_DIFF_LOGIC:
m_params.m_arith_expand_eqs = true;
if (m_params.m_arith_fixnum) {
if (m_params.m_arith_int_only)
m_context.register_plugin(alloc(smt::theory_dense_si, m_manager, m_params));
@ -731,6 +742,7 @@ namespace smt {
}
break;
case AS_UTVPI:
m_params.m_arith_expand_eqs = true;
if (m_params.m_arith_int_only)
m_context.register_plugin(alloc(smt::theory_iutvpi, m_manager));
else

9
src/smt/theory_arith.h
View file

@ -578,10 +578,15 @@ namespace smt {
void flush_bound_axioms();
typename atoms::iterator next_sup(atom* a1, atom_kind kind,
typename atoms::iterator it,
typename atoms::iterator end);
typename atoms::iterator end,
bool& found_compatible);
typename atoms::iterator next_inf(atom* a1, atom_kind kind,
typename atoms::iterator it,
typename atoms::iterator end);
typename atoms::iterator end,
bool& found_compatible);
typename atoms::iterator first(atom_kind kind,
typename atoms::iterator it,
typename atoms::iterator end);
struct compare_atoms {
bool operator()(atom* a1, atom* a2) const { return a1->get_k() < a2->get_k(); }
};

73
src/smt/theory_arith_core.h
View file

@ -810,6 +810,8 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::mk_bound_axioms(atom * a1) {
theory_var v = a1->get_var();
atoms & occs = m_var_occs[v];
if (!get_context().is_searching()) {
//
// NB. We make an assumption that user push calls propagation
@ -819,11 +821,9 @@ namespace smt {
m_new_atoms.push_back(a1);
return;
}
theory_var v = a1->get_var();
inf_numeral const & k1(a1->get_k());
atom_kind kind1 = a1->get_atom_kind();
TRACE("mk_bound_axioms", tout << "making bound axioms for v" << v << " " << kind1 << " " << k1 << "\n";);
atoms & occs = m_var_occs[v];
typename atoms::iterator it = occs.begin();
typename atoms::iterator end = occs.end();
@ -874,6 +874,9 @@ namespace smt {
parameter coeffs[3] = { parameter(symbol("farkas")),
parameter(rational(1)), parameter(rational(1)) };
//std::cout << "v" << v << " " << ((kind1==A_LOWER)?"<= ":">= ") << k1 << "\t ";
//std::cout << "v" << v << " " << ((kind2==A_LOWER)?"<= ":">= ") << k2 << "\n";
if (kind1 == A_LOWER) {
if (kind2 == A_LOWER) {
if (k2 <= k1) {
@ -944,39 +947,74 @@ namespace smt {
std::sort(atoms.begin(), atoms.end(), compare_atoms());
std::sort(occs.begin(), occs.end(), compare_atoms());
typename atoms::iterator begin = occs.begin();
typename atoms::iterator begin1 = occs.begin();
typename atoms::iterator begin2 = occs.begin();
typename atoms::iterator end = occs.end();
typename atoms::iterator lo_inf = begin, lo_sup = begin;
typename atoms::iterator hi_inf = begin, hi_sup = begin;
begin1 = first(A_LOWER, begin1, end);
begin2 = first(A_UPPER, begin2, end);
typename atoms::iterator lo_inf = begin1, lo_sup = begin1;
typename atoms::iterator hi_inf = begin2, hi_sup = begin2;
typename atoms::iterator lo_inf1 = begin1, lo_sup1 = begin1;
typename atoms::iterator hi_inf1 = begin2, hi_sup1 = begin2;
bool flo_inf, fhi_inf, flo_sup, fhi_sup;
//std::cout << atoms.size() << "\n";
ptr_addr_hashtable<typename atom> visited;
for (unsigned i = 0; i < atoms.size(); ++i) {
atom* a1 = atoms[i];
lo_inf = next_inf(a1, A_LOWER, lo_inf, end);
hi_inf = next_inf(a1, A_UPPER, hi_inf, end);
lo_sup = next_sup(a1, A_LOWER, lo_sup, end);
hi_sup = next_sup(a1, A_UPPER, hi_sup, end);
if (lo_inf != end) mk_bound_axiom(a1, *lo_inf);
if (lo_sup != end) mk_bound_axiom(a1, *lo_sup);
if (hi_inf != end) mk_bound_axiom(a1, *hi_inf);
if (hi_sup != end) mk_bound_axiom(a1, *hi_sup);
lo_inf1 = next_inf(a1, A_LOWER, lo_inf, end, flo_inf);
hi_inf1 = next_inf(a1, A_UPPER, hi_inf, end, fhi_inf);
lo_sup1 = next_sup(a1, A_LOWER, lo_sup, end, flo_sup);
hi_sup1 = next_sup(a1, A_UPPER, hi_sup, end, fhi_sup);
//std::cout << "v" << a1->get_var() << ((a1->get_atom_kind()==A_LOWER)?" <= ":" >= ") << a1->get_k() << "\n";
//std::cout << (lo_inf1 != end) << " " << (lo_sup1 != end) << " " << (hi_inf1 != end) << " " << (hi_sup1 != end) << "\n";
if (lo_inf1 != end) lo_inf = lo_inf1;
if (lo_sup1 != end) lo_sup = lo_sup1;
if (hi_inf1 != end) hi_inf = hi_inf1;
if (hi_sup1 != end) hi_sup = hi_sup1;
if (!flo_inf) lo_inf = end;
if (!fhi_inf) hi_inf = end;
if (!flo_sup) lo_sup = end;
if (!fhi_sup) hi_sup = end;
visited.insert(a1);
if (lo_inf1 != end && lo_inf != end && !visited.contains(*lo_inf)) mk_bound_axiom(a1, *lo_inf);
if (lo_sup1 != end && lo_sup != end && !visited.contains(*lo_sup)) mk_bound_axiom(a1, *lo_sup);
if (hi_inf1 != end && hi_inf != end && !visited.contains(*hi_inf)) mk_bound_axiom(a1, *hi_inf);
if (hi_sup1 != end && hi_sup != end && !visited.contains(*hi_sup)) mk_bound_axiom(a1, *hi_sup);
}
}
}
template<typename Ext>
typename theory_arith<Ext>::atoms::iterator
theory_arith<Ext>::first(
atom_kind kind,
typename atoms::iterator it,
typename atoms::iterator end) {
for (; it != end; ++it) {
atom* a = *it;
if (a->get_atom_kind() == kind) return it;
}
return end;
}
template<typename Ext>
typename theory_arith<Ext>::atoms::iterator
theory_arith<Ext>::next_inf(
atom* a1,
atom_kind kind,
typename atoms::iterator it,
typename atoms::iterator end) {
typename atoms::iterator end,
bool& found_compatible) {
inf_numeral const & k1(a1->get_k());
typename atoms::iterator result = end;
found_compatible = false;
for (; it != end; ++it) {
atom * a2 = *it;
if (a1 == a2) continue;
if (a2->get_atom_kind() != kind) continue;
inf_numeral const & k2(a2->get_k());
found_compatible = true;
if (k2 <= k1) {
result = it;
}
@ -993,14 +1031,17 @@ namespace smt {
atom* a1,
atom_kind kind,
typename atoms::iterator it,
typename atoms::iterator end) {
typename atoms::iterator end,
bool& found_compatible) {
inf_numeral const & k1(a1->get_k());
found_compatible = false;
for (; it != end; ++it) {
atom * a2 = *it;
if (a1 == a2) continue;
if (a2->get_atom_kind() != kind) continue;
inf_numeral const & k2(a2->get_k());
if (k2 > k1) {
found_compatible = true;
if (k1 < k2) {
return it;
}
}

9
src/smt/theory_diff_logic_def.h
View file

@ -722,6 +722,7 @@ theory_var theory_diff_logic<Ext>::mk_term(app* n) {
app* a, *offset;
theory_var source, target;
enode* e;
context& ctx = get_context();
TRACE("arith", tout << mk_pp(n, get_manager()) << "\n";);
@ -732,6 +733,13 @@ theory_var theory_diff_logic<Ext>::mk_term(app* n) {
else if (is_offset(n, a, offset, r)) {
// n = a + k
source = mk_var(a);
for (unsigned i = 0; i < n->get_num_args(); ++i) {
expr* arg = n->get_arg(i);
std::cout << "internalize: " << mk_pp(arg, get_manager()) << " " << ctx.e_internalized(arg) << "\n";
if (!ctx.e_internalized(arg)) {
ctx.internalize(arg, false);
}
}
e = get_context().mk_enode(n, false, false, true);
target = mk_var(e);
numeral k(r);
@ -779,6 +787,7 @@ theory_var theory_diff_logic<Ext>::mk_num(app* n, rational const& r) {
}
else {
theory_var zero = get_zero();
SASSERT(n->get_num_args() == 0);
e = ctx.mk_enode(n, false, false, true);
v = mk_var(e);
// internalizer is marking enodes as interpreted whenever the associated ast is a value and a constant.