mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-10-28 07:17:49 -07:00
parent c68c56b0e7 f1412d3f32
commit 4d078dc0a9
40 changed files with 753 additions and 326 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
contrib/cmake/src/solver/CMakeLists.txt
View file

@ -5,6 +5,7 @@ z3_add_component(solver
mus.cpp
solver.cpp
solver_na2as.cpp
solver2tactic.cpp
tactic2solver.cpp
COMPONENT_DEPENDENCIES
model

10
scripts/mk_util.py
View file

@ -1505,6 +1505,9 @@ class PythonInstallComponent(Component):
os.path.join(self.pythonPkgDir, 'z3', '__pycache__', '*.pyc'),
in_prefix=self.in_prefix_install
)
MakeRuleCmd.remove_installed_files(out,
os.path.join(self.pythonPkgDir, 'z3', 'lib',
self.libz3Component.dll_file()))
def mk_makefile(self, out):
return
@ -3073,6 +3076,11 @@ def mk_vs_proj_property_groups(f, name, target_ext, type):
f.write(' <CharacterSet>Unicode</CharacterSet>\n')
f.write(' <UseOfMfc>false</UseOfMfc>\n')
f.write(' </PropertyGroup>\n')
f.write(' <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'" Label="Configuration">\n')
f.write(' <ConfigurationType>%s</ConfigurationType>\n' % type)
f.write(' <CharacterSet>Unicode</CharacterSet>\n')
f.write(' <UseOfMfc>false</UseOfMfc>\n')
f.write(' </PropertyGroup>\n')
f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.props" />\n')
f.write(' <ImportGroup Label="ExtensionSettings" />\n')
f.write(' <ImportGroup Label="PropertySheets">\n')
@ -3275,7 +3283,7 @@ class MakeRuleCmd(object):
#print("WARNING: Generating makefile rule that {}s {} '{}' which is outside the installation prefix '{}'.".format(
# action_string, 'to' if is_install else 'from', path, PREFIX))
else:
assert not os.path.isabs(path)
# assert not os.path.isabs(path)
install_root = cls.install_root()
return install_root

18
src/api/api_pb.cpp
View file

@ -57,5 +57,23 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args,
Z3_ast const args[], int _coeffs[],
int k) {
Z3_TRY;
LOG_Z3_mk_pble(c, num_args, args, _coeffs, k);
RESET_ERROR_CODE();
pb_util util(mk_c(c)->m());
vector<rational> coeffs;
for (unsigned i = 0; i < num_args; ++i) {
coeffs.push_back(rational(_coeffs[i]));
}
ast* a = util.mk_eq(num_args, coeffs.c_ptr(), to_exprs(args), rational(k));
mk_c(c)->save_ast_trail(a);
check_sorts(c, a);
RETURN_Z3(of_ast(a));
Z3_CATCH_RETURN(0);
}
};

15
src/api/dotnet/Context.cs
View file

@ -2640,6 +2640,21 @@ namespace Microsoft.Z3
AST.ArrayToNative(args),
coeffs, k));
}
/// <summary>
/// Create a pseudo-Boolean equal constraint.
/// </summary>
public BoolExpr MkPBEq(int[] coeffs, BoolExpr[] args, int k)
{
Contract.Requires(args != null);
Contract.Requires(coeffs != null);
Contract.Requires(args.Length == coeffs.Length);
Contract.Requires(Contract.Result<BoolExpr[]>() != null);
CheckContextMatch<BoolExpr>(args);
return new BoolExpr(this, Native.Z3_mk_pbeq(nCtx, (uint) args.Length,
AST.ArrayToNative(args),
coeffs, k));
}
#endregion
#region Numerals

9
src/api/dotnet/Optimize.cs
View file

@ -258,10 +258,13 @@ namespace Microsoft.Z3
/// <summary>
/// Return a string the describes why the last to check returned unknown
/// </summary>
public String getReasonUnknown()
public String ReasonUnknown
{
Contract.Ensures(Contract.Result<string>() != null);
return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
get
{
Contract.Ensures(Contract.Result<string>() != null);
return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
}
}

3
src/api/dotnet/Z3Exception.cs
View file

