mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-07 00:11:55 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-11-10 03:03:23 -08:00
commit 733f44d141
151 changed files with 3249 additions and 1504 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/mam.cpp
View file

@ -2091,7 +2091,6 @@ namespace {
enode * n = m_registers[j2->m_reg]->get_root();
if (n->get_num_parents() == 0)
return nullptr;
unsigned num_args = n->get_num_args();
enode_vector * v = mk_enode_vector();
enode_vector::const_iterator it1 = n->begin_parents();
enode_vector::const_iterator end1 = n->end_parents();

7
src/smt/seq_eq_solver.cpp
View file

@ -684,11 +684,12 @@ bool theory_seq::branch_quat_variable(depeq const& e) {
cond = true;
}
// xs and ys cannot align
else if (!can_align_from_lhs(xs, ys) && !can_align_from_rhs(xs, ys))
else if (!can_align_from_lhs(xs, ys) && !can_align_from_rhs(xs, ys) && !can_align_from_lhs(ys, xs) && !can_align_from_rhs(ys, xs))
cond = true;
if (!cond)
return false;
literal_vector lits;
if (xs == ys) {
@ -724,7 +725,7 @@ bool theory_seq::branch_quat_variable(depeq const& e) {
}
}
else {
TRACE("seq", tout << mk_pp(x1, m) << " > " << mk_pp(y1, m) << "\n";);
TRACE("seq", tout << mk_pp(x1, m) << " >\n" << mk_pp(y1, m) << "\n";);
if (ctx.get_assignment(lit3) == l_undef) {
ctx.mark_as_relevant(lit3);
return true;
@ -1144,7 +1145,7 @@ bool theory_seq::solve_nth_eq(expr_ref_vector const& ls, expr_ref_vector const&
m.inc_ref(rhs);
m.inc_ref(ls[0]);
m_nth_eq2_cache.insert(std::make_pair(rhs, ls[0]));
ctx.push_trail(remove_obj_pair_map(m, m_nth_eq2_cache, rhs, ls[0]));
get_trail_stack().push(remove_obj_pair_map(m, m_nth_eq2_cache, rhs, ls[0]));
ls1.push_back(s);
if (!idx_is_zero) rs1.push_back(m_sk.mk_pre(s, idx));
rs1.push_back(m_util.str.mk_unit(rhs));

2
src/smt/seq_offset_eq.h
View file

@ -42,7 +42,7 @@ namespace smt {
seq_offset_eq(theory& th, ast_manager& m);
bool empty() const { return m_offset_equalities.empty(); }
/**
\breif determine if r1 = r2 + offset
\brief determine if r1 = r2 + offset
*/
bool find(enode* r1, enode* r2, int& offset) const;
bool contains(enode* r1, enode* r2) const { int offset = 0; return find(r1, r2, offset); }

209
src/smt/seq_regex.cpp
View file

@ -12,6 +12,7 @@ Abstract:
Author:
Nikolaj Bjorner (nbjorner) 2020-5-22
Margus Veanes 2021
--*/
@ -253,10 +254,8 @@ namespace smt {
* (accept s (i + 1) (derivative s[i] r)
*
* Acceptance of a derivative is unfolded into a disjunction over
* all derivatives. Effectively, this implements the following rule,
* but all in one step:
* (accept s i (ite c r1 r2)) =>
* c & (accept s i r1) \/ ~c & (accept s i r2)
* all derivatives. Effectively, this implements the following rule:
* (accept s i (ite c r1 r2)) => (ite c (accept s i r1) (accept s i r2))
*/
void seq_regex::propagate_accept(literal lit) {
SASSERT(!lit.sign());
@ -302,6 +301,7 @@ namespace smt {
unsigned min_len = re().min_length(r);
unsigned min_len_plus_i = u().max_plus(min_len, idx);
literal len_s_ge_min = th.m_ax.mk_ge(th.mk_len(s), min_len_plus_i);
// Acc(s,i,r) ==> |s| >= i + minlength(r)
th.propagate_lit(nullptr, 1, &lit, len_s_ge_min);
// Axiom equivalent to the above: th.add_axiom(~lit, len_s_ge_min);
@ -316,6 +316,8 @@ namespace smt {
STRACE("seq_regex_brief", tout
<< " (Warning: min_length returned 0 for"
<< " non-nullable regex)";);
// since nullable(r) = false:
// Acc(s,i,r) ==> |s|>i
th.propagate_lit(nullptr, 1, &lit, ~len_s_le_i);
}
else if (!m.is_true(is_nullable)) {
@ -327,7 +329,9 @@ namespace smt {
<< " (Warning: is_nullable did not simplify)";);
literal is_nullable_lit = th.mk_literal(is_nullable);
ctx.mark_as_relevant(is_nullable_lit);
// Acc(s,i,r) & |s|<=i ==> nullable(r)
th.add_axiom(~lit, ~len_s_le_i, is_nullable_lit);
//TODO: what if is_nullable contains an in_re
if (str().is_in_re(is_nullable))
th.add_unhandled_expr(is_nullable);
}
@ -335,14 +339,19 @@ namespace smt {
// Rule 3: derivative unfolding
literal_vector accept_next;
expr_ref hd = th.mk_nth(s, i);
expr_ref s_i = th.mk_nth(s, i);
expr_ref deriv(m);
deriv = derivative_wrapper(hd, r);
deriv = mk_derivative_wrapper(s_i, r);
STRACE("seq_regex", tout
<< "mk_derivative_wrapper: " << re().to_str(deriv) << std::endl;);
expr_ref accept_deriv(m);
accept_deriv = mk_deriv_accept(s, idx + 1, deriv);
accept_next.push_back(~lit);
accept_next.push_back(len_s_le_i);
accept_next.push_back(th.mk_literal(accept_deriv));
// Acc(s, i, r) => (|s|<=i or Acc(s, i+1, D(s_i,r)))
// where Acc(s, i+1, ite(c, t, f)) = ite(c, Acc(s, i+1, t), Acc(s, i+1, t))
// and Acc(s, i+1, r U s) = Acc(s, i+1, r) or Acc(s, i+1, s)
th.add_axiom(accept_next);
}
@ -418,20 +427,21 @@ namespace smt {
/*
Wrapper around calls to is_nullable from the seq rewriter.
Note: the nullable wrapper and derivative wrapper actually use
TODO: clean up the following:
Note: the is_nullable_wrapper and mk_derivative_wrapper actually use
different sequence rewriters; these are at:
m_seq_rewrite
(returned by seq_rw())
th.m_rewrite.m_imp->m_cfg.m_seq_rw
(private, can't be accessed directly)
As a result operations are cached separately for the nullable
and derivative calls. TBD if caching them using the same rewriter
makes any difference.
and derivative calls.
*/
expr_ref seq_regex::is_nullable_wrapper(expr* r) {
STRACE("seq_regex", tout << "nullable: " << mk_pp(r, m) << std::endl;);
expr_ref result = seq_rw().is_nullable(r);
//TODO: rewrite seems unnecessary here
rewrite(result);
STRACE("seq_regex", tout << "nullable result: " << mk_pp(result, m) << std::endl;);
@ -442,39 +452,28 @@ namespace smt {
}
/*
Wrapper around the regex symbolic derivative from the seq rewriter.
Ensures that the derivative is written in a normalized BDD form
with optimizations for if-then-else expressions involving the head.
Note: the nullable wrapper and derivative wrapper actually use
different sequence rewriters; these are at:
m_seq_rewrite
(returned by seq_rw())
th.m_rewrite.m_imp->m_cfg.m_seq_rw
(private, can't be accessed directly)
As a result operations are cached separately for the nullable
and derivative calls. TBD if caching them using the same rewriter
makes any difference.
First creates a derivatrive of r wrt x=(:var 0) and then replaces x by ele.
This will create a cached entry for the generic derivative of r that is independent of ele.
*/
expr_ref seq_regex::derivative_wrapper(expr* hd, expr* r) {
STRACE("seq_regex", tout << "derivative(" << mk_pp(hd, m) << "): " << mk_pp(r, m) << std::endl;);
expr_ref seq_regex::mk_derivative_wrapper(expr* ele, expr* r) {
STRACE("seq_regex", tout << "derivative(" << mk_pp(ele, m) << "): " << mk_pp(r, m) << std::endl;);
// Use canonical variable for head
expr_ref hd_canon(m.mk_var(0, hd->get_sort()), m);
expr_ref result(re().mk_derivative(hd_canon, r), m);
rewrite(result);
// Uses canonical variable (:var 0) for the derivative element
expr_ref der(seq_rw().mk_derivative(r), m);
// Substitute with real head
// Substitute (:var 0) with the actual element
var_subst subst(m);
expr_ref_vector sub(m);
sub.push_back(hd);
result = subst(result, sub);
sub.push_back(ele);
der = subst(der, sub);
STRACE("seq_regex", tout << "derivative result: " << mk_pp(result, m) << std::endl;);
STRACE("seq_regex", tout << "derivative result: " << mk_pp(der, m) << std::endl;);
STRACE("seq_regex_brief", tout << "d(" << state_str(r) << ")="
<< state_str(result) << " ";);
<< state_str(der) << " ";);
return result;
//TODO: simplify der further, if ele implies further simplifications
//e.g. if ele='b' then de(ite (x='a') t f) simplifies to t
return der;
}
void seq_regex::propagate_eq(expr* r1, expr* r2) {
@ -557,7 +556,7 @@ namespace smt {
literal null_lit = th.mk_literal(is_nullable);
expr_ref hd = mk_first(r, n);
expr_ref d(m);
d = derivative_wrapper(hd, r);
d = mk_derivative_wrapper(hd, r);
literal_vector lits;
lits.push_back(~lit);
@ -584,11 +583,10 @@ namespace smt {
}
/*
Given a string s, index i, and a derivative regex d, return an
Given a string s, index i, and a derivative r, return an
expression that is equivalent to
accept s i r
but which pushes accept s i r into the leaves (next derivatives to
explore).
but which pushes accept s i r into the leaves
Input r is of type regex; output is of type bool.
@ -600,14 +598,18 @@ namespace smt {
expr_ref seq_regex::mk_deriv_accept(expr* s, unsigned i, expr* r) {
vector<expr*> to_visit;
to_visit.push_back(r);
obj_map<expr, expr*> re_to_bool;
obj_map<expr, expr*> re_to_accept;
expr_ref_vector _temp_bool_owner(m); // temp owner for bools we create
// DFS
bool s_is_longer_than_i = str().min_length(s) > i;
expr* i_int = a().mk_int(i);
_temp_bool_owner.push_back(i_int);
// DFS, avoids duplicating derivative construction that has already been done
while (to_visit.size() > 0) {
expr* e = to_visit.back();
expr* econd = nullptr, *e1 = nullptr, *e2 = nullptr;
if (!re_to_bool.contains(e)) {
if (!re_to_accept.contains(e)) {
// First visit: add children
STRACE("seq_regex_verbose", tout << "1";);
if (m.is_ite(e, econd, e1, e2) ||
@ -616,36 +618,40 @@ namespace smt {
to_visit.push_back(e2);
}
// Mark first visit by adding nullptr to the map
re_to_bool.insert(e, nullptr);
re_to_accept.insert(e, nullptr);
}
else if (re_to_bool.find(e) == nullptr) {
else if (re_to_accept.find(e) == nullptr) {
// Second visit: set value
STRACE("seq_regex_verbose", tout << "2";);
to_visit.pop_back();
if (m.is_ite(e, econd, e1, e2)) {
expr* b1 = re_to_bool.find(e1);
expr* b2 = re_to_bool.find(e2);
expr* b = m.mk_ite(econd, b1, b2);
expr* b1 = re_to_accept.find(e1);
expr* b2 = re_to_accept.find(e2);
expr* b = m.is_true(econd) || b1 == b2 ? b1 : m.is_false(econd) ? b2 : m.mk_ite(econd, b1, b2);
_temp_bool_owner.push_back(b);
re_to_bool.find(e) = b;
re_to_accept.find(e) = b;
}
else if (re().is_empty(e) || (s_is_longer_than_i && re().is_epsilon(e)))
{
// s[i..] in [] <==> false, also: s[i..] in () <==> false when |s|>i
re_to_accept.find(e) = m.mk_false();
}
else if (re().is_full_seq(e) || (s_is_longer_than_i && re().is_dot_plus(e)))
{
// s[i..] in .* <==> true, also: s[i..] in .+ <==> true when |s|>i
re_to_accept.find(e) = m.mk_true();
}
/*
else if (re().is_empty(e))
{
re_to_bool.find(e) = m.mk_false();
}
else if (re().is_epsilon(e))
{
expr* iplus1 = a().mk_int(i);
expr* one = a().mk_int(1);
_temp_bool_owner.push_back(iplus1);
_temp_bool_owner.push_back(one);
//the substring starting after position iplus1 must be empty
expr* s_end = str().mk_substr(s, iplus1, one);
//the substring starting after position i must be empty
expr* s_end = str().mk_substr(s, i_int, one);
expr* s_end_is_epsilon = m.mk_eq(s_end, str().mk_empty(m.get_sort(s)));
_temp_bool_owner.push_back(s_end_is_epsilon);
re_to_bool.find(e) = s_end_is_epsilon;
re_to_accept.find(e) = s_end_is_epsilon;
STRACE("seq_regex_verbose", tout
<< "added empty sequence leaf: "
@ -653,18 +659,16 @@ namespace smt {
}
*/
else if (re().is_union(e, e1, e2)) {
expr* b1 = re_to_bool.find(e1);
expr* b2 = re_to_bool.find(e2);
expr* b = m.mk_or(b1, b2);
expr* b1 = re_to_accept.find(e1);
expr* b2 = re_to_accept.find(e2);
expr* b = m.is_false(b1) || b1 == b2 ? b2 : m.is_false(b2) ? b1 : m.mk_or(b1, b2);
_temp_bool_owner.push_back(b);
re_to_bool.find(e) = b;
re_to_accept.find(e) = b;
}
else {
expr* iplus1 = a().mk_int(i);
_temp_bool_owner.push_back(iplus1);
expr_ref acc_leaf = sk().mk_accept(s, iplus1, e);
expr_ref acc_leaf = sk().mk_accept(s, i_int, e);
_temp_bool_owner.push_back(acc_leaf);
re_to_bool.find(e) = acc_leaf;
re_to_accept.find(e) = acc_leaf;
STRACE("seq_regex_verbose", tout
<< "mk_deriv_accept: added accept leaf: "
@ -680,59 +684,44 @@ namespace smt {
// Finalize
expr_ref result(m);
result = re_to_bool.find(r); // Assigns ownership of all exprs in
// re_to_bool for after this completes
result = re_to_accept.find(r); // Assigns ownership of all exprs in
// re_to_accept for after this completes
rewrite(result);
return result;
}
/*
Return a list of all leaves in the derivative of a regex r,
Return a list of all target regexes in the derivative of a regex r,
ignoring the conditions along each path.
Warning: Although the derivative
normal form tries to eliminate unsat condition paths, one cannot
assume that the path to each leaf is satisfiable in general
(e.g. when regexes are created using re.pred).
So not all results may correspond to satisfiable predicates.
It is OK to rely on the results being satisfiable for completeness,
but not soundness.
The derivative construction uses (:var 0) and tries
to eliminate unsat condition paths but it does not perform
full satisfiability checks and it is not guaranteed
that all targets are actually reachable
*/
void seq_regex::get_all_derivatives(expr* r, expr_ref_vector& results) {
// Get derivative
sort* seq_sort = nullptr;
VERIFY(u().is_re(r, seq_sort));
expr_ref n(m.mk_fresh_const("re.char", seq_sort), m);
expr_ref hd = mk_first(r, n);
expr_ref d(m);
d = derivative_wrapper(hd, r);
void seq_regex::get_derivative_targets(expr* r, expr_ref_vector& targets) {
// constructs the derivative wrt (:var 0)
expr_ref d(seq_rw().mk_derivative(r), m);
// DFS
vector<expr*> to_visit;
to_visit.push_back(d);
obj_map<expr, bool> visited; // set<expr> (bool is used as a unit type)
while (to_visit.size() > 0) {
expr* e = to_visit.back();
to_visit.pop_back();
if (visited.contains(e)) continue;
visited.insert(e, true);
expr* econd = nullptr, *e1 = nullptr, *e2 = nullptr;
if (m.is_ite(e, econd, e1, e2) ||
re().is_union(e, e1, e2)) {
to_visit.push_back(e1);
to_visit.push_back(e2);
}
else if (!re().is_empty(e)) {
results.push_back(e);
STRACE("seq_regex_verbose", tout
<< "get_all_derivatives: added deriv: "
<< mk_pp(e, m) << std::endl;);
// use DFS to collect all the targets (leaf regexes) in d.
expr* _1 = nullptr, * e1 = nullptr, * e2 = nullptr;
obj_hashtable<expr>::entry* _2 = nullptr;
vector<expr*> workset;
workset.push_back(d);
obj_hashtable<expr> done;
done.insert(d);
while (workset.size() > 0) {
expr* e = workset.back();
workset.pop_back();
if (m.is_ite(e, _1, e1, e2) || re().is_union(e, e1, e2)) {
if (done.insert_if_not_there_core(e1, _2))
workset.push_back(e1);
if (done.insert_if_not_there_core(e2, _2))
workset.push_back(e2);
}
else if (!re().is_empty(e))
targets.push_back(e);
}
STRACE("seq_regex", tout << "Number of derivatives: "
<< results.size() << std::endl;);
STRACE("seq_regex_brief", tout << "#derivs=" << results.size() << " ";);
}
/*
@ -800,7 +789,7 @@ namespace smt {
th.add_axiom(~lit, ~th.mk_literal(is_nullable));
expr_ref hd = mk_first(r, n);
expr_ref d(m);
d = derivative_wrapper(hd, r);
d = mk_derivative_wrapper(hd, r);
literal_vector lits;
expr_ref_pair_vector cofactors(m);
get_cofactors(d, cofactors);
@ -884,7 +873,7 @@ namespace smt {
STRACE("state_graph",
if (!m_state_graph.is_seen(r_id))
tout << std::endl << "state(" << r_id << ") = " << seq_util::rex::pp(re(), r) << std::endl << "info(" << r_id << ") = " << re().get_info(r) << std::endl;);
tout << std::endl << "state(" << r_id << ") = " << re().to_str(r) << std::endl << "info(" << r_id << ") = " << re().get_info(r) << std::endl;);
// Add state
m_state_graph.add_state(r_id);
STRACE("seq_regex", tout << "Updating state graph for regex "
@ -900,14 +889,14 @@ namespace smt {
expr_ref_vector derivatives(m);
STRACE("seq_regex_verbose", tout
<< "getting all derivs: " << r_id << " " << std::endl;);
get_all_derivatives(r, derivatives);
get_derivative_targets(r, derivatives);
for (auto const& dr: derivatives) {
unsigned dr_id = get_state_id(dr);
STRACE("seq_regex_verbose", tout
<< std::endl << " traversing deriv: " << dr_id << " ";);
STRACE("state_graph",
if (!m_state_graph.is_seen(dr_id))
tout << "state(" << dr_id << ") = " << seq_util::rex::pp(re(), dr) << std::endl << "info(" << dr_id << ") = " << re().get_info(dr) << std::endl;);
tout << "state(" << dr_id << ") = " << re().to_str(dr) << std::endl << "info(" << dr_id << ") = " << re().get_info(dr) << std::endl;);
// Add state
m_state_graph.add_state(dr_id);
bool maybecycle = can_be_in_cycle(r, dr);

4
src/smt/seq_regex.h
View file

@ -158,12 +158,12 @@ namespace smt {
expr_ref symmetric_diff(expr* r1, expr* r2);
expr_ref is_nullable_wrapper(expr* r);
expr_ref derivative_wrapper(expr* hd, expr* r);
expr_ref mk_derivative_wrapper(expr* hd, expr* r);
// Various support for unfolding derivative expressions that are
// returned by derivative_wrapper
expr_ref mk_deriv_accept(expr* s, unsigned i, expr* r);
void get_all_derivatives(expr* r, expr_ref_vector& results);
void get_derivative_targets(expr* r, expr_ref_vector& targets);
void get_cofactors(expr* r, expr_ref_pair_vector& result);
void get_cofactors_rec(expr* r, expr_ref_vector& conds,
expr_ref_pair_vector& result);

8
src/smt/smt_conflict_resolution.cpp
View file

@ -413,6 +413,7 @@ namespace smt {
// of justification are considered level zero.
if (m_conflict_lvl <= m_ctx.get_search_level()) {
TRACE("conflict", tout << "problem is unsat\n";);
TRACE("conflict", m_ctx.display(tout););
if (m.proofs_enabled())
mk_conflict_proof(conflict, not_l);
if (m_ctx.tracking_assumptions())
@ -473,7 +474,8 @@ namespace smt {
TRACE("conflict",
tout << "new scope level: " << m_new_scope_lvl << "\n";
tout << "intern. scope level: " << m_lemma_iscope_lvl << "\n";);
tout << "intern. scope level: " << m_lemma_iscope_lvl << "\n";
tout << "lemma: " << m_lemma << "\n";);
if (m.proofs_enabled())
mk_conflict_proof(conflict, not_l);
@ -760,6 +762,7 @@ namespace smt {
m_lemma .shrink(j);
m_lemma_atoms.shrink(j);
m_ctx.m_stats.m_num_minimized_lits += sz - j;
TRACE("conflict", tout << "lemma: " << m_lemma << "\n";);
}
/**
@ -1359,9 +1362,8 @@ namespace smt {
void conflict_resolution::process_antecedent_for_unsat_core(literal antecedent) {
bool_var var = antecedent.var();
TRACE("conflict", tout << "processing antecedent: ";
CTRACE("conflict", !m_ctx.is_marked(var), tout << "processing antecedent: ";
m_ctx.display_literal_info(tout << antecedent << " ", antecedent);
tout << (m_ctx.is_marked(var)?"marked":"not marked");
tout << "\n";);
if (!m_ctx.is_marked(var)) {

9
src/smt/smt_context.cpp
View file

@ -34,6 +34,7 @@ Revision History:
#include "smt/smt_context.h"
#include "smt/smt_quick_checker.h"
#include "smt/uses_theory.h"
#include "smt/theory_special_relations.h"
#include "smt/smt_for_each_relevant_expr.h"
#include "smt/smt_model_generator.h"
#include "smt/smt_model_checker.h"
@ -1543,6 +1544,14 @@ namespace smt {
}
}
void context::get_specrels(func_decl_set& rels) const {
family_id fid = m.get_family_id("specrels");
theory* th = get_theory(fid);
if (th)
dynamic_cast<theory_special_relations*>(th)->get_specrels(rels);
}
void context::relevant_eh(expr * n) {
if (b_internalized(n)) {
bool_var v = get_bool_var(n);

6
src/smt/smt_context.h
View file

@ -279,6 +279,9 @@ namespace smt {
return m_app2enode[n->get_id()];
}
void get_specrels(func_decl_set& rels) const;
/**
\brief Similar to get_enode, but returns 0 if n is to e_internalized.
*/
@ -1189,7 +1192,6 @@ namespace smt {
bool more_than_k_unassigned_literals(clause * cls, unsigned k);
void internalize_assertions();
void asserted_inconsistent();
@ -1606,6 +1608,8 @@ namespace smt {
void assert_expr(expr * e, proof * pr);
void internalize_assertions();
void push();
void pop(unsigned num_scopes);

44
src/smt/smt_context_pp.cpp
View file

@ -113,9 +113,17 @@ namespace smt {
}
std::ostream& context::display_literals_smt2(std::ostream& out, unsigned num_lits, literal const* lits) const {
for (unsigned i = 0; i < num_lits; ++i) {
out << literal_vector(num_lits, lits) << ":\n";
#if 1
expr_ref_vector fmls(m);
for (unsigned i = 0; i < num_lits; ++i)
fmls.push_back(literal2expr(lits[i]));
expr_ref c = mk_or(fmls);
out << c << "\n";
#else
for (unsigned i = 0; i < num_lits; ++i)
display_literal_smt2(out, lits[i]) << "\n";
}
#endif
return out;
}
@ -254,22 +262,30 @@ namespace smt {
}
void context::display_eqc(std::ostream & out) const {
bool first = true;
for (enode * x : m_enodes) {
expr * n = x->get_expr();
expr * r = x->get_root()->get_expr();
if (n != r) {
if (first) {
out << "equivalence classes:\n";
first = false;
}
out << "#" << n->get_id() << " -> #" << r->get_id() << ": ";
out << mk_pp(n, m) << " -> " << mk_pp(r, m) << "\n";
if (m_enodes.empty())
return;
unsigned count = 0;
for (enode * r : m_enodes)
if (r->is_root())
++count;
out << "equivalence classes: " << count << "\n";
for (enode * r : m_enodes) {
if (!r->is_root())
continue;
out << "#" << enode_pp(r, *this) << "\n";
if (r->get_class_size() == 1)
continue;
for (enode* n : *r) {
if (n != r)
out << " #" << enode_pp(n, *this) << "\n";
}
}
}
void context::display_app_enode_map(std::ostream & out) const {
return;
// mainly useless
if (!m_e_internalized_stack.empty()) {
out << "expression -> enode:\n";
unsigned sz = m_e_internalized_stack.size();
@ -668,7 +684,7 @@ namespace smt {
std::ostream& operator<<(std::ostream& out, enode_pp const& p) {
ast_manager& m = p.ctx.get_manager();
enode* n = p.n;
return out << "[#" << n->get_owner_id() << " " << mk_bounded_pp(n->get_expr(), m) << "]";
return out << n->get_owner_id() << ": " << mk_bounded_pp(n->get_expr(), m);
}
std::ostream& operator<<(std::ostream& out, enode_eq_pp const& p) {

2
src/smt/smt_enode.cpp
View file

@ -50,7 +50,7 @@ namespace smt {
n->m_lbl_hash = -1;
n->m_proof_is_logged = false;
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
for (unsigned i = 0; i < num_args; i++) {
enode * arg = app2enode[owner->get_arg(i)->get_id()];
n->m_args[i] = arg;
SASSERT(n->get_arg(i) == arg);

2
src/smt/smt_internalizer.cpp
View file

@ -1387,7 +1387,7 @@ namespace smt {
default:
break;
}
TRACE("mk_clause", display_literals_verbose(tout << "after simplification:\n", num_lits, lits) << "\n";);
TRACE("mk_clause", display_literals_verbose(tout << "after simplification: " << literal_vector(num_lits, lits) << "\n", num_lits, lits) << "\n";);
unsigned activity = 1;
bool lemma = is_lemma(k);

14
src/smt/smt_model_finder.cpp
View file

@ -50,6 +50,7 @@ namespace smt {
class evaluator {
public:
virtual ~evaluator() = default;
virtual expr* eval(expr* n, bool model_completion) = 0;
};
@ -401,6 +402,7 @@ namespace smt {
expr_ref_vector* m_new_constraints{ nullptr };
random_gen m_rand;
func_decl_set m_specrels;
void reset_sort2k() {
@ -470,6 +472,7 @@ namespace smt {
ast_manager& get_manager() const { return m; }
void reset() {
m_specrels.reset();
flush_nodes();
m_nodes.reset();
m_next_node_id = 0;
@ -479,6 +482,11 @@ namespace smt {
reset_sort2k();
}
void set_specrels(context& c) {
m_specrels.reset();
c.get_specrels(m_specrels);
}
void set_model(proto_model* m) {
reset_eval_cache();
m_model = m;
@ -1049,9 +1057,13 @@ namespace smt {
*/
void complete_partial_funcs(func_decl_set const& partial_funcs) {
for (func_decl* f : partial_funcs) {
// Complete the current interpretation
m_model->complete_partial_func(f, true);
if (m_specrels.contains(f))
continue;
unsigned arity = f->get_arity();
func_interp* fi = m_model->get_func_interp(f);
if (fi->is_constant())
@ -2399,9 +2411,11 @@ namespace smt {
}
}
void model_finder::process_auf(ptr_vector<quantifier> const& qs, proto_model* mdl) {
m_auf_solver->reset();
m_auf_solver->set_model(mdl);
m_auf_solver->set_specrels(*m_context);
for (quantifier* q : qs) {
quantifier_info* qi = get_quantifier_info(q);

11
src/smt/smt_parallel.cpp
View file

@ -149,21 +149,18 @@ namespace smt {
expr_ref c(pm);
pctx.get_fparams().m_max_conflicts = std::min(thread_max_conflicts, max_conflicts);
if (num_rounds > 0 && (pctx.get_fparams().m_threads_cube_frequency % num_rounds) == 0) {
if (num_rounds > 0 && (pctx.get_fparams().m_threads_cube_frequency % num_rounds) == 0)
cube(pctx, lasms, c);
}
IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i;
if (num_rounds > 0) verbose_stream() << " :round " << num_rounds;
if (c) verbose_stream() << " :cube " << mk_bounded_pp(c, pm, 3);
verbose_stream() << ")\n";);
lbool r = pctx.check(lasms.size(), lasms.data());
if (r == l_undef && pctx.m_num_conflicts >= max_conflicts) {
// no-op
}
else if (r == l_undef && pctx.m_num_conflicts >= thread_max_conflicts) {
if (r == l_undef && pctx.m_num_conflicts >= max_conflicts)
; // no-op
else if (r == l_undef && pctx.m_num_conflicts >= thread_max_conflicts)
return;
}
else if (r == l_false && pctx.unsat_core().contains(c)) {
IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i << " :learn " << mk_bounded_pp(c, pm, 3) << ")");
pctx.assert_expr(mk_not(mk_and(pctx.unsat_core())));

4
src/smt/smt_relevancy.h
View file

@ -169,12 +169,12 @@ namespace smt {
bool enabled() const;
/**
\Brief Return the region allocator for the smt::context that owns this propagator.
\brief Return the region allocator for the smt::context that owns this propagator.
*/
region & get_region() const;
/**
\Brief Return the ast_manager for the smt::context that owns this propagator.
\brief Return the ast_manager for the smt::context that owns this propagator.
*/
ast_manager & get_manager() const;

5
src/smt/smt_theory.cpp
View file

@ -208,10 +208,11 @@ namespace smt {
}
void theory::log_axiom_instantiation(app * r, unsigned axiom_id, unsigned num_bindings, app * const * bindings, unsigned pattern_id, const vector<std::tuple<enode *, enode *>> & used_enodes) {
ast_manager & m = get_manager();
app_ref _r(r, m);
ast_manager & m = get_manager();
SASSERT(r->get_ref_count() > 0);
std::ostream& out = m.trace_stream();
symbol const & family_name = m.get_family_name(get_family_id());
if (pattern_id == UINT_MAX) {
out << "[inst-discovered] theory-solving " << static_cast<void *>(nullptr) << " " << family_name << "#";
if (axiom_id != UINT_MAX)

4
src/smt/smt_theory.h
View file

@ -453,9 +453,6 @@ namespace smt {
std::ostream& display_flat_app(std::ostream & out, app * n) const;
std::ostream& display_var_def(std::ostream & out, theory_var v) const { return display_app(out, get_enode(v)->get_expr()); }
std::ostream& display_var_flat_def(std::ostream & out, theory_var v) const { return display_flat_app(out, get_enode(v)->get_expr()); }
protected:
void log_axiom_instantiation(app * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0,
@ -481,6 +478,7 @@ namespace smt {
}
void log_axiom_unit(app* r) {
expr_ref _r(r, m);
log_axiom_instantiation(r);
m.trace_stream() << "[end-of-instance]\n";
}

14
src/smt/theory_arith_aux.h
View file

@ -2239,17 +2239,17 @@ namespace smt {
ctx.push_trail(value_trail<unsigned>(m_assume_eq_head));
while (m_assume_eq_head < m_assume_eq_candidates.size()) {
std::pair<theory_var, theory_var> const & p = m_assume_eq_candidates[m_assume_eq_head];
theory_var v1 = p.first;
theory_var v2 = p.second;
auto const& [v1, v2] = m_assume_eq_candidates[m_assume_eq_head];
enode* n1 = get_enode(v1);
enode* n2 = get_enode(v2);
m_assume_eq_head++;
CTRACE("func_interp_bug",
get_value(v1) == get_value(v2) &&
get_enode(v1)->get_root() != get_enode(v2)->get_root(),
tout << "assuming eq: #" << get_enode(v1)->get_owner_id() << " = #" << get_enode(v2)->get_owner_id() << "\n";);
n1->get_root() != n2->get_root(),
tout << "assuming eq: #" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";);
if (get_value(v1) == get_value(v2) &&
get_enode(v1)->get_root() != get_enode(v2)->get_root() &&
assume_eq(get_enode(v1), get_enode(v2))) {
n1->get_root() != n2->get_root() &&
assume_eq(n1, n2)) {
++m_stats.m_assume_eqs;
return true;
}

100
src/smt/theory_arith_pp.h
View file

@ -82,18 +82,17 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::display_row(std::ostream & out, row const & r, bool compact) const {
typename vector<row_entry>::const_iterator it = r.begin_entries();
typename vector<row_entry>::const_iterator end = r.end_entries();
out << "(v" << r.get_base_var() << ") : ";
bool first = true;
for (; it != end; ++it) {
if (!it->is_dead()) {
for (auto const& e : r) {
if (!e.is_dead()) {
if (first)
first = false;
else
out << " + ";
theory_var s = it->m_var;
numeral const & c = it->m_coeff;
theory_var s = e.m_var;
numeral const & c = e.m_coeff;
if (!c.is_one())
out << c << "*";
if (compact) {
@ -103,7 +102,7 @@ namespace smt {
}
}
else
display_var_flat_def(out, s);
out << enode_pp(get_enode(s), ctx);
}
}
out << "\n";
@ -117,20 +116,16 @@ namespace smt {
else
out << "rows (expanded view):\n";
unsigned num = m_rows.size();
for (unsigned r_id = 0; r_id < num; r_id++) {
if (m_rows[r_id].m_base_var != null_theory_var) {
for (unsigned r_id = 0; r_id < num; r_id++)
if (m_rows[r_id].m_base_var != null_theory_var)
display_row(out, r_id, compact);
}
}
}
template<typename Ext>
void theory_arith<Ext>::display_row_shape(std::ostream & out, row const & r) const {
typename vector<row_entry>::const_iterator it = r.begin_entries();
typename vector<row_entry>::const_iterator end = r.end_entries();
for (; it != end; ++it) {
if (!it->is_dead()) {
numeral const & c = it->m_coeff;
for (auto const& e : r) {
if (!e.is_dead()) {
numeral const & c = e.m_coeff;
if (c.is_one())
out << "1";
else if (c.is_minus_one())
@ -150,11 +145,9 @@ namespace smt {
template<typename Ext>
bool theory_arith<Ext>::is_one_minus_one_row(row const & r) const {
typename vector<row_entry>::const_iterator it = r.begin_entries();
typename vector<row_entry>::const_iterator end = r.end_entries();
for (; it != end; ++it) {
if (!it->is_dead()) {
numeral const & c = it->m_coeff;
for (auto const& e : r) {
if (!e.is_dead()) {
numeral const & c = e.m_coeff;
if (!c.is_one() && !c.is_minus_one())
return false;
}
@ -184,11 +177,9 @@ namespace smt {
for (unsigned r_id = 0; r_id < num; r_id++) {
row const & r = m_rows[r_id];
if (r.m_base_var != null_theory_var) {
typename vector<row_entry>::const_iterator it = r.begin_entries();
typename vector<row_entry>::const_iterator end = r.end_entries();
for (; it != end; ++it) {
if (!it->is_dead()) {
numeral const & c = it->m_coeff;
for (auto const& e : r) {
if (!e.is_dead()) {
numeral const & c = e.m_coeff;
if (c.to_rational().is_big()) {
std::string str = c.to_rational().to_string();
if (str.length() > 48)
@ -215,11 +206,9 @@ namespace smt {
row const & r = m_rows[r_id];
if (r.m_base_var != null_theory_var) {
num_rows++;
typename vector<row_entry>::const_iterator it = r.begin_entries();
typename vector<row_entry>::const_iterator end = r.end_entries();
for (; it != end; ++it) {
if (!it->is_dead()) {
numeral const & c = it->m_coeff;
for (auto const& e : r) {
if (!e.is_dead()) {
numeral const & c = e.m_coeff;
num_non_zeros++;
if (c.is_one())
num_ones++;
@ -284,11 +273,9 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::display_row_info(std::ostream & out, row const & r) const {
display_row(out, r, true);
typename vector<row_entry>::const_iterator it = r.begin_entries();
typename vector<row_entry>::const_iterator end = r.end_entries();
for (; it != end; ++it)
if (!it->is_dead())
display_var(out, it->m_var);
for (auto const& e : r)
if (!e.is_dead())
display_var(out, e.m_var);
}
/**
@ -298,15 +285,14 @@ namespace smt {
void theory_arith<Ext>::display_simplified_row(std::ostream & out, row const & r) const {
bool has_rat_coeff = false;
numeral k;
typename vector<row_entry>::const_iterator it = r.begin_entries();
typename vector<row_entry>::const_iterator end = r.end_entries();
out << "(v" << r.get_base_var() << ") : ";
bool first = true;
for (; it != end; ++it) {
if (it->is_dead())
for (auto const& e : r) {
if (e.is_dead())
continue;
theory_var v = it->m_var;
numeral const & c = it->m_coeff;
theory_var v = e.m_var;
numeral const & c = e.m_coeff;
if (is_fixed(v)) {
k += c * lower_bound(v).get_rational();
continue;
@ -328,11 +314,9 @@ namespace smt {
}
out << "\n";
if (has_rat_coeff) {
typename vector<row_entry>::const_iterator it = r.begin_entries();
typename vector<row_entry>::const_iterator end = r.end_entries();
for (; it != end; ++it)
if (!it->is_dead() && (is_base(it->m_var) || (!is_fixed(it->m_var) && (lower(it->m_var) || upper(it->m_var)))))
display_var(out, it->m_var);
for (auto const& e : r)
if (!e.is_dead() && (is_base(e.m_var) || (!is_fixed(e.m_var) && (lower(e.m_var) || upper(e.m_var)))))
display_var(out, e.m_var);
}
}
@ -385,8 +369,7 @@ namespace smt {
out << ", shared: " << get_context().is_shared(get_enode(v));
out << ", unassigned: " << m_unassigned_atoms[v];
out << ", rel: " << get_context().is_relevant(get_enode(v));
out << ", def: ";
display_var_flat_def(out, v);
out << ", def: " << enode_pp(get_enode(v), ctx);
out << "\n";
}
@ -477,28 +460,17 @@ namespace smt {
theory_var v = a->get_var();
inf_numeral const & k = a->get_k();
enode * e = get_enode(v);
if (show_sign) {
if (!a->is_true())
out << "not ";
else
out << " ";
}
if (show_sign)
out << (a->is_true()?" ":"not ");
out << "v";
out.width(3);
out << std::left << v << " #";
out.width(3);
out << e->get_owner_id();
out << std::right;
out << " ";
if (a->get_atom_kind() == A_LOWER)
out << ">=";
else
out << "<=";
out << " ";
out << " " << ((a->get_atom_kind() == A_LOWER)? ">=" : "<=") << " ";
out.width(6);
out << k << " ";
display_var_flat_def(out, v);
out << "\n";
out << k << " " << enode_pp(get_enode(v), ctx) << "\n";
}
template<typename Ext>

34
src/smt/theory_array_full.cpp
View file

@ -707,6 +707,38 @@ namespace smt {
}
else if (!has_large_domain(store_app)) {
//
// let A = store(B, i, v)
//
// Add:
// default(A) = A[epsilon]
// default(B) = B[epsilon]
//
//
expr_ref_vector args1(m), args2(m);
args1.push_back(store_app->get_arg(0));
args2.push_back(store_app);
for (unsigned i = 1; i + 1 < num_args; ++i) {
expr* arg = store_app->get_arg(i);
sort* srt = arg->get_sort();
auto ep = mk_epsilon(srt);
args1.push_back(ep.first);
args2.push_back(ep.first);
}
app_ref sel1(m), sel2(m);
sel1 = mk_select(args1);
sel2 = mk_select(args2);
ctx.internalize(def1, false);
ctx.internalize(def2, false);
is_new = try_assign_eq(def1, sel1) || try_assign_eq(def2, sel2);
return is_new;
#if 0
//
// This is incorrect, issue #5593.
//
// let A = store(B, i, v)
//
// Add:
@ -731,7 +763,9 @@ namespace smt {
app_ref sel1(m), sel2(m);
sel1 = mk_select(args1);
sel2 = mk_select(args2);
std::cout << "small domain " << sel1 << " " << sel2 << "\n";
is_new = try_assign_eq(sel1, sel2);
#endif
}
ctx.internalize(def1, false);

2
src/smt/theory_datatype.cpp
View file

@ -297,7 +297,7 @@ namespace smt {
TRACE("datatype", tout << "internalizing term:\n" << mk_pp(term, m) << "\n";);
unsigned num_args = term->get_num_args();
for (unsigned i = 0; i < num_args; i++)
ctx.internalize(term->get_arg(i), false);
ctx.internalize(term->get_arg(i), has_quantifiers(term));
// the internalization of the arguments may trigger the internalization of term.
if (ctx.e_internalized(term))
return true;

16
src/smt/theory_fpa.cpp
View file

@ -38,7 +38,7 @@ namespace smt {
{
params_ref p;
p.set_bool("arith_lhs", true);
m_th_rw.updt_params(p);
m_th_rw.updt_params(p);
}
theory_fpa::~theory_fpa()
@ -215,11 +215,12 @@ namespace smt {
}
void theory_fpa::assert_cnstr(expr * e) {
expr_ref _e(e, m);
if (m.is_true(e)) return;
TRACE("t_fpa_detail", tout << "asserting " << mk_ismt2_pp(e, m) << "\n";);
if (m.has_trace_stream()) log_axiom_instantiation(e);
ctx.internalize(e, false);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
literal lit(ctx.get_literal(e));
ctx.mark_as_relevant(lit);
ctx.mk_th_axiom(get_id(), 1, &lit);
@ -284,6 +285,9 @@ namespace smt {
}
default: /* ignore */;
}
if (!ctx.relevancy())
relevant_eh(term);
}
return true;
@ -454,13 +458,9 @@ namespace smt {
expr * args[] = { bv_val_a->get_arg(0), bv_val_a->get_arg(1), bv_val_a->get_arg(2) };
cc_args = m_bv_util.mk_concat(3, args);
c = m.mk_eq(wrapped, cc_args);
// NB code review: #5454 exposes a bug in fpa_solver that
// could be latent here as well. It needs also the equality
// n == bv_val_e to be asserted such that whenever something is assigned th
// bit-vector value cc_args it is equated with n
// I don't see another way this constraint would be enforced.
assert_cnstr(c);
assert_cnstr(mk_side_conditions());
assert_cnstr(m.mk_eq(n, bv_val_e));
}
else {
expr_ref wu(m);
@ -627,7 +627,7 @@ namespace smt {
bv2fp.convert_min_max_specials(&mdl, &new_model, seen);
bv2fp.convert_uf2bvuf(&mdl, &new_model, seen);
for (func_decl* f : seen)
for (func_decl* f : seen)
mdl.unregister_decl(f);
for (unsigned i = 0; i < new_model.get_num_constants(); i++) {

119
src/smt/theory_lra.cpp
View file

@ -173,8 +173,8 @@ class theory_lra::imp {
unsigned_vector m_bounds_trail;
unsigned m_asserted_qhead;
svector<unsigned> m_to_check; // rows that should be checked for theory propagation
svector<unsigned> m_bv_to_propagate; // Boolean variables that can be propagated
svector<std::pair<theory_var, theory_var> > m_assume_eq_candidates;
unsigned m_assume_eq_head;
lp::u_set m_tmp_var_set;
@ -233,6 +233,7 @@ class theory_lra::imp {
resource_limit m_resource_limit;
lp_bounds m_new_bounds;
symbol m_farkas;
vector<parameter> m_bound_params;
lp::lp_bound_propagator<imp> m_bp;
context& ctx() const { return th.get_context(); }
@ -870,6 +871,10 @@ public:
m_bound_terms(m),
m_bound_predicate(m)
{
m_bound_params.push_back(parameter(m_farkas));
m_bound_params.push_back(parameter(rational(1)));
m_bound_params.push_back(parameter(rational(1)));
}
~imp() {
@ -1071,7 +1076,7 @@ public:
lp().pop(num_scopes);
// VERIFY(l_false != make_feasible());
m_new_bounds.reset();
m_to_check.reset();
m_bv_to_propagate.reset();
if (m_nla)
m_nla->pop(num_scopes);
TRACE("arith", tout << "num scopes: " << num_scopes << " new scope level: " << m_scopes.size() << "\n";);
@ -1493,29 +1498,24 @@ public:
ctx().push_trail(value_trail<unsigned>(m_assume_eq_head));
while (m_assume_eq_head < m_assume_eq_candidates.size()) {
std::pair<theory_var, theory_var> const & p = m_assume_eq_candidates[m_assume_eq_head];
theory_var v1 = p.first;
theory_var v2 = p.second;
auto const [v1, v2] = m_assume_eq_candidates[m_assume_eq_head];
enode* n1 = get_enode(v1);
enode* n2 = get_enode(v2);
m_assume_eq_head++;
CTRACE("arith",
is_eq(v1, v2) && n1->get_root() != n2->get_root(),
tout << "assuming eq: v" << v1 << " = v" << v2 << "\n";);
if (is_eq(v1, v2) && n1->get_root() != n2->get_root() && th.assume_eq(n1, n2)) {
if (is_eq(v1, v2) && n1->get_root() != n2->get_root() && th.assume_eq(n1, n2))
return true;
}
}
return false;
}
bool is_eq(theory_var v1, theory_var v2) {
if (use_nra_model()) {
if (use_nra_model())
return m_nla->am().eq(nl_value(v1, *m_a1), nl_value(v2, *m_a2));
}
else {
else
return get_ivalue(v1) == get_ivalue(v2);
}
}
bool has_delayed_constraints() const {
@ -1523,6 +1523,8 @@ public:
}
final_check_status final_check_eh() {
if (propagate_core())
return FC_CONTINUE;
m_model_is_initialized = false;
IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n");
lbool is_sat = l_true;
@ -1534,9 +1536,7 @@ public:
switch (is_sat) {
case l_true:
TRACE("arith", display(tout);
/* ctx().display(tout);*/
);
TRACE("arith", display(tout));
switch (check_lia()) {
case l_true:
@ -2048,41 +2048,59 @@ public:
return false;
}
bool m_new_def{ false };
bool m_new_def = false ;
bool adaptive() const { return ctx().get_fparams().m_arith_adaptive; }
double adaptive_assertion_threshold() const { return ctx().get_fparams().m_arith_adaptive_assertion_threshold; }
bool process_atoms() const {
if (!adaptive())
return true;
unsigned total_conflicts = ctx().get_num_conflicts();
if (total_conflicts < 10)
return true;
double f = static_cast<double>(m_num_conflicts)/static_cast<double>(total_conflicts);
return f >= adaptive_assertion_threshold();
}
bool can_propagate() {
return process_atoms() && can_propagate_core();
}
bool can_propagate_core() {
return m_asserted_atoms.size() > m_asserted_qhead || m_new_def;
}
void propagate() {
bool propagate() {
return process_atoms() && propagate_core();
}
bool propagate_core() {
m_model_is_initialized = false;
flush_bound_axioms();
if (!can_propagate()) {
return;
}
m_new_def = false;
if (!can_propagate_core())
return false;
m_new_def = false;
while (m_asserted_qhead < m_asserted_atoms.size() && !ctx().inconsistent() && m.inc()) {
bool_var bv = m_asserted_atoms[m_asserted_qhead].m_bv;
bool is_true = m_asserted_atoms[m_asserted_qhead].m_is_true;
m_to_check.push_back(bv);
auto [bv, is_true] = m_asserted_atoms[m_asserted_qhead];
m_bv_to_propagate.push_back(bv);
api_bound* b = nullptr;
TRACE("arith", tout << "propagate: " << literal(bv, !is_true) << "\n";);
if (m_bool_var2bound.find(bv, b)) {
TRACE("arith", tout << "propagate: " << literal(bv, !is_true) << "\n";
if (!m_bool_var2bound.contains(bv)) tout << "not found\n");
if (m_bool_var2bound.find(bv, b))
assert_bound(bv, is_true, *b);
}
else {
TRACE("arith", tout << "not found " << bv << "\n";);
}
++m_asserted_qhead;
}
if (ctx().inconsistent()) {
m_to_check.reset();
return;
m_bv_to_propagate.reset();
return true;
}
lbool lbl = make_feasible();
if (!m.inc())
return;
return false;
switch(lbl) {
case l_false:
@ -2096,7 +2114,7 @@ public:
case l_undef:
break;
}
return true;
}
bool should_propagate() const {
@ -2246,26 +2264,28 @@ public:
assign(bound, m_core, m_eqs, m_params);
}
void add_eq(lpvar u, lpvar v, lp::explanation const& e) {
bool add_eq(lpvar u, lpvar v, lp::explanation const& e, bool is_fixed) {
if (ctx().inconsistent())
return;
return false;
theory_var uv = lp().local_to_external(u); // variables that are returned should have external representations
theory_var vv = lp().local_to_external(v); // so maybe better to have them already transformed to external form
enode* n1 = get_enode(uv);
enode* n2 = get_enode(vv);
TRACE("arith", tout << "add-eq " << mk_pp(n1->get_expr(), m) << " == " << mk_pp(n2->get_expr(), m) << " " << n1->get_expr_id() << " == " << n2->get_expr_id() << "\n";);
if (n1->get_root() == n2->get_root())
return;
return false;
expr* e1 = n1->get_expr();
expr* e2 = n2->get_expr();
if (e1->get_sort() != e2->get_sort())
return;
if (m.is_ite(e1) || m.is_ite(e2))
return;
return false;
if (!is_fixed && !a.is_numeral(e1) && !a.is_numeral(e2) && (m.is_ite(e1) || m.is_ite(e2)))
return false;
reset_evidence();
for (auto ev : e)
set_evidence(ev.ci(), m_core, m_eqs);
assign_eq(uv, vv);
return true;
}
literal_vector m_core2;
@ -2440,6 +2460,7 @@ public:
typedef lp_bounds::iterator iterator;
void flush_bound_axioms() {
CTRACE("arith", !m_new_bounds.empty(), tout << "flush bound axioms\n";);
while (!m_new_bounds.empty()) {
@ -2458,7 +2479,7 @@ public:
CTRACE("arith", atoms.size() > 1,
for (auto* a : atoms) a->display(tout) << "\n";);
lp_bounds occs(m_bounds[v]);
std::sort(atoms.begin(), atoms.end(), compare_bounds());
std::sort(occs.begin(), occs.end(), compare_bounds());
@ -2558,14 +2579,15 @@ public:
}
void propagate_basic_bounds() {
for (auto const& bv : m_to_check) {
for (auto const& bv : m_bv_to_propagate) {
api_bound* b = nullptr;
if (m_bool_var2bound.find(bv, b)) {
propagate_bound(bv, ctx().get_assignment(bv) == l_true, *b);
if (ctx().inconsistent()) break;
if (ctx().inconsistent())
break;
}
}
m_to_check.reset();
m_bv_to_propagate.reset();
}
// for glb lo': lo' < lo:
@ -2633,10 +2655,7 @@ public:
ctx().display_literals_verbose(tout, m_core);
ctx().display_literal_verbose(tout << " => ", lit2);
tout << "\n";);
m_params.push_back(parameter(m_farkas));
m_params.push_back(parameter(rational(1)));
m_params.push_back(parameter(rational(1)));
assign(lit2, m_core, m_eqs, m_params);
assign(lit2, m_core, m_eqs, m_bound_params);
++m_stats.m_bounds_propagations;
}
@ -3194,7 +3213,7 @@ public:
m_assume_eq_head = 0;
m_scopes.reset();
m_stats.reset();
m_to_check.reset();
m_bv_to_propagate.reset();
m_model_is_initialized = false;
}
@ -3661,7 +3680,7 @@ public:
else if (can_get_value(v)) out << " = " << get_value(v);
if (is_int(v)) out << ", int";
if (ctx().is_shared(get_enode(v))) out << ", shared";
out << " := "; th.display_var_flat_def(out, v) << "\n";
out << " := " << enode_pp(get_enode(v), ctx()) << "\n";
}
}

1
src/smt/theory_opt.h
View file

@ -29,6 +29,7 @@ namespace smt {
class theory_opt {
public:
typedef inf_eps_rational<inf_rational> inf_eps;
virtual ~theory_opt() = default;
virtual inf_eps value(theory_var) = 0;
virtual inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared) = 0;
virtual theory_var add_objective(app* term) = 0;

37
src/smt/theory_recfun.cpp
View file

@ -246,17 +246,23 @@ namespace smt {
literal theory_recfun::mk_eq_lit(expr* l, expr* r) {
literal lit;
if (m.is_true(r) || m.is_false(r)) {
std::swap(l, r);
}
if (m.is_true(l)) {
lit = mk_literal(r);
}
else if (m.is_false(l)) {
lit = ~mk_literal(r);
if (has_quantifiers(l) || has_quantifiers(r)) {
expr_ref eq1(m.mk_eq(l, r), m);
expr_ref fn(m.mk_fresh_const("rec-eq", m.mk_bool_sort()), m);
expr_ref eq(m.mk_eq(fn, eq1), m);
ctx.assert_expr(eq);
ctx.internalize_assertions();
lit = mk_literal(fn);
}
else {
lit = mk_eq(l, r, false);
if (m.is_true(r) || m.is_false(r))
std::swap(l, r);
if (m.is_true(l))
lit = mk_literal(r);
else if (m.is_false(l))
lit = ~mk_literal(r);
else
lit = mk_eq(l, r, false);
}
ctx.mark_as_relevant(lit);
return lit;
@ -282,14 +288,12 @@ namespace smt {
auto & vars = e.m_def->get_vars();
expr_ref lhs(e.m_lhs, m);
unsigned depth = get_depth(e.m_lhs);
expr_ref rhs(apply_args(depth, vars, e.m_args, e.m_def->get_rhs()), m);
expr_ref rhs(apply_args(depth, vars, e.m_args, e.m_def->get_rhs()), m);
literal lit = mk_eq_lit(lhs, rhs);
std::function<literal(void)> fn = [&]() { return lit; };
scoped_trace_stream _tr(*this, fn);
ctx.mk_th_axiom(get_id(), 1, &lit);
TRACEFN("macro expansion yields " << pp_lit(ctx, lit));
if (has_quantifiers(rhs))
throw default_exception("quantified formulas in recursive functions are not supported");
}
/**
@ -377,6 +381,13 @@ namespace smt {
unsigned depth = get_depth(e.m_pred);
expr_ref lhs(u().mk_fun_defined(d, args), m);
expr_ref rhs = apply_args(depth, vars, args, e.m_cdef->get_rhs());
if (has_quantifiers(rhs)) {
expr_ref fn(m.mk_fresh_const("rec-eq", m.mk_bool_sort()), m);
expr_ref eq(m.mk_eq(fn, rhs), m);
ctx.assert_expr(eq);
ctx.internalize_assertions();
rhs = fn;
}
literal_vector clause;
for (auto & g : e.m_cdef->get_guards()) {
expr_ref guard = apply_args(depth, vars, args, g);
@ -394,8 +405,6 @@ namespace smt {
std::function<literal_vector(void)> fn = [&]() { return clause; };
scoped_trace_stream _tr(*this, fn);
ctx.mk_th_axiom(get_id(), clause);
if (has_quantifiers(rhs))
throw default_exception("quantified formulas in recursive functions are not supported");
}
final_check_status theory_recfun::final_check_eh() {

102
src/smt/theory_seq.cpp
View file

@ -562,55 +562,66 @@ void theory_seq::mk_decompose(expr* e, expr_ref& head, expr_ref& tail) {
/*
\brief Check extensionality (for sequences).
*/
bool theory_seq::check_extensionality(expr* e1, enode* n1, enode* n2) {
dependency* dep = nullptr;
expr* o1 = n1->get_expr();
expr* o2 = n2->get_expr();
if (o1->get_sort() != o2->get_sort())
return true;
if (ctx.is_diseq(n1, n2) || m_exclude.contains(o1, o2))
return true;
expr_ref e2(m);
if (!canonize(n2->get_expr(), dep, e2))
return false;
m_new_eqs.reset();
bool change = false;
if (!m_seq_rewrite.reduce_eq(e1, e2, m_new_eqs, change)) {
TRACE("seq", tout << "exclude " << mk_pp(o1, m) << " " << mk_pp(o2, m) << "\n";);
m_exclude.update(o1, o2);
return true;
}
for (auto const& p : m_new_eqs) {
if (m_exclude.contains(p.first, p.second)) {
TRACE("seq", tout << "excluded " << mk_pp(p.first, m) << " " << mk_pp(p.second, m) << "\n";);
return true;
}
}
ctx.assume_eq(n1, n2);
return false;
}
bool theory_seq::check_extensionality() {
unsigned sz = get_num_vars();
unsigned_vector seqs;
dependency* dep = nullptr;
expr_ref e1(m);
for (unsigned v = 0; v < sz; ++v) {
enode* n1 = get_enode(v);
expr* o1 = n1->get_expr();
if (n1 != n1->get_root()) {
continue;
}
if (!seqs.empty() && ctx.is_relevant(n1) && m_util.is_seq(o1) && ctx.is_shared(n1)) {
dependency* dep = nullptr;
expr_ref e1(m);
if (!canonize(o1, dep, e1)) {
// check extensionality for sequence arguments of nth_u
// two occurrences of nth_u(a,x), nth_u(b,y) must induce comparing sequences a, b
// whenever x = y
if (m_util.str.is_nth_u(o1) && n1->is_cgr()) {
auto* r0 = n1->get_arg(0)->get_root();
auto* r1 = n1->get_arg(1)->get_root();
if (!canonize(r0->get_expr(), dep, e1))
return false;
}
for (theory_var v : seqs) {
enode* n2 = get_enode(v);
expr* o2 = n2->get_expr();
if (o1->get_sort() != o2->get_sort()) {
continue;
}
if (ctx.is_diseq(n1, n2) || m_exclude.contains(o1, o2)) {
continue;
}
expr_ref e2(m);
if (!canonize(n2->get_expr(), dep, e2)) {
for (auto* p : r1->get_parents())
if (p != n1 && p->is_cgr() && m_util.str.is_nth_u(p->get_expr()) &&
!check_extensionality(e1, r0, p->get_arg(0)->get_root()))
return false;
}
m_new_eqs.reset();
bool change = false;
if (!m_seq_rewrite.reduce_eq(e1, e2, m_new_eqs, change)) {
TRACE("seq", tout << "exclude " << mk_pp(o1, m) << " " << mk_pp(o2, m) << "\n";);
m_exclude.update(o1, o2);
continue;
}
bool excluded = false;
for (auto const& p : m_new_eqs) {
if (m_exclude.contains(p.first, p.second)) {
TRACE("seq", tout << "excluded " << mk_pp(p.first, m) << " " << mk_pp(p.second, m) << "\n";);
excluded = true;
break;
}
}
if (excluded) {
continue;
}
ctx.assume_eq(n1, n2);
}
if (!n1->is_root())
continue;
if (!m_util.is_seq(o1))
continue;
if (!seqs.empty() && ctx.is_relevant(n1) && ctx.is_shared(n1)) {
if (!canonize(o1, dep, e1))
return false;
}
for (theory_var v : seqs)
if (!check_extensionality(e1, n1, get_enode(v)))
return false;
}
seqs.push_back(v);
}
@ -726,7 +737,7 @@ void theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vect
svector<assumption> assumptions;
const_cast<dependency_manager&>(m_dm).linearize(dep, assumptions);
for (assumption const& a : assumptions) {
if (a.lit != null_literal) {
if (a.lit != null_literal && a.lit != true_literal) {
lits.push_back(a.lit);
SASSERT(ctx.get_assignment(a.lit) == l_true);
}
@ -743,7 +754,7 @@ bool theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits
return false;
if (ctx.get_assignment(lit) == l_true)
return false;
literal_vector lits(n, _lits);
if (lit == false_literal) {
@ -2368,7 +2379,7 @@ void theory_seq::validate_fmls(enode_pair_vector const& eqs, literal_vector cons
theory_var theory_seq::mk_var(enode* n) {
expr* o = n->get_expr();
if (!m_util.is_seq(o) && !m_util.is_re(o))
if (!m_util.is_seq(o) && !m_util.is_re(o) && !m_util.str.is_nth_u(o))
return null_theory_var;
if (is_attached_to_var(n))
@ -2898,6 +2909,7 @@ bool theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
if (n1->get_root() == n2->get_root()) {
return false;
}
ctx.mark_as_relevant(n1);
ctx.mark_as_relevant(n2);
@ -2979,8 +2991,8 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
m_rewrite(se1);
m_rewrite(se2);
if (is_true) {
expr_ref f1 = m_sk.mk_indexof_left(se1, se2);
expr_ref f2 = m_sk.mk_indexof_right(se1, se2);
expr_ref f1 = m_sk.mk_contains_left(se1, se2);
expr_ref f2 = m_sk.mk_contains_right(se1, se2);
f = mk_concat(f1, se2, f2);
propagate_eq(lit, f, e1, true);
propagate_eq(lit, mk_len(f), mk_len(e1), false);

1
src/smt/theory_seq.h
View file

@ -458,6 +458,7 @@ namespace smt {
void add_unhandled_expr(expr* e);
bool check_extensionality();
bool check_extensionality(expr* e1, enode* n1, enode* n2);
bool check_contains();
bool check_lts();
dependency* m_eq_deps { nullptr };

8
src/smt/theory_special_relations.cpp
View file

@ -1146,5 +1146,11 @@ namespace smt {
expr* e = ctx.bool_var2expr(a.var());
out << (a.phase() ? "" : "(not ") << mk_pp(e, get_manager()) << (a.phase() ? "" : ")") << "\n";
}
void theory_special_relations::get_specrels(func_decl_set& rels) const {
for (auto [f, r] : m_relations)
rels.insert(m_util.get_relation(r->m_decl));
}
}

2
src/smt/theory_special_relations.h
View file

@ -199,6 +199,8 @@ namespace smt {
bool can_propagate() override { return m_can_propagate; }
void propagate() override;
void display(std::ostream & out) const override;
void get_specrels(func_decl_set& rels) const;
};
}

8
src/smt/user_propagator.h
View file

@ -48,7 +48,7 @@ namespace smt {
void reset() { memset(this, 0, sizeof(*this)); }
};
void* m_user_context;
void* m_user_context = nullptr;
solver::push_eh_t m_push_eh;
solver::pop_eh_t m_pop_eh;
solver::fresh_eh_t m_fresh_eh;
@ -56,13 +56,13 @@ namespace smt {
solver::fixed_eh_t m_fixed_eh;
solver::eq_eh_t m_eq_eh;
solver::eq_eh_t m_diseq_eh;
solver::context_obj* m_api_context { nullptr };
unsigned m_qhead { 0 };
solver::context_obj* m_api_context = nullptr;
unsigned m_qhead = 0;
uint_set m_fixed;
vector<prop_info> m_prop;
unsigned_vector m_prop_lim;
vector<literal_vector> m_id2justification;
unsigned m_num_scopes { 0 };
unsigned m_num_scopes = 0;
literal_vector m_lits;
enode_pair_vector m_eqs;
stats m_stats;