theory_str parameters

src/smt/params/smt_params_helper.pyg

@@ -62,5 +62,7 @@ def_module_params(module_name='smt',
                           ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
                           ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'),
                           ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
-                          ('str.strong_arrangements', BOOL, True, 'assert equivalences instead of implications when generating string arrangement axioms')
+                          ('str.strong_arrangements', BOOL, True, 'assert equivalences instead of implications when generating string arrangement axioms'),
+                          ('str.aggressive_length_testing', BOOL, False, 'prioritize testing concrete length values over generating more options'),
+                          ('str.aggressive_value_testing', BOOL, False, 'prioritize testing concrete string constant values over generating more options')
                           ))

src/smt/params/theory_str_params.cpp

@@ -21,4 +21,6 @@ Revision History:
 void theory_str_params::updt_params(params_ref const & _p) {
     smt_params_helper p(_p);
     m_AssertStrongerArrangements = p.str_strong_arrangements();
+    m_AggressiveLengthTesting = p.str_aggressive_length_testing();
+    m_AggressiveValueTesting = p.str_aggressive_value_testing();
 }

src/smt/params/theory_str_params.h

@@ -30,8 +30,22 @@ struct theory_str_params {
      */
     bool m_AssertStrongerArrangements;
 
+    /*
+     * If AggressiveLengthTesting is true, we manipulate the phase of length tester equalities
+     * to prioritize trying concrete length options over choosing the "more" option.
+     */
+    bool m_AggressiveLengthTesting;
+
+    /*
+     * Similarly, if AggressiveValueTesting is true, we manipulate the phase of value tester equalities
+     * to prioritize trying concrete value options over choosing the "more" option.
+     */
+    bool m_AggressiveValueTesting;
+
     theory_str_params(params_ref const & p = params_ref()):
-        m_AssertStrongerArrangements(true)
+        m_AssertStrongerArrangements(true),
+        m_AggressiveLengthTesting(false),
+        m_AggressiveValueTesting(false)
     {
         updt_params(p);
     }

src/smt/theory_str.cpp

@@ -33,8 +33,6 @@ theory_str::theory_str(ast_manager & m, theory_str_params const & params):
         theory(m.mk_family_id("str")),
         m_params(params),
         /* Options */
-        opt_AggressiveLengthTesting(false),
-        opt_AggressiveValueTesting(false),
         opt_AggressiveUnrollTesting(true),
         opt_EagerStringConstantLengthAssertions(true),
         opt_VerifyFinalCheckProgress(true),
@@ -8364,7 +8362,7 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr *
 			<< "val_indicator = " << mk_ismt2_pp(val_indicator, m) << std::endl
 			<< "lenstr = " << lenStr << std::endl
 			<< "tries = " << tries << std::endl;
-            if (opt_AggressiveValueTesting) {
+            if (m_params.m_AggressiveValueTesting) {
                 tout << "note: aggressive value testing is enabled" << std::endl;
             }
 	);
@@ -8408,7 +8406,7 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr *
 	for (long long i = l; i < h; i++) {
 		// TODO can we share the val_indicator constants with the length tester cache?
 		orList.push_back(m.mk_eq(val_indicator, m_strutil.mk_string(longlong_to_string(i).c_str()) ));
-		if (opt_AggressiveValueTesting) {
+		if (m_params.m_AggressiveValueTesting) {
 		    literal l = mk_eq(val_indicator, m_strutil.mk_string(longlong_to_string(i).c_str()), false);
 		    ctx.mark_as_relevant(l);
 		    ctx.force_phase(l);
@@ -8429,7 +8427,7 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr *
 	}
 	if (!coverAll) {
 		orList.push_back(m.mk_eq(val_indicator, m_strutil.mk_string("more")));
-		if (opt_AggressiveValueTesting) {
+		if (m_params.m_AggressiveValueTesting) {
 		    literal l = mk_eq(val_indicator, m_strutil.mk_string("more"), false);
 		    ctx.mark_as_relevant(l);
 		    ctx.force_phase(~l);
@@ -8980,7 +8978,7 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr
 
 	TRACE("t_str_detail",
 	        tout << "building andList and orList" << std::endl;
-	        if (opt_AggressiveLengthTesting) {
+	        if (m_params.m_AggressiveLengthTesting) {
 	            tout << "note: aggressive length testing is active" << std::endl;
 	        }
 	);
@@ -9007,7 +9005,7 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr
 		expr_ref or_expr(ctx.mk_eq_atom(indicator, str_indicator), m);
 		orList.push_back(or_expr);
 
-		if (opt_AggressiveLengthTesting) {
+		if (m_params.m_AggressiveLengthTesting) {
 		    literal l = mk_eq(indicator, str_indicator, false);
 		    ctx.mark_as_relevant(l);
 		    ctx.force_phase(l);
@@ -9019,7 +9017,7 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr
 
 	// TODO cache mk_string("more")
 	orList.push_back(m.mk_eq(indicator, m_strutil.mk_string("more")));
-	if (opt_AggressiveLengthTesting) {
+	if (m_params.m_AggressiveLengthTesting) {
 	    literal l = mk_eq(indicator, m_strutil.mk_string("more"), false);
 	    ctx.mark_as_relevant(l);
 	    ctx.force_phase(~l);

src/smt/theory_str.h

@@ -100,18 +100,6 @@ namespace smt {
     protected:
         theory_str_params const & m_params;
 
-        /*
-         * If AggressiveLengthTesting is true, we manipulate the phase of length tester equalities
-         * to prioritize trying concrete length options over choosing the "more" option.
-         */
-        bool opt_AggressiveLengthTesting;
-
-        /*
-         * Similarly, if AggressiveValueTesting is true, we manipulate the phase of value tester equalities
-         * to prioritize trying concrete value options over choosing the "more" option.
-         */
-        bool opt_AggressiveValueTesting;
-
         /*
          * If AggressiveUnrollTesting is true, we manipulate the phase of regex unroll tester equalities
          * to prioritize trying concrete unroll counts over choosing the "more" option.