@ -14,7 +14,7 @@ Author:
Christoph Wintersteiger (cwinter) 2012-03-15
Notes:
--*/
using System;
@ -24,6 +24,7 @@ namespace Microsoft.Z3
/// <summary>
/// The exception base class for error reporting from Z3
/// </summary>
[Serializable]
public class Z3Exception : Exception
{
/// <summary>

22
src/api/python/z3/z3.py
View file

@ -1817,7 +1817,7 @@ class QuantifierRef(BoolRef):
"""
if __debug__:
_z3_assert(idx < self.num_vars(), "Invalid variable idx")
return SortRef(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)
return _to_sort_ref(Z3_get_quantifier_bound_sort(self.ctx_ref(), self.ast, idx), self.ctx)
def children(self):
"""Return a list containing a single element self.body()
@ -7654,6 +7654,26 @@ def PbLe(args, k):
_coeffs[i] = coeffs[i]
return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)
def PbEq(args, k):
"""Create a Pseudo-Boolean inequality k constraint.
>>> a, b, c = Bools('a b c')
>>> f = PbEq(((a,1),(b,3),(c,2)), 3)
"""
args = _get_args(args)
args, coeffs = zip(*args)
if __debug__:
_z3_assert(len(args) > 0, "Non empty list of arguments expected")
ctx = _ctx_from_ast_arg_list(args)
if __debug__:
_z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
args = _coerce_expr_list(args, ctx)
_args, sz = _to_ast_array(args)
_coeffs = (ctypes.c_int * len(coeffs))()
for i in range(len(coeffs)):
_coeffs[i] = coeffs[i]
return BoolRef(Z3_mk_pbeq(ctx.ref(), sz, _args, _coeffs, k), ctx)
def solve(*args, **keywords):
"""Solve the constraints `*args`.

16
src/api/z3_api.h
View file

@ -861,6 +861,9 @@ typedef enum
- Z3_OP_PB_GE: Generalized Pseudo-Boolean cardinality constraint.
Example 2*x + 3*y + 2*z >= 4
- Z3_OP_PB_EQ: Generalized Pseudo-Boolean equality constraint.
Example 2*x + 1*y + 2*z + 1*u = 4
- Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN: Floating-point rounding mode RNE
- Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY: Floating-point rounding mode RNA
@ -1166,6 +1169,7 @@ typedef enum {
Z3_OP_PB_AT_MOST=0x900,
Z3_OP_PB_LE,
Z3_OP_PB_GE,
Z3_OP_PB_EQ,
// Floating-Point Arithmetic
Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN,
@ -3913,6 +3917,18 @@ extern "C" {
Z3_ast const args[], int coeffs[],
int k);
/**
\brief Pseudo-Boolean relations.
Encode k1*p1 + k2*p2 + ... + kn*pn = k
def_API('Z3_mk_pbeq', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in_array(1,INT), _in(INT)))
*/
Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args,
Z3_ast const args[], int coeffs[],
int k);
/**
\brief Convert a \c Z3_func_decl into \c Z3_ast. This is just type casting.

4
src/ast/arith_decl_plugin.h
View file

@ -264,6 +264,10 @@ public:
bool is_ge(expr const * n) const { return is_app_of(n, m_afid, OP_GE); }
bool is_lt(expr const * n) const { return is_app_of(n, m_afid, OP_LT); }
bool is_gt(expr const * n) const { return is_app_of(n, m_afid, OP_GT); }
bool is_le(func_decl const * n) const { return is_decl_of(n, m_afid, OP_LE); }
bool is_ge(func_decl const * n) const { return is_decl_of(n, m_afid, OP_GE); }
bool is_lt(func_decl const * n) const { return is_decl_of(n, m_afid, OP_LT); }
bool is_gt(func_decl const * n) const { return is_decl_of(n, m_afid, OP_GT); }
bool is_add(expr const * n) const { return is_app_of(n, m_afid, OP_ADD); }
bool is_sub(expr const * n) const { return is_app_of(n, m_afid, OP_SUB); }
bool is_uminus(expr const * n) const { return is_app_of(n, m_afid, OP_UMINUS); }

15
src/ast/fpa/bv2fpa_converter.cpp
View file

@ -322,10 +322,17 @@ void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model
v2 = mc->get_const_interp(a2->get_decl());
#else
expr * bv = mc->get_const_interp(to_app(to_app(a0)->get_arg(0))->get_decl());
unsigned bv_sz = m_bv_util.get_bv_size(bv);
v0 = m_bv_util.mk_extract(bv_sz-1, bv_sz-1, bv);
v1 = m_bv_util.mk_extract(bv_sz-2, sbits-1, bv);
v2 = m_bv_util.mk_extract(sbits-2, 0, bv);
if (bv == 0) {
v0 = m_bv_util.mk_numeral(0, 1);
v1 = m_bv_util.mk_numeral(0, ebits);
v2 = m_bv_util.mk_numeral(0, sbits-1);
}
else {
unsigned bv_sz = m_bv_util.get_bv_size(bv);
v0 = m_bv_util.mk_extract(bv_sz-1, bv_sz-1, bv);
v1 = m_bv_util.mk_extract(bv_sz-2, sbits-1, bv);
v2 = m_bv_util.mk_extract(sbits-2, 0, bv);
}
#endif
if (!v0) v0 = m_bv_util.mk_numeral(0, 1);

9
src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
View file

@ -165,6 +165,10 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
m_keyval_lim.push_back(m_keys.size());
}
unsigned get_num_scopes() const {
return m_keyval_lim.size();
}
void pop(unsigned num_scopes) {
if (num_scopes > 0) {
SASSERT(num_scopes <= m_keyval_lim.size());
@ -637,6 +641,7 @@ struct bit_blaster_rewriter::imp : public rewriter_tpl<blaster_rewriter_cfg> {
}
void push() { m_cfg.push(); }
void pop(unsigned s) { m_cfg.pop(s); }
unsigned get_num_scopes() const { return m_cfg.get_num_scopes(); }
};
bit_blaster_rewriter::bit_blaster_rewriter(ast_manager & m, params_ref const & p):
@ -680,3 +685,7 @@ void bit_blaster_rewriter::operator()(expr * e, expr_ref & result, proof_ref & r
m_imp->operator()(e, result, result_proof);
}
unsigned bit_blaster_rewriter::get_num_scopes() const {
return m_imp->get_num_scopes();
}

1
src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h
View file

@ -37,6 +37,7 @@ public:
void operator()(expr * e, expr_ref & result, proof_ref & result_proof);
void push();
void pop(unsigned num_scopes);
unsigned get_num_scopes() const;
};
#endif

4
src/ast/rewriter/enum2bv_rewriter.cpp
View file

@ -126,7 +126,7 @@ struct enum2bv_rewriter::imp {
unsigned nc = m_dt.get_datatype_num_constructors(s);
result = m.mk_fresh_const(f->get_name().str().c_str(), m_bv.mk_sort(bv_size));
f_fresh = to_app(result)->get_decl();
if (!is_power_of_two(nc)) {
if (!is_power_of_two(nc) || nc == 1) {
m_imp.m_bounds.push_back(m_bv.mk_ule(result, m_bv.mk_numeral(nc-1, bv_size)));
}
expr_ref f_def(m);
@ -168,7 +168,7 @@ struct enum2bv_rewriter::imp {
unsigned bv_size = get_bv_size(s);
m_sorts.push_back(m_bv.mk_sort(bv_size));
unsigned nc = m_dt.get_datatype_num_constructors(s);
if (!is_power_of_two(nc)) {
if (!is_power_of_two(nc) || nc == 1) {
bounds.push_back(m_bv.mk_ule(m.mk_var(q->get_num_decls()-i-1, m_sorts[i]), m_bv.mk_numeral(nc-1, bv_size)));
}
found = true;

216
src/ast/rewriter/pb2bv_rewriter.cpp
View file

@ -29,39 +29,6 @@ Notes:
struct pb2bv_rewriter::imp {
struct argc_t {
expr* m_arg;
rational m_coeff;
argc_t():m_arg(0), m_coeff(0) {}
argc_t(expr* arg, rational const& r): m_arg(arg), m_coeff(r) {}
};
struct argc_gt {
bool operator()(argc_t const& a, argc_t const& b) const {
return a.m_coeff > b.m_coeff;
}
};
struct argc_entry {
unsigned m_index;
rational m_k;
expr* m_value;
argc_entry(unsigned i, rational const& k): m_index(i), m_k(k), m_value(0) {}
argc_entry():m_index(0), m_k(0), m_value(0) {}
struct eq {
bool operator()(argc_entry const& a, argc_entry const& b) const {
return a.m_index == b.m_index && a.m_k == b.m_k;
}
};
struct hash {
unsigned operator()(argc_entry const& a) const {
return a.m_index ^ a.m_k.hash();
}
};
};
typedef hashtable<argc_entry, argc_entry::hash, argc_entry::eq> argc_cache;
ast_manager& m;
params_ref m_params;
expr_ref_vector m_lemmas;
@ -79,6 +46,9 @@ struct pb2bv_rewriter::imp {
pb_util pb;
bv_util bv;
expr_ref_vector m_trail;
expr_ref_vector m_args;
rational m_k;
vector<rational> m_coeffs;
template<lbool is_le>
expr_ref mk_le_ge(expr_ref_vector& fmls, expr* a, expr* b, expr* bound) {
@ -109,8 +79,23 @@ struct pb2bv_rewriter::imp {
// The procedure for checking >= k is symmetric and checking for = k is
// achieved by checking <= k on intermediary addends and the resulting sum is = k.
//
// is_le = l_true - <=
// is_le = l_undef - =
// is_le = l_false - >=
//
template<lbool is_le>
expr_ref mk_le_ge(func_decl *f, unsigned sz, expr * const* args, rational const & k) {
expr_ref mk_le_ge(unsigned sz, expr * const* args, rational const & k) {
TRACE("pb",
for (unsigned i = 0; i < sz; ++i) {
tout << m_coeffs[i] << "*" << mk_pp(args[i], m) << " ";
if (i + 1 < sz && !m_coeffs[i+1].is_neg()) tout << "+ ";
}
switch (is_le) {
case l_true: tout << "<= "; break;
case l_undef: tout << "= "; break;
case l_false: tout << ">= "; break;
}
tout << m_k << "\n";);
if (k.is_zero()) {
if (is_le != l_false) {
return expr_ref(m.mk_not(mk_or(m, sz, args)), m);
@ -119,6 +104,9 @@ struct pb2bv_rewriter::imp {
return expr_ref(m.mk_true(), m);
}
}
if (k.is_neg()) {
return expr_ref((is_le == l_false)?m.mk_true():m.mk_false(), m);
}
SASSERT(k.is_pos());
expr_ref zero(m), bound(m);
expr_ref_vector es(m), fmls(m);
@ -126,7 +114,8 @@ struct pb2bv_rewriter::imp {
zero = bv.mk_numeral(rational(0), nb);
bound = bv.mk_numeral(k, nb);
for (unsigned i = 0; i < sz; ++i) {
if (pb.get_coeff(f, i) > k) {
SASSERT(!m_coeffs[i].is_neg());
if (m_coeffs[i] > k) {
if (is_le != l_false) {
fmls.push_back(m.mk_not(args[i]));
}
@ -135,7 +124,7 @@ struct pb2bv_rewriter::imp {
}
}
else {
es.push_back(mk_ite(args[i], bv.mk_numeral(pb.get_coeff(f, i), nb), zero));
es.push_back(mk_ite(args[i], bv.mk_numeral(m_coeffs[i], nb), zero));
}
}
while (es.size() > 1) {
@ -151,10 +140,17 @@ struct pb2bv_rewriter::imp {
case l_true:
return mk_and(fmls);
case l_false:
fmls.push_back(bv.mk_ule(bound, es.back()));
if (!es.empty()) {
fmls.push_back(bv.mk_ule(bound, es.back()));
}
return mk_or(fmls);
case l_undef:
fmls.push_back(m.mk_eq(bound, es.back()));
if (es.empty()) {
fmls.push_back(m.mk_bool_val(k.is_zero()));
}
else {
fmls.push_back(m.mk_eq(bound, es.back()));
}
return mk_and(fmls);
default:
UNREACHABLE();
@ -165,6 +161,10 @@ struct pb2bv_rewriter::imp {
expr_ref mk_bv(func_decl * f, unsigned sz, expr * const* args) {
decl_kind kind = f->get_decl_kind();
rational k = pb.get_k(f);
m_coeffs.reset();
for (unsigned i = 0; i < sz; ++i) {
m_coeffs.push_back(pb.get_coeff(f, i));
}
SASSERT(!k.is_neg());
switch (kind) {
case OP_PB_GE:
@ -173,13 +173,13 @@ struct pb2bv_rewriter::imp {
nargs.append(sz, args);
dualize(f, nargs, k);
SASSERT(!k.is_neg());
return mk_le_ge<l_true>(f, sz, nargs.c_ptr(), k);
return mk_le_ge<l_true>(sz, nargs.c_ptr(), k);
}
case OP_PB_LE:
case OP_AT_MOST_K:
return mk_le_ge<l_true>(f, sz, args, k);
return mk_le_ge<l_true>(sz, args, k);
case OP_PB_EQ:
return mk_le_ge<l_undef>(f, sz, args, k);
return mk_le_ge<l_undef>(sz, args, k);
default:
UNREACHABLE();
return expr_ref(m.mk_true(), m);
@ -228,17 +228,17 @@ struct pb2bv_rewriter::imp {
}
}
public:
card2bv_rewriter(imp& i, ast_manager& m):
m_sort(*this),
m(m),
m_imp(i),
au(m),
pb(m),
bv(m),
m_sort(*this),
m_trail(m)
m_trail(m),
m_args(m)
{}
br_status mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
@ -247,8 +247,31 @@ struct pb2bv_rewriter::imp {
++m_imp.m_num_translated;
return BR_DONE;
}
else if (f->get_family_id() == au.get_family_id() && mk_arith(f, sz, args, result)) {
else if (au.is_le(f) && is_pb(args[0], args[1])) {
++m_imp.m_num_translated;
result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
return BR_DONE;
}
else if (au.is_lt(f) && is_pb(args[0], args[1])) {
++m_imp.m_num_translated;
++m_k;
result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
return BR_DONE;
}
else if (au.is_ge(f) && is_pb(args[1], args[0])) {
++m_imp.m_num_translated;
result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
return BR_DONE;
}
else if (au.is_gt(f) && is_pb(args[1], args[0])) {
++m_imp.m_num_translated;
++m_k;
result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
return BR_DONE;
}
else if (m.is_eq(f) && is_pb(args[0], args[1])) {
++m_imp.m_num_translated;
result = mk_le_ge<l_undef>(m_args.size(), m_args.c_ptr(), m_k);
return BR_DONE;
}
else {
@ -256,43 +279,75 @@ struct pb2bv_rewriter::imp {
}
}
//
// NSB: review
// we should remove this code and rely on a layer above to deal with
// whatever it accomplishes. It seems to break types.
//
bool mk_arith(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
if (f->get_decl_kind() == OP_ADD) {
unsigned bits = 0;
for (unsigned i = 0; i < sz; i++) {
rational val1, val2;
if (au.is_int(args[i]) && au.is_numeral(args[i], val1)) {
bits += val1.get_num_bits();
bool is_pb(expr* x, expr* y) {
m_args.reset();
m_coeffs.reset();
m_k.reset();
return is_pb(x, rational::one()) && is_pb(y, rational::minus_one());
}
bool is_pb(expr* e, rational const& mul) {
if (!is_app(e)) {
return false;
}
app* a = to_app(e);
rational r, r1, r2;
expr* c, *th, *el;
unsigned sz = a->get_num_args();
if (a->get_family_id() == au.get_family_id()) {
switch (a->get_decl_kind()) {
case OP_ADD:
for (unsigned i = 0; i < sz; ++i) {
if (!is_pb(a->get_arg(i), mul)) return false;
}
else if (m.is_ite(args[i]) &&
au.is_numeral(to_app(args[i])->get_arg(1), val1) && val1.is_one() &&
au.is_numeral(to_app(args[i])->get_arg(2), val2) && val2.is_zero()) {
bits++;
return true;
case OP_SUB: {
if (!is_pb(a->get_arg(0), mul)) return false;
r = -mul;
for (unsigned i = 1; i < sz; ++i) {
if (!is_pb(a->get_arg(1), r)) return false;
}
else
return false;
return true;
}
case OP_UMINUS:
return is_pb(a->get_arg(0), -mul);
case OP_NUM:
VERIFY(au.is_numeral(a, r));
m_k -= mul * r;
return true;
case OP_MUL:
if (sz != 2) {
return false;
}
if (au.is_numeral(a->get_arg(0), r)) {
r *= mul;
return is_pb(a->get_arg(1), r);
}
if (au.is_numeral(a->get_arg(1), r)) {
r *= mul;
return is_pb(a->get_arg(0), r);
}
return false;
default:
return false;
}
}
if (m.is_ite(a, c, th, el) && au.is_numeral(th, r1) && au.is_numeral(el, r2)) {
r1 *= mul;
r2 *= mul;
if (r1 < r2) {
m_args.push_back(::mk_not(m, c));
m_coeffs.push_back(r2-r1);
m_k -= r1;
}
else {
m_args.push_back(c);
m_coeffs.push_back(r1-r2);
m_k -= r2;
}
result = 0;
for (unsigned i = 0; i < sz; i++) {
rational val1, val2;
expr * q;
if (au.is_int(args[i]) && au.is_numeral(args[i], val1))
q = bv.mk_numeral(val1, bits);
else
q = mk_ite(to_app(args[i])->get_arg(0), bv.mk_numeral(1, bits), bv.mk_numeral(0, bits));
result = (i == 0) ? q : bv.mk_bv_add(result.get(), q);
}
return true;
}
else {
return false;
}
return false;
}
void mk_pb(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
@ -378,6 +433,9 @@ struct pb2bv_rewriter::imp {
void operator()(expr * e, expr_ref & result, proof_ref & result_proof) {
m_rw(e, result, result_proof);
}
void assert_expr(expr * e, expr_ref & result, proof_ref & result_proof) {
m_rw(e, result, result_proof);
}
void push() {
m_fresh_lim.push_back(m_fresh.size());
}
@ -414,9 +472,13 @@ unsigned pb2bv_rewriter::get_num_steps() const { return m_imp->get_num_steps();
void pb2bv_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p); }
func_decl_ref_vector const& pb2bv_rewriter::fresh_constants() const { return m_imp->m_fresh; }
void pb2bv_rewriter::operator()(expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(e, result, result_proof); }
void pb2bv_rewriter::assert_expr(expr* e, expr_ref & result, proof_ref & result_proof) {
m_imp->assert_expr(e, result, result_proof);
}
void pb2bv_rewriter::push() { m_imp->push(); }
void pb2bv_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); }
void pb2bv_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); }
unsigned pb2bv_rewriter::num_translated() const { return m_imp->m_num_translated; }
void pb2bv_rewriter::collect_statistics(statistics & st) const { m_imp->collect_statistics(st); }

1
src/ast/rewriter/pb2bv_rewriter.h
View file

@ -36,6 +36,7 @@ public:
void cleanup();
func_decl_ref_vector const& fresh_constants() const;
void operator()(expr * e, expr_ref & result, proof_ref & result_proof);
void assert_expr(expr* e, expr_ref & result, proof_ref & result_proof);
void push();
void pop(unsigned num_scopes);
void flush_side_constraints(expr_ref_vector& side_constraints);

2
src/cmd_context/cmd_context.cpp
View file

@ -736,7 +736,7 @@ bool cmd_context::set_logic(symbol const & s) {
std::string cmd_context::reason_unknown() const {
if (m_check_sat_result.get() == 0)
throw cmd_exception("state of the most recent check-sat command is not unknown");
throw cmd_exception("state of the most recent check-sat command is not known");
return m_check_sat_result->reason_unknown();
}

61
src/sat/sat_solver.cpp
View file

@ -3151,22 +3151,32 @@ namespace sat {
lbool solver::get_consequences(literal_vector const& asms, literal_vector const& lits, vector<literal_vector>& conseq) {
m_antecedents.reset();
literal_set unfixed(lits), assumptions(asms);
literal_set vars(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);
if (asms.empty()) {
bool_var v = mk_var(true, false);
literal lit(v, false);
init_assumptions(1, &lit, 0, 0);
}
else {
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()) {
unsigned num_units = 0, num_iterations = 0;
extract_fixed_consequences(num_units, assumptions, vars, conseq);
while (!vars.empty()) {
++num_iterations;
checkpoint();
literal_set::iterator it = unfixed.begin(), end = unfixed.end();
literal_set::iterator it = vars.begin(), end = vars.end();
unsigned num_resolves = 0;
lbool is_sat = l_true;
for (; it != end; ++it) {
literal lit = *it;
if (value(lit) != l_undef) {
@ -3177,29 +3187,44 @@ namespace sat {
propagate(false);
while (inconsistent()) {
if (!resolve_conflict()) {
TRACE("sat", tout << "inconsistent\n";);
return l_false;
TRACE("sat", display(tout << "inconsistent\n"););
m_inconsistent = false;
is_sat = l_undef;
break;
}
propagate(false);
propagate(false);
++num_resolves;
}
if (scope_lvl() == 1) {
break;
}
}
lbool is_sat;
while (true) {
is_sat = bounded_search();
if (is_sat == l_undef) {
restart();
continue;
if (is_sat == l_true) {
if (scope_lvl() == 1 && num_resolves > 0) {
is_sat = l_undef;
}
else {
is_sat = bounded_search();
if (is_sat == l_undef) {
restart();
}
}
break;
}
if (is_sat == l_false) {
TRACE("sat", tout << "unsat\n";);
m_inconsistent = false;
}
if (is_sat == l_true) {
delete_unfixed(unfixed);
delete_unfixed(vars);
}
extract_fixed_consequences(num_units, assumptions, unfixed, conseq);
extract_fixed_consequences(num_units, assumptions, vars, conseq);
IF_VERBOSE(1, verbose_stream() << "(get-consequences"
<< " iterations: " << num_iterations
<< " variables: " << vars.size()
<< " fixed: " << conseq.size()
<< " unfixed: " << lits.size() - conseq.size() - vars.size()
<< ")\n";);
}
return l_true;
}

43
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -234,6 +234,7 @@ public:
}
virtual lbool get_consequences_core(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) {
init_preprocess();
TRACE("sat", tout << assumptions << "\n" << vars << "\n";);
sat::literal_vector asms;
sat::bool_var_vector bvars;
@ -257,10 +258,12 @@ public:
bool_var2conseq.insert(lconseq[i][0].var(), i);
}
// extract original fixed variables
// extract original fixed variables
u_map<expr*> asm2dep;
extract_asm2dep(dep2asm, asm2dep);
for (unsigned i = 0; i < vars.size(); ++i) {
expr_ref cons(m);
if (extract_fixed_variable(dep2asm, vars[i], bool_var2conseq, lconseq, cons)) {
if (extract_fixed_variable(dep2asm, asm2dep, vars[i], bool_var2conseq, lconseq, cons)) {
conseq.push_back(cons);
}
}
@ -339,7 +342,7 @@ public:
mk_bit_blaster_tactic(m, m_bb_rewriter.get()),
//mk_aig_tactic(),
using_params(mk_simplify_tactic(m), simp2_p));
for (unsigned i = 0; i < m_num_scopes; ++i) {
while (m_bb_rewriter->get_num_scopes() < m_num_scopes) {
m_bb_rewriter->push();
}
m_preprocess->reset();
@ -362,6 +365,7 @@ private:
}
catch (tactic_exception & ex) {
IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
TRACE("sat", tout << "exception: " << ex.msg() << "\n";);
m_preprocess = 0;
m_bb_rewriter = 0;
return l_undef;
@ -371,8 +375,18 @@ private:
return l_undef;
}
g = m_subgoals[0];
expr_ref_vector atoms(m);
TRACE("sat", g->display_with_dependencies(tout););
m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true);
m_goal2sat.get_interpreted_atoms(atoms);
if (!atoms.empty()) {
std::stringstream strm;
strm << "interpreted atoms sent to SAT solver " << atoms;
TRACE("sat", tout << strm.str() << "\n";);
IF_VERBOSE(1, verbose_stream() << strm.str() << "\n";);
set_reason_unknown(strm.str().c_str());
return l_undef;
}
return l_true;
}
@ -439,9 +453,7 @@ private:
return internalized;
}
bool extract_fixed_variable(dep2asm_t& dep2asm, expr* v, u_map<unsigned> const& bool_var2conseq, vector<sat::literal_vector> const& lconseq, expr_ref& conseq) {
u_map<expr*> asm2dep;
extract_asm2dep(dep2asm, asm2dep);
bool extract_fixed_variable(dep2asm_t& dep2asm, u_map<expr*>& asm2dep, expr* v, u_map<unsigned> const& bool_var2conseq, vector<sat::literal_vector> const& lconseq, expr_ref& conseq) {
sat::bool_var_vector bvars;
if (!internalize_var(v, bvars)) {
@ -474,6 +486,7 @@ private:
return true;
}
vector<rational> m_exps;
void internalize_value(sat::literal_vector const& value, expr* v, expr_ref& val) {
bv_util bvutil(m);
if (is_uninterp_const(v) && m.is_bool(v)) {
@ -482,10 +495,16 @@ private:
}
else if (is_uninterp_const(v) && bvutil.is_bv_sort(m.get_sort(v))) {
SASSERT(value.size() == bvutil.get_bv_size(v));
if (m_exps.empty()) {
m_exps.push_back(rational::one());
}
while (m_exps.size() < value.size()) {
m_exps.push_back(rational(2)*m_exps.back());
}
rational r(0);
for (unsigned i = 0; i < value.size(); ++i) {
if (!value[i].sign()) {
r += rational(2).expt(i);
r += m_exps[i];
}
}
val = m.mk_eq(v, bvutil.mk_numeral(r, value.size()));
@ -501,10 +520,14 @@ private:
}
dep2asm_t dep2asm;
goal_ref g = alloc(goal, m, true, false); // models, maybe cores are enabled
for (; m_fmls_head < m_fmls.size(); ++m_fmls_head) {
g->assert_expr(m_fmls[m_fmls_head].get());
for (unsigned i = 0 ; i < m_fmls.size(); ++i) {
g->assert_expr(m_fmls[i].get());
}
return internalize_goal(g, dep2asm);
lbool res = internalize_goal(g, dep2asm);
if (res != l_undef) {
m_fmls_head = m_fmls.size();
}
return res;
}
void extract_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) {

17
src/sat/tactic/goal2sat.cpp
View file

@ -59,6 +59,7 @@ struct goal2sat::imp {
bool m_ite_extra;
unsigned long long m_max_memory;
expr_ref_vector m_trail;
expr_ref_vector m_interpreted_atoms;
bool m_default_external;
imp(ast_manager & _m, params_ref const & p, sat::solver & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external):
@ -67,6 +68,7 @@ struct goal2sat::imp {
m_map(map),
m_dep2asm(dep2asm),
m_trail(m),
m_interpreted_atoms(m),
m_default_external(default_external) {
updt_params(p);
m_true = sat::null_bool_var;
@ -128,6 +130,9 @@ struct goal2sat::imp {
m_map.insert(t, v);
l = sat::literal(v, sign);
TRACE("goal2sat", tout << "new_var: " << v << "\n" << mk_ismt2_pp(t, m) << "\n";);
if (ext && !is_uninterp_const(t)) {
m_interpreted_atoms.push_back(t);
}
}
}
else {
@ -474,7 +479,7 @@ bool goal2sat::has_unsupported_bool(goal const & g) {
return test<unsupported_bool_proc>(g);
}
goal2sat::goal2sat():m_imp(0) {
goal2sat::goal2sat():m_imp(0), m_interpreted_atoms(0) {
}
void goal2sat::collect_param_descrs(param_descrs & r) {
@ -492,10 +497,20 @@ struct goal2sat::scoped_set_imp {
}
};
void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external) {
imp proc(g.m(), p, t, m, dep2asm, default_external);
scoped_set_imp set(this, &proc);
proc(g);
dealloc(m_interpreted_atoms);
m_interpreted_atoms = alloc(expr_ref_vector, g.m());
m_interpreted_atoms->append(proc.m_interpreted_atoms);
}
void goal2sat::get_interpreted_atoms(expr_ref_vector& atoms) {
if (m_interpreted_atoms) {
atoms.append(*m_interpreted_atoms);
}
}

6
src/sat/tactic/goal2sat.h
View file

@ -38,8 +38,11 @@ class goal2sat {
struct imp;
imp * m_imp;
struct scoped_set_imp;
expr_ref_vector* m_interpreted_atoms;
public:
goal2sat();
~goal2sat() { dealloc(m_interpreted_atoms); }
typedef obj_map<expr, sat::literal> dep2asm_map;
@ -53,12 +56,13 @@ public:
\remark m doesn't need to be empty. the definitions there are
reused.
\warning conversion throws a tactic_exception, if it is interrupted (by set_cancel),
an unsupported operator is found, or memory consumption limit is reached (set with param :max-memory).
*/
void operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false);
void get_interpreted_atoms(expr_ref_vector& atoms);
};

1
src/smt/smt_consequences.cpp
View file

@ -258,6 +258,7 @@ namespace smt {
TRACE("context", tout << is_sat << "\n";);
return is_sat;
}
obj_map<expr, expr*> var2val;
index_set _assumptions;
for (unsigned i = 0; i < assumptions.size(); ++i) {

16
src/smt/smt_context.cpp
View file

@ -1111,7 +1111,8 @@ namespace smt {
if (r1 == r2) {
TRACE("add_diseq_inconsistent", tout << "add_diseq #" << n1->get_owner_id() << " #" << n2->get_owner_id() << " inconsistency, scope_lvl: " << m_scope_lvl << "\n";);
return false; // context is inconsistent
theory_id t1 = r1->m_th_var_list.get_th_id();
return get_theory(t1)->use_diseqs();
}
// Propagate disequalities to theories
@ -1748,8 +1749,10 @@ namespace smt {
unsigned qhead = m_qhead;
if (!bcp())
return false;
if (get_cancel_flag())
if (get_cancel_flag()) {
m_qhead = qhead;
return true;
}
SASSERT(!inconsistent());
propagate_relevancy(qhead);
if (inconsistent())
@ -1767,8 +1770,10 @@ namespace smt {
m_qmanager->propagate();
if (inconsistent())
return false;
if (resource_limits_exceeded())
if (resource_limits_exceeded()) {
m_qhead = qhead;
return true;
}
if (!can_propagate()) {
CASSERT("diseq_bug", inconsistent() || check_missing_diseq_conflict());
CASSERT("eqc_bool", check_eqc_bool_assignment());
@ -3773,9 +3778,14 @@ namespace smt {
#ifdef Z3DEBUG
for (unsigned i = 0; i < num_lits; i++) {
literal l = lits[i];
<<<<<<< HEAD
expr* real_atom;
if (expr_signs[i] != l.sign()) {
=======
if (expr_signs[i] != l.sign()) {
expr* real_atom;
>>>>>>> f1412d3f3249529224f4180f601652da210b274a
VERIFY(m_manager.is_not(expr_lits.get(i), real_atom));
// the sign must have flipped when internalizing
CTRACE("resolve_conflict_bug", real_atom != bool_var2expr(l.var()), tout << mk_pp(real_atom, m_manager) << "\n" << mk_pp(bool_var2expr(l.var()), m_manager) << "\n";);

55
src/smt/tactic/smt_tactic.cpp
View file

@ -24,63 +24,10 @@ Notes:
#include"rewriter_types.h"
#include"filter_model_converter.h"
#include"ast_util.h"
#include"solver2tactic.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 smt_tactic : public tactic {
smt_params m_params;

2
src/smt/tactic/smt_tactic.h
View file

@ -32,8 +32,6 @@ tactic * mk_smt_tactic(params_ref const & p = params_ref());
tactic * mk_smt_tactic_using(bool auto_config = true, params_ref const & p = params_ref());
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);
/*
ADD_TACTIC("smt", "apply a SAT based SMT solver.", "mk_smt_tactic(p)")
*/

15
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
/**
@ -196,7 +197,19 @@ public:
virtual lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
switch_inc_mode();
return m_solver2->get_consequences(asms, vars, consequences);
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) {

115
src/solver/mus.cpp
View file

@ -239,6 +239,17 @@ struct mus::imp {
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();
@ -345,110 +356,6 @@ struct mus::imp {
return m_weight;
}
lbool qx(expr_ref_vector& mus) {
expr_set core, support;
for (unsigned i = 0; i < m_lit2expr.size(); ++i) {
core.insert(m_lit2expr[i].get());
}
lbool is_sat = qx(core, support, false);
if (is_sat == l_true) {
expr_set::iterator it = core.begin(), end = core.end();
mus.reset();
for (; it != end; ++it) {
mus.push_back(*it);
}
}
return is_sat;
}
lbool qx(expr_set& assignment, expr_set& support, bool has_support) {
lbool is_sat = l_true;
#if 0
if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";);
return l_true;
}
#endif
if (has_support) {
expr_ref_vector asms(m);
scoped_append _sa1(*this, asms, support);
scoped_append _sa2(*this, asms, m_assumptions);
is_sat = m_solver.check_sat(asms);
switch (is_sat) {
case l_false: {
expr_set core;
get_core(core);
support &= core;
assignment.reset();
return l_true;
}
case l_undef:
return l_undef;
case l_true:
update_model();
break;
default:
break;
}
}
if (assignment.size() == 1) {
return l_true;
}
expr_set assign2;
split(assignment, assign2);
support |= assignment;
is_sat = qx(assign2, support, !assignment.empty());
unsplit(support, assignment);
if (is_sat != l_true) return is_sat;
support |= assign2;
is_sat = qx(assignment, support, !assign2.empty());
assignment |= assign2;
unsplit(support, assign2);
return is_sat;
}
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]);
}
}
}
void unsplit(expr_set& A, expr_set& B) {
expr_set A1, B1;
expr_set::iterator it = A.begin(), end = A.end();
for (; it != end; ++it) {
if (B.contains(*it)) {
B1.insert(*it);
}
else {
A1.insert(*it);
}
}
A = A1;
B = B1;
}
void split(expr_set& lits1, expr_set& lits2) {
unsigned half = lits1.size()/2;
expr_set lits3;
expr_set::iterator it = lits1.begin(), end = lits1.end();
for (unsigned i = 0; it != end; ++it, ++i) {
if (i < half) {
lits3.insert(*it);
}
else {
lits2.insert(*it);
}
}
lits1 = lits3;
}
};
mus::mus(solver& s) {

16
src/solver/solver.cpp
View file

@ -21,6 +21,8 @@ Notes:
#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();
@ -56,7 +58,19 @@ struct scoped_assumption_push {
};
lbool solver::get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
return get_consequences_core(asms, vars, 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) {

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;
public:
solver2tactic(solver* s):
m(s->get_manager()),
m_solver(s)
{}
virtual void updt_params(params_ref const & 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) {
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);
m_solver->push();
m_solver->assert_expr(clauses);
lbool r = m_solver->check_sat(assumptions.size(), assumptions.c_ptr());
switch (r) {
case l_true:
if (in->models_enabled()) {
model_ref mdl;
m_solver->get_model(mdl);
mc = model2model_converter(mdl.get());
mc = concat(fmc.get(), mc.get());
}
in->reset();
result.push_back(in.get());
pc = 0;
core = 0;
break;
case l_false: {
in->reset();
proof* pr = 0;
expr_dependency* lcore = 0;
if (in->proofs_enabled()) {
pr = m_solver->get_proof();
}
if (in->unsat_core_enabled()) {
ptr_vector<expr> core;
m_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());
mc = 0;
pc = 0;
core = 0;
break;
}
case l_undef:
if (m.canceled()) {
throw tactic_exception(Z3_CANCELED_MSG);
}
throw tactic_exception(m_solver->reason_unknown().c_str());
}
m_solver->pop(1);
}
virtual void collect_statistics(statistics & st) const {
m_solver->collect_statistics(st);
}
virtual void reset_statistics() {}
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

1
src/solver/tactic2solver.cpp
View file

@ -160,6 +160,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) {

39
src/tactic/arith/bound_manager.cpp
View file

@ -79,12 +79,23 @@ static bool is_strict(decl_kind k) {
return k == OP_LT || k == OP_GT;
}
bool bound_manager::is_numeral(expr* v, numeral& n, bool& is_int) {
expr* w;
if (m_util.is_uminus(v, w) && is_numeral(w, n, is_int)) {
n.neg();
return true;
}
return m_util.is_numeral(v, n, is_int);
}
void bound_manager::operator()(expr * f, expr_dependency * d) {
TRACE("bound_manager", tout << "processing:\n" << mk_ismt2_pp(f, m()) << "\n";);
expr * v;
numeral n;
if (is_disjunctive_bound(f, d))
return;
if (is_equality_bound(f, d))
return;
bool pos = true;
while (m().is_not(f, f))
pos = !pos;
@ -99,10 +110,10 @@ void bound_manager::operator()(expr * f, expr_dependency * d) {
expr * lhs = t->get_arg(0);
expr * rhs = t->get_arg(1);
bool is_int;
if (is_uninterp_const(lhs) && m_util.is_numeral(rhs, n, is_int)) {
if (is_uninterp_const(lhs) && is_numeral(rhs, n, is_int)) {
v = lhs;
}
else if (is_uninterp_const(rhs) && m_util.is_numeral(lhs, n, is_int)) {
else if (is_uninterp_const(rhs) && is_numeral(lhs, n, is_int)) {
v = rhs;
k = swap_decl(k);
}
@ -165,6 +176,26 @@ void bound_manager::insert_lower(expr * v, bool strict, numeral const & n, expr_
}
}
bool bound_manager::is_equality_bound(expr * f, expr_dependency * d) {
expr* x, *y;
if (!m().is_eq(f, x, y)) {
return false;
}
if (!is_uninterp_const(x)) {
std::swap(x, y);
}
numeral n;
bool is_int;
if (is_uninterp_const(x) && is_numeral(y, n, is_int)) {
insert_lower(x, false, n, d);
insert_upper(x, false, n, d);
return true;
}
else {
return false;
}
}
bool bound_manager::is_disjunctive_bound(expr * f, expr_dependency * d) {
numeral lo, hi, n;
if (!m().is_or(f)) return false;
@ -176,14 +207,14 @@ bool bound_manager::is_disjunctive_bound(expr * f, expr_dependency * d) {
expr * e = to_app(f)->get_arg(i);
if (!m().is_eq(e, x, y)) return false;
if (is_uninterp_const(x) &&
m_util.is_numeral(y, n, is_int) && is_int &&
is_numeral(y, n, is_int) && is_int &&
(x == v || v == 0)) {
if (v == 0) { v = x; lo = hi = n; }
if (n < lo) lo = n;
if (n > hi) hi = n;
}
else if (is_uninterp_const(y) &&
m_util.is_numeral(x, n, is_int) && is_int &&
is_numeral(x, n, is_int) && is_int &&
(y == v || v == 0)) {
if (v == 0) { v = y; lo = hi = n; }
if (n < lo) lo = n;

2
src/tactic/arith/bound_manager.h
View file

@ -36,6 +36,8 @@ private:
obj_map<expr, expr_dependency*> m_upper_deps;
ptr_vector<expr> m_bounded_vars;
bool is_disjunctive_bound(expr * f, expr_dependency * d);
bool is_equality_bound(expr * f, expr_dependency * d);
bool is_numeral(expr* v, rational& n, bool& is_int);
void insert_lower(expr * v, bool strict, numeral const & n, expr_dependency * d);
void insert_upper(expr * v, bool strict, numeral const & n, expr_dependency * d);
public:

1
src/tactic/nlsat_smt/nl_purify_tactic.cpp
View file

@ -59,6 +59,7 @@ Revision History:
#include "model_smt2_pp.h"
#include "expr_safe_replace.h"
#include "ast_util.h"
#include "solver2tactic.h"
class nl_purify_tactic : public tactic {

45
src/tactic/portfolio/bounded_int2bv_solver.cpp
View file

@ -14,7 +14,7 @@ Author:
Nikolaj Bjorner (nbjorner) 2016-10-23
Notes:
--*/
#include "bounded_int2bv_solver.h"
@ -76,7 +76,7 @@ public:
virtual solver* translate(ast_manager& m, params_ref const& p) {
return alloc(bounded_int2bv_solver, m, p, m_solver->translate(m, p));
}
virtual void assert_expr(expr * t) {
m_assertions.push_back(t);
}
@ -89,7 +89,7 @@ public:
}
virtual void pop_core(unsigned n) {
m_assertions.reset();
m_assertions.reset();
m_solver->pop(n);
if (n > 0) {
@ -109,7 +109,7 @@ public:
while (n > 0) {
dealloc(m_bounds.back());
m_bounds.pop_back();
m_bounds.pop_back();
--n;
}
}
@ -120,25 +120,25 @@ public:
}
virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); }
virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }
virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }
virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); }
virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); }
virtual void collect_statistics(statistics & st) const { m_solver->collect_statistics(st); }
virtual void get_unsat_core(ptr_vector<expr> & r) { m_solver->get_unsat_core(r); }
virtual void get_model(model_ref & mdl) {
virtual void get_model(model_ref & mdl) {
m_solver->get_model(mdl);
if (mdl) {
extend_model(mdl);
filter_model(mdl);
filter_model(mdl);
}
}
}
virtual proof * get_proof() { return m_solver->get_proof(); }
virtual std::string reason_unknown() const { return m_solver->reason_unknown(); }
virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
virtual ast_manager& get_manager() const { return m; }
virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
virtual lbool get_consequences_core(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) { return m_solver->find_mutexes(vars, mutexes); }
virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
flush_assertions();
expr_ref_vector bvars(m);
for (unsigned i = 0; i < vars.size(); ++i) {
@ -201,7 +201,7 @@ private:
value = m_arith.mk_add(value, m_arith.mk_numeral(offset, true));
}
TRACE("int2bv", tout << mk_pp(it->m_key, m) << " " << value << "\n";);
ext.insert(it->m_key, value);
ext.insert(it->m_key, value);
}
ext(mdl, 0);
}
@ -224,7 +224,7 @@ private:
if (bm.has_lower(e, lo, s1) && bm.has_upper(e, hi, s2) && lo <= hi && !s1 && !s2) {
func_decl* fbv;
rational offset;
if (!m_int2bv.find(f, fbv)) {
if (!m_int2bv.find(f, fbv)) {
rational n = hi - lo + rational::one();
unsigned num_bits = get_num_bits(n);
expr_ref b(m);
@ -247,10 +247,21 @@ private:
expr_ref t(m.mk_const(fbv), m);
t = m_bv.mk_bv2int(t);
if (!offset.is_zero()) {
t = m_arith.mk_add(t, m_arith.mk_numeral(lo, true));
t = m_arith.mk_add(t, m_arith.mk_numeral(offset, true));
}
TRACE("pb", tout << lo << " <= " << hi << " offset: " << offset << "\n"; tout << mk_pp(e, m) << " |-> " << t << "\n";);
sub.insert(e, t);
}
else {
IF_VERBOSE(1,
verbose_stream() << "unprocessed entry: " << mk_pp(e, m) << "\n";
if (bm.has_lower(e, lo, s1)) {
verbose_stream() << "lower: " << lo << " " << s1 << "\n";
}
if (bm.has_upper(e, hi, s2)) {
verbose_stream() << "upper: " << hi << " " << s2 << "\n";
});
}
}
}
@ -273,7 +284,7 @@ private:
bm(m_assertions[i].get());
}
expr_safe_replace sub(m);
accumulate_sub(sub);
accumulate_sub(sub);
proof_ref proof(m);
expr_ref fml1(m), fml2(m);
if (sub.empty()) {
@ -281,8 +292,12 @@ private:
}
else {
for (unsigned i = 0; i < m_assertions.size(); ++i) {
sub(m_assertions[i].get(), fml1);
sub(m_assertions[i].get(), fml1);
m_rewriter(fml1, fml2, proof);
if (m.canceled()) {
m_rewriter.reset();
return;
}
m_solver->assert_expr(fml2);
TRACE("int2bv", tout << fml2 << "\n";);
}

2
src/tactic/portfolio/enum2bv_solver.cpp
View file

@ -115,8 +115,6 @@ public:
}
}
lbool r = m_solver->get_consequences(asms, bvars, consequences);
std::cout << consequences.size() << "\n";
// translate bit-vector consequences back to enumeration types
for (unsigned i = 0; i < consequences.size(); ++i) {

2
src/tactic/portfolio/pb2bv_solver.cpp
View file

@ -113,7 +113,7 @@ private:
expr_ref fml(m);
expr_ref_vector fmls(m);
for (unsigned i = 0; i < m_assertions.size(); ++i) {
m_rewriter(m_assertions[i].get(), fml, proof);
m_rewriter.assert_expr(m_assertions[i].get(), fml, proof);
m_solver->assert_expr(fml);
}
m_rewriter.flush_side_constraints(fmls);

3
src/tactic/portfolio/smt_strategic_solver.cpp
View file

@ -40,6 +40,7 @@ Notes:
#include"inc_sat_solver.h"
#include"fd_solver.h"
#include"bv_rewriter.h"
#include"solver2tactic.h"
tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const & logic) {
@ -89,6 +90,8 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
return mk_qffpbv_tactic(m, p);
else if (logic=="HORN")
return mk_horn_tactic(m, p);
else if (logic == "QF_FD")
return mk_solver2tactic(mk_fd_solver(m, p));
//else if (logic=="QF_UFNRA")
// return mk_qfufnra_tactic(m, p);
else

3
src/test/qe_arith.cpp
View file

@ -375,6 +375,9 @@ static void add_random_ineq(
case opt::t_le:
fml = a.mk_le(t1, t2);
break;
case opt::t_mod:
NOT_IMPLEMENTED_YET();
break;
}
fmls.push_back(fml);
mbo.add_constraint(vars, rational(coeff), rel);

1
src/util/rlimit.cpp
View file

@ -29,6 +29,7 @@ uint64 reslimit::count() const {
return m_count;
}
bool reslimit::inc() {
++m_count;
return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit);

80
src/util/sorting_network.h
View file

@ -202,7 +202,8 @@ Notes:
return ge(full, k, n, in.c_ptr());
}
else if (k == 1) {
return mk_at_most_1(full, n, xs);
literal_vector ors;
return mk_at_most_1(full, n, xs, ors);
}
else {
SASSERT(2*k <= n);
@ -221,6 +222,9 @@ Notes:
if (dualize(k, n, xs, in)) {
return eq(k, n, in.c_ptr());
}
else if (k == 1) {
return mk_exactly_1(true, n, xs);
}
else {
SASSERT(2*k <= n);
m_t = EQ;
@ -238,12 +242,56 @@ Notes:
private:
literal mk_at_most_1(bool full, unsigned n, literal const* xs) {
literal mk_and(literal l1, literal l2) {
literal result = fresh();
add_clause(ctx.mk_not(result), l1);
add_clause(ctx.mk_not(result), l2);
add_clause(ctx.mk_not(l1), ctx.mk_not(l2), result);
return result;
}
void mk_implies_or(literal l, unsigned n, literal const* xs) {
literal_vector lits(n, xs);
lits.push_back(ctx.mk_not(l));
add_clause(lits);
}
void mk_or_implies(literal l, unsigned n, literal const* xs) {
for (unsigned j = 0; j < n; ++j) {
add_clause(ctx.mk_not(xs[j]), l);
}
}
literal mk_or(literal_vector const& ors) {
if (ors.size() == 1) {
return ors[0];
}
literal result = fresh();
mk_implies_or(result, ors.size(), ors.c_ptr());
mk_or_implies(result, ors.size(), ors.c_ptr());
return result;
}
literal mk_exactly_1(bool full, unsigned n, literal const* xs) {
literal_vector ors;
literal r1 = mk_at_most_1(full, n, xs, ors);
if (full) {
r1 = mk_and(r1, mk_or(ors));
}
else {
mk_implies_or(r1, ors.size(), ors.c_ptr());
}
return r1;
}
literal mk_at_most_1(bool full, unsigned n, literal const* xs, literal_vector& ors) {
TRACE("pb", tout << (full?"full":"partial") << " ";
for (unsigned i = 0; i < n; ++i) tout << xs[i] << " ";
tout << "\n";);
if (!full && n >= 4) {
if (false && !full && n >= 4) {
return mk_at_most_1_bimander(n, xs);
}
literal_vector in(n, xs);
@ -252,9 +300,10 @@ Notes:
literal_vector ands;
ands.push_back(result);
while (!in.empty()) {
literal_vector ors;
ors.reset();
unsigned i = 0;
unsigned n = in.size();
if (n + 1 == inc_size) ++inc_size;
bool last = n <= inc_size;
for (; i + inc_size < n; i += inc_size) {
mk_at_most_1_small(full, last, inc_size, in.c_ptr() + i, result, ands, ors);
@ -267,7 +316,6 @@ Notes:
}
in.reset();
in.append(ors);
ors.reset();
}
if (full) {
add_clause(ands);
@ -278,29 +326,23 @@ Notes:
void mk_at_most_1_small(bool full, bool last, unsigned n, literal const* xs, literal result, literal_vector& ands, literal_vector& ors) {
SASSERT(n > 0);
if (n == 1) {
if (!last) {
ors.push_back(xs[0]);
}
ors.push_back(xs[0]);
return;
}
if (!last) {
literal ex = fresh();
for (unsigned j = 0; j < n; ++j) {
add_clause(ctx.mk_not(xs[j]), ex);
}
if (full) {
literal_vector lits(n, xs);
lits.push_back(ctx.mk_not(ex));
add_clause(lits.size(), lits.c_ptr());
}
ors.push_back(ex);
literal ex = fresh();
mk_or_implies(ex, n, xs);
if (full) {
mk_implies_or(ex, n, xs);
}
ors.push_back(ex);
// result => xs[0] + ... + xs[n-1] <= 1
for (unsigned i = 0; i < n; ++i) {
for (unsigned j = i + 1; j < n; ++j) {
add_clause(ctx.mk_not(result), ctx.mk_not(xs[i]), ctx.mk_not(xs[j]));
}
}
// xs[0] + ... + xs[n-1] <= 1 => and_x
if (full) {
literal and_i = fresh();