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

src/api/api_ast.cpp

@@ -1124,6 +1124,20 @@ extern "C" {
             case OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE;
             case OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE;
 
+            case _OP_STRING_STRREPL: return Z3_OP_SEQ_REPLACE;
+            case _OP_STRING_CONCAT: return Z3_OP_SEQ_CONCAT;
+            case _OP_STRING_LENGTH: return Z3_OP_SEQ_LENGTH;
+            case _OP_STRING_STRCTN: return Z3_OP_SEQ_CONTAINS;
+            case _OP_STRING_PREFIX: return Z3_OP_SEQ_PREFIX;
+            case _OP_STRING_SUFFIX: return Z3_OP_SEQ_SUFFIX;
+            case _OP_STRING_IN_REGEXP: return Z3_OP_SEQ_IN_RE;
+            case _OP_STRING_TO_REGEXP: return Z3_OP_SEQ_TO_RE;
+            case _OP_STRING_CHARAT: return Z3_OP_SEQ_AT;
+            case _OP_STRING_SUBSTR: return Z3_OP_SEQ_EXTRACT;
+            case _OP_STRING_STRIDOF: return Z3_OP_SEQ_INDEX;
+            case _OP_REGEXP_EMPTY: return Z3_OP_RE_EMPTY_SET;
+            case _OP_REGEXP_FULL: return Z3_OP_RE_FULL_SET;
+
             case OP_STRING_STOI: return Z3_OP_STR_TO_INT;
             case OP_STRING_ITOS: return Z3_OP_INT_TO_STR;
 

src/api/dotnet/Expr.cs

@@ -797,6 +797,22 @@ namespace Microsoft.Z3
         public bool IsLabelLit { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } }
         #endregion
 
+        #region Sequences and Strings
+
+        /// <summary>
+        /// Check whether expression is a string constant.
+        /// </summary>
+        /// <returns>a Boolean</returns>
+        public bool IsString  { get { return IsApp && 0 != Native.Z3_is_string(Context.nCtx, NativeObject); } }
+
+        /// <summary>
+        /// Retrieve string corresponding to string constant.
+        /// </summary>
+        /// <remarks>the expression should be a string constant, (IsString should be true).</remarks>
+        public string String { get { return Native.Z3_get_string(Context.nCtx, NativeObject); } }        
+
+        #endregion
+
         #region Proof Terms
         /// <summary>
         /// Indicates whether the term is a binary equivalence modulo namings.

src/api/dotnet/Model.cs

@@ -19,6 +19,7 @@ Notes:
 
 using System;
 using System.Diagnostics.Contracts;
+using System.Collections.Generic;
 
 namespace Microsoft.Z3
 {
@@ -131,6 +132,24 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// Enumerate constants in model.
+        /// </summary>
+        public IEnumerable<KeyValuePair<FuncDecl, Expr>> Consts
+        {
+            get
+            {
+                uint nc = NumConsts;
+                for (uint i = 0; i < nc; ++i)
+                {
+                    var f = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
+                    IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);
+                    if (n == IntPtr.Zero) continue;
+                    yield return new KeyValuePair<FuncDecl, Expr>(f, Expr.Create(Context, n));
+                }
+            }
+        }
+
         /// <summary>
         /// The number of function interpretations in the model.
         /// </summary>

src/api/java/Expr.java

@@ -126,7 +126,7 @@ public class Expr extends AST
         if (isApp() && args.length != getNumArgs()) {
             throw new Z3Exception("Number of arguments does not match");
         }
-        return new Expr(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(),
+        return Expr.create(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(),
                 args.length, Expr.arrayToNative(args)));
     }
 
@@ -1277,6 +1277,26 @@ public class Expr extends AST
         return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL_LIT;
     }
 
