mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-03 01:40:22 +00:00
Code Activity

Merge branch 'upstream-master' into release-1.0

Browse source 
Conflicts:
	src/cmd_context/check_logic.cpp
	src/cmd_context/cmd_context.cpp
	src/cmd_context/cmd_context.h
	src/smt/params/smt_params_helper.pyg
	src/smt/smt_context.cpp
This commit is contained in:
Murphy Berzish 2017-02-18 15:04:44 -05:00
commit 235ea79043
588 changed files with 21784 additions and 15202 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/solver/check_sat_result.h
View file

@ -48,12 +48,18 @@ public:
lbool status() const { return m_status; }
virtual void collect_statistics(statistics & st) const = 0;
virtual void get_unsat_core(ptr_vector<expr> & r) = 0;
virtual void get_unsat_core(expr_ref_vector & r) {
ptr_vector<expr> core;
get_unsat_core(core);
r.append(core.size(), core.c_ptr());
}
virtual void get_model(model_ref & m) = 0;
virtual proof * get_proof() = 0;
virtual std::string reason_unknown() const = 0;
virtual void set_reason_unknown(char const* msg) = 0;
virtual void get_labels(svector<symbol> & r) = 0;
virtual ast_manager& get_manager() = 0;
virtual ast_manager& get_manager() const = 0;
};
/**
@ -69,7 +75,7 @@ struct simple_check_sat_result : public check_sat_result {
simple_check_sat_result(ast_manager & m);
virtual ~simple_check_sat_result();
virtual ast_manager& get_manager() { return m_proof.get_manager(); }
virtual ast_manager& get_manager() const { return m_proof.get_manager(); }
virtual void collect_statistics(statistics & st) const;
virtual void get_unsat_core(ptr_vector<expr> & r);
virtual void get_model(model_ref & m);

32
src/solver/combined_solver.cpp
View file

@ -21,6 +21,7 @@ Notes:
#include"solver.h"
#include"scoped_timer.h"
#include"combined_solver_params.hpp"
#include"common_msgs.h"
#define PS_VB_LVL 15
/**
@ -101,7 +102,7 @@ private:
m_inc_unknown_behavior = static_cast<inc_unknown_behavior>(p.solver2_unknown());
}
virtual ast_manager& get_manager() { return m_solver1->get_manager(); }
virtual ast_manager& get_manager() const { return m_solver1->get_manager(); }
bool has_quantifiers() const {
unsigned sz = get_num_assertions();
@ -194,12 +195,29 @@ public:
return m_solver1->get_scope_level();
}
virtual lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
switch_inc_mode();
m_use_solver1_results = false;
try {
return m_solver2->get_consequences(asms, vars, consequences);
}
catch (z3_exception& ex) {
if (get_manager().canceled()) {
set_reason_unknown(Z3_CANCELED_MSG);
}
else {
set_reason_unknown(ex.msg());
}
}
return l_undef;
}
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
m_check_sat_executed = true;
m_use_solver1_results = false;
if (get_num_assumptions() != 0 ||
num_assumptions > 0 || // assumptions were provided
num_assumptions > 0 || // assumptions were provided
m_ignore_solver1) {
// must use incremental solver
switch_inc_mode();
@ -209,7 +227,7 @@ public:
if (m_inc_mode) {
if (m_inc_timeout == UINT_MAX) {
IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 2 (without a timeout)\")\n";);
lbool r = m_solver2->check_sat(0, 0);
lbool r = m_solver2->check_sat(num_assumptions, assumptions);
if (r != l_undef || !use_solver1_when_undef()) {
return r;
}
@ -220,7 +238,7 @@ public:
lbool r = l_undef;
try {
scoped_timer timer(m_inc_timeout, &eh);
r = m_solver2->check_sat(0, 0);
r = m_solver2->check_sat(num_assumptions, assumptions);
}
catch (z3_exception&) {
if (!eh.m_canceled) {
@ -236,7 +254,7 @@ public:
IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 1\")\n";);
m_use_solver1_results = true;
return m_solver1->check_sat(0, 0);
return m_solver1->check_sat(num_assumptions, assumptions);
}
virtual void set_progress_callback(progress_callback * callback) {
@ -262,8 +280,8 @@ public:
return m_solver2->get_assumption(idx - c1);
}
virtual void display(std::ostream & out) const {
m_solver1->display(out);
virtual std::ostream& display(std::ostream & out) const {
return m_solver1->display(out);
}
virtual void collect_statistics(statistics & st) const {

395
src/solver/mus.cpp Normal file
View file

@ -0,0 +1,395 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
mus.cpp
Abstract:
MUS extraction.
Author:
Nikolaj Bjorner (nbjorner) 2014-20-7
Notes:
--*/
#include "solver.h"
#include "mus.h"
#include "ast_pp.h"
#include "ast_util.h"
#include "model_evaluator.h"
struct mus::imp {
typedef obj_hashtable<expr> expr_set;
solver& m_solver;
ast_manager& m;
expr_ref_vector m_lit2expr;
expr_ref_vector m_assumptions;
obj_map<expr, unsigned> m_expr2lit;
model_ref m_model;
expr_ref_vector m_soft;
vector<rational> m_weights;
rational m_weight;
imp(solver& s):
m_solver(s), m(s.get_manager()), m_lit2expr(m), m_assumptions(m), m_soft(m)
{}
void reset() {
m_lit2expr.reset();
m_expr2lit.reset();
m_assumptions.reset();
}
bool is_literal(expr* lit) const {
expr* l;
return is_uninterp_const(lit) || (m.is_not(lit, l) && is_uninterp_const(l));
}
unsigned add_soft(expr* lit) {
SASSERT(is_literal(lit));
unsigned idx = m_lit2expr.size();
m_expr2lit.insert(lit, idx);
m_lit2expr.push_back(lit);
TRACE("mus", tout << idx << ": " << mk_pp(lit, m) << "\n" << m_lit2expr << "\n";);
return idx;
}
void add_assumption(expr* lit) {
SASSERT(is_literal(lit));
m_assumptions.push_back(lit);
}
lbool get_mus(expr_ref_vector& mus) {
m_model.reset();
mus.reset();
if (m_lit2expr.size() == 1) {
mus.push_back(m_lit2expr.back());
return l_true;
}
return get_mus1(mus);
}
lbool get_mus(ptr_vector<expr>& mus) {
mus.reset();
expr_ref_vector result(m);
lbool r = get_mus(result);
mus.append(result.size(), result.c_ptr());
return r;
}
lbool get_mus1(expr_ref_vector& mus) {
ptr_vector<expr> unknown(m_lit2expr.size(), m_lit2expr.c_ptr());
ptr_vector<expr> core_exprs;
while (!unknown.empty()) {
IF_VERBOSE(12, verbose_stream() << "(mus reducing core: " << unknown.size() << " new core: " << mus.size() << ")\n";);
TRACE("mus", display_vec(tout << "core: ", unknown); display_vec(tout << "mus: ", mus););
expr* lit = unknown.back();
unknown.pop_back();
expr_ref not_lit(mk_not(m, lit), m);
lbool is_sat = l_undef;
{
scoped_append _sa1(*this, mus, unknown);
scoped_append _sa2(*this, mus, m_assumptions);
mus.push_back(not_lit);
is_sat = m_solver.check_sat(mus);
}
switch (is_sat) {
case l_undef:
return is_sat;
case l_true:
mus.push_back(lit);
update_model();
break;
default:
core_exprs.reset();
m_solver.get_unsat_core(core_exprs);
if (!core_exprs.contains(not_lit)) {
// unknown := core_exprs \ mus
unknown.reset();
for (unsigned i = 0; i < core_exprs.size(); ++i) {
if (!mus.contains(core_exprs[i])) {
unknown.push_back(core_exprs[i]);
}
}
TRACE("mus", display_vec(tout << "core exprs:", core_exprs);
display_vec(tout << "core:", unknown);
display_vec(tout << "mus:", mus);
);
}
break;
}
}
// SASSERT(is_core(mus));
return l_true;
}
// use correction sets
lbool get_mus2(expr_ref_vector& mus) {
expr* lit = 0;
lbool is_sat;
ptr_vector<expr> unknown(m_lit2expr.size(), m_lit2expr.c_ptr());
while (!unknown.empty()) {
IF_VERBOSE(12, verbose_stream() << "(mus reducing core: " << unknown.size() << " new core: " << mus.size() << ")\n";);
{
scoped_append _sa1(*this, mus, m_assumptions);
is_sat = get_next_mcs(mus, unknown, lit);
}
if (l_false == is_sat) {
mus.push_back(lit);
}
else {
return is_sat;
}
}
//SASSERT(is_core(mus));
return l_true;
}
// find the next literal to be a member of a core.
lbool get_next_mcs(expr_ref_vector& mus, ptr_vector<expr>& unknown, expr*& core_literal) {
ptr_vector<expr> mss;
expr_ref_vector nmcs(m);
expr_set core, min_core, nmcs_set;
bool min_core_valid = false;
expr* min_lit = 0;
while (!unknown.empty()) {
expr* lit = unknown.back();
unknown.pop_back();
model_ref mdl;
scoped_append assume_mss(*this, mus, mss); // current satisfied literals
scoped_append assume_nmcs(*this, mus, nmcs); // current non-satisfied literals
scoped_append assume_lit(*this, mus, lit); // current unknown literal
switch (m_solver.check_sat(mus)) {
case l_true: {
TRACE("mus", tout << "literal can be satisfied: " << mk_pp(lit, m) << "\n";);
mss.push_back(lit);
m_solver.get_model(mdl);
model_evaluator eval(*mdl.get());
for (unsigned i = 0; i < unknown.size(); ) {
expr_ref tmp(m);
eval(unknown[i], tmp);
if (m.is_true(tmp)) {
mss.push_back(unknown[i]);
unknown[i] = unknown.back();
unknown.pop_back();
}
else {
++i;
}
}
break;
}
case l_false:
TRACE("mus", tout << "literal is in a core: " << mk_pp(lit, m) << "\n";);
nmcs.push_back(mk_not(m, lit));
nmcs_set.insert(nmcs.back());
get_core(core);
if (!core.contains(lit)) {
// The current mus is already a core.
unknown.reset();
return l_true;
}
if (have_intersection(nmcs_set, core)) {
// can't use this core directly. Hypothetically, we
// could try to combine min_core with core and
// see if the combination produces a better minimal core.
SASSERT(min_core_valid);
break;
}
if (!min_core_valid || core.size() < min_core.size()) {
// The current core is smallest so far, so we get fewer unknowns from it.
min_core = core;
min_core_valid = true;
min_lit = lit;
}
break;
case l_undef:
return l_undef;
}
}
SASSERT(min_core_valid);
if (!min_core_valid) {
// all unknown soft constraints were satisfiable
return l_true;
}
expr_set mss_set;
for (unsigned i = 0; i < mss.size(); ++i) {
mss_set.insert(mss[i]);
}
expr_set::iterator it = min_core.begin(), end = min_core.end();
for (; it != end; ++it) {
if (mss_set.contains(*it) && min_lit != *it) {
unknown.push_back(*it);
}
}
core_literal = min_lit;
return l_false;
}
void get_core(expr_set& core) {
core.reset();
ptr_vector<expr> core_exprs;
m_solver.get_unsat_core(core_exprs);
for (unsigned i = 0; i < core_exprs.size(); ++i) {
if (m_expr2lit.contains(core_exprs[i])) {
core.insert(core_exprs[i]);
}
}
}
bool have_intersection(expr_set const& A, expr_set const& B) {
if (A.size() < B.size()) {
expr_set::iterator it = A.begin(), end = A.end();
for (; it != end; ++it) {
if (B.contains(*it)) return true;
}
}
else {
expr_set::iterator it = B.begin(), end = B.end();
for (; it != end; ++it) {
if (A.contains(*it)) return true;
}
}
return false;
}
bool is_core(expr_ref_vector const& mus) {
return l_false == m_solver.check_sat(mus);
}
class scoped_append {
expr_ref_vector& m_fmls;
unsigned m_size;
public:
scoped_append(imp& imp, expr_ref_vector& fmls1, expr_set const& fmls2):
m_fmls(fmls1),
m_size(fmls1.size()) {
expr_set::iterator it = fmls2.begin(), end = fmls2.end();
for (; it != end; ++it) {
fmls1.push_back(*it);
}
}
scoped_append(imp& imp, expr_ref_vector& fmls1, expr_ref_vector const& fmls2):
m_fmls(fmls1),
m_size(fmls1.size()) {
fmls1.append(fmls2);
}
scoped_append(imp& imp, expr_ref_vector& fmls1, ptr_vector<expr> const& fmls2):
m_fmls(fmls1),
m_size(fmls1.size()) {
fmls1.append(fmls2.size(), fmls2.c_ptr());
}
scoped_append(imp& imp, expr_ref_vector& fmls1, expr* fml):
m_fmls(fmls1),
m_size(fmls1.size()) {
fmls1.push_back(fml);
}
~scoped_append() {
m_fmls.shrink(m_size);
}
};
template<class T>
void display_vec(std::ostream& out, T const& v) const {
for (unsigned i = 0; i < v.size(); ++i) {
out << v[i] << " ";
}
out << "\n";
}
void display_vec(std::ostream& out, expr_ref_vector const& v) const {
for (unsigned i = 0; i < v.size(); ++i)
out << mk_pp(v[i], m) << " ";
out << "\n";
}
void display_vec(std::ostream& out, ptr_vector<expr> const& v) const {
for (unsigned i = 0; i < v.size(); ++i)
out << mk_pp(v[i], m) << " ";
out << "\n";
}
void set_soft(unsigned sz, expr* const* soft, rational const* weights) {
m_model.reset();
m_weight.reset();
m_soft.append(sz, soft);
m_weights.append(sz, weights);
for (unsigned i = 0; i < sz; ++i) {
m_weight += weights[i];
}
}
void update_model() {
if (m_soft.empty()) return;
model_ref mdl;
expr_ref tmp(m);
m_solver.get_model(mdl);
rational w;
for (unsigned i = 0; i < m_soft.size(); ++i) {
mdl->eval(m_soft[i].get(), tmp);
if (!m.is_true(tmp)) {
w += m_weights[i];
}
}
if (w < m_weight || !m_model.get()) {
m_model = mdl;
m_weight = w;
}
}
rational get_best_model(model_ref& mdl) {
mdl = m_model;
return m_weight;
}
};
mus::mus(solver& s) {
m_imp = alloc(imp, s);
}
mus::~mus() {
dealloc(m_imp);
}
unsigned mus::add_soft(expr* lit) {
return m_imp->add_soft(lit);
}
void mus::add_assumption(expr* lit) {
return m_imp->add_assumption(lit);
}
lbool mus::get_mus(ptr_vector<expr>& mus) {
return m_imp->get_mus(mus);
}
lbool mus::get_mus(expr_ref_vector& mus) {
return m_imp->get_mus(mus);
}
void mus::reset() {
m_imp->reset();
}
void mus::set_soft(unsigned sz, expr* const* soft, rational const* weights) {
m_imp->set_soft(sz, soft, weights);
}
rational mus::get_best_model(model_ref& mdl) {
return m_imp->get_best_model(mdl);
}

