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

fixing #1520

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-28 18:03:13 -07:00
commit 1cb3f7c792
27 changed files with 340 additions and 272 deletions
Download patch file Download diff file Expand all files Collapse all files

7
scripts/update_api.py
View file

@ -1665,6 +1665,7 @@ for v in ('Z3_LIBRARY_PATH', 'PATH', 'PYTHONPATH'):
_all_dirs.extend(_default_dirs)
_failures = []
for d in _all_dirs:
try:
d = os.path.realpath(d)
@ -1673,14 +1674,16 @@ for d in _all_dirs:
if os.path.isfile(d):
_lib = ctypes.CDLL(d)
break
except:
except Exception as e:
_failures += [e]
pass
if _lib is None:
# If all else failed, ask the system to find it.
try:
_lib = ctypes.CDLL('libz3.%s' % _ext)
except:
except Exception as e:
_failures += [e]
pass
if _lib is None:

14
src/api/api_ast.cpp
View file

@ -384,12 +384,14 @@ extern "C" {
Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d) {
LOG_Z3_get_decl_name(c, d);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, nullptr);
return of_symbol(to_func_decl(d)->get_name());
}
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d) {
LOG_Z3_get_decl_num_parameters(c, d);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
return to_func_decl(d)->get_num_parameters();
}
@ -397,6 +399,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_decl_parameter_kind(c, d, idx);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, Z3_PARAMETER_INT);
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB, nullptr);
return Z3_PARAMETER_INT;
@ -429,6 +432,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_decl_int_parameter(c, d, idx);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB, nullptr);
return 0;
@ -446,6 +450,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_decl_double_parameter(c, d, idx);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB, nullptr);
return 0;
@ -463,6 +468,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_decl_symbol_parameter(c, d, idx);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB, nullptr);
return nullptr;
@ -480,6 +486,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_decl_sort_parameter(c, d, idx);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB, nullptr);
RETURN_Z3(nullptr);
@ -497,6 +504,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_decl_ast_parameter(c, d, idx);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB, nullptr);
RETURN_Z3(nullptr);
@ -514,6 +522,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_decl_func_decl_parameter(c, d, idx);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB, nullptr);
RETURN_Z3(nullptr);
@ -531,6 +540,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_decl_rational_parameter(c, d, idx);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, "");
if (idx >= to_func_decl(d)->get_num_parameters()) {
SET_ERROR_CODE(Z3_IOB, nullptr);
return "";
@ -549,6 +559,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_sort_name(c, t);
RESET_ERROR_CODE();
CHECK_VALID_AST(t, nullptr);
return of_symbol(to_sort(t)->get_name());
Z3_CATCH_RETURN(nullptr);
}
@ -567,6 +578,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_arity(c, d);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
return to_func_decl(d)->get_arity();
Z3_CATCH_RETURN(0);
}
@ -575,6 +587,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_domain_size(c, d);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
return to_func_decl(d)->get_arity();
Z3_CATCH_RETURN(0);
}
@ -583,6 +596,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_domain(c, d, i);
RESET_ERROR_CODE();
CHECK_VALID_AST(d, 0);
if (i >= to_func_decl(d)->get_arity()) {
SET_ERROR_CODE(Z3_IOB, nullptr);
RETURN_Z3(nullptr);

21
src/api/api_numeral.cpp
View file

@ -26,6 +26,7 @@ Revision History:
#include "ast/fpa_decl_plugin.h"
bool is_numeral_sort(Z3_context c, Z3_sort ty) {
if (!ty) return false;
sort * _ty = to_sort(ty);
family_id fid = _ty->get_family_id();
if (fid != mk_c(c)->get_arith_fid() &&
@ -145,7 +146,8 @@ extern "C" {
Z3_bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a) {
Z3_TRY;
LOG_Z3_is_numeral_ast(c, a);
RESET_ERROR_CODE();
RESET_ERROR_CODE();
CHECK_IS_EXPR(a, Z3_FALSE);
expr* e = to_expr(a);
return
mk_c(c)->autil().is_numeral(e) ||
@ -160,11 +162,8 @@ extern "C" {
Z3_TRY;
// This function is not part of the public API
RESET_ERROR_CODE();
CHECK_IS_EXPR(a, Z3_FALSE);
expr* e = to_expr(a);
if (!e) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return Z3_FALSE;
}
if (mk_c(c)->autil().is_numeral(e, r)) {
return Z3_TRUE;
}
@ -187,6 +186,7 @@ extern "C" {
// This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
LOG_Z3_get_numeral_string(c, a);
RESET_ERROR_CODE();
CHECK_IS_EXPR(a, Z3_FALSE);
rational r;
Z3_bool ok = Z3_get_numeral_rational(c, a, r);
if (ok == Z3_TRUE) {
@ -232,11 +232,8 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_numeral_decimal_string(c, a, precision);
RESET_ERROR_CODE();
CHECK_IS_EXPR(a, "");
expr* e = to_expr(a);
if (!e) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return "";
}
rational r;
arith_util & u = mk_c(c)->autil();
if (u.is_numeral(e, r) && !r.is_int()) {
@ -267,6 +264,7 @@ extern "C" {
// This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
LOG_Z3_get_numeral_small(c, a, num, den);
RESET_ERROR_CODE();
CHECK_IS_EXPR(a, Z3_FALSE);
rational r;
Z3_bool ok = Z3_get_numeral_rational(c, a, r);
if (ok == Z3_TRUE) {
@ -292,6 +290,7 @@ extern "C" {
// This function invokes Z3_get_numeral_int64, but it is still ok to add LOG command here because it does not return a Z3 object.
LOG_Z3_get_numeral_int(c, v, i);
RESET_ERROR_CODE();
CHECK_IS_EXPR(v, Z3_FALSE);
if (!i) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return Z3_FALSE;
@ -310,6 +309,7 @@ extern "C" {
// This function invokes Z3_get_numeral_uint64, but it is still ok to add LOG command here because it does not return a Z3 object.
LOG_Z3_get_numeral_uint(c, v, u);
RESET_ERROR_CODE();
CHECK_IS_EXPR(v, Z3_FALSE);
if (!u) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return Z3_FALSE;
@ -328,6 +328,7 @@ extern "C" {
// This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
LOG_Z3_get_numeral_uint64(c, v, u);
RESET_ERROR_CODE();
CHECK_IS_EXPR(v, Z3_FALSE);
if (!u) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return Z3_FALSE;
@ -348,6 +349,7 @@ extern "C" {
// This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
LOG_Z3_get_numeral_int64(c, v, i);
RESET_ERROR_CODE();
CHECK_IS_EXPR(v, Z3_FALSE);
if (!i) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return Z3_FALSE;
@ -367,6 +369,7 @@ extern "C" {
// This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object.
LOG_Z3_get_numeral_rational_int64(c, v, num, den);
RESET_ERROR_CODE();
CHECK_IS_EXPR(v, Z3_FALSE);
if (!num || !den) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return Z3_FALSE;

4
src/ast/ast.cpp
View file

@ -2406,7 +2406,6 @@ quantifier * ast_manager::mk_quantifier(quantifier_kind k, unsigned num_decls, s
*m_trace_stream << " #" << patterns[i]->get_id();
}
*m_trace_stream << " #" << body->get_id() << "\n";
}
return r;
@ -2420,6 +2419,9 @@ quantifier * ast_manager::mk_lambda(unsigned num_decls, sort * const * decl_sort
sort* s = autil.mk_array_sort(num_decls, decl_sorts, ::get_sort(body));
quantifier * new_node = new (mem) quantifier(num_decls, decl_sorts, decl_names, body, s);
quantifier * r = register_node(new_node);
if (m_trace_stream && r == new_node) {
*m_trace_stream << "[mk-lambda] #" << r->get_id() << ": #" << body->get_id() << "\n";
}
return r;
}

5
src/ast/rewriter/seq_rewriter.cpp
View file

@ -1881,7 +1881,7 @@ bool seq_rewriter::reduce_contains(expr* a, expr* b, expr_ref_vector& disj) {
unsigned sz = s.length();
expr_ref_vector es(m());
for (unsigned j = 0; j < sz; ++j) {
es.push_back(m_util.str.mk_char(s, j));
es.push_back(m_util.str.mk_unit(m_util.str.mk_char(s, j)));
}
es.append(m_lhs.size() - i, m_lhs.c_ptr() + i);
for (unsigned j = 0; j < sz; ++j) {
@ -1896,9 +1896,8 @@ bool seq_rewriter::reduce_contains(expr* a, expr* b, expr_ref_vector& disj) {
if (m_util.str.is_string(b, s)) {
expr* all = m_util.re.mk_full_seq(m_util.re.mk_re(m().get_sort(b)));
std::cout << sort_ref(m().get_sort(all), m()) << "\n";
disj.push_back(m_util.re.mk_in_re(m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i),
m_util.re.mk_concat(all, m_util.str.mk_concat(m_util.re.mk_to_re(b), all))));
m_util.re.mk_concat(all, m_util.re.mk_concat(m_util.re.mk_to_re(b), all))));
return true;
}

15
src/smt/old_interval.cpp
View file

@ -561,15 +561,24 @@ interval & interval::operator/=(interval const & other) {
TRACE("interval", other.display_with_dependencies(tout););
if (other.m_lower.is_pos() || (other.m_lower.is_zero() && other.m_lower_open)) {
// other.lower > 0
// x in ([0, 0] / [other.lo, other.up]), for other.lo > 0
// <=>
// x >= 0: because y*x >= 0 & y > 0
// x <= 0: because y*x <= 0 & y > 0
m_lower_dep = join(m_lower_dep, other.m_lower_dep);
m_upper_dep = join(m_upper_dep, other.m_lower_dep);
}
else {
// assertion must hold since !other.contains_zero()
SASSERT(other.m_upper.is_neg() || (other.m_upper.is_zero() && other.m_upper_open));
SASSERT(other.m_upper.is_neg() || (other.m_upper.is_zero() && other.m_upper_open));
// other.upper < 0
m_lower_dep = join(m_lower_dep, other.m_upper_dep);
m_upper_dep = join(m_upper_dep, other.m_upper_dep);
// x in ([0, 0] / [other.lo, other.up]), for up < 0
// <=>
// x >= 0: because y*x <= 0 & y < 0
// x <= 0: because y*x >= 0 & y < 0
v_dependency* lower_dep = m_lower_dep;
m_lower_dep = join(m_upper_dep, other.m_upper_dep);
m_upper_dep = join(lower_dep, other.m_upper_dep);
}
return *this;
}

5
src/smt/smt_context.cpp
View file

@ -228,7 +228,6 @@ namespace smt {
}
void context::copy_plugins(context& src, context& dst) {
// copy theory plugins
for (theory* old_th : src.m_theory_set) {
theory * new_th = old_th->mk_fresh(&dst);
@ -236,8 +235,8 @@ namespace smt {
}
}
context * context::mk_fresh(symbol const * l, smt_params * p) {
context * new_ctx = alloc(context, m_manager, p == nullptr ? m_fparams : *p);
context * context::mk_fresh(symbol const * l, smt_params * p, params_ref const& pa) {
context * new_ctx = alloc(context, m_manager, p ? *p : m_fparams, pa);
new_ctx->set_logic(l == nullptr ? m_setup.get_logic() : *l);
copy_plugins(*this, *new_ctx);
return new_ctx;

2
src/smt/smt_context.h
View file

@ -1493,7 +1493,7 @@ namespace smt {
If l == 0, then the logic of this context is used in the new context.
If p == 0, then this->m_params is used
*/
context * mk_fresh(symbol const * l = nullptr, smt_params * p = nullptr);
context * mk_fresh(symbol const * l = nullptr, smt_params * smtp = nullptr, params_ref const & p = params_ref());
static void copy(context& src, context& dst);

2
src/smt/smt_context_pp.cpp
View file

@ -422,8 +422,6 @@ namespace smt {
out << "(check-sat)\n";
}
#define BUFFER_SZ 128
unsigned context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent, symbol const& logic) const {
std::stringstream strm;
strm << "lemma_" << (++m_lemma_id) << ".smt2";

14
src/smt/smt_internalizer.cpp
View file

@ -678,8 +678,18 @@ namespace smt {
push_trail(set_merge_tf_trail(n));
n->m_merge_tf = true;
lbool val = get_assignment(v);
if (val != l_undef)
push_eq(n, val == l_true ? m_true_enode : m_false_enode, eq_justification(literal(v, val == l_false)));
switch (val) {
case l_undef:
break;
case l_true:
if (n->get_root() != m_true_enode->get_root())
push_eq(n, m_true_enode, eq_justification(literal(v, false)));
break;
case l_false:
if (n->get_root() != m_false_enode->get_root())
push_eq(n, m_false_enode, eq_justification(literal(v, true)));
break;
}
}
}

2
src/smt/smt_literal.h
View file

@ -103,7 +103,7 @@ namespace smt {
void display_compact(std::ostream & out, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map);
void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep = " ");
void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep = "\n");
template<typename T>
void neg_literals(unsigned num_lits, literal const * lits, T & result) {

5
src/smt/smt_model_checker.cpp
View file

@ -384,10 +384,13 @@ namespace smt {
m_fparams = alloc(smt_params, m_context->get_fparams());
m_fparams->m_relevancy_lvl = 0; // no relevancy since the model checking problems are quantifier free
m_fparams->m_case_split_strategy = CS_ACTIVITY; // avoid warning messages about smt.case_split >= 3.
m_fparams->m_arith_dump_lemmas = false;
}
if (!m_aux_context) {
symbol logic;
m_aux_context = m_context->mk_fresh(&logic, m_fparams.get());
params_ref p;
p.set_bool("arith.dump_lemmas", false);
m_aux_context = m_context->mk_fresh(&logic, m_fparams.get(), p);
}
}

12
src/smt/smt_setup.cpp
View file

@ -627,9 +627,6 @@ namespace smt {
m_params.m_phase_selection = PS_CACHING_CONSERVATIVE2;
m_params.m_random_initial_activity = IA_ZERO;
}
// if (st.m_num_arith_ineqs == st.m_num_diff_ineqs && st.m_num_arith_eqs == st.m_num_diff_eqs && st.arith_k_sum_is_small())
// m_context.register_plugin(new smt::theory_si_arith(m_manager, m_params));
// else
setup_i_arith();
setup_arrays();
}
@ -654,7 +651,7 @@ namespace smt {
//
m_params.m_ng_lift_ite = LI_FULL;
TRACE("setup", tout << "max_eager_multipatterns: " << m_params.m_qi_max_eager_multipatterns << "\n";);
setup_i_arith();
m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
setup_arrays();
}
@ -832,7 +829,10 @@ namespace smt {
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
break;
case AS_NEW_ARITH:
setup_lra_arith();
if (st.m_num_non_linear != 0)
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
else
setup_lra_arith();
break;
default:
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
@ -994,7 +994,7 @@ namespace smt {
}
if (st.num_theories() == 2 && st.has_uf() && is_arith(st)) {
if (!st.m_has_real)
if (!st.m_has_real && st.m_num_non_linear == 0)
setup_QF_UFLIA(st);
else if (!st.m_has_int && st.m_num_non_linear == 0)
setup_QF_UFLRA();

2
src/smt/smt_theory.cpp
View file

@ -123,7 +123,7 @@ namespace smt {
context & ctx = get_context();
app * eq = ctx.mk_eq_atom(a, b);
TRACE("mk_var_bug", tout << "mk_eq: " << eq->get_id() << " " << a->get_id() << " " << b->get_id() << "\n";
tout << mk_ll_pp(a, get_manager()) << "\n" << mk_ll_pp(b, get_manager()););
tout << mk_ll_pp(a, get_manager()) << "\n" << mk_ll_pp(b, get_manager()););
ctx.internalize(eq, gate_ctx);
return ctx.get_literal(eq);
}

40
src/smt/theory_arith_aux.h
View file

@ -731,35 +731,34 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::derived_bound::push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) {
TRACE("arith", tout << m_lits << " " << m_eqs.size() << "\n";);
if (proofs_enabled) {
for (unsigned i = 0; i < m_lits.size(); ++i) {
a.push_lit(m_lits[i], coeff, proofs_enabled);
}
for (unsigned i = 0; i < m_eqs.size(); ++i) {
a.push_eq(m_eqs[i], coeff, proofs_enabled);
}
for (literal l : m_lits)
a.push_lit(l, coeff, proofs_enabled);
for (auto const& e : m_eqs)
a.push_eq(e, coeff, proofs_enabled);
}
else {
a.append(m_lits.size(), m_lits.c_ptr());
a.append(m_eqs.size(), m_eqs.c_ptr());
a.append(m_eqs.size(), m_eqs.c_ptr());
}
}
template<typename Ext>
void theory_arith<Ext>::derived_bound::display(theory_arith<Ext> const& th, std::ostream& out) const {
out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << bound::get_value();
ast_manager& m = th.get_manager();
for (unsigned i = 0; i < m_eqs.size(); ++i) {
enode* a = m_eqs[i].first;
enode* b = m_eqs[i].second;
out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << bound::get_value() << "\n";
out << "expr: " << mk_pp(th.var2expr(bound::get_var()), m) << "\n";
for (auto const& e : m_eqs) {
enode* a = e.first;
enode* b = e.second;
out << " ";
out << "#" << a->get_owner_id() << " " << mk_pp(a->get_owner(), m) << " = "
<< "#" << b->get_owner_id() << " " << mk_pp(b->get_owner(), m);
<< "#" << b->get_owner_id() << " " << mk_pp(b->get_owner(), m) << "\n";
}
for (unsigned i = 0; i < m_lits.size(); ++i) {
literal l = m_lits[i];
out << " " << l << ":"; th.get_context().display_detailed_literal(out, l);
for (literal l : m_lits) {
out << l << ":"; th.get_context().display_detailed_literal(out, l) << "\n";
}
}
@ -882,13 +881,10 @@ namespace smt {
}
TRACE("derived_bound",
tout << "explanation:\n";
literal_vector::const_iterator it1 = new_bound->m_lits.begin();
literal_vector::const_iterator end1 = new_bound->m_lits.end();
for (; it1 != end1; ++it1) tout << *it1 << " ";
for (literal l : new_bound->m_lits) tout << l << " ";
tout << " ";
eq_vector::const_iterator it2 = new_bound->m_eqs.begin();
eq_vector::const_iterator end2 = new_bound->m_eqs.end();
for (; it2 != end2; ++it2) tout << "#" << it2->first->get_owner_id() << "=#" << it2->second->get_owner_id() << " ";
for (auto const& e : new_bound->m_eqs)
tout << "#" << e.first->get_owner_id() << "=#" << e.second->get_owner_id() << " ";
tout << "\n";);
DEBUG_CODE(CTRACE("derived_bound", k != val, tout << "k: " << k << ", k_norm: " << k_norm << ", val: " << val << "\n";););
SASSERT(k == val);

89
src/smt/theory_arith_core.h
View file

@ -1708,7 +1708,7 @@ namespace smt {
template<typename Ext>
theory* theory_arith<Ext>::mk_fresh(context* new_ctx) {
return alloc(theory_arith<Ext>, new_ctx->get_manager(), m_params);
return alloc(theory_arith<Ext>, new_ctx->get_manager(), new_ctx->get_fparams());
}
template<typename Ext>
@ -1853,10 +1853,7 @@ namespace smt {
void theory_arith<Ext>::restore_assignment() {
CASSERT("arith", valid_row_assignment());
TRACE("restore_assignment_bug", tout << "START restore_assignment...\n";);
typename svector<unsigned>::iterator it = m_update_trail_stack.begin();
typename svector<unsigned>::iterator end = m_update_trail_stack.end();
for(; it != end; ++it) {
theory_var v = *it;
for (theory_var v : m_update_trail_stack) {
TRACE("restore_assignment_bug", tout << "restoring v" << v << " <- " << m_old_value[v] << "\n";);
SASSERT(!is_quasi_base(v));
SASSERT(m_in_update_trail_stack.contains(v));
@ -2237,11 +2234,7 @@ namespace smt {
theory_var best = null_theory_var;
inf_numeral best_error;
inf_numeral curr_error;
typename var_heap::iterator it = m_to_patch.begin();
typename var_heap::iterator end = m_to_patch.end();
//unsigned n = 0;
for (; it != end; ++it) {
theory_var v = *it;
for (theory_var v : m_to_patch) {
if (below_lower(v))
curr_error = lower(v)->get_value() - get_value(v);
else if (above_upper(v))
@ -2391,10 +2384,11 @@ namespace smt {
TRACE("sign_row_conflict", tout << "v" << x_i << " is_below: " << is_below << " delta: " << delta << "\n"; display_var(tout, x_i);
tout << "is_below_lower: " << below_lower(x_i) << ", is_above_upper: " << above_upper(x_i) << "\n";
display_row(tout, r, true);
display_row(tout, r, false);
ante.display(tout););
set_conflict(ante, ante, "farkas");
// display_bounds_in_smtlib();
}
// -----------------------------------
@ -2535,10 +2529,9 @@ namespace smt {
antecedents ante(*this);
b1->push_justification(ante, numeral(1), coeffs_enabled());
b2->push_justification(ante, numeral(1), coeffs_enabled());
set_conflict(ante, ante, "farkas");
TRACE("arith_conflict", tout << "bound conflict v" << b1->get_var() << "\n";
tout << "bounds: " << b1 << " " << b2 << "\n";);
set_conflict(ante, ante, "farkas");
}
// -----------------------------------
@ -2771,8 +2764,10 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::explain_bound(row const & r, int idx, bool is_lower, inf_numeral & delta, antecedents& ante) {
SASSERT(delta >= inf_numeral::zero());
if (!relax_bounds() && (!ante.lits().empty() || !ante.eqs().empty()))
TRACE("arith_conflict", tout << "relax: " << relax_bounds() << " lits: " << ante.lits().size() << " eqs: " << ante.eqs().size() << " idx: " << idx << "\n";);
if (!relax_bounds() && (!ante.lits().empty() || !ante.eqs().empty())) {
return;
}
context & ctx = get_context();
row_entry const & entry = r[idx];
numeral coeff = entry.m_coeff;
@ -2790,9 +2785,11 @@ namespace smt {
if (!it->is_dead() && idx != idx2) {
bound * b = get_bound(it->m_var, is_lower ? it->m_coeff.is_pos() : it->m_coeff.is_neg());
SASSERT(b);
if (!b->has_justification())
if (!b->has_justification()) {
continue;
}
if (!relax_bounds() || delta.is_zero()) {
TRACE("propagate_bounds", tout << "push justification: v" << it->m_var << "\n";);
b->push_justification(ante, it->m_coeff, coeffs_enabled());
continue;
}
@ -2821,10 +2818,7 @@ namespace smt {
inf_numeral k_2 = k_1;
atom * new_atom = nullptr;
atoms const & as = m_var_occs[it->m_var];
typename atoms::const_iterator it = as.begin();
typename atoms::const_iterator end = as.end();
for (; it != end; ++it) {
atom * a = *it;
for (atom * a : as) {
if (a == b)
continue;
bool_var bv = a->get_bool_var();
@ -2880,10 +2874,7 @@ namespace smt {
atoms const & as = m_var_occs[v];
inf_numeral const & epsilon = get_epsilon(v);
inf_numeral delta;
typename atoms::const_iterator it = as.begin();
typename atoms::const_iterator end = as.end();
for (; it != end; ++it) {
atom * a = *it;
for (atom* a : as) {
bool_var bv = a->get_bool_var();
literal l(bv);
if (get_context().get_assignment(bv) == l_undef) {
@ -2952,8 +2943,29 @@ namespace smt {
context & ctx = get_context();
if (dump_lemmas()) {
TRACE("arith", ante.display(tout) << " --> "; ctx.display_detailed_literal(tout, l); tout << "\n";);
ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().c_ptr(),
unsigned id = ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().c_ptr(),
ante.eqs().size(), ante.eqs().c_ptr(), l);
#if 1
if (id == 394) {
enable_trace("sign_row_conflict");
enable_trace("nl_arith_bug");
enable_trace("nl_evaluate");
enable_trace("propagate_bounds");
enable_trace("propagate_bounds_bug");
enable_trace("arith_conflict");
enable_trace("non_linear");
enable_trace("non_linear_bug");
}
SASSERT(id != 395);
if (id == 396) {
disable_trace("nl_arith_bug");
disable_trace("propagate_bounds");
disable_trace("arith_conflict");
disable_trace("non_linear");
disable_trace("non_linear_bug");
}
#endif
}
}
@ -2961,8 +2973,28 @@ namespace smt {
void theory_arith<Ext>::dump_lemmas(literal l, derived_bound const& ante) {
context & ctx = get_context();
if (dump_lemmas()) {
ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().c_ptr(),
unsigned id = ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().c_ptr(),
ante.eqs().size(), ante.eqs().c_ptr(), l);
#if 1
if (id == 394) {
enable_trace("nl_arith_bug");
enable_trace("nl_evaluate");
enable_trace("propagate_bounds");
enable_trace("arith_conflict");
enable_trace("propagate_bounds_bug");
enable_trace("non_linear");
enable_trace("non_linear_bug");
}
SASSERT(id != 395);
if (id == 396) {
enable_trace("sign_row_conflict");
disable_trace("nl_arith_bug");
disable_trace("propagate_bounds");
disable_trace("arith_conflict");
disable_trace("non_linear");
disable_trace("non_linear_bug");
}
#endif
}
}
@ -2972,12 +3004,13 @@ namespace smt {
context & ctx = get_context();
antecedents ante(*this);
explain_bound(r, idx, is_lower, delta, ante);
dump_lemmas(l, ante);
TRACE("propagate_bounds",
ante.display(tout) << " --> ";
ctx.display_detailed_literal(tout, l);
tout << "\n";);
dump_lemmas(l, ante);
if (ante.lits().size() < small_lemma_size() && ante.eqs().empty()) {
literal_vector & lits = m_tmp_literal_vector2;
lits.reset();
@ -3060,14 +3093,14 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::set_conflict(antecedents const& ante, antecedents& bounds, char const* proof_rule) {
dump_lemmas(false_literal, ante);
set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), bounds, proof_rule);
dump_lemmas(false_literal, ante);
}
template<typename Ext>
void theory_arith<Ext>::set_conflict(derived_bound const& ante, antecedents& bounds, char const* proof_rule) {
dump_lemmas(false_literal, ante);
set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), bounds, proof_rule);
dump_lemmas(false_literal, ante);
}
template<typename Ext>

119
src/smt/theory_arith_nl.h
View file

@ -58,7 +58,6 @@ namespace smt {
void theory_arith<Ext>::mark_var(theory_var v, svector<theory_var> & vars, var_set & already_found) {
if (already_found.contains(v))
return;
TRACE("non_linear", tout << "marking: v" << v << "\n";);
already_found.insert(v);
vars.push_back(v);
}
@ -71,8 +70,7 @@ namespace smt {
if (is_pure_monomial(v)) {
expr * n = var2expr(v);
SASSERT(m_util.is_mul(n));
for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) {
expr * curr = to_app(n)->get_arg(i);
for (expr * curr : *to_app(n)) {
theory_var v = expr2var(curr);
SASSERT(v != null_theory_var);
mark_var(v, vars, already_found);
@ -118,22 +116,19 @@ namespace smt {
var_set already_found;
row_set already_visited_rows;
context & ctx = get_context();
svector<theory_var>::const_iterator it = m_nl_monomials.begin();
svector<theory_var>::const_iterator end = m_nl_monomials.end();
for (; it != end; ++it) {
theory_var v = *it;
for (theory_var v : m_nl_monomials) {
expr * n = var2expr(v);
if (ctx.is_relevant(n))
mark_var(v, vars, already_found);
}
for (unsigned idx = 0; idx < vars.size(); idx++) {
TRACE("non_linear", tout << "marking dependents of: v" << vars[idx] << "\n";);
mark_dependents(vars[idx], vars, already_found, already_visited_rows);
// NB: vars changes inside of loop
for (unsigned idx = 0; idx < vars.size(); ++idx) {
theory_var v = vars[idx];
TRACE("non_linear", tout << "marking dependents of: v" << v << "\n";);
mark_dependents(v, vars, already_found, already_visited_rows);
}
TRACE("non_linear", tout << "variables in non linear cluster:\n";
svector<theory_var>::const_iterator it = vars.begin();
svector<theory_var>::const_iterator end = vars.end();
for (; it != end; ++it) tout << "v" << *it << " ";
for (theory_var v : vars) tout << "v" << v << " ";
tout << "\n";);
}
@ -227,9 +222,8 @@ namespace smt {
SASSERT(!m_util.is_numeral(m));
if (m_util.is_mul(m)) {
unsigned num_vars = 0;
expr * var = nullptr;
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
expr * curr = to_app(m)->get_arg(i);
expr * var = nullptr;
for (expr * curr : *to_app(m)) {
if (var != curr) {
num_vars++;
var = curr;
@ -254,9 +248,7 @@ namespace smt {
unsigned curr_idx = 0;
expr * var = nullptr;
unsigned power = 0;
unsigned j;
for (j = 0; j < to_app(m)->get_num_args(); j++) {
expr * arg = to_app(m)->get_arg(j);
for (expr * arg : *to_app(m)) {
if (var == nullptr) {
var = arg;
power = 1;
@ -360,6 +352,7 @@ namespace smt {
template<typename Ext>
interval theory_arith<Ext>::evaluate_as_interval(expr * n) {
expr* arg;
rational val;
TRACE("nl_evaluate", tout << "evaluating: " << mk_bounded_pp(n, get_manager(), 10) << "\n";);
if (has_var(n)) {
TRACE("nl_evaluate", tout << "n has a variable associated with it\n";);
@ -370,8 +363,8 @@ namespace smt {
else if (m_util.is_add(n)) {
TRACE("nl_evaluate", tout << "is add\n";);
interval r(m_dep_manager, rational(0));
for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) {
r += evaluate_as_interval(to_app(n)->get_arg(i));
for (expr* arg : *to_app(n)) {
r += evaluate_as_interval(arg);
}
TRACE("cross_nested_eval_bug", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";);
return r;
@ -388,31 +381,28 @@ namespace smt {
it.expt(power);
r *= it;
}
TRACE("cross_nested_eval_bug", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";);
TRACE("nl_evaluate", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";);
return r;
}
else if (m_util.is_to_real(n, arg)) {
return evaluate_as_interval(arg);
}
else if (m_util.is_numeral(n, val)) {
TRACE("nl_evaluate", tout << "is numeral\n";);
return interval(m_dep_manager, val);
}
else {
rational val;
if (m_util.is_numeral(n, val)) {
TRACE("nl_evaluate", tout << "is numeral\n";);
return interval(m_dep_manager, val);
}
else {
TRACE("nl_evaluate", tout << "is unknown\n";);
return interval(m_dep_manager);
}
TRACE("nl_evaluate", tout << "is unknown\n";);
return interval(m_dep_manager);
}
}
template<typename Ext>
void theory_arith<Ext>::display_monomial(std::ostream & out, expr * m) const {
void theory_arith<Ext>::display_monomial(std::ostream & out, expr * n) const {
bool first = true;
unsigned num_vars = get_num_vars_in_monomial(m);
unsigned num_vars = get_num_vars_in_monomial(n);
for (unsigned i = 0; i < num_vars; i++) {
var_power_pair p = get_var_and_degree(m, i);
var_power_pair p = get_var_and_degree(n, i);
SASSERT(p.first != 0);
if (first) first = false; else out << " * ";
out << mk_bounded_pp(p.first, get_manager()) << "^" << p.second;
@ -425,10 +415,8 @@ namespace smt {
m_dep_manager.linearize(dep, bounds);
m_tmp_lit_set.reset();
m_tmp_eq_set.reset();
ptr_vector<void>::const_iterator it = bounds.begin();
ptr_vector<void>::const_iterator end = bounds.end();
for (; it != end; ++it) {
bound * b = static_cast<bound*>(*it);
for (void* _b : bounds) {
bound * b = static_cast<bound*>(_b);
accumulate_justification(*b, new_bound, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set);
}
}
@ -544,21 +532,19 @@ namespace smt {
the method returns without doing anything.
*/
template<typename Ext>
bool theory_arith<Ext>::propagate_nl_downward(expr * m, unsigned i) {
SASSERT(is_pure_monomial(m));
SASSERT(i < get_num_vars_in_monomial(m));
var_power_pair p = get_var_and_degree(m, i);
bool theory_arith<Ext>::propagate_nl_downward(expr * n, unsigned i) {
SASSERT(is_pure_monomial(n));
SASSERT(i < get_num_vars_in_monomial(n));
var_power_pair p = get_var_and_degree(n, i);
expr * v = p.first;
unsigned power = p.second;
TRACE("propagate_nl_downward", tout << "m: " << mk_ismt2_pp(m, get_manager()) << "\nv: " << mk_ismt2_pp(v, get_manager()) <<
"\npower: " << power << "\n";);
if (power != 1)
return false; // TODO: remove, when the n-th root is implemented in interval.
unsigned num_vars = get_num_vars_in_monomial(m);
unsigned num_vars = get_num_vars_in_monomial(n);
interval other_bounds(m_dep_manager, rational(1));
// TODO: the following code can be improved it is quadratic on the degree of the monomial.
for (unsigned i = 0; i < num_vars; i++) {
var_power_pair p = get_var_and_degree(m, i);
var_power_pair p = get_var_and_degree(n, i);
if (p.first == v)
continue;
expr * var = p.first;
@ -567,7 +553,13 @@ namespace smt {
}
if (other_bounds.contains_zero())
return false; // interval division requires that divisor doesn't contain 0.
interval r = mk_interval_for(m);
interval r = mk_interval_for(n);
TRACE("nl_arith_bug", tout << "m: " << mk_ismt2_pp(n, get_manager()) << "\nv: " << mk_ismt2_pp(v, get_manager()) <<
"\npower: " << power << "\n";
tout << "num_vars: " << num_vars << "\n";
display_interval(tout << "monomial bounds\n", r);
display_interval(tout << "other bounds\n", other_bounds);
);
r /= other_bounds;
return update_bounds_using_interval(v, r);
}
@ -907,7 +899,6 @@ namespace smt {
}
TRACE("non_linear_bug", tout << "enode: " << get_context().get_enode(rhs) << " enode_id: " << get_context().get_enode(rhs)->get_owner_id() << "\n";);
theory_var new_v = expr2var(rhs);
TRACE("non_linear_bug", ctx.display(tout););
SASSERT(new_v != null_theory_var);
new_lower = alloc(derived_bound, new_v, inf_numeral(0), B_LOWER);
new_upper = alloc(derived_bound, new_v, inf_numeral(0), B_UPPER);
@ -953,19 +944,17 @@ namespace smt {
}
accumulate_justification(*l, *new_lower, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set);
TRACE("non_linear",
for (unsigned j = 0; j < new_lower->m_lits.size(); ++j) {
ctx.display_detailed_literal(tout, new_lower->m_lits[j]);
tout << " ";
TRACE("non_linear",
for (literal l : new_lower->m_lits) {
ctx.display_detailed_literal(tout, l) << " ";
}
tout << "\n";);
accumulate_justification(*u, *new_lower, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set);
TRACE("non_linear",
for (unsigned j = 0; j < new_lower->m_lits.size(); ++j) {
ctx.display_detailed_literal(tout, new_lower->m_lits[j]);
tout << " ";
for (literal l : new_lower->m_lits) {
ctx.display_detailed_literal(tout, l) << " ";
}
tout << "\n";);
@ -977,9 +966,8 @@ namespace smt {
TRACE("non_linear",
new_lower->display(*this, tout << "lower: "); tout << "\n";
new_upper->display(*this, tout << "upper: "); tout << "\n";
for (unsigned j = 0; j < new_upper->m_lits.size(); ++j) {
ctx.display_detailed_literal(tout, new_upper->m_lits[j]);
tout << " ";
for (literal lit : new_upper->m_lits) {
ctx.display_detailed_literal(tout, lit) << " ";
}
tout << "\n";);
@ -1123,14 +1111,14 @@ namespace smt {
continue;
if (is_pure_monomial(v)) {
expr * m = var2expr(v);
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
theory_var curr = expr2var(to_app(m)->get_arg(i));
for (expr* arg : *to_app(m)) {
theory_var curr = expr2var(arg);
if (m_tmp_var_set.contains(curr))
return true;
}
SASSERT(m == var2expr(v));
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
theory_var curr = expr2var(to_app(m)->get_arg(i));
for (expr* arg : *to_app(m)) {
theory_var curr = expr2var(arg);
if (!is_fixed(curr))
m_tmp_var_set.insert(curr);
}
@ -1936,10 +1924,7 @@ namespace smt {
derived_bound b(null_theory_var, inf_numeral(0), B_LOWER);
dependency2new_bound(d, b);
set_conflict(b, ante, "arith_nl");
TRACE("non_linear",
for (unsigned i = 0; i < b.m_lits.size(); ++i) {
tout << b.m_lits[i] << " ";
});
TRACE("non_linear", for (literal lit : b.m_lits) tout << lit << " "; tout << "\n";);
}
/**
@ -2387,7 +2372,7 @@ namespace smt {
elim_quasi_base_rows();
move_non_base_vars_to_bounds();
TRACE("non_linear", tout << "processing non linear constraints...\n"; get_context().display(tout););
TRACE("non_linear_verbose", tout << "processing non linear constraints...\n"; get_context().display(tout););
if (!make_feasible()) {
TRACE("non_linear", tout << "failed to move variables to bounds.\n";);
failed();

49
src/smt/theory_arith_pp.h
View file

@ -391,19 +391,19 @@ namespace smt {
void theory_arith<Ext>::display_vars(std::ostream & out) const {
out << "vars:\n";
int n = get_num_vars();
int inf_vars = 0;
int int_inf_vars = 0;
for (theory_var v = 0; v < n; v++) {
if ((lower(v) && lower(v)->get_value() > get_value(v))
|| (upper(v) && upper(v)->get_value() < get_value(v)))
inf_vars++;
if (is_int(v) && !get_value(v).is_int())
int_inf_vars++;
}
out << "infeasibles = " << inf_vars << " int_inf = " << int_inf_vars << std::endl;
for (theory_var v = 0; v < n; v++) {
display_var(out, v);
}
int inf_vars = 0;
int int_inf_vars = 0;
for (theory_var v = 0; v < n; v++) {
if ((lower(v) && lower(v)->get_value() > get_value(v))
|| (upper(v) && upper(v)->get_value() < get_value(v)))
inf_vars++;
if (is_int(v) && !get_value(v).is_int())
int_inf_vars++;
}
out << "infeasibles = " << inf_vars << " int_inf = " << int_inf_vars << std::endl;
for (theory_var v = 0; v < n; v++) {
display_var(out, v);
}
}
template<typename Ext>
@ -418,9 +418,9 @@ namespace smt {
th.get_context().display_literals_verbose(out, lits().size(), lits().c_ptr());
if (!lits().empty()) out << "\n";
ast_manager& m = th.get_manager();
for (unsigned i = 0; i < m_eqs.size(); ++i) {
out << mk_pp(m_eqs[i].first->get_owner(), m) << " ";
out << mk_pp(m_eqs[i].second->get_owner(), m) << "\n";
for (auto const& e : m_eqs) {
out << mk_pp(e.first->get_owner(), m) << " ";
out << mk_pp(e.second->get_owner(), m) << "\n";
}
return out;
}
@ -431,27 +431,24 @@ namespace smt {
m_dep_manager.linearize(dep, bounds);
m_tmp_lit_set.reset();
m_tmp_eq_set.reset();
ptr_vector<void>::const_iterator it = bounds.begin();
ptr_vector<void>::const_iterator end = bounds.end();
for (; it != end; ++it) {
bound * b = static_cast<bound*>(*it);
out << " ";
b->display(*this, out);
for (void *_b : bounds) {
bound * b = static_cast<bound*>(_b);
b->display(*this, out << "\n");
}
}
template<typename Ext>
void theory_arith<Ext>::display_interval(std::ostream & out, interval const& i) {
i.display(out);
display_deps(out << " lo:", i.get_lower_dependencies());
display_deps(out << " hi:", i.get_upper_dependencies());
display_deps(out << "\nlo:", i.get_lower_dependencies());
display_deps(out << "\nhi:", i.get_upper_dependencies());
}
template<typename Ext>
void theory_arith<Ext>::display_atoms(std::ostream & out) const {
out << "atoms:\n";
for (unsigned i = 0; i < m_atoms.size(); i++)
display_atom(out, m_atoms[i], false);
for (atom * a : m_atoms)
display_atom(out, a, false);
}
template<typename Ext>

88
src/smt/theory_bv.cpp
View file

@ -138,9 +138,9 @@ namespace smt {
void theory_bv::process_args(app * n) {
context & ctx = get_context();
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++)
ctx.internalize(n->get_arg(i), false);
for (expr* arg : *n) {
ctx.internalize(arg, false);
}
}
enode * theory_bv::mk_enode(app * n) {
@ -185,11 +185,9 @@ namespace smt {
void theory_bv::get_bits(theory_var v, expr_ref_vector & r) {
context & ctx = get_context();
literal_vector & bits = m_bits[v];
literal_vector::const_iterator it = bits.begin();
literal_vector::const_iterator end = bits.end();
for (; it != end; ++it) {
for (literal lit : bits) {
expr_ref l(get_manager());
ctx.literal2expr(*it, l);
ctx.literal2expr(lit, l);
r.push_back(l);
}
}
@ -358,18 +356,16 @@ namespace smt {
void mark_bits(conflict_resolution & cr, literal_vector const & bits) {
context & ctx = cr.get_context();
literal_vector::const_iterator it = bits.begin();
literal_vector::const_iterator end = bits.end();
for (; it != end; ++it) {
if (it->var() != true_bool_var) {
if (ctx.get_assignment(*it) == l_true)
cr.mark_literal(*it);
for (literal lit : bits) {
if (lit.var() != true_bool_var) {
if (ctx.get_assignment(lit) == l_true)
cr.mark_literal(lit);
else
cr.mark_literal(~(*it));
cr.mark_literal(~lit);
}
}
}
void get_proof(conflict_resolution & cr, literal l, ptr_buffer<proof> & prs, bool & visited) {
if (l.var() == true_bool_var)
return;
@ -830,10 +826,9 @@ namespace smt {
while (i > 0) {
i--;
theory_var arg = get_arg_var(e, i);
literal_vector::const_iterator it = m_bits[arg].begin();
literal_vector::const_iterator end = m_bits[arg].end();
for (; it != end; ++it)
add_bit(v, *it);
for (literal lit : m_bits[arg]) {
add_bit(v, lit);
}
}
find_wpos(v);
}
@ -1308,10 +1303,9 @@ namespace smt {
theory_var v = e->get_th_var(get_id());
if (v != null_theory_var) {
literal_vector & bits = m_bits[v];
literal_vector::iterator it = bits.begin();
literal_vector::iterator end = bits.end();
for (; it != end; ++it)
ctx.mark_as_relevant(*it);
for (literal lit : bits) {
ctx.mark_as_relevant(lit);
}
}
}
}
@ -1463,35 +1457,27 @@ namespace smt {
SASSERT(bv_size == get_bv_size(r2));
m_merge_aux[0].reserve(bv_size+1, null_theory_var);
m_merge_aux[1].reserve(bv_size+1, null_theory_var);
#define RESET_MERGET_AUX() { \
zero_one_bits::iterator it = bits1.begin(); \
zero_one_bits::iterator end = bits1.end(); \
for (; it != end; ++it) \
m_merge_aux[it->m_is_true][it->m_idx] = null_theory_var; \
}
#define RESET_MERGET_AUX() for (auto & zo : bits1) m_merge_aux[zo.m_is_true][zo.m_idx] = null_theory_var;
DEBUG_CODE(for (unsigned i = 0; i < bv_size; i++) { SASSERT(m_merge_aux[0][i] == null_theory_var || m_merge_aux[1][i] == null_theory_var); });
// save info about bits1
zero_one_bits::iterator it = bits1.begin();
zero_one_bits::iterator end = bits1.end();
for (; it != end; ++it)
m_merge_aux[it->m_is_true][it->m_idx] = it->m_owner;
for (auto & zo : bits1) m_merge_aux[zo.m_is_true][zo.m_idx] = zo.m_owner;
// check if bits2 is consistent with bits1, and copy new bits to bits1
it = bits2.begin();
end = bits2.end();
for (; it != end; ++it) {
theory_var v2 = it->m_owner;
theory_var v1 = m_merge_aux[!it->m_is_true][it->m_idx];
for (auto & zo : bits2) {
theory_var v2 = zo.m_owner;
theory_var v1 = m_merge_aux[!zo.m_is_true][zo.m_idx];
if (v1 != null_theory_var) {
// conflict was detected ... v1 and v2 have complementary bits
SASSERT(m_bits[v1][it->m_idx] == ~(m_bits[v2][it->m_idx]));
SASSERT(m_bits[v1][zo.m_idx] == ~(m_bits[v2][zo.m_idx]));
SASSERT(m_bits[v1].size() == m_bits[v2].size());
mk_new_diseq_axiom(v1, v2, it->m_idx);
mk_new_diseq_axiom(v1, v2, zo.m_idx);
RESET_MERGET_AUX();
return false;
}
if (m_merge_aux[it->m_is_true][it->m_idx] == null_theory_var) {
if (m_merge_aux[zo.m_is_true][zo.m_idx] == null_theory_var) {
// copy missing variable to bits1
bits1.push_back(*it);
bits1.push_back(zo);
}
}
// reset m_merge_aux vector
@ -1614,11 +1600,9 @@ namespace smt {
out << std::right << ", bits:";
context & ctx = get_context();
literal_vector const & bits = m_bits[v];
literal_vector::const_iterator it = bits.begin();
literal_vector::const_iterator end = bits.end();
for (; it != end; ++it) {
for (literal lit : bits) {
out << " ";
ctx.display_literal(out, *it);
ctx.display_literal(out, lit);
}
numeral val;
if (get_fixed_value(v, val))
@ -1740,13 +1724,11 @@ namespace smt {
SASSERT(_bits.size() == num_bits);
svector<bool> already_found;
already_found.resize(bv_sz, false);
zero_one_bits::const_iterator it = _bits.begin();
zero_one_bits::const_iterator end = _bits.end();
for (; it != end; ++it) {
SASSERT(find(it->m_owner) == v);
SASSERT(bits[it->m_is_true][it->m_idx]);
SASSERT(!already_found[it->m_idx]);
already_found[it->m_idx] = true;
for (auto & zo : _bits) {
SASSERT(find(zo.m_owner) == v);
SASSERT(bits[zo.m_is_true][zo.m_idx]);
SASSERT(!already_found[zo.m_idx]);
already_found[zo.m_idx] = true;
}
}
return true;

30
src/smt/theory_lra.cpp
View file

@ -516,7 +516,7 @@ class theory_lra::imp {
rational r1;
v = mk_var(t);
svector<lp::var_index> vars;
ptr_vector<expr> todo;
ptr_buffer<expr> todo;
todo.push_back(t);
while (!todo.empty()) {
expr* n = todo.back();
@ -536,7 +536,7 @@ class theory_lra::imp {
vars.push_back(get_var_index(mk_var(n)));
}
}
TRACE("arith", tout << mk_pp(t, m) << " " << _has_var << "\n";);
TRACE("arith", tout << "v" << v << "(" << get_var_index(v) << ") := " << mk_pp(t, m) << " " << _has_var << "\n";);
if (!_has_var) {
ensure_nra();
m_nra->add_monomial(get_var_index(v), vars.size(), vars.c_ptr());
@ -1190,12 +1190,12 @@ public:
if (m_solver->is_term(wi)) {
const lp::lar_term& term = m_solver->get_term(wi);
result += term.m_v * coeff;
for (const auto & i : term.m_coeffs) {
if (m_variable_values.count(i.first) > 0) {
result += m_variable_values[i.first] * coeff * i.second;
for (const auto & i : term) {
if (m_variable_values.count(i.var()) > 0) {
result += m_variable_values[i.var()] * coeff * i.coeff();
}
else {
m_todo_terms.push_back(std::make_pair(i.first, coeff * i.second));
m_todo_terms.push_back(std::make_pair(i.var(), coeff * i.coeff()));
}
}
}
@ -1481,7 +1481,7 @@ public:
}
if (!m_nra) return l_true;
if (!m_nra->need_check()) return l_true;
m_a1 = 0; m_a2 = 0;
m_a1 = nullptr; m_a2 = nullptr;
lbool r = m_nra->check(m_explanation);
m_a1 = alloc(scoped_anum, m_nra->am());
m_a2 = alloc(scoped_anum, m_nra->am());
@ -2153,8 +2153,8 @@ public:
vi = m_todo_vars.back();
m_todo_vars.pop_back();
lp::lar_term const& term = m_solver->get_term(vi);
for (auto const& coeff : term.m_coeffs) {
lp::var_index wi = coeff.first;
for (auto const& coeff : term) {
lp::var_index wi = coeff.var();
if (m_solver->is_term(wi)) {
m_todo_vars.push_back(wi);
}
@ -2605,19 +2605,23 @@ public:
m_todo_terms.push_back(std::make_pair(vi, rational::one()));
TRACE("arith", tout << "v" << v << " := w" << vi << "\n";
m_solver->print_term(m_solver->get_term(vi), tout); tout << "\n";);
m_nra->am().set(r, 0);
while (!m_todo_terms.empty()) {
rational wcoeff = m_todo_terms.back().second;
// lp::var_index wi = m_todo_terms.back().first; // todo : got a warning "wi is not used"
vi = m_todo_terms.back().first;
m_todo_terms.pop_back();
lp::lar_term const& term = m_solver->get_term(vi);
TRACE("arith", m_solver->print_term(term, tout); tout << "\n";);
scoped_anum r1(m_nra->am());
rational c1 = term.m_v * wcoeff;
m_nra->am().set(r1, c1.to_mpq());
m_nra->am().add(r, r1, r);
for (auto const coeff : term.m_coeffs) {
lp::var_index wi = coeff.first;
c1 = coeff.second * wcoeff;
for (auto const & arg : term) {
lp::var_index wi = m_solver->local2external(arg.var());
c1 = arg.coeff() * wcoeff;
if (m_solver->is_term(wi)) {
m_todo_terms.push_back(std::make_pair(wi, c1));
}

46
src/smt/theory_seq.cpp
View file

@ -889,38 +889,35 @@ bool theory_seq::branch_quat_variable(eq const& e) {
return true;
}
void theory_seq::len_offset(expr* const& e, rational val) {
void theory_seq::len_offset(expr* e, rational val) {
context & ctx = get_context();
expr *l1 = nullptr, *l2 = nullptr, *l21 = nullptr, *l22 = nullptr;
rational fact;
if (m_autil.is_add(e, l1, l2) && m_autil.is_mul(l2, l21, l22) &&
m_autil.is_numeral(l21, fact) && fact.is_minus_one()) {
m_autil.is_numeral(l21, fact) && fact.is_minus_one()) {
if (ctx.e_internalized(l1) && ctx.e_internalized(l22)) {
enode* r1 = ctx.get_enode(l1)->get_root(), *n1 = r1;
enode* r2 = ctx.get_enode(l22)->get_root(), *n2 = r2;
expr *e1 = nullptr, *e2 = nullptr;
do {
if (!m_util.str.is_length(n1->get_owner(), e1))
n1 = n1->get_next();
else
if (m_util.str.is_length(n1->get_owner(), e1))
break;
n1 = n1->get_next();
}
while (n1 != r1);
do {
if (!m_util.str.is_length(n2->get_owner(), e2))
n2 = n2->get_next();
else
if (m_util.str.is_length(n2->get_owner(), e2))
break;
n2 = n2->get_next();
}
while (n2 != r2);
obj_map<enode, int> tmp;
if (m_util.str.is_length(n1->get_owner(), e1)
&& m_util.str.is_length(n2->get_owner(), e2)) {
obj_map<enode, int> tmp;
m_len_offset.find(r1, tmp);
&& m_util.str.is_length(n2->get_owner(), e2) &&
m_len_offset.find(r1, tmp)) {
tmp.insert(r2, val.get_int32());
m_len_offset.insert(r1, tmp);
TRACE("seq", tout << "a length pair: " << mk_pp(e1, m)
<< ", " << mk_pp(e2, m) << "\n";);
TRACE("seq", tout << "a length pair: " << mk_pp(e1, m) << ", " << mk_pp(e2, m) << "\n";);
return;
}
}
@ -1307,32 +1304,34 @@ bool theory_seq::len_based_split(eq const& e) {
y12 = mk_concat(Z, y12);
}
}
else
lenY11 = m_util.str.mk_length(y11);
else {
lenY11 = m_util.str.mk_length(y11);
}
dependency* dep = e.dep();
literal_vector lits;
literal lit1 = mk_eq(lenX11, lenY11, false);
if (ctx.get_assignment(lit1) != l_true) {
return false;
}
lits.push_back(lit1);
if (ls.size()>=2 && rs.size()>=2 && (ls.size()>2 || rs.size()>2)) {
if (ls.size() >= 2 && rs.size() >= 2 && (ls.size() > 2 || rs.size() > 2)) {
expr_ref len1(m_autil.mk_int(0),m), len2(m_autil.mk_int(0),m);
for (unsigned i = 2; i < ls.size(); ++i)
len1 = mk_add(len1, m_util.str.mk_length(ls[i]));
for (unsigned i = 2; i < rs.size(); ++i)
len2 = mk_add(len2, m_util.str.mk_length(rs[i]));
bool flag = false;
literal lit2;
if (!m_autil.is_numeral(len1) && !m_autil.is_numeral(len2)) {
literal lit2 = mk_eq(len1, len2, false);
flag = ctx.get_assignment(lit2) == l_true;
lit2 = mk_eq(len1, len2, false);
}
else {
expr_ref eq_len(m.mk_eq(len1, len2), m);
flag = ctx.find_assignment(eq_len) == l_true;
lit2 = mk_literal(eq_len);
}
if (flag) {
literal lit2 = mk_eq(len1, len2, false);
if (ctx.get_assignment(lit2) == l_true) {
lits.push_back(lit2);
TRACE("seq", tout << mk_pp(len1, m) << " = " << mk_pp(len2, m) << "\n";);
expr_ref lhs(m), rhs(m);
@ -5277,9 +5276,10 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) {
void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
enode* n1 = get_enode(v1);
enode* n2 = get_enode(v2);
enode* n2 = get_enode(v2);
expr_ref e1(n1->get_owner(), m);
expr_ref e2(n2->get_owner(), m);
SASSERT(n1->get_root() != n2->get_root());
m_exclude.update(e1, e2);
expr_ref eq(m.mk_eq(e1, e2), m);
TRACE("seq", tout << "new disequality " << get_context().get_scope_level() << ": " << eq << "\n";);

2
src/smt/theory_seq.h
View file

@ -375,7 +375,7 @@ namespace smt {
void init_model(expr_ref_vector const& es);
void len_offset(expr* const& e, rational val);
void len_offset(expr* e, rational val);
void prop_arith_to_len_offset();
int find_fst_non_empty_idx(expr_ref_vector const& x) const;
expr* find_fst_non_empty_var(expr_ref_vector const& x) const;

1
src/util/lp/int_solver.h
View file

@ -50,7 +50,6 @@ public:
// main function to check that the solution provided by lar_solver is valid for integral values,
// or provide a way of how it can be adjusted.
lia_move check(lar_term& t, mpq& k, explanation& ex, bool & upper);
lia_move check_(lar_term& t, mpq& k, explanation& ex, bool & upper);
bool move_non_basic_column_to_bounds(unsigned j);
lia_move check_wrapper(lar_term& t, mpq& k, explanation& ex);
bool is_base(unsigned j) const;

2
src/util/lp/lar_solver.cpp
View file

@ -540,11 +540,13 @@ lp_status lar_solver::maximize_term(unsigned ext_j,
if (m_int_solver->is_base(j)) {
if (!remove_from_basis(j)) { // consider a special version of remove_from_basis that would not remove inf_int columns
m_mpq_lar_core_solver.m_r_x = backup;
term_max = prev_value;
return lp_status::FEASIBLE; // it should not happen
}
}
m_int_solver->patch_nbasic_column(j, false);
if (!column_value_is_integer(j)) {
term_max = prev_value;
m_mpq_lar_core_solver.m_r_x = backup;
return lp_status::FEASIBLE;
}

2
src/util/lp/lar_solver.h
View file

@ -247,6 +247,8 @@ public:
void calculate_implied_bounds_for_row(unsigned i, bound_propagator & bp);
unsigned adjust_column_index_to_term_index(unsigned j) const;
var_index local2external(var_index idx) const { return m_var_register.local_to_external(idx); }
void propagate_bounds_on_a_term(const lar_term& t, bound_propagator & bp, unsigned term_offset);

21
src/util/lp/lia_move.h
View file

@ -28,4 +28,25 @@ enum class lia_move {
undef,
unsat
};
inline std::string lia_move_to_string(lia_move m) {
switch (m) {
case lia_move::sat:
return "sat";
case lia_move::branch:
return "branch";
case lia_move::cut:
return "cut";
case lia_move::conflict:
return "conflict";
case lia_move::continue_with_check:
return "continue_with_check";
case lia_move::undef:
return "undef";
case lia_move::unsat:
return "unsat";
default:
lp_assert(false);
};
return "strange";
}
}

13
src/util/lp/nra_solver.cpp
View file

@ -24,11 +24,12 @@ namespace nra {
lp::lar_solver& s;
reslimit& m_limit;
params_ref m_params;
u_map<polynomial::var> m_lp2nl; // map from lar_solver variables to nlsat::solver variables
u_map<polynomial::var> m_lp2nl; // map from lar_solver variables to nlsat::solver variables
scoped_ptr<nlsat::solver> m_nlsat;
scoped_ptr<scoped_anum> m_zero;
vector<mon_eq> m_monomials;
unsigned_vector m_monomials_lim;
mutable std::unordered_map<lp::var_index, rational> m_variable_values; // current model
mutable std::unordered_map<lp::var_index, rational> m_variable_values; // current model
imp(lp::lar_solver& s, reslimit& lim, params_ref const& p):
s(s),
@ -90,6 +91,7 @@ namespace nra {
lbool check(lp::explanation_t& ex) {
SASSERT(need_check());
m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
m_zero = alloc(scoped_anum, am());
m_lp2nl.reset();
vector<nlsat::assumption, false> core;
@ -208,12 +210,17 @@ namespace nra {
if (!m_lp2nl.find(v, r)) {
r = m_nlsat->mk_var(is_int(v));
m_lp2nl.insert(v, r);
TRACE("arith", tout << "v" << v << " := x" << r << "\n";);
}
return r;
}
nlsat::anum const& value(lp::var_index v) const {
return m_nlsat->value(m_lp2nl.find(v));
polynomial::var pv;
if (m_lp2nl.find(v, pv))
return m_nlsat->value(pv);
else
return *m_zero;
}
nlsat::anum_manager& am() {