diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 6f3052f6e..8d4fe5552 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -72,6 +72,7 @@ IS_FREEBSD=False IS_OPENBSD=False IS_CYGWIN=False IS_CYGWIN_MINGW=False +IS_MSYS2=False VERBOSE=True DEBUG_MODE=False SHOW_CPPS = True @@ -152,6 +153,9 @@ def is_cygwin(): def is_cygwin_mingw(): return IS_CYGWIN_MINGW +def is_msys2(): + return IS_MSYS2 + def norm_path(p): return os.path.expanduser(os.path.normpath(p)) @@ -227,7 +231,7 @@ def rmf(fname): def exec_compiler_cmd(cmd): r = exec_cmd(cmd) - if is_windows() or is_cygwin_mingw(): + if is_windows() or is_cygwin_mingw() or is_cygwin() or is_msys2(): rmf('a.exe') else: rmf('a.out') @@ -606,6 +610,13 @@ 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'): + IS_MSYS2=True + if os.uname()[4] == 'x86_64': + LINUX_X64=True + else: + LINUX_X64=False + def display_help(exit_code): print("mk_make.py: Z3 Makefile generator\n") @@ -1229,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': + elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'OpenBSD' or sysname.startswith('MSYS_NT'): return 'so' elif sysname == 'CYGWIN': return 'dll' @@ -1783,6 +1794,8 @@ class JavaDLLComponent(Component): t = t.replace('PLATFORM', 'openbsd') elif IS_CYGWIN: t = t.replace('PLATFORM', 'cygwin') + elif IS_MSYS2: + t = t.replace('PLATFORM', 'win32') else: t = t.replace('PLATFORM', 'win32') out.write(t) @@ -2446,7 +2459,7 @@ def mk_config(): if sysname == 'Darwin': SO_EXT = '.dylib' SLIBFLAGS = '-dynamiclib' - elif sysname == 'Linux': + elif sysname == 'Linux' or sysname.startswith('MSYS_NT'): CXXFLAGS = '%s -D_LINUX_' % CXXFLAGS OS_DEFINES = '-D_LINUX_' SO_EXT = '.so' @@ -2466,10 +2479,10 @@ def mk_config(): SO_EXT = '.so' SLIBFLAGS = '-shared' elif sysname[:6] == 'CYGWIN': - CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS + CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS OS_DEFINES = '-D_CYGWIN' - SO_EXT = '.dll' - SLIBFLAGS = '-shared' + SO_EXT = '.dll' + SLIBFLAGS = '-shared' else: raise MKException('Unsupported platform: %s' % sysname) if is64(): diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index d6ca8c9b2..937aa6a2b 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/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'), diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index c508a65cb..7b508c7d8 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4389,7 +4389,8 @@ namespace smt { subst.push_back(arg); } expr_ref bodyr(m); - var_subst sub(m, false); + var_subst sub(m, true); + TRACE("context", tout << expr_ref(q, m) << " " << subst << "\n";); sub(body, subst.size(), subst.c_ptr(), bodyr); func_decl* f = to_app(fn)->get_decl(); func_interp* fi = alloc(func_interp, m, f->get_arity()); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index f47d6011f..a1f0f9777 100644 --- a/src/smt/theory_str.cpp +++ b/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; - TRACE("str", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << std::endl;); + if (get_manager().is_true(_e)) return; 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); - assert_axiom(case3); + { + th_rewriter rw(m); + + 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); - - SASSERT(breakdownAssert); + expr_ref breakdownAssert_rw(breakdownAssert, m); + rw(breakdownAssert_rw); + 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 - if (!ctx.e_internalized(e)) { + // safety + 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(binary_search_len_tester_stack, freeVar)); binary_search_info new_info(lowerBound, midPoint, upperBound, windowSize);