mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

Merge remote-tracking branch 'upstream/master' into issue1274-crash

Browse source
This commit is contained in:
Murphy Berzish 2017-10-31 17:07:54 -04:00
commit 2d25355611
4 changed files with 84 additions and 124 deletions
Download patch file Download diff file Expand all files Collapse all files

25
scripts/mk_util.py
View file

@ -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():

2
src/smt/params/smt_params_helper.pyg
View file

@ -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'),

3
src/smt/smt_context.cpp
View file

@ -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());

178
src/smt/theory_str.cpp
View file

@ -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<theory_str>(binary_search_len_tester_stack, freeVar));
binary_search_info new_info(lowerBound, midPoint, upperBound, windowSize);