+    /**
+     * Check whether expression is a string constant.
+     * @return a boolean
+     */
+    public boolean isString() 
+    {
+        return isApp() && Native.isString(getContext().nCtx(), getNativeObject());
+    }
+
+    /**
+     * Retrieve string corresponding to string constant.
+     * Remark: the expression should be a string constant, (isString() should return true).
+     * @throws Z3Exception on error
+     * @return a string
+     */
+    public String getString()
+    {
+	return Native.getString(getContext().nCtx(), getNativeObject());
+    }
+
     /**
      * Indicates whether the term is a binary equivalence modulo namings.
      * Remarks: This binary predicate is used in proof terms. It captures

src/sat/sat_solver/inc_sat_solver.cpp

@@ -130,13 +130,36 @@ public:
         m_solver.display_wcnf(out, m_asms.size(), m_asms.c_ptr(), nweights.c_ptr());
     }
 
+    bool is_literal(expr* e) const {
+        return 
+            is_uninterp_const(e) ||
+            (m.is_not(e, e) && is_uninterp_const(e));
+    }
+
     virtual lbool check_sat(unsigned sz, expr * const * assumptions) {
         m_solver.pop_to_base_level();
+        expr_ref_vector _assumptions(m);
+        obj_map<expr, expr*> asm2fml;
+        for (unsigned i = 0; i < sz; ++i) {
+            if (!is_literal(assumptions[i])) {
+                expr_ref a(m.mk_fresh_const("s", m.mk_bool_sort()), m);
+                expr_ref fml(m.mk_eq(a, assumptions[i]), m);
+                assert_expr(fml);
+                _assumptions.push_back(a);
+                asm2fml.insert(a, assumptions[i]);
+            }
+            else {
+                _assumptions.push_back(assumptions[i]);
+                asm2fml.insert(assumptions[i], assumptions[i]);
+            }
+        }
+        
+        TRACE("sat", tout << _assumptions << "\n";);
         dep2asm_t dep2asm;
         m_model = 0;
         lbool r = internalize_formulas();
         if (r != l_true) return r;
-        r = internalize_assumptions(sz, assumptions, dep2asm);
+        r = internalize_assumptions(sz, _assumptions.c_ptr(), dep2asm);
         if (r != l_true) return r;
 
         r = m_solver.check(m_asms.size(), m_asms.c_ptr());
@@ -150,7 +173,7 @@ public:
         case l_false:
             // TBD: expr_dependency core is not accounted for.
             if (!m_asms.empty()) {
-                extract_core(dep2asm);
+                extract_core(dep2asm, asm2fml);
             }
             break;
         default:
@@ -241,6 +264,7 @@ public:
         sat::bool_var_vector bvars;
         vector<sat::literal_vector> lconseq;
         dep2asm_t dep2asm;
+        obj_map<expr, expr*> asm2fml;
         m_solver.pop_to_base_level();
         lbool r = internalize_formulas();
         if (r != l_true) return r;
@@ -251,7 +275,7 @@ public:
         r = m_solver.get_consequences(m_asms, bvars, lconseq);
         if (r == l_false) {
             if (!m_asms.empty()) {
-                extract_core(dep2asm);
+                extract_core(dep2asm, asm2fml);
             }
             return r;
         }
@@ -302,7 +326,6 @@ public:
         return l_true;
     }
 
-
     virtual std::string reason_unknown() const {
         return m_unknown;
     }
@@ -569,7 +592,7 @@ private:
         }
     }
 
-    void extract_core(dep2asm_t& dep2asm) {
+    void extract_core(dep2asm_t& dep2asm, obj_map<expr, expr*> const& asm2fml) {
         u_map<expr*> asm2dep;
         extract_asm2dep(dep2asm, asm2dep);
         sat::literal_vector const& core = m_solver.get_core();
@@ -590,6 +613,9 @@ private:
         for (unsigned i = 0; i < core.size(); ++i) {
             expr* e = 0;
             VERIFY(asm2dep.find(core[i].index(), e));
+            if (asm2fml.contains(e)) {
+                e = asm2fml.find(e);
+            }
             m_core.push_back(e);
         }
     }

src/smt/theory_lra.cpp

@@ -487,7 +487,7 @@ namespace smt {
                 result = m_theory_var2var_index[v];
             }
             if (result == UINT_MAX) {
-                result = m_solver->add_var(v);
+                result = m_solver->add_var(v); // TBD: is_int(v);
                 m_theory_var2var_index.setx(v, result, UINT_MAX);
                 m_var_index2theory_var.setx(result, v, UINT_MAX);
                 m_var_trail.push_back(v);

src/smt/theory_str.cpp

@@ -25,6 +25,7 @@
 #include<algorithm>
 #include"theory_seq_empty.h"
 #include"theory_arith.h"
+#include"ast_util.h"
 
 namespace smt {
     
@@ -98,7 +99,7 @@ namespace smt {
         if (defaultCharset) {
             // valid C strings can't contain the null byte ('\0')
             charSetSize = 255;
-            char_set = alloc_svect(char, charSetSize);
+            char_set.resize(256, 0);            
             int idx = 0;
             // small letters
             for (int i = 97; i < 123; i++) {
@@ -157,8 +158,7 @@ namespace smt {
         } else {
             const char setset[] = { 'a', 'b', 'c' };
             int fSize = sizeof(setset) / sizeof(char);
-
+            char_set.resize(fSize, 0);
-            char_set = alloc_svect(char, fSize);
             charSetSize = fSize;
             for (int i = 0; i < charSetSize; i++) {
                 char_set[i] = setset[i];
@@ -494,6 +494,7 @@ namespace smt {
 
         sort * string_sort = u.str.mk_string_sort();
         app * a = mk_fresh_const(name.c_str(), string_sort);
+        m_trail.push_back(a);
 
         TRACE("str", tout << "a->get_family_id() = " << a->get_family_id() << std::endl
               << "this->get_family_id() = " << this->get_family_id() << std::endl;);
@@ -507,7 +508,6 @@ namespace smt {
         m_basicstr_axiom_todo.push_back(ctx.get_enode(a));
         TRACE("str", tout << "add " << mk_pp(a, m) << " to m_basicstr_axiom_todo" << std::endl;);
 
-        m_trail.push_back(a);
         variable_set.insert(a);
         internal_variable_set.insert(a);
         track_variable_scope(a);
@@ -521,6 +521,7 @@ namespace smt {
 
         sort * string_sort = u.str.mk_string_sort();
         app * a = mk_fresh_const("regex", string_sort);
+        m_trail.push_back(a);
 
         ctx.internalize(a, false);
         SASSERT(ctx.get_enode(a) != NULL);
@@ -529,7 +530,6 @@ namespace smt {
         m_basicstr_axiom_todo.push_back(ctx.get_enode(a));
         TRACE("str", tout << "add " << mk_pp(a, m) << " to m_basicstr_axiom_todo" << std::endl;);
 
-        m_trail.push_back(a);
         variable_set.insert(a);
         //internal_variable_set.insert(a);
         regex_variable_set.insert(a);
@@ -5563,7 +5563,7 @@ namespace smt {
                         if (arg0VecSize > 0 && arg1VecSize > 0 && u.str.is_string(arg0_grdItor->first[arg0VecSize - 1]) && u.str.is_string(arg1_grdItor->first[0])) {
                             ndVec.pop_back();
                             ndVec.push_back(mk_concat(arg0_grdItor->first[arg0VecSize - 1], arg1_grdItor->first[0]));
-                            for (int i = 1; i < arg1VecSize; i++) {
+                            for (size_t i = 1; i < arg1VecSize; i++) {
                                 ndVec.push_back(arg1_grdItor->first[i]);
                             }
                         } else {
@@ -5666,7 +5666,7 @@ namespace smt {
         if (subStrCnt == 1) {
             zstring subStrVal;
             if (u.str.is_string(subStrVec[0], subStrVal)) {
-                for (int i = 0; i < strCnt; i++) {
+                for (size_t i = 0; i < strCnt; i++) {
                     zstring strVal;
                     if (u.str.is_string(strVec[i], strVal)) {
                         if (strVal.contains(subStrVal)) {
@@ -5675,7 +5675,7 @@ namespace smt {
                     }
                 }
             } else {
-                for (int i = 0; i < strCnt; i++) {
+                for (size_t i = 0; i < strCnt; i++) {
                     if (strVec[i] == subStrVec[0]) {
                         return true;
                     }
@@ -5683,7 +5683,7 @@ namespace smt {
             }
             return false;
         } else {
-            for (int i = 0; i <= (strCnt - subStrCnt); i++) {
+            for (size_t i = 0; i <= (strCnt - subStrCnt); i++) {
                 // The first node in subStrVect should be
                 //   * constant: a suffix of a note in strVec[i]
                 //   * variable:
@@ -5712,7 +5712,7 @@ namespace smt {
 
                 // middle nodes
                 bool midNodesOK = true;
-                for (int j = 1; j < subStrCnt - 1; j++) {
+                for (size_t j = 1; j < subStrCnt - 1; j++) {
                     if (subStrVec[j] != strVec[i + j]) {
                         midNodesOK = false;
                         break;
@@ -6927,9 +6927,9 @@ namespace smt {
         ast_manager & m = get_manager();
         if (lenTester_fvar_map.contains(lenTester)) {
             expr * fVar = lenTester_fvar_map[lenTester];
-            expr * toAssert = gen_len_val_options_for_free_var(fVar, lenTester, lenTesterValue);
+			expr_ref toAssert(gen_len_val_options_for_free_var(fVar, lenTester, lenTesterValue), m);
             TRACE("str", tout << "asserting more length tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;);
-            if (toAssert != NULL) {
+            if (toAssert) {
                 assert_axiom(toAssert);
             }
         }
@@ -9123,7 +9123,7 @@ namespace smt {
 
     zstring theory_str::gen_val_string(int len, int_vector & encoding) {
         SASSERT(charSetSize > 0);
-        SASSERT(char_set != NULL);
+        SASSERT(!char_set.empty());
 
         std::string re(len, char_set[0]);
         for (int i = 0; i < (int) encoding.size() - 1; i++) {
@@ -9240,8 +9240,7 @@ namespace smt {
 
         // ----------------------------------------------------------------------------------------
         
-        ptr_vector<expr> orList;
+        expr_ref_vector orList(m), andList(m);
-        ptr_vector<expr> andList;
 
         for (long long i = l; i < h; i++) {
             orList.push_back(m.mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()) ));
@@ -9262,7 +9261,7 @@ namespace smt {
             } else {
                 strAst = mk_string(aStr);
             }
-            andList.push_back(m.mk_eq(orList[orList.size() - 1], m.mk_eq(freeVar, strAst)));
+            andList.push_back(m.mk_eq(orList[orList.size() - 1].get(), m.mk_eq(freeVar, strAst)));
         }
         if (!coverAll) {
             orList.push_back(m.mk_eq(val_indicator, mk_string("more")));
@@ -9273,21 +9272,8 @@ namespace smt {
             }
         }
 
-        expr ** or_items = alloc_svect(expr*, orList.size());
+        andList.push_back(mk_or(orList));
-        expr ** and_items = alloc_svect(expr*, andList.size() + 1);
+        expr_ref valTestAssert = mk_and(andList);
-
-        for (int i = 0; i < (int) orList.size(); i++) {
-            or_items[i] = orList[i];
-        }
-        if (orList.size() > 1)
-            and_items[0] = m.mk_or(orList.size(), or_items);
-        else
-            and_items[0] = or_items[0];
-
-        for (int i = 0; i < (int) andList.size(); i++) {
-            and_items[i + 1] = andList[i];
-        }
-        expr * valTestAssert = m.mk_and(andList.size() + 1, and_items);
 
         // ---------------------------------------
         // If the new value tester is $$_val_x_16_i
@@ -9300,20 +9286,9 @@ namespace smt {
             if (vTester != val_indicator)
                 andList.push_back(m.mk_eq(vTester, mk_string("more")));
         }
-        expr * assertL = NULL;
+        expr_ref assertL = mk_and(andList);
-        if (andList.size() == 1) {
-            assertL = andList[0];
-        } else {
-            expr ** and_items = alloc_svect(expr*, andList.size());
-            for (int i = 0; i < (int) andList.size(); i++) {
-                and_items[i] = andList[i];
-            }
-            assertL = m.mk_and(andList.size(), and_items);
-        }
-
         // (assertL => valTestAssert) <=> (!assertL OR valTestAssert)
-        valTestAssert = m.mk_or(m.mk_not(assertL), valTestAssert);
+        return m.mk_or(m.mk_not(assertL), valTestAssert);
-        return valTestAssert;
     }
 
     expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator,
@@ -9378,7 +9353,7 @@ namespace smt {
                           << " doesn't have an equivalence class value." << std::endl;);
                     refresh_theory_var(aTester);
 
-                    expr * makeupAssert = gen_val_options(freeVar, len_indicator, aTester, len_valueStr, i);
+                    expr_ref makeupAssert(gen_val_options(freeVar, len_indicator, aTester, len_valueStr, i), m);
 
                     TRACE("str", tout << "var: " << mk_ismt2_pp(freeVar, m) << std::endl
                           << mk_ismt2_pp(makeupAssert, m) << std::endl;);
@@ -9400,8 +9375,7 @@ namespace smt {
                     fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, valTester));
                     print_value_tester_list(fvar_valueTester_map[freeVar][len]);
                 }
-                expr * nextAssert = gen_val_options(freeVar, len_indicator, valTester, len_valueStr, i + 1);
+                return gen_val_options(freeVar, len_indicator, valTester, len_valueStr, i + 1);
-                return nextAssert;
             }
 
             return NULL;

src/smt/theory_str.h

@@ -330,7 +330,7 @@ protected:
 
     std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA
 
-    char * char_set;
+    svector<char> char_set;
     std::map<char, int>  charSetLookupTable;
     int           charSetSize;