69
src/solver/mus.h Normal file
View file

@ -0,0 +1,69 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
mus.h
Abstract:
Basic MUS extraction
Author:
Nikolaj Bjorner (nbjorner) 2014-20-7
Notes:
--*/
#ifndef MUS_H_
#define MUS_H_
class mus {
struct imp;
imp * m_imp;
public:
mus(solver& s);
~mus();
/**
Add soft constraint.
Assume that the solver context enforces that
cls is equivalent to a disjunction of args.
Assume also that cls is a literal.
*/
unsigned add_soft(expr* cls);
void add_soft(unsigned sz, expr* const* clss) {
for (unsigned i = 0; i < sz; ++i) add_soft(clss[i]);
}
/**
Additional assumption for solver to be used along with solver context,
but not used in core computation. This facility is useful when querying
for a core over only a subset of soft constraints. It has the same
logical functionality as asserting 'lit' to the solver and pushing a scope
(and popping the scope before the solver is used for other constraints).
*/
void add_assumption(expr* lit);
lbool get_mus(ptr_vector<expr>& mus);
lbool get_mus(expr_ref_vector& mus);
void reset();
/**
Instrument MUS extraction to also provide the minimal
penalty model, if any is found.
The minimal penalty model has the least weight for the
supplied soft constraints.
*/
void set_soft(unsigned sz, expr* const* soft, rational const* weights);
rational get_best_model(model_ref& mdl);
};
#endif

