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

scripts/mk_util.py

@@ -610,7 +610,7 @@ elif os.name == 'posix':
         IS_CYGWIN=True
         if (CC != None and "mingw" in CC):
             IS_CYGWIN_MINGW=True
-    elif os.uname()[0].startswith('MSYS_NT'):
+    elif os.uname()[0].startswith('MSYS_NT') or os.uname()[0].startswith('MINGW'):
         IS_MSYS2=True
         if os.uname()[4] == 'x86_64':
             LINUX_X64=True
@@ -1240,7 +1240,7 @@ def get_so_ext():
     sysname = os.uname()[0]
     if sysname == 'Darwin':
         return 'dylib'
-    elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'OpenBSD' or sysname.startswith('MSYS_NT'):
+    elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'OpenBSD' or sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
         return 'so'
     elif sysname == 'CYGWIN':
         return 'dll'
@@ -1888,7 +1888,6 @@ class MLComponent(Component):
     def _init_ocamlfind_paths(self):
         """
             Initialises self.destdir and self.ldconf
-
             Do not call this from the MLComponent constructor because OCAMLFIND
             has not been checked at that point
         """
@@ -2459,7 +2458,7 @@ def mk_config():
         if sysname == 'Darwin':
             SO_EXT         = '.dylib'
             SLIBFLAGS      = '-dynamiclib'
-        elif sysname == 'Linux' or sysname.startswith('MSYS_NT'):
+        elif sysname == 'Linux' or sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
             CXXFLAGS       = '%s -D_LINUX_' % CXXFLAGS
             OS_DEFINES     = '-D_LINUX_'
             SO_EXT         = '.so'
@@ -3173,7 +3172,6 @@ class MakeRuleCmd(object):
     """
         These class methods provide a convenient way to emit frequently
         needed commands used in Makefile rules
-
         Note that several of the method are meant for use during ``make
         install`` and ``make uninstall``.  These methods correctly use
         ``$(PREFIX)`` and ``$(DESTDIR)`` and therefore are preferrable
@@ -3349,10 +3347,8 @@ def configure_file(template_file_path, output_file_path, substitutions):
         Read a template file ``template_file_path``, perform substitutions
         found in the ``substitutions`` dictionary and write the result to
         the output file ``output_file_path``.
-
         The template file should contain zero or more template strings of the
         form ``@NAME@``.
-
         The substitutions dictionary maps old strings (without the ``@``
         symbols) to their replacements.
     """

src/smt/params/smt_params_helper.pyg

@@ -74,7 +74,7 @@ def_module_params(module_name='smt',
                           ('str.fast_length_tester_cache', BOOL, False, 'cache length tester constants instead of regenerating them'),
                           ('str.fast_value_tester_cache', BOOL, True, 'cache value tester constants instead of regenerating them'),
                           ('str.string_constant_cache', BOOL, True, 'cache all generated string constants generated from anywhere in theory_str'),
-                          ('str.use_binary_search', BOOL, False, 'use a binary search heuristic for finding concrete length values for free variables in theory_str (set to False to use linear search)'),
+                          ('str.use_binary_search', BOOL, True, 'use a binary search heuristic for finding concrete length values for free variables in theory_str (set to False to use linear search)'),
                           ('str.binary_search_start', UINT, 64, 'initial upper bound for theory_str binary search'),
                           ('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'),
                           ('str.finite_overlap_models', BOOL, False, 'attempt a finite model search for overlapping variables instead of completely giving up on the arrangement'),

src/smt/theory_str.cpp

@@ -166,14 +166,18 @@ namespace smt {
         }
     }
 
