From ad778f87c74580c73c22b769bdd4b142ff18226d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Jan 2016 16:03:37 -0800 Subject: [PATCH 1/7] change data-structures to concanetation decomposition normal form Signed-off-by: Nikolaj Bjorner --- src/ast/ast_smt2_pp.cpp | 12 +- src/ast/rewriter/seq_rewriter.cpp | 118 +++++++--- src/ast/rewriter/seq_rewriter.h | 7 +- src/ast/seq_decl_plugin.h | 1 + src/smt/theory_seq.cpp | 343 ++++++++++-------------------- src/smt/theory_seq.h | 155 ++------------ 6 files changed, 235 insertions(+), 401 deletions(-) diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 333c9c229..e31e5aab6 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -1201,14 +1201,18 @@ std::ostream& operator<<(std::ostream& out, app_ref const& e) { } std::ostream& operator<<(std::ostream& out, expr_ref_vector const& e) { - for (unsigned i = 0; i < e.size(); ++i) - out << mk_ismt2_pp(e[i], e.get_manager()) << "\n"; + for (unsigned i = 0; i < e.size(); ++i) { + out << mk_ismt2_pp(e[i], e.get_manager()); + if (i + 1 < e.size()) out << "; "; + } return out; } std::ostream& operator<<(std::ostream& out, app_ref_vector const& e) { - for (unsigned i = 0; i < e.size(); ++i) - out << mk_ismt2_pp(e[i], e.get_manager()) << "\n"; + for (unsigned i = 0; i < e.size(); ++i) { + out << mk_ismt2_pp(e[i], e.get_manager()); + if (i + 1 < e.size()) out << "; "; + } return out; } diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 3ee8675d8..d85060f1d 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -830,11 +830,12 @@ br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) { br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) { expr_ref_vector lhs(m()), rhs(m()), res(m()); - if (!reduce_eq(l, r, lhs, rhs)) { + bool changed = false; + if (!reduce_eq(l, r, lhs, rhs, changed)) { result = m().mk_false(); return BR_DONE; } - if (lhs.size() == 1 && lhs[0].get() == l && rhs[0].get() == r) { + if (!changed) { return BR_FAILED; } for (unsigned i = 0; i < lhs.size(); ++i) { @@ -844,20 +845,19 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) { return BR_REWRITE3; } -bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs) { +bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change) { expr* a, *b; zstring s; - bool change = false; + bool lchange = false; + SASSERT(lhs.empty()); // solve from back while (true) { while (!rs.empty() && m_util.str.is_empty(rs.back())) { rs.pop_back(); - change = true; } while (!ls.empty() && m_util.str.is_empty(ls.back())) { ls.pop_back(); - change = true; } if (ls.empty() || rs.empty()) { break; @@ -901,7 +901,9 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_ else { break; } + TRACE("seq", tout << "change back\n";); change = true; + lchange = true; } // solve from front @@ -956,7 +958,10 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_ else { break; } + TRACE("seq", tout << "change front\n";); + change = true; + lchange = true; } // reduce strings zstring s1, s2; @@ -982,7 +987,9 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_ else { rs[head2] = m_util.str.mk_string(s2.extract(l, s2.length()-l)); } + TRACE("seq", tout << "change string\n";); change = true; + lchange = true; } while (head1 < ls.size() && head2 < rs.size() && @@ -1002,52 +1009,109 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_ if (l < s2.length()) { rs.push_back(m_util.str.mk_string(s2.extract(0, s2.length()-l))); } + TRACE("seq", tout << "change string back\n";); change = true; + lchange = true; } bool is_sat; unsigned szl = ls.size() - head1, szr = rs.size() - head2; expr* const* _ls = ls.c_ptr() + head1, * const* _rs = rs.c_ptr() + head2; + + if (length_constrained(szl, _ls, szr, _rs, lhs, rhs, is_sat)) { ls.reset(); rs.reset(); - return is_sat; - } - if (is_subsequence(szl, _ls, szr, _rs, lhs, rhs, is_sat)) { - ls.reset(); rs.reset(); + change = true; return is_sat; } - if (szl == 0 && szr == 0) { - ls.reset(); rs.reset(); - return true; - } - else if (!change) { - // skip - SASSERT(lhs.empty()); - } - else { - // could solve if either side is fixed size. - SASSERT(szl > 0 && szr > 0); - lhs.push_back(m_util.str.mk_concat(szl, ls.c_ptr() + head1)); - rhs.push_back(m_util.str.mk_concat(szr, rs.c_ptr() + head2)); + if (szr == 0 && szl == 0) { ls.reset(); rs.reset(); + return true; } - SASSERT(lhs.empty() || ls.empty()); + if (szr == 0 && szl > 0) { + std::swap(szr, szl); + std::swap(_ls, _rs); + } + if (szl == 0 && szr > 0) { + if (set_empty(szr, _rs, true, lhs, rhs)) { + lchange |= szr > 1; + change |= szr > 1; + TRACE("seq", tout << lchange << " " << szr << "\n";); + if (szr == 1 && !lchange) { + lhs.reset(); + rhs.reset(); + } + else { + ls.reset(); + rs.reset(); + } + return true; + } + else { + return false; + } + } + SASSERT(szl > 0 && szr > 0); + + if (is_subsequence(szl, _ls, szr, _rs, lhs, rhs, is_sat)) { + ls.reset(); rs.reset(); + change = true; + return is_sat; + } + + if (lchange) { + if (head1 > 0) { + for (unsigned i = 0; i < szl; ++i) { + ls[i] = ls[i + head1]; + } + } + ls.shrink(szl); + if (head2 > 0) { + for (unsigned i = 0; i < szr; ++i) { + rs[i] = rs[i + head2]; + } + } + rs.shrink(szr); + } + SASSERT(rs.empty() == ls.empty()); + change |= lchange; return true; } -bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs) { +void seq_rewriter::add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_vector& lhs, expr_ref_vector& rhs) { + if (ls.empty() && !rs.empty()) { + rhs.push_back(m_util.str.mk_concat(rs)); + lhs.push_back(m_util.str.mk_empty(m().get_sort(rhs.back()))); + } + else if (rs.empty() && !ls.empty()) { + lhs.push_back(m_util.str.mk_concat(ls)); + rhs.push_back(m_util.str.mk_empty(m().get_sort(lhs.back()))); + } + else if (!rs.empty() && !ls.empty()) { + lhs.push_back(m_util.str.mk_concat(ls)); + rhs.push_back(m_util.str.mk_concat(rs)); + } +} + + +bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& changed) { m_lhs.reset(); m_rhs.reset(); m_util.str.get_concat(l, m_lhs); m_util.str.get_concat(r, m_rhs); - if (reduce_eq(m_lhs, m_rhs, lhs, rhs)) { + bool change = false; + if (reduce_eq(m_lhs, m_rhs, lhs, rhs, change)) { SASSERT(lhs.size() == rhs.size()); - if (lhs.empty()) { + if (!change) { lhs.push_back(l); rhs.push_back(r); } + else { + add_seqs(m_lhs, m_rhs, lhs, rhs); + } + changed |= change; return true; } else { diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 9d4dbb14f..b9d3460aa 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -90,9 +90,12 @@ public: br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result); - bool reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs); + bool reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change); + + bool reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change); + + void add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_vector& lhs, expr_ref_vector& rhs); - bool reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs); }; diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 8cd67a406..00ada9e86 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -223,6 +223,7 @@ public: app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); } app* mk_concat(expr* a, expr* b, expr* c) { return mk_concat(a, mk_concat(b, c)); } expr* mk_concat(unsigned n, expr* const* es) { if (n == 1) return es[0]; SASSERT(n > 1); return m.mk_app(m_fid, OP_SEQ_CONCAT, n, es); } + expr* mk_concat(expr_ref_vector const& es) { return mk_concat(es.size(), es.c_ptr()); } app* mk_length(expr* a) { return m.mk_app(m_fid, OP_SEQ_LENGTH, 1, &a); } app* mk_substr(expr* a, expr* b, expr* c) { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_SEQ_EXTRACT, 3, es); } app* mk_contains(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONTAINS, 2, es); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index f5353e8d0..a51e32d90 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -650,17 +650,22 @@ void theory_seq::enforce_length_coherence(enode* n1, enode* n2) { bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependency* deps) { context& ctx = get_context(); expr_ref_vector lhs(m), rhs(m); - if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs)) { + bool changed = false; + if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs, changed)) { // equality is inconsistent.x2 TRACE("seq", tout << ls << " != " << rs << "\n";); set_conflict(deps); return true; } - if (lhs.empty()) { + if (!changed) { + SASSERT(lhs.empty() && rhs.empty()); return false; } - SASSERT(lhs.size() == rhs.size()); - SASSERT(ls.empty() && rs.empty()); + SASSERT(lhs.size() == rhs.size()); + m_seq_rewrite.add_seqs(ls, rs, lhs, rhs); + if (lhs.empty()) { + return true; + } for (unsigned i = 0; !ctx.inconsistent() && i < lhs.size(); ++i) { expr_ref li(lhs[i].get(), m); expr_ref ri(rhs[i].get(), m); @@ -686,10 +691,10 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc } bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* deps) { - if (l.size() == 1 && is_var(l[0]) && !occurs(l[0], r) && add_solution(l[0], mk_concat(r), deps)) { + if (l.size() == 1 && is_var(l[0]) && !occurs(l[0], r) && add_solution(l[0], mk_concat(r, m.get_sort(l[0])), deps)) { return true; } - if (r.size() == 1 && is_var(r[0]) && !occurs(r[0], l) && add_solution(r[0], mk_concat(l), deps)) { + if (r.size() == 1 && is_var(r[0]) && !occurs(r[0], l) && add_solution(r[0], mk_concat(l, m.get_sort(r[0])), deps)) { return true; } @@ -697,11 +702,9 @@ bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& } bool theory_seq::solve_unit_eq(expr* l, expr* r, dependency* deps) { - SASSERT(l != r); if (l == r) { return true; - } - + } if (is_var(l) && !occurs(l, r) && add_solution(l, r, deps)) { return true; } @@ -773,7 +776,8 @@ bool theory_seq::solve_eqs(unsigned i) { context& ctx = get_context(); bool change = false; for (; !ctx.inconsistent() && i < m_eqs.size(); ++i) { - eq e = m_eqs[i]; + eq const& e = m_eqs[i]; + TRACE("seq", tout << i << "\n";); if (solve_eq(e.ls(), e.rs(), e.dep())) { if (i + 1 != m_eqs.size()) { eq e1 = m_eqs[m_eqs.size()-1]; @@ -785,6 +789,7 @@ bool theory_seq::solve_eqs(unsigned i) { change = true; } } + TRACE("seq", tout << "solve_eqs\n";); return change || ctx.inconsistent(); } @@ -796,20 +801,22 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de dependency* dep2 = 0; bool change = canonize(l, ls, dep2); change = canonize(r, rs, dep2) || change; - TRACE("seq", tout << ls << " = " << rs << "\n";); deps = m_dm.mk_join(dep2, deps); + TRACE("seq", tout << l << " = " << r << " ==> "; + tout << ls << " = " << rs << "\n";); if (!ctx.inconsistent() && simplify_eq(ls, rs, deps)) { return true; } TRACE("seq", tout << ls << " = " << rs << "\n";); - SASSERT(rs.empty() == ls.empty()); - if (ls.empty()) { + if (ls.empty() && rs.empty()) { return true; } if (!ctx.inconsistent() && solve_unit_eq(ls, rs, deps)) { + TRACE("seq", tout << "unit\n";); return true; } if (!ctx.inconsistent() && solve_binary_eq(ls, rs, deps)) { + TRACE("seq", tout << "binary\n";); return true; } if (!ctx.inconsistent() && change) { @@ -871,6 +878,7 @@ bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector cons return false; } if (xs.size() != ys.size()) { + TRACE("seq", tout << "binary conflict\n";); set_conflict(dep); return false; } @@ -928,149 +936,24 @@ bool theory_seq::solve_nqs(unsigned i) { bool change = false; context & ctx = get_context(); for (; !ctx.inconsistent() && i < m_nqs.size(); ++i) { - if (!m_nqs[i].is_solved()) { - solve_ne(i); + if (solve_ne(i)) { + if (i + 1 != m_nqs.size()) { + ne n = m_nqs[m_nqs.size()-1]; + m_nqs.set(i, n); + --i; + } + m_nqs.pop_back(); } } return m_new_propagation || ctx.inconsistent(); } -void theory_seq::solve_ne(unsigned idx) { + +bool theory_seq::solve_ne(unsigned idx) { context& ctx = get_context(); ne const& n = m_nqs[idx]; TRACE("seq", display_disequation(tout, n);); - SASSERT(!n.is_solved()); - unsigned num_undef_lits = 0; - for (unsigned i = 0; i < n.m_lits.size(); ++i) { - switch (ctx.get_assignment(n.m_lits[i])) { - case l_false: - // mark as solved in - mark_solved(idx); - return; - case l_true: - break; - case l_undef: - ++num_undef_lits; - break; - } - } - for (unsigned i = 0; i < n.m_lhs.size(); ++i) { - expr_ref_vector& ls = m_ls; - expr_ref_vector& rs = m_rs; - expr_ref_vector& lhs = m_lhs; - expr_ref_vector& rhs = m_rhs; - ls.reset(); rs.reset(); lhs.reset(); rhs.reset(); - dependency* deps = 0; - expr* l = n.m_lhs[i]; - expr* r = n.m_rhs[i]; - canonize(l, ls, deps); - canonize(r, rs, deps); - if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs)) { - mark_solved(idx); - return; - } - else if (lhs.empty() || (lhs.size() == 1 && lhs[0].get() == l)) { - // continue - } - else { - TRACE("seq", - for (unsigned j = 0; j < lhs.size(); ++j) { - tout << mk_pp(lhs[j].get(), m) << " "; - } - tout << "\n"; - tout << mk_pp(l, m) << " != " << mk_pp(r, m) << "\n";); - - for (unsigned j = 0; j < lhs.size(); ++j) { - expr_ref nl(lhs[j].get(), m); - expr_ref nr(rhs[j].get(), m); - if (m_util.is_seq(nl) || m_util.is_re(nl)) { - m_trail_stack.push(push_ne(*this, idx, nl, nr)); - } - else { - literal lit(mk_eq(nl, nr, false)); - m_trail_stack.push(push_lit(*this, idx, lit)); - ctx.mark_as_relevant(lit); - switch (ctx.get_assignment(lit)) { - case l_false: - mark_solved(idx); - return; - case l_true: - break; - case l_undef: - ++num_undef_lits; - m_new_propagation = true; - break; - } - } - } - m_trail_stack.push(push_dep(*this, idx, deps)); - erase_index(idx, i); - --i; - } - } - if (num_undef_lits == 1 && n.m_lhs.empty()) { - literal_vector lits; - literal undef_lit = null_literal; - for (unsigned i = 0; i < n.m_lits.size(); ++i) { - literal lit = n.m_lits[i]; - switch (ctx.get_assignment(lit)) { - case l_true: - lits.push_back(lit); - break; - case l_false: - UNREACHABLE(); - break; - case l_undef: - SASSERT(undef_lit == null_literal); - undef_lit = lit; - break; - } - } - TRACE("seq", tout << "propagate: " << undef_lit << "\n";); - SASSERT(undef_lit != null_literal); - propagate_lit(n.m_dep, lits.size(), lits.c_ptr(), ~undef_lit); - } - else if (num_undef_lits == 0 && n.m_lhs.empty()) { - literal_vector lits(n.m_lits); - lits.push_back(~mk_eq(n.m_l, n.m_r, false)); - set_conflict(n.m_dep, lits); - SASSERT(m_new_propagation); - } - else if (false && num_undef_lits == 0 && n.m_lhs.size() == 1) { - expr* l = n.m_lhs[0]; - expr* r = n.m_rhs[0]; - if (m_util.str.is_empty(r)) { - std::swap(l, r); - } - if (m_util.str.is_empty(l) && is_var(r)) { - literal lit = ~mk_eq_empty(r); - switch (ctx.get_assignment(lit)) { - case l_true: { - expr_ref head(m), tail(m); - mk_decompose(r, head, tail); - expr_ref conc = mk_concat(head, tail); - propagate_is_conc(r, conc); - m_new_propagation = true; - break; - } - case l_undef: - m_new_propagation = true; - break; - case l_false: - break; - } - } - } -} - - -#if 0 -bool theory_seq::solve_ne2(unsigned idx) { - context& ctx = get_context(); - ne2 const& n = m_nqs[idx]; - TRACE("seq", display_disequation(tout, n);); - unsigned num_undef_lits = 0; for (unsigned i = 0; i < n.lits().size(); ++i) { switch (ctx.get_assignment(n.lits(i))) { @@ -1083,10 +966,10 @@ bool theory_seq::solve_ne2(unsigned idx) { break; } } - unsigned_vector unchanged; - dependency* new_deps = 0; + + dependency* new_deps = n.dep(); vector new_ls, new_rs; - literal_vector new_lits = n.lits(); + literal_vector new_lits(n.lits()); bool updated = false; for (unsigned i = 0; i < n.ls().size(); ++i) { expr_ref_vector& ls = m_ls; @@ -1095,34 +978,49 @@ bool theory_seq::solve_ne2(unsigned idx) { expr_ref_vector& rhs = m_rhs; ls.reset(); rs.reset(); lhs.reset(); rhs.reset(); dependency* deps = 0; - expr_ref_vector const& l = n.ls(i); - expr_ref_vector const& r = n.rs(i); - change = canonize(l, ls, deps) || change; - change = canonize(r, rs, deps) || change; - if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs)) { + bool change = false; + change = canonize(n.ls(i), ls, deps) || change; + change = canonize(n.rs(i), rs, deps) || change; + + if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs, change)) { return true; } - else if (!change && lhs.empty()) { - unchanged.push_back(i); - } - else if (change && lhs.empty()) { - + else if (!change) { +// std::cout << n.ls(i) << " " << ls << "\n"; +// std::cout << n.rs(i) << " " << rs << "\n"; + continue; } else { + + if (!updated) { + for (unsigned j = 0; j < i; ++j) { + new_ls.push_back(n.ls(j)); + new_rs.push_back(n.rs(j)); + } + } updated = true; + if (!ls.empty() || !rs.empty()) { + new_ls.push_back(ls); + new_rs.push_back(rs); + } TRACE("seq", for (unsigned j = 0; j < lhs.size(); ++j) { tout << mk_pp(lhs[j].get(), m) << " "; } tout << "\n"; - tout << l << " != " << r << "\n";); + tout << n.ls(i) << " != " << n.rs(i) << "\n";); for (unsigned j = 0; j < lhs.size(); ++j) { - expr_ref nl(lhs[j].get(), m); - expr_ref nr(rhs[j].get(), m); + expr* nl = lhs[j].get(); + expr* nr = rhs[j].get(); if (m_util.is_seq(nl) || m_util.is_re(nl)) { - new_ls.push_back(nl); - new_rs.push_back(nr); + ls.reset(); + rs.reset(); + SASSERT(!m_util.str.is_concat(nl)); + SASSERT(!m_util.str.is_concat(nr)); + ls.push_back(nl); rs.push_back(nr); + new_ls.push_back(ls); + new_rs.push_back(rs); } else { literal lit(mk_eq(nl, nr, false)); @@ -1140,7 +1038,7 @@ bool theory_seq::solve_ne2(unsigned idx) { } } } - new_deps = deps; + new_deps = m_dm.mk_join(deps, new_deps); } } if (num_undef_lits == 1 && new_ls.empty()) { @@ -1166,31 +1064,19 @@ bool theory_seq::solve_ne2(unsigned idx) { propagate_lit(new_deps, lits.size(), lits.c_ptr(), ~undef_lit); return true; } - else if (num_undef_lits == 0 && new_ls.empty()) { - set_conflict(new_deps, new_lits); - SASSERT(m_new_propagation); - return true; + else if (updated) { + if (num_undef_lits == 0 && new_ls.empty()) { + TRACE("seq", tout << "conflict\n";); + set_conflict(new_deps, new_lits); + SASSERT(m_new_propagation); + } + else { + m_nqs.push_back(ne(new_ls, new_rs, new_lits, new_deps)); + } } - else if (change) { - - } - return change; + return updated; } -#endif - -void theory_seq::mark_solved(unsigned idx) { - m_trail_stack.push(solved_ne(*this, idx)); -} - -void theory_seq::erase_index(unsigned idx, unsigned i) { - ne const& n = m_nqs[idx]; - unsigned sz = n.m_lhs.size(); - if (i + 1 != sz) { - m_trail_stack.push(set_ne(*this, idx, i, n.m_lhs[sz-1], n.m_rhs[sz-1])); - } - m_trail_stack.push(pop_ne(*this, idx)); -} bool theory_seq::simplify_and_solve_eqs() { context & ctx = get_context(); @@ -1308,26 +1194,24 @@ void theory_seq::display_equations(std::ostream& out) const { void theory_seq::display_disequations(std::ostream& out) const { bool first = true; for (unsigned i = 0; i < m_nqs.size(); ++i) { - if (!m_nqs[i].is_solved()) { - if (first) out << "Disequations:\n"; - first = false; - display_disequation(out, m_nqs[i]); - } - } + if (first) out << "Disequations:\n"; + first = false; + display_disequation(out, m_nqs[i]); + } } void theory_seq::display_disequation(std::ostream& out, ne const& e) const { - for (unsigned j = 0; j < e.m_lits.size(); ++j) { - out << e.m_lits[j] << " "; + for (unsigned j = 0; j < e.lits().size(); ++j) { + out << e.lits(j) << " "; } - if (e.m_lits.size() > 0) { + if (e.lits().size() > 0) { out << "\n"; } - for (unsigned j = 0; j < e.m_lhs.size(); ++j) { - out << mk_pp(e.m_lhs[j], m) << " != " << mk_pp(e.m_rhs[j], m) << "\n"; + for (unsigned j = 0; j < e.ls().size(); ++j) { + out << e.ls(j) << " != " << e.rs(j) << "\n"; } - if (e.m_dep) { - display_deps(out, e.m_dep); + if (e.dep()) { + display_deps(out, e.dep()); } } @@ -1529,44 +1413,40 @@ expr_ref theory_seq::canonize(expr* e, dependency*& eqs) { return result; } -bool theory_seq::canonize(expr* e0, expr_ref_vector& es, dependency*& eqs) { - dependency* dep = 0; - expr* e = m_rep.find(e0, dep); - bool change = e != e0; +bool theory_seq::canonize(expr* e, expr_ref_vector& es, dependency*& eqs) { expr* e1, *e2; - if (m_util.str.is_concat(e, e1, e2)) { - change = canonize(e1, es, eqs) || change; - change = canonize(e2, es, eqs) || change; - } - else if (m_util.str.is_empty(e)) { - // skip - } - else { - expr_ref e3 = expand(e, eqs); - if (m_util.str.is_concat(e3) || m_util.str.is_empty(e3)) { - change = canonize(e3, es, eqs) || change; + expr_ref e3(e, m); + bool change = false; + while (true) { + if (m_util.str.is_concat(e3, e1, e2)) { + canonize(e1, es, eqs); + e3 = e2; + change = true; + continue; + } + if (m_util.str.is_empty(e3)) { + return true; + } + + expr_ref e4 = expand(e3, eqs); + change |= e4 != e3; + if (m_util.str.is_concat(e4) || m_util.str.is_empty(e4)) { + e3 = e4; + continue; } else { - change = e3 != e || change; - es.push_back(e3); + es.push_back(e4); + break; } } - eqs = m_dm.mk_join(eqs, dep); return change; } bool theory_seq::canonize(expr_ref_vector const& es, expr_ref_vector& result, dependency*& eqs) { - dependency* dep = 0; bool change = false; for (unsigned i = 0; i < es.size(); ++i) { - expr_ref r = expand(es[i], eqs); - change |= r != es[i]; - if (m_util.str.is_concat(r)) { - canonize(r, result, eqs); - } - else if (!m_util.str.is_empty(r)) { - result.push_back(r); - } + change = canonize(es[i], result, eqs) || change; + SASSERT(!m_util.str.is_concat(es[i]) || change); } return change; } @@ -2093,7 +1973,7 @@ void theory_seq::ensure_nth(literal lit, expr* s, expr* idx) { s2 = tail; } elems.push_back(s2); - conc = mk_concat(elems); + conc = mk_concat(elems, m.get_sort(s)); propagate_eq(lit, s, conc, true); } @@ -2295,7 +2175,10 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { expr_ref eq(m.mk_eq(e1, e2), m); m_rewrite(eq); if (!m.is_false(eq)) { - m_nqs.push_back(ne(e1, e2)); + literal lit = ~mk_eq(e1, e2, false); + SASSERT(get_context().get_assignment(lit) == l_true); + dependency* dep = m_dm.mk_leaf(assumption(lit)); + m_nqs.push_back(ne(e1, e2, dep)); solve_nqs(m_nqs.size() - 1); } // add solution for variable that is non-empty? diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 1e19bcddb..d14dbba6d 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -141,22 +141,30 @@ namespace smt { } - class ne2 { + class ne { vector m_lhs; vector m_rhs; literal_vector m_lits; dependency* m_dep; public: - ne2(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep): + ne(expr_ref const& l, expr_ref const& r, dependency* dep): m_dep(dep) { - m_lhs.push_back(l); - m_rhs.push_back(r); + expr_ref_vector ls(l.get_manager()); ls.push_back(l); + expr_ref_vector rs(r.get_manager()); rs.push_back(r); + m_lhs.push_back(ls); + m_rhs.push_back(rs); } - ne2(ne2 const& other): + ne(vector const& l, vector const& r, literal_vector const& lits, dependency* dep): + m_lhs(l), + m_rhs(r), + m_lits(lits), + m_dep(dep) {} + + ne(ne const& other): m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_lits(other.m_lits), m_dep(other.m_dep) {} - ne2& operator=(ne2 const& other) { + ne& operator=(ne const& other) { if (this != &other) { m_lhs.reset(); m_lhs.append(other.m_lhs); m_rhs.reset(); m_rhs.append(other.m_rhs); @@ -174,136 +182,6 @@ namespace smt { dependency* dep() const { return m_dep; } }; - - // asserted or derived disqequality with dependencies - struct ne { - bool m_solved; - expr_ref m_l, m_r; - expr_ref_vector m_lhs; - expr_ref_vector m_rhs; - literal_vector m_lits; - dependency* m_dep; - ne(expr_ref& l, expr_ref& r): - m_solved(false), m_l(l), m_r(r), m_lhs(l.get_manager()), m_rhs(r.get_manager()), m_dep(0) { - m_lhs.push_back(l); - m_rhs.push_back(r); - } - ne(ne const& other): - m_solved(other.m_solved), m_l(other.m_l), m_r(other.m_r), m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_lits(other.m_lits), m_dep(other.m_dep) {} - ne& operator=(ne const& other) { - m_solved = other.m_solved; - m_l = other.m_l; - m_r = other.m_r; - m_lhs.reset(); m_lhs.append(other.m_lhs); - m_rhs.reset(); m_rhs.append(other.m_rhs); - m_lits.reset(); m_lits.append(other.m_lits); - m_dep = other.m_dep; - return *this; - } - bool is_solved() const { return m_solved; } - }; - - class pop_lit : public trail { - unsigned m_idx; - literal m_lit; - public: - pop_lit(theory_seq& th, unsigned idx): m_idx(idx), m_lit(th.m_nqs[idx].m_lits.back()) { - th.m_nqs.ref(m_idx).m_lits.pop_back(); - } - virtual void undo(theory_seq & th) { th.m_nqs.ref(m_idx).m_lits.push_back(m_lit); } - }; - class push_lit : public trail { - unsigned m_idx; - public: - push_lit(theory_seq& th, unsigned idx, literal lit): m_idx(idx) { - th.m_nqs.ref(m_idx).m_lits.push_back(lit); - } - virtual void undo(theory_seq & th) { th.m_nqs.ref(m_idx).m_lits.pop_back(); } - }; - class set_lit : public trail { - unsigned m_idx; - unsigned m_i; - literal m_lit; - public: - set_lit(theory_seq& th, unsigned idx, unsigned i, literal lit): - m_idx(idx), m_i(i), m_lit(th.m_nqs[idx].m_lits[i]) { - th.m_nqs.ref(m_idx).m_lits[i] = lit; - } - virtual void undo(theory_seq & th) { th.m_nqs.ref(m_idx).m_lits[m_i] = m_lit; } - }; - - class solved_ne : public trail { - unsigned m_idx; - public: - solved_ne(theory_seq& th, unsigned idx) : m_idx(idx) { th.m_nqs.ref(idx).m_solved = true; } - virtual void undo(theory_seq& th) { th.m_nqs.ref(m_idx).m_solved = false; } - }; - void mark_solved(unsigned idx); - - class push_ne : public trail { - unsigned m_idx; - public: - push_ne(theory_seq& th, unsigned idx, expr* l, expr* r) : m_idx(idx) { - th.m_nqs.ref(m_idx).m_lhs.push_back(l); - th.m_nqs.ref(m_idx).m_rhs.push_back(r); - } - virtual void undo(theory_seq& th) { th.m_nqs.ref(m_idx).m_lhs.pop_back(); th.m_nqs.ref(m_idx).m_rhs.pop_back(); } - }; - - class pop_ne : public trail { - expr_ref m_lhs; - expr_ref m_rhs; - unsigned m_idx; - public: - pop_ne(theory_seq& th, unsigned idx): - m_lhs(th.m_nqs[idx].m_lhs.back(), th.m), - m_rhs(th.m_nqs[idx].m_rhs.back(), th.m), - m_idx(idx) { - th.m_nqs.ref(idx).m_lhs.pop_back(); - th.m_nqs.ref(idx).m_rhs.pop_back(); - } - virtual void undo(theory_seq& th) { - th.m_nqs.ref(m_idx).m_lhs.push_back(m_lhs); - th.m_nqs.ref(m_idx).m_rhs.push_back(m_rhs); - m_lhs.reset(); - m_rhs.reset(); - } - }; - - class set_ne : public trail { - expr_ref m_lhs; - expr_ref m_rhs; - unsigned m_idx; - unsigned m_i; - public: - set_ne(theory_seq& th, unsigned idx, unsigned i, expr* l, expr* r): - m_lhs(th.m_nqs[idx].m_lhs[i], th.m), - m_rhs(th.m_nqs[idx].m_rhs[i], th.m), - m_idx(idx), - m_i(i) { - th.m_nqs.ref(idx).m_lhs[i] = l; - th.m_nqs.ref(idx).m_rhs[i] = r; - } - virtual void undo(theory_seq& th) { - th.m_nqs.ref(m_idx).m_lhs[m_i] = m_lhs; - th.m_nqs.ref(m_idx).m_rhs[m_i] = m_rhs; - m_lhs.reset(); - m_rhs.reset(); - } - }; - - class push_dep : public trail { - dependency* m_dep; - unsigned m_idx; - public: - push_dep(theory_seq& th, unsigned idx, dependency* d): m_dep(th.m_nqs[idx].m_dep), m_idx(idx) { - th.m_nqs.ref(idx).m_dep = d; - } - virtual void undo(theory_seq& th) { - th.m_nqs.ref(m_idx).m_dep = m_dep; - } - }; - class apply { public: virtual ~apply() {} @@ -441,12 +319,13 @@ namespace smt { bool solve_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep); bool propagate_max_length(expr* l, expr* r, dependency* dep); + expr_ref mk_empty(sort* s) { return expr_ref(m_util.str.mk_empty(s), m); } expr_ref mk_concat(unsigned n, expr*const* es) { return expr_ref(m_util.str.mk_concat(n, es), m); } - expr_ref mk_concat(expr_ref_vector const& es) { return mk_concat(es.size(), es.c_ptr()); } + expr_ref mk_concat(expr_ref_vector const& es, sort* s) { if (es.empty()) return mk_empty(s); return mk_concat(es.size(), es.c_ptr()); } expr_ref mk_concat(expr* e1, expr* e2) { return expr_ref(m_util.str.mk_concat(e1, e2), m); } expr_ref mk_concat(expr* e1, expr* e2, expr* e3) { return expr_ref(m_util.str.mk_concat(e1, e2, e3), m); } bool solve_nqs(unsigned i); - void solve_ne(unsigned i); + bool solve_ne(unsigned i); // asserting consequences void linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const; From 0e6aaf02113eb2bc0f21b21148e17cfaf895aa18 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Jan 2016 20:05:49 -0800 Subject: [PATCH 2/7] Issue #407 build break Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 4 ++-- src/ast/seq_decl_plugin.cpp | 4 +++- src/smt/theory_seq.cpp | 16 +++++----------- 3 files changed, 10 insertions(+), 14 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index d85060f1d..d94e54935 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1064,13 +1064,13 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_ if (lchange) { if (head1 > 0) { for (unsigned i = 0; i < szl; ++i) { - ls[i] = ls[i + head1]; + ls[i] = ls[i + head1].get(); } } ls.shrink(szl); if (head2 > 0) { for (unsigned i = 0; i < szr; ++i) { - rs[i] = rs[i + head2]; + rs[i] = rs[i + head2].get(); } } rs.shrink(szr); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 9c8a085e8..165e24eac 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -666,5 +666,7 @@ void seq_util::str::get_concat(expr* e, expr_ref_vector& es) const { get_concat(e1, es); e = e2; } - es.push_back(e); + if (!is_empty(e)) { + es.push_back(e); + } } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index a51e32d90..4bc867717 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1422,21 +1422,15 @@ bool theory_seq::canonize(expr* e, expr_ref_vector& es, dependency*& eqs) { canonize(e1, es, eqs); e3 = e2; change = true; - continue; } - if (m_util.str.is_empty(e3)) { + else if (m_util.str.is_empty(e3)) { return true; } - - expr_ref e4 = expand(e3, eqs); - change |= e4 != e3; - if (m_util.str.is_concat(e4) || m_util.str.is_empty(e4)) { - e3 = e4; - continue; - } else { - es.push_back(e4); - break; + expr_ref e4 = expand(e3, eqs); + change |= e4 != e3; + m_util.str.get_concat(e4, es); + break; } } return change; From 023c564839a9930f39f89e47c3314ac9b1b36885 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Jan 2016 20:10:54 -0800 Subject: [PATCH 3/7] Issue #406 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 77af10463..afdca7464 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -536,7 +536,7 @@ class SortRef(AstRef): def __hash__(self): """ Hash code. """ - AstRef.__hash__(self) + return AstRef.__hash__(self) def is_sort(s): """Return `True` if `s` is a Z3 sort. @@ -802,7 +802,7 @@ class ExprRef(AstRef): def __hash__(self): """ Hash code. """ - AstRef.__hash__(self) + return AstRef.__hash__(self) def __ne__(self, other): """Return a Z3 expression that represents the constraint `self != other`. From 17a32a4e5f981e948bf10d405c41a917ed912baa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Jan 2016 20:14:16 -0800 Subject: [PATCH 4/7] ml build failure Signed-off-by: Nikolaj Bjorner --- src/api/ml/z3.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 54b9c3932..20986e438 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -835,11 +835,14 @@ end = struct let o = Z3native.mk_app (context_gno ctx) (AST.ptr_of_ast fa) (List.length args) (expr_lton args) in expr_of_ptr ctx o - let apply1 ctx f t = expr_of_ptr ctx (f (context_gno ctx) (gno t)) in + let apply1 ctx f t = + expr_of_ptr ctx (f (context_gno ctx) (gno t)) - let apply2 ctx f t1 t2 = expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2)) in + let apply2 ctx f t1 t2 = + expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2)) - let apply3 ctx f t1 t2 t3 = expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2) (gno t3)) in + let apply3 ctx f t1 t2 t3 = + expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2) (gno t3)) let simplify ( x : expr ) ( p : Params.params option ) = match p with From 183d3821cefa371b51e00b499b8a8ba04fc49347 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Jan 2016 20:14:43 -0800 Subject: [PATCH 5/7] ml build failure, issue #403 Signed-off-by: Nikolaj Bjorner --- src/api/ml/z3.ml | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 20986e438..9dc53133e 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -835,15 +835,14 @@ end = struct let o = Z3native.mk_app (context_gno ctx) (AST.ptr_of_ast fa) (List.length args) (expr_lton args) in expr_of_ptr ctx o - let apply1 ctx f t = - expr_of_ptr ctx (f (context_gno ctx) (gno t)) + let apply1 ctx f t = + expr_of_ptr ctx (f (context_gno ctx) (gno t)) - let apply2 ctx f t1 t2 = - expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2)) - - let apply3 ctx f t1 t2 t3 = - expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2) (gno t3)) + let apply2 ctx f t1 t2 = + expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2)) + let apply3 ctx f t1 t2 t3 = + expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2) (gno t3)) let simplify ( x : expr ) ( p : Params.params option ) = match p with | None -> expr_of_ptr (Expr.gc x) (Z3native.simplify (gnc x) (gno x)) From 98f750f90ded5c3a8f472ff780da385ba5e3bfcc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Jan 2016 20:37:47 -0800 Subject: [PATCH 6/7] ml build failure, issue #403 Signed-off-by: Nikolaj Bjorner --- src/api/ml/z3.ml | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 9dc53133e..bca0bdd1b 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -437,6 +437,8 @@ end = struct | UNINTERPRETED_SORT | FINITE_DOMAIN_SORT | RELATION_SORT + | RE_SORT + | SEQ_SORT | FLOATING_POINT_SORT | ROUNDING_MODE_SORT -> Sort(z3_native_object_of_ast_ptr ctx no) | UNKNOWN_SORT -> raise (Z3native.Exception "Unknown sort kind encountered") @@ -783,6 +785,10 @@ sig val mk_numeral_string : context -> string -> Sort.sort -> expr val mk_numeral_int : context -> int -> Sort.sort -> expr val equal : expr -> expr -> bool + val apply1 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr) -> expr -> expr + val apply2 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) -> expr -> expr -> expr + val apply3 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) + -> expr -> expr -> expr -> expr val compare : expr -> expr -> int end = struct type expr = Expr of AST.ast @@ -1075,8 +1081,9 @@ struct let f i = (Sort.sort_of_ptr (gc x) (Z3native.get_quantifier_bound_sort (gnc x) (gno x) i)) in mk_list f n - let get_body ( x : quantifier ) = - apply1 (gc x) Z3native.get_quantifier_body x + let get_body ( x : quantifier ) = + let ctx = gc x in + expr_of_ptr ctx (Z3native.get_quantifier_body (context_gno ctx) (gno x)) let mk_bound ( ctx : context ) ( index : int ) ( ty : Sort.sort ) = expr_of_ptr ctx (Z3native.mk_bound (context_gno ctx) index (Sort.gno ty)) @@ -1246,11 +1253,11 @@ struct apply2 ctx Z3native.mk_set_add set element let mk_del ( ctx : context ) ( set : expr ) ( element : expr ) = - apply2 Z3native.mk_set_del set element + apply2 ctx Z3native.mk_set_del set element let mk_union ( ctx : context ) ( args : expr list ) = - let r = expr_of_ptr ctx (Z3native.mk_set_union (context_gno ctx) (List.length args) (expr_lton args)) in - r + expr_of_ptr ctx (Z3native.mk_set_union (context_gno ctx) (List.length args) (expr_lton args)) + let mk_intersection ( ctx : context ) ( args : expr list ) = expr_of_ptr ctx (Z3native.mk_set_intersect (context_gno ctx) (List.length args) (expr_lton args)) From 7e3676e24ac31d1c9b3f71c8a38f041142ff1069 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 8 Jan 2016 13:25:14 +0000 Subject: [PATCH 7/7] bugfix for ML example --- examples/ml/ml_example.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/examples/ml/ml_example.ml b/examples/ml/ml_example.ml index df062bde4..5b1c05069 100644 --- a/examples/ml/ml_example.ml +++ b/examples/ml/ml_example.ml @@ -287,16 +287,15 @@ let fpa_example ( ctx : context ) = (* ((_ to_fp 11 53) #x401c000000000000)) *) (* ((_ to_fp 11 53) RTZ 1.75 2))) *) (* ((_ to_fp 11 53) RTZ 7.0))) *) - let c1 = (mk_fp ctx - (mk_numeral_string ctx "0" (BitVector.mk_sort ctx 1)) - (mk_numeral_string ctx "3377699720527872" (BitVector.mk_sort ctx 52)) - (mk_numeral_string ctx "1025" (BitVector.mk_sort ctx 11))) in + let c1 = (mk_fp ctx (mk_numeral_string ctx "0" (BitVector.mk_sort ctx 1)) + (mk_numeral_string ctx "1025" (BitVector.mk_sort ctx 11)) + (mk_numeral_string ctx "3377699720527872" (BitVector.mk_sort ctx 52))) in let c2 = (mk_to_fp_bv ctx (mk_numeral_string ctx "4619567317775286272" (BitVector.mk_sort ctx 64)) (mk_sort ctx 11 53)) in let c3 = (mk_to_fp_int_real ctx (RoundingMode.mk_rtz ctx) - (mk_numeral_string ctx "2" (Integer.mk_sort ctx)) + (mk_numeral_string ctx "2" (Integer.mk_sort ctx)) (mk_numeral_string ctx "1.75" (Real.mk_sort ctx)) (FloatingPoint.mk_sort ctx 11 53)) in let c4 = (mk_to_fp_real ctx (RoundingMode.mk_rtz ctx)