mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

disable length test/theory case split integration theory_str

Browse source
This commit is contained in:
Murphy Berzish 2017-01-10 12:34:44 -05:00
parent 5f854c6689
commit 9004e1b23e
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_str.cpp
View file

@ -9324,12 +9324,14 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr
andList.push_back(ctx.mk_eq_atom(orList.get(orList.size() - 1), m_autil.mk_ge(freeVarLen, mk_int(h)))); andList.push_back(ctx.mk_eq_atom(orList.get(orList.size() - 1), m_autil.mk_ge(freeVarLen, mk_int(h))));
/*
{ // more experimental theory case split support { // more experimental theory case split support
expr_ref tmp(m_autil.mk_ge(freeVarLen, mk_int(h)), m); expr_ref tmp(m_autil.mk_ge(freeVarLen, mk_int(h)), m);
ctx.internalize(m_autil.mk_ge(freeVarLen, mk_int(h)), false); ctx.internalize(m_autil.mk_ge(freeVarLen, mk_int(h)), false);
case_split_literals.push_back(ctx.get_literal(tmp)); case_split_literals.push_back(ctx.get_literal(tmp));
ctx.mk_th_case_split(case_split_literals.size(), case_split_literals.c_ptr()); ctx.mk_th_case_split(case_split_literals.size(), case_split_literals.c_ptr());
} }
*/
expr_ref_vector or_items(m); expr_ref_vector or_items(m);
expr_ref_vector and_items(m); expr_ref_vector and_items(m);
@ -9532,7 +9534,7 @@ expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenT
literal_vector case_split_literals; literal_vector case_split_literals;
expr_ref next_case_split(binary_search_case_split(freeVar, newTester, newBounds, case_split_literals)); expr_ref next_case_split(binary_search_case_split(freeVar, newTester, newBounds, case_split_literals));
m_trail.push_back(next_case_split); m_trail.push_back(next_case_split);
ctx.mk_th_case_split(case_split_literals.size(), case_split_literals.c_ptr()); // ctx.mk_th_case_split(case_split_literals.size(), case_split_literals.c_ptr());
return next_case_split; return next_case_split;
} else { // lastTesterConstant is a concrete value } else { // lastTesterConstant is a concrete value
TRACE("t_str", tout << "length is fixed; generating models for free var" << std::endl;); TRACE("t_str", tout << "length is fixed; generating models for free var" << std::endl;);
@ -9578,7 +9580,7 @@ expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenT
literal_vector case_split_literals; literal_vector case_split_literals;
expr_ref initial_case_split(binary_search_case_split(freeVar, firstTester, new_info, case_split_literals)); expr_ref initial_case_split(binary_search_case_split(freeVar, firstTester, new_info, case_split_literals));
m_trail.push_back(initial_case_split); m_trail.push_back(initial_case_split);
ctx.mk_th_case_split(case_split_literals.size(), case_split_literals.c_ptr()); // ctx.mk_th_case_split(case_split_literals.size(), case_split_literals.c_ptr());
return initial_case_split; return initial_case_split;
} }
} }