-    void theory_str::assert_axiom(expr * e) {
+    void theory_str::assert_axiom(expr * _e) {
         if (opt_VerifyFinalCheckProgress) {
             finalCheckProgressIndicator = true;
         }
 
-        if (get_manager().is_true(e)) return;
+        if (get_manager().is_true(_e)) return;
-        TRACE("str", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << std::endl;);
         context & ctx = get_context();
+        ast_manager& m = get_manager();
+        TRACE("str", tout << "asserting " << mk_ismt2_pp(_e, m) << std::endl;);
+        expr_ref e(_e, m);
+        //th_rewriter rw(m);
+        //rw(e);
         if (!ctx.b_internalized(e)) {
             ctx.internalize(e, false);
         }
@@ -1422,104 +1426,6 @@ namespace smt {
         assert_axiom(finalAxiom);
     }
 
-    void theory_str::instantiate_axiom_Substr(enode * e) {
-        context & ctx = get_context();
-        ast_manager & m = get_manager();
-
-        app * expr = e->get_owner();
-        if (axiomatized_terms.contains(expr)) {
-            TRACE("str", tout << "already set up Substr axiom for " << mk_pp(expr, m) << std::endl;);
-            return;
-        }
-        axiomatized_terms.insert(expr);
-
-        TRACE("str", tout << "instantiate Substr axiom for " << mk_pp(expr, m) << std::endl;);
-
-        expr_ref substrBase(expr->get_arg(0), m);
-        expr_ref substrPos(expr->get_arg(1), m);
-        expr_ref substrLen(expr->get_arg(2), m);
-        SASSERT(substrBase);
-        SASSERT(substrPos);
-        SASSERT(substrLen);
-
-        expr_ref zero(m_autil.mk_numeral(rational::zero(), true), m);
-        expr_ref minusOne(m_autil.mk_numeral(rational::minus_one(), true), m);
-        SASSERT(zero);
-        SASSERT(minusOne);
-
-        expr_ref_vector argumentsValid_terms(m);
-        // pos >= 0
-        argumentsValid_terms.push_back(m_autil.mk_ge(substrPos, zero));
-        // pos < strlen(base)
-        // --> pos + -1*strlen(base) < 0
-        argumentsValid_terms.push_back(mk_not(m, m_autil.mk_ge(
-                                                    m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, substrLen)),
-                                                    zero)));
-
-        // len >= 0
-        argumentsValid_terms.push_back(m_autil.mk_ge(substrLen, zero));
-
-        expr_ref argumentsValid(mk_and(argumentsValid_terms), m);
-        SASSERT(argumentsValid);
-        ctx.internalize(argumentsValid, false);
-
-        // (pos+len) >= strlen(base)
-        // --> pos + len + -1*strlen(base) >= 0
-        expr_ref lenOutOfBounds(m_autil.mk_ge(
-                                    m_autil.mk_add(substrPos, substrLen, m_autil.mk_mul(minusOne, mk_strlen(substrBase))),
-                                    zero), m);
-        SASSERT(lenOutOfBounds);
-        ctx.internalize(argumentsValid, false);
-
-        // Case 1: pos < 0 or pos >= strlen(base) or len < 0
-        // ==> (Substr ...) = ""
-        expr_ref case1_premise(mk_not(m, argumentsValid), m);
-        SASSERT(case1_premise);
-        ctx.internalize(case1_premise, false);
-        expr_ref case1_conclusion(ctx.mk_eq_atom(expr, mk_string("")), m);
-        SASSERT(case1_conclusion);
-        ctx.internalize(case1_conclusion, false);
-        expr_ref case1(rewrite_implication(case1_premise, case1_conclusion), m);
-        SASSERT(case1);
-
-        // Case 2: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) >= strlen(base)
-        // ==> base = t0.t1 AND len(t0) = pos AND (Substr ...) = t1
-        expr_ref t0(mk_str_var("t0"), m);
-        expr_ref t1(mk_str_var("t1"), m);
-        expr_ref case2_conclusion(m.mk_and(
-                                      ctx.mk_eq_atom(substrBase, mk_concat(t0,t1)),
-                                      ctx.mk_eq_atom(mk_strlen(t0), substrPos),
-                                      ctx.mk_eq_atom(expr, t1)), m);
-        expr_ref case2(rewrite_implication(m.mk_and(argumentsValid, lenOutOfBounds), case2_conclusion), m);
-        SASSERT(case2);
-
-        // Case 3: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) < strlen(base)
-        // ==> base = t2.t3.t4 AND len(t2) = pos AND len(t3) = len AND (Substr ...) = t3
-
-        expr_ref t2(mk_str_var("t2"), m);
-        expr_ref t3(mk_str_var("t3"), m);
-        expr_ref t4(mk_str_var("t4"), m);
-        expr_ref_vector case3_conclusion_terms(m);
-        case3_conclusion_terms.push_back(ctx.mk_eq_atom(substrBase, mk_concat(t2, mk_concat(t3, t4))));
-        case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t2), substrPos));
-        case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t3), substrLen));
-        case3_conclusion_terms.push_back(ctx.mk_eq_atom(expr, t3));
-        expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m);
-        expr_ref case3(rewrite_implication(m.mk_and(argumentsValid, mk_not(m, lenOutOfBounds)), case3_conclusion), m);
-        SASSERT(case3);
-
-        ctx.internalize(case1, false);
-        ctx.internalize(case2, false);
-        ctx.internalize(case3, false);
-
-        expr_ref finalAxiom(m.mk_and(case1, case2, case3), m);
-        SASSERT(finalAxiom);
-        assert_axiom(finalAxiom);
-    }
-
-#if 0
-    // rewrite
-    // requires to add th_rewriter to assert_axiom to enforce normal form.
     void theory_str::instantiate_axiom_Substr(enode * e) {
         context & ctx = get_context();
         ast_manager & m = get_manager();
@@ -1551,6 +1457,7 @@ namespace smt {
         argumentsValid_terms.push_back(mk_not(m, m_autil.mk_ge(
                                                     m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, substrLen)),
                                                     zero)));
