mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3 into new_ocaml_install

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-12-14 13:02:49 +00:00
commit 1f0b5cd0bc
35 changed files with 898 additions and 403 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/python/z3.py
View file

@ -5693,8 +5693,6 @@ class Statistics:
>>> s.check()
sat
>>> st = s.statistics()
>>> st.keys()
['nlsat propagations', 'nlsat stages', 'rlimit count', 'max memory', 'memory', 'num allocs']
"""
return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
@ -5730,8 +5728,6 @@ class Statistics:
>>> s.check()
sat
>>> st = s.statistics()
>>> st.keys()
['nlsat propagations', 'nlsat stages', 'rlimit count', 'max memory', 'memory', 'num allocs']
>>> st.nlsat_propagations
2
>>> st.nlsat_stages

10
src/ast/ast_smt2_pp.cpp
View file

@ -364,16 +364,18 @@ format * smt2_pp_environment::pp_arith_literal(app * t, bool decimal, unsigned d
}
format * smt2_pp_environment::pp_string_literal(app * t) {
std::string s;
zstring s;
std::string encs;
VERIFY (get_sutil().str.is_string(t, s));
encs = s.encode();
std::ostringstream buffer;
buffer << "\"";
for (unsigned i = 0; i < s.length(); ++i) {
if (s[i] == '\"') {
for (unsigned i = 0; i < encs.length(); ++i) {
if (encs[i] == '\"') {
buffer << "\"\"";
}
else {
buffer << s[i];
buffer << encs[i];
}
}
buffer << "\"";

2
src/ast/normal_forms/nnf.cpp
View file

@ -373,7 +373,7 @@ struct nnf::imp {
if (memory::get_allocation_size() > m_max_memory)
throw nnf_exception(Z3_MAX_MEMORY_MSG);
if (m().canceled())
throw nnf_exception(Z3_CANCELED_MSG);
throw nnf_exception(m().limit().get_cancel_msg());
}
void set_new_child_flag() {

2
src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
View file

@ -28,7 +28,7 @@ void bit_blaster_tpl<Cfg>::checkpoint() {
if (memory::get_allocation_size() > m_max_memory)
throw rewriter_exception(Z3_MAX_MEMORY_MSG);
if (m().canceled())
throw rewriter_exception(Z3_CANCELED_MSG);
throw rewriter_exception(m().limit().get_cancel_msg());
cooperate("bit-blaster");
}

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

@ -121,7 +121,7 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
(a + string) + string = a + string
*/
br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) {
std::string s1, s2;
zstring s1, s2;
expr* c, *d;
bool isc1 = m_util.str.is_string(a, s1);
bool isc2 = m_util.str.is_string(b, s2);
@ -150,10 +150,10 @@ br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) {
}
br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
std::string b;
zstring b;
m_es.reset();
m_util.str.get_concat(a, m_es);
size_t len = 0;
unsigned len = 0;
unsigned j = 0;
for (unsigned i = 0; i < m_es.size(); ++i) {
if (m_util.str.is_string(m_es[i], b)) {
@ -189,21 +189,21 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
}
br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result) {
std::string s;
zstring s;
rational pos, len;
if (m_util.str.is_string(a, s) && m_autil.is_numeral(b, pos) && m_autil.is_numeral(c, len) &&
pos.is_unsigned() && len.is_unsigned() && pos.get_unsigned() <= s.length()) {
unsigned _pos = pos.get_unsigned();
unsigned _len = len.get_unsigned();
result = m_util.str.mk_string(s.substr(_pos, _len));
result = m_util.str.mk_string(s.extract(_pos, _len));
return BR_DONE;
}
return BR_FAILED;
}
br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
std::string c, d;
zstring c, d;
if (m_util.str.is_string(a, c) && m_util.str.is_string(b, d)) {
result = m().mk_bool_val(0 != strstr(c.c_str(), d.c_str()));
result = m().mk_bool_val(c.contains(d));
return BR_DONE;
}
// check if subsequence of b is in a.
@ -225,15 +225,12 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
}
br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
std::string c;
zstring c;
rational r;
if (m_util.str.is_string(a, c) && m_autil.is_numeral(b, r) && r.is_unsigned()) {
unsigned j = r.get_unsigned();
if (j < c.length()) {
char ch = c[j];
c[0] = ch;
c[1] = 0;
result = m_util.str.mk_string(c);
result = m_util.str.mk_string(c.extract(j, 1));
return BR_DONE;
}
}
@ -241,19 +238,14 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
}
br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result) {
std::string s1, s2;
zstring s1, s2;
rational r;
bool isc1 = m_util.str.is_string(a, s1);
bool isc2 = m_util.str.is_string(b, s2);
if (isc1 && isc2 && m_autil.is_numeral(c, r) && r.is_unsigned()) {
for (unsigned i = r.get_unsigned(); i < s1.length(); ++i) {
if (strncmp(s1.c_str() + i, s2.c_str(), s2.length()) == 0) {
result = m_autil.mk_numeral(rational(i) - r, true);
return BR_DONE;
}
}
result = m_autil.mk_numeral(rational(-1), true);
int idx = s1.indexof(s2, r.get_unsigned());
result = m_autil.mk_numeral(rational(idx), true);
return BR_DONE;
}
if (m_autil.is_numeral(c, r) && r.is_neg()) {
@ -270,23 +262,10 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
}
br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& result) {
std::string s1, s2, s3;
zstring s1, s2, s3;
if (m_util.str.is_string(a, s1) && m_util.str.is_string(b, s2) &&
m_util.str.is_string(c, s3)) {
std::ostringstream buffer;
bool can_replace = true;
for (size_t i = 0; i < s1.length(); ) {
if (can_replace && strncmp(s1.c_str() + i, s2.c_str(), s2.length()) == 0) {
buffer << s3;
i += s2.length();
can_replace = false;
}
else {
buffer << s1[i];
++i;
}
}
result = m_util.str.mk_string(buffer.str());
result = m_util.str.mk_string(s1.replace(s2, s3));
return BR_DONE;
}
if (b == c) {
@ -298,15 +277,11 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu
br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
TRACE("seq", tout << mk_pp(a, m()) << " " << mk_pp(b, m()) << "\n";);
std::string s1, s2;
zstring s1, s2;
bool isc1 = m_util.str.is_string(a, s1);
bool isc2 = m_util.str.is_string(b, s2);
if (isc1 && isc2) {
bool prefix = s1.length() <= s2.length();
for (unsigned i = 0; i < s1.length() && prefix; ++i) {
prefix = s1[i] == s2[i];
}
result = m().mk_bool_val(prefix);
result = m().mk_bool_val(s1.prefixof(s2));
return BR_DONE;
}
if (m_util.str.is_empty(a)) {
@ -321,7 +296,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
if (a1 != b1 && isc1 && isc2) {
if (s1.length() <= s2.length()) {
if (strncmp(s1.c_str(), s2.c_str(), s1.length()) == 0) {
if (s1.prefixof(s2)) {
if (a == a1) {
result = m().mk_true();
return BR_DONE;
@ -329,10 +304,10 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
m_util.str.get_concat(a, as);
m_util.str.get_concat(b, bs);
SASSERT(as.size() > 1);
s2 = std::string(s2.c_str() + s1.length(), s2.length() - s1.length());
s2 = s2.extract(s1.length(), s2.length()-s1.length());
bs[0] = m_util.str.mk_string(s2);
result = m_util.str.mk_prefix(m_util.str.mk_concat(as.size()-1, as.c_ptr()+1),
m_util.str.mk_concat(bs.size(), bs.c_ptr()));
m_util.str.mk_concat(bs.size(), bs.c_ptr()));
return BR_REWRITE_FULL;
}
else {
@ -341,7 +316,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
}
}
else {
if (strncmp(s1.c_str(), s2.c_str(), s2.length()) == 0) {
if (s2.prefixof(s1)) {
if (b == b1) {
result = m().mk_false();
return BR_DONE;
@ -349,7 +324,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
m_util.str.get_concat(a, as);
m_util.str.get_concat(b, bs);
SASSERT(bs.size() > 1);
s1 = std::string(s1.c_str() + s2.length(), s1.length() - s2.length());
s1 = s1.extract(s2.length(), s1.length() - s2.length());
as[0] = m_util.str.mk_string(s1);
result = m_util.str.mk_prefix(m_util.str.mk_concat(as.size(), as.c_ptr()),
m_util.str.mk_concat(bs.size()-1, bs.c_ptr()+1));
@ -396,7 +371,7 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
result = m().mk_true();
return BR_DONE;
}
std::string s1, s2;
zstring s1, s2;
if (m_util.str.is_empty(a)) {
result = m().mk_true();
return BR_DONE;
@ -438,21 +413,18 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
}
if (isc1 && isc2) {
if (s1.length() == s2.length()) {
SASSERT(s1 != s2);
//SASSERT(s1 != s2);
result = m().mk_false();
return BR_DONE;
}
else if (s1.length() < s2.length()) {
bool suffix = true;
for (unsigned i = 0; i < s1.length(); ++i) {
suffix = s1[s1.length()-i-1] == s2[s2.length()-i-1];
}
bool suffix = s1.suffixof(s2);
if (suffix && a1 == 0) {
result = m().mk_true();
return BR_DONE;
}
else if (suffix) {
s2 = std::string(s2.c_str(), s2.length()-s1.length());
s2 = s2.extract(0, s2.length()-s1.length());
b2 = m_util.str.mk_string(s2);
result = m_util.str.mk_suffix(a1, b1?m_util.str.mk_concat(b1, b2):b2);
return BR_DONE;
@ -468,12 +440,9 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
result = m().mk_false();
return BR_DONE;
}
bool suffix = true;
for (unsigned i = 0; i < s2.length(); ++i) {
suffix = s1[s1.length()-i-1] == s2[s2.length()-i-1];
}
bool suffix = s2.suffixof(s1);
if (suffix) {
s1 = std::string(s1.c_str(), s1.length()-s2.length());
s1 = s1.extract(0, s1.length()-s2.length());
a2 = m_util.str.mk_string(s1);
result = m_util.str.mk_suffix(a1?m_util.str.mk_concat(a1, a2):a2, b1);
return BR_DONE;
@ -491,14 +460,15 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) {
rational r;
if (m_autil.is_numeral(a, r)) {
result = m_util.str.mk_string(r.to_string());
result = m_util.str.mk_string(symbol(r.to_string().c_str()));
return BR_DONE;
}
return BR_FAILED;
}
br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
std::string s;
if (m_util.str.is_string(a, s)) {
zstring str;
if (m_util.str.is_string(a, str)) {
std::string s = str.encode();
for (unsigned i = 0; i < s.length(); ++i) {
if (s[i] == '-') { if (i != 0) return BR_FAILED; }
else if ('0' <= s[i] && s[i] <= '9') continue;
@ -550,6 +520,7 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs) {
expr* a, *b;
zstring s;
bool change = false;
expr_ref_vector trail(m());
m_lhs.reset();
@ -558,23 +529,55 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
m_util.str.get_concat(r, m_rhs);
// solve from back
while (!m_lhs.empty() && !m_rhs.empty()) {
if (m_lhs.back() == m_rhs.back()) {
while (true) {
while (!m_rhs.empty() && m_util.str.is_empty(m_rhs.back())) {
m_rhs.pop_back();
change = true;
}
while (!m_lhs.empty() && m_util.str.is_empty(m_lhs.back())) {
m_lhs.pop_back();
change = true;
}
if (m_lhs.empty() || m_rhs.empty()) {
break;
}
expr* l = m_lhs.back();
expr* r = m_rhs.back();
if (m_util.str.is_unit(r) && m_util.str.is_string(l)) {
std::swap(l, r);
std::swap(m_lhs, m_rhs);
}
if (l == r) {
m_lhs.pop_back();
m_rhs.pop_back();
}
else if(m_util.str.is_unit(m_lhs.back(), a) &&
m_util.str.is_unit(m_rhs.back(), b)) {
else if(m_util.str.is_unit(l, a) &&
m_util.str.is_unit(r, b)) {
lhs.push_back(a);
rhs.push_back(b);
m_lhs.pop_back();
m_rhs.pop_back();
}
else if (!m_rhs.empty() && m_util.str.is_empty(m_rhs.back())) {
m_rhs.pop_back();
}
else if (!m_lhs.empty() && m_util.str.is_empty(m_lhs.back())) {
else if (m_util.str.is_unit(l, a) && m_util.str.is_string(r, s)) {
SASSERT(s.length() > 0);
unsigned ch = s[s.length()-1];
SASSERT(s.num_bits() == m_butil.get_bv_size(a));
expr_ref bv(m());
bv = m_butil.mk_numeral(ch, s.num_bits());
SASSERT(m_butil.is_bv(a));
lhs.push_back(bv);
rhs.push_back(a);
m_lhs.pop_back();
if (s.length() == 1) {
m_rhs.pop_back();
}
else {
expr_ref s2(m_util.str.mk_string(s.extract(0, s.length()-2)), m());
m_rhs[m_rhs.size()-1] = s2;
trail.push_back(s2);
}
}
else {
break;
@ -584,23 +587,55 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
// solve from front
unsigned head1 = 0, head2 = 0;
while (head1 < m_lhs.size() && head2 < m_rhs.size()) {
if (m_lhs[head1] == m_rhs[head2]) {
while (true) {
while (head1 < m_lhs.size() && m_util.str.is_empty(m_lhs[head1])) {
++head1;
}
while (head2 < m_rhs.size() && m_util.str.is_empty(m_rhs[head2])) {
++head2;
}
if (head1 == m_lhs.size() || head2 == m_rhs.size()) {
break;
}
SASSERT(head1 < m_lhs.size() && head2 < m_rhs.size());
expr* l = m_lhs[head1];
expr* r = m_rhs[head2];
if (m_util.str.is_unit(r) && m_util.str.is_string(l)) {
std::swap(l, r);
std::swap(m_lhs, m_rhs);
}
if (l == r) {
++head1;
++head2;
}
else if(m_util.str.is_unit(m_lhs[head1], a) &&
m_util.str.is_unit(m_rhs[head2], b)) {
else if(m_util.str.is_unit(l, a) &&
m_util.str.is_unit(r, b)) {
lhs.push_back(a);
rhs.push_back(b);
++head1;
++head2;
}
else if (head1 < m_lhs.size() && m_util.str.is_empty(m_lhs[head1])) {
++head1;
}
else if (head2 < m_rhs.size() && m_util.str.is_empty(m_rhs[head2])) {
++head2;
else if (m_util.str.is_unit(l, a) && m_util.str.is_string(r, s)) {
SASSERT(s.length() > 0);
unsigned ch = s[0];
SASSERT(s.num_bits() == m_butil.get_bv_size(a));
expr_ref bv(m());
bv = m_butil.mk_numeral(ch, s.num_bits());
SASSERT(m_butil.is_bv(a));
lhs.push_back(bv);
rhs.push_back(a);
m_lhs.pop_back();
if (s.length() == 1) {
m_rhs.pop_back();
}
else {
expr_ref s2(m_util.str.mk_string(s.extract(1, s.length()-1)), m());
m_rhs[m_rhs.size()-1] = s2;
trail.push_back(s2);
}
}
else {
break;
@ -608,13 +643,13 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
change = true;
}
// reduce strings
std::string s1, s2;
zstring s1, s2;
while (head1 < m_lhs.size() &&
head2 < m_rhs.size() &&
m_util.str.is_string(m_lhs[head1], s1) &&
m_util.str.is_string(m_rhs[head2], s2)) {
size_t l = std::min(s1.length(), s2.length());
for (size_t i = 0; i < l; ++i) {
unsigned l = std::min(s1.length(), s2.length());
for (unsigned i = 0; i < l; ++i) {
if (s1[i] != s2[i]) {
return false;
}
@ -623,14 +658,14 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
++head1;
}
else {
m_lhs[head1] = m_util.str.mk_string(std::string(s1.c_str()+l,s1.length()-l));
m_lhs[head1] = m_util.str.mk_string(s1.extract(l, s1.length()-l));
trail.push_back(m_lhs[head1]);
}
if (l == s2.length()) {
++head2;
}
else {
m_rhs[head2] = m_util.str.mk_string(std::string(s2.c_str()+l,s2.length()-l));
m_rhs[head2] = m_util.str.mk_string(s2.extract(l, s2.length()-l));
trail.push_back(m_rhs[head2]);
}
change = true;
@ -639,8 +674,8 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
head2 < m_rhs.size() &&
m_util.str.is_string(m_lhs.back(), s1) &&
m_util.str.is_string(m_rhs.back(), s2)) {
size_t l = std::min(s1.length(), s2.length());
for (size_t i = 0; i < l; ++i) {
unsigned l = std::min(s1.length(), s2.length());
for (unsigned i = 0; i < l; ++i) {
if (s1[s1.length()-i-1] != s2[s2.length()-i-1]) {
return false;
}
@ -648,11 +683,11 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
m_lhs.pop_back();
m_rhs.pop_back();
if (l < s1.length()) {
m_lhs.push_back(m_util.str.mk_string(std::string(s1.c_str(),s1.length()-l)));
m_lhs.push_back(m_util.str.mk_string(s1.extract(0, s1.length()-l)));
trail.push_back(m_lhs.back());
}
if (l < s2.length()) {
m_rhs.push_back(m_util.str.mk_string(std::string(s2.c_str(),s2.length()-l)));
m_rhs.push_back(m_util.str.mk_string(s2.extract(0, s2.length()-l)));
trail.push_back(m_rhs.back());
}
change = true;
@ -703,7 +738,7 @@ expr* seq_rewriter::concat_non_empty(unsigned n, expr* const* as) {
}
bool seq_rewriter::set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs) {
std::string s;
zstring s;
for (unsigned i = 0; i < sz; ++i) {
if (m_util.str.is_unit(es[i])) {
if (all) return false;
@ -725,8 +760,8 @@ bool seq_rewriter::set_empty(unsigned sz, expr* const* es, bool all, expr_ref_ve
return true;
}
bool seq_rewriter::min_length(unsigned n, expr* const* es, size_t& len) {
std::string s;
bool seq_rewriter::min_length(unsigned n, expr* const* es, unsigned& len) {
zstring s;
bool bounded = true;
len = 0;
for (unsigned i = 0; i < n; ++i) {
@ -749,7 +784,7 @@ bool seq_rewriter::min_length(unsigned n, expr* const* es, size_t& len) {
bool seq_rewriter::length_constrained(unsigned szl, expr* const* l, unsigned szr, expr* const* r,
expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat) {
is_sat = true;
size_t len1 = 0, len2 = 0;
unsigned len1 = 0, len2 = 0;
bool bounded1 = min_length(szl, l, len1);
bool bounded2 = min_length(szr, r, len2);
if (bounded1 && len1 < len2) {

6
src/ast/rewriter/seq_rewriter.h
View file

@ -21,6 +21,7 @@ Notes:
#include"seq_decl_plugin.h"
#include"arith_decl_plugin.h"
#include"bv_decl_plugin.h"
#include"rewriter_types.h"
#include"params.h"
#include"lbool.h"
@ -32,6 +33,7 @@ Notes:
class seq_rewriter {
seq_util m_util;
arith_util m_autil;
bv_util m_butil;
ptr_vector<expr> m_es, m_lhs, m_rhs;
br_status mk_seq_concat(expr* a, expr* b, expr_ref& result);
@ -58,12 +60,12 @@ class seq_rewriter {
expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat);
bool length_constrained(unsigned n, expr* const* l, unsigned m, expr* const* r,
expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat);
bool min_length(unsigned n, expr* const* es, size_t& len);
bool min_length(unsigned n, expr* const* es, unsigned& len);
expr* concat_non_empty(unsigned n, expr* const* es);
public:
seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
m_util(m), m_autil(m) {
m_util(m), m_autil(m), m_butil(m) {
}
ast_manager & m() const { return m_util.get_manager(); }
family_id get_fid() const { return m_util.get_family_id(); }

159
src/ast/seq_decl_plugin.cpp
View file

@ -22,6 +22,145 @@ Revision History:
#include "ast_pp.h"
#include <sstream>
zstring::zstring(encoding enc): m_encoding(enc) {}
zstring::zstring(char const* s, encoding enc): m_encoding(enc) {
// TBD: epply decoding
while (*s) {
m_buffer.push_back(*s);
++s;
}
}
zstring::zstring(zstring const& other) {
m_buffer = other.m_buffer;
m_encoding = other.m_encoding;
}
zstring::zstring(unsigned num_bits, bool const* ch) {
SASSERT(num_bits == 8 || num_bits == 16);
m_encoding = (num_bits == 8)?ascii:unicode;
unsigned n = 0;
for (unsigned i = 0; i < num_bits; ++i) {
n |= (((unsigned)ch[i]) << num_bits);
}
m_buffer.push_back(n);
}
zstring::zstring(unsigned ch, encoding enc) {
m_encoding = enc;
m_buffer.push_back(ch & ((enc == ascii)?0x000000FF:0x0000FFFF));
}
zstring& zstring::operator=(zstring const& other) {
m_encoding = other.m_encoding;
m_buffer.reset();
m_buffer.append(other.m_buffer);
return *this;
}
zstring zstring::replace(zstring const& src, zstring const& dst) const {
zstring result(m_encoding);
if (length() < src.length()) {
return zstring(*this);
}
bool found = false;
for (unsigned i = 0; i <= length() - src.length(); ++i) {
bool eq = !found;
for (unsigned j = 0; eq && j < src.length(); ++j) {
eq = m_buffer[i+j] == src[j];
}
if (eq) {
result.m_buffer.append(dst.m_buffer);
found = true;
}
else {
result.m_buffer.push_back(m_buffer[i]);
}
}
return result;
}
std::string zstring::encode() const {
// TBD apply encodings.
SASSERT(m_encoding == ascii);
std::ostringstream strm;
for (unsigned i = 0; i < m_buffer.size(); ++i) {
strm << (char)(m_buffer[i]);
}
return strm.str();
}
bool zstring::suffixof(zstring const& other) const {
if (length() > other.length()) return false;
bool suffix = true;
for (unsigned i = 0; suffix && i < length(); ++i) {
suffix = m_buffer[length()-i-1] == other[other.length()-i-1];
}
return suffix;
}
bool zstring::prefixof(zstring const& other) const {
if (length() > other.length()) return false;
bool prefix = true;
for (unsigned i = 0; prefix && i < length(); ++i) {
prefix = m_buffer[i] == other[i];
}
return prefix;
}
bool zstring::contains(zstring const& other) const {
if (other.length() > length()) return false;
unsigned last = length() - other.length();
bool cont = false;
for (unsigned i = 0; !cont && i <= last; ++i) {
cont = true;
for (unsigned j = 0; cont && j < other.length(); ++j) {
cont = other[j] == m_buffer[j+i];
}
}
return cont;
}
int zstring::indexof(zstring const& other, int offset) const {
SASSERT(offset >= 0);
if (offset == length()) return -1;
if (other.length() + offset > length()) return -1;
unsigned last = length() - other.length();
for (unsigned i = static_cast<unsigned>(offset); i <= last; ++i) {
bool prefix = true;
for (unsigned j = 0; prefix && j < other.length(); ++j) {
prefix = m_buffer[i + j] == other[j];
}
if (prefix) {
return static_cast<int>(i);
}
}
return -1;
}
zstring zstring::extract(int offset, int len) const {
zstring result(m_encoding);
SASSERT(0 <= offset && 0 <= len);
int last = std::min(offset+len, static_cast<int>(length()));
for (int i = offset; i < last; ++i) {
result.m_buffer.push_back(m_buffer[i]);
}
return result;
}
zstring zstring::operator+(zstring const& other) const {
SASSERT(m_encoding == other.m_encoding);
zstring result(*this);
result.m_buffer.append(other.m_buffer);
return result;
}
std::ostream& zstring::operator<<(std::ostream& out) const {
return out << encode();
}
seq_decl_plugin::seq_decl_plugin(): m_init(false),
m_stringc_sym("String"),
m_string(0),
@ -452,6 +591,14 @@ app* seq_decl_plugin::mk_string(symbol const& s) {
return m_manager->mk_const(f);
}
app* seq_decl_plugin::mk_string(zstring const& s) {
symbol sym(s.encode().c_str());
parameter param(sym);
func_decl* f = m_manager->mk_const_decl(m_stringc_sym, m_string,
func_decl_info(m_family_id, OP_STRING_CONST, 1, &param));
return m_manager->mk_const(f);
}
bool seq_decl_plugin::is_value(app* e) const {
return is_app_of(e, m_family_id, OP_STRING_CONST);
}
@ -463,6 +610,18 @@ app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort
return m.mk_app(f, n, args);
}
app* seq_util::str::mk_string(zstring const& s) { return u.seq.mk_string(s); }
bool seq_util::str::is_string(expr const* n, zstring& s) const {
if (is_string(n)) {
s = zstring(to_app(n)->get_decl()->get_parameter(0).get_symbol().bare_str());
return true;
}
else {
return false;
}
}
void seq_util::str::get_concat(expr* e, ptr_vector<expr>& es) const {
expr* e1, *e2;

48
src/ast/seq_decl_plugin.h
View file

@ -81,6 +81,36 @@ enum seq_op_kind {
};
class zstring {
public:
enum encoding {
ascii,
unicode
};
private:
buffer<unsigned> m_buffer;
encoding m_encoding;
public:
zstring(encoding enc = ascii);
zstring(char const* s, encoding enc = ascii);
zstring(zstring const& other);
zstring(unsigned num_bits, bool const* ch);
zstring(unsigned ch, encoding enc = ascii);
zstring& operator=(zstring const& other);
zstring replace(zstring const& src, zstring const& dst) const;
unsigned num_bits() const { return (m_encoding==ascii)?8:16; }
std::string encode() const;
unsigned length() const { return m_buffer.size(); }
unsigned operator[](unsigned i) const { return m_buffer[i]; }
bool empty() const { return m_buffer.empty(); }
bool suffixof(zstring const& other) const;
bool prefixof(zstring const& other) const;
bool contains(zstring const& other) const;
int indexof(zstring const& other, int offset) const;
zstring extract(int lo, int hi) const;
zstring operator+(zstring const& other) const;
std::ostream& operator<<(std::ostream& out) const;
};
class seq_decl_plugin : public decl_plugin {
struct psig {
@ -146,6 +176,7 @@ public:
bool is_char(ast* a) const { return a == m_char; }
app* mk_string(symbol const& s);
app* mk_string(zstring const& s);
};
class seq_util {
@ -161,6 +192,7 @@ public:
bool is_re(sort* s) const { return is_sort_of(s, m_fid, RE_SORT); }
bool is_re(sort* s, sort*& seq) const { return is_sort_of(s, m_fid, RE_SORT) && (seq = to_sort(s->get_parameter(0).get_ast()), true); }
bool is_seq(expr* e) const { return is_seq(m.get_sort(e)); }
bool is_seq(sort* s, sort*& seq) { return is_seq(s) && (seq = to_sort(s->get_parameter(0).get_ast()), true); }
bool is_re(expr* e) const { return is_re(m.get_sort(e)); }
bool is_re(expr* e, sort*& seq) const { return is_re(m.get_sort(e), seq); }
@ -171,14 +203,18 @@ public:
seq_util& u;
ast_manager& m;
family_id m_fid;
app* mk_string(char const* s) { return mk_string(symbol(s)); }
app* mk_string(std::string const& s) { return mk_string(symbol(s.c_str())); }
public:
str(seq_util& u): u(u), m(u.m), m_fid(u.m_fid) {}
sort* mk_seq(sort* s) { parameter param(s); return m.mk_sort(m_fid, SEQ_SORT, 1, &param); }
app* mk_empty(sort* s) { return m.mk_const(m.mk_func_decl(m_fid, OP_SEQ_EMPTY, 0, 0, 0, (expr*const*)0, s)); }
app* mk_string(zstring const& s);
app* mk_string(symbol const& s) { return u.seq.mk_string(s); }
app* mk_string(char const* s) { return mk_string(symbol(s)); }
app* mk_string(std::string const& s) { return mk_string(symbol(s.c_str())); }
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(mk_concat(a, b), c);
@ -190,17 +226,17 @@ public:
app* mk_prefix(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_PREFIX, 2, es); }
app* mk_suffix(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_SUFFIX, 2, es); }
app* mk_index(expr* a, expr* b, expr* i) { expr* es[3] = { a, b, i}; return m.mk_app(m_fid, OP_SEQ_INDEX, 3, es); }
app* mk_unit(expr* u) { return m.mk_app(m_fid, OP_SEQ_UNIT, 1, &u); }
bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); }
bool is_string(expr const* n, std::string& s) const {
return is_string(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol().str(), true);
}
bool is_string(expr const* n, symbol& s) const {
return is_string(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol(), true);
}
bool is_string(expr const* n, zstring& s) const;
bool is_empty(expr const* n) const { symbol s;
return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0);
}

4
src/muz/base/dl_context.h
View file

@ -487,9 +487,7 @@ namespace datalog {
// -----------------------------------
bool canceled() {
if (m.limit().inc()) return true;
m_last_status = CANCELED;
return false;
return m.canceled() && (m_last_status = CANCELED, true);
}
void cleanup();

6
src/muz/rel/rel_context.cpp
View file

@ -151,6 +151,7 @@ namespace datalog {
m_context.ensure_closed();
transform_rules();
if (m_context.canceled()) {
TRACE("dl", tout << "canceled\n";);
result = l_undef;
break;
}
@ -191,6 +192,7 @@ namespace datalog {
IF_VERBOSE(10, m_ectx.report_big_relations(1000, verbose_stream()););
if (m_context.canceled()) {
TRACE("dl", tout << "canceled\n";);
result = l_undef;
break;
}
@ -206,6 +208,7 @@ namespace datalog {
}
if (timeout_after_this_round) {
m_context.set_status(TIMEOUT);
TRACE("dl", tout << "timeout\n";);
result = l_undef;
break;
}
@ -272,6 +275,7 @@ namespace datalog {
if (some_non_empty) {
m_answer = mk_and(m, ans.size(), ans.c_ptr());
if (is_approx) {
TRACE("dl", tout << "approx\n";);
res = l_undef;
m_context.set_status(APPROX);
}
@ -286,6 +290,7 @@ namespace datalog {
m_answer = m.mk_false();
break;
case l_undef:
TRACE("dl", tout << "saturation in undef\n";);
break;
}
return res;
@ -367,6 +372,7 @@ namespace datalog {
m_last_result_relation->to_formula(m_answer);
if (!m_last_result_relation->is_precise()) {
m_context.set_status(APPROX);
TRACE("dl", tout << "approx\n";);
res = l_undef;
}
}

2
src/parsers/smt2/smt2parser.cpp
View file

@ -1069,7 +1069,7 @@ namespace smt2 {
void parse_string_const() {
SASSERT(curr() == scanner::STRING_TOKEN);
expr_stack().push_back(sutil().str.mk_string(m_scanner.get_string()));
expr_stack().push_back(sutil().str.mk_string(symbol(m_scanner.get_string())));
TRACE("smt2parser", tout << "new string: " << mk_pp(expr_stack().back(), m()) << "\n";);
next();
}

2
src/qe/qe.cpp
View file

@ -2051,7 +2051,7 @@ namespace qe {
void checkpoint() {
if (m.canceled())
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m.limit().get_cancel_msg());
cooperate("qe");
}

10
src/qe/qe_lite.cpp
View file

@ -738,7 +738,7 @@ namespace eq {
void checkpoint() {
cooperate("der");
if (m.canceled())
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m.limit().get_cancel_msg());
}
public:
@ -917,8 +917,8 @@ namespace ar {
void checkpoint() {
cooperate("der");
if (m.canceled())
throw tactic_exception(TACTIC_CANCELED_MSG);
}
throw tactic_exception(m.limit().get_cancel_msg());
}
public:
@ -2207,7 +2207,7 @@ namespace fm {
void checkpoint() {
cooperate("fm");
if (m.canceled())
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m.limit().get_cancel_msg());
}
public:
@ -2477,7 +2477,7 @@ class qe_lite_tactic : public tactic {
void checkpoint() {
if (m.canceled())
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m.limit().get_cancel_msg());
cooperate("qe-lite");
}

2
src/qe/qe_sat_tactic.cpp
View file

@ -662,7 +662,7 @@ namespace qe {
void checkpoint() {
if (m.canceled()) {
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m.limit().get_cancel_msg());
}
cooperate("qe-sat");
}

2
src/qe/qe_tactic.cpp
View file

@ -45,7 +45,7 @@ class qe_tactic : public tactic {
void checkpoint() {
if (m.canceled())
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m.limit().get_cancel_msg());
cooperate("qe");
}

4
src/sat/tactic/goal2sat.cpp
View file

@ -333,7 +333,7 @@ struct goal2sat::imp {
loop:
cooperate("goal2sat");
if (m.canceled())
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m.limit().get_cancel_msg());
if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
frame & fr = m_frame_stack.back();
@ -626,7 +626,7 @@ struct sat2goal::imp {
void checkpoint() {
if (m.canceled())
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m.limit().get_cancel_msg());
if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
}

2
src/smt/smt_model_finder.cpp
View file

@ -3318,7 +3318,7 @@ namespace smt {
void model_finder::checkpoint(char const* msg) {
cooperate(msg);
if (m_context && m_context->get_cancel_flag())
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m_context->get_manager().limit().get_cancel_msg());
}
mf::quantifier_info * model_finder::get_quantifier_info(quantifier * q) const {

2
src/smt/tactic/unit_subsumption_tactic.cpp
View file

@ -58,7 +58,7 @@ struct unit_subsumption_tactic : public tactic {
void checkpoint() {
if (m.canceled()) {
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m.limit().get_cancel_msg());
}
}

560
src/smt/theory_seq.cpp
View file

@ -27,6 +27,7 @@ Revision History:
using namespace smt;
void theory_seq::solution_map::update(expr* e, expr* r, enode_pair_dependency* d) {
m_cache.reset();
std::pair<expr*, enode_pair_dependency*> value;
if (m_map.find(e, value)) {
add_trail(DEL, e, value.first, value.second);
@ -47,21 +48,17 @@ void theory_seq::solution_map::add_trail(map_update op, expr* l, expr* r, enode_
expr* theory_seq::solution_map::find(expr* e, enode_pair_dependency*& d) {
std::pair<expr*, enode_pair_dependency*> value;
d = 0;
unsigned num_finds = 0;
expr* result = e;
while (m_map.find(result, value)) {
d = m_dm.mk_join(d, value.second);
result = value.first;
++num_finds;
}
if (num_finds > 1) { // path compression for original key only.
update(e, result, d);
}
return result;
}
void theory_seq::solution_map::pop_scope(unsigned num_scopes) {
if (num_scopes == 0) return;
m_cache.reset();
unsigned start = m_limit[m_limit.size() - num_scopes];
for (unsigned i = m_updates.size(); i > start; ) {
--i;
@ -80,12 +77,19 @@ void theory_seq::solution_map::pop_scope(unsigned num_scopes) {
}
void theory_seq::solution_map::display(std::ostream& out) const {
map_t::iterator it = m_map.begin(), end = m_map.end();
eqdep_map_t::iterator it = m_map.begin(), end = m_map.end();
for (; it != end; ++it) {
out << mk_pp(it->m_key, m) << " |-> " << mk_pp(it->m_value.first, m) << "\n";
}
}
bool theory_seq::exclusion_table::contains(expr* e, expr* r) const {
if (e->get_id() > r->get_id()) {
std::swap(e, r);
}
return m_table.contains(std::make_pair(e, r));
}
void theory_seq::exclusion_table::update(expr* e, expr* r) {
if (e->get_id() > r->get_id()) {
std::swap(e, r);
@ -118,9 +122,7 @@ void theory_seq::exclusion_table::display(std::ostream& out) const {
theory_seq::theory_seq(ast_manager& m):
theory(m.mk_family_id("seq")),
m(m),
m_dam(m_dep_array_value_manager, m_alloc),
m_rep(m, m_dm),
m_sort2len_fn(m),
m_factory(0),
m_ineqs(m),
m_exclude(m),
@ -128,14 +130,12 @@ theory_seq::theory_seq(ast_manager& m):
m_axioms_head(0),
m_branch_variable_head(0),
m_incomplete(false),
m_has_length(false),
m_model_completion(false),
m_rewrite(m),
m_util(m),
m_autil(m),
m_trail_stack(*this) {
m_lhs.push_back(expr_array());
m_rhs.push_back(expr_array());
m_deps.push_back(enode_pair_dependency_array());
m_prefix_sym = "seq.prefix.suffix";
m_suffix_sym = "seq.suffix.prefix";
m_left_sym = "seq.left";
@ -145,11 +145,6 @@ theory_seq::theory_seq(ast_manager& m):
}
theory_seq::~theory_seq() {
unsigned num_scopes = m_lhs.size()-1;
if (num_scopes > 0) pop_scope_eh(num_scopes);
m.del(m_lhs.back());
m.del(m_rhs.back());
m_dam.del(m_deps.back());
}
@ -166,18 +161,30 @@ final_check_status theory_seq::final_check_eh() {
return FC_CONTINUE;
}
if (branch_variable()) {
TRACE("seq", tout << "branch\n";);
return FC_CONTINUE;
}
if (split_variable()) {
TRACE("seq", tout << "split_variable\n";);
return FC_CONTINUE;
}
if (ctx.inconsistent()) {
return FC_CONTINUE;
}
if (m.size(m_lhs.back()) > 0 || m_incomplete) {
return FC_GIVEUP;
if (!check_length_coherence()) {
TRACE("seq", tout << "check_length_coherence\n";);
return FC_CONTINUE;
}
return FC_DONE;
if (!check_length_coherence_tbd()) {
TRACE("seq", tout << "check_length_coherence\n";);
return FC_GIVEUP;
}
if (is_solved()) {
TRACE("seq", tout << "is_solved\n";);
return FC_DONE;
}
return FC_GIVEUP;
}
bool theory_seq::check_ineqs() {
@ -192,25 +199,24 @@ bool theory_seq::check_ineqs() {
propagate_lit(eqs, ctx.get_literal(a));
return false;
}
else if (!m.is_false(b)) {
TRACE("seq", tout << "Disequality is undetermined: " << mk_pp(a, m) << " " << b << "\n";);
}
}
return true;
}
bool theory_seq::branch_variable() {
context& ctx = get_context();
TRACE("seq", ctx.display(tout););
expr_array& lhs = m_lhs.back();
expr_array& rhs = m_rhs.back();
unsigned sz = m.size(lhs);
unsigned sz = m_eqs.size();
ptr_vector<expr> ls, rs;
for (unsigned i = 0; i < sz; ++i) {
unsigned k = (i + m_branch_variable_head) % sz;
expr* l = m.get(lhs, k);
expr* r = m.get(rhs, k);
TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << "\n";);
eq e = m_eqs[k];
TRACE("seq", tout << e.m_lhs << " = " << e.m_rhs << "\n";);
ls.reset(); rs.reset();
m_util.str.get_concat(l, ls);
m_util.str.get_concat(r, rs);
m_util.str.get_concat(e.m_lhs, ls);
m_util.str.get_concat(e.m_rhs, rs);
if (!ls.empty() && find_branch_candidate(ls[0], rs)) {
m_branch_variable_head = k;
@ -242,10 +248,10 @@ bool theory_seq::find_branch_candidate(expr* l, ptr_vector<expr> const& rs) {
if (occurs(l, rs[j])) {
return false;
}
std::string s;
zstring s;
if (m_util.str.is_string(rs[j], s)) {
for (size_t k = 1; k < s.length(); ++k) {
v = m_util.str.mk_string(std::string(s.c_str(), k));
v = m_util.str.mk_string(s.extract(0, k));
if (v0) v = m_util.str.mk_concat(v0, v);
if (assume_equality(l, v)) {
return true;
@ -267,11 +273,11 @@ bool theory_seq::assume_equality(expr* l, expr* r) {
}
else {
TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << "\n";);
if (!ctx.e_internalized(l)) ctx.internalize(l, false);
if (!ctx.e_internalized(r)) ctx.internalize(r, false);
ctx.mark_as_relevant(ctx.get_enode(l));
ctx.mark_as_relevant(ctx.get_enode(r));
ctx.assume_eq(ctx.get_enode(l), ctx.get_enode(r));
enode* n1 = ensure_enode(l);
enode* n2 = ensure_enode(r);
ctx.mark_as_relevant(n1);
ctx.mark_as_relevant(n2);
ctx.assume_eq(n1, n2);
return true;
}
}
@ -281,13 +287,105 @@ bool theory_seq::split_variable() {
return false;
}
bool theory_seq::check_length_coherence() {
if (!m_has_length) return true;
context& ctx = get_context();
bool coherent = true;
for (unsigned i = 0; i < m_eqs.size(); ++i) {
m_eqs[i].m_dep;
expr_ref v1(m), v2(m), l(m_eqs[i].m_lhs), r(m_eqs[i].m_rhs);
expr_ref len1(m_util.str.mk_length(l), m);
expr_ref len2(m_util.str.mk_length(r), m);
enode* n1 = ensure_enode(len1);
enode* n2 = ensure_enode(len2);
if (n1->get_root() != n2->get_root()) {
TRACE("seq", tout << len1 << " = " << len2 << "\n";);
propagate_eq(m_eqs[i].m_dep, n1, n2);
coherent = false;
}
}
return coherent;
}
bool theory_seq::check_length_coherence_tbd() {
if (!m_has_length) return true;
context& ctx = get_context();
bool coherent = true;
// each variable that canonizes to itself can have length 0.
unsigned sz = get_num_vars();
for (unsigned i = 0; i < sz; ++i) {
enode* n = get_enode(i);
expr* e = n->get_owner();
if (m_util.is_re(e)) {
continue;
}
SASSERT(m_util.is_seq(e));
// extend length of variables.
enode_pair_dependency* dep = 0;
expr* f = m_rep.find(e, dep);
if (is_var(f) && f == e) {
expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
TRACE("seq", tout << "Unsolved " << mk_pp(e, m) << "\n";);
#if 0
if (!assume_equality(e, emp)) {
// e = emp \/ e = head*tail & head = unit(v)
sort* char_sort = 0;
VERIFY(m_util.is_seq(m.get_sort(e), char_sort));
expr_ref tail(mk_skolem(symbol("seq.tail"), e), m);
expr_ref v(mk_skolem(symbol("seq.head.elem"), e, 0, 0, char_sort), m);
expr_ref head(m_util.str.mk_unit(v), m);
expr_ref conc(m_util.str.mk_concat(head, tail), m);
literal e_eq_emp(mk_eq(e, emp, false));
add_axiom(e_eq_emp, mk_eq(e, conc, false));
}
#endif
coherent = false;
}
}
return coherent;
}
bool theory_seq::check_ineq_coherence() {
bool all_false = true;
for (unsigned i = 0; all_false && i < m_ineqs.size(); ++i) {
expr* a = m_ineqs[i].get();
enode_pair_dependency* eqs = 0;
expr_ref b = canonize(a, eqs);
all_false = m.is_false(b);
if (all_false) {
TRACE("seq", tout << "equality is undetermined: " << mk_pp(a, m) << " " << b << "\n";);
}
}
return all_false;
}
/*
- Eqs = 0
- Diseqs evaluate to false
- lengths are coherent.
*/
bool theory_seq::is_solved() {
if (!m_eqs.empty()) {
return false;
}
if (!check_ineq_coherence()) {
return false;
}
SASSERT(check_length_coherence());
return true;
}
void theory_seq::propagate_lit(enode_pair_dependency* dep, literal lit) {
context& ctx = get_context();
ctx.mark_as_relevant(lit);
vector<enode_pair, false> _eqs;
m_dm.linearize(dep, _eqs);
TRACE("seq", ctx.display_detailed_literal(tout, lit);
tout << " <-\n"; display_deps(tout, dep););
tout << " <- "; display_deps(tout, dep););
justification* js =
ctx.mk_justification(
ext_theory_propagation_justification(
@ -312,7 +410,7 @@ void theory_seq::propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2)
vector<enode_pair, false> _eqs;
m_dm.linearize(dep, _eqs);
TRACE("seq",
tout << mk_pp(n1->get_owner(), m) << " " << mk_pp(n2->get_owner(), m) << " <- ";
tout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << " <- ";
display_deps(tout, dep);
);
@ -342,14 +440,19 @@ bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_dependency* deps) {
}
SASSERT(lhs.size() == rhs.size());
for (unsigned i = 0; i < lhs.size(); ++i) {
m.push_back(m_lhs.back(), lhs[i].get());
m.push_back(m_rhs.back(), rhs[i].get());
m_dam.push_back(m_deps.back(), deps);
expr_ref l(lhs[i].get(), m);
expr_ref r(rhs[i].get(), m);
if (m_util.is_seq(l) || m_util.is_re(l)) {
m_eqs.push_back(eq(l, r, deps));
}
else {
propagate_eq(deps, ensure_enode(l), ensure_enode(r));
}
}
TRACE("seq",
tout << mk_pp(l, m) << " = " << mk_pp(r, m) << " => ";
for (unsigned i = 0; i < lhs.size(); ++i) {
tout << mk_pp(lhs[i].get(), m) << " = " << mk_pp(rhs[i].get(), m) << "; ";
for (unsigned i = 0; i < m_eqs.size(); ++i) {
tout << m_eqs[i].m_lhs << " = " << m_eqs[i].m_rhs << "; ";
}
tout << "\n";
);
@ -436,23 +539,19 @@ bool theory_seq::solve_basic_eqs() {
bool theory_seq::pre_process_eqs(bool simplify_or_solve) {
context& ctx = get_context();
bool change = false;
expr_array& lhs = m_lhs.back();
expr_array& rhs = m_rhs.back();
enode_pair_dependency_array& deps = m_deps.back();
for (unsigned i = 0; !ctx.inconsistent() && i < m.size(lhs); ++i) {
for (unsigned i = 0; !ctx.inconsistent() && i < m_eqs.size(); ++i) {
eq e = m_eqs[i];
if (simplify_or_solve?
simplify_eq(m.get(lhs, i), m.get(rhs, i), m_dam.get(deps, i)):
solve_unit_eq(m.get(lhs, i), m.get(rhs, i), m_dam.get(deps, i))) {
if (i + 1 != m.size(lhs)) {
m.set(lhs, i, m.get(lhs, m.size(lhs)-1));
m.set(rhs, i, m.get(rhs, m.size(rhs)-1));
m_dam.set(deps, i, m_dam.get(deps, m_dam.size(deps)-1));
simplify_eq(e.m_lhs, e.m_rhs, e.m_dep):
solve_unit_eq(e.m_lhs, e.m_rhs, e.m_dep)) {
if (i + 1 != m_eqs.size()) {
eq e1 = m_eqs[m_eqs.size()-1];
m_eqs.set(i, e1);
--i;
++m_stats.m_num_reductions;
}
m.pop_back(lhs);
m.pop_back(rhs);
m_dam.pop_back(deps);
m_eqs.pop_back();
change = true;
}
}
@ -482,10 +581,7 @@ bool theory_seq::internalize_term(app* term) {
unsigned num_args = term->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
expr* arg = term->get_arg(i);
ctx.internalize(arg, false);
if (ctx.e_internalized(arg)) {
mk_var(ctx.get_enode(arg));
}
mk_var(ensure_enode(arg));
}
if (m.is_bool(term)) {
bool_var bv = ctx.mk_bool_var(term);
@ -501,6 +597,10 @@ bool theory_seq::internalize_term(app* term) {
}
mk_var(e);
}
if (m_util.str.is_length(term) && !m_has_length) {
m_trail_stack.push(value_trail<theory_seq, bool>(m_has_length));
m_has_length = true;
}
if (!m_util.str.is_concat(term) &&
!m_util.str.is_string(term) &&
!m_util.str.is_empty(term) &&
@ -511,11 +611,6 @@ bool theory_seq::internalize_term(app* term) {
!m_util.is_skolem(term)) {
set_incomplete(term);
}
expr* arg;
func_decl* fn;
if (m_util.str.is_length(term, arg) && !m_sort2len_fn.find(m.get_sort(arg), fn)) {
m_trail_stack.push(ast2ast_trail<theory_seq, sort, func_decl>(m_sort2len_fn, m.get_sort(arg), term->get_decl()));
}
return true;
}
@ -524,14 +619,14 @@ void theory_seq::apply_sort_cnstr(enode* n, sort* s) {
}
void theory_seq::display(std::ostream & out) const {
if (m.size(m_lhs.back()) == 0 &&
if (m_eqs.size() == 0 &&
m_ineqs.empty() &&
m_rep.empty() &&
m_exclude.empty()) {
return;
}
out << "Theory seq\n";
if (m.size(m_lhs.back()) > 0) {
if (m_eqs.size() > 0) {
out << "Equations:\n";
display_equations(out);
}
@ -552,22 +647,20 @@ void theory_seq::display(std::ostream & out) const {
}
void theory_seq::display_equations(std::ostream& out) const {
expr_array const& lhs = m_lhs.back();
expr_array const& rhs = m_rhs.back();
enode_pair_dependency_array const& deps = m_deps.back();
for (unsigned i = 0; i < m.size(lhs); ++i) {
out << mk_pp(m.get(lhs, i), m) << " = " << mk_pp(m.get(rhs, i), m) << " <-\n";
display_deps(out, m_dam.get(deps, i));
for (unsigned i = 0; i < m_eqs.size(); ++i) {
eq const& e = m_eqs[i];
out << e.m_lhs << " = " << e.m_rhs << " <- ";
display_deps(out, e.m_dep);
}
}
void theory_seq::display_deps(std::ostream& out, enode_pair_dependency* dep) const {
if (!dep) return;
vector<enode_pair, false> _eqs;
const_cast<enode_pair_dependency_manager&>(m_dm).linearize(dep, _eqs);
for (unsigned i = 0; i < _eqs.size(); ++i) {
out << " " << mk_pp(_eqs[i].first->get_owner(), m) << " = " << mk_pp(_eqs[i].second->get_owner(), m) << "\n";
out << " " << mk_pp(_eqs[i].first->get_owner(), m) << " = " << mk_pp(_eqs[i].second->get_owner(), m);
}
out << "\n";
}
void theory_seq::collect_statistics(::statistics & st) const {
@ -628,37 +721,53 @@ expr_ref theory_seq::canonize(expr* e, enode_pair_dependency*& eqs) {
expr_ref theory_seq::expand(expr* e, enode_pair_dependency*& eqs) {
enode_pair_dependency* deps = 0;
expr_dep ed;
expr* r = 0;
if (m_rep.find_cache(e, ed)) {
eqs = m_dm.mk_join(eqs, ed.second);
return expr_ref(ed.first, m);
}
e = m_rep.find(e, deps);
expr_ref result(m);
expr* e1, *e2;
eqs = m_dm.mk_join(eqs, deps);
if (m_util.str.is_concat(e, e1, e2)) {
return expr_ref(m_util.str.mk_concat(expand(e1, eqs), expand(e2, eqs)), m);
result = m_util.str.mk_concat(expand(e1, deps), expand(e2, deps));
}
if (m_util.str.is_empty(e) || m_util.str.is_string(e)) {
return expr_ref(e, m);
else if (m_util.str.is_empty(e) || m_util.str.is_string(e)) {
result = e;
}
if (m.is_eq(e, e1, e2)) {
return expr_ref(m.mk_eq(expand(e1, eqs), expand(e2, eqs)), m);
else if (m.is_eq(e, e1, e2)) {
result = m.mk_eq(expand(e1, deps), expand(e2, deps));
}
if (m_util.str.is_prefix(e, e1, e2)) {
return expr_ref(m_util.str.mk_prefix(expand(e1, eqs), expand(e2, eqs)), m);
else if (m_util.str.is_prefix(e, e1, e2)) {
result = m_util.str.mk_prefix(expand(e1, deps), expand(e2, deps));
}
if (m_util.str.is_suffix(e, e1, e2)) {
return expr_ref(m_util.str.mk_suffix(expand(e1, eqs), expand(e2, eqs)), m);
else if (m_util.str.is_suffix(e, e1, e2)) {
result = m_util.str.mk_suffix(expand(e1, deps), expand(e2, deps));
}
if (m_util.str.is_contains(e, e1, e2)) {
return expr_ref(m_util.str.mk_contains(expand(e1, eqs), expand(e2, eqs)), m);
else if (m_util.str.is_contains(e, e1, e2)) {
result = m_util.str.mk_contains(expand(e1, deps), expand(e2, deps));
}
if (m_model_completion && is_var(e)) {
else if (m_model_completion && is_var(e)) {
SASSERT(m_factory);
expr_ref val(m);
val = m_factory->get_fresh_value(m.get_sort(e));
val = m_factory->get_some_value(m.get_sort(e));
if (val) {
m_rep.update(e, val, 0);
return val;
result = val;
}
else {
result = e;
}
}
return expr_ref(e, m);
else {
result = e;
}
expr_dep edr(result, deps);
m_rep.add_cache(e, edr);
eqs = m_dm.mk_join(eqs, deps);
return result;
}
void theory_seq::add_dependency(enode_pair_dependency*& dep, enode* a, enode* b) {
@ -700,48 +809,18 @@ void theory_seq::deque_axiom(expr* n) {
else if (m_util.str.is_at(n)) {
add_at_axiom(n);
}
}
/*
\brief nodes n1 and n2 are about to get merged.
if n1 occurs in the context of a length application,
then instantiate length axioms for each concatenation in the class of n2.
In this way we ensure that length respects concatenation.
*/
void theory_seq::new_eq_len_concat(enode* n1, enode* n2) {
context& ctx = get_context();
if (n1->get_root() == n2->get_root()) {
return;
else if (m_util.str.is_unit(n)) {
add_length_unit_axiom(n);
}
SASSERT(n1->get_root() != n2->get_root());
if (!m_util.is_seq(n1->get_owner())) {
return;
else if (m_util.str.is_empty(n)) {
add_length_empty_axiom(n);
}
func_decl* f_len = 0;
if (!m_sort2len_fn.find(m.get_sort(n1->get_owner()), f_len)) {
return;
else if (m_util.str.is_concat(n)) {
add_length_concat_axiom(n);
}
enode* r1 = n1->get_root();
enode_vector::const_iterator it = ctx.begin_enodes_of(f_len);
enode_vector::const_iterator end = ctx.end_enodes_of(f_len);
bool has_len = false;
for (; !has_len && it != end; ++it) {
has_len = ((*it)->get_root() == r1);
else if (m_util.str.is_string(n)) {
add_length_string_axiom(n);
}
if (!has_len) {
return;
}
enode* start2 = n2;
do {
expr* o = n2->get_owner();
if (!is_var(o)) {
expr_ref ln(m_util.str.mk_length(o), m);
enque_axiom(ln);
}
n2 = n2->get_next();
}
while (n2 != start2);
}
@ -753,7 +832,7 @@ void theory_seq::new_eq_len_concat(enode* n1, enode* n2) {
lit or s = "" or len(c) = 1
lit or s = "" or !prefix(s, x*s1)
*/
void theory_seq::tightest_prefix(expr* s, expr* x, literal lit) {
void theory_seq::tightest_prefix(expr* s, expr* x, literal lit1, literal lit2) {
expr_ref s1 = mk_skolem(symbol("seq.first"), s);
expr_ref c = mk_skolem(symbol("seq.last"), s);
expr_ref s1c(m_util.str.mk_concat(s1, c), m);
@ -761,26 +840,32 @@ void theory_seq::tightest_prefix(expr* s, expr* x, literal lit) {
expr_ref one(m_autil.mk_int(1), m);
expr_ref emp(m_util.str.mk_empty(m.get_sort(s)), m);
literal s_eq_emp = mk_eq(s, emp, false);
add_axiom(lit, s_eq_emp, mk_eq(s, s1c, false));
add_axiom(lit, s_eq_emp, mk_eq(lc, one, false));
add_axiom(lit, s_eq_emp, ~mk_literal(m_util.str.mk_contains(s, m_util.str.mk_concat(x, s1))));
add_axiom(lit1, lit2, s_eq_emp, mk_eq(s, s1c, false));
add_axiom(lit1, lit2, s_eq_emp, mk_eq(lc, one, false));
add_axiom(lit1, lit2, s_eq_emp, ~mk_literal(m_util.str.mk_contains(s, m_util.str.mk_concat(x, s1))));
}
/*
// index of s in t starting at offset.
let i = Index(t, s, 0):
len(t) = 0 => i = -1
len(t) != 0 & !contains(t, s) => i = -1
len(t) != 0 & contains(t, s) => t = xsy & i = len(x)
len(t) != 0 & contains(t, s) & s != emp => tightest_prefix(x, s)
let i = Index(t, s, offset)
if offset = 0:
(!contains(t, s) -> i = -1)
(s = empty -> i = 0)
(contains(t, s) & s != empty -> t = xsy)
(contains(t, s) -> tightest_prefix(s, x))
if 0 <= offset < len(t):
t = zt' & len(z) == offset
add above constraints with t'
if offset >= len(t):
i = -1
if offset < 0:
?
0 <= offset < len(t) => xy = t & len(x) = offset & (-1 = indexof(t, s, 0) => -1 = i)
& (indexof(t, s, 0) >= 0 => indexof(t, s, 0) + offset = i)
offset = len(t) => i = -1
if offset < 0 or offset >= len(t)
under specified
optional lemmas:
(len(s) > len(t) -> i = -1)
@ -794,20 +879,45 @@ void theory_seq::add_indexof_axiom(expr* i) {
minus_one = m_autil.mk_int(-1);
zero = m_autil.mk_int(0);
emp = m_util.str.mk_empty(m.get_sort(s));
if (m_autil.is_numeral(offset, r) && r.is_zero()) {
literal offset_ne_zero = null_literal;
bool is_num = m_autil.is_numeral(offset, r);
if (is_num && r.is_zero()) {
offset_ne_zero = null_literal;
}
else {
offset_ne_zero = ~mk_eq(offset, zero, false);
}
if (!is_num || r.is_zero()) {
expr_ref x = mk_skolem(m_contains_left_sym, t, s);
expr_ref y = mk_skolem(m_contains_right_sym, t, s);
xsy = m_util.str.mk_concat(x,s,y);
literal cnt = mk_literal(m_util.str.mk_contains(t, s));
literal eq_empty = mk_eq(s, emp, false);
add_axiom(cnt, mk_eq(i, minus_one, false));
add_axiom(~eq_empty, mk_eq(i, zero, false));
add_axiom(~cnt, eq_empty, mk_eq(t, xsy, false));
tightest_prefix(s, x, ~cnt);
add_axiom(offset_ne_zero, cnt, mk_eq(i, minus_one, false));
add_axiom(offset_ne_zero, ~eq_empty, mk_eq(i, zero, false));
add_axiom(offset_ne_zero, ~cnt, eq_empty, mk_eq(t, xsy, false));
tightest_prefix(s, x, ~cnt, offset_ne_zero);
}
else {
// TBD
if (is_num && r.is_zero()) {
return;
}
// offset >= len(t) => indexof(s, t, offset) = -1
expr_ref len_t(m_util.str.mk_length(t), m);
literal offset_ge_len = mk_literal(m_autil.mk_ge(mk_sub(offset, len_t), zero));
add_axiom(offset_ge_len, mk_eq(i, minus_one, false));
// 0 <= offset & offset < len(t) => t = xy
// 0 <= offset & offset < len(t) => len(x) = offset
// 0 <= offset & offset < len(t) & ~contains(s, y) => indexof(t, s, offset) = -1
// 0 <= offset & offset < len(t) & contains(s, y) => index(t, s, offset) = indexof(y, s, 0) + len(t)
expr_ref x = mk_skolem(symbol("seq.indexof.left"), t, s, offset);
expr_ref y = mk_skolem(symbol("seq.indexof.right"), t, s, offset);
expr_ref indexof(m_util.str.mk_index(y, s, zero), m);
// TBD:
//literal offset_ge_0 = mk_literal(m_autil.mk_ge(offset, zero));
//add_axiom(~offset_ge_0, offset_ge_len, mk_eq(indexof, i, false));
//add_axiom(~offset_ge_0, offset_ge_len, mk_eq(m_util.str.mk_length(x), offset, false));
//add_axiom(~offset_ge_0, offset_ge_len, mk_eq(t, m_util.str.mk_concat(x, y), false));
}
/*
@ -832,39 +942,56 @@ void theory_seq::add_replace_axiom(expr* r) {
tightest_prefix(s, x, ~cnt);
}
void theory_seq::add_length_unit_axiom(expr* n) {
if (!m_has_length) return;
SASSERT(m_util.str.is_unit(n));
expr_ref one(m_autil.mk_int(1), m), len(m_util.str.mk_length(n), m);
add_axiom(mk_eq(len, one, false));
}
void theory_seq::add_length_empty_axiom(expr* n) {
if (!m_has_length) return;
SASSERT(m_util.str.is_empty(n));
expr_ref zero(m_autil.mk_int(0), m), len(m_util.str.mk_length(n), m);
add_axiom(mk_eq(len, zero, false));
}
void theory_seq::add_length_string_axiom(expr* n) {
if (!m_has_length) return;
zstring s;
VERIFY(m_util.str.is_string(n, s));
expr_ref len(m_util.str.mk_length(n), m);
expr_ref ls(m_autil.mk_numeral(rational(s.length(), rational::ui64()), true), m);
add_axiom(mk_eq(len, ls, false));
}
void theory_seq::add_length_concat_axiom(expr* n) {
if (!m_has_length) return;
expr* a, *b;
VERIFY(m_util.str.is_concat(n, a, b));
expr_ref len(m_util.str.mk_length(n), m);
expr_ref _a(m_util.str.mk_length(a), m);
expr_ref _b(m_util.str.mk_length(b), m);
expr_ref a_p_b(m_autil.mk_add(_a, _b), m);
add_axiom(mk_eq(len, a_p_b, false));
}
/*
let n = len(x)
len(x) >= 0
len(x) = 0 => x = ""
x = "" => len(x) = 0
len(x) = rewrite(len(x))
*/
void theory_seq::add_length_axiom(expr* n) {
expr* x, *a, *b;
expr* x;
VERIFY(m_util.str.is_length(n, x));
expr_ref zero(m), one(m), emp(m);
zero = m_autil.mk_int(0);
std::string s;
if (m_util.str.is_unit(n)) {
one = m_autil.mk_int(1);
add_axiom(mk_eq(n, one, false));
}
else if (m_util.str.is_empty(n)) {
add_axiom(mk_eq(n, zero, false));
}
else if (m_util.str.is_string(n, s)) {
expr_ref ls(m_autil.mk_numeral(rational(s.length(), rational::ui64()), true), m);
add_axiom(mk_eq(n, ls, false));
}
else if (m_util.str.is_concat(n, a, b)) {
expr_ref _a(m_util.str.mk_length(a), m);
expr_ref _b(m_util.str.mk_length(b), m);
expr_ref a_p_b(m_autil.mk_add(_a, _b), m);
add_axiom(mk_eq(n, a_p_b, false));
}
else {
emp = m_util.str.mk_empty(m.get_sort(x));
if (!m_util.str.is_unit(x) &&
!m_util.str.is_empty(x) &&
!m_util.str.is_string(x) &&
!m_util.str.is_concat(x)) {
expr_ref zero(m_autil.mk_int(0), m);
expr_ref emp(m_util.str.mk_empty(m.get_sort(x)), m);
literal eq1(mk_eq(zero, n, false));
literal eq2(mk_eq(x, emp, false));
add_axiom(mk_literal(m_autil.mk_ge(n, zero)));
@ -877,6 +1004,15 @@ expr* theory_seq::mk_sub(expr* a, expr* b) {
return m_autil.mk_add(a, m_autil.mk_mul(m_autil.mk_int(-1), b));
}
enode* theory_seq::ensure_enode(expr* e) {
context& ctx = get_context();
if (!ctx.e_internalized(e)) {
ctx.internalize(e, false);
ctx.mark_as_relevant(ctx.get_enode(e));
}
return ctx.get_enode(e);
}
/*
TBD: check semantics of extract.
@ -943,7 +1079,7 @@ void theory_seq::add_at_axiom(expr* e) {
literal theory_seq::mk_literal(expr* _e) {
expr_ref e(_e, m);
context& ctx = get_context();
ctx.internalize(e, false);
ensure_enode(e);
return ctx.get_literal(e);
}
@ -959,9 +1095,14 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4) {
}
expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2) {
expr* es[2] = { e1, e2 };
return expr_ref(m_util.mk_skolem(name, e2?2:1, es, m.get_sort(e1)), m);
expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1,
expr* e2, expr* e3, sort* range) {
expr* es[3] = { e1, e2, e3 };
unsigned len = e3?3:(e2?2:1);
if (!range) {
range = m.get_sort(e1);
}
return expr_ref(m_util.mk_skolem(name, len, es, range), m);
}
void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2) {
@ -970,10 +1111,9 @@ void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2) {
tout << mk_pp(ctx.bool_var2enode(v)->get_owner(), m) << " => "
<< mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";);
ctx.internalize(e1, false);
SASSERT(ctx.e_internalized(e2));
enode* n1 = ctx.get_enode(e1);
enode* n2 = ctx.get_enode(e2);
enode* n1 = ensure_enode(e1);
enode* n2 = ensure_enode(e2);
literal lit(v);
justification* js =
ctx.mk_justification(
@ -1009,10 +1149,6 @@ void theory_seq::assign_eq(bool_var v, bool is_true) {
else if (m_util.str.is_in_re(e, e1, e2)) {
// TBD
}
else if (m.is_eq(e, e1, e2)) {
new_eq_eh(ctx.get_enode(e1)->get_th_var(get_id()),
ctx.get_enode(e1)->get_th_var(get_id()));
}
else {
UNREACHABLE();
}
@ -1027,14 +1163,10 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) {
enode* n1 = get_enode(v1);
enode* n2 = get_enode(v2);
if (n1 != n2) {
expr* o1 = n1->get_owner(), *o2 = n2->get_owner();
TRACE("seq", tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << "\n";);
m.push_back(m_lhs.back(), o1);
m.push_back(m_rhs.back(), o2);
m_dam.push_back(m_deps.back(), m_dm.mk_leaf(enode_pair(n1, n2)));
new_eq_len_concat(n1, n2);
new_eq_len_concat(n2, n1);
expr_ref o1(n1->get_owner(), m);
expr_ref o2(n2->get_owner(), m);
TRACE("seq", tout << o1 << " = " << o2 << "\n";);
m_eqs.push_back(eq(o1, o2, m_dm.mk_leaf(enode_pair(n1, n2))));
}
}
@ -1047,53 +1179,27 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
}
void theory_seq::push_scope_eh() {
TRACE("seq", tout << "push " << m_lhs.size() << "\n";);
TRACE("seq", tout << "push " << m_eqs.size() << "\n";);
theory::push_scope_eh();
m_rep.push_scope();
m_exclude.push_scope();
m_dm.push_scope();
m_trail_stack.push_scope();
m_trail_stack.push(value_trail<theory_seq, unsigned>(m_axioms_head));
expr_array lhs, rhs;
enode_pair_dependency_array deps;
m.copy(m_lhs.back(), lhs);
m.copy(m_rhs.back(), rhs);
m_dam.copy(m_deps.back(), deps);
m_lhs.push_back(lhs);
m_rhs.push_back(rhs);
m_deps.push_back(deps);
m_eqs.push_scope();
}
void theory_seq::pop_scope_eh(unsigned num_scopes) {
TRACE("seq", tout << "pop " << m_lhs.size() << "\n";);
TRACE("seq", tout << "pop " << m_eqs.size() << "\n";);
m_trail_stack.pop_scope(num_scopes);
theory::pop_scope_eh(num_scopes);
m_dm.pop_scope(num_scopes);
m_rep.pop_scope(num_scopes);
m_exclude.pop_scope(num_scopes);
while (num_scopes > 0) {
--num_scopes;
m.del(m_lhs.back());
m.del(m_rhs.back());
m_dam.del(m_deps.back());
m_lhs.pop_back();
m_rhs.pop_back();
m_deps.pop_back();
}
m_eqs.pop_scopes(num_scopes);
}
void theory_seq::restart_eh() {
#if 0
m.del(m_lhs.back());
m.del(m_rhs.back());
m_dam.del(m_deps.back());
m_lhs.reset();
m_rhs.reset();
m_deps.reset();
m_lhs.push_back(expr_array());
m_rhs.push_back(expr_array());
m_deps.push_back(enode_pair_dependency_array());
#endif
}
void theory_seq::relevant_eh(app* n) {
@ -1101,7 +1207,11 @@ void theory_seq::relevant_eh(app* n) {
m_util.str.is_index(n) ||
m_util.str.is_replace(n) ||
m_util.str.is_extract(n) ||
m_util.str.is_at(n)) {
m_util.str.is_at(n) ||
m_util.str.is_concat(n) ||
m_util.str.is_empty(n) ||
m_util.str.is_unit(n) ||
m_util.str.is_string(n)) {
enque_axiom(n);
}
}

81
src/smt/theory_seq.h
View file

@ -23,37 +23,38 @@ Revision History:
#include "seq_decl_plugin.h"
#include "theory_seq_empty.h"
#include "th_rewriter.h"
#include "union_find.h"
#include "ast_trail.h"
#include "scoped_vector.h"
namespace smt {
class theory_seq : public theory {
struct config {
static const bool preserve_roots = true;
static const unsigned max_trail_sz = 16;
static const unsigned factor = 2;
typedef small_object_allocator allocator;
};
typedef scoped_dependency_manager<enode_pair> enode_pair_dependency_manager;
typedef enode_pair_dependency_manager::dependency enode_pair_dependency;
struct enode_pair_dependency_array_config : public config {
typedef enode_pair_dependency* value;
typedef dummy_value_manager<value> value_manager;
static const bool ref_count = false;
};
typedef parray_manager<enode_pair_dependency_array_config> enode_pair_dependency_array_manager;
typedef enode_pair_dependency_array_manager::ref enode_pair_dependency_array;
typedef union_find<theory_seq> th_union_find;
typedef trail_stack<theory_seq> th_trail_stack;
typedef std::pair<expr*, enode_pair_dependency*> expr_dep;
typedef obj_map<expr, expr_dep> eqdep_map_t;
// cache to track evaluations under equalities
class eval_cache {
eqdep_map_t m_map;
expr_ref_vector m_trail;
public:
eval_cache(ast_manager& m): m_trail(m) {}
bool find(expr* v, expr_dep& r) const { return m_map.find(v, r); }
void insert(expr* v, expr_dep& r) { m_trail.push_back(v); m_trail.push_back(r.first); m_map.insert(v, r); }
void reset() { m_map.reset(); m_trail.reset(); }
};
// map from variables to representatives
// + a cache for normalization.
class solution_map {
enum map_update { INS, DEL };
typedef obj_map<expr, std::pair<expr*, enode_pair_dependency*> > map_t;
ast_manager& m;
enode_pair_dependency_manager& m_dm;
map_t m_map;
eqdep_map_t m_map;
eval_cache m_cache;
expr_ref_vector m_lhs, m_rhs;
ptr_vector<enode_pair_dependency> m_deps;
svector<map_update> m_updates;
@ -61,15 +62,20 @@ namespace smt {
void add_trail(map_update op, expr* l, expr* r, enode_pair_dependency* d);
public:
solution_map(ast_manager& m, enode_pair_dependency_manager& dm): m(m), m_dm(dm), m_lhs(m), m_rhs(m) {}
solution_map(ast_manager& m, enode_pair_dependency_manager& dm):
m(m), m_cache(m), m_dm(dm), m_lhs(m), m_rhs(m) {}
bool empty() const { return m_map.empty(); }
void update(expr* e, expr* r, enode_pair_dependency* d);
void add_cache(expr* v, expr_dep& r) { m_cache.insert(v, r); }
bool find_cache(expr* v, expr_dep& r) { return m_cache.find(v, r); }
expr* find(expr* e, enode_pair_dependency*& d);
void cache(expr* e, expr* r, enode_pair_dependency* d);
void push_scope() { m_limit.push_back(m_updates.size()); }
void pop_scope(unsigned num_scopes);
void display(std::ostream& out) const;
};
// Table of current disequalities
class exclusion_table {
typedef obj_pair_hashtable<expr, expr> table_t;
ast_manager& m;
@ -81,14 +87,23 @@ namespace smt {
~exclusion_table() { }
bool empty() const { return m_table.empty(); }
void update(expr* e, expr* r);
bool contains(expr* e, expr* r) {
return m_table.contains(std::make_pair(e, r));
}
bool contains(expr* e, expr* r) const;
void push_scope() { m_limit.push_back(m_lhs.size()); }
void pop_scope(unsigned num_scopes);
void display(std::ostream& out) const;
};
// Asserted or derived equality with dependencies
struct eq {
expr_ref m_lhs;
expr_ref m_rhs;
enode_pair_dependency* m_dep;
eq(expr_ref& l, expr_ref& r, enode_pair_dependency* d):
m_lhs(l), m_rhs(r), m_dep(d) {}
eq(eq const& other): m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_dep(other.m_dep) {}
eq& operator=(eq const& other) { m_lhs = other.m_lhs; m_rhs = other.m_rhs; m_dep = other.m_dep; return *this; }
};
struct stats {
stats() { reset(); }
void reset() { memset(this, 0, sizeof(stats)); }
@ -96,15 +111,10 @@ namespace smt {
unsigned m_num_reductions;
};
ast_manager& m;
small_object_allocator m_alloc;
enode_pair_dependency_array_config::value_manager m_dep_array_value_manager;
enode_pair_dependency_manager m_dm;
enode_pair_dependency_array_manager m_dam;
solution_map m_rep; // unification representative.
vector<expr_array> m_lhs, m_rhs; // persistent sets of equalities.
vector<enode_pair_dependency_array> m_deps; // persistent sets of dependencies.
scoped_vector<eq> m_eqs; // set of current equations.
ast2ast_trailmap<sort, func_decl> m_sort2len_fn; // length functions per sort.
seq_factory* m_factory; // value factory
expr_ref_vector m_ineqs; // inequalities to check solution against
exclusion_table m_exclude; // set of asserted disequalities.
@ -112,6 +122,7 @@ namespace smt {
unsigned m_axioms_head; // index of first axiom to add.
unsigned m_branch_variable_head; // index of first equation to examine.
bool m_incomplete; // is the solver (clearly) incomplete for the fragment.
bool m_has_length; // is length applied
bool m_model_completion; // during model construction, invent values in canonizer
th_rewriter m_rewrite;
seq_util m_util;
@ -152,6 +163,10 @@ namespace smt {
bool simplify_and_solve_eqs(); // solve unitary equalities
bool branch_variable(); // branch on a variable
bool split_variable(); // split a variable
bool is_solved();
bool check_length_coherence();
bool check_length_coherence_tbd();
bool check_ineq_coherence();
bool pre_process_eqs(bool simplify_or_solve);
bool simplify_eqs();
@ -187,15 +202,17 @@ namespace smt {
void add_replace_axiom(expr* e);
void add_extract_axiom(expr* e);
void add_length_axiom(expr* n);
void add_length_unit_axiom(expr* n);
void add_length_empty_axiom(expr* n);
void add_length_concat_axiom(expr* n);
void add_length_string_axiom(expr* n);
void add_at_axiom(expr* n);
literal mk_literal(expr* n);
void tightest_prefix(expr* s, expr* x, literal lit);
void tightest_prefix(expr* s, expr* x, literal lit, literal lit2 = null_literal);
expr* mk_sub(expr* a, expr* b);
enode* ensure_enode(expr* a);
void new_eq_len_concat(enode* n1, enode* n2);
expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0);
expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0, expr* e3 = 0, sort* range = 0);
void set_incomplete(app* term);

15
src/smt/theory_seq_empty.h
View file

@ -64,15 +64,20 @@ namespace smt {
}
virtual expr* get_some_value(sort* s) {
if (u.is_string(s))
return u.str.mk_string(symbol(""));
NOT_IMPLEMENTED_YET();
if (u.is_seq(s)) {
return u.str.mk_empty(s);
}
sort* seq = 0;
if (u.is_re(s, seq)) {
return u.re.mk_to_re(u.str.mk_empty(seq));
}
UNREACHABLE();
return 0;
}
virtual bool get_some_values(sort* s, expr_ref& v1, expr_ref& v2) {
if (u.is_string(s)) {
v1 = u.str.mk_string("a");
v2 = u.str.mk_string("b");
v1 = u.str.mk_string(symbol("a"));
v2 = u.str.mk_string(symbol("b"));
return true;
}
NOT_IMPLEMENTED_YET();

2
src/tactic/aig/aig.cpp
View file

@ -131,7 +131,7 @@ struct aig_manager::imp {
if (memory::get_allocation_size() > m_max_memory)
throw aig_exception(TACTIC_MAX_MEMORY_MSG);
if (m().canceled())
throw aig_exception(TACTIC_CANCELED_MSG);
throw aig_exception(m().limit().get_cancel_msg());
cooperate("aig");
}

2
src/tactic/arith/arith_bounds_tactic.cpp
View file

@ -37,7 +37,7 @@ struct arith_bounds_tactic : public tactic {
void checkpoint() {
if (m.canceled()) {
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m.limit().get_cancel_msg());
}
}

2
src/tactic/arith/degree_shift_tactic.cpp
View file

@ -100,7 +100,7 @@ class degree_shift_tactic : public tactic {
void checkpoint() {
if (m.canceled())
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m.limit().get_cancel_msg());
cooperate("degree_shift");
}

2
src/tactic/arith/diff_neq_tactic.cpp
View file

@ -289,7 +289,7 @@ class diff_neq_tactic : public tactic {
unsigned nvars = num_vars();
while (m_stack.size() < nvars) {
if (m.canceled())
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m.limit().get_cancel_msg());
TRACE("diff_neq_tactic", display_model(tout););
var x = m_stack.size();
if (extend_model(x))

4
src/tactic/arith/fm_tactic.cpp
View file

@ -197,7 +197,7 @@ class fm_tactic : public tactic {
clauses::iterator it = m_clauses[i].begin();
clauses::iterator end = m_clauses[i].end();
for (; it != end; ++it) {
if (m.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG);
if (m.canceled()) throw tactic_exception(m.limit().get_cancel_msg());
switch (process(x, *it, u, ev, val)) {
case NONE:
TRACE("fm_mc", tout << "no bound for:\n" << mk_ismt2_pp(*it, m) << "\n";);
@ -1543,7 +1543,7 @@ class fm_tactic : public tactic {
void checkpoint() {
cooperate("fm");
if (m.canceled())
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m.limit().get_cancel_msg());
if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
}

2
src/tactic/bv/bv_size_reduction_tactic.cpp
View file

@ -176,7 +176,7 @@ struct bv_size_reduction_tactic::imp {
void checkpoint() {
if (m.canceled())
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m.limit().get_cancel_msg());
}
void operator()(goal & g, model_converter_ref & mc) {

2
src/tactic/bv/bvarray2uf_tactic.cpp
View file

@ -50,7 +50,7 @@ class bvarray2uf_tactic : public tactic {
void checkpoint() {
if (m_manager.canceled())
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m_manager.limit().get_cancel_msg());
}
void operator()(goal_ref const & g,

2
src/tactic/core/cofactor_elim_term_ite.cpp
View file

@ -36,7 +36,7 @@ struct cofactor_elim_term_ite::imp {
if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
if (m.canceled())
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m.limit().get_cancel_msg());
}
// Collect atoms that contain term if-then-else

2
src/tactic/core/ctx_simplify_tactic.cpp
View file

@ -96,7 +96,7 @@ struct ctx_simplify_tactic::imp {
if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
if (m.canceled())
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m.limit().get_cancel_msg());
}
bool shared(expr * t) const {

2
src/tactic/core/reduce_args_tactic.cpp
View file

@ -94,7 +94,7 @@ struct reduce_args_tactic::imp {
void checkpoint() {
if (m_manager.canceled())
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m_manager.limit().get_cancel_msg());
cooperate("reduce-args");
}

4
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -77,8 +77,8 @@ class solve_eqs_tactic : public tactic {
void checkpoint() {
if (m().canceled())
throw tactic_exception(TACTIC_CANCELED_MSG);
cooperate("solve-eqs");
throw tactic_exception(m().limit().get_cancel_msg());
cooperate("solve-eqs");
}
// Check if the number of occurrences of t is below the specified threshold :solve-eqs-max-occs

2
src/tactic/sls/sls_engine.cpp
View file

@ -95,7 +95,7 @@ void sls_engine::collect_statistics(statistics& st) const {
void sls_engine::checkpoint() {
if (m_manager.canceled())
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m_manager.limit().get_cancel_msg());
cooperate("sls");
}

4
src/tactic/ufbv/quasi_macros_tactic.cpp
View file

@ -77,8 +77,8 @@ class quasi_macros_tactic : public tactic {
while (more) { // CMW: use repeat(...) ?
if (m().canceled())
throw tactic_exception(TACTIC_CANCELED_MSG);
throw tactic_exception(m().limit().get_cancel_msg());
new_forms.reset();
new_proofs.reset();
more = qm(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs);

129
src/util/scoped_vector.h Normal file
View file

@ -0,0 +1,129 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
scoped_vector.h
Abstract:
Vector that restores during backtracking.
Author:
Nikolaj Bjorner (nbjorner) 2015-12-13
Revision History:
--*/
#ifndef SCOPED_VECTOR_H_
#define SCOPED_VECTOR_H_
#include"vector.h"
template<typename T>
class scoped_vector {
unsigned m_size;
unsigned m_elems_start;
unsigned_vector m_sizes;
vector<T> m_elems;
unsigned_vector m_elems_lim;
unsigned_vector m_index;
unsigned_vector m_src, m_dst;
unsigned_vector m_src_lim;
public:
scoped_vector(): m_size(0), m_elems_start(0) {}
// m_index : External-Index -> Internal-Index
// m_index.size() = max(m_sizes)
// m_src[i] -> m_dst[i] // trail into m_index updates
// m_src_lim last index to be updated.
void push_scope() {
m_elems_start = m_elems.size();
m_sizes.push_back(m_size);
m_src_lim.push_back(m_src.size());
m_elems_lim.push_back(m_elems_start);
}
void pop_scopes(unsigned num_scopes) {
if (num_scopes == 0) return;
unsigned new_size = m_sizes.size() - num_scopes;
unsigned src_lim = m_src_lim[new_size];
for (unsigned i = m_src.size(); i > src_lim; ) {
--i;
m_index[m_src[i]] = m_dst[i];
}
m_src.shrink(src_lim);
m_dst.shrink(src_lim);
m_src_lim.shrink(new_size);
m_elems.shrink(m_elems_lim[new_size]);
m_elems_lim.resize(new_size);
m_elems_start = m_elems.size();
m_size = m_sizes[new_size];
m_sizes.shrink(new_size);
}
T const& operator[](unsigned idx) const {
SASSERT(idx < m_size);
return m_elems[m_index[idx]];
}
void set(unsigned idx, T const& t) {
SASSERT(idx < m_size);
unsigned n = m_index[idx];
if (n >= m_elems_start) {
m_elems[n] = t;
}
else {
set_index(idx, m_elems.size());
m_elems.push_back(t);
}
SASSERT(invariant());
}
void push_back(T const& t) {
set_index(m_size, m_elems.size());
m_elems.push_back(t);
++m_size;
SASSERT(invariant());
}
void pop_back() {
SASSERT(m_size > 0);
if (m_index[m_size-1] == m_elems.size()-1 &&
m_elems.size() > m_elems_start) {
m_elems.pop_back();
}
--m_size;
SASSERT(invariant());
}
unsigned size() const { return m_size; }
bool empty() const { return m_size == 0; }
private:
void set_index(unsigned src, unsigned dst) {
while (src >= m_index.size()) {
m_index.push_back(0);
}
SASSERT(src < m_index.size());
if (src < m_elems_start) {
m_src.push_back(src);
m_dst.push_back(m_index[src]);
}
m_index[src] = dst;
}
bool invariant() const {
return
m_size <= m_elems.size() &&
m_elems_start <= m_elems.size();
}
};
#endif