From 466269ee130e5a1925af28dd5b98fa3d74cfbb34 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 5 May 2021 10:06:03 -0500 Subject: [PATCH 01/40] theory_str iterator refactoring and dead code removal (#5222) * z3str3: iterator refactoring * z3str3: remove old nfa dead code * z3str3: continued iterator refactoring * z3str3: remove unroll dead code * z3str3: ctx_dep_analysis iterator refactoring * z3str3: continued iterator refactoring * z3str3: final iterator refactoring --- src/smt/theory_str.cpp | 777 ++++++++++------------------------------- src/smt/theory_str.h | 54 +-- 2 files changed, 195 insertions(+), 636 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index ba81cb2e1..6ef086b60 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -139,7 +139,6 @@ namespace smt { regex_terms.reset(); regex_terms_by_string.reset(); regex_automaton_assumptions.reset(); - regex_nfa_cache.reset(); regex_terms_with_path_constraints.reset(); regex_terms_with_length_constraints.reset(); regex_term_to_length_constraint.reset(); @@ -5015,7 +5014,6 @@ namespace smt { } } - //for (keysItor2 = contain_pair_idx_map[n2].begin(); keysItor2 != contain_pair_idx_map[n2].end(); keysItor2++) { for (auto const& key2 : contain_pair_idx_map[n2]) { // keysItor2 is on set {<.., n2>, ..., , ...} //std::pair key2 = *keysItor2; @@ -5112,11 +5110,7 @@ namespace smt { // * key1.first = key2.first // check eqc(key1.second) and eqc(key2.second) // ----------------------------------------------------------- - //expr_ref_vector::iterator eqItorSub1 = subAst1Eqc.begin(); - //for (; eqItorSub1 != subAst1Eqc.end(); eqItorSub1++) { for (auto eqSubVar1 : subAst1Eqc) { - //expr_ref_vector::iterator eqItorSub2 = subAst2Eqc.begin(); - //for (; eqItorSub2 != subAst2Eqc.end(); eqItorSub2++) { for (auto eqSubVar2 : subAst2Eqc) { // ------------ // key1.first = key2.first /\ containPairBoolMap[] @@ -5456,23 +5450,21 @@ namespace smt { get_grounded_concats(depth + 1, arg0DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap); get_grounded_concats(depth + 1, arg1DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap); - std::map, std::set >::iterator arg0_grdItor = groundedMap[arg0DeAlias].begin(); std::map, std::set >::iterator arg1_grdItor; - for (; arg0_grdItor != groundedMap[arg0DeAlias].end(); arg0_grdItor++) { - arg1_grdItor = groundedMap[arg1DeAlias].begin(); - for (; arg1_grdItor != groundedMap[arg1DeAlias].end(); arg1_grdItor++) { + for (auto const &arg0_grdItor : groundedMap[arg0DeAlias]) { + for (auto const &arg1_grdItor : groundedMap[arg1DeAlias]) { std::vector ndVec; - ndVec.insert(ndVec.end(), arg0_grdItor->first.begin(), arg0_grdItor->first.end()); - size_t arg0VecSize = arg0_grdItor->first.size(); - size_t arg1VecSize = arg1_grdItor->first.size(); - if (arg0VecSize > 0 && arg1VecSize > 0 && u.str.is_string(arg0_grdItor->first[arg0VecSize - 1]) && u.str.is_string(arg1_grdItor->first[0])) { + ndVec.insert(ndVec.end(), arg0_grdItor.first.begin(), arg0_grdItor.first.end()); + size_t arg0VecSize = arg0_grdItor.first.size(); + size_t arg1VecSize = arg1_grdItor.first.size(); + if (arg0VecSize > 0 && arg1VecSize > 0 && u.str.is_string(arg0_grdItor.first[arg0VecSize - 1]) && u.str.is_string(arg1_grdItor.first[0])) { ndVec.pop_back(); - ndVec.push_back(mk_concat(arg0_grdItor->first[arg0VecSize - 1], arg1_grdItor->first[0])); + ndVec.push_back(mk_concat(arg0_grdItor.first[arg0VecSize - 1], arg1_grdItor.first[0])); for (size_t i = 1; i < arg1VecSize; i++) { - ndVec.push_back(arg1_grdItor->first[i]); + ndVec.push_back(arg1_grdItor.first[i]); } } else { - ndVec.insert(ndVec.end(), arg1_grdItor->first.begin(), arg1_grdItor->first.end()); + ndVec.insert(ndVec.end(), arg1_grdItor.first.begin(), arg1_grdItor.first.end()); } // only insert if we don't know "node = concat(ndVec)" since one set of condition leads to this is enough if (groundedMap[node].find(ndVec) == groundedMap[node].end()) { @@ -5480,12 +5472,12 @@ namespace smt { if (arg0 != arg0DeAlias) { groundedMap[node][ndVec].insert(ctx.mk_eq_atom(arg0, arg0DeAlias)); } - groundedMap[node][ndVec].insert(arg0_grdItor->second.begin(), arg0_grdItor->second.end()); + groundedMap[node][ndVec].insert(arg0_grdItor.second.begin(), arg0_grdItor.second.end()); if (arg1 != arg1DeAlias) { groundedMap[node][ndVec].insert(ctx.mk_eq_atom(arg1, arg1DeAlias)); } - groundedMap[node][ndVec].insert(arg1_grdItor->second.begin(), arg1_grdItor->second.end()); + groundedMap[node][ndVec].insert(arg1_grdItor.second.begin(), arg1_grdItor.second.end()); } } } @@ -5506,16 +5498,15 @@ namespace smt { expr * deAliasedEqConcat = dealias_node(eqConcat, varAliasMap, concatAliasMap); get_grounded_concats(depth + 1, deAliasedEqConcat, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap); - std::map, std::set >::iterator grdItor = groundedMap[deAliasedEqConcat].begin(); - for (; grdItor != groundedMap[deAliasedEqConcat].end(); grdItor++) { + for (auto const &grdItor : groundedMap[deAliasedEqConcat]) { std::vector ndVec; - ndVec.insert(ndVec.end(), grdItor->first.begin(), grdItor->first.end()); + ndVec.insert(ndVec.end(), grdItor.first.begin(), grdItor.first.end()); // only insert if we don't know "node = concat(ndVec)" since one set of condition leads to this is enough if (groundedMap[node].find(ndVec) == groundedMap[node].end()) { // condition: node = deAliasedEqConcat groundedMap[node][ndVec].insert(ctx.mk_eq_atom(node, deAliasedEqConcat)); // appending conditions for "deAliasedEqConcat = CONCAT(ndVec)" - groundedMap[node][ndVec].insert(grdItor->second.begin(), grdItor->second.end()); + groundedMap[node][ndVec].insert(grdItor.second.begin(), grdItor.second.end()); } } } @@ -5532,19 +5523,16 @@ namespace smt { void theory_str::print_grounded_concat(expr * node, std::map, std::set > > & groundedMap) { TRACE("str", tout << mk_pp(node, get_manager()) << std::endl;); if (groundedMap.find(node) != groundedMap.end()) { - std::map, std::set >::iterator itor = groundedMap[node].begin(); - for (; itor != groundedMap[node].end(); ++itor) { + for (auto const &itor : groundedMap[node]) { TRACE("str", tout << "\t[grounded] "; - std::vector::const_iterator vIt = itor->first.begin(); - for (; vIt != itor->first.end(); ++vIt) { - tout << mk_pp(*vIt, get_manager()) << ", "; + for (auto const &vIt : itor.first) { + tout << mk_pp(vIt, get_manager()) << ", "; } tout << std::endl; tout << "\t[condition] "; - std::set::iterator sIt = itor->second.begin(); - for (; sIt != itor->second.end(); sIt++) { - tout << mk_pp(*sIt, get_manager()) << ", "; + for (auto const &sIt : itor.second) { + tout << mk_pp(sIt, get_manager()) << ", "; } tout << std::endl; ); @@ -5659,12 +5647,9 @@ namespace smt { std::map, std::set > > & groundedMap) { ast_manager & m = get_manager(); - std::map, std::set >::iterator itorStr = groundedMap[strDeAlias].begin(); - std::map, std::set >::iterator itorSubStr; - for (; itorStr != groundedMap[strDeAlias].end(); itorStr++) { - itorSubStr = groundedMap[subStrDeAlias].begin(); - for (; itorSubStr != groundedMap[subStrDeAlias].end(); itorSubStr++) { - bool contain = is_partial_in_grounded_concat(itorStr->first, itorSubStr->first); + for (auto const &itorStr : groundedMap[strDeAlias]) { + for (auto const &itorSubStr : groundedMap[subStrDeAlias]) { + bool contain = is_partial_in_grounded_concat(itorStr.first, itorSubStr.first); if (contain) { expr_ref_vector litems(m); if (str != strDeAlias) { @@ -5674,15 +5659,11 @@ namespace smt { litems.push_back(ctx.mk_eq_atom(subStr, subStrDeAlias)); } - //litems.insert(itorStr->second.begin(), itorStr->second.end()); - //litems.insert(itorSubStr->second.begin(), itorSubStr->second.end()); - for (std::set::const_iterator i1 = itorStr->second.begin(); - i1 != itorStr->second.end(); ++i1) { - litems.push_back(*i1); + for (auto const &i1: itorStr.second) { + litems.push_back(i1); } - for (std::set::const_iterator i1 = itorSubStr->second.begin(); - i1 != itorSubStr->second.end(); ++i1) { - litems.push_back(*i1); + for (auto const &i1 : itorSubStr.second) { + litems.push_back(i1); } expr_ref implyR(boolVar, m); @@ -6094,201 +6075,6 @@ namespace smt { return no_assertions; } - // Convert a regular expression to an e-NFA using Thompson's construction - void nfa::convert_re(expr * e, unsigned & start, unsigned & end, seq_util & u) { - start = next_id(); - end = next_id(); - if (u.re.is_to_re(e)) { - app * a = to_app(e); - expr * arg_str = a->get_arg(0); - zstring str; - if (u.str.is_string(arg_str, str)) { - if (str.length() == 0) { - // transitioning on the empty string is handled specially - TRACE("str", tout << "empty string epsilon-move " << start << " --> " << end << std::endl;); - make_epsilon_move(start, end); - } else { - TRACE("str", tout << "build NFA for '" << str << "'" << "\n";); - /* - * For an n-character string, we make (n-1) intermediate states, - * labelled i_(0) through i_(n-2). - * Then we construct the following transitions: - * start --str[0]--> i_(0) --str[1]--> i_(1) --...--> i_(n-2) --str[n-1]--> final - */ - unsigned last = start; - for (int i = 0; i <= ((int)str.length()) - 2; ++i) { - unsigned i_state = next_id(); - make_transition(last, str[i], i_state); - TRACE("str", tout << "string transition " << last << "--" << str[i] << "--> " << i_state << "\n";); - last = i_state; - } - make_transition(last, str[(str.length() - 1)], end); - TRACE("str", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";); - } - } else { // ! u.str.is_string(arg_str, str) - TRACE("str", tout << "WARNING: invalid string constant in str.to.re! Cancelling." << std::endl;); - u.get_manager().raise_exception("invalid term in str.to.re, argument must be a string constant"); - m_valid = false; - return; - } - } else if (u.re.is_concat(e)){ - app * a = to_app(e); - expr * re1 = a->get_arg(0); - expr * re2 = a->get_arg(1); - unsigned start1, end1; - convert_re(re1, start1, end1, u); - unsigned start2, end2; - convert_re(re2, start2, end2, u); - // start --e--> start1 --...--> end1 --e--> start2 --...--> end2 --e--> end - make_epsilon_move(start, start1); - make_epsilon_move(end1, start2); - make_epsilon_move(end2, end); - TRACE("str", tout << "concat NFA: start = " << start << ", end = " << end << std::endl;); - } else if (u.re.is_union(e)) { - app * a = to_app(e); - expr * re1 = a->get_arg(0); - expr * re2 = a->get_arg(1); - unsigned start1, end1; - convert_re(re1, start1, end1, u); - unsigned start2, end2; - convert_re(re2, start2, end2, u); - - // start --e--> start1 ; start --e--> start2 - // end1 --e--> end ; end2 --e--> end - make_epsilon_move(start, start1); - make_epsilon_move(start, start2); - make_epsilon_move(end1, end); - make_epsilon_move(end2, end); - TRACE("str", tout << "union NFA: start = " << start << ", end = " << end << std::endl;); - } else if (u.re.is_star(e)) { - app * a = to_app(e); - expr * subex = a->get_arg(0); - unsigned start_subex, end_subex; - convert_re(subex, start_subex, end_subex, u); - // start --e--> start_subex, start --e--> end - // end_subex --e--> start_subex, end_subex --e--> end - make_epsilon_move(start, start_subex); - make_epsilon_move(start, end); - make_epsilon_move(end_subex, start_subex); - make_epsilon_move(end_subex, end); - TRACE("str", tout << "star NFA: start = " << start << ", end = " << end << std::endl;); - } else if (u.re.is_range(e)) { - // range('a', 'z') - // start --'a'--> end - // start --'b'--> end - // ... - // start --'z'--> end - app * a = to_app(e); - expr * c1 = a->get_arg(0); - expr * c2 = a->get_arg(1); - zstring s_c1, s_c2; - u.str.is_string(c1, s_c1); - u.str.is_string(c2, s_c2); - - unsigned int id1 = s_c1[0]; - unsigned int id2 = s_c2[0]; - if (id1 > id2) { - unsigned int tmp = id1; - id1 = id2; - id2 = tmp; - } - - for (unsigned int i = id1; i <= id2; ++i) { - char ch = (char)i; - make_transition(start, ch, end); - } - - TRACE("str", tout << "range NFA: start = " << start << ", end = " << end << std::endl;); - } else if (u.re.is_full_seq(e)) { - // effectively the same as .* where . can be any single character - // start --e--> tmp - // tmp --e--> end - // tmp --C--> tmp for every character C - unsigned tmp = next_id(); - make_epsilon_move(start, tmp); - make_epsilon_move(tmp, end); - for (unsigned int i = 0; i < 256; ++i) { - char ch = (char)i; - make_transition(tmp, ch, tmp); - } - TRACE("str", tout << "re.all NFA: start = " << start << ", end = " << end << std::endl;); - } else if (u.re.is_full_char(e)) { - // effectively . (match any one character) - for (unsigned int i = 0; i < 256; ++i) { - char ch = (char)i; - make_transition(start, ch, end); - } - TRACE("str", tout << "re.allchar NFA: start = " << start << ", end = " << end << std::endl;); - } else { - TRACE("str", tout << "invalid regular expression" << std::endl;); - m_valid = false; - return; - } - } - - void nfa::epsilon_closure(unsigned start, std::set & closure) { - std::deque worklist; - closure.insert(start); - worklist.push_back(start); - - while(!worklist.empty()) { - unsigned state = worklist.front(); - worklist.pop_front(); - if (epsilon_map.find(state) != epsilon_map.end()) { - for (std::set::iterator it = epsilon_map[state].begin(); - it != epsilon_map[state].end(); ++it) { - unsigned new_state = *it; - if (closure.find(new_state) == closure.end()) { - closure.insert(new_state); - worklist.push_back(new_state); - } - } - } - } - } - - bool nfa::matches(zstring input) { - /* - * Keep a set of all states the NFA can currently be in. - * Initially this is the e-closure of m_start_state - * For each character A in the input string, - * the set of next states contains - * all states in transition_map[S][A] for each S in current_states, - * and all states in epsilon_map[S] for each S in current_states. - * After consuming the entire input string, - * the match is successful iff current_states contains m_end_state. - */ - std::set current_states; - epsilon_closure(m_start_state, current_states); - for (unsigned i = 0; i < input.length(); ++i) { - char A = (char)input[i]; - std::set next_states; - for (std::set::iterator it = current_states.begin(); - it != current_states.end(); ++it) { - unsigned S = *it; - // check transition_map - if (transition_map[S].find(A) != transition_map[S].end()) { - next_states.insert(transition_map[S][A]); - } - } - - // take e-closure over next_states to compute the actual next_states - std::set epsilon_next_states; - for (std::set::iterator it = next_states.begin(); it != next_states.end(); ++it) { - unsigned S = *it; - std::set closure; - epsilon_closure(S, closure); - epsilon_next_states.insert(closure.begin(), closure.end()); - } - current_states = epsilon_next_states; - } - if (current_states.find(m_end_state) != current_states.end()) { - return true; - } else { - return false; - } - } - /* * strArgmt::solve_concat_eq_str() * Solve concatenations of the form: @@ -6710,35 +6496,29 @@ namespace smt { TRACE("str", tout << "lhs eqc:" << std::endl; tout << "Concats:" << std::endl; - for (std::set::iterator it = eqc_concat_lhs.begin(); it != eqc_concat_lhs.end(); ++it) { - expr * ex = *it; + for (auto const &ex : eqc_concat_lhs) { tout << mk_ismt2_pp(ex, get_manager()) << std::endl; } tout << "Variables:" << std::endl; - for (std::set::iterator it = eqc_var_lhs.begin(); it != eqc_var_lhs.end(); ++it) { - expr * ex = *it; + for (auto const &ex : eqc_var_lhs) { tout << mk_ismt2_pp(ex, get_manager()) << std::endl; } tout << "Constants:" << std::endl; - for (std::set::iterator it = eqc_const_lhs.begin(); it != eqc_const_lhs.end(); ++it) { - expr * ex = *it; + for (auto const &ex : eqc_const_lhs) { tout << mk_ismt2_pp(ex, get_manager()) << std::endl; } tout << "rhs eqc:" << std::endl; tout << "Concats:" << std::endl; - for (std::set::iterator it = eqc_concat_rhs.begin(); it != eqc_concat_rhs.end(); ++it) { - expr * ex = *it; + for (auto const &ex : eqc_concat_rhs) { tout << mk_ismt2_pp(ex, get_manager()) << std::endl; } tout << "Variables:" << std::endl; - for (std::set::iterator it = eqc_var_rhs.begin(); it != eqc_var_rhs.end(); ++it) { - expr * ex = *it; + for (auto const &ex : eqc_var_rhs) { tout << mk_ismt2_pp(ex, get_manager()) << std::endl; } tout << "Constants:" << std::endl; - for (std::set::iterator it = eqc_const_rhs.begin(); it != eqc_const_rhs.end(); ++it) { - expr * ex = *it; + for (auto const &ex : eqc_const_rhs) { tout << mk_ismt2_pp(ex, get_manager()) << std::endl; } ); @@ -6750,15 +6530,13 @@ namespace smt { if (!eqc_const_lhs.empty()) { expr * conStr = *(eqc_const_lhs.begin()); - std::set::iterator itor2 = eqc_concat_rhs.begin(); - for (; itor2 != eqc_concat_rhs.end(); itor2++) { - solve_concat_eq_str(*itor2, conStr); + for (auto const &itor2 : eqc_concat_rhs) { + solve_concat_eq_str(itor2, conStr); } } else if (!eqc_const_rhs.empty()) { expr* conStr = *(eqc_const_rhs.begin()); - std::set::iterator itor1 = eqc_concat_lhs.begin(); - for (; itor1 != eqc_concat_lhs.end(); itor1++) { - solve_concat_eq_str(*itor1, conStr); + for (auto const &itor1 : eqc_concat_lhs) { + solve_concat_eq_str(itor1, conStr); } } @@ -6811,16 +6589,14 @@ namespace smt { int hasCommon = 0; if (!eqc_concat_lhs.empty() && !eqc_concat_rhs.empty()) { - std::set::iterator itor1 = eqc_concat_lhs.begin(); - std::set::iterator itor2 = eqc_concat_rhs.begin(); - for (; itor1 != eqc_concat_lhs.end(); itor1++) { - if (eqc_concat_rhs.find(*itor1) != eqc_concat_rhs.end()) { + for (auto const &itor1 : eqc_concat_lhs) { + if (eqc_concat_rhs.find(itor1) != eqc_concat_rhs.end()) { hasCommon = 1; break; } } - for (; itor2 != eqc_concat_rhs.end(); itor2++) { - if (eqc_concat_lhs.find(*itor2) != eqc_concat_lhs.end()) { + for (auto const &itor2 : eqc_concat_rhs) { + if (eqc_concat_lhs.find(itor2) != eqc_concat_lhs.end()) { hasCommon = 1; break; } @@ -6829,10 +6605,11 @@ namespace smt { if (opt_ConcatOverlapAvoid) { bool found = false; // check each pair and take the first ones that won't immediately overlap - for (itor1 = eqc_concat_lhs.begin(); itor1 != eqc_concat_lhs.end() && !found; ++itor1) { - expr * concat_lhs = *itor1; - for (itor2 = eqc_concat_rhs.begin(); itor2 != eqc_concat_rhs.end() && !found; ++itor2) { - expr * concat_rhs = *itor2; + for (auto const &concat_lhs : eqc_concat_lhs) { + if (found) { + break; + } + for (auto const &concat_rhs : eqc_concat_rhs) { if (will_result_in_overlap(concat_lhs, concat_rhs)) { TRACE("str", tout << "Concats " << mk_pp(concat_lhs, m) << " and " << mk_pp(concat_rhs, m) << " will result in overlap; skipping." << std::endl;); @@ -7045,8 +6822,7 @@ namespace smt { expr_ref_vector formulas(get_manager()); ctx.get_assignments(formulas); tout << "dumping all formulas:" << std::endl; - for (expr_ref_vector::iterator i = formulas.begin(); i != formulas.end(); ++i) { - expr * ex = *i; + for (auto const &ex : formulas) { tout << mk_pp(ex, get_manager()) << (ctx.is_relevant(ex) ? "" : " (NOT REL)") << std::endl; } ); @@ -7257,8 +7033,7 @@ namespace smt { expr_ref_vector assignments(m); ctx.get_assignments(assignments); - for (expr_ref_vector::iterator i = assignments.begin(); i != assignments.end(); ++i) { - expr * ex = *i; + for (auto const &ex : assignments) { recursive_check_variable_scope(ex); } } @@ -7283,9 +7058,8 @@ namespace smt { // list of expr* to remove from cut_var_map ptr_vector cutvarmap_removes; - obj_map >::iterator varItor = cut_var_map.begin(); - while (varItor != cut_var_map.end()) { - std::stack & val = cut_var_map[varItor->m_key]; + for (auto const &varItor : cut_var_map) { + std::stack & val = cut_var_map[varItor.m_key]; while ((!val.empty()) && (val.top()->level != 0) && (val.top()->level >= sLevel)) { // TRACE("str", tout << "remove cut info for " << mk_pp(e, get_manager()) << std::endl; print_cut_var(e, tout);); // T_cut * aCut = val.top(); @@ -7293,9 +7067,8 @@ namespace smt { // dealloc(aCut); } if (val.empty()) { - cutvarmap_removes.insert(varItor->m_key); + cutvarmap_removes.insert(varItor.m_key); } - varItor++; } for (expr* ex : cutvarmap_removes) @@ -7335,11 +7108,10 @@ namespace smt { tout << "dumping all assignments:" << std::endl; expr_ref_vector assignments(m); ctx.get_assignments(assignments); - for (expr_ref_vector::iterator i = assignments.begin(); i != assignments.end(); ++i) { - expr * ex = *i; + for (auto const &ex : assignments) { tout << mk_ismt2_pp(ex, m) << (ctx.is_relevant(ex) ? "" : " (NOT REL)") << std::endl; } - ); + ); } // returns true if needle appears as a subterm anywhere under haystack, @@ -7411,8 +7183,6 @@ namespace smt { } } - // NOTE: this function used to take an argument `Z3_ast node`; - // it was not used and so was removed from the signature void theory_str::classify_ast_by_type_in_positive_context(std::map & varMap, std::map & concatMap, std::map & unrollMap) { @@ -7420,8 +7190,7 @@ namespace smt { expr_ref_vector assignments(m); ctx.get_assignments(assignments); - for (expr_ref_vector::iterator it = assignments.begin(); it != assignments.end(); ++it) { - expr * argAst = *it; + for (auto const &argAst : assignments) { // the original code jumped through some hoops to check whether the AST node // is a function, then checked whether that function is "interesting". // however, the only thing that's considered "interesting" is an equality predicate. @@ -7470,25 +7239,21 @@ namespace smt { std::map > & var_eq_concat_map, std::map > & var_eq_unroll_map, std::map & concat_eq_constStr_map, - std::map > & concat_eq_concat_map, - std::map > & unrollGroupMap) { + std::map > & concat_eq_concat_map) { #ifdef _TRACE ast_manager & mgr = get_manager(); { tout << "(0) alias: variables" << std::endl; std::map > aliasSumMap; - std::map::iterator itor0 = aliasIndexMap.begin(); - for (; itor0 != aliasIndexMap.end(); itor0++) { - aliasSumMap[itor0->second][itor0->first] = 1; + for (auto const &itor0 : aliasIndexMap) { + aliasSumMap[itor0.second][itor0.first] = 1; } - std::map >::iterator keyItor = aliasSumMap.begin(); - for (; keyItor != aliasSumMap.end(); keyItor++) { + for (auto const &keyItor : aliasSumMap) { tout << " * "; - tout << mk_pp(keyItor->first, mgr); + tout << mk_pp(keyItor.first, mgr); tout << " : "; - std::map::iterator innerItor = keyItor->second.begin(); - for (; innerItor != keyItor->second.end(); innerItor++) { - tout << mk_pp(innerItor->first, mgr); + for (auto const &innerItor : keyItor.second) { + tout << mk_pp(innerItor.first, mgr); tout << ", "; } tout << std::endl; @@ -7498,13 +7263,12 @@ namespace smt { { tout << "(1) var = constStr:" << std::endl; - std::map::iterator itor1 = var_eq_constStr_map.begin(); - for (; itor1 != var_eq_constStr_map.end(); itor1++) { + for (auto const &itor1 : var_eq_constStr_map) { tout << " * "; - tout << mk_pp(itor1->first, mgr); + tout << mk_pp(itor1.first, mgr); tout << " = "; - tout << mk_pp(itor1->second, mgr); - if (!in_same_eqc(itor1->first, itor1->second)) { + tout << mk_pp(itor1.second, mgr); + if (!in_same_eqc(itor1.first, itor1.second)) { tout << " (not true in ctx)"; } tout << std::endl; @@ -7514,14 +7278,12 @@ namespace smt { { tout << "(2) var = concat:" << std::endl; - std::map >::iterator itor2 = var_eq_concat_map.begin(); - for (; itor2 != var_eq_concat_map.end(); itor2++) { + for (auto const &itor2 : var_eq_concat_map) { tout << " * "; - tout << mk_pp(itor2->first, mgr); + tout << mk_pp(itor2.first, mgr); tout << " = { "; - std::map::iterator i_itor = itor2->second.begin(); - for (; i_itor != itor2->second.end(); i_itor++) { - tout << mk_pp(i_itor->first, mgr); + for (auto const &i_itor : itor2.second) { + tout << mk_pp(i_itor.first, mgr); tout << ", "; } tout << std::endl; @@ -7531,12 +7293,10 @@ namespace smt { { tout << "(3) var = unrollFunc:" << std::endl; - std::map >::iterator itor2 = var_eq_unroll_map.begin(); - for (; itor2 != var_eq_unroll_map.end(); itor2++) { - tout << " * " << mk_pp(itor2->first, mgr) << " = { "; - std::map::iterator i_itor = itor2->second.begin(); - for (; i_itor != itor2->second.end(); i_itor++) { - tout << mk_pp(i_itor->first, mgr) << ", "; + for (auto const &itor2 : var_eq_unroll_map) { + tout << " * " << mk_pp(itor2.first, mgr) << " = { "; + for (auto const &i_itor : itor2.second) { + tout << mk_pp(i_itor.first, mgr) << ", "; } tout << " }" << std::endl; } @@ -7545,12 +7305,11 @@ namespace smt { { tout << "(4) concat = constStr:" << std::endl; - std::map::iterator itor3 = concat_eq_constStr_map.begin(); - for (; itor3 != concat_eq_constStr_map.end(); itor3++) { + for (auto const &itor3 : concat_eq_constStr_map) { tout << " * "; - tout << mk_pp(itor3->first, mgr); + tout << mk_pp(itor3.first, mgr); tout << " = "; - tout << mk_pp(itor3->second, mgr); + tout << mk_pp(itor3.second, mgr); tout << std::endl; } @@ -7559,13 +7318,11 @@ namespace smt { { tout << "(5) eq concats:" << std::endl; - std::map >::iterator itor4 = concat_eq_concat_map.begin(); - for (; itor4 != concat_eq_concat_map.end(); itor4++) { - if (itor4->second.size() > 1) { - std::map::iterator i_itor = itor4->second.begin(); + for (auto const &itor4 : concat_eq_concat_map) { + if (itor4.second.size() > 1) { tout << " * "; - for (; i_itor != itor4->second.end(); i_itor++) { - tout << mk_pp(i_itor->first, mgr); + for (auto const &i_itor : itor4.second) { + tout << mk_pp(i_itor.first, mgr); tout << " , "; } tout << std::endl; @@ -7574,40 +7331,6 @@ namespace smt { tout << std::endl; } - { - tout << "(6) eq unrolls:" << std::endl; - std::map >::iterator itor5 = unrollGroupMap.begin(); - for (; itor5 != unrollGroupMap.end(); itor5++) { - tout << " * "; - std::set::iterator i_itor = itor5->second.begin(); - for (; i_itor != itor5->second.end(); i_itor++) { - tout << mk_pp(*i_itor, mgr) << ", "; - } - tout << std::endl; - } - tout << std::endl; - } - - { - tout << "(7) unroll = concats:" << std::endl; - std::map >::iterator itor5 = unrollGroupMap.begin(); - for (; itor5 != unrollGroupMap.end(); itor5++) { - tout << " * "; - expr * unroll = itor5->first; - tout << mk_pp(unroll, mgr) << std::endl; - enode * e_curr = ctx.get_enode(unroll); - enode * e_curr_end = e_curr; - do { - app * curr = e_curr->get_expr(); - if (u.str.is_concat(curr)) { - tout << " >>> " << mk_pp(curr, mgr) << std::endl; - } - e_curr = e_curr->get_next(); - } while (e_curr != e_curr_end); - tout << std::endl; - } - tout << std::endl; - } #else return; #endif // _TRACE @@ -7627,7 +7350,7 @@ namespace smt { * > should split the unroll function so that var2 and var3 are bounded by new unrolls */ int theory_str::ctx_dep_analysis(std::map & strVarMap, std::map & freeVarMap, - std::map > & unrollGroupMap, std::map > & var_eq_concat_map) { + std::map > & var_eq_concat_map) { std::map concatMap; std::map unrollMap; std::map aliasIndexMap; @@ -7750,13 +7473,12 @@ namespace smt { // -------------------------------------------------- std::map concats_eq_index_map; - std::map::iterator concatItor = concatMap.begin(); - for(; concatItor != concatMap.end(); ++concatItor) { - if (concats_eq_index_map.find(concatItor->first) != concats_eq_index_map.end()) { + for(auto const &concatItor : concatMap) { + if (concats_eq_index_map.find(concatItor.first) != concats_eq_index_map.end()) { continue; } expr * aRoot = nullptr; - expr * curr = concatItor->first; + expr * curr = concatItor.first; do { if (u.str.is_concat(to_app(curr))) { if (aRoot == nullptr) { @@ -7766,16 +7488,15 @@ namespace smt { } } curr = get_eqc_next(curr); - } while (curr != concatItor->first); + } while (curr != concatItor.first); } - concatItor = concatMap.begin(); - for(; concatItor != concatMap.end(); ++concatItor) { + for(auto const &concatItor : concatMap) { expr * deAliasConcat = nullptr; - if (concats_eq_index_map.find(concatItor->first) != concats_eq_index_map.end()) { - deAliasConcat = concats_eq_index_map[concatItor->first]; + if (concats_eq_index_map.find(concatItor.first) != concats_eq_index_map.end()) { + deAliasConcat = concats_eq_index_map[concatItor.first]; } else { - deAliasConcat = concatItor->first; + deAliasConcat = concatItor.first; } // (3) concat_eq_conststr, e.g. concat(a,b) = "str1" @@ -7806,7 +7527,7 @@ namespace smt { // print some debugging info TRACE("str", trace_ctx_dep(tout, aliasIndexMap, var_eq_constStr_map, var_eq_concat_map, var_eq_unroll_map, - concat_eq_constStr_map, concat_eq_concat_map, unrollGroupMap);); + concat_eq_constStr_map, concat_eq_concat_map);); /* if (!contain_pair_bool_map.empty()) { @@ -7817,25 +7538,23 @@ namespace smt { // step 4: dependence analysis // (1) var = string constant - for (std::map::iterator itor = var_eq_constStr_map.begin(); - itor != var_eq_constStr_map.end(); ++itor) { - expr * var = get_alias_index_ast(aliasIndexMap, itor->first); - expr * strAst = itor->second; + for (auto const &itor : var_eq_constStr_map) { + expr * var = get_alias_index_ast(aliasIndexMap, itor.first); + expr * strAst = itor.second; depMap[var][strAst] = 1; } // (2) var = concat - for (std::map >::iterator itor = var_eq_concat_map.begin(); - itor != var_eq_concat_map.end(); ++itor) { - expr * var = get_alias_index_ast(aliasIndexMap, itor->first); - for (std::map::iterator itor1 = itor->second.begin(); itor1 != itor->second.end(); ++itor1) { - expr * concat = itor1->first; + for (auto const &itor : var_eq_concat_map) { + expr * var = get_alias_index_ast(aliasIndexMap, itor.first); + for (auto const &itor1 : itor.second) { + expr * concat = itor1.first; std::map inVarMap; std::map inConcatMap; std::map inUnrollMap; classify_ast_by_type(concat, inVarMap, inConcatMap, inUnrollMap); - for (std::map::iterator itor2 = inVarMap.begin(); itor2 != inVarMap.end(); ++itor2) { - expr * varInConcat = get_alias_index_ast(aliasIndexMap, itor2->first); + for (auto const &itor2 : inVarMap) { + expr * varInConcat = get_alias_index_ast(aliasIndexMap, itor2.first); if (!(depMap[var].find(varInConcat) != depMap[var].end() && depMap[var][varInConcat] == 1)) { depMap[var][varInConcat] = 2; } @@ -7843,20 +7562,19 @@ namespace smt { } } - for (std::map >::iterator itor = var_eq_unroll_map.begin(); - itor != var_eq_unroll_map.end(); itor++) { - expr * var = get_alias_index_ast(aliasIndexMap, itor->first); - for (std::map::iterator itor1 = itor->second.begin(); itor1 != itor->second.end(); itor1++) { - expr * unrollFunc = itor1->first; + for (auto const &itor : var_eq_unroll_map) { + expr * var = get_alias_index_ast(aliasIndexMap, itor.first); + for (auto const &itor1 : itor.second) { + expr * unrollFunc = itor1.first; std::map inVarMap; std::map inConcatMap; std::map inUnrollMap; classify_ast_by_type(unrollFunc, inVarMap, inConcatMap, inUnrollMap); - for (std::map::iterator itor2 = inVarMap.begin(); itor2 != inVarMap.end(); itor2++) { - expr * varInFunc = get_alias_index_ast(aliasIndexMap, itor2->first); + for (auto const &itor2 : inVarMap) { + expr * varInFunc = get_alias_index_ast(aliasIndexMap, itor2.first); TRACE("str", tout << "var in unroll = " << - mk_ismt2_pp(itor2->first, m) << std::endl + mk_ismt2_pp(itor2.first, m) << std::endl << "dealiased var = " << mk_ismt2_pp(varInFunc, m) << std::endl;); // it's possible that we have both (Unroll $$_regVar_0 $$_unr_0) /\ (Unroll abcd $$_unr_0), @@ -7875,16 +7593,15 @@ namespace smt { } // (3) concat = string constant - for (std::map::iterator itor = concat_eq_constStr_map.begin(); - itor != concat_eq_constStr_map.end(); itor++) { - expr * concatAst = itor->first; - expr * constStr = itor->second; + for (auto const &itor : concat_eq_constStr_map) { + expr * concatAst = itor.first; + expr * constStr = itor.second; std::map inVarMap; std::map inConcatMap; std::map inUnrollMap; classify_ast_by_type(concatAst, inVarMap, inConcatMap, inUnrollMap); - for (std::map::iterator itor2 = inVarMap.begin(); itor2 != inVarMap.end(); itor2++) { - expr * varInConcat = get_alias_index_ast(aliasIndexMap, itor2->first); + for (auto const &itor2 : inVarMap) { + expr * varInConcat = get_alias_index_ast(aliasIndexMap, itor2.first); if (!(depMap[varInConcat].find(constStr) != depMap[varInConcat].end() && depMap[varInConcat][constStr] == 1)) depMap[varInConcat][constStr] = 3; } @@ -7906,16 +7623,15 @@ namespace smt { std::map > mRMap; std::set nSet; - for (std::map >::iterator itor = concat_eq_concat_map.begin(); - itor != concat_eq_concat_map.end(); itor++) { + for (auto const &itor : concat_eq_concat_map) { mostLeftNodes.clear(); mostRightNodes.clear(); expr * mLConst = nullptr; expr * mRConst = nullptr; - for (std::map::iterator itor1 = itor->second.begin(); itor1 != itor->second.end(); itor1++) { - expr * concatNode = itor1->first; + for (auto const &itor1 : itor.second) { + expr * concatNode = itor1.first; expr * mLNode = getMostLeftNodeInConcat(concatNode); zstring strval; if (u.str.is_string(to_app(mLNode), strval)) { @@ -7942,9 +7658,8 @@ namespace smt { // ------------------------------------------------------------------------------------- // e.g. Concat(x, ...) = Concat("abc", ...) // ------------------------------------------------------------------------------------- - for (std::map::iterator itor1 = mostLeftNodes.begin(); - itor1 != mostLeftNodes.end(); itor1++) { - expr * deVar = get_alias_index_ast(aliasIndexMap, itor1->first); + for (auto const &itor1 : mostLeftNodes) { + expr * deVar = get_alias_index_ast(aliasIndexMap, itor1.first); if (depMap[deVar].find(mLConst) == depMap[deVar].end() || depMap[deVar][mLConst] != 1) { depMap[deVar][mLConst] = 4; } @@ -7959,41 +7674,39 @@ namespace smt { // x and u are constrained by each other // ------------------------------------------------------------------------------------- nSet.clear(); - std::map::iterator itl = mostLeftNodes.begin(); - for (; itl != mostLeftNodes.end(); itl++) { + for (auto const &itl : mostLeftNodes) { bool lfHasEqcValue = false; - get_eqc_value(itl->first, lfHasEqcValue); + get_eqc_value(itl.first, lfHasEqcValue); if (lfHasEqcValue) continue; - expr * deVar = get_alias_index_ast(aliasIndexMap, itl->first); + expr * deVar = get_alias_index_ast(aliasIndexMap, itl.first); nSet.insert(deVar); } if (nSet.size() > 1) { int lId = -1; - for (std::set::iterator itor2 = nSet.begin(); itor2 != nSet.end(); itor2++) { - if (mLIdxMap.find(*itor2) != mLIdxMap.end()) { - lId = mLIdxMap[*itor2]; + for (auto const &itor2 : nSet) { + if (mLIdxMap.find(itor2) != mLIdxMap.end()) { + lId = mLIdxMap[itor2]; break; } } if (lId == -1) lId = static_cast(mLMap.size()); - for (std::set::iterator itor2 = nSet.begin(); itor2 != nSet.end(); itor2++) { + for (auto const &itor2 : nSet) { bool itorHasEqcValue = false; - get_eqc_value(*itor2, itorHasEqcValue); + get_eqc_value(itor2, itorHasEqcValue); if (itorHasEqcValue) continue; - mLIdxMap[*itor2] = lId; - mLMap[lId].insert(*itor2); + mLIdxMap[itor2] = lId; + mLMap[lId].insert(itor2); } } } if (mRConst != nullptr) { - for (std::map::iterator itor1 = mostRightNodes.begin(); - itor1 != mostRightNodes.end(); itor1++) { - expr * deVar = get_alias_index_ast(aliasIndexMap, itor1->first); + for (auto const &itor1 : mostRightNodes) { + expr * deVar = get_alias_index_ast(aliasIndexMap, itor1.first); if (depMap[deVar].find(mRConst) == depMap[deVar].end() || depMap[deVar][mRConst] != 1) { depMap[deVar][mRConst] = 5; } @@ -8002,29 +7715,27 @@ namespace smt { { nSet.clear(); - std::map::iterator itr = mostRightNodes.begin(); - for (; itr != mostRightNodes.end(); itr++) { - expr * deVar = get_alias_index_ast(aliasIndexMap, itr->first); + for (auto const &itr : mostRightNodes) { + expr * deVar = get_alias_index_ast(aliasIndexMap, itr.first); nSet.insert(deVar); } if (nSet.size() > 1) { int rId = -1; - std::set::iterator itor2 = nSet.begin(); - for (; itor2 != nSet.end(); itor2++) { - if (mRIdxMap.find(*itor2) != mRIdxMap.end()) { - rId = mRIdxMap[*itor2]; + for (auto const &itor2 : nSet) { + if (mRIdxMap.find(itor2) != mRIdxMap.end()) { + rId = mRIdxMap[itor2]; break; } } if (rId == -1) rId = static_cast(mRMap.size()); - for (itor2 = nSet.begin(); itor2 != nSet.end(); itor2++) { + for (auto const &itor2 : nSet) { bool rHasEqcValue = false; - get_eqc_value(*itor2, rHasEqcValue); + get_eqc_value(itor2, rHasEqcValue); if (rHasEqcValue) continue; - mRIdxMap[*itor2] = rId; - mRMap[rId].insert(*itor2); + mRIdxMap[itor2] = rId; + mRMap[rId].insert(itor2); } } } @@ -8033,13 +7744,13 @@ namespace smt { // print the dependence map TRACE("str", tout << "Dependence Map" << std::endl; - for(std::map >::iterator itor = depMap.begin(); itor != depMap.end(); itor++) { - tout << mk_pp(itor->first, m); + for(auto const &itor : depMap) { + tout << mk_pp(itor.first, m); rational nnLen; - bool nnLen_exists = get_len_value(itor->first, nnLen); + bool nnLen_exists = get_len_value(itor.first, nnLen); tout << " [len = " << (nnLen_exists ? nnLen.to_string() : "?") << "] \t-->\t"; - for (std::map::iterator itor1 = itor->second.begin(); itor1 != itor->second.end(); itor1++) { - tout << mk_pp(itor1->first, m) << "(" << itor1->second << "), "; + for (auto const &itor1 : itor.second) { + tout << mk_pp(itor1.first, m) << "(" << itor1.second << "), "; } tout << std::endl; } @@ -8051,11 +7762,11 @@ namespace smt { //--------------------------------------------------------------- // remove L/R most var in eq concat since they are constrained with each other std::map > lrConstrainedMap; - for (std::map >::iterator itor = mLMap.begin(); itor != mLMap.end(); itor++) { - for (std::set::iterator it1 = itor->second.begin(); it1 != itor->second.end(); it1++) { + for (auto const &itor : mLMap) { + for (std::set::iterator it1 = itor.second.begin(); it1 != itor.second.end(); it1++) { std::set::iterator it2 = it1; it2++; - for (; it2 != itor->second.end(); it2++) { + for (; it2 != itor.second.end(); it2++) { expr * n1 = *it1; expr * n2 = *it2; lrConstrainedMap[n1][n2] = 1; @@ -8063,11 +7774,11 @@ namespace smt { } } } - for (std::map >::iterator itor = mRMap.begin(); itor != mRMap.end(); itor++) { - for (std::set::iterator it1 = itor->second.begin(); it1 != itor->second.end(); it1++) { + for (auto const &itor : mRMap) { + for (std::set::iterator it1 = itor.second.begin(); it1 != itor.second.end(); it1++) { std::set::iterator it2 = it1; it2++; - for (; it2 != itor->second.end(); it2++) { + for (; it2 != itor.second.end(); it2++) { expr * n1 = *it1; expr * n2 = *it2; lrConstrainedMap[n1][n2] = 1; @@ -8077,16 +7788,14 @@ namespace smt { } if (depMap.empty()) { - std::map::iterator itor = strVarMap.begin(); - for (; itor != strVarMap.end(); itor++) { - expr * var = get_alias_index_ast(aliasIndexMap, itor->first); + for (auto const &itor : strVarMap) { + expr * var = get_alias_index_ast(aliasIndexMap, itor.first); if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) { freeVarMap[var] = 1; } else { int lrConstrained = 0; - std::map::iterator lrit = freeVarMap.begin(); - for (; lrit != freeVarMap.end(); lrit++) { - if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) { + for (auto const &lrit : freeVarMap) { + if (lrConstrainedMap[var].find(lrit.first) != lrConstrainedMap[var].end()) { lrConstrained = 1; break; } @@ -8102,18 +7811,16 @@ namespace smt { // aliasIndexMap[y]= x, aliasIndexMap[z] = x // depMap t ~ "abc"(1) // x should be free - std::map::iterator itor2 = strVarMap.begin(); - for (; itor2 != strVarMap.end(); itor2++) { - if (aliasIndexMap.find(itor2->first) != aliasIndexMap.end()) { - expr * var = aliasIndexMap[itor2->first]; + for (auto const &itor2 : strVarMap) { + if (aliasIndexMap.find(itor2.first) != aliasIndexMap.end()) { + expr * var = aliasIndexMap[itor2.first]; if (depMap.find(var) == depMap.end()) { if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) { freeVarMap[var] = 1; } else { int lrConstrained = 0; - std::map::iterator lrit = freeVarMap.begin(); - for (; lrit != freeVarMap.end(); lrit++) { - if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) { + for (auto const &lrit : freeVarMap) { + if (lrConstrainedMap[var].find(lrit.first) != lrConstrainedMap[var].end()) { lrConstrained = 1; break; } @@ -8123,17 +7830,16 @@ namespace smt { } } } - } else if (aliasIndexMap.find(itor2->first) == aliasIndexMap.end()) { + } else if (aliasIndexMap.find(itor2.first) == aliasIndexMap.end()) { // if a variable is not in aliasIndexMap and not in depMap, it's free - if (depMap.find(itor2->first) == depMap.end()) { - expr * var = itor2->first; + if (depMap.find(itor2.first) == depMap.end()) { + expr * var = itor2.first; if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) { freeVarMap[var] = 1; } else { int lrConstrained = 0; - std::map::iterator lrit = freeVarMap.begin(); - for (; lrit != freeVarMap.end(); lrit++) { - if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) { + for (auto const &lrit : freeVarMap) { + if (lrConstrainedMap[var].find(lrit.first) != lrConstrainedMap[var].end()) { lrConstrained = 1; break; } @@ -8146,11 +7852,10 @@ namespace smt { } } - std::map >::iterator itor = depMap.begin(); - for (; itor != depMap.end(); itor++) { - for (std::map::iterator itor1 = itor->second.begin(); itor1 != itor->second.end(); itor1++) { - if (variable_set.find(itor1->first) != variable_set.end()) { // expr type = var - expr * var = get_alias_index_ast(aliasIndexMap, itor1->first); + for (auto const &itor : depMap) { + for (auto const &itor1 : itor.second) { + if (variable_set.find(itor1.first) != variable_set.end()) { // expr type = var + expr * var = get_alias_index_ast(aliasIndexMap, itor1.first); // if a var is dep on itself and all dependence are type 2, it's a free variable // e.g {y --> x(2), y(2), m --> m(2), n(2)} y,m are free { @@ -8160,9 +7865,8 @@ namespace smt { freeVarMap[var] = 1; } else { int lrConstrained = 0; - std::map::iterator lrit = freeVarMap.begin(); - for (; lrit != freeVarMap.end(); lrit++) { - if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) { + for (auto const &lrit : freeVarMap) { + if (lrConstrainedMap[var].find(lrit.first) != lrConstrainedMap[var].end()) { lrConstrained = 1; break; } @@ -8438,18 +8142,17 @@ namespace smt { ctx.get_assignments(assignments); bool axiomAdded = false; // collect all concats in context - for (expr_ref_vector::iterator it = assignments.begin(); it != assignments.end(); ++it) { - if (! ctx.is_relevant(*it)) { + for (auto const &it : assignments) { + if (! ctx.is_relevant(it)) { continue; } - if (m.is_eq(*it)) { - collect_var_concat(*it, varSet, concatSet); + if (m.is_eq(it)) { + collect_var_concat(it, varSet, concatSet); } } // iterate each concat // if a concat doesn't have length info, check if the length of all leaf nodes can be resolved - for (std::set::iterator it = concatSet.begin(); it != concatSet.end(); it++) { - expr * concat = *it; + for (auto const &concat : concatSet) { rational lenValue; expr_ref concatlenExpr (mk_strlen(concat), m) ; bool allLeafResolved = true; @@ -8461,10 +8164,10 @@ namespace smt { std::set leafNodes; get_unique_non_concat_nodes(concat, leafNodes); expr_ref_vector l_items(m); - for (std::set::iterator leafIt = leafNodes.begin(); leafIt != leafNodes.end(); ++leafIt) { + for (auto const &leafIt : leafNodes) { rational leafLenValue; - if (get_len_value(*leafIt, leafLenValue)) { - expr_ref leafItLenExpr (mk_strlen(*leafIt), m); + if (get_len_value(leafIt, leafLenValue)) { + expr_ref leafItLenExpr (mk_strlen(leafIt), m); expr_ref leafLenValueExpr (mk_int(leafLenValue), m); expr_ref lcExpr (ctx.mk_eq_atom(leafItLenExpr, leafLenValueExpr), m); l_items.push_back(lcExpr); @@ -8486,8 +8189,7 @@ namespace smt { } // if no concat length is propagated, check the length of variables. if (! axiomAdded) { - for (std::set::iterator it = varSet.begin(); it != varSet.end(); it++) { - expr * var = *it; + for (auto const &var : varSet) { rational lenValue; expr_ref varlen (mk_strlen(var), m) ; if (! get_arith_value(varlen, lenValue)) { @@ -8532,16 +8234,14 @@ namespace smt { if (opt_DeferEQCConsistencyCheck) { TRACE("str", tout << "performing deferred EQC consistency check" << std::endl;); std::set eqc_roots; - for (ptr_vector::const_iterator it = ctx.begin_enodes(); it != ctx.end_enodes(); ++it) { - enode * e = *it; + for (auto const &e : ctx.enodes()) { enode * root = e->get_root(); eqc_roots.insert(root); } bool found_inconsistency = false; - for (std::set::iterator it = eqc_roots.begin(); it != eqc_roots.end(); ++it) { - enode * e = *it; + for (auto const &e : eqc_roots) { app * a = e->get_expr(); if (!(a->get_sort() == u.str.mk_string_sort())) { TRACE("str", tout << "EQC root " << mk_pp(a, m) << " not a string term; skipping" << std::endl;); @@ -8584,9 +8284,8 @@ namespace smt { // run dependence analysis to find free string variables std::map varAppearInAssign; std::map freeVar_map; - std::map > unrollGroup_map; std::map > var_eq_concat_map; - int conflictInDep = ctx_dep_analysis(varAppearInAssign, freeVar_map, unrollGroup_map, var_eq_concat_map); + int conflictInDep = ctx_dep_analysis(varAppearInAssign, freeVar_map, var_eq_concat_map); if (conflictInDep == -1) { m_stats.m_solved_by = 2; return FC_DONE; @@ -8594,12 +8293,10 @@ namespace smt { // enhancement: improved backpropagation of string constants into var=concat terms bool backpropagation_occurred = false; - for (std::map >::iterator veqc_map_it = var_eq_concat_map.begin(); - veqc_map_it != var_eq_concat_map.end(); ++veqc_map_it) { - expr * var = veqc_map_it->first; - for (std::map::iterator concat_map_it = veqc_map_it->second.begin(); - concat_map_it != veqc_map_it->second.end(); ++concat_map_it) { - app * concat = to_app(concat_map_it->first); + for (auto const &veqc_map_it : var_eq_concat_map) { + expr * var = veqc_map_it.first; + for (auto const &concat_map_it : veqc_map_it.second) { + app * concat = to_app(concat_map_it.first); expr * concat_lhs = concat->get_arg(0); expr * concat_rhs = concat->get_arg(1); // If the concat LHS and RHS both have a string constant in their EQC, @@ -8670,24 +8367,18 @@ namespace smt { expr_ref_vector free_variables(m); std::set unused_internal_variables; { // Z3str2 free variables check - std::map::iterator itor = varAppearInAssign.begin(); - for (; itor != varAppearInAssign.end(); ++itor) { - /* - std::string vName = std::string(Z3_ast_to_string(ctx, itor->first)); - if (vName.length() >= 3 && vName.substr(0, 3) == "$$_") - continue; - */ - if (internal_variable_set.find(itor->first) != internal_variable_set.end()) { + for (auto const &itor : varAppearInAssign) { + if (internal_variable_set.find(itor.first) != internal_variable_set.end()) { // this can be ignored, I think - TRACE("str", tout << "free internal variable " << mk_pp(itor->first, m) << " ignored" << std::endl;); + TRACE("str", tout << "free internal variable " << mk_pp(itor.first, m) << " ignored" << std::endl;); continue; } bool hasEqcValue = false; - get_eqc_value(itor->first, hasEqcValue); + get_eqc_value(itor.first, hasEqcValue); if (!hasEqcValue) { - TRACE("str", tout << "found free variable " << mk_pp(itor->first, m) << std::endl;); + TRACE("str", tout << "found free variable " << mk_pp(itor.first, m) << std::endl;); needToAssignFreeVars = true; - free_variables.push_back(itor->first); + free_variables.push_back(itor.first); // break; } else { // debug @@ -8771,8 +8462,7 @@ namespace smt { return FC_DONE; } else { TRACE("str", tout << "Assigning decoy values to free internal variables." << std::endl;); - for (std::set::iterator it = unused_internal_variables.begin(); it != unused_internal_variables.end(); ++it) { - expr * var = *it; + for (auto const &var : unused_internal_variables) { expr_ref assignment(m.mk_eq(var, mk_string("**unused**")), m); assert_axiom(assignment); } @@ -8793,96 +8483,15 @@ namespace smt { } ); - // ----------------------------------------------------------- - // variables in freeVar are those not bounded by Concats - // classify variables in freeVarMap: - // (1) freeVar = unroll(r1, t1) - // (2) vars are not bounded by either concat or unroll - // ----------------------------------------------------------- - std::map > fv_unrolls_map; - - // erase var bounded by an unroll function from freeVar_map - for (std::map >::iterator fvIt3 = fv_unrolls_map.begin(); - fvIt3 != fv_unrolls_map.end(); fvIt3++) { - expr * var = fvIt3->first; - TRACE("str", tout << "erase free variable " << mk_pp(var, m) << " from freeVar_map, it is bounded by an Unroll" << std::endl;); - freeVar_map.erase(var); - } - - // collect the case: - // * Concat(X, Y) = unroll(r1, t1) /\ Concat(X, Y) = unroll(r2, t2) - // concatEqUnrollsMap[Concat(X, Y)] = {unroll(r1, t1), unroll(r2, t2)} - - std::map > concatEqUnrollsMap; - for (std::map >::iterator urItor = unrollGroup_map.begin(); - urItor != unrollGroup_map.end(); urItor++) { - expr * unroll = urItor->first; - expr * curr = unroll; - do { - if (u.str.is_concat(to_app(curr))) { - concatEqUnrollsMap[curr].insert(unroll); - concatEqUnrollsMap[curr].insert(unrollGroup_map[unroll].begin(), unrollGroup_map[unroll].end()); - } - enode * e_curr = ctx.get_enode(curr); - curr = e_curr->get_next()->get_expr(); - // curr = get_eqc_next(curr); - } while (curr != unroll); - } - - std::map > concatFreeArgsEqUnrollsMap; - std::set fvUnrollSet; - for (std::map >::iterator concatItor = concatEqUnrollsMap.begin(); - concatItor != concatEqUnrollsMap.end(); concatItor++) { - expr * concat = concatItor->first; - expr * concatArg1 = to_app(concat)->get_arg(0); - expr * concatArg2 = to_app(concat)->get_arg(1); - bool arg1Bounded = false; - bool arg2Bounded = false; - // arg1 - if (variable_set.find(concatArg1) != variable_set.end()) { - if (freeVar_map.find(concatArg1) == freeVar_map.end()) { - arg1Bounded = true; - } else { - fvUnrollSet.insert(concatArg1); - } - } else if (u.str.is_concat(to_app(concatArg1))) { - if (concatEqUnrollsMap.find(concatArg1) == concatEqUnrollsMap.end()) { - arg1Bounded = true; - } - } - // arg2 - if (variable_set.find(concatArg2) != variable_set.end()) { - if (freeVar_map.find(concatArg2) == freeVar_map.end()) { - arg2Bounded = true; - } else { - fvUnrollSet.insert(concatArg2); - } - } else if (u.str.is_concat(to_app(concatArg2))) { - if (concatEqUnrollsMap.find(concatArg2) == concatEqUnrollsMap.end()) { - arg2Bounded = true; - } - } - if (!arg1Bounded && !arg2Bounded) { - concatFreeArgsEqUnrollsMap[concat].insert( - concatEqUnrollsMap[concat].begin(), - concatEqUnrollsMap[concat].end()); - } - } - for (std::set::iterator vItor = fvUnrollSet.begin(); vItor != fvUnrollSet.end(); vItor++) { - TRACE("str", tout << "remove " << mk_pp(*vItor, m) << " from freeVar_map" << std::endl;); - freeVar_map.erase(*vItor); - } - // Assign free variables - std::set fSimpUnroll; { TRACE("str", tout << "free var map (#" << freeVar_map.size() << "):" << std::endl; - for (std::map::iterator freeVarItor1 = freeVar_map.begin(); freeVarItor1 != freeVar_map.end(); freeVarItor1++) { - expr * freeVar = freeVarItor1->first; + for (auto const &freeVarItor1 : freeVar_map) { + expr * freeVar = freeVarItor1.first; rational lenValue; bool lenValue_exists = get_len_value(freeVar, lenValue); - tout << mk_pp(freeVar, m) << " [depCnt = " << freeVarItor1->second << ", length = " + tout << mk_pp(freeVar, m) << " [depCnt = " << freeVarItor1.second << ", length = " << (lenValue_exists ? lenValue.to_string() : "?") << "]" << std::endl; } diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index ccedcfc5c..14356f8a1 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -107,54 +107,6 @@ public: } }; -struct c_hash { unsigned operator()(char u) const { return (unsigned)u; } }; -struct c_eq { bool operator()(char u1, char u2) const { return u1 == u2; } }; - -class nfa { -protected: - bool m_valid; - unsigned m_next_id; - - unsigned next_id() { - unsigned retval = m_next_id; - ++m_next_id; - return retval; - } - - unsigned m_start_state; - unsigned m_end_state; - - std::map > transition_map; - std::map > epsilon_map; - - void make_transition(unsigned start, char symbol, unsigned end) { - transition_map[start][symbol] = end; - } - - void make_epsilon_move(unsigned start, unsigned end) { - epsilon_map[start].insert(end); - } - - // Convert a regular expression to an e-NFA using Thompson's construction - void convert_re(expr * e, unsigned & start, unsigned & end, seq_util & u); - -public: - nfa(seq_util & u, expr * e) -: m_valid(true), m_next_id(0), m_start_state(0), m_end_state(0) { - convert_re(e, m_start_state, m_end_state, u); - } - - nfa() : m_valid(false), m_next_id(0), m_start_state(0), m_end_state(0) {} - - bool is_valid() const { - return m_valid; - } - - void epsilon_closure(unsigned start, std::set & closure); - - bool matches(zstring input); -}; - class regex_automaton_under_assumptions { protected: expr * re_term; @@ -489,7 +441,6 @@ protected: obj_hashtable regex_terms; obj_map > regex_terms_by_string; // S --> [ (str.in.re S *) ] obj_map > regex_automaton_assumptions; // RegEx --> [ aut+assumptions ] - obj_map regex_nfa_cache; // Regex term --> NFA obj_hashtable regex_terms_with_path_constraints; // set of string terms which have had path constraints asserted in the current scope obj_hashtable regex_terms_with_length_constraints; // set of regex terms which had had length constraints asserted in the current scope obj_map regex_term_to_length_constraint; // (str.in.re S R) -> (length constraint over S wrt. R) @@ -718,15 +669,14 @@ protected: void check_consistency_contains(expr * e, bool is_true); int ctx_dep_analysis(std::map & strVarMap, std::map & freeVarMap, - std::map > & unrollGroupMap, std::map > & var_eq_concat_map); + std::map > & var_eq_concat_map); void trace_ctx_dep(std::ofstream & tout, std::map & aliasIndexMap, std::map & var_eq_constStr_map, std::map > & var_eq_concat_map, std::map > & var_eq_unroll_map, std::map & concat_eq_constStr_map, - std::map > & concat_eq_concat_map, - std::map > & unrollGroupMap); + std::map > & concat_eq_concat_map); bool term_appears_as_subterm(expr * needle, expr * haystack); void classify_ast_by_type(expr * node, std::map & varMap, From 179988e161ede103db1ed749eb90b82e880e69db Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 5 May 2021 12:53:20 -0700 Subject: [PATCH 02/40] support recursive terms (#5246) Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.cpp | 24 +++++++++++++++++++++++- src/math/lp/lar_solver.h | 2 ++ src/math/lp/lar_term.h | 14 ++++++++++++-- 3 files changed, 37 insertions(+), 3 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index fc4253e41..0837a7b5d 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -162,7 +162,7 @@ namespace lp { continue; if (!m_terms[k]->contains(basis_j)) continue; - m_terms[k]->subst(basis_j, m_mpq_lar_core_solver.m_r_solver.m_pivot_row); + m_terms[k]->subst_in_row(basis_j, m_mpq_lar_core_solver.m_r_solver.m_pivot_row); } } @@ -1717,6 +1717,27 @@ namespace lp { return true; } + void lar_solver::subst_known_terms(lar_term* t) { + std::set seen_terms; + for (const auto&p : *t) { + auto j = p.column(); + if (this->column_corresponds_to_term(j)) { + seen_terms.insert(j); + } + } + while (!seen_terms.empty()) { + unsigned j = *seen_terms.begin(); + seen_terms.erase(j); + auto tj = this->m_var_register.local_to_external(j); + auto& ot = this->get_term(tj); + for(const auto& p : ot){ + if (this->column_corresponds_to_term(p.column())) { + seen_terms.insert(p.column()); + } + } + t->subst_by_term(ot, j); + } + } // do not register in m_var_register this term if ext_i == UINT_MAX var_index lar_solver::add_term(const vector>& coeffs, unsigned ext_i) { TRACE("lar_solver_terms", print_linear_combination_of_column_indices_only(coeffs, tout) << ", ext_i =" << ext_i << "\n";); @@ -1726,6 +1747,7 @@ namespace lp { if (strategy_is_undecided()) return add_term_undecided(coeffs); lar_term* t = new lar_term(coeffs); + subst_known_terms(t); push_term(t); SASSERT(m_terms.size() == m_term_register.size()); unsigned adjusted_term_index = m_terms.size() - 1; diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 452614caa..6e61354ff 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -584,6 +584,8 @@ public: } return out; } + + void subst_known_terms(lar_term*); inline std::ostream& print_column_bound_info(unsigned j, std::ostream& out) const { return m_mpq_lar_core_solver.m_r_solver.print_column_bound_info(j, out); diff --git a/src/math/lp/lar_term.h b/src/math/lp/lar_term.h index bea2d24d3..a8ab37473 100644 --- a/src/math/lp/lar_term.h +++ b/src/math/lp/lar_term.h @@ -53,10 +53,20 @@ public: unsigned size() const { return static_cast(m_coeffs.size()); } template - const T & coeffs() const { + const T & coeffs() const { return m_coeffs; } + void subst_by_term(const lar_term& t, unsigned term_column) { + auto it = this->m_coeffs.find_core(term_column); + if (it == nullptr) return; + mpq a = it->get_data().m_value; + this->m_coeffs.erase(term_column); + for (const auto & p : t) { + this->add_monomial(a * p.coeff(), p.column()); + } + } + lar_term(const vector>& coeffs) { for (const auto & p : coeffs) { add_monomial(p.first, p.second); @@ -94,7 +104,7 @@ public: } // j is the basic variable to substitute - void subst(unsigned j, indexed_vector & li) { + void subst_in_row(unsigned j, indexed_vector & li) { auto* it = m_coeffs.find_core(j); if (it == nullptr) return; const mpq & b = it->get_data().m_value; From 85bd4b5242d4466a6f89645c0c4619b70ee37517 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 May 2021 13:10:48 -0700 Subject: [PATCH 03/40] #5223 Signed-off-by: Nikolaj Bjorner --- src/sat/smt/bv_internalize.cpp | 20 ++++++-------------- src/sat/smt/bv_solver.h | 1 - src/sat/smt/dt_solver.cpp | 15 ++++++++++++++- src/sat/smt/dt_solver.h | 3 ++- src/sat/smt/euf_model.cpp | 5 ++++- 5 files changed, 26 insertions(+), 18 deletions(-) diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index 88f0f79c1..d6c3d4e64 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -162,7 +162,7 @@ namespace bv { #define internalize_bin(F) bin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits) { m_bb.F(sz, xs, ys, bits); }; internalize_binary(a, bin); #define internalize_un(F) un = [&](unsigned sz, expr* const* xs, expr_ref_vector& bits) { m_bb.F(sz, xs, bits);}; internalize_unary(a, un); -#define internalize_ac(F) bin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits) { m_bb.F(sz, xs, ys, bits); }; internalize_ac_binary(a, bin); +#define internalize_ac(F) bin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits) { m_bb.F(sz, xs, ys, bits); }; internalize_binary(a, bin); #define internalize_pun(F) pun = [&](unsigned sz, expr* const* xs, unsigned p, expr_ref_vector& bits) { m_bb.F(sz, xs, p, bits);}; internalize_par_unary(a, pun); #define internalize_nfl(F) ebin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref& out) { m_bb.F(sz, xs, ys, out);}; internalize_novfl(a, ebin); #define internalize_int(B, U) ibin = [&](expr* x, expr* y) { return B(x, y); }; iun = [&](expr* x) { return U(x); }; internalize_interp(a, ibin, iun); @@ -559,27 +559,19 @@ namespace bv { init_bits(n, bits); } - void solver::internalize_binary(app* e, std::function& fn) { - SASSERT(e->get_num_args() == 2); - expr_ref_vector arg1_bits(m), arg2_bits(m), bits(m); - get_arg_bits(e, 0, arg1_bits); - get_arg_bits(e, 1, arg2_bits); - SASSERT(arg1_bits.size() == arg2_bits.size()); - fn(arg1_bits.size(), arg1_bits.data(), arg2_bits.data(), bits); - init_bits(e, bits); - } - void solver::internalize_ac_binary(app* e, std::function& fn) { + void solver::internalize_binary(app* e, std::function& fn) { SASSERT(e->get_num_args() >= 1); expr_ref_vector bits(m), new_bits(m), arg_bits(m); + unsigned i = e->get_num_args() - 1; - get_arg_bits(e, i, bits); - for (; i-- > 0; ) { + get_arg_bits(e, 0, bits); + for (unsigned i = 1; i < e->get_num_args(); ++i) { arg_bits.reset(); get_arg_bits(e, i, arg_bits); SASSERT(arg_bits.size() == bits.size()); new_bits.reset(); - fn(arg_bits.size(), arg_bits.data(), bits.data(), new_bits); + fn(bits.size(), bits.data(), arg_bits.data(), new_bits); bits.swap(new_bits); } init_bits(e, bits); diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index 4bb65c995..daf21a132 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -239,7 +239,6 @@ namespace bv { bool internalize_circuit(app* a); void internalize_unary(app* n, std::function& fn); void internalize_binary(app* n, std::function& fn); - void internalize_ac_binary(app* n, std::function& fn); void internalize_par_unary(app* n, std::function& fn); void internalize_novfl(app* n, std::function& fn); void internalize_interp(app* n, std::function& ibin, std::function& un); diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp index adc99ce9e..133510a84 100644 --- a/src/sat/smt/dt_solver.cpp +++ b/src/sat/smt/dt_solver.cpp @@ -469,12 +469,12 @@ namespace dt { void solver::merge_eh(theory_var v1, theory_var v2, theory_var, theory_var) { // v1 is the new root - TRACE("dt", tout << "merging v" << v1 << " v" << v2 << "\n";); SASSERT(v1 == static_cast(m_find.find(v1))); var_data* d1 = m_var_data[v1]; var_data* d2 = m_var_data[v2]; auto* con1 = d1->m_constructor; auto* con2 = d2->m_constructor; + TRACE("dt", tout << "merging v" << v1 << " v" << v2 << "\n" << ctx.bpp(con1) << " " << ctx.bpp(con2) << "\n";); if (con1 && con2 && con1->get_decl() != con2->get_decl()) ctx.set_conflict(euf::th_explain::conflict(*this, con1, con2)); else if (con2 && !con1) { @@ -721,6 +721,19 @@ namespace dt { return true; } + bool solver::include_func_interp(func_decl* f) const { + if (!dt.is_accessor(f)) + return false; + func_decl* con = dt.get_accessor_constructor(f); + for (enode* app : ctx.get_egraph().enodes_of(f)) { + enode* arg = app->get_arg(0)->get_root(); + if (is_constructor(arg) && arg->get_decl() != con) + return true; + } + return false; + } + + sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) { if (!visit_rec(m, e, sign, root, redundant)) return sat::null_literal; diff --git a/src/sat/smt/dt_solver.h b/src/sat/smt/dt_solver.h index 7e78acb27..cd5529075 100644 --- a/src/sat/smt/dt_solver.h +++ b/src/sat/smt/dt_solver.h @@ -60,7 +60,7 @@ namespace dt { stats() { reset(); } }; - datatype_util dt; + mutable datatype_util dt; array_util m_autil; stats m_stats; ptr_vector m_var_data; @@ -150,6 +150,7 @@ namespace dt { bool unit_propagate() override { return false; } void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override; bool add_dep(euf::enode* n, top_sort& dep) override; + bool include_func_interp(func_decl* f) const override; sat::literal internalize(expr* e, bool sign, bool root, bool redundant) override; void internalize(expr* e, bool redundant) override; euf::theory_var mk_var(euf::enode* n) override; diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index c8780252a..7020ed08c 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -208,7 +208,6 @@ namespace euf { fi = alloc(func_interp, m, arity); mdl->register_decl(f, fi); } - TRACE("euf", tout << f->get_name() << "\n";); args.reset(); for (enode* arg : enode_args(n)) args.push_back(m_values.get(arg->get_root_id())); @@ -216,6 +215,10 @@ namespace euf { SASSERT(args.size() == arity); if (!fi->get_entry(args.data())) fi->insert_new_entry(args.data(), v); + TRACE("euf", tout << f->get_name() << "\n"; + for (expr* arg : args) tout << mk_pp(arg, m) << " "; + tout << "\n -> " << mk_pp(v, m) << "\n";); + } } } From 2b1b10be69817c85a5e378eae13bd38832b897c3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 May 2021 13:50:53 -0700 Subject: [PATCH 04/40] fix #5236 --- src/smt/mam.cpp | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 387afa386..0e5764539 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -1843,7 +1843,7 @@ namespace { enode_vector m_bindings; enode_vector m_args; backtrack_stack m_backtrack_stack; - unsigned m_top; + unsigned m_top { 0 }; const instruction * m_pc; // auxiliary temporary variables @@ -2210,8 +2210,13 @@ namespace { if (curr->get_num_args() == expected_num_args && m_context.is_relevant(curr)) break; } - if (bp.m_it == bp.m_end) + if (bp.m_it == bp.m_end) { + if (best_v) { + bp.m_to_recycle = nullptr; + recycle_enode_vector(best_v); + } return nullptr; + } m_top++; update_max_generation(*(bp.m_it), nullptr); return *(bp.m_it); From 87c0a8136f501daaefb76f5276c2e792fb66706f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 May 2021 16:11:21 -0700 Subject: [PATCH 05/40] #5223 --- src/sat/smt/dt_solver.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp index 133510a84..07c269d48 100644 --- a/src/sat/smt/dt_solver.cpp +++ b/src/sat/smt/dt_solver.cpp @@ -249,7 +249,7 @@ namespace dt { SASSERT(!d->m_constructor); SASSERT(!recognizer || ctx.value(recognizer) == l_false || !is_final); - TRACE("dt", tout << "non_rec_c: " << non_rec_c->get_name() << " #rec: " << d->m_recognizers.size() << "\n";); + TRACE("dt", tout << ctx.bpp(n) << " non_rec_c: " << non_rec_c->get_name() << " #rec: " << d->m_recognizers.size() << "\n";); if (!recognizer && non_rec_c->get_arity() == 0) { sat::literal eq = eq_internalize(n->get_expr(), m.mk_const(non_rec_c)); @@ -474,7 +474,7 @@ namespace dt { var_data* d2 = m_var_data[v2]; auto* con1 = d1->m_constructor; auto* con2 = d2->m_constructor; - TRACE("dt", tout << "merging v" << v1 << " v" << v2 << "\n" << ctx.bpp(con1) << " " << ctx.bpp(con2) << "\n";); + TRACE("dt", tout << "merging v" << v1 << " v" << v2 << "\n" << ctx.bpp(var2enode(v1)) << " == " << ctx.bpp(var2enode(v2)) << " " << ctx.bpp(con1) << " " << ctx.bpp(con2) << "\n";); if (con1 && con2 && con1->get_decl() != con2->get_decl()) ctx.set_conflict(euf::th_explain::conflict(*this, con1, con2)); else if (con2 && !con1) { @@ -782,7 +782,6 @@ namespace dt { } } mk_var(n); - } else if (is_recognizer(term)) { mk_var(n); @@ -794,6 +793,8 @@ namespace dt { SASSERT(is_accessor(term)); SASSERT(n->num_args() == 1); mk_var(n->get_arg(0)); + if (is_datatype(n)) + mk_var(n); } return true; From 7e330c15e763ce1eb956f3cba9d6a1972adf4232 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 May 2021 16:57:06 -0700 Subject: [PATCH 06/40] #5223 --- src/sat/smt/arith_solver.cpp | 9 +++++++++ src/sat/smt/arith_solver.h | 1 + 2 files changed, 10 insertions(+) diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index bb8e1d054..a005b10c7 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -580,6 +580,7 @@ namespace arith { verbose_stream() << n->bool_var() << " " << n->value() << " " << get_phase(n->bool_var()) << " " << ctx.bpp(n) << "\n"; verbose_stream() << *b << "\n";); IF_VERBOSE(0, ctx.display(verbose_stream())); + IF_VERBOSE(0, verbose_stream() << mdl << "\n"); UNREACHABLE(); } } @@ -1438,4 +1439,12 @@ namespace arith { ctx.get_antecedents(l, jst, r, probing); } + bool solver::include_func_interp(func_decl* f) const { + return + a.is_div0(f) || + a.is_idiv0(f) || + a.is_power0(f) || + a.is_rem0(f) || + a.is_mod0(f); + } } diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h index 91955c716..17887535d 100644 --- a/src/sat/smt/arith_solver.h +++ b/src/sat/smt/arith_solver.h @@ -444,6 +444,7 @@ namespace arith { void apply_sort_cnstr(euf::enode* n, sort* s) override {} bool is_shared(theory_var v) const override; lbool get_phase(bool_var v) override; + bool include_func_interp(func_decl* f) const override; // bounds and equality propagation callbacks lp::lar_solver& lp() { return *m_solver; } From 7e7360dd0c04cdee95c3f74a59908209742c5212 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 May 2021 17:40:42 -0700 Subject: [PATCH 07/40] #5223 --- src/ast/macros/quantifier_macro_info.cpp | 6 ++++-- src/sat/smt/q_solver.cpp | 4 +++- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/ast/macros/quantifier_macro_info.cpp b/src/ast/macros/quantifier_macro_info.cpp index 24e5a32e4..2647baf2f 100644 --- a/src/ast/macros/quantifier_macro_info.cpp +++ b/src/ast/macros/quantifier_macro_info.cpp @@ -25,14 +25,16 @@ quantifier_macro_info::quantifier_macro_info(ast_manager& m, quantifier* q) : m_is_auf(true), m_has_x_eq_y(false), m_the_one(m) { - SASSERT(is_forall(q)); collect_macro_candidates(q); } void quantifier_macro_info::collect_macro_candidates(quantifier* q) { macro_util mutil(m); macro_util::macro_candidates candidates(m); - mutil.collect_macro_candidates(q, candidates); + quantifier_ref qa(q, m); + if (is_exists(q)) + qa = m.update_quantifier(q, quantifier_kind::forall_k, m.mk_not(q->get_expr())); + mutil.collect_macro_candidates(qa, candidates); unsigned num_candidates = candidates.size(); for (unsigned i = 0; i < num_candidates; i++) { cond_macro* mc = alloc(cond_macro, m, candidates.get_f(i), candidates.get_def(i), candidates.get_cond(i), diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index ebb553365..26d170fb8 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -148,8 +148,10 @@ namespace q { sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) { SASSERT(is_forall(e) || is_exists(e)); sat::bool_var v = ctx.get_si().add_bool_var(e); - sat::literal lit = ctx.attach_lit(sat::literal(v, sign), e); + sat::literal lit = ctx.attach_lit(sat::literal(v, false), e); mk_var(ctx.get_egraph().find(e)); + if (sign) + lit.neg(); return lit; } From 7373946d6739ce58b761edd6f90ba28d5ee76a72 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Philipp=20Schr=C3=B6er?= Date: Fri, 7 May 2021 23:00:33 +0200 Subject: [PATCH 08/40] julia: fix duplicate method (#5251) Resulted in "Double registration for method" errors when loading Z3.jl with a current build of Z3. --- src/api/julia/z3jl.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/julia/z3jl.cpp b/src/api/julia/z3jl.cpp index 5b04d4a17..dc18e37b6 100644 --- a/src/api/julia/z3jl.cpp +++ b/src/api/julia/z3jl.cpp @@ -451,7 +451,7 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) .method("add", static_cast(&optimize::add)) .method("add", static_cast(&optimize::add)) .method("add", static_cast(&optimize::add)) - .method("add", static_cast(&optimize::add_soft)) + .method("add", static_cast(&optimize::add)) .method("add_soft", static_cast(&optimize::add_soft)) .method("add_soft", static_cast(&optimize::add_soft)) .MM(optimize, maximize) From 31a5bd7fd7dc401f0af99261900f0b706c18aba4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 9 May 2021 20:33:39 -0700 Subject: [PATCH 09/40] regression from July 4 2020 tweeted by Dr. RJ and crowd profiled - let's submit this somwhere? Signed-off-by: Nikolaj Bjorner --- src/ast/expr_substitution.h | 2 +- src/sat/smt/sat_dual_solver.cpp | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ast/expr_substitution.h b/src/ast/expr_substitution.h index ae02e371e..bbd1c0e8e 100644 --- a/src/ast/expr_substitution.h +++ b/src/ast/expr_substitution.h @@ -51,7 +51,7 @@ public: void reset(); void cleanup(); - obj_map const sub() const { return m_subst; } + obj_map const & sub() const { return m_subst; } std::ostream& display(std::ostream& out); }; diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp index 22af58d59..7a48f8809 100644 --- a/src/sat/smt/sat_dual_solver.cpp +++ b/src/sat/smt/sat_dual_solver.cpp @@ -147,6 +147,7 @@ namespace sat { if (m_solver.value(r) == l_true) lits.push_back(r); out << "roots: " << lits << "\n"; + m_solver.display(out); return out; } From 28328e63fd4d3bc733809a9f386ecccb78fa0163 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 9 May 2021 20:48:11 -0700 Subject: [PATCH 10/40] fix #5255 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/pb2bv_tactic.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index aeda016c7..98724923b 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -657,13 +657,14 @@ private: SASSERT(pos); r = m.mk_true(); } - else { - SASSERT((c.is_zero() && k == GE) || - (c.is_one() && k == LE)); + else if ((c.is_zero() && k == GE) || + (c.is_one() && k == LE)) { // unit 0 >= x, 1 <= x SASSERT(pos); r = mk_unit(rhs, k == GE); } + else + throw_non_pb(t); return; } throw_non_pb(t); @@ -985,7 +986,7 @@ private: void throw_tactic(expr* e) { std::stringstream strm; - strm << "goal is in a fragment unsupported by pb2bv. Offending expression: " << mk_pp(e, m); + strm << "goal is in a fragment not supported by pb2bv. Offending expression: " << mk_pp(e, m); throw tactic_exception(strm.str()); } }; From a61e9d6b49c405d94a184fc073858aab3da63f99 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 May 2021 10:33:43 -0700 Subject: [PATCH 11/40] #5260 --- src/ast/rewriter/bool_rewriter.cpp | 2 +- src/sat/tactic/goal2sat.cpp | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index b60310476..f21b2c554 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -62,7 +62,7 @@ br_status bool_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * co return BR_DONE; case OP_XOR: switch (num_args) { - case 0: return BR_FAILED; + case 0: result = m().mk_false(); return BR_DONE; case 1: result = args[0]; return BR_DONE; case 2: mk_xor(args[0], args[1], result); return BR_DONE; default: UNREACHABLE(); return BR_FAILED; diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index d11ff60a9..9cb21c769 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -577,6 +577,8 @@ struct goal2sat::imp : public sat::sat_internalizer { } void convert_iff2(app * t, bool root, bool sign) { + if (t->get_num_args() != 2) + throw default_exception("unexpected number of arguments to xor"); SASSERT(t->get_num_args() == 2); unsigned sz = m_result_stack.size(); SASSERT(sz >= 2); From 987099c765d76c48ca5168b7d0cdde7aed47b7a8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 May 2021 10:54:21 -0700 Subject: [PATCH 12/40] Hoist creation of m_rep for #5259 --- src/ast/rewriter/th_rewriter.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 99f26234a..8e00bf657 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -51,6 +51,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { recfun_rewriter m_rec_rw; arith_util m_a_util; bv_util m_bv_util; + expr_safe_replace m_rep; expr_ref_vector m_pinned; unsigned long long m_max_memory; // in bytes unsigned m_max_steps; @@ -685,12 +686,11 @@ struct th_rewriter_cfg : public default_rewriter_cfg { void apply_subst(ptr_buffer& patterns) { if (!m_subst) return; + if (patterns.empty()) + return; expr_ref tmp(m()); - expr_safe_replace rep(m()); - for (auto kv : m_subst->sub()) - rep.insert(kv.m_key, kv.m_value); for (unsigned i = 0; i < patterns.size(); ++i) { - rep(patterns[i], tmp); + m_rep(patterns[i], tmp); m_pinned.push_back(tmp); patterns[i] = tmp; } @@ -796,6 +796,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { m_rec_rw(m), m_a_util(m), m_bv_util(m), + m_rep(m), m_pinned(m), m_used_dependencies(m), m_subst(nullptr) { @@ -805,6 +806,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg { void set_substitution(expr_substitution * s) { reset(); m_subst = s; + m_rep.reset(); + for (auto kv : m_subst->sub()) + m_rep.insert(kv.m_key, kv.m_value); } void reset() { From e2a52ed6eeccbdf5ce01d9b04b7acac347fd20e7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 May 2021 11:15:19 -0700 Subject: [PATCH 13/40] #5259 again --- src/ast/rewriter/th_rewriter.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 8e00bf657..1f80d57a6 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -52,9 +52,10 @@ struct th_rewriter_cfg : public default_rewriter_cfg { arith_util m_a_util; bv_util m_bv_util; expr_safe_replace m_rep; + bool m_new_subst { false }; expr_ref_vector m_pinned; unsigned long long m_max_memory; // in bytes - unsigned m_max_steps; + unsigned m_max_steps; bool m_pull_cheap_ite; bool m_flat; bool m_cache_all; @@ -688,6 +689,12 @@ struct th_rewriter_cfg : public default_rewriter_cfg { return; if (patterns.empty()) return; + if (m_new_subst) { + m_rep.reset(); + for (auto kv : m_subst->sub()) + m_rep.insert(kv.m_key, kv.m_value); + m_new_subst = false; + } expr_ref tmp(m()); for (unsigned i = 0; i < patterns.size(); ++i) { m_rep(patterns[i], tmp); @@ -806,9 +813,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { void set_substitution(expr_substitution * s) { reset(); m_subst = s; - m_rep.reset(); - for (auto kv : m_subst->sub()) - m_rep.insert(kv.m_key, kv.m_value); + m_new_subst = true; } void reset() { From 2ea4b0f4e0371747309ee890e7df95f3d2f31b29 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 May 2021 11:42:11 -0700 Subject: [PATCH 14/40] #5260 --- src/model/model_evaluator.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 2fa79b2ce..b1dc9c1ab 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -266,6 +266,7 @@ struct evaluator_cfg : public default_rewriter_cfg { func_interp * fi = m_model.get_func_interp(g); if (fi && (result = fi->get_array_interp(g))) { model_evaluator ev(m_model, m_params); + ev.set_model_completion(false); result = ev(result); m_pinned.push_back(result); m_def_cache.insert(g, result); From f02fbb49bb7ecb34a561fcab51e11f7cd46067d0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 May 2021 13:00:52 -0700 Subject: [PATCH 15/40] fix #5253 --- src/sat/smt/q_mam.cpp | 14 ++++---------- src/smt/mam.cpp | 14 +++++--------- 2 files changed, 9 insertions(+), 19 deletions(-) diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp index a73df33ae..6a7b8e1e4 100644 --- a/src/sat/smt/q_mam.cpp +++ b/src/sat/smt/q_mam.cpp @@ -1224,16 +1224,10 @@ namespace q { m_mp_already_processed[first_idx] = true; linearise_multi_pattern(first_idx); } - -#ifdef Z3DEBUG - for (unsigned i = 0; i < m_qa->get_num_decls(); i++) { - CTRACE("mam_new_bug", m_vars[i] < 0, tout << mk_ismt2_pp(m_qa, m) << "\ni: " << i << " m_vars[i]: " << m_vars[i] << "\n"; - tout << "m_mp:\n" << mk_ismt2_pp(m_mp, m) << "\n"; - tout << "tree:\n" << *m_tree << "\n"; - ); - SASSERT(m_vars[i] >= 0); - } -#endif + for (unsigned i = 0; i < m_qa->get_num_decls(); i++) + if (m_vars[i] == -1) + return; + SASSERT(head->m_next == 0); m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, m_qa->get_num_decls(), reinterpret_cast(m_vars.begin()))); diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 0e5764539..25fe5c43d 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -1218,15 +1218,11 @@ namespace { linearise_multi_pattern(first_idx); } -#ifdef Z3DEBUG - for (unsigned i = 0; i < m_qa->get_num_decls(); i++) { - CTRACE("mam_new_bug", m_vars[i] < 0, tout << mk_ismt2_pp(m_qa, m) << "\ni: " << i << " m_vars[i]: " << m_vars[i] << "\n"; - tout << "m_mp:\n" << mk_ismt2_pp(m_mp, m) << "\n"; - tout << "tree:\n" << *m_tree << "\n"; - ); - SASSERT(m_vars[i] >= 0); - } -#endif + // check that all variables are captured by pattern. + for (unsigned i = 0; i < m_qa->get_num_decls(); i++) + if (m_vars[i] == -1) + return; + SASSERT(head->m_next == 0); m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, m_qa->get_num_decls(), reinterpret_cast(m_vars.begin()))); From 897a2d647044212c6abdf8f92a100f3a52877277 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 May 2021 13:33:37 -0700 Subject: [PATCH 16/40] #5261 --- src/shell/dimacs_frontend.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp index 8dc3104fc..7350745f2 100644 --- a/src/shell/dimacs_frontend.cpp +++ b/src/shell/dimacs_frontend.cpp @@ -264,15 +264,15 @@ unsigned read_dimacs(char const * file_name) { } switch (r) { case l_true: - std::cout << "sat\n"; + std::cout << "s SATISFIABLE\n"; if (file_name && gparams::get_ref().get_bool("model_validate", false)) verify_solution(file_name); display_model(*g_solver); break; case l_undef: - std::cout << "unknown\n"; + std::cout << "s UNKNOWN\n"; break; case l_false: - std::cout << "unsat\n"; + std::cout << "s UNSATISFIABLE\n"; if (p.get_bool("dimacs.core", false)) { display_core(*g_solver, tracking_clauses); } From d27d09f87ac6270c371b2f850d0491570bbe770f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 May 2021 13:35:25 -0700 Subject: [PATCH 17/40] #5261 --- src/shell/dimacs_frontend.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp index 7350745f2..ec157a291 100644 --- a/src/shell/dimacs_frontend.cpp +++ b/src/shell/dimacs_frontend.cpp @@ -66,6 +66,7 @@ static void STD_CALL on_ctrl_c(int) { static void display_model(sat::solver const & s) { sat::model const & m = s.get_model(); + std::cout << "v "; for (unsigned i = 1; i < m.size(); i++) { switch (m[i]) { case l_false: std::cout << "-" << i << " "; break; @@ -77,7 +78,7 @@ static void display_model(sat::solver const & s) { } static void display_core(sat::solver const& s, vector const& tracking_clauses) { - std::cout << "core\n"; + std::cout << "v core\n"; sat::literal_vector const& c = s.get_core(); for (unsigned i = 0; i < c.size(); ++i) { sat::literal_vector const& cls = tracking_clauses[c[i].var()]; From cd82205b061b221808875198944e5bbb82ea2781 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 May 2021 19:14:18 -0700 Subject: [PATCH 18/40] nit --- src/qe/qe_lite.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index da9367362..58fe3b293 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -2316,7 +2316,7 @@ public: if (is_exists(tmp) && to_quantifier(tmp)->get_qid() == qe_lite) { used_vars used; tmp = to_quantifier(tmp)->get_expr(); - used.process(tmp); + used(tmp); var_subst vs(m, true); fml = vs(tmp, vars.size(), (expr*const*)vars.data()); // collect set of variables that were used. From 7869cdbbc88a70d7915f26c39259066985ea0d70 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 12 May 2021 10:43:16 -0700 Subject: [PATCH 19/40] #5259 - the Ranjit 2s shave shave a couple of seconds from the Ranjit regression --- src/ast/normal_forms/nnf.cpp | 11 ++++++----- src/ast/rewriter/var_subst.cpp | 4 +++- src/ast/used_vars.cpp | 15 +++++++++++++-- src/ast/used_vars.h | 10 +++++++++- 4 files changed, 31 insertions(+), 9 deletions(-) diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index 19b776aba..d0398543b 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -72,6 +72,7 @@ class skolemizer { cache m_cache; cache m_cache_pr; bool m_proofs_enabled; + used_vars m_uv; void process(quantifier * q, expr_ref & r, proof_ref & p) { @@ -81,14 +82,14 @@ class skolemizer { p = nullptr; return; } - used_vars uv; - uv(q); + m_uv.reset(); + m_uv(q); SASSERT(is_well_sorted(m, q)); - unsigned sz = uv.get_max_found_var_idx_plus_1(); + unsigned sz = m_uv.get_max_found_var_idx_plus_1(); ptr_buffer sorts; expr_ref_vector args(m); for (unsigned i = 0; i < sz; i++) { - sort * s = uv.get(i); + sort * s = m_uv.get(i); if (s != nullptr) { sorts.push_back(s); args.push_back(m.mk_var(i, s)); @@ -111,7 +112,7 @@ class skolemizer { // (VAR num_decls-1) is in the last position. // for (unsigned i = 0; i < sz; i++) { - sort * s = uv.get(i); + sort * s = m_uv.get(i); if (s != nullptr) substitution.push_back(m.mk_var(i, s)); else diff --git a/src/ast/rewriter/var_subst.cpp b/src/ast/rewriter/var_subst.cpp index 13dd4f459..a61cfdc4e 100644 --- a/src/ast/rewriter/var_subst.cpp +++ b/src/ast/rewriter/var_subst.cpp @@ -79,7 +79,9 @@ expr_ref unused_vars_eliminator::operator()(quantifier* q) { result = q; return result; } + unsigned num_decls = q->get_num_decls(); m_used.reset(); + m_used.set_num_decls(num_decls); m_used.process(q->get_expr()); unsigned num_patterns = q->get_num_patterns(); for (unsigned i = 0; i < num_patterns; i++) @@ -88,7 +90,7 @@ expr_ref unused_vars_eliminator::operator()(quantifier* q) { for (unsigned i = 0; i < num_no_patterns; i++) m_used.process(q->get_no_pattern(i)); - unsigned num_decls = q->get_num_decls(); + if (m_used.uses_all_vars(num_decls)) { q->set_no_unused_vars(); result = q; diff --git a/src/ast/used_vars.cpp b/src/ast/used_vars.cpp index a3030f087..29321d98a 100644 --- a/src/ast/used_vars.cpp +++ b/src/ast/used_vars.cpp @@ -22,6 +22,9 @@ Revision History: void used_vars::process(expr * n, unsigned delta) { unsigned j, idx; + if (m_num_found_vars == m_num_decls) + return; + m_cache.reset(); m_todo.reset(); m_todo.push_back(expr_delta_pair(n, delta)); @@ -58,8 +61,16 @@ void used_vars::process(expr * n, unsigned delta) { if (idx >= delta) { idx = idx - delta; if (idx >= m_found_vars.size()) - m_found_vars.resize(idx + 1); - m_found_vars[idx] = to_var(n)->get_sort(); + m_found_vars.resize(idx + 1, nullptr); + if (!m_found_vars[idx]) { + m_found_vars[idx] = to_var(n)->get_sort(); + if (idx < m_num_decls) + m_num_found_vars++; + if (m_num_found_vars == m_num_decls) { + m_todo.reset(); + return; + } + } } break; case AST_QUANTIFIER: diff --git a/src/ast/used_vars.h b/src/ast/used_vars.h index dbd7ae854..c9ecdcfea 100644 --- a/src/ast/used_vars.h +++ b/src/ast/used_vars.h @@ -26,18 +26,26 @@ class used_vars { typedef hashtable, default_eq > cache; cache m_cache; svector m_todo; + unsigned m_num_decls{ UINT_MAX }; + unsigned m_num_found_vars{ 0 }; void process(expr * n, unsigned delta); public: void operator()(expr * n) { - m_found_vars.reset(); + reset(); process(n, 0); } void reset() { m_found_vars.reset(); + m_num_decls = UINT_MAX; + m_num_found_vars = 0; + } + + void set_num_decls(unsigned n) { + m_num_decls = n; } void process(expr * n) { From f942c3df91caf1ad86a17234c9630247f2fdacd6 Mon Sep 17 00:00:00 2001 From: Zachary Wimer Date: Wed, 12 May 2021 13:10:14 -0700 Subject: [PATCH 20/40] operator= checks this equality before moving (#5265) --- src/api/c++/z3++.h | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 5e66c4d3e..4072c0744 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -511,9 +511,11 @@ namespace z3 { return *this; } ast & operator=(ast && s) noexcept { - object::operator=(std::forward(s)); - m_ast = s.m_ast; - s.m_ast = nullptr; + if (this != &s) { + object::operator=(std::forward(s)); + m_ast = s.m_ast; + s.m_ast = nullptr; + } return *this; } Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; } From 8ca6f567d3d38be39d28996cee752814e296701d Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Sun, 16 May 2021 13:53:08 -0700 Subject: [PATCH 21/40] fixing issue #5140 (#5268) --- src/ast/seq_decl_plugin.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 9a7b53946..048e6ffed 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1480,7 +1480,7 @@ seq_util::rex::info seq_util::rex::info::orelse(seq_util::rex::info const& i) co // unsigned ite_min_length = std::min(min_length, i.min_length); // lbool ite_nullable = (nullable == i.nullable ? nullable : l_undef); // TBD: whether ite is interpreted or not depends on whether the condition is interpreted and both branches are interpreted - return info(false, false, false, false, normalized && i.normalized, monadic && i.monadic, singleton && i.singleton, nullable, min_length, std::max(star_height, i.star_height)); + return info(false, false, false, false, normalized && i.normalized, monadic && i.monadic, singleton && i.singleton, nullable, std::min(min_length, i.min_length), std::max(star_height, i.star_height)); } else return i; From 93a9847815feb7bdfd6b324e8192b879c89266f2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 16 May 2021 15:44:44 -0700 Subject: [PATCH 22/40] BUILD_LIBZ3_SHARED Signed-off-by: Nikolaj Bjorner --- contrib/ci/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/contrib/ci/README.md b/contrib/ci/README.md index 61e61e45e..8b48ac32e 100644 --- a/contrib/ci/README.md +++ b/contrib/ci/README.md @@ -42,7 +42,7 @@ the future. * `Z3_BUILD_TYPE` - CMake build type (`RelWithDebInfo`, `Release`, `Debug`, or `MinSizeRel`) * `Z3_CMAKE_GENERATOR` - CMake generator (`Ninja` or `Unix Makefiles`) * `Z3_VERBOSE_BUILD_OUTPUT` - Show compile commands in CMake builds (`0` or `1`) -* `Z3_STATIC_BUILD` - Build Z3 binaries and libraries statically (`0` or `1`) +* `Z3_BUILD_LIBZ3_SHARED` - Build Z3 binaries and libraries dynamically/statically (`0` or `1`) * `Z3_SYSTEM_TEST_GIT_REVISION` - Git revision of [z3test](https://github.com/Z3Prover/z3test). If empty lastest revision will be used. * `Z3_WARNINGS_AS_ERRORS` - Set the `WARNINGS_AS_ERRORS` CMake option passed to Z3 (`OFF`, `ON`, or `SERIOUS_ONLY`) From d2bd92eab97bbc9528349b137d58f991f4805265 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 17 May 2021 10:42:34 -0700 Subject: [PATCH 23/40] fix #5271 --- src/smt/smt_model_checker.cpp | 9 ++++++++- src/smt/smt_parallel.cpp | 23 +++++++++++++++++------ 2 files changed, 25 insertions(+), 7 deletions(-) diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index e0214972b..4598a9a3f 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -319,7 +319,14 @@ namespace smt { struct scoped_ctx_push { context* c; scoped_ctx_push(context* c): c(c) { c->push(); } - ~scoped_ctx_push() { c->pop(1); } + ~scoped_ctx_push() { + try { + c->pop(1); + } + catch (...) { + ; + } + } }; /** diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index e82b3f56e..744d5ce2b 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -193,14 +193,25 @@ namespace smt { } catch (z3_error & err) { - error_code = err.error_code(); - ex_kind = ERROR_EX; - done = true; + if (finished_id == UINT_MAX) { + error_code = err.error_code(); + ex_kind = ERROR_EX; + done = true; + } } catch (z3_exception & ex) { - ex_msg = ex.msg(); - ex_kind = DEFAULT_EX; - done = true; + if (finished_id == UINT_MAX) { + ex_msg = ex.msg(); + ex_kind = DEFAULT_EX; + done = true; + } + } + catch (...) { + if (finished_id == UINT_MAX) { + ex_msg = "unknown exception"; + ex_kind = ERROR_EX; + done = true; + } } }; From 1a432529dd769aa56b624410ffd6a80d34ef3099 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 17 May 2021 11:10:05 -0700 Subject: [PATCH 24/40] fix #5272 --- src/cmd_context/cmd_context.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 6bcca936a..fd8eeb3f1 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -879,8 +879,9 @@ void cmd_context::insert(symbol const & s, func_decl * f) { void cmd_context::insert(symbol const & s, psort_decl * p) { pm().inc_ref(p); if (m_psort_decls.contains(s)) { + symbol _s = s; pm().dec_ref(p); - throw cmd_exception("sort already defined ", s); + throw cmd_exception("sort already defined ", _s); } m_psort_decls.insert(s, p); if (!m_global_decls) { From 8384f38eb5cae5bcef6380d50c65060154b6b5c5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 17 May 2021 15:41:51 -0700 Subject: [PATCH 25/40] fix #5254 --- src/opt/opt_context.cpp | 17 +---------- src/opt/opt_solver.cpp | 67 +++++++++++++++++++++++------------------ src/opt/opt_solver.h | 6 +--- src/opt/optsmt.cpp | 19 ++++++------ src/opt/optsmt.h | 1 - 5 files changed, 49 insertions(+), 61 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index c522dbf60..eab037bd2 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1714,23 +1714,8 @@ namespace opt { objective const& obj = m_objectives[i]; switch(obj.m_type) { case O_MINIMIZE: - case O_MAXIMIZE: { - inf_eps n = m_optsmt.get_lower(obj.m_index); - if (false && // theory_lra doesn't produce infinitesimals - m_optsmt.objective_is_model_valid(obj.m_index) && - n.get_infinity().is_zero() && - n.get_infinitesimal().is_zero() && - is_numeral((*m_model)(obj.m_term), r1)) { - rational r2 = n.get_rational(); - if (obj.m_type == O_MINIMIZE) { - r1.neg(); - } - CTRACE("opt", r1 != r2, tout << obj.m_term << " evaluates to " << r1 << " but has objective " << r2 << "\n";); - CTRACE("opt", r1 != r2, tout << *m_model;); - SASSERT(r1 == r2); - } + case O_MAXIMIZE: break; - } case O_MAXSMT: { rational value(0); for (unsigned i = 0; i < obj.m_terms.size(); ++i) { diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 42a92e128..c1a4c68a9 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -244,23 +244,46 @@ namespace opt { smt::theory_var v = m_objective_vars[i]; bool has_shared = false; m_last_model = nullptr; + // + // compute an optimization hint. + // The hint is valid if there are no shared symbols (a pure LP). + // Generally, the hint is not necessarily valid and has to be checked + // relative to other theories. + // inf_eps val = get_optimizer().maximize(v, blocker, has_shared); m_context.get_model(m_last_model); inf_eps val2; - m_valid_objectives[i] = true; has_shared = true; TRACE("opt", tout << (has_shared?"has shared":"non-shared") << " " << val << " " << blocker << "\n"; if (m_last_model) tout << *m_last_model << "\n";); if (!m_models[i]) m_models.set(i, m_last_model.get()); + + // + // retrieve value of objective from current model and update + // current optimal. + // + auto update_objective = [&]() { + rational r; + expr_ref value = (*m_last_model)(m_objective_terms.get(i)); + if (arith_util(m).is_numeral(value, r) && r > m_objective_values[i]) + m_objective_values[i] = inf_eps(r); + }; + + update_objective(); - auto decrement = [&]() { + + // + // check that "val" obtained from optimization hint is a valid bound. + // + auto check_bound = [&]() { SASSERT(has_shared); - decrement_value(i, val); + bool ok = bound_value(i, val); if (l_true != m_context.check(0, nullptr)) return false; - m_context.get_model(m_last_model); - return true; + m_context.get_model(m_last_model); + update_objective(); + return ok; }; if (!val.is_finite()) { @@ -270,19 +293,16 @@ namespace opt { TRACE("opt", tout << "updated\n";); m_last_model = nullptr; m_context.get_model(m_last_model); - if (has_shared && val != current_objective_value(i)) { - if (!decrement()) - return false; - } - else { + if (!has_shared || val == current_objective_value(i)) m_models.set(i, m_last_model.get()); - } + else if (!check_bound()) + return false; } - else if (!decrement()) + else if (!check_bound()) return false; m_objective_values[i] = val; TRACE("opt", { - tout << "objective: " << mk_pp(m_objective_terms[i].get(), m) << "\n"; + tout << "objective: " << mk_pp(m_objective_terms.get(i), m) << "\n"; tout << "maximal value: " << val << "\n"; tout << "new condition: " << blocker << "\n"; if (m_models[i]) model_smt2_pp(tout << "update model:\n", m, *m_models[i], 0); @@ -291,10 +311,9 @@ namespace opt { return true; } - lbool opt_solver::decrement_value(unsigned i, inf_eps& val) { + bool opt_solver::bound_value(unsigned i, inf_eps& val) { push_core(); expr_ref ge = mk_ge(i, val); - TRACE("opt", tout << ge << "\n";); assert_expr(ge); lbool is_sat = m_context.check(0, nullptr); is_sat = adjust_result(is_sat); @@ -303,19 +322,7 @@ namespace opt { m_models.set(i, m_last_model.get()); } pop_core(1); - TRACE("opt", tout << is_sat << "\n";); - if (is_sat != l_true) { - // cop-out approximation - if (arith_util(m).is_real(m_objective_terms.get(i))) { - val -= inf_eps(inf_rational(rational(0), true)); - } - else { - val -= inf_eps(inf_rational(rational(1))); - } - m_valid_objectives[i] = false; - } - return is_sat; - + return is_sat == l_true; } lbool opt_solver::adjust_result(lbool r) { @@ -338,10 +345,12 @@ namespace opt { for (unsigned i = m_models.size(); i-- > 0; ) { auto* mdl = m_models[i]; if (mdl) { + TRACE("opt", tout << "get " << i << "\n" << *mdl << "\n";); m = mdl; return; } } + TRACE("opt", tout << "get last\n";); m = m_last_model.get(); } @@ -384,7 +393,6 @@ namespace opt { m_objective_vars.push_back(v); m_objective_values.push_back(inf_eps(rational::minus_one(), inf_rational())); m_objective_terms.push_back(term); - m_valid_objectives.push_back(true); m_models.push_back(nullptr); return v; } @@ -486,7 +494,6 @@ namespace opt { m_objective_vars.reset(); m_objective_values.reset(); m_objective_terms.reset(); - m_valid_objectives.reset(); } opt_solver& opt_solver::to_opt(solver& s) { diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 2a84734e4..caac008fd 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -77,7 +77,6 @@ namespace opt { vector m_objective_values; sref_vector m_models; expr_ref_vector m_objective_terms; - bool_vector m_valid_objectives; bool m_dump_benchmarks; static unsigned m_dump_count; statistics m_stats; @@ -124,9 +123,6 @@ namespace opt { inf_eps const & saved_objective_value(unsigned obj_index); inf_eps current_objective_value(unsigned obj_index); model* get_model_idx(unsigned obj_index) { return m_models[obj_index]; } - bool objective_is_model_valid(unsigned obj_index) const { - return m_valid_objectives[obj_index]; - } bool was_unknown() const { return m_was_unknown; } @@ -147,7 +143,7 @@ namespace opt { symbol const& logic = symbol::null, char const * status = "unknown", char const * attributes = ""); private: - lbool decrement_value(unsigned i, inf_eps& val); + bool bound_value(unsigned i, inf_eps& val); void set_model(unsigned i); lbool adjust_result(lbool r); }; diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index f074f5fc1..0aebf522b 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -195,24 +195,25 @@ namespace opt { lbool optsmt::geometric_lex(unsigned obj_index, bool is_maximize) { TRACE("opt", tout << "index: " << obj_index << " is-max: " << is_maximize << "\n";); arith_util arith(m); - bool is_int = arith.is_int(m_objs[obj_index].get()); + bool is_int = arith.is_int(m_objs.get(obj_index)); lbool is_sat = l_true; expr_ref bound(m), last_bound(m); - for (unsigned i = 0; i < obj_index; ++i) { + for (unsigned i = 0; i < obj_index; ++i) commit_assignment(i); - } unsigned steps = 0; unsigned step_incs = 0; rational delta_per_step(1); unsigned num_scopes = 0; + inf_eps last_objective = inf_eps(rational(-1), inf_rational(0)); while (m.inc()) { SASSERT(delta_per_step.is_int()); SASSERT(delta_per_step.is_pos()); is_sat = m_s->check_sat(0, nullptr); TRACE("opt", tout << "check " << is_sat << "\n"; + tout << "last bound: " << last_bound << "\n"; tout << "lower: " << m_lower[obj_index] << "\n"; tout << "upper: " << m_upper[obj_index] << "\n"; ); @@ -221,6 +222,7 @@ namespace opt { m_s->get_model(m_model); SASSERT(m_model); inf_eps obj = m_s->saved_objective_value(obj_index); + TRACE("opt", tout << "saved objective: " << obj << "\n";); update_lower_lex(obj_index, obj, is_maximize); if (!is_int || !m_lower[obj_index].is_finite()) { delta_per_step = rational(1); @@ -233,12 +235,12 @@ namespace opt { else { ++steps; } - if (delta_per_step > rational::one()) { + if (delta_per_step > rational::one() || obj == last_objective) { m_s->push(); ++num_scopes; bound = m_s->mk_ge(obj_index, obj + inf_eps(delta_per_step)); } - TRACE("opt", tout << "delta: " << delta_per_step << " " << bound << "\n";); + last_objective = obj; if (bound == last_bound) { break; } @@ -357,6 +359,7 @@ namespace opt { } void optsmt::update_lower_lex(unsigned idx, inf_eps const& v, bool is_maximize) { + TRACE("opt", tout << v << " lower: " << m_lower[idx] << "\n";); if (v > m_lower[idx]) { m_lower[idx] = v; IF_VERBOSE(1, @@ -368,6 +371,7 @@ namespace opt { for (unsigned i = idx+1; i < m_vars.size(); ++i) { m_lower[i] = m_s->saved_objective_value(i); } + TRACE("opt", tout << "update best model " << *m_model << "\n";); m_best_model = m_model; m_s->get_labels(m_labels); m_context.set_model(m_model); @@ -532,10 +536,6 @@ namespace opt { return m_lower[i]; } - bool optsmt::objective_is_model_valid(unsigned index) const { - return m_s->objective_is_model_valid(index); - } - inf_eps optsmt::get_upper(unsigned i) const { if (i >= m_upper.size()) return inf_eps(); return m_upper[i]; @@ -543,6 +543,7 @@ namespace opt { void optsmt::get_model(model_ref& mdl, svector & labels) { mdl = m_best_model.get(); + TRACE("opt", tout << *mdl << "\n";); labels = m_labels; } diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h index a7555977b..80dd4e5f7 100644 --- a/src/opt/optsmt.h +++ b/src/opt/optsmt.h @@ -61,7 +61,6 @@ namespace opt { void commit_assignment(unsigned index); inf_eps get_lower(unsigned index) const; inf_eps get_upper(unsigned index) const; - bool objective_is_model_valid(unsigned index) const; void get_model(model_ref& mdl, svector& labels); model* get_model(unsigned index) const { return m_models[index]; } From 55f8ad068f7e0922959a8e7856760940d4778b93 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 17 May 2021 15:51:03 -0700 Subject: [PATCH 26/40] fix #5262 --- src/qe/mbp/mbp_arith.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp index b0f8f9eb5..04385b392 100644 --- a/src/qe/mbp/mbp_arith.cpp +++ b/src/qe/mbp/mbp_arith.cpp @@ -194,17 +194,19 @@ namespace mbp { else if (m.is_ite(t, t1, t2, t3)) { val = eval(t1); - SASSERT(m.is_true(val) || m.is_false(val)); TRACE("qe", tout << mk_pp(t1, m) << " := " << val << "\n";); if (m.is_true(val)) { linearize(mbo, eval, mul, t2, c, fmls, ts, tids); fmls.push_back(t1); } - else { + else if (m.is_false(val)) { expr_ref not_t1(mk_not(m, t1), m); fmls.push_back(not_t1); linearize(mbo, eval, mul, t3, c, fmls, ts, tids); } + else { + throw default_exception("mbp evaluation didn't produce a truth value"); + } } else if (a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && !mul1.is_zero()) { rational r; From 4f9ad28a057eb1dfc8deb66881b2b9093fc7ab69 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 17 May 2021 16:16:12 -0700 Subject: [PATCH 27/40] fix #5252 --- src/model/model_evaluator.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index b1dc9c1ab..23bab1761 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include "ast/ast_pp.h" #include "ast/ast_util.h" +#include "ast/recfun_decl_plugin.h" #include "ast/rewriter/rewriter_types.h" #include "ast/rewriter/bool_rewriter.h" #include "ast/rewriter/arith_rewriter.h" @@ -374,6 +375,8 @@ struct evaluator_cfg : public default_rewriter_cfg { var_subst vs(m, false); result = vs(fi->get_interp(), num, args); + if (!is_ground(result.get()) && recfun::util(m).is_defined(f)) + return BR_DONE; return BR_REWRITE_FULL; } From 30974968afbb6aaf74c83d017bce4f989b2b7352 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 17 May 2021 17:41:34 -0700 Subject: [PATCH 28/40] fix #5256 Signed-off-by: Nikolaj Bjorner --- src/smt/tactic/ctx_solver_simplify_tactic.cpp | 52 ++++++++++++------- 1 file changed, 33 insertions(+), 19 deletions(-) diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp index ec867f59d..e7608dd4b 100644 --- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp +++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp @@ -213,37 +213,51 @@ protected: sz = a->get_num_args(); n2 = nullptr; + bool found = false; + + // + // This is a single traversal version of the context + // simplifier. It simplifies only the first occurrence of + // a sub-term with respect to the context. + // + for (unsigned i = 0; i < sz; ++i) { expr* arg = a->get_arg(i); - if (cache.find(arg, path_r)) { - // - // This is a single traversal version of the context - // simplifier. It simplifies only the first occurrence of - // a sub-term with respect to the context. - // - - if (path_r.m_parent == self_pos && path_r.m_idx == i) { - args.push_back(path_r.m_expr); + if (cache.find(arg, path_r) && + path_r.m_parent == self_pos && path_r.m_idx == i) { + args.push_back(path_r.m_expr); + found = true; + continue; + } + args.push_back(arg); + } + + // + // the context is not equivalent to top-level + // if it is already simplified. + // Bug exposes such a scenario #5256 + // + if (!found) { + args.reset(); + for (unsigned i = 0; i < sz; ++i) { + expr* arg = a->get_arg(i); + if (!n2 && !m.is_value(arg)) { + n2 = mk_fresh(id, arg->get_sort()); + trail.push_back(n2); + todo.push_back(expr_pos(self_pos, ++child_id, i, arg)); + names.push_back(n2); + args.push_back(n2); } else { args.push_back(arg); } } - else if (!n2 && !m.is_value(arg)) { - n2 = mk_fresh(id, arg->get_sort()); - trail.push_back(n2); - todo.push_back(expr_pos(self_pos, ++child_id, i, arg)); - names.push_back(n2); - args.push_back(n2); - } - else { - args.push_back(arg); - } } m_mk_app(a->get_decl(), args.size(), args.data(), res); trail.push_back(res); // child needs to be visited. if (n2) { + SASSERT(!found); m_solver.push(); tmp = m.mk_eq(res, n); m_solver.assert_expr(tmp); From 0490056e7a6ced9b9a93f56151233ff5b7bafe26 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 17 May 2021 19:19:28 -0700 Subject: [PATCH 29/40] na Signed-off-by: Nikolaj Bjorner --- src/opt/optsmt.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 0aebf522b..0bc7ba986 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -235,7 +235,7 @@ namespace opt { else { ++steps; } - if (delta_per_step > rational::one() || obj == last_objective) { + if (delta_per_step > rational::one() || (obj == last_objective && is_int)) { m_s->push(); ++num_scopes; bound = m_s->mk_ge(obj_index, obj + inf_eps(delta_per_step)); From 9031b5b94957f7da1ef9a1c5a8630ea3e368e500 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 18 May 2021 11:46:46 -0700 Subject: [PATCH 30/40] fix build Signed-off-by: Nikolaj Bjorner --- src/smt/tactic/ctx_solver_simplify_tactic.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp index e7608dd4b..fd05c4a8e 100644 --- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp +++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp @@ -190,6 +190,8 @@ protected: parent_pos = todo.back().m_parent; self_idx = todo.back().m_idx; n = names.back(); + bool found = false; + if (cache.contains(e)) { goto done; @@ -213,7 +215,6 @@ protected: sz = a->get_num_args(); n2 = nullptr; - bool found = false; // // This is a single traversal version of the context From 7b3a587505349959b90795dd81eb917ee0b6962d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 18 May 2021 18:04:03 -0700 Subject: [PATCH 31/40] fix #5225 --- src/smt/smt_consequences.cpp | 2 +- src/smt/smt_relevancy.cpp | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index 6b61bec62..b54e92a70 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -385,10 +385,10 @@ namespace smt { expr* e = kv.m_key; expr* val = kv.m_value; literal lit = mk_diseq(e, val); - mark_as_relevant(lit); if (get_assignment(lit) != l_undef) { continue; } + mark_as_relevant(lit); ++num_vars; push_scope(); assign(lit, b_justification::mk_axiom(), true); diff --git a/src/smt/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp index 5bc7bf9d2..6d20072cb 100644 --- a/src/smt/smt_relevancy.cpp +++ b/src/smt/smt_relevancy.cpp @@ -333,7 +333,8 @@ namespace smt { if (e != nullptr) { enode * curr = e; do { - set_relevant(curr->get_expr()); + if (!is_relevant_core(curr->get_expr())) + set_relevant(curr->get_expr()); curr = curr->get_next(); } while (curr != e); From d450fd4227122bb5fae139f4c15ea1c4c8403db4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 May 2021 10:03:49 -0700 Subject: [PATCH 32/40] #5215 --- src/qe/mbp/mbp_arith.cpp | 2 ++ src/sat/smt/q_ematch.cpp | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp index 04385b392..eb394c59f 100644 --- a/src/qe/mbp/mbp_arith.cpp +++ b/src/qe/mbp/mbp_arith.cpp @@ -374,6 +374,8 @@ namespace mbp { ts.push_back(var2expr(index2expr, v)); if (!d.m_coeff.is_zero()) ts.push_back(a.mk_numeral(d.m_coeff, is_int)); + if (ts.empty()) + ts.push_back(a.mk_numeral(rational(0), is_int)); t = mk_add(ts); if (!d.m_div.is_one() && is_int) t = a.mk_idiv(t, a.mk_numeral(d.m_div, is_int)); diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index 58ceab662..74856ccbe 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -166,9 +166,9 @@ namespace q { todo.push_back(e); while (!todo.empty()) { expr* t = todo.back(); + todo.pop_back(); if (m_mark.is_marked(t)) continue; - todo.pop_back(); m_mark.mark(t); if (is_ground(t)) { add_watch(ctx.get_egraph().find(t), clause_idx); From abe3ef2382ef3b36baf9c8827b4e57e16a328f91 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 May 2021 10:33:23 -0700 Subject: [PATCH 33/40] #5215 --- src/sat/smt/bv_internalize.cpp | 3 +-- src/sat/smt/bv_solver.cpp | 20 +++++++++++++------- src/sat/tactic/goal2sat.cpp | 20 +------------------- 3 files changed, 15 insertions(+), 28 deletions(-) diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index d6c3d4e64..f06d2d0df 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -284,7 +284,6 @@ namespace bv { } void solver::register_true_false_bit(theory_var v, unsigned idx) { - SASSERT(s().value(m_bits[v][idx]) != l_undef); sat::literal l = m_bits[v][idx]; SASSERT(l == mk_true() || ~l == mk_true()); bool is_true = l == mk_true(); @@ -369,7 +368,7 @@ namespace bv { sat::literal solver::mk_true() { if (m_true == sat::null_literal) { ctx.push(value_trail(m_true)); - m_true = ctx.internalize(m.mk_true(), false, false, false); + m_true = ctx.internalize(m.mk_true(), false, true, false); } return m_true; } diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index 3a35a73d5..0c57508ef 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -95,14 +95,20 @@ namespace bv { result.reset(); unsigned i = 0; for (literal b : m_bits[v]) { - switch (ctx.s().value(b)) { - case l_false: - break; - case l_undef: - return false; - case l_true: + if (b == ~m_true) + ; + else if (b == m_true) result += power2(i); - break; + else { + switch (ctx.s().value(b)) { + case l_false: + break; + case l_undef: + return false; + case l_true: + result += power2(i); + break; + } } ++i; } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 9cb21c769..c08944bee 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -75,7 +75,6 @@ struct goal2sat::imp : public sat::sat_internalizer { expr_ref_vector m_trail; func_decl_ref_vector m_unhandled_funs; bool m_default_external; - bool m_xor_solver { false }; bool m_euf { false }; bool m_drat { false }; bool m_is_redundant { false }; @@ -108,7 +107,6 @@ struct goal2sat::imp : public sat::sat_internalizer { sat_params sp(p); m_ite_extra = p.get_bool("ite_extra", true); m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); - m_xor_solver = p.get_bool("xor_solver", false); m_euf = sp.euf(); m_drat = sp.drat_file().is_non_empty_string(); } @@ -576,7 +574,7 @@ struct goal2sat::imp : public sat::sat_internalizer { } } - void convert_iff2(app * t, bool root, bool sign) { + void convert_iff(app * t, bool root, bool sign) { if (t->get_num_args() != 2) throw default_exception("unexpected number of arguments to xor"); SASSERT(t->get_num_args() == 2); @@ -611,13 +609,6 @@ struct goal2sat::imp : public sat::sat_internalizer { } } - void convert_iff(app * t, bool root, bool sign) { - if (!m_euf && is_xor(t)) - convert_ba(t, root, sign); - else - convert_iff2(t, root, sign); - } - func_decl_ref_vector const& interpreted_funs() { auto* ext = dynamic_cast(m_solver.get_extension()); if (ext) @@ -723,10 +714,6 @@ struct goal2sat::imp : public sat::sat_internalizer { } } - bool is_xor(app* t) const { - return m_xor_solver && m.is_iff(t) && m.is_iff(t->get_arg(1)); - } - struct scoped_stack { imp& i; sat::literal_vector& r; @@ -784,11 +771,6 @@ struct goal2sat::imp : public sat::sat_internalizer { visit(t->get_arg(0), root, !sign); continue; } - if (!m_euf && is_xor(t)) { - convert_ba(t, root, sign); - m_frame_stack.pop_back(); - continue; - } unsigned num = t->get_num_args(); while (m_frame_stack[fsz-1].m_idx < num) { expr * arg = t->get_arg(m_frame_stack[fsz-1].m_idx); From ec034679ce0680a1de90956250f76ce4a7fffcf2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 May 2021 12:42:38 -0700 Subject: [PATCH 34/40] #5215 memory leaks --- src/api/api_config_params.cpp | 6 ++---- src/math/lp/var_register.h | 2 +- src/sat/smt/euf_ackerman.cpp | 1 + src/shell/main.cpp | 25 ++++++++++++------------- src/util/gparams.cpp | 6 ++++++ src/util/gparams.h | 3 +++ src/util/scoped_timer.cpp | 1 + 7 files changed, 26 insertions(+), 18 deletions(-) diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp index 211e2abde..fd7c94f22 100644 --- a/src/api/api_config_params.cpp +++ b/src/api/api_config_params.cpp @@ -46,16 +46,14 @@ extern "C" { gparams::reset(); env_params::updt_params(); } - - static std::string g_Z3_global_param_get_buffer; Z3_bool_opt Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) { memory::initialize(UINT_MAX); LOG_Z3_global_param_get(param_id, param_value); *param_value = nullptr; try { - g_Z3_global_param_get_buffer = gparams::get_value(param_id); - *param_value = g_Z3_global_param_get_buffer.c_str(); + gparams::g_buffer() = gparams::get_value(param_id); + *param_value = gparams::g_buffer().c_str(); return true; } catch (z3_exception & ex) { diff --git a/src/math/lp/var_register.h b/src/math/lp/var_register.h index 6b1f02ca1..49767274d 100644 --- a/src/math/lp/var_register.h +++ b/src/math/lp/var_register.h @@ -39,7 +39,7 @@ public: }; class var_register { - svector m_local_to_external; + vector m_local_to_external; std::unordered_map m_external_to_local; unsigned m_locals_mask; unsigned m_locals_mask_inverted; diff --git a/src/sat/smt/euf_ackerman.cpp b/src/sat/smt/euf_ackerman.cpp index abf8e5625..941b1e0ac 100644 --- a/src/sat/smt/euf_ackerman.cpp +++ b/src/sat/smt/euf_ackerman.cpp @@ -34,6 +34,7 @@ namespace euf { m.dec_ref(inf->a); m.dec_ref(inf->b); m.dec_ref(inf->c); + dealloc(inf); } m_table.reset(); m_queue = nullptr; diff --git a/src/shell/main.cpp b/src/shell/main.cpp index ce8083cc2..73eee2ad1 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -46,7 +46,6 @@ Revision History: typedef enum { IN_UNSPECIFIED, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_LP, IN_Z3_LOG, IN_MPS, IN_DRAT } input_kind; -static std::string g_aux_input_file; static char const * g_input_file = nullptr; static char const * g_drat_input_file = nullptr; static bool g_standard_input = false; @@ -124,7 +123,7 @@ void display_usage() { std::cout << "Use 'z3 -p' for the complete list of global and module parameters.\n"; } -static void parse_cmd_line_args(int argc, char ** argv) { +static void parse_cmd_line_args(std::string& input_file, int argc, char ** argv) { long timeout = 0; int i = 1; char * eq_pos = nullptr; @@ -134,19 +133,18 @@ static void parse_cmd_line_args(int argc, char ** argv) { if (arg[0] == '-' && arg[1] == '-' && arg[2] == 0) { // Little hack used to read files with strange names such as -foo.smt2 // z3 -- -foo.smt2 - i++; - g_aux_input_file = ""; - for (; i < argc; i++) { - g_aux_input_file += argv[i]; - if (i < argc - 1) - g_aux_input_file += " "; - } if (g_input_file) { warning_msg("input file was already specified."); + break; } - else { - g_input_file = g_aux_input_file.c_str(); + i++; + input_file = ""; + for (; i < argc; i++) { + input_file += argv[i]; + if (i < argc - 1) + input_file += " "; } + g_input_file = input_file.c_str(); break; } @@ -321,11 +319,12 @@ static void parse_cmd_line_args(int argc, char ** argv) { int STD_CALL main(int argc, char ** argv) { - try{ + try { unsigned return_value = 0; memory::initialize(0); memory::exit_when_out_of_memory(true, "ERROR: out of memory"); - parse_cmd_line_args(argc, argv); + std::string input_file; + parse_cmd_line_args(input_file, argc, argv); env_params::updt_params(); if (g_input_file && g_standard_input) { diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index d227bced5..0c679e388 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -137,6 +137,7 @@ struct gparams::imp { smap m_module_params; params_ref m_params; region m_region; + std::string m_buffer; void check_registered() { if (m_modules_registered) @@ -651,3 +652,8 @@ void gparams::finalize() { dealloc(g_imp); DEALLOC_MUTEX(gparams_mux); } + +std::string& gparams::g_buffer() { + SASSERT(g_imp); + return g_imp->m_buffer; +} diff --git a/src/util/gparams.h b/src/util/gparams.h index 75e8cb02c..0efad4a07 100644 --- a/src/util/gparams.h +++ b/src/util/gparams.h @@ -26,6 +26,9 @@ class gparams { public: typedef default_exception exception; + static std::string& g_buffer(); + + /** \brief Reset all global and module parameters. */ diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index 644c234c4..e144cf636 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -153,4 +153,5 @@ void scoped_timer::finalize() { } } num_workers = 0; + available_workers.clear(); } From e0860ea17314324608de517ecb0aa07b115f3674 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 May 2021 13:31:31 -0700 Subject: [PATCH 35/40] fix #5279 --- src/ast/datatype_decl_plugin.cpp | 1 - src/ast/datatype_decl_plugin.h | 8 ++++---- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 152256c69..7190d5bf9 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -645,7 +645,6 @@ namespace datatype { return false; func_decl* c = get_accessor_constructor(f); SASSERT(n == 1); - std::cout << f->get_name() << " " << mk_pp(args[0], m) << "\n"; if (is_constructor(args[0])) return to_app(args[0])->get_decl() != c; return false; diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index 8b609073d..6ac438f16 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -103,10 +103,10 @@ namespace datatype { namespace param_size { class size { - unsigned m_ref; + unsigned m_ref{ 0 }; public: - size(): m_ref(0) {} - virtual ~size() {} + size() {} + virtual ~size() { } void inc_ref() { ++m_ref; } void dec_ref(); static size* mk_offset(sort_size const& s); @@ -197,7 +197,7 @@ namespace datatype { sort_ref_vector const& params() const { return m_params; } util& u() const { return m_util; } param_size::size* sort_size() { return m_sort_size; } - void set_sort_size(param_size::size* p) { m_sort_size = p; if (p) p->inc_ref(); m_sort = nullptr; } + void set_sort_size(param_size::size* p) { auto* q = m_sort_size; m_sort_size = p; if (p) p->inc_ref(); if (q) q->dec_ref(); m_sort = nullptr; } def* translate(ast_translation& tr, util& u); }; From cc12e3ed38cce114359f9bbc10705093891b83f2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 May 2021 16:52:24 -0700 Subject: [PATCH 36/40] fix #5280 --- src/smt/theory_lra.cpp | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 8ded1bb49..2141eb26c 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -983,9 +983,8 @@ public: enode * n1 = get_enode(lhs); enode * n2 = get_enode(rhs); TRACE("arith_verbose", tout << mk_pp(atom, m) << " " << is_arith(n1) << " " << is_arith(n2) << "\n";); - if (is_arith(n1) && is_arith(n2) && n1 != n2) { + if (is_arith(n1) && is_arith(n2) && n1 != n2) m_arith_eq_adapter.mk_axioms(n1, n2); - } } void assign_eh(bool_var v, bool is_true) { @@ -1024,7 +1023,7 @@ public: } bool use_diseqs() const { - return true; + return ctx().get_fparams().m_arith_eager_eq_axioms; } void new_diseq_eh(theory_var v1, theory_var v2) { @@ -1085,7 +1084,6 @@ public: } void relevant_eh(app* n) { - TRACE("arith", tout << mk_pp(n, m) << "\n";); expr* n1, *n2; if (a.is_mod(n, n1, n2)) mk_idiv_mod_axioms(n1, n2); @@ -2083,7 +2081,7 @@ public: bool is_true = m_asserted_atoms[m_asserted_qhead].m_is_true; m_to_check.push_back(bv); api_bound* b = nullptr; - TRACE("arith", tout << "propagate: " << bv << "\n";); + TRACE("arith", tout << "propagate: " << literal(bv, !is_true) << "\n";); if (m_bool_var2bound.find(bv, b)) { assert_bound(bv, is_true, *b); } @@ -2303,6 +2301,8 @@ public: ctx().mk_clause(m_core2.size(), m_core2.data(), js, CLS_TH_LEMMA, nullptr); } else { + std::cout << "assign " << lit << " " << core << " " << eqs.size() << "\n"; + ctx().display_literal_verbose(std::cout << " => ", lit) << "\n"; ctx().assign( lit, ctx().mk_justification( ext_theory_propagation_justification( @@ -2642,14 +2642,16 @@ public: if (sign) lit2.neg(); } - TRACE("arith", - ctx().display_literal_verbose(tout, lit1); - ctx().display_literal_verbose(tout << " => ", lit2); - tout << "\n";); updt_unassigned_bounds(v, -1); ++m_stats.m_bound_propagations2; reset_evidence(); m_core.push_back(lit1); + ctx().display_literals_verbose(std::cout, m_core); + ctx().display_literal_verbose(std::cout << " => ", lit2) << "\n"; + TRACE("arith", + ctx().display_literals_verbose(tout, m_core); + ctx().display_literal_verbose(tout << " => ", lit2); + tout << "\n";); m_params.push_back(parameter(m_farkas)); m_params.push_back(parameter(rational(1))); m_params.push_back(parameter(rational(1))); From c959e28d4a1f031c9a3f8823e2c4fa256362d013 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 20 May 2021 04:26:45 -0700 Subject: [PATCH 37/40] remove prints, remove ability to toggle eager_eq_axioms option NB. Spacer sets eager_eq_axioms option to false, but relevancy of this option is not clear at all as all other default paths don't use this option and theory_lra is incorrect when it is set to false. --- src/smt/theory_lra.cpp | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 2141eb26c..b76bb2fbf 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -976,8 +976,6 @@ public: } void internalize_eq_eh(app * atom, bool_var) { - if (!ctx().get_fparams().m_arith_eager_eq_axioms) - return; expr* lhs = nullptr, *rhs = nullptr; VERIFY(m.is_eq(atom, lhs, rhs)); enode * n1 = get_enode(lhs); @@ -1023,7 +1021,7 @@ public: } bool use_diseqs() const { - return ctx().get_fparams().m_arith_eager_eq_axioms; + return true; } void new_diseq_eh(theory_var v1, theory_var v2) { @@ -2301,8 +2299,6 @@ public: ctx().mk_clause(m_core2.size(), m_core2.data(), js, CLS_TH_LEMMA, nullptr); } else { - std::cout << "assign " << lit << " " << core << " " << eqs.size() << "\n"; - ctx().display_literal_verbose(std::cout << " => ", lit) << "\n"; ctx().assign( lit, ctx().mk_justification( ext_theory_propagation_justification( @@ -2646,8 +2642,6 @@ public: ++m_stats.m_bound_propagations2; reset_evidence(); m_core.push_back(lit1); - ctx().display_literals_verbose(std::cout, m_core); - ctx().display_literal_verbose(std::cout << " => ", lit2) << "\n"; TRACE("arith", ctx().display_literals_verbose(tout, m_core); ctx().display_literal_verbose(tout << " => ", lit2); From 03d2c5f3d0868526088cde0a163c542e5dae0eda Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 20 May 2021 12:58:27 -0700 Subject: [PATCH 38/40] consolidate literals --- src/sat/sat_types.h | 162 +------------------------------ src/smt/smt_clause.cpp | 4 +- src/smt/smt_context.cpp | 4 +- src/smt/smt_context.h | 2 +- src/smt/smt_context_pp.cpp | 4 +- src/smt/smt_literal.cpp | 55 ++++++----- src/smt/smt_literal.h | 87 +++-------------- src/test/finder.cpp | 110 ++++++++++----------- src/util/sat_literal.h | 194 +++++++++++++++++++++++++++++++++++++ 9 files changed, 299 insertions(+), 323 deletions(-) create mode 100644 src/util/sat_literal.h diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index 54e2b0e5e..57300a705 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -27,6 +27,7 @@ Revision History: #include "util/uint_set.h" #include "util/stopwatch.h" #include "util/symbol.h" +#include "util/sat_literal.h" class params_ref; class reslimit; @@ -35,89 +36,11 @@ class statistics; namespace sat { #define SAT_VB_LVL 10 - // TODO: there is some duplication in the sat and smt namespaces. - // The sat namespace should be the base. - // I should cleanup the smt namespace later. - - /** - \brief A boolean variable is just an integer. - */ - typedef unsigned bool_var; - - typedef svector bool_var_vector; - - const bool_var null_bool_var = UINT_MAX >> 1; - - /** - \brief The literal b is represented by the value 2*b, and - the literal (not b) by the value 2*b + 1 - */ - class literal { - unsigned m_val; - explicit literal(unsigned v):m_val(v) {} - public: - literal():m_val(null_bool_var << 1) { - SASSERT(var() == null_bool_var && !sign()); - } - - literal(bool_var v, bool _sign): - m_val((v << 1) + static_cast(_sign)) { - SASSERT(var() == v); - SASSERT(sign() == _sign); - } - - bool_var var() const { - return m_val >> 1; - } - - bool sign() const { - return m_val & 1; - } - - literal unsign() const { - return literal(m_val & ~1); - } - - unsigned index() const { - return m_val; - } - - void neg() { - m_val = m_val ^ 1; - } - - friend literal operator~(literal l) { - return literal(l.m_val ^ 1); - } - - unsigned to_uint() const { return m_val; } - - unsigned hash() const { return to_uint(); } - - friend literal to_literal(unsigned x); - friend bool operator<(literal const & l1, literal const & l2); - friend bool operator==(literal const & l1, literal const & l2); - friend bool operator!=(literal const & l1, literal const & l2); - }; - - const literal null_literal; - struct literal_hash : obj_hash {}; - - inline literal to_literal(unsigned x) { return literal(x); } - inline bool operator<(literal const & l1, literal const & l2) { return l1.m_val < l2.m_val; } - inline bool operator==(literal const & l1, literal const & l2) { return l1.m_val == l2.m_val; } - inline bool operator!=(literal const & l1, literal const & l2) { return l1.m_val != l2.m_val; } - - inline std::ostream & operator<<(std::ostream & out, literal l) { if (l == null_literal) out << "null"; else out << (l.sign() ? "-" : "") << l.var(); return out; } - - typedef svector literal_vector; - typedef std::pair literal_pair; typedef size_t clause_offset; typedef size_t ext_constraint_idx; typedef size_t ext_justification_idx; - struct literal2unsigned { unsigned operator()(literal l) const { return l.to_uint(); } }; typedef approx_set_tpl literal_approx_set; @@ -141,7 +64,6 @@ namespace sat { typedef svector model; - inline void negate(literal_vector& ls) { for (unsigned i = 0; i < ls.size(); ++i) ls[i].neg(); } inline lbool value_at(bool_var v, model const & m) { return m[v]; } inline lbool value_at(literal l, model const & m) { lbool r = value_at(l.var(), m); return l.sign() ? ~r : r; } @@ -155,88 +77,6 @@ namespace sat { return out; } - typedef tracked_uint_set uint_set; - - typedef uint_set bool_var_set; - - class literal_set { - uint_set m_set; - public: - literal_set(literal_vector const& v) { - for (unsigned i = 0; i < v.size(); ++i) insert(v[i]); - } - literal_set() {} - literal_vector to_vector() const { - literal_vector result; - for (literal lit : *this) result.push_back(lit); - return result; - } - literal_set& operator=(literal_vector const& v) { - reset(); - for (unsigned i = 0; i < v.size(); ++i) insert(v[i]); - return *this; - } - - void insert(literal l) { m_set.insert(l.index()); } - void remove(literal l) { m_set.remove(l.index()); } - literal pop() { return to_literal(m_set.erase()); } - bool contains(literal l) const { return m_set.contains(l.index()); } - bool empty() const { return m_set.empty(); } - unsigned size() const { return m_set.size(); } - void reset() { m_set.reset(); } - void finalize() { m_set.finalize(); } - class iterator { - uint_set::iterator m_it; - public: - iterator(uint_set::iterator it):m_it(it) {} - literal operator*() const { return to_literal(*m_it); } - iterator& operator++() { ++m_it; return *this; } - iterator operator++(int) { iterator tmp = *this; ++m_it; return tmp; } - bool operator==(iterator const& it) const { return m_it == it.m_it; } - bool operator!=(iterator const& it) const { return m_it != it.m_it; } - }; - iterator begin() const { return iterator(m_set.begin()); } - iterator end() const { return iterator(m_set.end()); } - literal_set& operator&=(literal_set const& other) { - m_set &= other.m_set; - return *this; - } - literal_set& operator|=(literal_set const& other) { - m_set |= other.m_set; - return *this; - } - }; - - struct dimacs_lit { - literal m_lit; - dimacs_lit(literal l):m_lit(l) {} - }; - - inline std::ostream & operator<<(std::ostream & out, dimacs_lit const & dl) { - literal l = dl.m_lit; - if (l.sign()) out << "-" << (l.var() + 1); - else out << (l.var() + 1); - return out; - } - - struct mk_lits_pp { - unsigned m_num; - literal const * m_lits; - mk_lits_pp(unsigned num, literal const * ls):m_num(num), m_lits(ls) {} - }; - - inline std::ostream & operator<<(std::ostream & out, mk_lits_pp const & ls) { - for (unsigned i = 0; i < ls.m_num; i++) { - if (i > 0) out << " "; - out << ls.m_lits[i]; - } - return out; - } - - inline std::ostream & operator<<(std::ostream & out, literal_vector const & ls) { - return out << mk_lits_pp(ls.size(), ls.data()); - } - class i_local_search { public: virtual ~i_local_search() {} diff --git a/src/smt/smt_clause.cpp b/src/smt/smt_clause.cpp index 291adbecf..654ed161f 100644 --- a/src/smt/smt_clause.cpp +++ b/src/smt/smt_clause.cpp @@ -101,7 +101,7 @@ namespace smt { out << "(clause"; for (unsigned i = 0; i < m_num_literals; i++) { out << " "; - m_lits[i].display(out, m, bool_var2expr_map); + smt::display(out, m_lits[i], m, bool_var2expr_map); } return out << ")"; } @@ -110,7 +110,7 @@ namespace smt { out << "(clause"; for (unsigned i = 0; i < m_num_literals; i++) { out << " "; - m_lits[i].display_compact(out, bool_var2expr_map); + smt::display_compact(out, m_lits[i], bool_var2expr_map); } return out << ")"; } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 9c45df153..d16e3a051 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3081,7 +3081,7 @@ namespace smt { literal l2 = *set_it; if (l2 != l) { b_justification js(l); - TRACE("theory_case_split", tout << "case split literal "; l2.display(tout, m, m_bool_var2expr.data()); tout << std::endl;); + TRACE("theory_case_split", tout << "case split literal "; smt::display(tout, l2, m, m_bool_var2expr.data()); tout << std::endl;); if (l2 == true_literal || l2 == false_literal || l2 == null_literal) continue; assign(~l2, js); if (inconsistent()) { @@ -4188,7 +4188,7 @@ namespace smt { for (unsigned i = 0; i < num_lits; i++) { display_literal(tout, v[i]); tout << "\n"; - v[i].display(tout, m, m_bool_var2expr.data()); + smt::display(tout, v[i], m, m_bool_var2expr.data()); tout << "\n\n"; } tout << "\n";); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 163d205f8..20d177955 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1357,7 +1357,7 @@ namespace smt { std::ostream& display_literal(std::ostream & out, literal l) const; - std::ostream& display_detailed_literal(std::ostream & out, literal l) const { l.display(out, m, m_bool_var2expr.data()); return out; } + std::ostream& display_detailed_literal(std::ostream & out, literal l) const { return smt::display(out, l, m, m_bool_var2expr.data()); } void display_literal_info(std::ostream & out, literal l) const; diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 4c3fb18e0..ed1dae13b 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -89,7 +89,7 @@ namespace smt { } std::ostream& context::display_literal(std::ostream & out, literal l) const { - l.display_compact(out, m_bool_var2expr.data()); return out; + smt::display_compact(out, l, m_bool_var2expr.data()); return out; } std::ostream& context::display_literals(std::ostream & out, unsigned num_lits, literal const * lits) const { @@ -120,7 +120,7 @@ namespace smt { } void context::display_literal_info(std::ostream & out, literal l) const { - l.display_compact(out, m_bool_var2expr.data()); + smt::display_compact(out, l, m_bool_var2expr.data()); display_literal_smt2(out, l); out << "relevant: " << is_relevant(bool_var2expr(l.var())) << ", val: " << get_assignment(l) << "\n"; } diff --git a/src/smt/smt_literal.cpp b/src/smt/smt_literal.cpp index 55592d9ab..f654f684d 100644 --- a/src/smt/smt_literal.cpp +++ b/src/smt/smt_literal.cpp @@ -22,41 +22,44 @@ Revision History: namespace smt { - void literal::display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const { - if (*this == true_literal) + std::ostream& display(std::ostream & out, literal lit, ast_manager & m, expr * const * bool_var2expr_map) { + if (lit == true_literal) out << "true"; - else if (*this == false_literal) + else if (lit == false_literal) out << "false"; - else if (*this == null_literal) + else if (lit == null_literal) out << "null"; - else if (sign()) - out << "(not " << mk_bounded_pp(bool_var2expr_map[var()], m, 3) << ")"; + else if (lit.sign()) + out << "(not " << mk_bounded_pp(bool_var2expr_map[lit.var()], m, 3) << ")"; else - out << mk_bounded_pp(bool_var2expr_map[var()], m, 3); + out << mk_bounded_pp(bool_var2expr_map[lit.var()], m, 3); + return out; } - void literal::display_smt2(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const { - if (*this == true_literal) + std::ostream& display_smt2(std::ostream & out, literal lit, ast_manager & m, expr * const * bool_var2expr_map) { + if (lit == true_literal) out << "true"; - else if (*this == false_literal) + else if (lit == false_literal) out << "false"; - else if (*this == null_literal) + else if (lit == null_literal) out << "null"; - else if (sign()) - out << "(not " << mk_pp(bool_var2expr_map[var()], m, 3) << ")"; + else if (lit.sign()) + out << "(not " << mk_pp(bool_var2expr_map[lit.var()], m, 3) << ")"; else - out << mk_pp(bool_var2expr_map[var()], m, 3); + out << mk_pp(bool_var2expr_map[lit.var()], m, 3); + return out; } - void literal::display_compact(std::ostream & out, expr * const * bool_var2expr_map) const { - if (*this == true_literal) + std::ostream& display_compact(std::ostream & out, literal lit, expr * const * bool_var2expr_map) { + if (lit == true_literal) out << "true"; - else if (*this == false_literal) + else if (lit == false_literal) out << "false"; - else if (sign()) - out << "(not #" << bool_var2expr_map[var()]->get_id() << ")"; + else if (lit.sign()) + out << "(not #" << bool_var2expr_map[lit.var()]->get_id() << ")"; else - out << "#" << bool_var2expr_map[var()]->get_id(); + out << "#" << bool_var2expr_map[lit.var()]->get_id(); + return out; } std::ostream & operator<<(std::ostream & out, literal l) { @@ -72,24 +75,26 @@ namespace smt { } std::ostream & operator<<(std::ostream & out, const literal_vector & v) { - display(out, v.begin(), v.end()); + ::display(out, v.begin(), v.end()); return out; } - void display_compact(std::ostream & out, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map) { + std::ostream& display_compact(std::ostream & out, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map) { for (unsigned i = 0; i < num_lits; i++) { if (i > 0) out << " "; - lits[i].display_compact(out, bool_var2expr_map); + display_compact(out, lits[i], bool_var2expr_map); } + return out; } - void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep) { + std::ostream& display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep) { for (unsigned i = 0; i < num_lits; i++) { if (i > 0) out << sep; - lits[i].display(out, m, bool_var2expr_map); + display(out, lits[i], m, bool_var2expr_map); } + return out; } /** diff --git a/src/smt/smt_literal.h b/src/smt/smt_literal.h index 863f4f13c..17ed9c6c4 100644 --- a/src/smt/smt_literal.h +++ b/src/smt/smt_literal.h @@ -21,90 +21,30 @@ Revision History: #include "ast/ast.h" #include "smt/smt_types.h" #include "util/approx_set.h" +#include "util/sat_literal.h" namespace smt { - /** - \brief The literal b is represented by the value 2*b, and - the literal (not b) by the value 2*b + 1 - - */ - class literal { - int m_val; - - public: - literal():m_val(-2) { - SASSERT(var() == null_bool_var && !sign()); - } - - explicit literal(bool_var v, bool sign = false): - m_val((v << 1) + static_cast(sign)) { - } - - bool_var var() const { - return m_val >> 1; - } - - bool sign() const { - return m_val & 1; - } - - int index() const { - return m_val; - } - - void neg() { - m_val = m_val ^ 1; - } - - friend literal operator~(literal l); - - friend literal to_literal(int x); - void display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const; + typedef sat::literal literal; + + inline literal to_literal(int x) { return sat::to_literal(x); } - void display_smt2(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const; - - void display_compact(std::ostream & out, expr * const * bool_var2expr_map) const; - - unsigned hash() const { return m_val; } - }; - - inline bool operator==(literal l1, literal l2) { - return l1.index() == l2.index(); - } - - inline bool operator!=(literal l1, literal l2) { - return l1.index() != l2.index(); - } - - inline bool operator<(literal l1, literal l2) { - return l1.index() < l2.index(); - } - - inline literal operator~(literal l) { - literal r; - r.m_val = l.m_val ^ 1; - return r; - } - - inline literal to_literal(int x) { - literal l; - l.m_val = x; - return l; - } - const literal null_literal; const literal true_literal(true_bool_var, false); const literal false_literal(true_bool_var, true); typedef svector literal_vector; typedef sbuffer literal_buffer; - std::ostream & operator<<(std::ostream & out, literal l); - std::ostream & operator<<(std::ostream & out, const literal_vector & v); - void display_compact(std::ostream & out, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map); + std::ostream& display(std::ostream & out, literal lit, ast_manager & m, expr * const * bool_var2expr_map); + + std::ostream& display_smt2(std::ostream & out, literal lit, ast_manager & m, expr * const * bool_var2expr_map); + + std::ostream& display_compact(std::ostream & out, literal lit, expr * const * bool_var2expr_map); - void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep = "\n"); + std::ostream& display_compact(std::ostream & out, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map); + + std::ostream& display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep = "\n"); template void neg_literals(unsigned num_lits, literal const * lits, T & result) { @@ -112,9 +52,6 @@ namespace smt { result.push_back(~lits[i]); } - struct literal2unsigned { unsigned operator()(literal l) const { return l.index(); } }; - - typedef approx_set_tpl literal_approx_set; bool backward_subsumption(unsigned num_lits1, literal const * lits1, unsigned num_lits2, literal const * lits2); }; diff --git a/src/test/finder.cpp b/src/test/finder.cpp index 488384fa3..c34a16d40 100644 --- a/src/test/finder.cpp +++ b/src/test/finder.cpp @@ -13,7 +13,7 @@ static void _init_solver(sat::solver& s) s.mk_var(); } -static void _mk_clause4(sat::solver& s, sat::literal w, sat::literal x, sat::literal y, sat::literal z) +static void _mk_clause4(sat::solver& s, sat::literal const & w, sat::literal const& x, sat::literal const& y, sat::literal const& z) { sat::literal lits[] = {w, x, y, z}; s.mk_clause(4, lits); @@ -41,10 +41,10 @@ static void tst_single_mux() { sat::solver s({}, r); _init_solver(s); - s.mk_clause({ 0, true }, { 1, true }, { 3, false }); - s.mk_clause({ 0, true }, { 1, false }, { 3, true }); - s.mk_clause({ 0, false }, { 2, true }, { 3, false }); - s.mk_clause({ 0, false }, { 2, false }, { 3, true }); + s.mk_clause(sat::literal(0, true), sat::literal(1, true), sat::literal(3, false)); + s.mk_clause(sat::literal(0, true), sat::literal(1, false), sat::literal(3, true)); + s.mk_clause(sat::literal(0, false), sat::literal(2, true), sat::literal(3, false)); + s.mk_clause(sat::literal(0, false), sat::literal(2, false), sat::literal(3, true)); _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_mux), "mux", 7, 0, 3, 5); } @@ -54,12 +54,12 @@ static void tst_single_maj() { sat::solver s({}, r); _init_solver(s); - s.mk_clause({ 0, false }, { 1, false }, { 3, true }); - s.mk_clause({ 0, false }, { 2, false }, { 3, true }); - s.mk_clause({ 1, false }, { 2, false }, { 3, true }); - s.mk_clause({ 0, true }, { 1, true }, { 3, false }); - s.mk_clause({ 0, true }, { 2, true }, { 3, false }); - s.mk_clause({ 1, true }, { 2, true }, { 3, false }); + s.mk_clause(sat::literal(0, false), sat::literal(1, false), sat::literal(3, true)); + s.mk_clause(sat::literal(0, false), sat::literal(2, false), sat::literal(3, true)); + s.mk_clause(sat::literal(1, false), sat::literal(2, false), sat::literal(3, true)); + s.mk_clause(sat::literal(0, true), sat::literal(1, true), sat::literal(3, false)); + s.mk_clause(sat::literal(0, true), sat::literal(2, true), sat::literal(3, false)); + s.mk_clause(sat::literal(1, true), sat::literal(2, true), sat::literal(3, false)); _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_maj), "maj", 6, 0, 2, 4); } @@ -69,10 +69,10 @@ static void tst_single_orand() { sat::solver s({}, r); _init_solver(s); - s.mk_clause({0, false}, {3, true}); - s.mk_clause({1, false}, {2, false}, {3, true}); - s.mk_clause({0, true}, {1, true}, {3, false}); - s.mk_clause({0, true}, {2, true}, {3, false}); + s.mk_clause(sat::literal(0, false), sat::literal(3, true)); + s.mk_clause(sat::literal(1, false), sat::literal(2, false), sat::literal(3, true)); + s.mk_clause(sat::literal(0, true), sat::literal(1, true), sat::literal(3, false)); + s.mk_clause(sat::literal(0, true), sat::literal(2, true), sat::literal(3, false)); _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_orand), "orand", 6, 0, 2, 4); } @@ -82,11 +82,11 @@ static void tst_single_and() { sat::solver s({}, r); _init_solver(s); - sat::literal ls1[] = {{0, true}, {1, true}, {2, true}, {3, false}}; + sat::literal ls1[] = {sat::literal(0, true), sat::literal(1, true), sat::literal(2, true), sat::literal(3, false)}; s.mk_clause(4, ls1); - s.mk_clause({0, false}, {3, true}); - s.mk_clause({1, false}, {3, true}); - s.mk_clause({2, false}, {3, true}); + s.mk_clause(sat::literal(0, false), sat::literal(3, true)); + s.mk_clause(sat::literal(1, false), sat::literal(3, true)); + s.mk_clause(sat::literal(2, false), sat::literal(3, true)); _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_and), "and", 6, 0, 2, 4); } @@ -96,14 +96,14 @@ static void tst_single_xor() { sat::solver s({}, r); _init_solver(s); - _mk_clause4(s, {0, true}, {1, false}, {2, false}, {3, false}); - _mk_clause4(s, {0, false}, {1, true}, {2, false}, {3, false}); - _mk_clause4(s, {0, false}, {1, false}, {2, true}, {3, false}); - _mk_clause4(s, {0, false}, {1, false}, {2, false}, {3, true}); - _mk_clause4(s, {0, false}, {1, true}, {2, true}, {3, true}); - _mk_clause4(s, {0, true}, {1, false}, {2, true}, {3, true}); - _mk_clause4(s, {0, true}, {1, true}, {2, false}, {3, true}); - _mk_clause4(s, {0, true}, {1, true}, {2, true}, {3, false}); + _mk_clause4(s, sat::literal(0, true), sat::literal(1, false), sat::literal(2, false), sat::literal(3, false)); + _mk_clause4(s, sat::literal(0, false), sat::literal(1, true), sat::literal(2, false), sat::literal(3, false)); + _mk_clause4(s, sat::literal(0, false), sat::literal(1, false), sat::literal(2, true), sat::literal(3, false)); + _mk_clause4(s, sat::literal(0, false), sat::literal(1, false), sat::literal(2, false), sat::literal(3, true)); + _mk_clause4(s, sat::literal(0, false), sat::literal(1, true), sat::literal(2, true), sat::literal(3, true)); + _mk_clause4(s, sat::literal(0, true), sat::literal(1, false), sat::literal(2, true), sat::literal(3, true)); + _mk_clause4(s, sat::literal(0, true), sat::literal(1, true), sat::literal(2, false), sat::literal(3, true)); + _mk_clause4(s, sat::literal(0, true), sat::literal(1, true), sat::literal(2, true), sat::literal(3, false)); _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_xor), "xor", 1, 3, 4, 6); } @@ -113,12 +113,12 @@ static void tst_single_andxor() { sat::solver s({}, r); _init_solver(s); - s.mk_clause({0, true}, {1, false}, {3, true}); - s.mk_clause({0, true}, {2, false}, {3, true}); - _mk_clause4(s, {0, true}, {1, true}, {2, true}, {3, false}); - s.mk_clause({0, false}, {1, false}, {3, false}); - s.mk_clause({0, false}, {2, false}, {3, false}); - _mk_clause4(s, {0, false}, {1, true}, {2, true}, {3, true}); + s.mk_clause(sat::literal(0, true), sat::literal(1, false), sat::literal(3, true)); + s.mk_clause(sat::literal(0, true), sat::literal(2, false), sat::literal(3, true)); + _mk_clause4(s, sat::literal(0, true), sat::literal(1, true), sat::literal(2, true), sat::literal(3, false)); + s.mk_clause(sat::literal(0, false), sat::literal(1, false), sat::literal(3, false)); + s.mk_clause(sat::literal(0, false), sat::literal(2, false), sat::literal(3, false)); + _mk_clause4(s, sat::literal(0, false), sat::literal(1, true), sat::literal(2, true), sat::literal(3, true)); _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_andxor), "andxor", 0, 6, 2, 4); } @@ -128,11 +128,11 @@ static void tst_single_xorand() { sat::solver s({}, r); _init_solver(s); - s.mk_clause({0, false}, {3, true}); - s.mk_clause({1, false}, {2, false}, {3, true}); - s.mk_clause({1, true}, {2, true}, {3, true}); - _mk_clause4(s, {0, true}, {1, true}, {2, false}, {3, false}); - _mk_clause4(s, {0, true}, {1, false}, {2, true}, {3, false}); + s.mk_clause(sat::literal(0, false), sat::literal(3, true)); + s.mk_clause(sat::literal(1, false), sat::literal(2, false), sat::literal(3, true)); + s.mk_clause(sat::literal(1, true), sat::literal(2, true), sat::literal(3, true)); + _mk_clause4(s, sat::literal(0, true), sat::literal(1, true), sat::literal(2, false), sat::literal(3, false)); + _mk_clause4(s, sat::literal(0, true), sat::literal(1, false), sat::literal(2, true), sat::literal(3, false)); _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_xorand), "xorand", 6, 0, 3, 5); } @@ -142,11 +142,11 @@ static void tst_single_gamble() { sat::solver s({}, r); _init_solver(s); - s.mk_clause({0, true}, {1, false}, {3, true}); - s.mk_clause({1, true}, {2, false}, {3, true}); - s.mk_clause({0, false}, {2, true}, {3, true}); - _mk_clause4(s, {0, false}, {1, false}, {2, false}, {3, false}); - _mk_clause4(s, {0, true}, {1, true}, {2, true}, {3, false}); + s.mk_clause(sat::literal(0, true), sat::literal(1, false), sat::literal(3, true)); + s.mk_clause(sat::literal(1, true), sat::literal(2, false), sat::literal(3, true)); + s.mk_clause(sat::literal(0, false), sat::literal(2, true), sat::literal(3, true)); + _mk_clause4(s, sat::literal(0, false), sat::literal(1, false), sat::literal(2, false), sat::literal(3, false)); + _mk_clause4(s, sat::literal(0, true), sat::literal(1, true), sat::literal(2, true), sat::literal(3, false)); _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_gamble), "gamble", 6, 0, 2, 4); } @@ -156,13 +156,13 @@ static void tst_single_onehot() { sat::solver s({}, r); _init_solver(s); - s.mk_clause({0, true}, {1, true}, {3, true}); - s.mk_clause({0, true}, {2, true}, {3, true}); - s.mk_clause({1, true}, {2, true}, {3, true}); - _mk_clause4(s, {0, false}, {1, false}, {2, false}, {3, true}); - _mk_clause4(s, {0, true}, {1, false}, {2, false}, {3, false}); - _mk_clause4(s, {0, false}, {1, true}, {2, false}, {3, false}); - _mk_clause4(s, {0, false}, {1, false}, {2, true}, {3, false}); + s.mk_clause(sat::literal(0, true), sat::literal(1, true), sat::literal(3, true)); + s.mk_clause(sat::literal(0, true), sat::literal(2, true), sat::literal(3, true)); + s.mk_clause(sat::literal(1, true), sat::literal(2, true), sat::literal(3, true)); + _mk_clause4(s, sat::literal(0, false), sat::literal(1, false), sat::literal(2, false), sat::literal(3, true)); + _mk_clause4(s, sat::literal(0, true), sat::literal(1, false), sat::literal(2, false), sat::literal(3, false)); + _mk_clause4(s, sat::literal(0, false), sat::literal(1, true), sat::literal(2, false), sat::literal(3, false)); + _mk_clause4(s, sat::literal(0, false), sat::literal(1, false), sat::literal(2, true), sat::literal(3, false)); _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_onehot), "onehot", 6, 0, 2, 4); } @@ -172,11 +172,11 @@ static void tst_single_dot() { sat::solver s({}, r); _init_solver(s); - s.mk_clause({0, false}, {2, false}, {3, true}); - s.mk_clause({0, true}, {1, true}, {3, true}); - s.mk_clause({0, true}, {2, true}, {3, true}); - s.mk_clause({0, false}, {2, true}, {3, false}); - _mk_clause4(s, {0, true}, {1, false}, {2, false}, {3, false}); + s.mk_clause(sat::literal(0, false), sat::literal(2, false), sat::literal(3, true)); + s.mk_clause(sat::literal(0, true), sat::literal(1, true), sat::literal(3, true)); + s.mk_clause(sat::literal(0, true), sat::literal(2, true), sat::literal(3, true)); + s.mk_clause(sat::literal(0, false), sat::literal(2, true), sat::literal(3, false)); + _mk_clause4(s, sat::literal(0, true), sat::literal(1, false), sat::literal(2, false), sat::literal(3, false)); _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_dot), "dot", 6, 0, 2, 4); } diff --git a/src/util/sat_literal.h b/src/util/sat_literal.h new file mode 100644 index 000000000..f8be2eb3f --- /dev/null +++ b/src/util/sat_literal.h @@ -0,0 +1,194 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + sat_literal.h + +Abstract: + + Literal datatype + +Author: + + Leonardo de Moura (leonardo) 2011-05-21. + +--*/ +#pragma once + +#include "util/lbool.h" +#include "util/vector.h" +#include "util/uint_set.h" + +namespace sat { + + /** + \brief A boolean variable is just an integer. + */ + typedef unsigned bool_var; + + typedef svector bool_var_vector; + + const bool_var null_bool_var = UINT_MAX >> 1; + + /** + \brief The literal b is represented by the value 2*b, and + the literal (not b) by the value 2*b + 1 + */ + class literal { + unsigned m_val; + public: + literal():m_val(null_bool_var << 1) { + SASSERT(var() == null_bool_var && !sign()); + } + + explicit literal(bool_var v, bool _sign = false): + m_val((v << 1) + static_cast(_sign)) { + SASSERT(var() == v); + SASSERT(sign() == _sign); + } + + bool_var var() const { + return m_val >> 1; + } + + bool sign() const { + return m_val & 1ul; + } + + literal unsign() const { + literal l; + l.m_val = m_val & ~1; + return l; + } + + unsigned index() const { + return m_val; + } + + void neg() { + m_val = m_val ^ 1; + } + + friend literal operator~(literal l) { + l.m_val = l.m_val ^1; + return l; + } + + unsigned to_uint() const { return m_val; } + + unsigned hash() const { return to_uint(); } + + friend literal to_literal(unsigned x); + friend bool operator<(literal const & l1, literal const & l2); + friend bool operator==(literal const & l1, literal const & l2); + friend bool operator!=(literal const & l1, literal const & l2); + }; + + const literal null_literal; + struct literal_hash : obj_hash {}; + + inline literal to_literal(unsigned x) { literal l; l.m_val = x; return l; } + inline bool operator<(literal const & l1, literal const & l2) { return l1.m_val < l2.m_val; } + inline bool operator==(literal const & l1, literal const & l2) { return l1.m_val == l2.m_val; } + inline bool operator!=(literal const & l1, literal const & l2) { return l1.m_val != l2.m_val; } + + + typedef svector literal_vector; + typedef std::pair literal_pair; + + struct literal2unsigned { unsigned operator()(literal l) const { return l.to_uint(); } }; + + typedef approx_set_tpl literal_approx_set; + + typedef approx_set_tpl var_approx_set; + + + inline void negate(literal_vector& ls) { for (unsigned i = 0; i < ls.size(); ++i) ls[i].neg(); } + + typedef tracked_uint_set uint_set; + + typedef uint_set bool_var_set; + + class literal_set { + uint_set m_set; + public: + literal_set(literal_vector const& v) { + for (unsigned i = 0; i < v.size(); ++i) insert(v[i]); + } + literal_set() {} + literal_vector to_vector() const { + literal_vector result; + for (literal lit : *this) result.push_back(lit); + return result; + } + literal_set& operator=(literal_vector const& v) { + reset(); + for (unsigned i = 0; i < v.size(); ++i) insert(v[i]); + return *this; + } + + void insert(literal l) { m_set.insert(l.index()); } + void remove(literal l) { m_set.remove(l.index()); } + literal pop() { return to_literal(m_set.erase()); } + bool contains(literal l) const { return m_set.contains(l.index()); } + bool empty() const { return m_set.empty(); } + unsigned size() const { return m_set.size(); } + void reset() { m_set.reset(); } + void finalize() { m_set.finalize(); } + class iterator { + uint_set::iterator m_it; + public: + iterator(uint_set::iterator it):m_it(it) {} + literal operator*() const { return to_literal(*m_it); } + iterator& operator++() { ++m_it; return *this; } + iterator operator++(int) { iterator tmp = *this; ++m_it; return tmp; } + bool operator==(iterator const& it) const { return m_it == it.m_it; } + bool operator!=(iterator const& it) const { return m_it != it.m_it; } + }; + iterator begin() const { return iterator(m_set.begin()); } + iterator end() const { return iterator(m_set.end()); } + literal_set& operator&=(literal_set const& other) { + m_set &= other.m_set; + return *this; + } + literal_set& operator|=(literal_set const& other) { + m_set |= other.m_set; + return *this; + } + }; + + struct dimacs_lit { + literal m_lit; + dimacs_lit(literal l):m_lit(l) {} + }; + + inline std::ostream & operator<<(std::ostream & out, dimacs_lit const & dl) { + literal l = dl.m_lit; + if (l.sign()) out << "-" << (l.var() + 1); + else out << (l.var() + 1); + return out; + } + + struct mk_lits_pp { + unsigned m_num; + literal const * m_lits; + mk_lits_pp(unsigned num, literal const * ls):m_num(num), m_lits(ls) {} + }; + + inline std::ostream & operator<<(std::ostream & out, mk_lits_pp const & ls) { + for (unsigned i = 0; i < ls.m_num; i++) { + if (i > 0) out << " "; + out << ls.m_lits[i]; + } + return out; + } + + inline std::ostream & operator<<(std::ostream & out, literal_vector const & ls) { + return out << mk_lits_pp(ls.size(), ls.data()); + } + +}; + +inline std::ostream & operator<<(std::ostream & out, sat::literal l) { if (l == sat::null_literal) out << "null"; else out << (l.sign() ? "-" : "") << l.var(); return out; } + From 9cc1549dbec90a01e91def0102b83bc12039b19f Mon Sep 17 00:00:00 2001 From: Matt Thornton Date: Thu, 20 May 2021 23:19:31 +0100 Subject: [PATCH 39/40] Use osx-x64 for mac rid rather than macos. (#5288) --- scripts/mk_nuget_release.py | 4 ++-- scripts/mk_nuget_task.py | 4 ++-- src/api/dotnet/Microsoft.Z3.csproj.in | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/scripts/mk_nuget_release.py b/scripts/mk_nuget_release.py index 1763f457d..d872645a6 100644 --- a/scripts/mk_nuget_release.py +++ b/scripts/mk_nuget_release.py @@ -48,7 +48,7 @@ os_info = {"z64-ubuntu-14" : ('so', 'ubuntu.14.04-x64'), 'x64-win' : ('dll', 'win-x64'), # Skip x86 as I can't get dotnet build to produce AnyCPU TargetPlatform # 'x86-win' : ('dll', 'win-x86'), - 'osx' : ('dylib', 'macos'), + 'osx' : ('dylib', 'osx-x64'), 'debian' : ('so', 'debian.8-x64') } def classify_package(f): @@ -69,7 +69,7 @@ def unpack(): # +- ubuntu.16.04-x64 # +- ubuntu.14.04-x64 # +- debian.8-x64 - # +- macos + # +- osx-x64 # + for f in os.listdir("packages"): print(f) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index 8039be69a..08f2680a8 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -28,7 +28,7 @@ os_info = {"z64-ubuntu-14" : ('so', 'ubuntu.14.04-x64'), 'glibc-2.31' : ('so', 'glibc-x64'), 'x64-win' : ('dll', 'win-x64'), 'x86-win' : ('dll', 'win-x86'), - 'osx' : ('dylib', 'macos'), + 'osx' : ('dylib', 'osx-x64'), 'debian' : ('so', 'debian.8-x64') } def classify_package(f): @@ -52,7 +52,7 @@ def unpack(packages, symbols): # +- win-x64 # +- win-x86 # +- ubuntu-x64 - # +- macos + # +- osx-x64 # + tmp = "tmp" if not symbols else "tmpsym" for f in os.listdir(packages): diff --git a/src/api/dotnet/Microsoft.Z3.csproj.in b/src/api/dotnet/Microsoft.Z3.csproj.in index 413c1d0ce..157334242 100644 --- a/src/api/dotnet/Microsoft.Z3.csproj.in +++ b/src/api/dotnet/Microsoft.Z3.csproj.in @@ -84,7 +84,7 @@ ${Z3_DOTNET_COMPILE_ITEMS} runtimes\linux-x64\native - runtimes\macos\native + runtimes\osx-x64\native From a59dcfdeabd57730ea0d122dc3254255d7b39465 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 20 May 2021 15:23:39 -0700 Subject: [PATCH 40/40] update python tag Signed-off-by: Nikolaj Bjorner --- scripts/nightly.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 5c0be55c1..d4c72a65f 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -74,7 +74,7 @@ stages: vmImage: "Ubuntu-18.04" container: "quay.io/pypa/manylinux2010_x86_64:latest" variables: - python: "/opt/python/cp35-cp35m/bin/python" + python: "/opt/python/cp37-cp37m/bin/python" steps: - script: $(python) scripts/mk_unix_dist.py --nodotnet --nojava - script: git clone https://github.com/z3prover/z3test z3test