+
         // len >= 0
         argumentsValid_terms.push_back(m_autil.mk_ge(substrLen, zero));
 
@@ -1564,7 +1471,7 @@ namespace smt {
 
         // Case 1: pos < 0 or pos >= strlen(base) or len < 0
         // ==> (Substr ...) = ""
-        expr_ref case1_premise(mk_not(m, argumentsValid), m);
+        expr_ref case1_premise(m.mk_not(argumentsValid), m);
         expr_ref case1_conclusion(ctx.mk_eq_atom(expr, mk_string("")), m);
         expr_ref case1(m.mk_implies(case1_premise, case1_conclusion), m);
 
@@ -1580,6 +1487,7 @@ namespace smt {
 
         // Case 3: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) < strlen(base)
         // ==> base = t2.t3.t4 AND len(t2) = pos AND len(t3) = len AND (Substr ...) = t3
+
         expr_ref t2(mk_str_var("t2"), m);
         expr_ref t3(mk_str_var("t3"), m);
         expr_ref t4(mk_str_var("t4"), m);
@@ -1589,13 +1497,24 @@ namespace smt {
         case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t3), substrLen));
         case3_conclusion_terms.push_back(ctx.mk_eq_atom(expr, t3));
         expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m);
-        expr_ref case3(m.mk_implies(m.mk_and(argumentsValid, mk_not(m, lenOutOfBounds)), case3_conclusion), m);
+        expr_ref case3(m.mk_implies(m.mk_and(argumentsValid, m.mk_not(lenOutOfBounds)), case3_conclusion), m);
 
-        assert_axiom(case1);
+        {
-        assert_axiom(case2);
+            th_rewriter rw(m);
-        assert_axiom(case3);
+
+            expr_ref case1_rw(case1, m);
+            rw(case1_rw);
+            assert_axiom(case1_rw);
+
+            expr_ref case2_rw(case2, m);
+            rw(case2_rw);
+            assert_axiom(case2_rw);
+
+            expr_ref case3_rw(case3, m);
+            rw(case3_rw);
+            assert_axiom(case3_rw);
+        }
     }
