From e459617c39b8ef171586f50748126de49dc53f85 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 16 Jan 2017 18:04:03 -0500 Subject: [PATCH] experimental finite model finding WIP, first successful run --- src/smt/params/smt_params_helper.pyg | 3 +- src/smt/params/theory_str_params.cpp | 1 + src/smt/params/theory_str_params.h | 8 ++ src/smt/theory_str.cpp | 160 ++++++++++++++++++++++++++- src/smt/theory_str.h | 6 + 5 files changed, 175 insertions(+), 3 deletions(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 8e8e52987..e23915ab4 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -72,5 +72,6 @@ def_module_params(module_name='smt', ('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.binary_search_start', UINT, 64, 'initial upper bound for theory_str binary search'), ('theory_case_split', BOOL, False, 'Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead.'), - ('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.') + ('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') )) diff --git a/src/smt/params/theory_str_params.cpp b/src/smt/params/theory_str_params.cpp index 2e98a4394..46302cf82 100644 --- a/src/smt/params/theory_str_params.cpp +++ b/src/smt/params/theory_str_params.cpp @@ -27,6 +27,7 @@ void theory_str_params::updt_params(params_ref const & _p) { m_UseFastLengthTesterCache = p.str_fast_length_tester_cache(); m_UseFastValueTesterCache = p.str_fast_value_tester_cache(); m_StringConstantCache = p.str_string_constant_cache(); + m_FiniteOverlapModels = p.str_finite_overlap_models(); m_UseBinarySearch = p.str_use_binary_search(); m_BinarySearchInitialUpperBound = p.str_binary_search_start(); } diff --git a/src/smt/params/theory_str_params.h b/src/smt/params/theory_str_params.h index 39c553780..4effb0897 100644 --- a/src/smt/params/theory_str_params.h +++ b/src/smt/params/theory_str_params.h @@ -68,6 +68,13 @@ struct theory_str_params { */ bool m_StringConstantCache; + /* + * If FiniteOverlapModels is set to true, + * arrangements that result in overlapping variables will generate a small number of models + * to test instead of completely giving up on the case. + */ + bool m_FiniteOverlapModels; + bool m_UseBinarySearch; unsigned m_BinarySearchInitialUpperBound; @@ -79,6 +86,7 @@ struct theory_str_params { m_UseFastLengthTesterCache(false), m_UseFastValueTesterCache(true), m_StringConstantCache(true), + m_FiniteOverlapModels(false), m_UseBinarySearch(false), m_BinarySearchInitialUpperBound(64) { diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index fd379fd2d..4ff80a613 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -4394,8 +4394,47 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) { add_theory_aware_branching_info(option1, 0.1, l_true); } else { loopDetected = true; - TRACE("t_str", tout << "AVOID LOOP: SKIPPED." << std::endl;); - TRACE("t_str", print_cut_var(m, tout); print_cut_var(y, tout);); + + if (m_params.m_FiniteOverlapModels) { + // TODO refactor this entire segment into its own method. this is really just for experiment purposes + TRACE("t_str", tout << "activating finite model testing for overlapping concats " + << mk_pp(concatAst1, mgr) << " and " << mk_pp(concatAst2, mgr) << std::endl;); + std::map concatMap; + std::map unrollMap; + std::map varMap; + classify_ast_by_type(concatAst1, varMap, concatMap, unrollMap); + classify_ast_by_type(concatAst2, varMap, concatMap, unrollMap); + TRACE("t_str_detail", tout << "found vars:"; + for (std::map::iterator it = varMap.begin(); it != varMap.end(); ++it) { + tout << " " << mk_pp(it->first, mgr); + } + tout << std::endl; + ); + + expr_ref testvar(mk_str_var("finiteModelTest"), mgr); + m_trail.push_back(testvar); + ptr_vector varlist; + + for (std::map::iterator it = varMap.begin(); it != varMap.end(); ++it) { + expr * v = it->first; + varlist.push_back(v); + } + + // make things easy for the core wrt. testvar + expr_ref t1(ctx.mk_eq_atom(testvar, m_strutil.mk_string("")), mgr); + expr_ref t_yes(ctx.mk_eq_atom(testvar, m_strutil.mk_string("yes")), mgr); + expr_ref testvaraxiom(mgr.mk_or(t1, t_yes), mgr); + assert_axiom(testvaraxiom); + + finite_model_test_varlists.insert(testvar, varlist); + m_trail_stack.push(insert_obj_map >(finite_model_test_varlists, testvar) ); + + arrangement_disjunction.push_back(t_yes); + add_theory_aware_branching_info(t_yes, -0.1, l_true); + } else { + TRACE("t_str", tout << "AVOID LOOP: SKIPPED." << std::endl;); + TRACE("t_str", print_cut_var(m, tout); print_cut_var(y, tout);); + } } for (std::list::iterator itor = overlapLen.begin(); itor != overlapLen.end(); itor++) { @@ -6564,6 +6603,114 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { } } +void theory_str::finite_model_test(expr * testvar, expr * str) { + context & ctx = get_context(); + ast_manager & m = get_manager(); + + if (!m_strutil.is_string(str)) return; + std::string s = m_strutil.get_string_constant_value(str); + if (s == "yes") { + TRACE("t_str", tout << "start finite model test for " << mk_pp(testvar, m) << std::endl;); + ptr_vector & vars = finite_model_test_varlists[testvar]; + for (ptr_vector::iterator it = vars.begin(); it != vars.end(); ++it) { + expr * v = *it; + // check for any sort of existing length tester we might interfere with + if (m_params.m_UseBinarySearch) { + NOT_IMPLEMENTED_YET(); + } else { + bool map_effectively_empty = false; + if (fvar_len_count_map.find(v) == fvar_len_count_map.end()) { + map_effectively_empty = true; + } + + if (!map_effectively_empty) { + map_effectively_empty = true; + ptr_vector indicator_set = fvar_lenTester_map[v]; + for (ptr_vector::iterator it = indicator_set.begin(); it != indicator_set.end(); ++it) { + expr * indicator = *it; + if (internal_variable_set.find(indicator) != internal_variable_set.end()) { + map_effectively_empty = false; + break; + } + } + } + + if (map_effectively_empty) { + TRACE("t_str_detail", tout << "no existing length testers for " << mk_pp(v, m) << std::endl;); + rational v_len; + if (get_len_value(v, v_len)) { + TRACE("t_str_detail", tout << "length = " << v_len.to_string() << std::endl;); + } else { + expr_ref vLengthExpr(mk_strlen(v), m); + + rational v_lower_bound; + bool lower_bound_exists = lower_bound(vLengthExpr, v_lower_bound); + rational v_upper_bound; + bool upper_bound_exists = upper_bound(vLengthExpr, v_upper_bound); + TRACE("t_str_detail", tout << "bounds = [" << (lower_bound_exists?v_lower_bound.to_string():"?") + << ".." << (upper_bound_exists?v_upper_bound.to_string():"?") << "]" << std::endl;); + + // make sure the bounds are non-negative + if (lower_bound_exists && v_lower_bound.is_neg()) { + v_lower_bound = rational::zero(); + } + if (upper_bound_exists && v_upper_bound.is_neg()) { + v_upper_bound = rational::zero(); + } + + if (lower_bound_exists && upper_bound_exists) { + // easiest case. we will search within these bounds + } else if (upper_bound_exists && !lower_bound_exists) { + // search between 0 and the upper bound + v_lower_bound == rational::zero(); + } else if (lower_bound_exists && !upper_bound_exists) { + // check some finite portion of the search space + // TODO here and below, factor out the increment to a param + v_upper_bound = v_lower_bound + rational(10); + } else { + // no bounds information + v_lower_bound = rational::zero(); + v_upper_bound = v_lower_bound + rational(10); + } + // now create a fake length tester over this finite disjunction of lengths + + fvar_len_count_map[v] = 1; + unsigned int testNum = fvar_len_count_map[v]; + + expr_ref indicator(mk_internal_lenTest_var(v, testNum), m); + SASSERT(indicator); + m_trail.push_back(indicator); + + fvar_lenTester_map[v].shrink(0); + fvar_lenTester_map[v].push_back(indicator); + lenTester_fvar_map[indicator] = v; + + expr_ref_vector orList(m); + expr_ref_vector andList(m); + + for (rational l = v_lower_bound; l <= v_upper_bound; l += rational::one()) { + // TODO integrate with the enhancements in gen_len_test_options() + std::string lStr = l.to_string(); + expr_ref str_indicator(m_strutil.mk_string(lStr), m); + expr_ref or_expr(ctx.mk_eq_atom(indicator, str_indicator), m); + orList.push_back(or_expr); + expr_ref and_expr(ctx.mk_eq_atom(or_expr, ctx.mk_eq_atom(vLengthExpr, m_autil.mk_numeral(l, true))), m); + andList.push_back(and_expr); + } + andList.push_back(mk_or(orList)); + expr_ref implLhs(ctx.mk_eq_atom(testvar, str), m); + expr_ref implRhs(mk_and(andList), m); + assert_implication(implLhs, implRhs); + } + } else { + // TODO figure out this case + NOT_IMPLEMENTED_YET(); + } + } + } // foreach (v in vars) + } // (s == "yes") +} + void theory_str::more_len_tests(expr * lenTester, std::string lenTesterValue) { ast_manager & m = get_manager(); if (lenTester_fvar_map.find(lenTester) != lenTester_fvar_map.end()) { @@ -6666,6 +6813,15 @@ void theory_str::handle_equality(expr * lhs, expr * rhs) { return; } + if (m_params.m_FiniteOverlapModels && !finite_model_test_varlists.empty()) { + // TODO NEXT + if (finite_model_test_varlists.contains(lhs)) { + finite_model_test(lhs, rhs); return; + } else if (finite_model_test_varlists.contains(rhs)) { + finite_model_test(rhs, lhs); return; + } + } + if (free_var_attempt(lhs, rhs) || free_var_attempt(rhs, lhs)) { return; } diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 7f1e1dd9c..050593691 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -335,6 +335,10 @@ namespace smt { // maps a length tester to the next length tester to be (re)used if the split is "high" obj_map binary_search_next_var_high; + // finite model finding data + // maps a finite model tester var to a list of variables that will be tested + obj_map > finite_model_test_varlists; + protected: void assert_axiom(expr * e); void assert_implication(expr * premise, expr * conclusion); @@ -588,6 +592,8 @@ namespace smt { // TESTING void refresh_theory_var(expr * e); + void finite_model_test(expr * v, expr * c); + public: theory_str(ast_manager & m, theory_str_params const & params); virtual ~theory_str();