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

VeriFIT · Jun 4, 2017 · a8ff97c · a8ff97c
2 parents 668bad6 + efd5727
commit a8ff97c
Showing 23 changed files with 193 additions and 124 deletions.
diff --git a/README-CMake.md b/README-CMake.md
@@ -1,4 +1,4 @@
-    # Z3's CMake build system
+# Z3's CMake build system
 
 [CMake](https://cmake.org/) is a "meta build system" that reads a description
 of the project written in the ``CMakeLists.txt`` files and emits a build

diff --git a/src/api/api_ast.cpp b/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;
 

diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs
@@ -797,6 +797,22 @@ public bool IsBV
         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.

diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs
@@ -19,6 +19,7 @@ Christoph Wintersteiger (cwinter) 2012-03-21
 
 using System;
 using System.Diagnostics.Contracts;
+using System.Collections.Generic;
 
 namespace Microsoft.Z3
 {
@@ -131,6 +132,24 @@ public FuncDecl[] ConstDecls
             }
         }
 
+        /// <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>

diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java
@@ -126,7 +126,7 @@ public Expr update(Expr[] args)
         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 boolean isLabelLit()
         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

diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
@@ -935,9 +935,9 @@ bool datatype_util::is_recursive(sort * ty) {
 
 
 bool datatype_util::is_enum_sort(sort* s) {
-	if (!is_datatype(s)) {
-		return false;
-	}
+    if (!is_datatype(s)) {
+        return false;
+    }
     bool r = false;
     if (m_is_enum.find(s, r))
         return r;

diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp
@@ -143,11 +143,11 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
         case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE;
         case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE;
         case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE;
-		case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: m_conv.mk_to_ubv_unspecified(f, num, args, result); return BR_DONE;
+        case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: m_conv.mk_to_ubv_unspecified(f, num, args, result); return BR_DONE;
         case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
-		case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: m_conv.mk_to_sbv_unspecified(f, num, args, result); return BR_DONE;
+        case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: m_conv.mk_to_sbv_unspecified(f, num, args, result); return BR_DONE;
         case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
-		case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: m_conv.mk_to_real_unspecified(f, num, args, result); return BR_DONE;
+        case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: m_conv.mk_to_real_unspecified(f, num, args, result); return BR_DONE;
         case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
         case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: m_conv.mk_to_ieee_bv_unspecified(f, num, args, result); return BR_DONE;
 

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
@@ -92,25 +92,25 @@ class sym_expr_boolean_algebra : public boolean_algebra<sym_expr*> {
         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());
-			}
-		}
-
-		sort* s = x->get_sort();
-		if (m.is_bool(s)) s = y->get_sort();
-		var_ref v(m.mk_var(0, s), m);
-		expr_ref fml1 = x->accept(v);
-		expr_ref fml2 = y->accept(v);
-		if (m.is_true(fml1)) {
-			return y;
-		}
+    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());
+            }
+        }
+
+        sort* s = x->get_sort();
+        if (m.is_bool(s)) s = y->get_sort();
+        var_ref v(m.mk_var(0, s), 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());
@@ -178,10 +178,10 @@ class sym_expr_boolean_algebra : public boolean_algebra<sym_expr*> {
         return sym_expr::mk_pred(fml, x->get_sort());
     }
 
-	/*virtual vector<std::pair<vector<bool>, T>> generate_min_terms(vector<T> constraints){
-		
-		return 0;
-	}*/
+    /*virtual vector<std::pair<vector<bool>, T>> generate_min_terms(vector<T> constraints){
+        
+        return 0;
+    }*/
 };
 
 re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m), m_ba(0), m_sa(0) {}

diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp
@@ -391,7 +391,7 @@ void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite
     if (is_marked(e)) {
         m_num_sharing++;
         return;
-    }	
+    }    
     if (stack_depth > m_max_stack_depth) {
         return;
     }

diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
@@ -1728,7 +1728,7 @@ namespace pdr {
 
     void context::validate_search() {
         expr_ref tr = m_search.get_trace(*this);
-		TRACE("pdr", tout << tr << "\n";);
+        TRACE("pdr", tout << tr << "\n";);
         smt::kernel solver(m, get_fparams());
         solver.assert_expr(tr);
         lbool res = solver.check();

diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -130,13 +130,36 @@ class inc_sat_solver : public solver {
         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 @@ class inc_sat_solver : public solver {
         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 @@ class inc_sat_solver : public solver {
         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 @@ class inc_sat_solver : public solver {
         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 @@ class inc_sat_solver : public solver {
         return l_true;
     }
 
-
     virtual std::string reason_unknown() const {
         return m_unknown;
     }
@@ -569,7 +592,7 @@ class inc_sat_solver : public solver {
         }
     }
 
-    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 @@ class inc_sat_solver : public solver {
         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);
         }
     }

diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp
@@ -51,9 +51,9 @@ namespace smt {
             if (!m_theory_var_priority.find(v2, p_v2)) {
                 p_v2 = 0.0;
             }
-	    // add clause activity
-	    p_v1 += m_activity[v1];
-	    p_v2 += m_activity[v2];
+        // add clause activity
+        p_v1 += m_activity[v1];
+        p_v2 += m_activity[v2];
             return p_v1 > p_v2;
         }
     };

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
@@ -3035,7 +3035,7 @@ namespace smt {
         // not counting any literals that get assigned by this method
         // this relies on bcp() to give us its old m_qhead and therefore
         // bcp() should always be called before this method
-	
+    
         unsigned assigned_literal_end = m_assigned_literals.size();
         for (; qhead < assigned_literal_end; ++qhead) {
             literal l = m_assigned_literals[qhead];

diff --git a/src/smt/smt_for_each_relevant_expr.cpp b/src/smt/smt_for_each_relevant_expr.cpp
@@ -23,7 +23,7 @@ Revision History:
 
 namespace smt {
 
-	bool check_at_labels::check(expr* n) {
+    bool check_at_labels::check(expr* n) {
         m_first = true;
         return count_at_labels_pos(n) <= 1;
     }

diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
@@ -279,7 +279,7 @@ namespace smt {
             m_aux_context->pop(1);
             return r == l_false; // quantifier is satisfied by m_curr_model
         }
-		
+        
         model_ref complete_cex;
         m_aux_context->get_model(complete_cex); 
 
@@ -425,7 +425,7 @@ namespace smt {
         ptr_vector<quantifier>::const_iterator end = m_qm->end_quantifiers();
         for (; it != end; ++it) {
             quantifier * q = *it;
-	    if(!m_qm->mbqi_enabled(q)) continue;
+        if(!m_qm->mbqi_enabled(q)) continue;
             TRACE("model_checker", 
                   tout << "Check: " << mk_pp(q, m) << "\n";
                   tout << m_context->get_assignment(q) << "\n";);

diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
@@ -426,19 +426,19 @@ namespace smt {
         ptr_buffer<enode> to_unmark;
         unsigned num_vars = get_num_vars();
         for (unsigned i = 0; i < num_vars; i++) {
-	    enode * n = get_enode(i);
+        enode * n = get_enode(i);
             if (ctx.is_relevant(n)) {
-	        enode * r = n->get_root();
-		if (!r->is_marked()){
-		    if(is_array_sort(r) && ctx.is_shared(r)) {
-		      TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";);
-		      theory_var r_th_var = r->get_th_var(get_id());
-		      SASSERT(r_th_var != null_theory_var);
-		      result.push_back(r_th_var);
-		    }
-		    r->set_mark();
-		    to_unmark.push_back(r);
-		}
+            enode * r = n->get_root();
+        if (!r->is_marked()){
+            if(is_array_sort(r) && ctx.is_shared(r)) {
+              TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";);
+              theory_var r_th_var = r->get_th_var(get_id());
+              SASSERT(r_th_var != null_theory_var);
+              result.push_back(r_th_var);
+            }
+            r->set_mark();
+            to_unmark.push_back(r);
+        }
             }
         }
         unmark_enodes(to_unmark.size(), to_unmark.c_ptr());