mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

add opt_NoQuickReturn_IntegerTheory check in theory_str::new_eq_check()

Browse source 
This allows us to assert an "inconsistent length" axiom from the integer theory
while continuing in new_eq_handler(). Currently active when
opt_NoQuickReturn_IntegerTheory is 'true' but this may be necessary
here and in other places, in general, to fix integer theory integration.
This commit is contained in:
Murphy Berzish 2016-08-01 17:05:02 -04:00
parent 6e348720b1
commit ee1af96f1b
2 changed files with 13 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/smt/theory_str.cpp
View file

@ -33,7 +33,7 @@ theory_str::theory_str(ast_manager & m):
opt_EagerStringConstantLengthAssertions(true),
opt_VerifyFinalCheckProgress(true),
opt_LCMUnrollStep(2),
opt_NoQuickReturn_Concat_IntegerTheory(false),
opt_NoQuickReturn_IntegerTheory(true),
opt_DisableIntegerTheoryIntegration(false),
/* Internal setup */
search_started(false),
@ -1467,11 +1467,16 @@ bool theory_str::new_eq_check(expr * lhs, expr * rhs) {
TRACE("t_str", tout << "inconsistency detected: " << mk_pp(eqc_nn1, m) << " cannot be equal to " << mk_pp(eqc_nn2, m) << std::endl;);
expr_ref to_assert(m.mk_not(ctx.mk_eq_atom(eqc_nn1, eqc_nn2)), m);
assert_axiom(to_assert);
// this shouldn't use the integer theory at all, so we don't allow the option of quick-return
return false;
}
if (!check_length_consistency(eqc_nn1, eqc_nn2)) {
TRACE("t_str", tout << "inconsistency detected: " << mk_pp(eqc_nn1, m) << " and " << mk_pp(eqc_nn2, m) << " have inconsistent lengths" << std::endl;);
return false;
if (opt_NoQuickReturn_IntegerTheory){
TRACE("t_str_detail", tout << "continuing in new_eq_check() due to opt_NoQuickReturn_IntegerTheory" << std::endl;);
} else {
return false;
}
}
}
eqc_iterator2 = eqc_iterator2->get_next();
@ -2175,7 +2180,7 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) {
assert_implication(premise, conclusion);
if (opt_NoQuickReturn_Concat_IntegerTheory) {
if (opt_NoQuickReturn_IntegerTheory) {
TRACE("t_str_detail", tout << "bypassing quick return from the end of this case" << std::endl;);
} else {
return;
@ -2195,7 +2200,7 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) {
expr_ref conclusion(m.mk_and(ax_r1, ax_r2), m);
assert_implication(premise, conclusion);
if (opt_NoQuickReturn_Concat_IntegerTheory) {
if (opt_NoQuickReturn_IntegerTheory) {
TRACE("t_str_detail", tout << "bypassing quick return from the end of this case" << std::endl;);
} else {
return;

10
src/smt/theory_str.h
View file

@ -95,14 +95,12 @@ namespace smt {
int opt_LCMUnrollStep;
/*
* If NoQuickReturn_Concat_IntegerTheory is set to true,
* the integer theory integration conditionals in simplify_concat_equality()
* If NoQuickReturn_IntegerTheory is set to true,
* integer theory integration checks that assert axioms
* will not return from the function after asserting their axioms.
* This means that control will fall through to the type 1-6 axioms,
* causing those to be added as well.
* The default behaviour of Z3str2 is to set this to 'false'.
* The default behaviour of Z3str2 is to set this to 'false'. This may be incorrect.
*/
bool opt_NoQuickReturn_Concat_IntegerTheory;
bool opt_NoQuickReturn_IntegerTheory;
/*
* If DisableIntegerTheoryIntegration is set to true,