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

src/api/api_context.cpp

@@ -142,7 +142,7 @@ namespace api {
         #pragma omp critical (set_interruptable)
         {
             if (m_interruptable)
-                (*m_interruptable)();
+                (*m_interruptable)(API_INTERRUPT_EH_CALLER);
             m_limit.cancel();
             m().limit().cancel();
         }

src/api/api_solver.cpp

@@ -296,10 +296,14 @@ extern "C" {
                 result = to_solver_ref(s)->check_sat(num_assumptions, _assumptions);
             }
             catch (z3_exception & ex) {
+                to_solver_ref(s)->set_reason_unknown(eh);
                 mk_c(c)->handle_exception(ex);
                 return Z3_L_UNDEF;
             }
         }
+        if (result == l_undef) {
+            to_solver_ref(s)->set_reason_unknown(eh);
+        }
         return static_cast<Z3_lbool>(result);
     }
     
@@ -466,10 +470,14 @@ extern "C" {
                 result = to_solver_ref(s)->get_consequences(_assumptions, _variables, _consequences);
             }
             catch (z3_exception & ex) {
+                to_solver_ref(s)->set_reason_unknown(eh);
                 mk_c(c)->handle_exception(ex);
                 return Z3_L_UNDEF;
             }
         }
+        if (result == l_undef) {
+            to_solver_ref(s)->set_reason_unknown(eh);
+        }
         for (unsigned i = 0; i < _consequences.size(); ++i) {
             to_ast_vector_ref(consequences).push_back(_consequences[i].get());
         }

src/api/ml/z3.ml

@@ -1215,6 +1215,44 @@ struct
   let mk_numeral ctx v size = Z3native.mk_numeral ctx v (mk_sort ctx size)
 end
 
+module Seq =
+struct
+  let mk_seq_sort  = Z3native.mk_seq_sort
+  let is_seq_sort = Z3native.is_seq_sort 
+  let mk_re_sort = Z3native.mk_re_sort
+  let is_re_sort = Z3native.is_re_sort
+  let mk_string_sort = Z3native.mk_string_sort
+  let is_string_sort = Z3native.is_string_sort
+  let mk_string = Z3native.mk_string
+  let is_string = Z3native.is_string
+  let get_string = Z3native.get_string
+  let mk_seq_empty = Z3native.mk_seq_empty
+  let mk_seq_unit = Z3native.mk_seq_unit
+  let mk_seq_concat ctx args = Z3native.mk_seq_concat ctx (List.length args) args
+  let mk_seq_prefix = Z3native.mk_seq_prefix
+  let mk_seq_suffix = Z3native.mk_seq_suffix
+  let mk_seq_contains = Z3native.mk_seq_contains 
+  let mk_seq_extract = Z3native.mk_seq_extract
+  let mk_seq_replace = Z3native.mk_seq_replace
+  let mk_seq_at = Z3native.mk_seq_at
+  let mk_seq_length = Z3native.mk_seq_length
+  let mk_seq_index = Z3native.mk_seq_index
+  let mk_str_to_int = Z3native.mk_str_to_int
+  let mk_int_to_str = Z3native.mk_int_to_str
+  let mk_seq_to_re = Z3native.mk_seq_to_re
+  let mk_seq_in_re = Z3native.mk_seq_in_re
+  let mk_re_plus = Z3native.mk_re_plus
+  let mk_re_star = Z3native.mk_re_star
+  let mk_re_option = Z3native.mk_re_option
+  let mk_re_union ctx args = Z3native.mk_re_union ctx (List.length args) args
+  let mk_re_concat ctx args = Z3native.mk_re_concat ctx (List.length args) args
+  let mk_re_range = Z3native.mk_re_range
+  let mk_re_loop = Z3native.mk_re_loop
+  let mk_re_intersect = Z3native.mk_re_intersect
+  let mk_re_complement = Z3native.mk_re_complement
+  let mk_re_empty = Z3native.mk_re_empty
+  let mk_re_full = Z3native.mk_re_full
+end
 
 module FloatingPoint =
 struct

src/api/ml/z3.mli

@@ -1825,6 +1825,116 @@ sig
   val mk_numeral : context -> string -> int -> Expr.expr
 end
 
