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

scripts/mk_util.py

@@ -2199,7 +2199,7 @@ def mk_config():
                     'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
                     'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
             elif VS_ARM:
-                print "ARM on VS is unsupported"
+                print("ARM on VS is unsupported")
                 exit(1)
             else:
                 config.write(
@@ -2225,7 +2225,7 @@ def mk_config():
                     'LINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n'
                     'SLINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n' % (LTCG, LTCG))
             elif VS_ARM:
-                print "ARM on VS is unsupported"
+                print("ARM on VS is unsupported")
                 exit(1)
             else:
                 config.write(

src/ast/rewriter/seq_rewriter.cpp

@@ -25,6 +25,8 @@ Notes:
 #include"automaton.h"
 #include"well_sorted.h"
 #include"var_subst.h"
+#include"symbolic_automata_def.h"
+
 
 expr_ref sym_expr::accept(expr* e) {
     ast_manager& m = m_t.get_manager();
@@ -37,6 +39,7 @@ expr_ref sym_expr::accept(expr* e) {
     }
     case t_char:
         SASSERT(m.get_sort(e) == m.get_sort(m_t));
+        SASSERT(m.get_sort(e) == m_sort);
         result = m.mk_eq(e, m_t);
         break;
     case t_range: {
@@ -67,8 +70,114 @@ struct display_expr1 {
     }
 };
 
+class sym_expr_boolean_algebra : public boolean_algebra<sym_expr*> {
+    ast_manager& m;
+    expr_solver& m_solver;
+    typedef sym_expr* T;
+public:
+    sym_expr_boolean_algebra(ast_manager& m, expr_solver& s): 
+        m(m), m_solver(s) {}
+
+    virtual T mk_false() {
+        expr_ref fml(m.mk_false(), m);
+        return sym_expr::mk_pred(fml, m.mk_bool_sort()); // use of Bool sort for bound variable is arbitrary
+    }
+    virtual T mk_true() {
+        expr_ref fml(m.mk_true(), m);
+        return sym_expr::mk_pred(fml, m.mk_bool_sort());
+    }
+    virtual T mk_and(T x, T y) {
+        if (x->is_char() && y->is_char()) {
+            if (x->get_char() == y->get_char()) {
+                return x;
+            }
+            if (m.are_distinct(x->get_char(), y->get_char())) {
+                expr_ref fml(m.mk_false(), m);
+                return sym_expr::mk_pred(fml, x->get_sort());
+            }
+        }
+        var_ref v(m.mk_var(0, x->get_sort()), m);
+        expr_ref fml1 = x->accept(v);
+        expr_ref fml2 = y->accept(v);
+        if (m.is_true(fml1)) return y;
+        if (m.is_true(fml2)) return x;
+        expr_ref fml(m.mk_and(fml1, fml2), m);
+        return sym_expr::mk_pred(fml, x->get_sort());
+    }
+    virtual T mk_or(T x, T y) {
+        if (x->is_char() && y->is_char() &&
+            x->get_char() == y->get_char()) {
+            return x;
+        }
+        var_ref v(m.mk_var(0, x->get_sort()), m);
+        expr_ref fml1 = x->accept(v);
+        expr_ref fml2 = y->accept(v);        
+        if (m.is_false(fml1)) return y;
+        if (m.is_false(fml2)) return x;
+        expr_ref fml(m.mk_or(fml1, fml2), m);
+        return sym_expr::mk_pred(fml, x->get_sort());
+    }
+
+    virtual T mk_and(unsigned sz, T const* ts) {
+        switch (sz) {
+        case 0: return mk_true();
+        case 1: return ts[0];
+        default: {
+            T t = ts[0];
+            for (unsigned i = 1; i < sz; ++i) {
+                t = mk_and(t, ts[i]);
+            }
+            return t;
+        }
+        }
+    }
+    virtual T mk_or(unsigned sz, T const* ts) {
+        switch (sz) {
+        case 0: return mk_false();
+        case 1: return ts[0];
+        default: {
+            T t = ts[0];
+            for (unsigned i = 1; i < sz; ++i) {
+                t = mk_or(t, ts[i]);
+            }
+            return t;
+        }
+        }
+    }
+    virtual lbool is_sat(T x) {
+        if (x->is_char()) {
+            return l_true;
+        }
+        if (x->is_range()) {
+            // TBD check lower is below upper.
+        }
+        expr_ref v(m.mk_fresh_const("x", x->get_sort()), m);
+        expr_ref fml = x->accept(v);
+        if (m.is_true(fml)) {
+            return l_true;
+        }
+        if (m.is_false(fml)) {
+            return l_false;
+        }
+        return m_solver.check_sat(fml);
+    }
+    virtual T mk_not(T x) {
+        var_ref v(m.mk_var(0, x->get_sort()), m);
+        expr_ref fml(m.mk_not(x->accept(v)), m);
+        return sym_expr::mk_pred(fml, x->get_sort());
+    }
+};
+
+re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m), m_ba(0), m_sa(0) {}
+
+re2automaton::~re2automaton() {}
+
+void re2automaton::set_solver(expr_solver* solver) {
+    m_solver = solver;
+    m_ba = alloc(sym_expr_boolean_algebra, m, *solver);
+    m_sa = alloc(symbolic_automata_t, sm, *m_ba.get());
+}
 
-re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m) {}
 
 eautomaton* re2automaton::operator()(expr* e) { 
     eautomaton* r = re2aut(e); 
@@ -136,7 +245,7 @@ eautomaton* re2automaton::re2aut(expr* e) {
             expr_ref _start(bv.mk_numeral(start, nb), m);
             expr_ref _stop(bv.mk_numeral(stop, nb), m);
             expr_ref _pred(m.mk_not(m.mk_and(bv.mk_ule(_start, v), bv.mk_ule(v, _stop))), m);
-            a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred));
+            a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred, s));
             return a.detach();
         }
         else if (u.re.is_to_re(e0, e1) && u.str.is_string(e1, s1) && s1.length() == 1) {
@@ -145,13 +254,14 @@ eautomaton* re2automaton::re2aut(expr* e) {
             expr_ref v(m.mk_var(0, s), m);
             expr_ref _ch(bv.mk_numeral(s1[0], nb), m);          
             expr_ref _pred(m.mk_not(m.mk_eq(v, _ch)), m);
-            a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred));
+            a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred, s));
             return a.detach();
         }
         else if (u.re.is_to_re(e0, e1) && u.str.is_unit(e1, e2)) {
-            expr_ref v(m.mk_var(0, m.get_sort(e2)), m);
+            sort* s = m.get_sort(e2);
+            expr_ref v(m.mk_var(0, s), m);
             expr_ref _pred(m.mk_not(m.mk_eq(v, e2)), m);
-            a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred));
+            a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred, s));
             return a.detach();
         }
         else {
@@ -187,14 +297,15 @@ eautomaton* re2automaton::re2aut(expr* e) {
     }
     else if (u.re.is_full(e)) {
         expr_ref tt(m.mk_true(), m);
-        sym_expr* _true = sym_expr::mk_pred(tt);
+        sort* seq_s, *char_s;
+        VERIFY (u.is_re(m.get_sort(e), seq_s));
+        VERIFY (u.is_seq(seq_s, char_s));
+        sym_expr* _true = sym_expr::mk_pred(tt, char_s);
         return eautomaton::mk_loop(sm, _true);
     }
-#if 0
+    else if (u.re.is_intersection(e, e1, e2) && m_sa && (a = re2aut(e1)) && (b = re2aut(e2))) {
-    else if (u.re.is_intersect(e, e1, e2)) {
+        return m_sa->mk_product(*a, *b);
-        // maybe later
     }
-#endif
     
     return 0;
 }

src/ast/rewriter/seq_rewriter.h

@@ -25,6 +25,7 @@ Notes:
 #include"params.h"
 #include"lbool.h"
 #include"automaton.h"
+#include"symbolic_automata.h"
 
 class sym_expr {
     enum ty {
@@ -33,21 +34,24 @@ class sym_expr {
         t_range
     };
     ty       m_ty;
+    sort*    m_sort;
     expr_ref m_t;
     expr_ref m_s;
     unsigned m_ref;
-    sym_expr(ty ty, expr_ref& t, expr_ref& s) : m_ty(ty), m_t(t), m_s(s), m_ref(0) {}
+    sym_expr(ty ty, expr_ref& t, expr_ref& s, sort* srt) : m_ty(ty), m_sort(srt), m_t(t), m_s(s), m_ref(0) {}
 public:
     expr_ref accept(expr* e);
-    static sym_expr* mk_char(expr_ref& t) { return alloc(sym_expr, t_char, t, t); }
+    static sym_expr* mk_char(expr_ref& t) { return alloc(sym_expr, t_char, t, t, t.get_manager().get_sort(t)); }
     static sym_expr* mk_char(ast_manager& m, expr* t) { expr_ref tr(t, m); return mk_char(tr); }
-    static sym_expr* mk_pred(expr_ref& t) { return alloc(sym_expr, t_pred, t, t); }
+    static sym_expr* mk_pred(expr_ref& t, sort* s) { return alloc(sym_expr, t_pred, t, t, s); }
-    static sym_expr* mk_range(expr_ref& lo, expr_ref& hi) { return alloc(sym_expr, t_range, lo, hi); }
+    static sym_expr* mk_range(expr_ref& lo, expr_ref& hi) { return alloc(sym_expr, t_range, lo, hi, lo.get_manager().get_sort(hi)); }
     void inc_ref() { ++m_ref;  }
     void dec_ref() { --m_ref; if (m_ref == 0) dealloc(this); }
     std::ostream& display(std::ostream& out) const;
     bool is_char() const { return m_ty == t_char; }
     bool is_pred() const { return !is_char(); }
+    bool is_range() const { return m_ty == t_range; }
+    sort* get_sort() const { return m_sort; }
     expr* get_char() const { SASSERT(is_char()); return m_t; }
 
 };
@@ -58,17 +62,31 @@ public:
     void dec_ref(sym_expr* s) { if (s) s->dec_ref(); }
 };
 
+class expr_solver {
+public:
+    virtual ~expr_solver() {}
+    virtual lbool check_sat(expr* e) = 0;
+};
+
 typedef automaton<sym_expr, sym_expr_manager> eautomaton;
 class re2automaton {
+    typedef boolean_algebra<sym_expr*> boolean_algebra_t;
+    typedef symbolic_automata<sym_expr, sym_expr_manager> symbolic_automata_t;
     ast_manager& m;
     sym_expr_manager sm;
     seq_util     u;     
     bv_util      bv;
+    scoped_ptr<expr_solver>         m_solver;
+    scoped_ptr<boolean_algebra_t>   m_ba;
+    scoped_ptr<symbolic_automata_t> m_sa;
+
     eautomaton* re2aut(expr* e);
     eautomaton* seq2aut(expr* e);
- public:
+public:
     re2automaton(ast_manager& m);
+    ~re2automaton();
     eautomaton* operator()(expr* e);
+    void set_solver(expr_solver* solver);
 };
 
 /**

src/math/automata/automaton.h

@@ -178,15 +178,19 @@ public:
         return alloc(automaton, a.m, a.init(), final, mvs);
     }
 
+    automaton* clone() const {
+        return clone(*this);
+    }
+
     // create the sum of disjoint automata
     static automaton* mk_union(automaton const& a, automaton const& b) {
         SASSERT(&a.m == &b.m);
         M& m = a.m;
         if (a.is_empty()) {
-            return clone(b);
+            return b.clone();
         }
         if (b.is_empty()) {
-            return clone(a);
+            return a.clone();
         }
         moves mvs;
         unsigned_vector final;
@@ -213,7 +217,7 @@ public:
             mvs.push_back(move(m, 0, a.init() + offset));
         }
         if (a.is_empty()) {
-            return clone(a);
+            return a.clone();
         }
 
         mvs.push_back(move(m, init, a.final_state() + offset));
@@ -227,16 +231,16 @@ public:
         SASSERT(&a.m == &b.m);
         M& m = a.m;
         if (a.is_empty()) {
-            return clone(a);
+            return a.clone();
         }
         if (b.is_empty()) {
-            return clone(b);
+            return b.clone();
         }
         if (a.is_epsilon()) {
-            return clone(b);
+            return b.clone();
         }
         if (b.is_epsilon()) {
-            return clone(a);
+            return a.clone();
         }
 
         moves mvs;
@@ -458,6 +462,7 @@ public:
     }
 
     unsigned init() const { return m_init; }
+    unsigned_vector const& final_states() const { return m_final_states; }
     unsigned in_degree(unsigned state) const { return m_delta_inv[state].size(); }
     unsigned out_degree(unsigned state) const { return m_delta[state].size(); }
     move const& get_move_from(unsigned state) const { SASSERT(m_delta[state].size() == 1); return m_delta[state][0]; }

src/math/automata/boolean_algebra.h

@@ -0,0 +1,46 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    boolean_algebra.h
+
+Abstract:
+
+    Boolean Algebra, a la Margus Veanes Automata library.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2016-2-27
+
+Revision History:
+
+
+--*/
+
+#ifndef BOOLEAN_ALGEBRA_H_
+#define BOOLEAN_ALGEBRA_H_
+
+#include "util.h"
+
+template<class T>
+class positive_boolean_algebra {
+public:
+    virtual T mk_false() = 0;
+    virtual T mk_true() = 0;
+    virtual T mk_and(T x, T y) = 0;
+    virtual T mk_or(T x, T y) = 0;
+    virtual T mk_and(unsigned sz, T const* ts) = 0;
+    virtual T mk_or(unsigned sz, T const* ts) = 0;
+    virtual lbool is_sat(T x) = 0;
+};
+
+template<class T>
+class boolean_algebra : public positive_boolean_algebra<T> {
+public:
+    virtual T mk_not(T x) = 0;
+    //virtual lbool are_equivalent(T x, T y) = 0;
+    //virtual T simplify(T x) = 0;    
+};
+
+#endif

src/math/automata/symbolic_automata.h

@@ -0,0 +1,104 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    symbolic_automata.h
+
+Abstract:
+
+    Symbolic Automata over Boolean Algebras, a la Margus Veanes Automata library.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2016-02-27.
+
+Revision History:
+
+
+--*/
+
+#ifndef SYMBOLIC_AUTOMATA_H_
+#define SYMBOLIC_AUTOMATA_H_
+
+
+#include "automaton.h"
+#include "boolean_algebra.h"
+
+
+template<class T, class M = default_value_manager<T> >
+class symbolic_automata {
+    typedef automaton<T, M>    automaton_t;
+    typedef boolean_algebra<T*> ba_t;
+    typedef typename automaton_t::move  move_t;
+    typedef vector<move_t>     moves_t;
+    typedef obj_ref<T, M>      ref_t;
+    typedef ref_vector<T, M>   refs_t;
+
+    M&    m;
+    ba_t& m_ba;
+
+
+    class block {
+        uint_set m_set;
+        unsigned m_rep;
+        bool     m_rep_chosen;
+    public:
+
+        block(): m_rep(0), m_rep_chosen(false) {}
+
+        block(uint_set const& s):
+            m_set(s),
+            m_rep(0),
+            m_rep_chosen(false) {
+        }
+
+        block(unsigned_vector const& vs) {
+            for (unsigned i = 0; i < vs.size(); ++i) {
+                m_set.insert(vs[i]);               
+            }
+            m_rep_chosen = false;
+            m_rep = 0;
+        }
+
+        block& operator=(block const& b) {
+            m_set = b.m_set;
+            m_rep = 0;
+            m_rep_chosen = false;
+            return *this;
+        }
+
+        unsigned get_representative() {
+            if (!m_rep_chosen) {
+                uint_set::iterator it = m_set.begin();
+                if (m_set.end() != it) {
+                    m_rep = *it;                    
+                }
+                m_rep_chosen = true;
+            }
+            return m_rep;
+        }
+
+        void add(unsigned i) { m_set.insert(i); }
+        bool contains(unsigned i) const { return m_set.contains(i); }        
+        bool is_empty() const { return m_set.empty(); }
+        unsigned size() const { return m_set.num_elems(); }
+        void remove(unsigned i) { m_set.remove(i); m_rep_chosen = false; }        
+        void clear() { m_set.reset(); m_rep_chosen = false; }
+        uint_set::iterator begin() { return m_set.begin(); }
+        uint_set::iterator end() { return m_set.end(); }
+    };
+
+public:
+    symbolic_automata(M& m, ba_t& ba): m(m), m_ba(ba) {}
+    automaton_t* mk_determinstic(automaton_t& a);
+    automaton_t* mk_complement(automaton_t& a);
+    automaton_t* remove_epsilons(automaton_t& a);
+    automaton_t* mk_total(automaton_t& a);
+    automaton_t* mk_minimize(automaton_t& a);
+    automaton_t* mk_product(automaton_t& a, automaton_t& b);
+};
+
+
+
+#endif 

src/math/automata/symbolic_automata_def.h

@@ -0,0 +1,228 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    symbolic_automata_def.h
+
+Abstract:
+
+    Symbolic Automata over Boolean Algebras, a la Margus Veanes Automata library.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2016-02-27.
+
+Revision History:
+
+
+--*/
+
+#ifndef SYMBOLIC_AUTOMATA_DEF_H_
+#define SYMBOLIC_AUTOMATA_DEF_H_
+
+
+#include "symbolic_automata.h"
+#include "hashtable.h"
+
+typedef std::pair<unsigned, unsigned> unsigned_pair;
+
+
+
+template<class T, class M>
+typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_total(automaton_t& a) {
+    unsigned dead_state = a.num_states();
+    moves_t mvs, new_mvs;
+    for (unsigned i = 0; i < dead_state; ++i) {
+        mvs.reset();
+        a.get_moves(i, mvs, true);
+        refs_t vs(m);
+        
+        for (unsigned j = 0; j < mvs.size(); ++j) {
+            vs.push_back(mvs[j].t());
+        }
+        ref_t cond(m_ba.mk_not(m_ba.mk_or(vs.size(), vs.c_ptr())), m);
+        lbool is_sat = m_ba.is_sat(cond);
+        if (is_sat == l_undef) {
+            return 0;
+        }
+        if (is_sat == l_true) {
+            new_mvs.push_back(move_t(m, i, dead_state, cond));
+        }
+    }
+    if (new_mvs.empty()) {
+        return a.clone();
+    }
+    new_mvs.push_back(move_t(m, dead_state, dead_state, m_ba.mk_true()));
+    automaton_t::append_moves(0, a, new_mvs);
+    
+    return alloc(automaton_t, m, a.init(), a.final_states(), new_mvs);        
+}
+
+template<class T, class M>
+typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minimize(automaton_t& a) {
+    if (a.is_empty()) {
+        return a.clone();
+    }
+
+    if (a.is_epsilon()) {
+        return a.clone();
+    }
+    // SASSERT(a.is_deterministic());
+    
+    scoped_ptr<automaton_t> fa = mk_total(a);
+    if (!fa) {
+        return 0;
+    }
+    
+    block final_block(fa->final_states());
+    block non_final_block(fa->non_final_states());
+    vector<block> blocks;
+    for (unsigned i = 0; i < fa->num_states(); ++i) {
+        if (fa->is_final_state(i)) {
+            blocks.push_back(final_block);
+        }
+        else {
+            blocks.push_back(non_final_block);
+        }
+    }
+    vector<block> W;
+    if (final_block.size() > non_final_block.size()) {
+        W.push_back(non_final_block);
+    }
+    else {
+        W.push_back(final_block);
+    }
+    
+#if 0
+    
+    refs_t trail(m);
+    u_map<T*> gamma;
+    moves_t mvs;
+    while (!W.empty()) {
+        block R(W.back());
+        W.pop_back();
+        block Rcopy(R);
+        gamma.reset();
+        uint_set::iterator it = Rcopy.begin(), end = Rcopy.end();
+        for (; it != end; ++it) {
+            unsigned q = *it;
+            mvs.reset();
+            fa->get_moves_to(q, mvs);
+            for (unsigned i = 0; i < mvs.size(); ++i) {
+                unsigned src = mvs[i].src();
+                if (blocks[src].size() > 1) {
+                    T* t = mvs[i]();
+                    if (gamma.find(src, t1)) {
+                        t = m_ba.mk_or(t, t1);
+                        trail.push_back(t);
+                    }
+                    gamma.insert(src, t);
+                }
+            }
+        }
+        hashtable<block*> relevant;
+        u_map<T*>::iterator end = gamma.end();
+        for (u_map<T*>::iterator it = gamma.begin(); it != end; ++it) {
+            relevant.insert(blocks[it->m_key]);
+        }
+        
+    }
+#endif
+    
+    return 0;
+        
+}
+
+template<class T, class M>
+typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_product(automaton_t& a, automaton_t& b) {
+    map<unsigned_pair, unsigned, pair_hash<unsigned_hash, unsigned_hash>, default_eq<unsigned_pair> > state_ids;
+    unsigned_pair init_pair(a.init(), b.init());
+    svector<unsigned_pair> todo;
+    todo.push_back(init_pair);
+    state_ids.insert(init_pair, 0);
+    moves_t mvs;
+    unsigned_vector final;
+    if (a.is_final_state(a.init()) && b.is_final_state(b.init())) {
+        final.push_back(0);
+    }
+    unsigned n = 1;
+    moves_t mvsA, mvsB;
+    while (!todo.empty()) {
+        unsigned_pair curr_pair = todo.back();
+        todo.pop_back();
+        unsigned src = state_ids[curr_pair];
+        mvsA.reset(); mvsB.reset();
+        a.get_moves_from(curr_pair.first,  mvsA, true);
+        b.get_moves_from(curr_pair.second, mvsB, true);
+        for (unsigned i = 0; i < mvsA.size(); ++i) {
+            for (unsigned j = 0; j < mvsB.size(); ++j) {
+                ref_t ab(m_ba.mk_and(mvsA[i].t(), mvsB[j].t()), m);   
+                lbool is_sat = m_ba.is_sat(ab);
+                if (is_sat == l_false) {
+                    continue;
+                }
+                else if (is_sat == l_undef) {
+                    return 0;
+                }
+                unsigned_pair tgt_pair(mvsA[i].dst(), mvsB[j].dst());
+                unsigned tgt;
+                if (!state_ids.find(tgt_pair, tgt)) {
+                    tgt = n++;
+                    state_ids.insert(tgt_pair, tgt);
+                    todo.push_back(tgt_pair);
+                    if (a.is_final_state(tgt_pair.first) && b.is_final_state(tgt_pair.second)) {
+                        final.push_back(tgt);
+                    }
+                }
+                mvs.push_back(move_t(m, src, tgt, ab));
+            }
+        }
+    }
+    
+    if (final.empty()) {
+        return alloc(automaton_t, m);
+    }
+    vector<moves_t> inv(n, moves_t());
+    for (unsigned i = 0; i < mvs.size(); ++i) {
+        move_t const& mv = mvs[i];
+        inv[mv.dst()].push_back(move_t(m, mv.dst(), mv.src(), mv.t())); 
+    }
+    
+    svector<bool> back_reachable(n, false);
+    for (unsigned i = 0; i < final.size(); ++i) {
+        back_reachable[final[i]] = true;
+    }
+    
+    unsigned_vector stack(final);
+    while (!stack.empty()) {
+        unsigned state = stack.back();
+        stack.pop_back();
+        moves_t const& mv = inv[state];
+        for (unsigned i = 0; i < mv.size(); ++i) {
+            state = mv[i].dst();
+            if (!back_reachable[state]) {
+                back_reachable[state] = true;
+                stack.push_back(state);
+            }
+        }
+    }
+    
+    moves_t mvs1;
+    for (unsigned i = 0; i < mvs.size(); ++i) {
+        move_t const& mv = mvs[i];
+        if (back_reachable[mv.dst()]) {
+            mvs1.push_back(mv);
+        }
+    }
+    if (mvs1.empty()) {
+        return alloc(automaton_t, m);
+    }
+    else {
+        return alloc(automaton_t, m, 0, final, mvs1);
+    }
+} 
+
+
+
+#endif 

src/sat/sat_solver/inc_sat_solver.cpp

@@ -425,7 +425,7 @@ private:
         DEBUG_CODE(
             for (unsigned i = 0; i < m_fmls.size(); ++i) {
                 expr_ref tmp(m);
-                VERIFY(m_model->eval(m_fmls[i].get(), tmp));                
+                VERIFY(m_model->eval(m_fmls[i].get(), tmp, true));                
                 CTRACE("sat", !m.is_true(tmp),
                        tout << "Evaluation failed: " << mk_pp(m_fmls[i].get(), m) 
                        << " to " << tmp << "\n";

src/smt/theory_seq.cpp

@@ -25,6 +25,7 @@ Revision History:
 #include "theory_seq.h"
 #include "ast_trail.h"
 #include "theory_arith.h"
+#include "smt_kernel.h"
 
 using namespace smt;
 
@@ -36,6 +37,21 @@ struct display_expr {
     }
 };
 
+class seq_expr_solver : public expr_solver {
+    kernel m_kernel;
+public:
+    seq_expr_solver(ast_manager& m, smt_params& fp):
+        m_kernel(m, fp)
+    {}
+
+    virtual lbool check_sat(expr* e) {
+        m_kernel.push();
+        m_kernel.assert_expr(e);
+        lbool r = m_kernel.check();
+        m_kernel.pop(1);
+        return r;
+    }
+};
 
 
 void theory_seq::solution_map::update(expr* e, expr* r, dependency* d) {
@@ -182,6 +198,7 @@ theory_seq::theory_seq(ast_manager& m):
     m(m),
     m_rep(m, m_dm),
     m_eq_id(0),
+    m_find(*this),
     m_factory(0),
     m_exclude(m),
     m_axioms(m),
@@ -198,28 +215,31 @@ theory_seq::theory_seq(ast_manager& m):
     m_new_solution(false),
     m_new_propagation(false),
     m_mk_aut(m) {
-    m_prefix = "seq.prefix.suffix";
+    m_prefix         = "seq.p.suffix";
-    m_suffix = "seq.suffix.prefix";
+    m_suffix         = "seq.s.prefix";
-    m_contains_left = "seq.contains.left";
+    m_accept         = "aut.accept";
-    m_contains_right = "seq.contains.right";
+    m_reject         = "aut.reject";
-    m_accept = "aut.accept";
-    m_reject = "aut.reject";
     m_tail           = "seq.tail";
     m_nth            = "seq.nth";
     m_seq_first      = "seq.first";
     m_seq_last       = "seq.last";
-    m_indexof_left   = "seq.indexof.left";
+    m_indexof_left   = "seq.idx.left";
-    m_indexof_right  = "seq.indexof.right";
+    m_indexof_right  = "seq.idx.right";
     m_aut_step       = "aut.step";
     m_pre            = "seq.pre";  // (seq.pre s l):  prefix of string s of length l
     m_post           = "seq.post"; // (seq.post s l): suffix of string s of length l
     m_eq             = "seq.eq";
+
 }
 
 theory_seq::~theory_seq() {
     m_trail_stack.reset();
 }
 
+void theory_seq::init(context* ctx) {
+    theory::init(ctx);
+    m_mk_aut.set_solver(alloc(seq_expr_solver, m, get_context().get_fparams()));
+}
 
 final_check_status theory_seq::final_check_eh() {
     TRACE("seq", display(tout << "level: " << get_context().get_scope_level() << "\n"););
@@ -585,7 +605,6 @@ bool theory_seq::fixed_length(expr* e) {
     }
     if (is_skolem(m_tail, e) || is_skolem(m_seq_first, e) || 
         is_skolem(m_indexof_left, e) || is_skolem(m_indexof_right, e) ||
-        is_skolem(m_contains_left, e) || is_skolem(m_contains_right, e) ||
         m_fixed.contains(e)) {
         return false;
     }
@@ -885,8 +904,8 @@ void theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) {
     enode_pair_vector eqs;
     linearize(dep, eqs, lits);
     TRACE("seq",
-          tout << "assert:" << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << " <- \n";
+          tout << "assert: " << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << " <-\n";
-          display_deps(tout, dep);
+          display_deps(tout, dep); 
           );
 
     justification* js = ctx.mk_justification(
@@ -944,6 +963,7 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
             // no-op
         }
         else if (m_util.is_seq(li) || m_util.is_re(li)) {
+            TRACE("seq", tout << "inserting " << li << " = " << ri << "\n";);
             m_eqs.push_back(mk_eqdep(li, ri, deps));            
         }
         else {
@@ -1101,6 +1121,7 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de
         return true;
     }
     if (!ctx.inconsistent() && change) {
+        TRACE("seq", tout << "inserting equality\n";);
         m_eqs.push_back(eq(m_eq_id++, ls, rs, deps));
         return true;
     }
@@ -2096,6 +2117,7 @@ theory_var theory_seq::mk_var(enode* n) {
     }
     else {
         theory_var v = theory::mk_var(n);
+        m_find.mk_var();
         get_context().attach_th_var(n, this, v);
         get_context().mark_as_relevant(n);
         return v;
@@ -2897,8 +2919,8 @@ void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
         new_eq_eh(deps, n1, n2);
     }
     TRACE("seq",
-          tout << "assert: " << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "<- \n";
+          tout << "assert: " << mk_pp(e1, m) << " = " << mk_pp(e2, m) << " <- \n";
-          ctx.display_literals_verbose(tout, lits););
+          if (!lits.empty()) { ctx.display_literals_verbose(tout, lits); tout << "\n"; });
     justification* js =
         ctx.mk_justification(
             ext_theory_eq_propagation_justification(
@@ -2963,14 +2985,14 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
     }
     else if (m_util.str.is_contains(e, e1, e2)) {
         if (is_true) {
-            expr_ref f1 = mk_skolem(m_contains_left, e1, e2);
+            expr_ref f1 = mk_skolem(m_indexof_left, e1, e2);
-            expr_ref f2 = mk_skolem(m_contains_right, e1, e2);
+            expr_ref f2 = mk_skolem(m_indexof_right, e1, e2);
             f = mk_concat(f1, e2, f2);
             propagate_eq(lit, f, e1, true);
         }
         else if (!canonizes(false, e)) {
             propagate_non_empty(lit, e2);
-#if 0
+#if 1
             dependency* dep = m_dm.mk_leaf(assumption(lit));
             m_ncs.push_back(nc(expr_ref(e, m), dep));
 #else
@@ -3030,6 +3052,12 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) {
 
 void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) {
     if (n1 != n2 && m_util.is_seq(n1->get_owner())) {
+        theory_var v1 = n1->get_th_var(get_id());
+        theory_var v2 = n2->get_th_var(get_id());
+        if (m_find.find(v1) == m_find.find(v2)) {
+            return;
+        }
+        m_find.merge(v1, v2);
         expr_ref o1(n1->get_owner(), m);
         expr_ref o2(n2->get_owner(), m);
         TRACE("seq", tout << o1 << " = " << o2 << "\n";);

src/smt/theory_seq.h

@@ -28,6 +28,7 @@ Revision History:
 #include "scoped_ptr_vector.h"
 #include "automaton.h"
 #include "seq_rewriter.h"
+#include "union_find.h"
 
 namespace smt {
 
@@ -44,6 +45,7 @@ namespace smt {
         typedef trail_stack<theory_seq> th_trail_stack;
         typedef std::pair<expr*, dependency*> expr_dep;
         typedef obj_map<expr, expr_dep> eqdep_map_t; 
+	typedef union_find<theory_seq> th_union_find;
 
         class seq_value_proc;
 
@@ -292,7 +294,8 @@ namespace smt {
         scoped_vector<eq>          m_eqs;        // set of current equations.
         scoped_vector<ne>          m_nqs;        // set of current disequalities.
         scoped_vector<nc>          m_ncs;        // set of non-contains constraints.
-        unsigned                   m_eq_id;
+        unsigned                   m_eq_id;	
+	th_union_find              m_find;
 
         seq_factory*               m_factory;    // value factory
         exclusion_table            m_exclude;    // set of asserted disequalities.
@@ -309,7 +312,7 @@ namespace smt {
         arith_util       m_autil;
         th_trail_stack   m_trail_stack;
         stats            m_stats;
-        symbol           m_prefix, m_suffix, m_contains_left, m_contains_right, m_accept, m_reject;
+        symbol           m_prefix, m_suffix, m_accept, m_reject;
         symbol           m_tail, m_nth, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step;
         symbol           m_pre, m_post, m_eq;
         ptr_vector<expr> m_todo;
@@ -329,6 +332,7 @@ namespace smt {
 
         obj_hashtable<expr>            m_fixed;            // string variables that are fixed length.
 
+        virtual void init(context* ctx);
         virtual final_check_status final_check_eh();
         virtual bool internalize_atom(app* atom, bool) { return internalize_term(atom); }
         virtual bool internalize_term(app*);
@@ -539,6 +543,11 @@ namespace smt {
         // model building
         app* mk_value(app* a);
 
+	th_trail_stack& get_trail_stack() { return m_trail_stack; }
+        void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2) {}
+        void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { }
+        void unmerge_eh(theory_var v1, theory_var v2) {}
+
     };
 };
 

src/tactic/bv/bv_bounds_tactic.cpp

@@ -20,9 +20,11 @@ Author:
 #include "ctx_simplify_tactic.h"
 #include "bv_decl_plugin.h"
 #include "ast_pp.h"
+#include <climits>
 
-static rational uMaxInt(unsigned sz) {
+static uint64_t uMaxInt(unsigned sz) {
-    return rational::power_of_two(sz) - rational::one();
+    SASSERT(sz <= 64);
+    return ULLONG_MAX >> (64u - sz);
 }
 
 namespace {
@@ -30,26 +32,26 @@ namespace {
 struct interval {
     // l < h: [l, h]
     // l > h: [0, h] U [l, UMAX_INT]
-    rational l, h;
+    uint64_t l, h;
     unsigned sz;
     bool tight;
 
     interval() {}
-    interval(const rational& l, const rational& h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) {
+    interval(uint64_t l, uint64_t h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) {
         // canonicalize full set
-        if (is_wrapped() && l == h + rational::one()) {
+        if (is_wrapped() && l == h + 1) {
-            this->l = rational::zero();
+            this->l = 0;
             this->h = uMaxInt(sz);
         }
         SASSERT(invariant());
     }
 
     bool invariant() const {
-        return !l.is_neg() && !h.is_neg() && l <= uMaxInt(sz) && h <= uMaxInt(sz) &&
+        return l <= uMaxInt(sz) && h <= uMaxInt(sz) &&
-               (!is_wrapped() || l != h+rational::one());
+               (!is_wrapped() || l != h+1);
     }
 
-    bool is_full() const { return l.is_zero() && h == uMaxInt(sz); }
+    bool is_full() const { return l == 0 && h == uMaxInt(sz); }
     bool is_wrapped() const { return l > h; }
     bool is_singleton() const { return l == h; }
 
@@ -129,18 +131,18 @@ struct interval {
     /// return false if negation is empty
     bool negate(interval& result) const {
         if (!tight) {
-            result = interval(rational::zero(), uMaxInt(sz), true);
+            result = interval(0, uMaxInt(sz), true);
             return true;
         }
 
         if (is_full())
             return false;
-        if (l.is_zero()) {
+        if (l == 0) {
-            result = interval(h + rational::one(), uMaxInt(sz), sz);
+            result = interval(h + 1, uMaxInt(sz), sz);
         } else if (uMaxInt(sz) == h) {
-            result = interval(rational::zero(), l - rational::one(), sz);
+            result = interval(0, l - 1, sz);
         } else {
-            result = interval(h + rational::one(), l - rational::one(), sz);
+            result = interval(h + 1, l - 1, sz);
         }
         return true;
     }
@@ -152,59 +154,76 @@ std::ostream& operator<<(std::ostream& o, const interval& I) {
 }
 
 
+struct undo_bound {
+    expr* e;
+    interval b;
+    bool fresh;
+    undo_bound(expr* e, const interval& b, bool fresh) : e(e), b(b), fresh(fresh) {}
+};
+
 class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
     typedef obj_map<expr, interval> map;
     typedef obj_map<expr, bool> expr_set;
     typedef obj_map<expr, expr_set*> expr_list_map;
 
-    ast_manager& m;
+    ast_manager&       m;
-    params_ref   m_params;
+    params_ref         m_params;
-    bool         m_propagate_eq;
+    bool               m_propagate_eq;
-    bv_util      m_bv;
+    bv_util            m_bv;
-    vector<map>  m_scopes;
+    vector<undo_bound> m_scopes;
-    map         *m_bound;
+    map                m_bound;
-    expr_list_map m_expr_vars;
+    expr_list_map      m_expr_vars;
+    expr_set           m_bound_exprs;
 
-    bool is_bound(expr *e, expr*& v, interval& b) {
+    bool is_number(expr *e, uint64_t& n, unsigned& sz) const {
-        rational n;
+        rational r;
+        if (m_bv.is_numeral(e, r, sz) && sz <= 64) {
+            n = r.get_uint64();
+            return true;
+        }
+        return false;
+    }
+
+    bool is_bound(expr *e, expr*& v, interval& b) const {
+        uint64_t n;
         expr *lhs, *rhs;
         unsigned sz;
 
         if (m_bv.is_bv_ule(e, lhs, rhs)) {
-            if (m_bv.is_numeral(lhs, n, sz)) { // C ule x <=> x uge C
+            if (is_number(lhs, n, sz)) { // C ule x <=> x uge C
                 if (m_bv.is_numeral(rhs))
                     return false;
                 b = interval(n, uMaxInt(sz), sz, true);
                 v = rhs;
                 return true;
             }
-            if (m_bv.is_numeral(rhs, n, sz)) { // x ule C
+            if (is_number(rhs, n, sz)) { // x ule C
-                b = interval(rational::zero(), n, sz, true);
+                b = interval(0, n, sz, true);
                 v = lhs;
                 return true;
             }
         } else if (m_bv.is_bv_sle(e, lhs, rhs)) {
-            if (m_bv.is_numeral(lhs, n, sz)) { // C sle x <=> x sge C
+            if (is_number(lhs, n, sz)) { // C sle x <=> x sge C
                 if (m_bv.is_numeral(rhs))
                     return false;
-                b = interval(n, rational::power_of_two(sz-1) - rational::one(), sz, true);
+                b = interval(n, (1ull << (sz-1)) - 1, sz, true);
                 v = rhs;
                 return true;
             }
-            if (m_bv.is_numeral(rhs, n, sz)) { // x sle C
+            if (is_number(rhs, n, sz)) { // x sle C
-                b = interval(rational::power_of_two(sz-1), n, sz, true);
+                b = interval(1ull << (sz-1), n, sz, true);
                 v = lhs;
                 return true;
             }
         } else if (m.is_eq(e, lhs, rhs)) {
-            if (m_bv.is_numeral(lhs, n, sz)) {
+            if (is_number(lhs, n, sz)) {
                 if (m_bv.is_numeral(rhs))
                     return false;
                 b = interval(n, n, sz, true);
                 v = rhs;
                 return true;
             }
-            if (m_bv.is_numeral(rhs, n, sz)) {
+            if (is_number(rhs, n, sz)) {
                 b = interval(n, n, sz, true);
                 v = lhs;
                 return true;
@@ -238,27 +257,29 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
     }
 
     bool expr_has_bounds(expr* t) {
+        bool has_bounds = false;
+        if (m_bound_exprs.find(t, has_bounds))
+            return has_bounds;
+
         app* a = to_app(t);
         if ((m_bv.is_bv_ule(t) || m_bv.is_bv_sle(t) || m.is_eq(t)) &&
-            (m_bv.is_numeral(a->get_arg(0)) || m_bv.is_numeral(a->get_arg(1))))
+            (m_bv.is_numeral(a->get_arg(0)) || m_bv.is_numeral(a->get_arg(1)))) {
-            return true;
+            has_bounds = true;
-
-        for (unsigned i = 0; i < a->get_num_args(); ++i) {
-            if (expr_has_bounds(a->get_arg(i)))
-                return true;
         }
-        return false;
+
+        for (unsigned i = 0; !has_bounds && i < a->get_num_args(); ++i) {
+            has_bounds = expr_has_bounds(a->get_arg(i));
+        }
+
+        m_bound_exprs.insert(t, has_bounds);
+        return has_bounds;
     }
 
 public:
-
     bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) {
-        m_scopes.push_back(map());
-        m_bound = &m_scopes.back();
         updt_params(p);
     }
 
-
     virtual void updt_params(params_ref const & p) {
         m_propagate_eq = p.get_bool("propagate_eq", false);
     }
@@ -285,10 +306,21 @@ public:
             if (sign)
                 VERIFY(b.negate(b));
 
-            push();
             TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";);
-            interval& r = m_bound->insert_if_not_there2(t1, b)->get_data().m_value;
+            map::obj_map_entry* e = m_bound.find_core(t1);
-            return r.intersect(b, r);
+            if (e) {
+                interval& old = e->get_data().m_value;
+                interval intr;
+                if (!old.intersect(b, intr))
+                    return false;
+                if (old == intr)
+                    return true;
+                m_scopes.insert(undo_bound(t1, old, false));
+                old = intr;
+            } else {
+                m_bound.insert(t1, b);
+                m_scopes.insert(undo_bound(t1, interval(), true));
+            }
         }
         return true;
     }
@@ -297,7 +329,7 @@ public:
         expr* t1;
         interval b;
 
-        if (m_bound->find(t, b) && b.is_singleton()) {
+        if (m_bound.find(t, b) && b.is_singleton()) {
             result = m_bv.mk_numeral(b.l, m_bv.get_bv_size(t));
             return true;
         }
@@ -324,16 +356,17 @@ public:
         interval ctx, intr;
         result = 0;
 
-        if (m_bound->find(t1, ctx)) {
+        if (b.is_full() && b.tight) {
+            result = m.mk_true();
+        } else if (m_bound.find(t1, ctx)) {
             if (ctx.implies(b)) {
                 result = m.mk_true();
             } else if (!b.intersect(ctx, intr)) {
                 result = m.mk_false();
             } else if (m_propagate_eq && intr.is_singleton()) {
-                result = m.mk_eq(t1, m_bv.mk_numeral(intr.l, m.get_sort(t1)));
+                result = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()),
+                                                     m.get_sort(t1)));
             }
-        } else if (b.is_full() && b.tight) {
-            result = m.mk_true();
         }
 
         CTRACE("bv", result != 0, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << result << "\n";);
@@ -346,36 +379,43 @@ public:
         if (m_bv.is_numeral(t))
             return false;
 
+        while (m.is_not(t, t));
+
         expr_set* used_exprs = get_expr_vars(t);
-        for (map::iterator I = m_bound->begin(), E = m_bound->end(); I != E; ++I) {
+        for (map::iterator I = m_bound.begin(), E = m_bound.end(); I != E; ++I) {
             if (I->m_value.is_singleton() && used_exprs->contains(I->m_key))
                 return true;
         }
 
-        while (m.is_not(t, t));
-
         expr* t1;
         interval b;
         // skip common case: single bound constraint without any context for simplification
         if (is_bound(t, t1, b)) {
-            return m_bound->contains(t1);
+            return b.is_full() || m_bound.contains(t1);
         }
         return expr_has_bounds(t);
     }
 
-    virtual void push() {
-        TRACE("bv", tout << "push\n";);
-        unsigned sz = m_scopes.size();
-        m_scopes.resize(sz + 1);
-        m_bound = &m_scopes.back();
-        m_bound->~map();
-        new (m_bound) map(m_scopes[sz - 1]);
-    }
-
     virtual void pop(unsigned num_scopes) {
         TRACE("bv", tout << "pop: " << num_scopes << "\n";);
-        m_scopes.shrink(m_scopes.size() - num_scopes);
+        if (m_scopes.empty())
-        m_bound = &m_scopes.back();
+            return;
+        unsigned target = m_scopes.size() - num_scopes;
+        if (target == 0) {
+            m_bound.reset();
+            m_scopes.reset();
+            return;
+        }
+        for (unsigned i = m_scopes.size()-1; i >= target; --i) {
+            undo_bound& undo = m_scopes[i];
+            SASSERT(m_bound.contains(undo.e));
+            if (undo.fresh) {
+                m_bound.erase(undo.e);
+            } else {
+                m_bound.insert(undo.e, undo.b);
+            }
+        }
+        m_scopes.shrink(target);
     }
 
     virtual simplifier * translate(ast_manager & m) {
@@ -383,7 +423,7 @@ public:
     }
 
     virtual unsigned scope_level() const {
-        return m_scopes.size() - 1;
+        return m_scopes.size();
     }
 };
 

src/tactic/core/ctx_simplify_tactic.cpp

@@ -36,7 +36,7 @@ public:
     virtual ~ctx_propagate_assertions() {}
     virtual bool assert_expr(expr * t, bool sign);
     virtual bool simplify(expr* t, expr_ref& result);
-    virtual void push();
+    void push();
     virtual void pop(unsigned num_scopes);
     virtual unsigned scope_level() const { return m_scopes.size(); }
     virtual simplifier * translate(ast_manager & m);
@@ -260,10 +260,6 @@ struct ctx_simplify_tactic::imp {
         return m_simp->scope_level();
     }
 
-    void push() { 
-        m_simp->push();
-    }
-
     void restore_cache(unsigned lvl) {
         if (lvl >= m_cache_undo.size())
             return;

src/tactic/core/ctx_simplify_tactic.h

@@ -31,7 +31,6 @@ public:
         virtual bool assert_expr(expr * t, bool sign) = 0;
         virtual bool simplify(expr* t, expr_ref& result) = 0;
         virtual bool may_simplify(expr* t) { return true; }
-        virtual void push() = 0;
         virtual void pop(unsigned num_scopes) = 0;
         virtual simplifier * translate(ast_manager & m) = 0;
         virtual unsigned scope_level() const = 0;