mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

Merge branch 'theory-assumptions' into develop

Browse source 
Conflicts:
	src/smt/smt_context.cpp
	src/smt/smt_context.h
	src/smt/smt_theory.h
This commit is contained in:
Murphy Berzish 2017-04-22 13:31:43 -04:00
commit 06cd07e3c2
53 changed files with 1712 additions and 929 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/smt/old_interval.cpp
View file

@ -81,7 +81,7 @@ ext_numeral & ext_numeral::operator*=(ext_numeral const & other) {
m_value.reset();
return *this;
}
if (is_infinite() || other.is_infinite()) {
if (sign() == other.sign())
m_kind = PLUS_INFINITY;
@ -203,7 +203,7 @@ interval::interval(v_dependency_manager & m, rational const & val, v_dependency
m_lower_dep(l_dep),
m_upper_dep(u_dep) {
}
/**
\brief Create intervals (-oo, val], (-oo, val), [val, oo), (val, oo)
*/
@ -271,8 +271,8 @@ interval & interval::operator-=(interval const & other) {
return operator+=(tmp);
}
v_dependency * interval::join(v_dependency * d1, v_dependency * d2, v_dependency * d3, v_dependency * d4) {
return m_manager.mk_join(m_manager.mk_join(d1, d2), m_manager.mk_join(d3,d4));
v_dependency * interval::join(v_dependency * d1, v_dependency * d2, v_dependency * d3, v_dependency * d4) {
return m_manager.mk_join(m_manager.mk_join(d1, d2), m_manager.mk_join(d3,d4));
}
/**
@ -318,7 +318,7 @@ interval & interval::operator*=(interval const & other) {
v_dependency * d_d = other.m_upper_dep;
TRACE("interval_bug", tout << "operator*= " << *this << " " << other << "\n";);
if (is_N()) {
if (other.is_N()) {
// x <= b <= 0, y <= d <= 0 --> b*d <= x*y
@ -452,7 +452,7 @@ interval & interval::operator*=(interval const & other) {
m_upper_dep = m_upper.is_infinite() ? 0 : join(b_d, d_d, a_d);
}
else {
// 0 <= a <= x, 0 <= c <= y --> a*c <= x*y
// 0 <= a <= x, 0 <= c <= y --> a*c <= x*y
// x <= b, y <= d --> x*y <= b*d (uses the fact that x is pos (a is not negative) or y is pos (c is not negative))
TRACE("interval_bug", tout << "(P, P)\n";);
SASSERT(other.is_P());
@ -467,7 +467,7 @@ interval & interval::operator*=(interval const & other) {
}
}
TRACE("interval_bug", tout << "operator*= result: " << *this << "\n";);
CTRACE("interval", !(!(contains_zero1 || contains_zero2) || contains_zero()),
CTRACE("interval", !(!(contains_zero1 || contains_zero2) || contains_zero()),
tout << "contains_zero1: " << contains_zero1 << ", contains_zero2: " << contains_zero2 << ", contains_zero(): " << contains_zero() << "\n";);
SASSERT(!(contains_zero1 || contains_zero2) || contains_zero());
return *this;
@ -482,7 +482,7 @@ bool interval::contains_zero() const {
tout << "m_upper.is_zero: " << m_upper.is_zero() << "\n";
tout << "m_upper_open: " << m_upper_open << "\n";
tout << "result: " << ((m_lower.is_neg() || (m_lower.is_zero() && !m_lower_open)) && (m_upper.is_pos() || (m_upper.is_zero() && !m_upper_open))) << "\n";);
return
return
(m_lower.is_neg() || (m_lower.is_zero() && !m_lower_open)) &&
(m_upper.is_pos() || (m_upper.is_zero() && !m_upper_open));
}
@ -510,7 +510,7 @@ interval & interval::inv() {
ext_numeral new_upper;
if (m_lower.is_zero()) {
SASSERT(m_lower_open);
ext_numeral plus_infinity(true);
ext_numeral plus_infinity(true);
new_upper = plus_infinity;
}
else {
@ -595,7 +595,7 @@ void interval::expt(unsigned n) {
else if (m_upper.is_neg()) {
// [l, u]^n = [u^n, l^n] if u < 0
// a <= x <= b < 0 --> x^n <= a^n (use lower and upper bound -- need the fact that x is negative)
// x <= b < 0 --> b^n <= x^n
// x <= b < 0 --> b^n <= x^n
std::swap(m_lower, m_upper);
std::swap(m_lower_open, m_upper_open);
std::swap(m_lower_dep, m_upper_dep);
@ -614,7 +614,7 @@ void interval::expt(unsigned n) {
m_upper = m_lower;
m_upper_open = m_lower_open;
}
m_upper_dep = m_upper.is_infinite() ? 0 : m_manager.mk_join(m_lower_dep, m_upper_dep);
m_upper_dep = m_upper.is_infinite() ? 0 : m_manager.mk_join(m_lower_dep, m_upper_dep);
m_lower = ext_numeral(0);
m_lower_open = false;
m_lower_dep = 0;

3
src/smt/params/smt_params_helper.pyg
View file

@ -77,5 +77,6 @@ def_module_params(module_name='smt',
('str.overlap_priority', DOUBLE, -0.1, 'theory-aware priority for overlapping variable cases; use smt.theory_aware_branching=true'),
('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'),
('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'),
('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core')
('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'),
('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body')
))

45
src/smt/smt_context.cpp
View file

@ -3242,8 +3242,7 @@ namespace smt {
});
validate_unsat_core();
// theory validation of unsat core
ptr_vector<theory>::iterator th_it = m_theory_set.begin();
ptr_vector<theory>::iterator th_it = m_theory_set.begin();
ptr_vector<theory>::iterator th_end = m_theory_set.end();
for (; th_it != th_end; ++th_it) {
lbool theory_result = (*th_it)->validate_unsat_core(m_unsat_core);
@ -3251,7 +3250,6 @@ namespace smt {
return l_undef;
}
}
return l_false;
}
@ -3297,15 +3295,10 @@ namespace smt {
setup_context(m_fparams.m_auto_config);
expr_ref_vector theory_assumptions(m_manager);
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it) {
(*it)->add_theory_assumptions(theory_assumptions);
}
get_theory_assumptions(theory_assumptions);
if (!theory_assumptions.empty()) {
TRACE("search", tout << "Adding theory assumptions to context" << std::endl;);
// this works even though we already did part of setup
return check(theory_assumptions.size(), theory_assumptions.c_ptr(), reset_cancel);
return check(theory_assumptions.size(), theory_assumptions.c_ptr(), reset_cancel, true);
}
internalize_assertions();
@ -3369,7 +3362,15 @@ namespace smt {
(*it)->setup();
}
lbool context::check(unsigned ext_num_assumptions, expr * const * ext_assumptions, bool reset_cancel) {
void context::get_theory_assumptions(expr_ref_vector & theory_assumptions) {
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it) {
(*it)->add_theory_assumptions(theory_assumptions);
}
}
lbool context::check(unsigned ext_num_assumptions, expr * const * ext_assumptions, bool reset_cancel, bool already_did_theory_assumptions) {
m_stats.m_num_checks++;
TRACE("check_bug", tout << "STARTING check(num_assumptions, assumptions)\n";
tout << "inconsistent: " << inconsistent() << ", m_unsat_core.empty(): " << m_unsat_core.empty() << "\n";
@ -3381,20 +3382,20 @@ namespace smt {
if (!check_preamble(reset_cancel))
return l_undef;
expr_ref_vector theory_assumptions(m_manager);
expr_ref_vector all_assumptions(m_manager);
for (unsigned i = 0; i < ext_num_assumptions; ++i) {
theory_assumptions.push_back(ext_assumptions[i]);
all_assumptions.push_back(ext_assumptions[i]);
}
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it) {
(*it)->add_theory_assumptions(theory_assumptions);
if (!already_did_theory_assumptions) {
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it) {
(*it)->add_theory_assumptions(all_assumptions);
}
}
if (!theory_assumptions.empty()) {
TRACE("search", tout << "Adding theory assumptions to context" << std::endl;);
}
unsigned num_assumptions = theory_assumptions.size();
expr * const * assumptions = theory_assumptions.c_ptr();
unsigned num_assumptions = all_assumptions.size();
expr * const * assumptions = all_assumptions.c_ptr();
if (!validate_assumptions(num_assumptions, assumptions))
return l_undef;

4
src/smt/smt_context.h
View file

@ -1094,6 +1094,8 @@ namespace smt {
void reset_assumptions();
void get_theory_assumptions(expr_ref_vector & theory_assumptions);
lbool mk_unsat_core();
void validate_unsat_core();
@ -1476,7 +1478,7 @@ namespace smt {
void pop(unsigned num_scopes);
lbool check(unsigned num_assumptions = 0, expr * const * assumptions = 0, bool reset_cancel = true);
lbool check(unsigned num_assumptions = 0, expr * const * assumptions = 0, bool reset_cancel = true, bool already_did_theory_assumptions = false);
lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed);

3
src/smt/smt_context_inv.cpp
View file

@ -433,6 +433,9 @@ namespace smt {
if (!is_ground(n)) {
continue;
}
if (is_quantifier(n) && m.is_rec_fun_def(to_quantifier(n))) {
continue;
}
switch (get_assignment(*it)) {
case l_undef:
break;

12
src/smt/smt_justification.cpp
View file

@ -246,13 +246,15 @@ namespace smt {
simple_justification::simple_justification(region & r, unsigned num_lits, literal const * lits):
m_num_literals(num_lits) {
m_literals = new (r) literal[num_lits];
memcpy(m_literals, lits, sizeof(literal) * num_lits);
if (num_lits != 0) {
m_literals = new (r) literal[num_lits];
memcpy(m_literals, lits, sizeof(literal) * num_lits);
#ifdef Z3DEBUG
for (unsigned i = 0; i < num_lits; i++) {
SASSERT(lits[i] != null_literal);
}
for (unsigned i = 0; i < num_lits; i++) {
SASSERT(lits[i] != null_literal);
}
#endif
}
}
void simple_justification::get_antecedents(conflict_resolution & cr) {

62
src/smt/smt_model_checker.cpp
View file

@ -316,7 +316,7 @@ namespace smt {
return false;
}
bool model_checker::check_rec_fun(quantifier* q) {
bool model_checker::check_rec_fun(quantifier* q, bool strict_rec_fun) {
TRACE("model_checker", tout << mk_pp(q, m) << "\n";);
SASSERT(q->get_num_patterns() == 2); // first pattern is the function, second is the body.
expr* fn = to_app(q->get_pattern(0))->get_arg(0);
@ -340,7 +340,7 @@ namespace smt {
}
sub(q->get_expr(), num_decls, args.c_ptr(), tmp);
m_curr_model->eval(tmp, result, true);
if (m.is_false(result)) {
if (strict_rec_fun ? !m.is_true(result) : m.is_false(result)) {
add_instance(q, args, 0);
return false;
}
@ -365,10 +365,10 @@ namespace smt {
bool model_checker::check(proto_model * md, obj_map<enode, app *> const & root2value) {
SASSERT(md != 0);
m_root2value = &root2value;
ptr_vector<quantifier>::const_iterator it = m_qm->begin_quantifiers();
ptr_vector<quantifier>::const_iterator end = m_qm->end_quantifiers();
if (it == end)
if (m_qm->num_quantifiers() == 0)
return true;
if (m_iteration_idx >= m_params.m_mbqi_max_iterations) {
@ -393,6 +393,36 @@ namespace smt {
bool found_relevant = false;
unsigned num_failures = 0;
check_quantifiers(false, found_relevant, num_failures);
if (found_relevant)
m_iteration_idx++;
TRACE("model_checker", tout << "model after check:\n"; model_pp(tout, *md););
TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);
m_max_cexs += m_params.m_mbqi_max_cexs;
if (num_failures == 0 && !m_context->validate_model()) {
num_failures = 1;
// this time force expanding recursive function definitions
// that are not forced true in the current model.
check_quantifiers(true, found_relevant, num_failures);
}
if (num_failures == 0)
m_curr_model->cleanup();
if (m_params.m_mbqi_trace) {
if (num_failures == 0)
verbose_stream() << "(smt.mbqi :succeeded true)\n";
else
verbose_stream() << "(smt.mbqi :num-failures " << num_failures << ")\n";
}
return num_failures == 0;
}
void model_checker::check_quantifiers(bool strict_rec_fun, bool& found_relevant, unsigned& num_failures) {
ptr_vector<quantifier>::const_iterator it = m_qm->begin_quantifiers();
ptr_vector<quantifier>::const_iterator end = m_qm->end_quantifiers();
for (; it != end; ++it) {
quantifier * q = *it;
if(!m_qm->mbqi_enabled(q)) continue;
@ -406,7 +436,7 @@ namespace smt {
}
found_relevant = true;
if (m.is_rec_fun_def(q)) {
if (!check_rec_fun(q)) {
if (!check_rec_fun(q, strict_rec_fun)) {
TRACE("model_checker", tout << "checking recursive function failed\n";);
num_failures++;
}
@ -420,26 +450,6 @@ namespace smt {
}
}
}
if (found_relevant)
m_iteration_idx++;
TRACE("model_checker", tout << "model after check:\n"; model_pp(tout, *md););
TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);
m_max_cexs += m_params.m_mbqi_max_cexs;
if (num_failures == 0 && !m_context->validate_model()) {
num_failures = 1;
}
if (num_failures == 0)
m_curr_model->cleanup();
if (m_params.m_mbqi_trace) {
if (num_failures == 0)
verbose_stream() << "(smt.mbqi :succeeded true)\n";
else
verbose_stream() << "(smt.mbqi :num-failures " << num_failures << ")\n";
}
return num_failures == 0;
}
void model_checker::init_search_eh() {

3
src/smt/smt_model_checker.h
View file

@ -59,7 +59,8 @@ namespace smt {
void assert_neg_q_m(quantifier * q, expr_ref_vector & sks);
bool add_blocking_clause(model * cex, expr_ref_vector & sks);
bool check(quantifier * q);
bool check_rec_fun(quantifier* q);
bool check_rec_fun(quantifier* q, bool strict_rec_fun);
void check_quantifiers(bool strict_rec_fun, bool& found_relevant, unsigned& num_failures);
struct instance {
quantifier * m_q;

4
src/smt/smt_quantifier.cpp
View file

@ -397,6 +397,10 @@ namespace smt {
return m_imp->m_quantifiers.end();
}
unsigned quantifier_manager::num_quantifiers() const {
return m_imp->m_quantifiers.size();
}
// The default plugin uses E-matching, MBQI and quick-checker
class default_qm_plugin : public quantifier_manager_plugin {
quantifier_manager * m_qm;

2
src/smt/smt_quantifier.h
View file

@ -91,6 +91,8 @@ namespace smt {
ptr_vector<quantifier>::const_iterator begin_quantifiers() const;
ptr_vector<quantifier>::const_iterator end_quantifiers() const;
unsigned num_quantifiers() const;
};
class quantifier_manager_plugin {

62
src/smt/smt_solver.cpp
View file

@ -38,6 +38,7 @@ namespace smt {
bool m_minimizing_core;
bool m_core_extend_patterns;
unsigned m_core_extend_patterns_max_distance;
bool m_core_extend_nonlocal_patterns;
obj_map<expr, expr*> m_name2assertion;
public:
@ -48,13 +49,15 @@ namespace smt {
m_context(m, m_smt_params),
m_minimizing_core(false),
m_core_extend_patterns(false),
m_core_extend_patterns_max_distance(UINT_MAX) {
m_core_extend_patterns_max_distance(UINT_MAX),
m_core_extend_nonlocal_patterns(false) {
m_logic = l;
if (m_logic != symbol::null)
m_context.set_logic(m_logic);
smt_params_helper smth(p);
m_core_extend_patterns = smth.core_extend_patterns();
m_core_extend_patterns_max_distance = smth.core_extend_patterns_max_distance();
m_core_extend_nonlocal_patterns = smth.core_extend_nonlocal_patterns();
}
virtual solver * translate(ast_manager & m, params_ref const & p) {
@ -81,6 +84,8 @@ namespace smt {
m_context.updt_params(p);
smt_params_helper smth(p);
m_core_extend_patterns = smth.core_extend_patterns();
m_core_extend_patterns_max_distance = smth.core_extend_patterns_max_distance();
m_core_extend_nonlocal_patterns = smth.core_extend_nonlocal_patterns();
}
virtual void collect_param_descrs(param_descrs & r) {
@ -172,6 +177,8 @@ namespace smt {
if (m_core_extend_patterns)
add_pattern_literals_to_core(r);
if (m_core_extend_nonlocal_patterns)
add_nonlocal_pattern_literals_to_core(r);
}
virtual void get_model(model_ref & m) {
@ -250,7 +257,7 @@ namespace smt {
}
};
void collect_pattern_func_decls(expr_ref & e, func_decl_set & fds) {
void collect_pattern_fds(expr_ref & e, func_decl_set & fds) {
collect_pattern_fds_proc p(get_manager(), fds);
expr_mark visited;
for_each_expr(p, visited, e);
@ -295,7 +302,7 @@ namespace smt {
expr_ref name(core[i], m);
SASSERT(m_name2assertion.contains(name));
expr_ref assrtn(m_name2assertion.find(name), m);
collect_pattern_func_decls(assrtn, pattern_fds);
collect_pattern_fds(assrtn, pattern_fds);
}
if (!pattern_fds.empty()) {
@ -317,6 +324,55 @@ namespace smt {
break;
}
}
struct collect_body_fds_proc {
ast_manager & m;
func_decl_set & m_fds;
collect_body_fds_proc(ast_manager & m, func_decl_set & fds) :
m(m), m_fds(fds) {
}
void operator()(var * n) {}
void operator()(app * n) {}
void operator()(quantifier * n) {
collect_fds_proc p(m, m_fds);
expr_fast_mark1 visited;
quick_for_each_expr(p, visited, n->get_expr());
}
};
void collect_body_func_decls(expr_ref & e, func_decl_set & fds) {
ast_manager & m = get_manager();
collect_body_fds_proc p(m, fds);
expr_mark visited;
for_each_expr(p, visited, e);
}
void add_nonlocal_pattern_literals_to_core(ptr_vector<expr> & core) {
ast_manager & m = get_manager();
obj_map<expr, expr*>::iterator it = m_name2assertion.begin();
obj_map<expr, expr*>::iterator end = m_name2assertion.end();
for (unsigned i = 0; it != end; it++, i++) {
expr_ref name(it->m_key, m);
expr_ref assrtn(it->m_value, m);
if (!core.contains(name)) {
func_decl_set pattern_fds, body_fds;
collect_pattern_fds(assrtn, pattern_fds);
collect_body_func_decls(assrtn, body_fds);
func_decl_set::iterator pit = pattern_fds.begin();
func_decl_set::iterator pend= pattern_fds.end();
for (; pit != pend; pit++) {
func_decl * fd = *pit;
if (!body_fds.contains(fd)) {
core.insert(name);
break;
}
}
}
}
}
};
};

5
src/smt/smt_theory.h
View file

@ -178,8 +178,9 @@ namespace smt {
}
/**
\brief This method is called by smt_context before the search starts to get any
extra assumptions the theory wants to use. (see theory_str for an example)
\brief This method is called by smt_context before the search starts
to get any extra assumptions the theory wants to use.
(See theory_str for an example)
*/
virtual void add_theory_assumptions(expr_ref_vector & assumptions) {
}

5
src/smt/theory_arith_nl.h
View file

@ -339,8 +339,13 @@ namespace smt {
tout << mk_pp(var, get_manager()) << "\n";
tout << "power " << power << ": " << expt(i, power) << "\n";
display_interval(tout << "target before: ", target); tout << "\n";);
i.expt(power);
target *= i;
get_manager().limit().inc((target.is_lower_open() || target.minus_infinity()) ? 1 : target.get_lower_value().bitsize());
get_manager().limit().inc((target.is_upper_open() || target.plus_infinity()) ? 1 : target.get_upper_value().bitsize());
TRACE("non_linear", display_interval(tout << "target after: ", target); tout << "\n";);
}

52
src/smt/theory_seq.cpp
View file

@ -255,6 +255,11 @@ final_check_status theory_seq::final_check_eh() {
TRACE("seq", tout << ">>solve_eqs\n";);
return FC_CONTINUE;
}
if (check_contains()) {
++m_stats.m_propagate_contains;
TRACE("seq", tout << ">>propagate_contains\n";);
return FC_CONTINUE;
}
if (solve_nqs(0)) {
++m_stats.m_solve_nqs;
TRACE("seq", tout << ">>solve_nqs\n";);
@ -290,11 +295,6 @@ final_check_status theory_seq::final_check_eh() {
TRACE("seq", tout << ">>propagate_automata\n";);
return FC_CONTINUE;
}
if (check_contains()) {
++m_stats.m_propagate_contains;
TRACE("seq", tout << ">>propagate_contains\n";);
return FC_CONTINUE;
}
if (is_solved()) {
TRACE("seq", tout << ">>is_solved\n";);
return FC_DONE;
@ -1159,7 +1159,7 @@ bool theory_seq::check_extensionality() {
}
/*
\brief check negated contains constriants.
\brief check negated contains constraints.
*/
bool theory_seq::check_contains() {
context & ctx = get_context();
@ -1199,6 +1199,11 @@ bool theory_seq::is_solved() {
IF_VERBOSE(10, display_disequation(verbose_stream() << "(seq.giveup ", m_nqs[0]); verbose_stream() << " is unsolved)\n";);
return false;
}
if (!m_ncs.empty()) {
TRACE("seq", display_nc(tout << "(seq.giveup ", m_ncs[0]); tout << " is unsolved)\n";);
IF_VERBOSE(10, display_nc(verbose_stream() << "(seq.giveup ", m_ncs[0]); verbose_stream() << " is unsolved)\n";);
return false;
}
return true;
}
@ -1984,6 +1989,22 @@ bool theory_seq::solve_nc(unsigned idx) {
m_new_propagation = true;
return true;
}
expr* e1, *e2;
if (m.is_eq(c, e1, e2)) {
literal eq = mk_eq(e1, e2, false);
propagate_lit(deps, 0, 0, ~eq);
return true;
}
if (m.is_or(c)) {
for (unsigned i = 0; i < to_app(c)->get_num_args(); ++i) {
expr_ref ci(to_app(c)->get_arg(i), m);
m_ncs.push_back(nc(ci, deps));
}
m_new_propagation = true;
return true;
}
return false;
}
@ -2345,6 +2366,17 @@ bool theory_seq::add_itos_axiom(expr* e) {
return false;
}
add_axiom(mk_eq(e2, n, false));
#if 1
expr_ref num_re(m), opt_re(m);
num_re = m_util.re.mk_range(m_util.str.mk_string(symbol("0")), m_util.str.mk_string(symbol("9")));
num_re = m_util.re.mk_plus(num_re);
opt_re = m_util.re.mk_opt(m_util.re.mk_to_re(m_util.str.mk_string(symbol("-"))));
num_re = m_util.re.mk_concat(opt_re, num_re);
app_ref in_re(m_util.re.mk_in_re(e, num_re), m);
internalize_term(in_re);
propagate_in_re(in_re, true);
#endif
m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));
return true;
}
@ -2407,13 +2439,17 @@ void theory_seq::display(std::ostream & out) const {
if (!m_ncs.empty()) {
out << "Non contains:\n";
for (unsigned i = 0; i < m_ncs.size(); ++i) {
out << "not " << mk_pp(m_ncs[i].contains(), m) << "\n";
display_deps(out << " <- ", m_ncs[i].deps()); out << "\n";
display_nc(out, m_ncs[i]);
}
}
}
void theory_seq::display_nc(std::ostream& out, nc const& nc) const {
out << "not " << mk_pp(nc.contains(), m) << "\n";
display_deps(out << " <- ", nc.deps()); out << "\n";
}
void theory_seq::display_equations(std::ostream& out) const {
for (unsigned i = 0; i < m_eqs.size(); ++i) {
display_equation(out, m_eqs[i]);

1
src/smt/theory_seq.h
View file

@ -570,6 +570,7 @@ namespace smt {
void display_disequation(std::ostream& out, ne const& e) const;
void display_deps(std::ostream& out, dependency* deps) const;
void display_deps(std::ostream& out, literal_vector const& lits, enode_pair_vector const& eqs) const;
void display_nc(std::ostream& out, nc const& nc) const;
public:
theory_seq(ast_manager& m);
virtual ~theory_seq();