157
src/solver/smt_logics.cpp Normal file
View file

@ -0,0 +1,157 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
smt_logics.cpp
Abstract:
Module for recognizing SMT logics.
Author:
Nikolaj Bjorner (nbjorner) 2016-11-4
Revision History:
--*/
#include "symbol.h"
#include "smt_logics.h"
bool smt_logics::supported_logic(symbol const & s) {
return logic_has_uf(s) || logic_is_all(s) || logic_has_fd(s) ||
logic_has_arith(s) || logic_has_bv(s) ||
logic_has_array(s) || logic_has_seq(s) || logic_has_str(s) ||
logic_has_horn(s) || logic_has_fpa(s);
}
bool smt_logics::logic_has_reals_only(symbol const& s) {
return
s == "QF_RDL" ||
s == "QF_LRA" ||
s == "UFLRA" ||
s == "LRA" ||
s == "RDL" ||
s == "QF_NRA" ||
s == "QF_UFNRA" ||
s == "QF_UFLRA";
}
bool smt_logics::logic_has_arith(symbol const & s) {
return
s == "QF_LRA" ||
s == "QF_LIA" ||
s == "QF_RDL" ||
s == "QF_IDL" ||
s == "QF_AUFLIA" ||
s == "QF_ALIA" ||
s == "QF_AUFLIRA" ||
s == "QF_AUFNIA" ||
s == "QF_AUFNIRA" ||
s == "QF_ANIA" ||
s == "QF_LIRA" ||
s == "QF_UFLIA" ||
s == "QF_UFLRA" ||
s == "QF_UFIDL" ||
s == "QF_UFRDL" ||
s == "QF_NIA" ||
s == "QF_NRA" ||
s == "QF_NIRA" ||
s == "QF_UFNRA" ||
s == "QF_UFNIA" ||
s == "QF_UFNIRA" ||
s == "QF_BVRE" ||
s == "ALIA" ||
s == "AUFLIA" ||
s == "AUFLIRA" ||
s == "AUFNIA" ||
s == "AUFNIRA" ||
s == "UFLIA" ||
s == "UFLRA" ||
s == "UFNRA" ||
s == "UFNIRA" ||
s == "NIA" ||
s == "NRA" ||
s == "UFNIA" ||
s == "LIA" ||
s == "LRA" ||
s == "UFIDL" ||
s == "QF_FP" ||
s == "QF_FPBV" ||
s == "QF_BVFP" ||
s == "QF_S" ||
s == "ALL" ||
s == "QF_FD" ||
s == "HORN";
}
bool smt_logics::logic_has_bv(symbol const & s) {
return
s == "UFBV" ||
s == "AUFBV" ||
s == "ABV" ||
s == "BV" ||
s == "QF_BV" ||
s == "QF_UFBV" ||
s == "QF_ABV" ||
s == "QF_AUFBV" ||
s == "QF_BVRE" ||
s == "QF_FPBV" ||
s == "QF_BVFP" ||
s == "ALL" ||
s == "QF_FD" ||
s == "HORN";
}
bool smt_logics::logic_has_array(symbol const & s) {
return
s == "QF_AX" ||
s == "QF_AUFLIA" ||
s == "QF_ANIA" ||
s == "QF_ALIA" ||
s == "QF_AUFLIRA" ||
s == "QF_AUFNIA" ||
s == "QF_AUFNIRA" ||
s == "ALIA" ||
s == "AUFLIA" ||
s == "AUFLIRA" ||
s == "AUFNIA" ||
s == "AUFNIRA" ||
s == "AUFBV" ||
s == "ABV" ||
s == "ALL" ||
s == "QF_ABV" ||
s == "QF_AUFBV" ||
s == "HORN";
}
bool smt_logics::logic_has_seq(symbol const & s) {
return s == "QF_BVRE" || s == "QF_S" || s == "ALL";
}
bool smt_logics::logic_has_str(symbol const & s) {
return s == "QF_S" || s == "ALL";
}
bool smt_logics::logic_has_fpa(symbol const & s) {
return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "ALL";
}
bool smt_logics::logic_has_uf(symbol const & s) {
return s == "QF_UF" || s == "UF";
}
bool smt_logics::logic_has_horn(symbol const& s) {
return s == "HORN";
}
bool smt_logics::logic_has_pb(symbol const& s) {
return s == "QF_FD" || s == "ALL";
}
bool smt_logics::logic_has_datatype(symbol const& s) {
return s == "QF_FD";
}

