diff --git a/contrib/cmake/src/solver/CMakeLists.txt b/contrib/cmake/src/solver/CMakeLists.txt
index 8142ca872..7f54e7745 100644
--- a/contrib/cmake/src/solver/CMakeLists.txt
+++ b/contrib/cmake/src/solver/CMakeLists.txt
@@ -5,6 +5,7 @@ z3_add_component(solver
mus.cpp
solver.cpp
solver_na2as.cpp
+ solver2tactic.cpp
tactic2solver.cpp
COMPONENT_DEPENDENCIES
model
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 309b08297..84931b47e 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -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(' Unicode\n')
f.write(' false\n')
f.write(' \n')
+ f.write(' \n')
+ f.write(' %s\n' % type)
+ f.write(' Unicode\n')
+ f.write(' false\n')
+ f.write(' \n')
f.write(' \n')
f.write(' \n')
f.write(' \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
diff --git a/src/api/api_pb.cpp b/src/api/api_pb.cpp
index 6d5a56d2c..b7c28c34f 100644
--- a/src/api/api_pb.cpp
+++ b/src/api/api_pb.cpp
@@ -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 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);
+ }
+
};
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 6ca48fcb0..c3c33a41e 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2640,6 +2640,21 @@ namespace Microsoft.Z3
AST.ArrayToNative(args),
coeffs, k));
}
+
+ ///
+ /// Create a pseudo-Boolean equal constraint.
+ ///
+ 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() != null);
+ CheckContextMatch(args);
+ return new BoolExpr(this, Native.Z3_mk_pbeq(nCtx, (uint) args.Length,
+ AST.ArrayToNative(args),
+ coeffs, k));
+ }
#endregion
#region Numerals
diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs
index 036aaf2f2..c8954a473 100644
--- a/src/api/dotnet/Optimize.cs
+++ b/src/api/dotnet/Optimize.cs
@@ -258,10 +258,13 @@ namespace Microsoft.Z3
///
/// Return a string the describes why the last to check returned unknown
///
- public String getReasonUnknown()
+ public String ReasonUnknown
{
- Contract.Ensures(Contract.Result() != null);
- return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
+ get
+ {
+ Contract.Ensures(Contract.Result() != null);
+ return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
+ }
}
diff --git a/src/api/dotnet/Z3Exception.cs b/src/api/dotnet/Z3Exception.cs
index adda43995..71e4fef1a 100644
--- a/src/api/dotnet/Z3Exception.cs
+++ b/src/api/dotnet/Z3Exception.cs
@@ -14,7 +14,7 @@ Author:
Christoph Wintersteiger (cwinter) 2012-03-15
Notes:
-
+
--*/
using System;
@@ -24,6 +24,7 @@ namespace Microsoft.Z3
///
/// The exception base class for error reporting from Z3
///
+ [Serializable]
public class Z3Exception : Exception
{
///
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index a037bbc5d..b9d7f6df0 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -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`.
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 9e9771884..069f83340 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -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.
diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index 4f0379674..410c50852 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -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); }
diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp
index 07a24e40a..0dec98e5c 100644
--- a/src/ast/fpa/bv2fpa_converter.cpp
+++ b/src/ast/fpa/bv2fpa_converter.cpp
@@ -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);
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
index c260178ad..e8d8c4e4b 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
@@ -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 {
}
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();
+}
+
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h
index b23daab3a..8db328ec8 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h
@@ -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
diff --git a/src/ast/rewriter/enum2bv_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp
index bbe07f625..cd0f54503 100644
--- a/src/ast/rewriter/enum2bv_rewriter.cpp
+++ b/src/ast/rewriter/enum2bv_rewriter.cpp
@@ -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;
diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
index 48d566f11..cf5b67793 100644
--- a/src/ast/rewriter/pb2bv_rewriter.cpp
+++ b/src/ast/rewriter/pb2bv_rewriter.cpp
@@ -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_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 m_coeffs;
template
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
- 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(f, sz, nargs.c_ptr(), k);
+ return mk_le_ge(sz, nargs.c_ptr(), k);
}
case OP_PB_LE:
case OP_AT_MOST_K:
- return mk_le_ge(f, sz, args, k);
+ return mk_le_ge(sz, args, k);
case OP_PB_EQ:
- return mk_le_ge(f, sz, args, k);
+ return mk_le_ge(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(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(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(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(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(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); }
diff --git a/src/ast/rewriter/pb2bv_rewriter.h b/src/ast/rewriter/pb2bv_rewriter.h
index 47d8361cb..569eaf07d 100644
--- a/src/ast/rewriter/pb2bv_rewriter.h
+++ b/src/ast/rewriter/pb2bv_rewriter.h
@@ -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);
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index b7c80f65a..930a8fc71 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -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();
}
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 1e667eccc..e70a30a5a 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -3151,22 +3151,32 @@ namespace sat {
lbool solver::get_consequences(literal_vector const& asms, literal_vector const& lits, 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;
}
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 349b60f55..f5efed726 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -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 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 const& bool_var2conseq, vector const& lconseq, expr_ref& conseq) {
- u_map asm2dep;
- extract_asm2dep(dep2asm, asm2dep);
+ bool extract_fixed_variable(dep2asm_t& dep2asm, u_map& asm2dep, expr* v, u_map const& bool_var2conseq, vector const& lconseq, expr_ref& conseq) {
sat::bool_var_vector bvars;
if (!internalize_var(v, bvars)) {
@@ -474,6 +486,7 @@ private:
return true;
}
+ vector 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) {
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 4d5542866..136921914 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -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(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);
+ }
}
diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h
index c6776f2f7..cd63cd497 100644
--- a/src/sat/tactic/goal2sat.h
+++ b/src/sat/tactic/goal2sat.h
@@ -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 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);
};
diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
index ef90aac4c..1c1d236ad 100644
--- a/src/smt/smt_consequences.cpp
+++ b/src/smt/smt_consequences.cpp
@@ -258,6 +258,7 @@ namespace smt {
TRACE("context", tout << is_sat << "\n";);
return is_sat;
}
+
obj_map var2val;
index_set _assumptions;
for (unsigned i = 0; i < assumptions.size(); ++i) {
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 912bbeb36..459c11a32 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -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";);
diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index f2fbcf6d9..2909d8848 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -24,63 +24,10 @@ Notes:
#include"rewriter_types.h"
#include"filter_model_converter.h"
#include"ast_util.h"
+#include"solver2tactic.h"
typedef obj_map expr2expr_map;
-void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector& assumptions, expr2expr_map& bool2dep, ref& fmc) {
- expr2expr_map dep2bool;
- ptr_vector 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::iterator it = deps.begin();
- ptr_vector::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;
diff --git a/src/smt/tactic/smt_tactic.h b/src/smt/tactic/smt_tactic.h
index dd113634b..a23695fd1 100644
--- a/src/smt/tactic/smt_tactic.h
+++ b/src/smt/tactic/smt_tactic.h
@@ -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& assumptions, obj_map& bool2dep, ref& fmc);
-
/*
ADD_TACTIC("smt", "apply a SAT based SMT solver.", "mk_smt_tactic(p)")
*/
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index fc76f85c1..7f5f6872e 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -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) {
diff --git a/src/solver/mus.cpp b/src/solver/mus.cpp
index 81635f906..91d47386e 100644
--- a/src/solver/mus.cpp
+++ b/src/solver/mus.cpp
@@ -239,6 +239,17 @@ struct mus::imp {
return l_false;
}
+ void get_core(expr_set& core) {
+ core.reset();
+ ptr_vector 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 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) {
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index 8f32019d5..441ece429 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -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) {
diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp
new file mode 100644
index 000000000..8646d4813
--- /dev/null
+++ b/src/solver/solver2tactic.cpp
@@ -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 expr2expr_map;
+
+void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector& assumptions, expr2expr_map& bool2dep, ref& fmc) {
+ expr2expr_map dep2bool;
+ ptr_vector 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::iterator it = deps.begin();
+ ptr_vector::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 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 assumptions;
+ ref 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 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); }
diff --git a/src/solver/solver2tactic.h b/src/solver/solver2tactic.h
new file mode 100644
index 000000000..65fbd37b1
--- /dev/null
+++ b/src/solver/solver2tactic.h
@@ -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& assumptions, obj_map& bool2dep, ref& fmc);
+
+#endif
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index f53301948..213ba5c1c 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -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) {
diff --git a/src/tactic/arith/bound_manager.cpp b/src/tactic/arith/bound_manager.cpp
index ed77467c3..97d93658c 100644
--- a/src/tactic/arith/bound_manager.cpp
+++ b/src/tactic/arith/bound_manager.cpp
@@ -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;
diff --git a/src/tactic/arith/bound_manager.h b/src/tactic/arith/bound_manager.h
index cc0d693e9..6a4dc2c96 100644
--- a/src/tactic/arith/bound_manager.h
+++ b/src/tactic/arith/bound_manager.h
@@ -36,6 +36,8 @@ private:
obj_map m_upper_deps;
ptr_vector 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:
diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.cpp b/src/tactic/nlsat_smt/nl_purify_tactic.cpp
index d8b016d7b..46b5a51b0 100644
--- a/src/tactic/nlsat_smt/nl_purify_tactic.cpp
+++ b/src/tactic/nlsat_smt/nl_purify_tactic.cpp
@@ -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 {
diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp
index f7236351c..0b136dda7 100644
--- a/src/tactic/portfolio/bounded_int2bv_solver.cpp
+++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp
@@ -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 & 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 & r) { m_solver->get_labels(r); }
virtual ast_manager& get_manager() const { return m; }
- virtual lbool find_mutexes(expr_ref_vector const& vars, 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& 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";);
}
diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp
index 369402114..b0f11cb91 100644
--- a/src/tactic/portfolio/enum2bv_solver.cpp
+++ b/src/tactic/portfolio/enum2bv_solver.cpp
@@ -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) {
diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp
index bfd533e8a..d1826e61d 100644
--- a/src/tactic/portfolio/pb2bv_solver.cpp
+++ b/src/tactic/portfolio/pb2bv_solver.cpp
@@ -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);
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index 81825221e..d2414ec72 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -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
diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp
index 79495e24f..a73f7ed38 100644
--- a/src/test/qe_arith.cpp
+++ b/src/test/qe_arith.cpp
@@ -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);
diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp
index 37b1f7904..9f6c692cc 100644
--- a/src/util/rlimit.cpp
+++ b/src/util/rlimit.cpp
@@ -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);
diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h
index 0f5d2838e..33c4f8b61 100644
--- a/src/util/sorting_network.h
+++ b/src/util/sorting_network.h
@@ -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();