+(** Sequences, Strings and Regular Expressions **)
+module Seq : 
+sig
+  (* create a sequence sort *)
+  val mk_seq_sort : context -> Sort.sort -> Sort.sort
+
+  (* test if sort is a sequence sort *)
+  val is_seq_sort : context -> Sort.sort -> bool
+
+  (* create regular expression sorts over sequences of the argument sort *)   
+  val mk_re_sort : context -> Sort.sort -> Sort.sort
+
+  (* test if sort is a regular expression sort *)
+  val is_re_sort : context -> Sort.sort -> bool
+
+  (* create string sort *)
+  val mk_string_sort : context -> Sort.sort
+
+  (* test if sort is a string sort (a sequence of 8-bit bit-vectors) *)
+  val is_string_sort : context -> Sort.sort -> bool 
+
+  (* create a string literal *)
+  val mk_string : context -> string -> Expr.expr
+
+  (* test if expression is a string *)
+  val is_string : context -> Expr.expr -> bool 
+
+  (* retrieve string from string Expr.expr *)
+  val get_string : context -> Expr.expr -> string 
+
+  (* the empty sequence over base sort *)
+  val mk_seq_empty : context -> Sort.sort -> Expr.expr 
+
+  (* a unit sequence *)
+  val mk_seq_unit : context -> Expr.expr -> Expr.expr 
+
+  (* sequence concatenation *)
+  val mk_seq_concat : context -> Expr.expr list -> Expr.expr 
+
+  (* predicate if the first argument is a prefix of the second *)
+  val mk_seq_prefix : context -> Expr.expr -> Expr.expr -> Expr.expr  
+
+  (* predicate if the first argument is a suffix of the second *)
+  val mk_seq_suffix : context -> Expr.expr -> Expr.expr -> Expr.expr  
+
+  (* predicate if the first argument contains the second *)
+  val mk_seq_contains : context -> Expr.expr -> Expr.expr -> Expr.expr  
+
+  (* extract sub-sequence starting at index given by second argument and of length provided by third argument *)
+  val mk_seq_extract : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr  
+
+  (* replace first occurrence of second argument by third *)
+  val mk_seq_replace : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr  
+
+  (* a unit sequence at index provided by second argument *)
+  val mk_seq_at : context -> Expr.expr -> Expr.expr -> Expr.expr 
+
+  (* length of a sequence *)
+  val mk_seq_length : context -> Expr.expr -> Expr.expr  
+
+  (* index of the first occurrence of the second argument in the first *)
+  val mk_seq_index : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr 
+
+  (* retrieve integer expression encoded in string *)
+  val mk_str_to_int : context -> Expr.expr -> Expr.expr
+
+  (* convert an integer expression to a string *)
+  val mk_int_to_str : context -> Expr.expr -> Expr.expr 
+
+  (* create regular expression that accepts the argument sequence *)
+  val mk_seq_to_re : context -> Expr.expr -> Expr.expr 
+
+  (* regular expression membership predicate *)
+  val mk_seq_in_re : context -> Expr.expr -> Expr.expr -> Expr.expr 
+
+  (* regular expression plus *)
+  val mk_re_plus : context -> Expr.expr -> Expr.expr 
+
+  (* regular expression star *)
+  val mk_re_star : context -> Expr.expr -> Expr.expr 
+
+  (* optional regular expression *)
+  val mk_re_option : context -> Expr.expr -> Expr.expr 
+
+  (* union of regular expressions *)
+  val mk_re_union : context -> Expr.expr list -> Expr.expr 
+
+  (* concatenation of regular expressions* )
+  val mk_re_concat : context -> Expr.expr list -> Expr.expr 
+  
+  (* regular expression for the range between two characters *)
+  val mk_re_range : context -> Expr.expr -> Expr.expr -> Expr.expr 
+
+  (* bounded loop regular expression *)
+  val mk_re_loop : context -> Expr.expr -> int -> int -> Expr.expr 
+  
+  (* intersection of regular expressions *)
+  val mk_re_intersect : context -> int -> Expr.expr list -> Expr.expr
+
+  (* the regular expression complement *)
+  val mk_re_complement : context -> Expr.expr -> Expr.expr 
+
+  (* the regular expression that accepts no sequences *)
+  val mk_re_empty : context -> Sort.sort -> Expr.expr 
+
+  (* the regular expression that accepts all sequences *)
+  val mk_re_full : context -> Sort.sort -> Expr.expr 
+
+end
+
 (** Floating-Point Arithmetic *)
 module FloatingPoint :
 sig