42
src/solver/smt_logics.h Normal file
View file

@ -0,0 +1,42 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
smt_logics.h
Abstract:
Module for recognizing SMT logics.
Author:
Nikolaj Bjorner (nbjorner) 2016-11-4
Revision History:
--*/
#ifndef SMT_LOGICS_H_
#define SMT_LOGICS_H_
class smt_logics {
public:
smt_logics() {}
static bool supported_logic(symbol const & s);
static bool logic_has_reals_only(symbol const& l);
static bool logic_is_all(symbol const& s) { return s == "ALL"; }
static bool logic_has_uf(symbol const& s);
static bool logic_has_arith(symbol const & s);
static bool logic_has_bv(symbol const & s);
static bool logic_has_array(symbol const & s);
static bool logic_has_seq(symbol const & s);
static bool logic_has_str(symbol const & s);
static bool logic_has_fpa(symbol const & s);
static bool logic_has_horn(symbol const& s);
static bool logic_has_pb(symbol const& s);
static bool logic_has_fd(symbol const& s) { return s == "QF_FD"; }
static bool logic_has_datatype(symbol const& s);
};
#endif /* SMT_LOGICS_H_ */

134
src/solver/solver.cpp
View file

@ -17,6 +17,12 @@ Notes:
--*/
#include"solver.h"
#include"model_evaluator.h"
#include"ast_util.h"
#include"ast_pp.h"
#include"ast_pp_util.h"
#include "common_msgs.h"
unsigned solver::get_num_assertions() const {
NOT_IMPLEMENTED_YET();
@ -28,7 +34,131 @@ expr * solver::get_assertion(unsigned idx) const {
return 0;
}
void solver::display(std::ostream & out) const {
out << "(solver)";
std::ostream& solver::display(std::ostream & out) const {
expr_ref_vector fmls(get_manager());
get_assertions(fmls);
ast_pp_util visitor(get_manager());
visitor.collect(fmls);
visitor.display_decls(out);
visitor.display_asserts(out, fmls, true);
return out;
}
void solver::get_assertions(expr_ref_vector& fmls) const {
unsigned sz = get_num_assertions();
for (unsigned i = 0; i < sz; ++i) {
fmls.push_back(get_assertion(i));
}
}
struct scoped_assumption_push {
expr_ref_vector& m_vec;
scoped_assumption_push(expr_ref_vector& v, expr* e): m_vec(v) { v.push_back(e); }
~scoped_assumption_push() { m_vec.pop_back(); }
};
lbool solver::get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
try {
return get_consequences_core(asms, vars, consequences);
}
catch (z3_exception& ex) {
if (asms.get_manager().canceled()) {
set_reason_unknown(Z3_CANCELED_MSG);
return l_undef;
}
else {
set_reason_unknown(ex.msg());
}
throw;
}
}
lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
ast_manager& m = asms.get_manager();
lbool is_sat = check_sat(asms);
if (is_sat != l_true) {
return is_sat;
}
model_ref model;
get_model(model);
expr_ref tmp(m), nlit(m), lit(m), val(m);
expr_ref_vector asms1(asms);
model_evaluator eval(*model.get());
unsigned k = 0;
for (unsigned i = 0; i < vars.size(); ++i) {
expr_ref_vector core(m);
tmp = vars[i];
val = eval(tmp);
if (!m.is_value(val)) {
// vars[i] is unfixed
continue;
}
if (m.is_bool(tmp) && is_uninterp_const(tmp)) {
if (m.is_true(val)) {
nlit = m.mk_not(tmp);
lit = tmp;
}
else if (m.is_false(val)) {
nlit = tmp;
lit = m.mk_not(tmp);
}
else {
// vars[i] is unfixed
continue;
}
scoped_assumption_push _scoped_push(asms1, nlit);
is_sat = check_sat(asms1);
switch (is_sat) {
case l_undef:
return is_sat;
case l_true:
// vars[i] is unfixed
break;
case l_false:
get_unsat_core(core);
k = 0;
for (unsigned j = 0; j < core.size(); ++j) {
if (core[j].get() != nlit) {
core[k] = core[j].get();
++k;
}
}
core.resize(k);
consequences.push_back(m.mk_implies(mk_and(core), lit));
break;
}
}
else {
lit = m.mk_eq(tmp, val);
nlit = m.mk_not(lit);
scoped_push _scoped_push(*this);
assert_expr(nlit);
is_sat = check_sat(asms);
switch (is_sat) {
case l_undef:
return is_sat;
case l_true:
// vars[i] is unfixed
break;
case l_false:
get_unsat_core(core);
consequences.push_back(m.mk_implies(mk_and(core), lit));
break;
}
}
}
return l_true;
}
lbool solver::find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
return l_true;
}
lbool solver::preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) {
return check_sat(0, 0);
}
bool solver::is_literal(ast_manager& m, expr* e) {
return is_uninterp_const(e) || (m.is_not(e, e) && is_uninterp_const(e));
}