-#endif
 
     void theory_str::instantiate_axiom_Replace(enode * e) {
         context & ctx = get_context();
@@ -1636,13 +1555,17 @@ namespace smt {
         // false branch
         expr_ref elseBranch(ctx.mk_eq_atom(result, expr->get_arg(0)), m);
 
+        th_rewriter rw(m);
+
         expr_ref breakdownAssert(m.mk_ite(condAst, m.mk_and(thenItems.size(), thenItems.c_ptr()), elseBranch), m);
-        assert_axiom(breakdownAssert);
+        expr_ref breakdownAssert_rw(breakdownAssert, m);
-        
+        rw(breakdownAssert_rw);
-        SASSERT(breakdownAssert);
+        assert_axiom(breakdownAssert_rw);
 
         expr_ref reduceToResult(ctx.mk_eq_atom(expr, result), m);
-        assert_axiom(reduceToResult);
+        expr_ref reduceToResult_rw(reduceToResult, m);
+        rw(reduceToResult_rw);
+        assert_axiom(reduceToResult_rw);
     }
 
     void theory_str::instantiate_axiom_str_to_int(enode * e) {
@@ -4752,12 +4675,10 @@ namespace smt {
     bool theory_str::get_arith_value(expr* e, rational& val) const {
         context& ctx = get_context();
         ast_manager & m = get_manager();
-
+        // safety
-    // safety
+        if (!ctx.e_internalized(e)) {
-    if (!ctx.e_internalized(e)) {
             return false;
-    }
+        }
-    
         // if an integer constant exists in the eqc, it should be the root
         enode * en_e = ctx.get_enode(e);
         enode * root_e = en_e->get_root();
@@ -9907,6 +9828,21 @@ namespace smt {
         expr_ref freeVarLen(mk_strlen(freeVar), m);
         SASSERT(freeVarLen);
 
+        {
+            rational freeVar_len_value;
+            if (get_len_value(freeVar, freeVar_len_value)) {
+                TRACE("str", tout << "special case: length of freeVar is known to be " << freeVar_len_value << std::endl;);
+                expr_ref concreteOption(ctx.mk_eq_atom(indicator, mk_string(freeVar_len_value.to_string().c_str()) ), m);
+                expr_ref concreteValue(ctx.mk_eq_atom(
+                        ctx.mk_eq_atom(indicator, mk_string(freeVar_len_value.to_string().c_str()) ),
+                        ctx.mk_eq_atom(freeVarLen, m_autil.mk_numeral(freeVar_len_value, true))), m);
+                expr_ref finalAxiom(m.mk_and(concreteOption, concreteValue), m);
+                SASSERT(finalAxiom);
+                m_trail.push_back(finalAxiom);
+                return finalAxiom;
+            }
+        }
+
         expr_ref_vector orList(m);
         expr_ref_vector andList(m);
 
@@ -10221,6 +10157,16 @@ namespace smt {
             }
             refresh_theory_var(firstTester);
 
+            {
+                rational freeVar_len_value;
+                if (get_len_value(freeVar, freeVar_len_value)) {
+                    TRACE("str", tout << "special case: length of freeVar is known to be " << freeVar_len_value << std::endl;);
+                    midPoint = freeVar_len_value;
+                    upperBound = midPoint * 2;
+                    windowSize = upperBound;
+                }
+            }
+
             binary_search_len_tester_stack[freeVar].push_back(firstTester);
             m_trail_stack.push(binary_search_trail<theory_str>(binary_search_len_tester_stack, freeVar));
             binary_search_info new_info(lowerBound, midPoint, upperBound, windowSize);
@@ -10484,6 +10430,9 @@ namespace smt {
             // iterate parents
             if (standAlone) {
                 // I hope this works!
+                if (!ctx.e_internalized(freeVar)) {
+                    ctx.internalize(freeVar, false);
+                }
                 enode * e_freeVar = ctx.get_enode(freeVar);
                 enode_vector::iterator it = e_freeVar->begin_parents();
                 for (; it != e_freeVar->end_parents(); ++it) {