keep

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

scripts/mk_nuget_task.py

@@ -25,7 +25,7 @@ def mk_dir(d):
 os_info = {"z64-ubuntu-14" : ('so', 'ubuntu.14.04-x64'),
            'ubuntu-18' : ('so', 'ubuntu-x64'),
            'ubuntu-20' : ('so', 'ubuntu-x64'),
-           'glibc-2.31' : ('so', 'glibc-x64'),
+           'glibc-2.31' : ('so', 'ubuntu-x64'),
            'x64-win' : ('dll', 'win-x64'),
            'x86-win' : ('dll', 'win-x86'),
            'osx' : ('dylib', 'osx-x64'),

scripts/release.yml

@@ -78,7 +78,7 @@ stages:
       vmImage: "ubuntu-latest"
     container: "quay.io/pypa/manylinux2010_x86_64:latest"
     variables:
-      python: "/opt/python/cp35-cp35m/bin/python"
+      python: "/opt/python/cp37-cp37m/bin/python"
     steps:
     - task: PythonScript@0
       displayName: Build

src/api/c++/z3++.h

@@ -164,7 +164,7 @@ namespace z3 {
         void set_context(Z3_context ctx) {
             m_ctx = ctx;
             m_enable_exceptions = true;
-            m_rounding_mode = RNA;
+            m_rounding_mode = RNE;
             Z3_set_error_handler(m_ctx, 0);
             Z3_set_ast_print_mode(m_ctx, Z3_PRINT_SMTLIB2_COMPLIANT);
         }
@@ -287,7 +287,7 @@ namespace z3 {
         /**
            \brief Return a RoundingMode sort.
          */
-        sort fpa_rounding_mode();
+        sort fpa_rounding_mode_sort();
         /**
            \brief Sets RoundingMode of FloatingPoints.
          */
@@ -342,6 +342,8 @@ namespace z3 {
         template<size_t precision>
         expr fpa_const(char const * name);
 
+        expr fpa_rounding_mode();
+
         expr bool_val(bool b);
 
         expr int_val(int n);
@@ -366,6 +368,8 @@ namespace z3 {
 
         expr fpa_val(double n);
         expr fpa_val(float n);
+        expr fpa_nan(sort const & s);
+        expr fpa_inf(sort const & s, bool sgn);
 
         expr string_val(char const* s);
         expr string_val(char const* s, unsigned n);
@@ -696,6 +700,8 @@ namespace z3 {
             \pre is_array()
         */
         sort array_range() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); }
+
+        friend std::ostream & operator<<(std::ostream & out, sort const & s) { return out << Z3_sort_to_string(s.ctx(), Z3_sort(s.m_ast)); }
     };
 
     /**
@@ -874,7 +880,7 @@ namespace z3 {
         bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast); check_error(); return r; }
 
         /**
-           \brief Return Boolean expression to test whether expression is inf
+           \brief Return Boolean expression to test for whether an FP expression is inf
         */
         expr mk_is_inf() const {
             assert(is_fpa());
@@ -884,7 +890,7 @@ namespace z3 {
         }
 
         /**
-           \brief Return Boolean expression to test for whether expression is a NaN
+           \brief Return Boolean expression to test for whether an FP expression is a NaN
         */
         expr mk_is_nan() const {
             assert(is_fpa());
@@ -893,6 +899,36 @@ namespace z3 {
             return expr(ctx(), r);
         }
 
+        /**
+           \brief Return Boolean expression to test for whether an FP expression is a normal
+        */
+        expr mk_is_normal() const {
+            assert(is_fpa());
+            Z3_ast r = Z3_mk_fpa_is_normal(ctx(), m_ast);
+            check_error();
+            return expr(ctx(), r);
+        }
+
+        /**
+           \brief Return Boolean expression to test for whether an FP expression is a subnormal
+        */
+        expr mk_is_subnormal() const {
+            assert(is_fpa());
+            Z3_ast r = Z3_mk_fpa_is_subnormal(ctx(), m_ast);
+            check_error();
+            return expr(ctx(), r);
+        }
+
+        /**
+           \brief Return Boolean expression to test for whether an FP expression is a zero
+        */
+        expr mk_is_zero() const {
+            assert(is_fpa());
+            Z3_ast r = Z3_mk_fpa_is_zero(ctx(), m_ast);
+            check_error();
+            return expr(ctx(), r);
+        }
+
         /**
            \brief Convert this fpa into an IEEE BV
         */
@@ -903,6 +939,16 @@ namespace z3 {
             return expr(ctx(), r);
         }
 
+        /**
+           \brief Convert this IEEE BV into a fpa
+        */
+        expr mk_from_ieee_bv(sort const &s) const {
+            assert(is_bv());
+            Z3_ast r = Z3_mk_fpa_to_fp_bv(ctx(), m_ast, s);
+            check_error();
+            return expr(ctx(), r);
+        }
+
         /**
            \brief Return string representation of numeral or algebraic number
            This method assumes the expression is numeral or algebraic
@@ -1078,17 +1124,6 @@ namespace z3 {
 
         operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
 
-        /**
-           \brief Return a RoundingMode sort.
-         */
-        sort fpa_rounding_mode() {
-            assert(is_fpa());
-            Z3_sort s = ctx().fpa_rounding_mode();
-            check_error();
-            return sort(ctx(), s);
-        }
-
-
         /**
            \brief Return the declaration associated with this application.
            This method assumes the expression is an application.
@@ -1297,8 +1332,12 @@ namespace z3 {
         expr rotate_right(unsigned i) { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
         expr repeat(unsigned i) { Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
 
+        friend expr bvredor(expr const & a);
+        friend expr bvredand(expr const & a);
+
         friend expr abs(expr const & a);
         friend expr sqrt(expr const & a, expr const & rm);
+        friend expr fp_eq(expr const & a, expr const & b);
 
         friend expr operator~(expr const & a);
         expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
@@ -1325,6 +1364,26 @@ namespace z3 {
         */
         friend expr fpa_to_ubv(expr const& t, unsigned sz);
 
+        /**
+           \brief Conversion of a signed bit-vector term into a floating-point.
+        */
+        friend expr sbv_to_fpa(expr const& t, sort s);
+
+        /**
+           \brief Conversion of an unsigned bit-vector term into a floating-point.
+        */
+        friend expr ubv_to_fpa(expr const& t, sort s);
+
+        /**
+           \brief Conversion of a floating-point term into another floating-point.
+        */
+        friend expr fpa_to_fpa(expr const& t, sort s);
+
+        /**
+           \brief Round a floating-point term into its closest integer.
+        */
+        friend expr round_fpa_to_closest_integer(expr const& t);
+
         /**
            \brief sequence and regular expression operations.
            + is overloaded as sequence concatenation and regular expression union.
@@ -1789,6 +1848,18 @@ namespace z3 {
         }
         return expr(a.ctx(), r); 
     }
+    inline expr bvredor(expr const & a) {
+        assert(a.is_bv());
+        Z3_ast r = Z3_mk_bvredor(a.ctx(), a);
+        a.check_error();
+        return expr(a.ctx(), r);
+    }
+    inline expr bvredand(expr const & a) {
+        assert(a.is_bv());
+        Z3_ast r = Z3_mk_bvredor(a.ctx(), a);
+        a.check_error();
+        return expr(a.ctx(), r);
+    }
     inline expr abs(expr const & a) { 
         Z3_ast r;
         if (a.is_int()) {
@@ -1812,6 +1883,13 @@ namespace z3 {
         a.check_error();
         return expr(a.ctx(), r);
     }
+    inline expr fp_eq(expr const & a, expr const & b) {
+        check_context(a, b);
+        assert(a.is_fpa());
+        Z3_ast r = Z3_mk_fpa_eq(a.ctx(), a, b);
+        a.check_error();
+        return expr(a.ctx(), r);
+    }
     inline expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
 
     inline expr fma(expr const& a, expr const& b, expr const& c, expr const& rm) {
@@ -1844,6 +1922,34 @@ namespace z3 {
         return expr(t.ctx(), r);
     }
 
+    inline expr sbv_to_fpa(expr const& t, sort s) {
+        assert(t.is_bv());
+        Z3_ast r = Z3_mk_fpa_to_fp_signed(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
+        t.check_error();
+        return expr(t.ctx(), r);
+    }
+
+    inline expr ubv_to_fpa(expr const& t, sort s) {
+        assert(t.is_bv());
+        Z3_ast r = Z3_mk_fpa_to_fp_unsigned(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
+        t.check_error();
+        return expr(t.ctx(), r);
+    }
+
+    inline expr fpa_to_fpa(expr const& t, sort s) {
+        assert(t.is_fpa());
+        Z3_ast r = Z3_mk_fpa_to_fp_float(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
+        t.check_error();
+        return expr(t.ctx(), r);
+    }
+
+    inline expr round_fpa_to_closest_integer(expr const& t) {
+        assert(t.is_fpa());
+        Z3_ast r = Z3_mk_fpa_round_to_integral(t.ctx(), t.ctx().fpa_rounding_mode(), t);
+        t.check_error();
+        return expr(t.ctx(), r);
+    }
+
     /**
        \brief Create the if-then-else expression <tt>ite(c, t, e)</tt>
 
@@ -3109,18 +3215,7 @@ namespace z3 {
     template<>
     inline sort context::fpa_sort<128>() { return fpa_sort(15, 113); }
 
-    inline sort context::fpa_rounding_mode() {
+    inline sort context::fpa_rounding_mode_sort() { Z3_sort r = Z3_mk_fpa_rounding_mode_sort(m_ctx); check_error(); return sort(*this, r); }
-        switch (m_rounding_mode) {
-        case RNA: return sort(*this, Z3_mk_fpa_rna(m_ctx));
-        case RNE: return sort(*this, Z3_mk_fpa_rne(m_ctx));
-        case RTP: return sort(*this, Z3_mk_fpa_rtp(m_ctx));
-        case RTN: return sort(*this, Z3_mk_fpa_rtn(m_ctx));
-        case RTZ: return sort(*this, Z3_mk_fpa_rtz(m_ctx));
-        default: return sort(*this); 
-        }
-    }
-
-    inline void context::set_rounding_mode(rounding_mode rm) { m_rounding_mode = rm; }
 
     inline sort context::array_sort(sort d, sort r) { Z3_sort s = Z3_mk_array_sort(m_ctx, d, r); check_error(); return sort(*this, s); }
     inline sort context::array_sort(sort_vector const& d, sort r) {
@@ -3277,6 +3372,19 @@ namespace z3 {
     template<size_t precision>
     inline expr context::fpa_const(char const * name) { return constant(name, fpa_sort<precision>()); }
 
+    inline void context::set_rounding_mode(rounding_mode rm) { m_rounding_mode = rm; }
+
+    inline expr context::fpa_rounding_mode() {
+        switch (m_rounding_mode) {
+        case RNA: return expr(*this, Z3_mk_fpa_rna(m_ctx));
+        case RNE: return expr(*this, Z3_mk_fpa_rne(m_ctx));
+        case RTP: return expr(*this, Z3_mk_fpa_rtp(m_ctx));
+        case RTN: return expr(*this, Z3_mk_fpa_rtn(m_ctx));
+        case RTZ: return expr(*this, Z3_mk_fpa_rtz(m_ctx));
+        default: return expr(*this);
+        }
+    }
+
     inline expr context::bool_val(bool b) { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
 
     inline expr context::int_val(int n) { Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }
@@ -3305,6 +3413,8 @@ namespace z3 {
 
     inline expr context::fpa_val(double n) { sort s = fpa_sort<64>(); Z3_ast r = Z3_mk_fpa_numeral_double(m_ctx, n, s); check_error(); return expr(*this, r); }
     inline expr context::fpa_val(float n) { sort s = fpa_sort<32>(); Z3_ast r = Z3_mk_fpa_numeral_float(m_ctx, n, s); check_error(); return expr(*this, r); }
+    inline expr context::fpa_nan(sort const & s) { Z3_ast r = Z3_mk_fpa_nan(m_ctx, s); check_error(); return expr(*this, r); }
+    inline expr context::fpa_inf(sort const & s, bool sgn) { Z3_ast r = Z3_mk_fpa_inf(m_ctx, s, sgn); check_error(); return expr(*this, r); }
 
     inline expr context::string_val(char const* s, unsigned n) { Z3_ast r = Z3_mk_lstring(m_ctx, n, s); check_error(); return expr(*this, r); }
     inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }

src/api/julia/z3jl.cpp

@@ -216,7 +216,6 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
         .MM(expr, is_string_value)
         .MM(expr, get_escaped_string)
         .MM(expr, get_string)
-        .MM(expr, fpa_rounding_mode)
         .MM(expr, decl)
         .MM(expr, num_args)
         .MM(expr, arg)

src/ast/ast.cpp

@@ -41,6 +41,9 @@ parameter::~parameter() {
     if (m_kind == PARAM_RATIONAL) {
         dealloc(m_rational);
     }
+    if (m_kind == PARAM_ZSTRING) {
+        dealloc(m_zstring);
+    }
 }
 
 parameter::parameter(parameter const& other) {
@@ -64,6 +67,7 @@ parameter& parameter::operator=(parameter const& other) {
     case PARAM_RATIONAL: m_rational = alloc(rational, other.get_rational()); break;
     case PARAM_DOUBLE: m_dval = other.m_dval; break;
     case PARAM_EXTERNAL: m_ext_id = other.m_ext_id; break;
+    case PARAM_ZSTRING: m_zstring = alloc(zstring, other.get_zstring()); break;
     default:
         UNREACHABLE();
         break;
@@ -99,6 +103,7 @@ bool parameter::operator==(parameter const & p) const {
     case PARAM_RATIONAL: return get_rational() == p.get_rational();
     case PARAM_DOUBLE: return m_dval == p.m_dval;
     case PARAM_EXTERNAL: return m_ext_id == p.m_ext_id;
+    case PARAM_ZSTRING: return get_zstring() == p.get_zstring();
     default: UNREACHABLE(); return false;
     }
 }
@@ -111,6 +116,7 @@ unsigned parameter::hash() const {
     case PARAM_SYMBOL:   b = get_symbol().hash(); break;
     case PARAM_RATIONAL: b = get_rational().hash(); break;
     case PARAM_DOUBLE:   b = static_cast<unsigned>(m_dval); break;
+    case PARAM_ZSTRING:  b = get_zstring().hash(); break;
     case PARAM_EXTERNAL: b = m_ext_id; break;
     }
     return (b << 2) | m_kind;
@@ -124,6 +130,7 @@ std::ostream& parameter::display(std::ostream& out) const {
     case PARAM_AST:      return out << "#" << get_ast()->get_id();
     case PARAM_DOUBLE:   return out << m_dval;
     case PARAM_EXTERNAL: return out << "@" << m_ext_id;
+    case PARAM_ZSTRING:  return out << get_zstring();
     default:
         UNREACHABLE();
         return out << "[invalid parameter]";

src/ast/ast.h

@@ -22,6 +22,7 @@ Revision History:
 #include "util/vector.h"
 #include "util/hashtable.h"
 #include "util/buffer.h"
+#include "util/zstring.h"
 #include "util/symbol.h"
 #include "util/rational.h"
 #include "util/hash.h"
@@ -100,6 +101,7 @@ public:
         PARAM_INT,
         PARAM_AST,
         PARAM_SYMBOL,
+        PARAM_ZSTRING,
         PARAM_RATIONAL,
         PARAM_DOUBLE,
         // PARAM_EXTERNAL is used for handling decl_plugin specific parameters.
@@ -119,6 +121,7 @@ private:
         ast*         m_ast;     // for PARAM_AST
         symbol       m_symbol;  // for PARAM_SYMBOL
         rational*    m_rational; // for PARAM_RATIONAL
+        zstring*     m_zstring;  // for PARAM_ZSTRING
         double       m_dval;   // for PARAM_DOUBLE (remark: this is not used in float_decl_plugin)
         unsigned     m_ext_id; // for PARAM_EXTERNAL
     };
@@ -132,6 +135,8 @@ public:
     explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL), m_symbol(s) {}
     explicit parameter(rational const & r): m_kind(PARAM_RATIONAL), m_rational(alloc(rational, r)) {}
     explicit parameter(rational && r) : m_kind(PARAM_RATIONAL), m_rational(alloc(rational, std::move(r))) {} 
+    explicit parameter(zstring const& s): m_kind(PARAM_ZSTRING), m_zstring(alloc(zstring, s)) {}
+    explicit parameter(zstring && s): m_kind(PARAM_ZSTRING), m_zstring(alloc(zstring, std::move(s))) {}
     explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {}
     explicit parameter(const char *s):m_kind(PARAM_SYMBOL), m_symbol(symbol(s)) {}
     explicit parameter(const std::string &s):m_kind(PARAM_SYMBOL), m_symbol(symbol(s)) {}
@@ -146,6 +151,7 @@ public:
         case PARAM_RATIONAL: m_rational = nullptr; std::swap(m_rational, other.m_rational); break;
         case PARAM_DOUBLE: m_dval = other.m_dval; break;
         case PARAM_EXTERNAL: m_ext_id = other.m_ext_id; break;
+        case PARAM_ZSTRING: m_zstring = other.m_zstring; break;
         default:
             UNREACHABLE();
             break;
@@ -163,6 +169,7 @@ public:
     bool is_rational() const { return m_kind == PARAM_RATIONAL; }
     bool is_double() const { return m_kind == PARAM_DOUBLE; }
     bool is_external() const { return m_kind == PARAM_EXTERNAL; }
+    bool is_zstring() const { return m_kind == PARAM_ZSTRING; }
 
     bool is_int(int & i) const { return is_int() && (i = get_int(), true); }
     bool is_ast(ast * & a) const { return is_ast() && (a = get_ast(), true); }
@@ -170,6 +177,7 @@ public:
     bool is_rational(rational & r) const { return is_rational() && (r = get_rational(), true); }
     bool is_double(double & d) const { return is_double() && (d = get_double(), true); }
     bool is_external(unsigned & id) const { return is_external() && (id = get_ext_id(), true); }
+    bool is_zstring(zstring& s) const { return is_zstring() && (s = get_zstring(), true); }
 
     /**
        \brief This method is invoked when the parameter is
@@ -187,6 +195,7 @@ public:
     ast * get_ast() const { SASSERT(is_ast()); return m_ast; }
     symbol get_symbol() const { SASSERT(is_symbol()); return m_symbol; }
     rational const & get_rational() const { SASSERT(is_rational()); return *m_rational; }
+    zstring const& get_zstring() const { SASSERT(is_zstring()); return *m_zstring; }
     double get_double() const { SASSERT(is_double()); return m_dval; }
     unsigned get_ext_id() const { SASSERT(is_external()); return m_ext_id; }
 

src/ast/ast_lt.cpp

@@ -23,6 +23,7 @@ Revision History:
 #define check_bool(B1,B2) if (B1 != B2) return !B1 && B2
 #define check_ptr(P1,P2) if (!P1 && P2) return true; if (P1 && !P2) return false
 #define check_ast(T1,T2) if (T1 != T2) { n1 = T1; n2 = T2; goto start; }
+#define check_zstring(S1, S2) if (S1 != S2) return S1 < S2
 
 #define check_parameter(p1, p2) {                               \
     check_value(p1.get_kind(), p2.get_kind());                  \
@@ -45,6 +46,9 @@ Revision History:
     case parameter::PARAM_EXTERNAL:                             \
         check_value(p1.get_ext_id(), p2.get_ext_id());          \
         break;                                                  \
+    case parameter::PARAM_ZSTRING:                              \
+        check_zstring(p1.get_zstring(), p2.get_zstring());      \
+        break;                                                  \
     default:                                                    \
         UNREACHABLE();                                          \
         break;                                                  \

src/ast/rewriter/seq_axioms.cpp

@@ -682,7 +682,7 @@ namespace seq {
         // itos(n) does not start with "0" when n > 0
         // n = 0 or at(itos(n),0) != "0"
         // alternative: n >= 0 => itos(stoi(itos(n))) = itos(n)
-        expr_ref zs(seq.str.mk_string(symbol("0")), m);
+        expr_ref zs(seq.str.mk_string("0"), m);
         m_rewrite(zs);
         expr_ref eq0 = mk_eq(n, zero);
         expr_ref at0 = mk_eq(seq.str.mk_at(e, zero), zs);

src/ast/rewriter/seq_rewriter.cpp

@@ -2159,7 +2159,7 @@ br_status seq_rewriter::mk_str_from_code(expr* a, expr_ref& result) {
     rational r;
     if (m_autil.is_numeral(a, r)) {
         if (r.is_neg() || r > u().max_char()) {
-            result = str().mk_string(symbol(""));
+            result = str().mk_string(zstring());
         }
         else {
             unsigned num = r.get_unsigned();
@@ -2207,10 +2207,10 @@ br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) {
     rational r;
     if (m_autil.is_numeral(a, r)) {
         if (r.is_int() && !r.is_neg()) {
-            result = str().mk_string(symbol(r.to_string()));
+            result = str().mk_string(zstring(r));
         }
         else {
-            result = str().mk_string(symbol(""));
+            result = str().mk_string(zstring());
         }
         return BR_DONE;
     }
@@ -2225,7 +2225,7 @@ br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) {
             eqs.push_back(m().mk_eq(b, str().mk_string(s)));
         }
         result = m().mk_or(eqs);
-        result = m().mk_ite(result, b, str().mk_string(symbol("")));
+        result = m().mk_ite(result, b, str().mk_string(zstring()));
         return BR_REWRITE2;
     }
     return BR_FAILED;
@@ -4884,13 +4884,17 @@ bool seq_rewriter::reduce_itos(expr_ref_vector& ls, expr_ref_vector& rs,
         str().is_itos(ls.get(0), n) &&
         is_string(rs.size(), rs.data(), s)) {
         std::string s1 = s.encode();
-        rational r(s1.c_str());
+        try {
-        if (s1 == r.to_string()) {
+            rational r(s1.c_str());
-            eqs.push_back(n, m_autil.mk_numeral(r, true));
+            if (s1 == r.to_string()) {
-            ls.reset(); 
+                eqs.push_back(n, m_autil.mk_numeral(r, true));
-            rs.reset();
+                ls.reset();
-            return true;
+                rs.reset();
+                return true;
+            }
         }
+        catch (...)
+        { }
     }
     return true;
 }

src/ast/seq_decl_plugin.cpp

@@ -375,7 +375,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_SEQ_EMPTY:
         match(*m_sigs[k], arity, domain, range, rng);
         if (rng == m_string) {
-            parameter param(symbol(""));
+            parameter param(zstring(""));
             return mk_func_decl(OP_STRING_CONST, 1, &param, 0, nullptr, m_string);
         }
         else {
@@ -474,7 +474,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         m.raise_exception("Incorrect arguments used for re.^. Expected one non-negative integer parameter");
 
     case OP_STRING_CONST:
-        if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) {
+        if (!(num_parameters == 1 && arity == 0 && parameters[0].is_zstring())) {
             m.raise_exception("invalid string declaration");
         }
         return m.mk_const_decl(m_stringc_sym, m_string,
@@ -503,7 +503,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         if (!(num_parameters == 1 && parameters[0].is_int())) 
             m.raise_exception("character literal expects integer parameter");
         zstring zs(parameters[0].get_int());        
-        parameter p(zs.encode());
+        parameter p(zs);
         return m.mk_const_decl(m_stringc_sym, m_string,func_decl_info(m_family_id, OP_STRING_CONST, 1, &p));
     }
         
@@ -630,16 +630,8 @@ void seq_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol
     sort_names.push_back(builtin_name("StringSequence", _STRING_SORT));
 }
 
-app* seq_decl_plugin::mk_string(symbol const& s) {
-    parameter param(s);
-    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);
-}
-
 app* seq_decl_plugin::mk_string(zstring const& s) {
-    symbol sym(s.encode());
+    parameter param(s);
-    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);
@@ -792,7 +784,7 @@ app* seq_util::mk_lt(expr* ch1, expr* ch2) const {
 
 bool seq_util::str::is_string(func_decl const* f, zstring& s) const {
     if (is_string(f)) {
-        s = zstring(f->get_parameter(0).get_symbol().bare_str());
+        s = f->get_parameter(0).get_zstring();
         return true;
     }
     else {

src/ast/seq_decl_plugin.h

@@ -191,7 +191,6 @@ public:
     unsigned max_char() const { return get_char_plugin().max_char(); }
     unsigned num_bits() const { return get_char_plugin().num_bits(); }
 
-    app* mk_string(symbol const& s);
     app* mk_string(zstring const& s);
     app* mk_char(unsigned ch);
 
@@ -262,9 +261,6 @@ public:
         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) {}
@@ -273,7 +269,6 @@ public:
         sort* mk_string_sort() const { return m.mk_sort(m_fid, _STRING_SORT, 0, nullptr); }
         app* mk_empty(sort* s) const { return m.mk_const(m.mk_func_decl(m_fid, OP_SEQ_EMPTY, 0, nullptr, 0, (expr*const*)nullptr, s)); }
         app* mk_string(zstring const& s) const;
-        app* mk_string(symbol const& s) const { return u.seq.mk_string(s); }
         app* mk_char(unsigned ch) const;
         app* mk_concat(expr* a, expr* b) const { 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) const { return mk_concat(a, mk_concat(b, c)); }
@@ -313,14 +308,12 @@ public:
         bool is_skolem(func_decl const* f)      const { return is_decl_of(f, m_fid, _OP_SEQ_SKOLEM); }
 
         bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); }
-        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(func_decl const* f) const { return is_decl_of(f, m_fid, OP_STRING_CONST); }
         bool is_string(expr const* n, zstring& s) const;
         bool is_string(func_decl const* f, zstring& s) const;
-        bool is_empty(expr const* n) const { symbol s;
+        bool is_empty(expr const* n) const {
-            return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0);
+            zstring s;
+            return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && s.empty());
         }
         bool is_concat(expr const* n)   const { return is_app_of(n, m_fid, OP_SEQ_CONCAT); }
         bool is_length(expr const* n)   const { return is_app_of(n, m_fid, OP_SEQ_LENGTH); }

src/cmd_context/simplify_cmd.cpp

@@ -104,7 +104,7 @@ public:
             ctx.display(ctx.regular_stream(), r);
             ctx.regular_stream() << std::endl; 
         }
-        if (!failed && m_params.get_bool("print_proofs", false)) {
+        if (!failed && m_params.get_bool("print_proofs", false) && pr.get()) {
             ast_smt_pp pp(ctx.m());
             pp.set_logic(ctx.get_logic());
             pp.display_expr_smt2(ctx.regular_stream(), pr.get());

src/math/lp/lar_solver.cpp

@@ -1719,7 +1719,7 @@ namespace lp {
 
     void lar_solver::subst_known_terms(lar_term* t) {
         std::set<unsigned> seen_terms;
-        for (const auto&p : *t) {
+        for (auto p : *t) {
             auto j = p.column();
             if (this->column_corresponds_to_term(j)) {
                 seen_terms.insert(j);
@@ -1730,10 +1730,10 @@ namespace lp {
             seen_terms.erase(j);
             auto tj = this->m_var_register.local_to_external(j);
             auto& ot = this->get_term(tj);
-            for(const auto&  p : ot){
+            for (auto p : ot){
-              if (this->column_corresponds_to_term(p.column())) {
+                if (this->column_corresponds_to_term(p.column())) {
-                 seen_terms.insert(p.column());
+                    seen_terms.insert(p.column());
-              }   
+                }   
             }
             t->subst_by_term(ot, j);
         }

src/math/lp/lar_term.h

@@ -62,13 +62,13 @@ public:
         if (it == nullptr) return;
         mpq a = it->get_data().m_value;
         this->m_coeffs.erase(term_column);
-        for (const auto & p : t) {
+        for (auto p : t) {
             this->add_monomial(a * p.coeff(), p.column());
         }
     }
 
     lar_term(const vector<std::pair<mpq, unsigned>>& coeffs) {
-        for (const auto & p : coeffs) {
+        for (auto const& p : coeffs) {
             add_monomial(p.first, p.second);
         }
     }

src/model/seq_factory.h

@@ -67,8 +67,8 @@ public:
     }
     bool get_some_values(sort* s, expr_ref& v1, expr_ref& v2) override {
         if (u.is_string(s)) {
-            v1 = u.str.mk_string(symbol("a"));
+            v1 = u.str.mk_string("a");
-            v2 = u.str.mk_string(symbol("b"));
+            v2 = u.str.mk_string("b");
             return true;
         }
         sort* ch;
@@ -94,10 +94,11 @@ public:
             while (true) {
                 std::ostringstream strm;
                 strm << m_unique_delim << std::hex << m_next++ << std::dec << m_unique_delim;
-                symbol sym(strm.str());
+                std::string s(strm.str());
+                symbol sym(s);
                 if (m_strings.contains(sym)) continue;
                 m_strings.insert(sym);
-                return u.str.mk_string(sym);
+                return u.str.mk_string(s);
             }
         }
         sort* seq = nullptr, *ch = nullptr;
@@ -131,8 +132,9 @@ public:
         return nullptr;
     }
     void register_value(expr* n) override {
-        symbol sym;
+        zstring s;
-        if (u.str.is_string(n, sym)) {
+        if (u.str.is_string(n, s)) {
+            symbol sym(s.encode());
             m_strings.insert(sym);
             if (sym.str().find(m_unique_delim) != std::string::npos) 
                 add_new_delim();

src/sat/smt/bv_internalize.cpp

@@ -563,7 +563,6 @@ namespace bv {
         SASSERT(e->get_num_args() >= 1);
         expr_ref_vector bits(m), new_bits(m), arg_bits(m);
         
-        unsigned i = e->get_num_args() - 1;
         get_arg_bits(e, 0, bits);
         for (unsigned i = 1; i < e->get_num_args(); ++i) {
             arg_bits.reset();

src/sat/smt/bv_solver.cpp

@@ -355,8 +355,6 @@ namespace bv {
             ctx.drat_eq_def(leq, eq);
         }
 
-        static unsigned s_count = 0;
-
         sat::literal_vector lits;
         switch (c.m_kind) {
         case bv_justification::kind_t::eq2bit:

src/smt/smt_case_split_queue.cpp

@@ -325,7 +325,7 @@ namespace {
         ast_manager &     m_manager;
         ptr_vector<expr>  m_queue;
         unsigned          m_head;
-        int               m_bs_num_bool_vars; //!< Number of boolean variable before starting to search.
+        bool_var          m_bs_num_bool_vars; //!< Number of boolean variable before starting to search.
         ptr_vector<expr>  m_queue2;
         unsigned          m_head2;
         svector<scope>    m_scopes;
@@ -513,7 +513,7 @@ namespace {
         smt_params &m_params;  
         ptr_vector<expr>  m_queue;
         unsigned          m_head;
-        int               m_bs_num_bool_vars; //!< Number of boolean variable before starting to search.
+        bool_var          m_bs_num_bool_vars; //!< Number of boolean variable before starting to search.
         bool_var_act_queue m_delayed_queue;
         svector<scope>    m_scopes;
     public:
@@ -745,7 +745,7 @@ namespace {
         ast_manager &        m_manager;
         ptr_vector<expr>     m_queue;
         unsigned             m_head;
-        int                  m_bs_num_bool_vars; //!< Number of boolean variable before starting to search.
+        bool_var             m_bs_num_bool_vars; //!< Number of boolean variable before starting to search.
         svector<queue_entry> m_queue2;
         svector<scope>       m_scopes;
         unsigned             m_current_generation;

src/smt/smt_context.cpp

@@ -1395,7 +1395,7 @@ namespace smt {
         SASSERT(get_bdata(v).is_enode());
         lbool val  = get_assignment(v);
         TRACE("propagate_bool_var_enode_bug", tout << "var: " << v << " #" << bool_var2expr(v)->get_id() << "\n";);
-        SASSERT(v < static_cast<int>(m_b_internalized_stack.size()));
+        SASSERT(v < m_b_internalized_stack.size());
         enode * n  = bool_var2enode(v);
 
         CTRACE("mk_bool_var", !n, tout << "No enode for " << v << "\n";);
@@ -1986,7 +1986,7 @@ namespace smt {
     void context::remove_lit_occs(clause const& cls, unsigned nbv) {
         if (!track_occs()) return;
         for (literal l : cls) {
-            if (l.var() < static_cast<int>(nbv)) 
+            if (l.var() < nbv) 
                 dec_ref(l);
         }
     }
@@ -2264,7 +2264,7 @@ namespace smt {
                     SASSERT(cls->get_num_atoms() == cls->get_num_literals());
                     for (unsigned j = 0; j < 2; j++) {
                         literal l           = cls->get_literal(j);
-                        if (l.var() < static_cast<int>(num_bool_vars)) {
+                        if (l.var() < num_bool_vars) {
                             // This boolean variable was not deleted during backtracking
                             //
                             // So, it is still a watch literal. I remove the watch, since
@@ -4096,7 +4096,7 @@ namespace smt {
                 expr * * atoms         = m_conflict_resolution->get_lemma_atoms();
                 for (unsigned i = 0; i < num_lits; i++) {
                     literal l   = lits[i];
-                    if (l.var() >= static_cast<int>(num_bool_vars)) {
+                    if (l.var() >= num_bool_vars) {
                         // This boolean variable was deleted during backtracking, it need to be recreated.
                         // Remark: atom may be a negative literal (not a). Z3 creates Boolean variables for not-gates that
                         // are nested in terms. Example: let f be a uninterpreted function from Bool -> Int.

src/smt/smt_context_inv.cpp

@@ -263,7 +263,7 @@ namespace smt {
     */
     bool context::check_th_diseq_propagation() const {
         TRACE("check_th_diseq_propagation", tout << "m_propagated_th_diseqs.size() " << m_propagated_th_diseqs.size() << "\n";);
-        int num = get_num_bool_vars();
+        unsigned num = get_num_bool_vars();
         if (inconsistent() || get_manager().limit().is_canceled()) {
             return true;
         }

src/smt/smt_context_pp.cpp

@@ -296,7 +296,7 @@ namespace smt {
 
     void context::display_hot_bool_vars(std::ostream & out) const {
         out << "hot bool vars:\n";
-        int num = get_num_bool_vars();
+        unsigned num = get_num_bool_vars();
         for (bool_var v = 0; v < num; v++) {
             double val = get_activity(v)/m_bvar_inc;
             if (val > 10.00) {

src/smt/smt_types.h

@@ -22,6 +22,7 @@ Revision History:
 #include "util/vector.h"
 #include "util/hashtable.h"
 #include "util/lbool.h"
+#include "util/sat_literal.h"
 
 class model;
 
@@ -29,9 +30,9 @@ namespace smt {
     /**
        \brief A boolean variable is just an integer.
     */
-    typedef int bool_var;
+    typedef sat::bool_var bool_var;
     
-    const bool_var null_bool_var  = -1;
+    const bool_var null_bool_var  = sat::null_bool_var;
     const bool_var true_bool_var  = 0;
     const bool_var first_bool_var = 1;
     

src/smt/theory_str.cpp

@@ -190,8 +190,7 @@ namespace smt {
     }
 
     expr * theory_str::mk_string(const char * str) {
-        symbol sym(str);
+        return u.str.mk_string(str);
-        return u.str.mk_string(sym);
     }
 
     void theory_str::collect_statistics(::statistics & st) const {

src/smt/theory_str.h

@@ -53,11 +53,11 @@ public:
         u(m), delim("!"), m_next(0) {}
     ~str_value_factory() override {}
     expr * get_some_value(sort * s) override {
-        return u.str.mk_string(symbol("some value"));
+        return u.str.mk_string("some value");
     }
     bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) override {
-        v1 = u.str.mk_string(symbol("value 1"));
+        v1 = u.str.mk_string("value 1");
-        v2 = u.str.mk_string(symbol("value 2"));
+        v2 = u.str.mk_string("value 2");
         return true;
     }
     expr * get_fresh_value(sort * s) override {
@@ -65,10 +65,11 @@ public:
             while (true) {
                 std::ostringstream strm;
                 strm << delim << std::hex << (m_next++) << std::dec << delim;
-                symbol sym(strm.str());
+                std::string s(strm.str());
+                symbol sym(s);
                 if (m_strings.contains(sym)) continue;
                 m_strings.insert(sym);
-                return u.str.mk_string(sym);
+                return u.str.mk_string(s);
             }
         }
         sort* seq = nullptr;

src/smt/theory_str_mc.cpp

@@ -1337,9 +1337,8 @@ namespace smt {
                             rw(arg_subst);
                             TRACE("str_fl", tout << "ival = " << ival << ", string arg evaluates to " << mk_pp(arg_subst, m) << std::endl;);
 
-                            symbol arg_str;
+                            zstring arg_zstr;
-                            if (u.str.is_string(arg_subst, arg_str)) {
+                            if (u.str.is_string(arg_subst, arg_zstr)) {
-                                zstring arg_zstr(arg_str.bare_str());
                                 rational arg_value;
                                 if (string_integer_conversion_valid(arg_zstr, arg_value)) {
                                     if (ival != arg_value) {
@@ -1365,9 +1364,8 @@ namespace smt {
                             (*replacer)(arg, arg_subst);
                             rw(arg_subst);
                             TRACE("str_fl", tout << "ival = " << ival << ", string arg evaluates to " << mk_pp(arg_subst, m) << std::endl;);
-                            symbol arg_str;
+                            zstring arg_zstr;
-                            if (u.str.is_string(arg_subst, arg_str)) {
+                            if (u.str.is_string(arg_subst, arg_zstr)) {
-                                zstring arg_zstr(arg_str.bare_str());
                                 if (ival >= rational::zero() && ival <= rational(u.max_char())) {
                                     // check that arg_subst has length 1 and that the codepoints are the same
                                     if (arg_zstr.length() != 1 || rational(arg_zstr[0]) != ival) {
@@ -1396,9 +1394,8 @@ namespace smt {
                             rw(e_subst);
                             TRACE("str_fl", tout << "ival = " << ival << ", string arg evaluates to " << mk_pp(e_subst, m) << std::endl;);
 
-                            symbol e_str;
+                            zstring e_zstr;
-                            if (u.str.is_string(e_subst, e_str)) {
+                            if (u.str.is_string(e_subst, e_zstr)) {
-                                zstring e_zstr(e_str.bare_str());
                                 // if arg is negative, e must be empty
                                 // if arg is non-negative, e must be valid AND cannot contain leading zeroes
 
@@ -1436,9 +1433,8 @@ namespace smt {
                             (*replacer)(e, e_subst);
                             rw(e_subst);
                             TRACE("str_fl", tout << "ival = " << ival << ", string arg evaluates to " << mk_pp(e_subst, m) << std::endl;);
-                            symbol e_str;
+                            zstring e_zstr;
-                            if (u.str.is_string(e_subst, e_str)) {
+                            if (u.str.is_string(e_subst, e_zstr)) {
-                                zstring e_zstr(e_str.bare_str());
                                 // if arg is out of range, e must be empty
                                 // if arg is in range, e must be valid
                                 if (ival <= rational::zero() || ival >= rational(u.max_char())) {

src/tactic/arith/recover_01_tactic.cpp

@@ -307,8 +307,7 @@ class recover_01_tactic : public tactic {
             new_goal->add(g->mc());
             new_goal->add(g->pc());
 
-            unsigned sz = g->size();
+            for (unsigned i = 0; i < g->size(); i++) {
-            for (unsigned i = 0; i < sz; i++) {
                 expr * f = g->form(i);
                 if (save_clause(f)) {
                     saved = true;
@@ -356,8 +355,7 @@ class recover_01_tactic : public tactic {
             m_rw.set_substitution(subst);
             expr_ref   new_curr(m);
             proof_ref  new_pr(m);
-            unsigned size = new_goal->size();
+            for (unsigned idx = 0; idx < new_goal->size(); idx++) {
-            for (unsigned idx = 0; idx < size; idx++) {
                 expr * curr = new_goal->form(idx);
                 m_rw(curr, new_curr);
                 new_goal->update(idx, new_curr);

src/tactic/core/symmetry_reduce_tactic.cpp

@@ -338,10 +338,8 @@ private:
         app_parents const& get_parents() { return m_use_funs; }
 
         void operator()(app* n) {
-            func_decl* f;
+            func_decl* f = n->get_decl();
-            unsigned sz = n->get_num_args();
+            for (expr* e : *n) {
-            for (unsigned i = 0; i < sz; ++i) {
-                expr* e = n->get_arg(i);
                 if (is_app(e)) {
                     auto& value = m_use_funs.insert_if_not_there(to_app(e), 0);
                     if (!value) value = alloc(fun_set);

src/util/zstring.cpp

@@ -87,6 +87,7 @@ zstring::zstring(char const* s) {
     SASSERT(well_formed());
 }
 
+
 bool zstring::uses_unicode() const {
     return gparams::get_value("unicode") != "false";
 }
@@ -234,12 +235,17 @@ zstring zstring::extract(unsigned offset, unsigned len) const {
     return result;
 }
 
+unsigned zstring::hash() const {
+    return unsigned_ptr_hash(m_buffer.data(), m_buffer.size(), 23);
+}
+
 zstring zstring::operator+(zstring const& other) const {
     zstring result(*this);
     result.m_buffer.append(other.m_buffer);
     return result;
 }
 
+
 bool zstring::operator==(const zstring& other) const {
     // two strings are equal iff they have the same length and characters
     if (length() != other.length()) {

src/util/zstring.h

@@ -19,6 +19,7 @@ Author:
 #include <string>
 #include "util/vector.h"
 #include "util/buffer.h"
+#include "util/rational.h"
 
 class zstring {
 private:
@@ -34,6 +35,7 @@ public:
     zstring() {}
     zstring(char const* s);
     zstring(const std::string &str) : zstring(str.c_str()) {}
+    zstring(rational const& r): zstring(r.to_string()) {}
     zstring(unsigned sz, unsigned const* s) { m_buffer.append(sz, s); SASSERT(well_formed()); }
     zstring(unsigned ch);
     zstring replace(zstring const& src, zstring const& dst) const;
@@ -51,6 +53,7 @@ public:
     zstring operator+(zstring const& other) const;
     bool operator==(const zstring& other) const;
     bool operator!=(const zstring& other) const;
+    unsigned hash() const;
 
     friend std::ostream& operator<<(std::ostream &os, const zstring &str);
     friend bool operator<(const zstring& lhs, const zstring& rhs);