45
src/solver/solver.h
View file

@ -54,7 +54,7 @@ public:
/**
\brief Update the solver internal settings.
*/
virtual void updt_params(params_ref const & p) {}
virtual void updt_params(params_ref const & p) { }
/**
\brief Store in \c r a description of the configuration
@ -79,6 +79,10 @@ public:
for (unsigned i = 0; i < ts.size(); ++i) assert_expr(ts[i]);
}
void assert_expr(ptr_vector<expr> const& ts) {
for (unsigned i = 0; i < ts.size(); ++i) assert_expr(ts[i]);
}
/**
\brief Add a new formula \c t to the assertion stack, and "tag" it with \c a.
The propositional variable \c a is used to track the use of \c t in a proof
@ -108,6 +112,10 @@ public:
*/
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) = 0;
lbool check_sat(expr_ref_vector const& asms) { return check_sat(asms.size(), asms.c_ptr()); }
lbool check_sat(app_ref_vector const& asms) { return check_sat(asms.size(), (expr* const*)asms.c_ptr()); }
/**
\brief Set a progress callback procedure that is invoked by this solver during check_sat.
@ -126,6 +134,11 @@ public:
*/
virtual expr * get_assertion(unsigned idx) const;
/**
\brief Retrieves assertions as a vector.
*/
void get_assertions(expr_ref_vector& fmls) const;
/**
\brief The number of tracked assumptions (see assert_expr(t, a)).
*/
@ -136,12 +149,33 @@ public:
*/
virtual expr * get_assumption(unsigned idx) const = 0;
/**
\brief under assumptions, asms, retrieve set of consequences that
fix values for expressions that can be built from vars.
The consequences are clauses whose first literal constrain one of the
functions from vars and the other literals are negations of literals from asms.
*/
virtual lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences);
/**
\brief Find maximal subsets A' of A such that |A'| <= 1. These subsets look somewhat similar to cores: cores have the property
that |~A'| >= 1, where ~A' is the set of negated formulas from A'
*/
virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes);
/**
\brief Preferential SAT. Prefer assumptions to be true, produce cores that witness cases when not all assumptions can be met.
by default, preferred sat ignores the assumptions.
*/
virtual lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores);
/**
\brief Display the content of this solver.
*/
virtual void display(std::ostream & out) const;
virtual std::ostream& display(std::ostream & out) const;
class scoped_push {
solver& s;
@ -151,6 +185,13 @@ public:
~scoped_push() { if (!m_nopop) s.pop(1); }
void disable_pop() { m_nopop = true; }
};
protected:
virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences);
bool is_literal(ast_manager& m, expr* e);
};
#endif

