na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/smt/seq_axioms.cpp

@@ -63,7 +63,7 @@ literal seq_axioms::mk_literal(expr* _e) {
     return ctx().get_literal(e);
 }
 
-/*
+/***
 
   let e = extract(s, i, l)
 
@@ -608,6 +608,18 @@ void seq_axioms::add_stoi_axiom(expr* e, unsigned k) {
    |s| >= 2 => e >= 10
    |s| >= 3 => e >= 100
 
+   There are no constraints to ensure that the string itos(e) 
+   contains the valid digits corresponding to e >= 0.
+   The validity of itos(e) is ensured by the following property:
+   e is either of the form stoi(s) for some s, or there is a term
+   stoi(itos(e)) and axiom e >= 0 => stoi(itos(e)) = e.
+   Then the axioms for stoi(itos(e)) ensure that the characters of
+   itos(e) are valid digits and the axiom stoi(itos(e)) = e ensures 
+   these digits encode e.
+   The option of constraining itos(e) digits directly does not
+   seem appealing becaues it requires an order of quadratic number
+   of constraints for all possible lengths of itos(e) (e.g, log_10(e)).
+
 */
 
 void seq_axioms::add_itos_axiom(expr* s, unsigned k) {
@@ -638,6 +650,10 @@ literal seq_axioms::is_digit(expr* ch) {
     return isd;
 }
 
+/**
+   Bridge character digits to integers.
+*/
+
 void seq_axioms::ensure_digit_axiom() {
     if (!m_digits_initialized) {
         for (unsigned i = 0; i < 10; ++i) {
@@ -742,6 +758,32 @@ void seq_axioms::add_prefix_axiom(expr* e) {
     add_axiom(lit, e1_gt_e2, ~mk_eq(c, d));
 }
 
+/***
+    let n = len(x)
+    - len(a ++ b) = len(a) + len(b) if x = a ++ b
+    - len(unit(u)) = 1              if x = unit(u)
+    - len(str) = str.length()       if x = str
+    - len(empty) = 0                if x = empty
+    - len(int.to.str(i)) >= 1       if x = int.to.str(i) and more generally if i = 0 then 1 else 1+floor(log(|i|))
+    - len(x) >= 0                   otherwise
+ */
+void seq_axioms::add_length_axiom(expr* n) {
+    expr* x = nullptr;
+    VERIFY(seq.str.is_length(n, x));
+    if (seq.str.is_concat(x) ||
+        seq.str.is_unit(x) ||
+        seq.str.is_empty(x) ||
+        seq.str.is_string(x)) {
+        expr_ref len(n, m);
+        m_rewrite(len);
+        SASSERT(n != len);
+        add_axiom(mk_eq(len, n));
+    }
+    else {
+        add_axiom(mk_ge(n, 0));
+    }
+}
+
 
 expr_ref seq_axioms::add_length_limit(expr* s, unsigned k) {
     expr_ref bound_tracker  = m_sk.mk_length_limit(s, k);

src/smt/seq_axioms.h

@@ -89,6 +89,7 @@ namespace smt {
         void add_lt_axiom(expr* n);
         void add_le_axiom(expr* n);
         void add_unit_axiom(expr* n);
+        void add_length_axiom(expr* n);
         literal is_digit(expr* ch);
 
         expr_ref add_length_limit(expr* s, unsigned k);

src/smt/theory_seq.cpp

@@ -3054,7 +3054,10 @@ void theory_seq::enque_axiom(expr* e) {
 void theory_seq::deque_axiom(expr* n) {
     TRACE("seq", tout << "deque: " << mk_bounded_pp(n, m, 2) << "\n";);
     if (m_util.str.is_length(n)) {
-        add_length_axiom(n);
+        m_ax.add_length_axiom(n);
+        if (!get_context().at_base_level()) {
+            m_trail_stack.push(push_replay(alloc(replay_axiom, m, n)));
+        }
     }
     else if (m_util.str.is_empty(n) && !has_length(n) && !m_has_length.empty()) {
         add_length_to_eqc(n);
@@ -3116,38 +3119,6 @@ expr_ref theory_seq::add_elim_string_axiom(expr* n) {
     return result;
 }
 
-
-/*
-    let n = len(x)
-    - len(a ++ b) = len(a) + len(b) if x = a ++ b
-    - len(unit(u)) = 1              if x = unit(u)
-    - len(str) = str.length()       if x = str
-    - len(empty) = 0                if x = empty
-    - len(int.to.str(i)) >= 1       if x = int.to.str(i) and more generally if i = 0 then 1 else 1+floor(log(|i|))
-    - len(x) >= 0                   otherwise
- */
-void theory_seq::add_length_axiom(expr* n) {
-    context& ctx = get_context();
-    expr* x = nullptr;
-    VERIFY(m_util.str.is_length(n, x));
-    if (m_util.str.is_concat(x) ||
-        m_util.str.is_unit(x) ||
-        m_util.str.is_empty(x) ||
-        m_util.str.is_string(x)) {
-        expr_ref len(n, m);
-        m_rewrite(len);
-        SASSERT(n != len);
-        add_axiom(mk_eq(len, n, false));
-    }
-    else {
-        add_axiom(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0))));
-    }
-    if (!ctx.at_base_level()) {
-        m_trail_stack.push(push_replay(alloc(replay_axiom, m, n)));
-    }
-}
-
-
 void theory_seq::propagate_in_re(expr* n, bool is_true) {
     TRACE("seq", tout << mk_pp(n, m) << " <- " << (is_true?"true":"false") << "\n";);
 

src/smt/theory_seq.h

@@ -604,7 +604,6 @@ namespace smt {
         void enque_axiom(expr* e);
         void deque_axiom(expr* e);
         void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal, literal l5 = null_literal);        
-        void add_length_axiom(expr* n);
         
         bool has_length(expr *e) const { return m_has_length.contains(e); }
         void add_length(expr* e, expr* l);