diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 0efb3dcce..e72acf3d6 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -63,7 +63,6 @@ namespace z3 { class func_entry; class statistics; class apply_result; - class fixedpoint; template class ast_vector_tpl; typedef ast_vector_tpl ast_vector; typedef ast_vector_tpl expr_vector; @@ -286,6 +285,15 @@ namespace z3 { expr num_val(int n, sort const & s); + /** + \brief parsing + */ + expr parse_string(char const* s); + expr parse_file(char const* file); + + expr parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls); + expr parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls); + /** \brief Interpolation support */ @@ -442,7 +450,10 @@ namespace z3 { \brief Return the internal sort kind. */ Z3_sort_kind sort_kind() const { return Z3_get_sort_kind(*m_ctx, *this); } - + /** + \brief Return name of sort. + */ + symbol name() const { Z3_symbol s = Z3_get_sort_name(ctx(), *this); check_error(); return symbol(ctx(), s); } /** \brief Return true if this sort is the Boolean sort. */ @@ -2454,6 +2465,37 @@ namespace z3 { return expr(a.ctx(), Z3_mk_interpolant(a.ctx(), a)); } + inline expr context::parse_string(char const* s) { + Z3_ast r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0); + check_error(); + return expr(*this, r); + + } + inline expr context::parse_file(char const* s) { + Z3_ast r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0); + check_error(); + return expr(*this, r); + } + + inline expr context::parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls) { + array sort_names(sorts.size()); + array decl_names(decls.size()); + array sorts1(sorts); + array decls1(decls); + for (unsigned i = 0; i < sorts.size(); ++i) { + sort_names[i] = sorts[i].name(); + } + for (unsigned i = 0; i < decls.size(); ++i) { + decl_names[i] = decls[i].name(); + } + Z3_ast r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr()); + check_error(); + return expr(*this, r); + } + + // inline expr context::parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls); + + inline check_result context::compute_interpolant(expr const& pat, params const& p, expr_vector& i, model& m) { Z3_ast_vector interp = 0; Z3_model mdl = 0; diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index a976de8be..d9f060784 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -197,6 +197,7 @@ public: is_sat = process_mutex(); if (is_sat != l_true) return is_sat; while (m_lower < m_upper) { + if (m_lower >= m_upper) break; TRACE("opt", display_vec(tout, m_asms); s().display(tout); @@ -235,8 +236,10 @@ public: init_local(); trace(); exprs cs; + lbool is_sat = process_mutex(); + if (is_sat != l_true) return is_sat; while (m_lower < m_upper) { - lbool is_sat = check_sat_hill_climb(m_asms); + is_sat = check_sat_hill_climb(m_asms); if (m.canceled()) { return l_undef; } @@ -272,7 +275,6 @@ public: } lbool process_mutex() { -#if 0 vector mutexes; lbool is_sat = s().find_mutexes(m_asms, mutexes); if (is_sat != l_true) { @@ -281,7 +283,9 @@ public: for (unsigned i = 0; i < mutexes.size(); ++i) { process_mutex(mutexes[i]); } -#endif + if (!mutexes.empty()) { + trace(); + } return l_true; } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index d8d273f2b..f553acb29 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -835,48 +835,66 @@ namespace sat { lbool solver::bounded_search() { while (true) { checkpoint(); - while (true) { - propagate(true); - if (!inconsistent()) - break; - if (!resolve_conflict()) - return l_false; - if (m_conflicts > m_config.m_max_conflicts) - return l_undef; - if (m_conflicts_since_restart > m_restart_threshold) - return l_undef; - if (scope_lvl() == 0) { - cleanup(); // cleaner may propagate frozen clauses - if (inconsistent()) { - TRACE("sat", tout << "conflict at level 0\n";); - return l_false; - } - gc(); - } + bool done = false; + while (!done) { + lbool is_sat = propagate_and_backjump_step(done); + if (is_sat != l_true) return is_sat; } gc(); if (!decide()) { - if (m_ext) { - switch (m_ext->check()) { - case CR_DONE: - mk_model(); - return l_true; - case CR_CONTINUE: - break; - case CR_GIVEUP: - throw abort_solver(); - } - } - else { - mk_model(); - return l_true; + lbool is_sat = final_check(); + if (is_sat != l_undef) { + return is_sat; } } } } + lbool solver::propagate_and_backjump_step(bool& done) { + done = true; + propagate(true); + if (!inconsistent()) + return l_true; + if (!resolve_conflict()) + return l_false; + if (m_conflicts > m_config.m_max_conflicts) + return l_undef; + if (m_conflicts_since_restart > m_restart_threshold) + return l_undef; + if (scope_lvl() == 0) { + cleanup(); // cleaner may propagate frozen clauses + if (inconsistent()) { + TRACE("sat", tout << "conflict at level 0\n";); + return l_false; + } + gc(); + } + done = false; + return l_true; + } + + lbool solver::final_check() { + if (m_ext) { + switch (m_ext->check()) { + case CR_DONE: + mk_model(); + return l_true; + case CR_CONTINUE: + break; + case CR_GIVEUP: + throw abort_solver(); + } + return l_undef; + } + else { + mk_model(); + return l_true; + } + } + + bool solver::check_inconsistent() { if (inconsistent()) { if (tracking_assumptions()) @@ -3035,6 +3053,220 @@ namespace sat { return r; } + lbool solver::find_mutexes(literal_vector const& lits, vector & mutexes) { + literal_vector ps(lits); + m_user_bin_clauses.reset(); + m_binary_clause_graph.reset(); + collect_bin_clauses(m_user_bin_clauses, true); + collect_bin_clauses(m_user_bin_clauses, false); + for (unsigned i = 0; i < m_user_bin_clauses.size(); ++i) { + literal l1 = m_user_bin_clauses[i].first; + literal l2 = m_user_bin_clauses[i].second; + m_binary_clause_graph.reserve(l1.index() + 1); + m_binary_clause_graph.reserve(l2.index() + 1); + m_binary_clause_graph.reserve((~l1).index() + 1); + m_binary_clause_graph.reserve((~l2).index() + 1); + m_binary_clause_graph[l1.index()].push_back(l2); + m_binary_clause_graph[l2.index()].push_back(l1); + } + while (!ps.empty()) { + literal_vector mutex; + literal_set other(ps); + while (!other.empty()) { + literal_set conseq; + literal p = other.pop(); + mutex.push_back(p); + if (other.empty()) { + break; + } + get_reachable(p, other, conseq); + other = conseq; + } + if (mutex.size() > 1) { + mutexes.push_back(mutex); + } + for (unsigned i = 0; i < mutex.size(); ++i) { + ps.erase(mutex[i]); + } + } + return l_true; + } + + void solver::get_reachable(literal p, literal_set const& goal, literal_set& reachable) { + literal_set seen; + literal_vector todo; + todo.push_back(p); + while (!todo.empty()) { + p = todo.back(); + todo.pop_back(); + if (seen.contains(p)) { + continue; + } + seen.insert(p); + literal np = ~p; + if (goal.contains(np)) { + reachable.insert(np); + } + todo.append(m_binary_clause_graph[np.index()]); + } + } + + lbool solver::get_consequences(literal_vector const& asms, bool_var_vector const& vars, vector& conseq) { + literal_vector lits; + lbool is_sat = check(asms.size(), asms.c_ptr()); + if (is_sat != l_true) { + return is_sat; + } + for (unsigned i = 0; i < vars.size(); ++i) { + bool_var v = vars[i]; + switch (get_model()[v]) { + case l_true: lits.push_back(literal(v, false)); break; + case l_false: lits.push_back(literal(v, true)); break; + default: break; + } + } + return get_consequences(asms, lits, conseq); + } + + lbool solver::get_consequences(literal_vector const& asms, literal_vector const& lits, vector& conseq) { + m_antecedents.reset(); + literal_set unfixed(lits), assumptions(asms); + + pop_to_base_level(); + if (inconsistent()) return l_false; + init_search(); + propagate(false); + if (inconsistent()) return l_false; + init_assumptions(asms.size(), asms.c_ptr(), 0, 0); + propagate(false); + if (check_inconsistent()) return l_false; + + unsigned num_units = 0; + extract_fixed_consequences(num_units, assumptions, unfixed, conseq); + while (!unfixed.empty()) { + checkpoint(); + literal_set::iterator it = unfixed.begin(), end = unfixed.end(); + unsigned chunk_size = 100; + for (; it != end && chunk_size > 0; ++it) { + literal lit = *it; + if (value(lit) != l_undef) { + continue; + } + --chunk_size; + push(); + assign(~lit, justification()); + propagate(false); + while (inconsistent()) { + if (!resolve_conflict()) { + TRACE("sat", tout << "inconsistent\n";); + return l_false; + } + propagate(false); + } + } + lbool is_sat; + while (true) { + is_sat = bounded_search(); + if (is_sat == l_undef) { + restart(); + continue; + } + break; + } + if (is_sat == l_false) { + TRACE("sat", tout << "unsat\n";); + m_inconsistent = false; + } + if (is_sat == l_true) { + delete_unfixed(unfixed); + } + extract_fixed_consequences(num_units, assumptions, unfixed, conseq); + } + return l_true; + } + + void solver::delete_unfixed(literal_set& unfixed) { + literal_set to_keep; + literal_set::iterator it = unfixed.begin(), end = unfixed.end(); + for (; it != end; ++it) { + literal lit = *it; + if (value(lit) == l_true) { + to_keep.insert(lit); + } + } + unfixed = to_keep; + } + + void solver::extract_fixed_consequences(unsigned& start, literal_set const& assumptions, literal_set& unfixed, vector& conseq) { + if (scope_lvl() > 1) { + pop(scope_lvl() - 1); + } + SASSERT(!inconsistent()); + unsigned sz = m_trail.size(); + for (unsigned i = start; i < sz; ++i) { + extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq); + } + start = sz; + } + + void solver::extract_assumptions(literal lit, index_set& s) { + justification js = m_justification[lit.var()]; + switch (js.get_kind()) { + case justification::NONE: + break; + case justification::BINARY: + s |= m_antecedents.find(js.get_literal().var()); + break; + case justification::TERNARY: + s |= m_antecedents.find(js.get_literal1().var()); + s |= m_antecedents.find(js.get_literal2().var()); + break; + case justification::CLAUSE: { + clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset())); + for (unsigned i = 0; i < c.size(); ++i) { + if (c[i] != lit) { + s |= m_antecedents.find(c[i].var()); + } + } + break; + } + case justification::EXT_JUSTIFICATION: { + fill_ext_antecedents(lit, js); + literal_vector::iterator it = m_ext_antecedents.begin(); + literal_vector::iterator end = m_ext_antecedents.end(); + for (; it != end; ++it) { + s |= m_antecedents.find(it->var()); + } + break; + } + default: + UNREACHABLE(); + break; + } + } + + void solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, literal_set& unfixed, vector& conseq) { + index_set s; + if (assumptions.contains(lit)) { + s.insert(lit.index()); + } + else { + add_assumption(lit); + extract_assumptions(lit, s); + } + m_antecedents.insert(lit.var(), s); + if (unfixed.contains(lit)) { + literal_vector cons; + cons.push_back(lit); + index_set::iterator it = s.begin(), end = s.end(); + for (; it != end; ++it) { + cons.push_back(to_literal(*it)); + } + unfixed.remove(lit); + conseq.push_back(cons); + } + } + void solver::asymmetric_branching() { if (scope_lvl() > 0 || inconsistent()) return; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 95988f3ca..785bc6856 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -300,6 +300,8 @@ namespace sat { bool decide(); bool_var next_var(); lbool bounded_search(); + lbool final_check(); + lbool propagate_and_backjump_step(bool& done); void init_search(); literal_vector m_min_core; @@ -409,6 +411,7 @@ namespace sat { void gc_lit(clause_vector& clauses, literal lit); void gc_bin(bool learned, literal nlit); void gc_var(bool_var v); + bool_var max_var(clause_vector& clauses, bool_var v); bool_var max_var(bool learned, bool_var v); @@ -428,6 +431,35 @@ namespace sat { void asymmetric_branching(); unsigned scc_bin(); + // ----------------------- + // + // Auxiliary methods. + // + // ----------------------- + public: + lbool find_mutexes(literal_vector const& lits, vector & mutexes); + + lbool get_consequences(literal_vector const& assms, bool_var_vector const& vars, vector& conseq); + + private: + + typedef hashtable index_set; + + u_map m_antecedents; + vector m_binary_clause_graph; + + void extract_assumptions(literal lit, index_set& s); + + void get_reachable(literal p, literal_set const& goal, literal_set& reachable); + + lbool get_consequences(literal_vector const& assms, literal_vector const& lits, vector& conseq); + + void delete_unfixed(literal_set& unfixed); + + void extract_fixed_consequences(unsigned& start, literal_set const& assumptions, literal_set& unfixed, vector& conseq); + + void extract_fixed_consequences(literal lit, literal_set const& assumptions, literal_set& unfixed, vector& conseq); + // ----------------------- // // Activity related stuff diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index ce6b199d6..6139b3e22 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -107,6 +107,7 @@ public: return check_sat(num_assumptions, assumptions, 0, 0); } + void display_weighted(std::ostream& out, unsigned sz, expr * const * assumptions, unsigned const* weights) { m_weights.reset(); if (weights != 0) { @@ -231,6 +232,33 @@ public: return 0; } + virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { + sat::literal_vector ls; + u_map lit2var; + for (unsigned i = 0; i < vars.size(); ++i) { + expr* e = vars[i]; + bool neg = m.is_not(e, e); + sat::bool_var v = m_map.to_bool_var(e); + if (v != sat::null_bool_var) { + sat::literal lit(v, neg); + ls.push_back(lit); + lit2var.insert(lit.index(), vars[i]); + } + } + vector ls_mutexes; + m_solver.find_mutexes(ls, ls_mutexes); + for (unsigned i = 0; i < ls_mutexes.size(); ++i) { + sat::literal_vector const ls_mutex = ls_mutexes[i]; + expr_ref_vector mutex(m); + for (unsigned j = 0; j < ls_mutex.size(); ++j) { + mutex.push_back(lit2var.find(ls_mutex[j].index())); + } + mutexes.push_back(mutex); + } + return l_true; + } + + virtual std::string reason_unknown() const { return m_unknown; } diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index c0c087e59..697af2e2d 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -105,6 +105,7 @@ namespace sat { inline std::ostream & operator<<(std::ostream & out, literal l) { out << (l.sign() ? "-" : "") << l.var(); return out; } typedef svector literal_vector; + typedef std::pair literal_pair; typedef unsigned clause_offset; typedef unsigned ext_constraint_idx; @@ -161,6 +162,17 @@ namespace sat { m_set.push_back(v); } + void remove(unsigned v) { + if (contains(v)) { + m_in_set[v] = false; + unsigned i = 0; + for (i = 0; i < m_set.size() && m_set[i] != v; ++i); + SASSERT(i < m_set.size()); + m_set[i] = m_set.back(); + m_set.pop_back(); + } + } + uint_set& operator=(uint_set const& other) { m_in_set = other.m_in_set; m_set = other.m_set; @@ -228,6 +240,7 @@ namespace sat { return result; } 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(); } diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 6ef828787..c75088246 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -137,6 +137,11 @@ lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector } lbool solver::find_mutexes(expr_ref_vector const& vars, vector& mutexes) { + return l_true; +#if 0 + // complete for literals, but inefficient. + // see more efficient (incomplete) version in sat_solver + mutexes.reset(); ast_manager& m = vars.get_manager(); @@ -187,19 +192,9 @@ lbool solver::find_mutexes(expr_ref_vector const& vars, vector& A.remove(mutex[i].get()); } } - - // While A != {}: - // R = {} - // P = ~A - // While P != {}: - // Pick p in ~P, - // R = R u { p } - // Let Q be consequences over P of p modulo F. - // Let P &= Q - // If |R| > 1: Yield R - // A \= R - return l_true; +#endif + } bool solver::is_literal(ast_manager& m, expr* e) {