177
src/solver/solver2tactic.cpp Normal file
View file

@ -0,0 +1,177 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
solver2tactic.cpp
Abstract:
Convert solver to a tactic.
Author:
Nikolaj Bjorner (nbjorner) 2016-10-17
Notes:
--*/
#include "solver.h"
#include "tactic.h"
#include"filter_model_converter.h"
#include "solver2tactic.h"
#include "ast_util.h"
typedef obj_map<expr, expr *> expr2expr_map;
void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector<expr>& assumptions, expr2expr_map& bool2dep, ref<filter_model_converter>& fmc) {
expr2expr_map dep2bool;
ptr_vector<expr> deps;
ast_manager& m = g->m();
expr_ref_vector clause(m);
unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++) {
expr * f = g->form(i);
expr_dependency * d = g->dep(i);
if (d == 0 || !g->unsat_core_enabled()) {
clauses.push_back(f);
}
else {
// create clause (not d1 \/ ... \/ not dn \/ f) when the d's are the assumptions/dependencies of f.
clause.reset();
clause.push_back(f);
deps.reset();
m.linearize(d, deps);
SASSERT(!deps.empty()); // d != 0, then deps must not be empty
ptr_vector<expr>::iterator it = deps.begin();
ptr_vector<expr>::iterator end = deps.end();
for (; it != end; ++it) {
expr * d = *it;
if (is_uninterp_const(d) && m.is_bool(d)) {
// no need to create a fresh boolean variable for d
if (!bool2dep.contains(d)) {
assumptions.push_back(d);
bool2dep.insert(d, d);
}
clause.push_back(m.mk_not(d));
}
else {
// must normalize assumption
expr * b = 0;
if (!dep2bool.find(d, b)) {
b = m.mk_fresh_const(0, m.mk_bool_sort());
dep2bool.insert(d, b);
bool2dep.insert(b, d);
assumptions.push_back(b);
if (!fmc) {
fmc = alloc(filter_model_converter, m);
}
fmc->insert(to_app(b)->get_decl());
}
clause.push_back(m.mk_not(b));
}
}
SASSERT(clause.size() > 1);
expr_ref cls(m);
cls = mk_or(m, clause.size(), clause.c_ptr());
clauses.push_back(cls);
}
}
}
class solver2tactic : public tactic {
ast_manager& m;
ref<solver> m_solver;
params_ref m_params;
statistics m_st;
public:
solver2tactic(solver* s):
m(s->get_manager()),
m_solver(s)
{}
virtual void updt_params(params_ref const & p) {
m_params.append(p);
m_solver->updt_params(p);
}
virtual void collect_param_descrs(param_descrs & r) {
m_solver->collect_param_descrs(r);
}
virtual void operator()(/* in */ goal_ref const & in,
/* out */ goal_ref_buffer & result,
/* out */ model_converter_ref & mc,
/* out */ proof_converter_ref & pc,
/* out */ expr_dependency_ref & core) {
pc = 0; mc = 0; core = 0;
expr_ref_vector clauses(m);
expr2expr_map bool2dep;
ptr_vector<expr> assumptions;
ref<filter_model_converter> fmc;
extract_clauses_and_dependencies(in, clauses, assumptions, bool2dep, fmc);
ref<solver> local_solver = m_solver->translate(m, m_params);
local_solver->assert_expr(clauses);
lbool r = local_solver->check_sat(assumptions.size(), assumptions.c_ptr());
switch (r) {
case l_true:
if (in->models_enabled()) {
model_ref mdl;
local_solver->get_model(mdl);
mc = model2model_converter(mdl.get());
mc = concat(fmc.get(), mc.get());
}
in->reset();
result.push_back(in.get());
break;
case l_false: {
in->reset();
proof* pr = 0;
expr_dependency* lcore = 0;
if (in->proofs_enabled()) {
pr = local_solver->get_proof();
pc = proof2proof_converter(m, pr);
}
if (in->unsat_core_enabled()) {
ptr_vector<expr> core;
local_solver->get_unsat_core(core);
for (unsigned i = 0; i < core.size(); ++i) {
lcore = m.mk_join(lcore, m.mk_leaf(bool2dep.find(core[i])));
}
}
in->assert_expr(m.mk_false(), pr, lcore);
result.push_back(in.get());
core = lcore;
break;
}
case l_undef:
if (m.canceled()) {
throw tactic_exception(Z3_CANCELED_MSG);
}
throw tactic_exception(local_solver->reason_unknown().c_str());
}
local_solver->collect_statistics(m_st);
}
virtual void collect_statistics(statistics & st) const {
st.copy(m_st);
}
virtual void reset_statistics() { m_st.reset(); }
virtual void cleanup() { }
virtual void reset() { cleanup(); }
virtual void set_logic(symbol const & l) {}
virtual void set_progress_callback(progress_callback * callback) {
m_solver->set_progress_callback(callback);
}
virtual tactic * translate(ast_manager & m) {
return alloc(solver2tactic, m_solver->translate(m, m_params));
}
};
tactic* mk_solver2tactic(solver* s) { return alloc(solver2tactic, s); }

