From ee1af96f1bf92d1546449dc30573b62f27c34fae Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 1 Aug 2016 17:05:02 -0400 Subject: [PATCH] add opt_NoQuickReturn_IntegerTheory check in theory_str::new_eq_check() 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. --- src/smt/theory_str.cpp | 13 +++++++++---- src/smt/theory_str.h | 10 ++++------ 2 files changed, 13 insertions(+), 10 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 2b94b0c40..a80fd2165 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -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; diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index bd66e64d4..74c1786df 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -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,