src/smt/mam.cpp

@@ -2080,12 +2080,13 @@ namespace smt {
     */
     enode_vector * interpreter::mk_depth1_vector(enode * n, func_decl * f, unsigned i) {
         enode_vector * v = mk_enode_vector();
+        unsigned num_args = n->get_num_args();
         n = n->get_root();
         enode_vector::const_iterator it  = n->begin_parents();
         enode_vector::const_iterator end = n->end_parents();
         for (; it != end; ++it) {
             enode * p = *it;
-            if (p->get_decl() == f  &&
+            if (p->get_decl() == f  && 
                 m_context.is_relevant(p)  &&
                 p->is_cgr() &&
                 i < p->get_num_args() &&
@@ -2105,6 +2106,7 @@ namespace smt {
         enode * n = m_registers[j2->m_reg]->get_root();
         if (n->get_num_parents() == 0)
             return 0;
+        unsigned num_args = n->get_num_args();
         enode_vector * v  = mk_enode_vector();
         enode_vector::const_iterator it1  = n->begin_parents();
         enode_vector::const_iterator end1 = n->end_parents();
@@ -2121,6 +2123,7 @@ namespace smt {
                 for (; it2 != end2; ++it2) {
                     enode * p2 = *it2;
                     if (p2->get_decl() == f &&
+                        num_args == n->get_num_args() && 
                         m_context.is_relevant(p2) &&
                         p2->is_cgr() &&
                         p2->get_arg(i)->get_root() == p) {

src/smt/theory_str.cpp

@@ -1670,6 +1670,8 @@ namespace smt {
             u.str.is_string(range1, range1val);
             u.str.is_string(range2, range2val);
             return zstring("[") + range1val + zstring("-") + range2val + zstring("]");
+        } else if (u.re.is_full(a_regex)) {
+            return zstring("(.*)");
         } else {
             TRACE("str", tout << "BUG: unrecognized regex term " << mk_pp(regex, get_manager()) << std::endl;);
             UNREACHABLE(); return zstring("");
@@ -1700,6 +1702,12 @@ namespace smt {
         expr_ref str(ex->get_arg(0), m);
         app * regex = to_app(ex->get_arg(1));
 
+        // quick reference for the following code:
+        //  - ex: top-level regex membership term
+        //  - str: string term appearing in ex
+        //  - regex: regex term appearing in ex
+        //  ex ::= (str.in.re str regex)
+
         if (u.re.is_to_re(regex)) {
             expr_ref rxStr(regex->get_arg(0), m);
             // want to assert 'expr IFF (str == rxStr)'
@@ -1779,6 +1787,9 @@ namespace smt {
             expr_ref finalAxiom(m.mk_iff(ex, rhs), m);
             SASSERT(finalAxiom);
             assert_axiom(finalAxiom);
+        } else if (u.re.is_full(regex)) {
+            // trivially true for any string!
+            assert_axiom(ex);
         } else {
             TRACE("str", tout << "ERROR: unknown regex expression " << mk_pp(regex, m) << "!" << std::endl;);
             NOT_IMPLEMENTED_YET();
@@ -6179,24 +6190,31 @@ namespace smt {
             expr * arg_str = a->get_arg(0);
             zstring str;
             if (u.str.is_string(arg_str, str)) {
-                TRACE("str", tout << "build NFA for '" << str << "'" << "\n";);
+                if (str.length() == 0) {
-                /*
+                    // transitioning on the empty string is handled specially
-                 * For an n-character string, we make (n-1) intermediate states,
+                    TRACE("str", tout << "empty string epsilon-move " << start << " --> " << end << std::endl;);
-                 * labelled i_(0) through i_(n-2).
+                    make_epsilon_move(start, end);
-                 * Then we construct the following transitions:
+                } else {
-                 * start --str[0]--> i_(0) --str[1]--> i_(1) --...--> i_(n-2) --str[n-1]--> final
+                    TRACE("str", tout << "build NFA for '" << str << "'" << "\n";);
-                 */
+                    /*
-                unsigned last = start;
+                     * For an n-character string, we make (n-1) intermediate states,
-                for (int i = 0; i <= ((int)str.length()) - 2; ++i) {
+                     * labelled i_(0) through i_(n-2).
-                    unsigned i_state = next_id();
+                     * Then we construct the following transitions:
-                    make_transition(last, str[i], i_state);
+                     * start --str[0]--> i_(0) --str[1]--> i_(1) --...--> i_(n-2) --str[n-1]--> final
-                    TRACE("str", tout << "string transition " << last << "--" << str[i] << "--> " << i_state << "\n";);
+                     */
-                    last = i_state;
+                    unsigned last = start;
+                    for (int i = 0; i <= ((int)str.length()) - 2; ++i) {
+                        unsigned i_state = next_id();
+                        make_transition(last, str[i], i_state);
+                        TRACE("str", tout << "string transition " << last << "--" << str[i] << "--> " << i_state << "\n";);
+                        last = i_state;
+                    }
+                    make_transition(last, str[(str.length() - 1)], end);
+                    TRACE("str", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";);
                 }
-                make_transition(last, str[(str.length() - 1)], end);
+            } else { // ! u.str.is_string(arg_str, str)
-                TRACE("str", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";);
+                TRACE("str", tout << "WARNING: invalid string constant in str.to.re! Cancelling." << std::endl;);
-            } else {
+                u.get_manager().raise_exception("invalid term in str.to.re, argument must be a string constant");
-                TRACE("str", tout << "invalid string constant in Str2Reg" << std::endl;);
                 m_valid = false;
                 return;
             }
@@ -6268,6 +6286,19 @@ namespace smt {
             }
 
             TRACE("str", tout << "range NFA: start = " << start << ", end = " << end << std::endl;);
+        } else if (u.re.is_full(e)) {
+            // effectively the same as .* where . can be any single character
+            // start --e--> tmp
+            // tmp --e--> end
+            // tmp --C--> tmp for every character C
+            unsigned tmp = next_id();
+            make_epsilon_move(start, tmp);
+            make_epsilon_move(tmp, end);
+            for (unsigned int i = 0; i < 256; ++i) {
+                char ch = (char)i;
+                make_transition(tmp, ch, tmp);
+            }
+            TRACE("str", tout << "re.all NFA: start = " << start << ", end = " << end << std::endl;);
         } else {
             TRACE("str", tout << "invalid regular expression" << std::endl;);
             m_valid = false;

src/solver/check_sat_result.cpp

@@ -18,6 +18,24 @@ Notes:
 --*/
 #include "solver/check_sat_result.h"
 
+void check_sat_result::set_reason_unknown(event_handler& eh) {
+    switch (eh.caller_id()) {
+    case UNSET_EH_CALLER: break;
+    case CTRL_C_EH_CALLER:
+        set_reason_unknown("interrupted from keyboard");
+        break;
+    case TIMEOUT_EH_CALLER:
+        set_reason_unknown("timeout");
+        break;
+    case RESLIMIT_EH_CALLER:
+        set_reason_unknown("max. resource limit exceeded");
+        break;
+    case API_INTERRUPT_EH_CALLER:
+        set_reason_unknown("interrupted");
+        break;
+    }
+}
+
 simple_check_sat_result::simple_check_sat_result(ast_manager & m):
     m_core(m),
     m_proof(m) {

src/solver/check_sat_result.h

@@ -22,6 +22,7 @@ Notes:
 #include "model/model.h"
 #include "util/lbool.h"
 #include "util/statistics.h"
+#include "util/event_handler.h"
 
 /**
    \brief Abstract interface for the result of a (check-sat) like command.
@@ -57,6 +58,7 @@ public:
     virtual proof * get_proof() = 0;
     virtual std::string reason_unknown() const = 0;
     virtual void set_reason_unknown(char const* msg) = 0;
+    void set_reason_unknown(event_handler& eh);
     virtual void get_labels(svector<symbol> & r) = 0;
     virtual ast_manager& get_manager() const = 0;
 

src/solver/combined_solver.cpp

@@ -89,8 +89,8 @@ private:
                 m_solver->get_manager().limit().dec_cancel();
             }
         }
-        virtual void operator()() {
+        virtual void operator()(event_handler_caller_t caller_id) {
-            m_canceled = true;
+            m_canceled = true;            
             m_solver->get_manager().limit().inc_cancel();
         }
     };

src/util/cancel_eh.h

@@ -31,10 +31,14 @@ class cancel_eh : public event_handler {
 public:
     cancel_eh(T & o): m_canceled(false), m_obj(o) {}
     ~cancel_eh() { if (m_canceled) m_obj.dec_cancel(); }
-    virtual void operator()() { 
+    virtual void operator()(event_handler_caller_t caller_id) {
-        m_canceled = true;
+        if (!m_canceled) {
-        m_obj.inc_cancel(); 
+            m_caller_id = caller_id;
+            m_canceled = true;
+            m_obj.inc_cancel(); 
+        }
     }
+    bool canceled() const { return m_canceled; }
 };
 
 #endif

src/util/event_handler.h

@@ -19,10 +19,22 @@ Revision History:
 #ifndef EVENT_HANDLER_H_
 #define EVENT_HANDLER_H_
 
+enum event_handler_caller_t {
+    UNSET_EH_CALLER,
+    CTRL_C_EH_CALLER,
+    TIMEOUT_EH_CALLER,
+    RESLIMIT_EH_CALLER,
+    API_INTERRUPT_EH_CALLER
+};
+
 class event_handler {
+protected:
+    event_handler_caller_t m_caller_id;
 public:
+    event_handler(): m_caller_id(UNSET_EH_CALLER) {}
     virtual ~event_handler() {}
-    virtual void operator()() = 0;
+    virtual void operator()(event_handler_caller_t caller_id) = 0;
+    event_handler_caller_t caller_id() const { return m_caller_id; }
 };
 
 #endif

src/util/scoped_ctrl_c.cpp

@@ -24,7 +24,7 @@ scoped_ctrl_c * scoped_ctrl_c::g_obj = 0;
 
 void scoped_ctrl_c::on_ctrl_c(int) {
     if (g_obj->m_first) {
-        g_obj->m_cancel_eh();
+        g_obj->m_cancel_eh(CTRL_C_EH_CALLER);
         if (g_obj->m_once) {
             g_obj->m_first = false;
             signal(SIGINT, on_ctrl_c); // re-install the handler

src/util/scoped_timer.cpp

@@ -85,7 +85,7 @@ struct scoped_timer::imp {
             obj->m_first = false;
         }
         else {
-            obj->m_eh->operator()();
+            obj->m_eh->operator()(TIMEOUT_EH_CALLER);
         }
     }
 #elif defined(__APPLE__) && defined(__MACH__)
@@ -98,7 +98,7 @@ struct scoped_timer::imp {
         int e = pthread_cond_timedwait(&st->m_condition_var, &st->m_mutex, &st->m_end_time);
         if (e != 0 && e != ETIMEDOUT)
             throw default_exception("failed to start timed wait");
-        st->m_eh->operator()();
+        st->m_eh->operator()(TIMEOUT_EH_CALLER);
 
         pthread_mutex_unlock(&st->m_mutex);
 
@@ -133,7 +133,7 @@ struct scoped_timer::imp {
         pthread_mutex_unlock(&st->m_mutex);
 
         if (e == ETIMEDOUT)
-            st->m_eh->operator()();
+            st->m_eh->operator()(TIMEOUT_EH_CALLER);
         return 0;
     }
 #else

src/util/timeout.cpp

@@ -32,10 +32,11 @@ void (* g_on_timeout)() = 0;
 
 class g_timeout_eh : public event_handler {
 public:
-    void operator()() {
+    void operator()(event_handler_caller_t caller_id) {
         #pragma omp critical (g_timeout_cs) 
         {
             std::cout << "timeout\n";
+            m_caller_id = caller_id;
             if (g_on_timeout)
                 g_on_timeout();
             if (g_timeout)