30
src/solver/solver2tactic.h Normal file
View file

@ -0,0 +1,30 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
solver2tactic.h
Abstract:
Convert solver to a tactic.
Author:
Nikolaj Bjorner (nbjorner) 2016-10-17
Notes:
--*/
#ifndef SOLVER2TACTIC_H_
#define SOLVER2TACTIC_H_
#include "tactic.h"
#include "filter_model_converter.h"
class solver;
tactic * mk_solver2tactic(solver* s);
void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector<expr>& assumptions, obj_map<expr, expr*>& bool2dep, ref<filter_model_converter>& fmc);
#endif

12
src/solver/solver_na2as.cpp
View file

@ -22,6 +22,7 @@ Notes:
#include"solver_na2as.h"
#include"ast_smt2_pp.h"
solver_na2as::solver_na2as(ast_manager & m):
m(m),
m_assumptions(m) {
@ -62,9 +63,20 @@ struct append_assumptions {
lbool solver_na2as::check_sat(unsigned num_assumptions, expr * const * assumptions) {
append_assumptions app(m_assumptions, num_assumptions, assumptions);
TRACE("solver_na2as", display(tout););
return check_sat_core(m_assumptions.size(), m_assumptions.c_ptr());
}
lbool solver_na2as::get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
append_assumptions app(m_assumptions, asms.size(), asms.c_ptr());
return get_consequences_core(m_assumptions, vars, consequences);
}
lbool solver_na2as::find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
return l_true;
}
void solver_na2as::push() {
m_scopes.push_back(m_assumptions.size());
push_core();

3
src/solver/solver_na2as.h
View file

@ -25,6 +25,7 @@ Notes:
#include"solver.h"
class solver_na2as : public solver {
protected:
ast_manager & m;
expr_ref_vector m_assumptions;
unsigned_vector m_scopes;
@ -44,6 +45,8 @@ public:
virtual unsigned get_num_assumptions() const { return m_assumptions.size(); }
virtual expr * get_assumption(unsigned idx) const { return m_assumptions[idx]; }
virtual lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences);
virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes);
protected:
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) = 0;
virtual void push_core() = 0;

36
src/solver/tactic2solver.cpp
View file

@ -21,8 +21,8 @@ Notes:
--*/
#include"solver_na2as.h"
#include"tactic.h"
#include"ast_pp_util.h"
#include"ast_translation.h"
#include"mus.h"
/**
\brief Simulates the incremental solver interface using a tactic.
@ -42,6 +42,7 @@ class tactic2solver : public solver_na2as {
bool m_produce_proofs;
bool m_produce_unsat_cores;
statistics m_stats;
public:
tactic2solver(ast_manager & m, tactic * t, params_ref const & p, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic);
virtual ~tactic2solver();
@ -73,11 +74,10 @@ public:
virtual unsigned get_num_assertions() const;
virtual expr * get_assertion(unsigned idx) const;
virtual void display(std::ostream & out) const;
virtual ast_manager& get_manager();
virtual ast_manager& get_manager() const;
};
ast_manager& tactic2solver::get_manager() { return m_assertions.get_manager(); }
ast_manager& tactic2solver::get_manager() const { return m_assertions.get_manager(); }
tactic2solver::tactic2solver(ast_manager & m, tactic * t, params_ref const & p, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic):
solver_na2as(m),
@ -96,7 +96,7 @@ tactic2solver::~tactic2solver() {
}
void tactic2solver::updt_params(params_ref const & p) {
m_params = p;
m_params.append(p);
}
void tactic2solver::collect_param_descrs(param_descrs & r) {
@ -137,15 +137,18 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
g->assert_expr(m_assertions.get(i));
}
for (unsigned i = 0; i < num_assumptions; i++) {
g->assert_expr(assumptions[i], m.mk_asserted(assumptions[i]), m.mk_leaf(assumptions[i]));
proof_ref pr(m.mk_asserted(assumptions[i]), m);
expr_dependency_ref ans(m.mk_leaf(assumptions[i]), m);
g->assert_expr(assumptions[i], pr, ans);
}
model_ref md;
proof_ref pr(m);
expr_dependency_ref core(m);
std::string reason_unknown = "unknown";
labels_vec labels;
try {
switch (::check_sat(*m_tactic, g, md, pr, core, reason_unknown)) {
switch (::check_sat(*m_tactic, g, md, labels, pr, core, reason_unknown)) {
case l_true:
m_result->set_status(l_true);
break;
@ -160,6 +163,7 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
}
}
catch (z3_error & ex) {
TRACE("tactic2solver", tout << "exception: " << ex.msg() << "\n";);
throw ex;
}
catch (z3_exception & ex) {
@ -203,8 +207,9 @@ void tactic2solver::collect_statistics(statistics & st) const {
}
void tactic2solver::get_unsat_core(ptr_vector<expr> & r) {
if (m_result.get())
if (m_result.get()) {
m_result->get_unsat_core(r);
}
}
void tactic2solver::get_model(model_ref & m) {
@ -240,21 +245,6 @@ expr * tactic2solver::get_assertion(unsigned idx) const {
return m_assertions.get(idx);
}
void tactic2solver::display(std::ostream & out) const {
ast_pp_util visitor(m_assertions.m());
visitor.collect(m_assertions);
visitor.display_decls(out);
visitor.display_asserts(out, m_assertions, true);
#if 0
ast_manager & m = m_assertions.m();
unsigned num = m_assertions.size();
out << "(solver";
for (unsigned i = 0; i < num; i++) {
out << "\n " << mk_ismt2_pp(m_assertions.get(i), m, 2);
}
out << ")";
#endif
}
solver * mk_tactic2solver(ast_manager & m,
tactic * t,