diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index cdd7bdeec..235453845 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1168,7 +1168,8 @@ class ExeComponent(Component):
c_dep = get_component(dep)
out.write(' ' + c_dep.get_link_name())
out.write('\n')
- out.write('\t$(LINK) $(LINK_OUT_FLAG)%s $(LINK_FLAGS)' % exefile)
+ extra_opt = '-static' if not IS_WINDOWS and STATIC_BIN else ''
+ out.write('\t$(LINK) %s $(LINK_OUT_FLAG)%s $(LINK_FLAGS)' % (extra_opt, exefile))
for obj in objs:
out.write(' ')
out.write(obj)
@@ -1972,7 +1973,7 @@ class MLComponent(Component):
z3mls = os.path.join(self.sub_dir, 'z3ml')
out.write('%s.cma: %s %s %s\n' % (z3mls, cmos, stubso, z3dllso))
out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmos, LIBZ3))
- out.write('%s.cmxa: %s %s %s\n' % (z3mls, cmxs, stubso, z3dllso))
+ out.write('%s.cmxa: %s %s %s %s.cma\n' % (z3mls, cmxs, stubso, z3dllso, z3mls))
out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmxs, LIBZ3))
out.write('%s.cmxs: %s.cmxa\n' % (z3mls, z3mls))
out.write('\t%s -shared -o %s.cmxs -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls))
@@ -2506,10 +2507,7 @@ def mk_config():
config.write('AR_OUTFLAG=\n')
config.write('EXE_EXT=\n')
config.write('LINK=%s\n' % CXX)
- if STATIC_BIN:
- config.write('LINK_FLAGS=-static\n')
- else:
- config.write('LINK_FLAGS=\n')
+ config.write('LINK_FLAGS=\n')
config.write('LINK_OUT_FLAG=-o \n')
config.write('LINK_EXTRA_FLAGS=-lpthread %s\n' % LDFLAGS)
config.write('SO_EXT=%s\n' % SO_EXT)
diff --git a/scripts/update_api.py b/scripts/update_api.py
index 04378b371..3a3b2c40a 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -1611,7 +1611,7 @@ _lib = None
def lib():
global _lib
if _lib is None:
- _dirs = ['.', pkg_resources.resource_filename('z3', 'lib'), os.path.join(sys.prefix, 'lib'), None]
+ _dirs = ['.', os.path.dirname(os.path.abspath(__file__)), pkg_resources.resource_filename('z3', 'lib'), os.path.join(sys.prefix, 'lib'), None]
for _dir in _dirs:
try:
init(_dir)
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index eda6831b5..efa3ec098 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -1128,6 +1128,10 @@ extern "C" {
case Z3_OP_RE_OPTION: return Z3_OP_RE_OPTION;
case Z3_OP_RE_CONCAT: return Z3_OP_RE_CONCAT;
case Z3_OP_RE_UNION: return Z3_OP_RE_UNION;
+ case Z3_OP_RE_INTERSECT: return Z3_OP_RE_INTERSECT;
+ case Z3_OP_RE_LOOP: return Z3_OP_RE_LOOP;
+ case Z3_OP_RE_FULL_SET: return Z3_OP_RE_FULL_SET;
+ case Z3_OP_RE_EMPTY_SET: return Z3_OP_RE_EMPTY_SET;
default:
return Z3_OP_INTERNAL;
}
diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp
index 5704ffdb0..138ea6fb0 100644
--- a/src/api/api_seq.cpp
+++ b/src/api/api_seq.cpp
@@ -116,15 +116,18 @@ extern "C" {
Z3_CATCH_RETURN("");
}
- Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq) {
- Z3_TRY;
- LOG_Z3_mk_seq_empty(c, seq);
- RESET_ERROR_CODE();
- app* a = mk_c(c)->sutil().str.mk_empty(to_sort(seq));
- mk_c(c)->save_ast_trail(a);
- RETURN_Z3(of_ast(a));
- Z3_CATCH_RETURN(0);
- }
+#define MK_SORTED(NAME, FN ) \
+ Z3_ast Z3_API NAME(Z3_context c, Z3_sort s) { \
+ Z3_TRY; \
+ LOG_ ## NAME(c, s); \
+ RESET_ERROR_CODE(); \
+ app* a = FN(to_sort(s)); \
+ mk_c(c)->save_ast_trail(a); \
+ RETURN_Z3(of_ast(a)); \
+ Z3_CATCH_RETURN(0); \
+ }
+
+ MK_SORTED(Z3_mk_seq_empty, mk_c(c)->sutil().str.mk_empty);
MK_UNARY(Z3_mk_seq_unit, mk_c(c)->get_seq_fid(), OP_SEQ_UNIT, SKIP);
MK_NARY(Z3_mk_seq_concat, mk_c(c)->get_seq_fid(), OP_SEQ_CONCAT, SKIP);
@@ -139,12 +142,27 @@ extern "C" {
MK_UNARY(Z3_mk_seq_to_re, mk_c(c)->get_seq_fid(), OP_SEQ_TO_RE, SKIP);
MK_BINARY(Z3_mk_seq_in_re, mk_c(c)->get_seq_fid(), OP_SEQ_IN_RE, SKIP);
+ Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi) {
+ Z3_TRY;
+ LOG_Z3_mk_re_loop(c, r, lo, hi);
+ RESET_ERROR_CODE();
+ app* a = hi == 0 ? mk_c(c)->sutil().re.mk_loop(to_expr(r), lo) : mk_c(c)->sutil().re.mk_loop(to_expr(r), lo, hi);
+ mk_c(c)->save_ast_trail(a);
+ RETURN_Z3(of_ast(a));
+ Z3_CATCH_RETURN(0);
+ }
MK_UNARY(Z3_mk_re_plus, mk_c(c)->get_seq_fid(), OP_RE_PLUS, SKIP);
MK_UNARY(Z3_mk_re_star, mk_c(c)->get_seq_fid(), OP_RE_STAR, SKIP);
MK_UNARY(Z3_mk_re_option, mk_c(c)->get_seq_fid(), OP_RE_OPTION, SKIP);
+ MK_UNARY(Z3_mk_re_complement, mk_c(c)->get_seq_fid(), OP_RE_COMPLEMENT, SKIP);
MK_NARY(Z3_mk_re_union, mk_c(c)->get_seq_fid(), OP_RE_UNION, SKIP);
+ MK_NARY(Z3_mk_re_intersect, mk_c(c)->get_seq_fid(), OP_RE_INTERSECT, SKIP);
MK_NARY(Z3_mk_re_concat, mk_c(c)->get_seq_fid(), OP_RE_CONCAT, SKIP);
+ MK_BINARY(Z3_mk_re_range, mk_c(c)->get_seq_fid(), OP_RE_RANGE, SKIP);
+
+ MK_SORTED(Z3_mk_re_empty, mk_c(c)->sutil().re.mk_empty);
+ MK_SORTED(Z3_mk_re_full, mk_c(c)->sutil().re.mk_full);
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 2a9c771a1..86dc77ad5 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -934,7 +934,20 @@ namespace z3 {
check_error();
return expr(ctx(), r);
}
-
+ friend expr range(expr const& lo, expr const& hi);
+ /**
+ \brief create a looping regular expression.
+ */
+ expr loop(unsigned lo) {
+ Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
+ check_error();
+ return expr(ctx(), r);
+ }
+ expr loop(unsigned lo, unsigned hi) {
+ Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
+ check_error();
+ return expr(ctx(), r);
+ }
/**
@@ -1227,7 +1240,6 @@ namespace z3 {
-
/**
\brief Create the if-then-else expression ite(c, t, e)
@@ -2436,31 +2448,51 @@ namespace z3 {
return expr(s.ctx(), r);
}
inline expr to_re(expr const& s) {
- Z3_ast r = Z3_mk_seq_to_re(s.ctx(), s);
- s.check_error();
- return expr(s.ctx(), r);
+ MK_EXPR1(Z3_mk_seq_to_re, s);
}
inline expr in_re(expr const& s, expr const& re) {
- check_context(s, re);
- Z3_ast r = Z3_mk_seq_in_re(s.ctx(), s, re);
+ MK_EXPR2(Z3_mk_seq_in_re, s, re);
+ }
+ inline expr plus(expr const& re) {
+ MK_EXPR1(Z3_mk_re_plus, re);
+ }
+ inline expr option(expr const& re) {
+ MK_EXPR1(Z3_mk_re_option, re);
+ }
+ inline expr star(expr const& re) {
+ MK_EXPR1(Z3_mk_re_star, re);
+ }
+ inline expr re_empty(sort const& s) {
+ Z3_ast r = Z3_mk_re_empty(s.ctx(), s);
s.check_error();
return expr(s.ctx(), r);
}
- inline expr plus(expr const& re) {
- Z3_ast r = Z3_mk_re_plus(re.ctx(), re);
- re.check_error();
- return expr(re.ctx(), r);
+ inline expr re_full(sort const& s) {
+ Z3_ast r = Z3_mk_re_full(s.ctx(), s);
+ s.check_error();
+ return expr(s.ctx(), r);
}
- inline expr option(expr const& re) {
- Z3_ast r = Z3_mk_re_option(re.ctx(), re);
- re.check_error();
- return expr(re.ctx(), r);
+ inline expr re_intersect(expr_vector const& args) {
+ assert(args.size() > 0);
+ context& ctx = args[0].ctx();
+ array _args(args);
+ Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr());
+ ctx.check_error();
+ return expr(ctx, r);
}
- inline expr star(expr const& re) {
- Z3_ast r = Z3_mk_re_star(re.ctx(), re);
- re.check_error();
- return expr(re.ctx(), r);
+ inline expr re_complement(expr const& a) {
+ MK_EXPR1(Z3_mk_re_complement, a);
}
+ inline expr range(expr const& lo, expr const& hi) {
+ check_context(lo, hi);
+ Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
+ lo.check_error();
+ return expr(lo.ctx(), r);
+ }
+
+
+
+
inline expr interpolant(expr const& a) {
return expr(a.ctx(), Z3_mk_interpolant(a.ctx(), a));
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index c3c33a41e..f12ad58ea 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2564,10 +2564,20 @@ namespace Microsoft.Z3
return new ReExpr(this, Native.Z3_mk_re_star(nCtx, re.NativeObject));
}
+ ///
+ /// Take the bounded Kleene star of a regular expression.
+ ///
+ public ReExpr MkLoop(ReExpr re, uint lo, uint hi = 0)
+ {
+ Contract.Requires(re != null);
+ Contract.Ensures(Contract.Result() != null);
+ return new ReExpr(this, Native.Z3_mk_re_loop(nCtx, re.NativeObject, lo, hi));
+ }
+
///
/// Take the Kleene plus of a regular expression.
///
- public ReExpr MPlus(ReExpr re)
+ public ReExpr MkPlus(ReExpr re)
{
Contract.Requires(re != null);
Contract.Ensures(Contract.Result() != null);
@@ -2577,13 +2587,23 @@ namespace Microsoft.Z3
///
/// Create the optional regular expression.
///
- public ReExpr MOption(ReExpr re)
+ public ReExpr MkOption(ReExpr re)
{
Contract.Requires(re != null);
Contract.Ensures(Contract.Result() != null);
return new ReExpr(this, Native.Z3_mk_re_option(nCtx, re.NativeObject));
}
+ ///
+ /// Create the complement regular expression.
+ ///
+ public ReExpr MkComplement(ReExpr re)
+ {
+ Contract.Requires(re != null);
+ Contract.Ensures(Contract.Result() != null);
+ return new ReExpr(this, Native.Z3_mk_re_complement(nCtx, re.NativeObject));
+ }
+
///
/// Create the concatenation of regular languages.
///
@@ -2609,6 +2629,52 @@ namespace Microsoft.Z3
CheckContextMatch(t);
return new ReExpr(this, Native.Z3_mk_re_union(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
}
+
+ ///
+ /// Create the intersection of regular languages.
+ ///
+ public ReExpr MkIntersect(params ReExpr[] t)
+ {
+ Contract.Requires(t != null);
+ Contract.Requires(Contract.ForAll(t, a => a != null));
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new ReExpr(this, Native.Z3_mk_re_intersect(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
+ }
+
+ ///
+ /// Create the empty regular expression.
+ ///
+ public ReExpr MkEmptyRe(Sort s)
+ {
+ Contract.Requires(s != null);
+ Contract.Ensures(Contract.Result() != null);
+ return new ReExpr(this, Native.Z3_mk_re_empty(nCtx, s.NativeObject));
+ }
+
+ ///
+ /// Create the full regular expression.
+ ///
+ public ReExpr MkFullRe(Sort s)
+ {
+ Contract.Requires(s != null);
+ Contract.Ensures(Contract.Result() != null);
+ return new ReExpr(this, Native.Z3_mk_re_full(nCtx, s.NativeObject));
+ }
+
+
+ ///
+ /// Create a range expression.
+ ///
+ public ReExpr MkRange(SeqExpr lo, SeqExpr hi)
+ {
+ Contract.Requires(lo != null);
+ Contract.Requires(hi != null);
+ Contract.Ensures(Contract.Result() != null);
+ CheckContextMatch(lo, hi);
+ return new ReExpr(this, Native.Z3_mk_re_range(nCtx, lo.NativeObject, hi.NativeObject));
+ }
#endregion
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index b7656c5da..d50968a32 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -31,13 +31,17 @@ public class Context implements AutoCloseable {
static final Object creation_lock = new Object();
public Context () {
- m_ctx = Native.mkContextRc(0);
- init();
+ synchronized (creation_lock) {
+ m_ctx = Native.mkContextRc(0);
+ init();
+ }
}
protected Context (long m_ctx) {
- this.m_ctx = m_ctx;
- init();
+ synchronized (creation_lock) {
+ this.m_ctx = m_ctx;
+ init();
+ }
}
@@ -59,13 +63,15 @@ public class Context implements AutoCloseable {
* module parameters. For this purpose we should now use {@code Global.setParameter}
**/
public Context(Map settings) {
- long cfg = Native.mkConfig();
- for (Map.Entry kv : settings.entrySet()) {
- Native.setParamValue(cfg, kv.getKey(), kv.getValue());
+ synchronized (creation_lock) {
+ long cfg = Native.mkConfig();
+ for (Map.Entry kv : settings.entrySet()) {
+ Native.setParamValue(cfg, kv.getKey(), kv.getValue());
+ }
+ m_ctx = Native.mkContextRc(cfg);
+ Native.delConfig(cfg);
+ init();
}
- m_ctx = Native.mkContextRc(cfg);
- Native.delConfig(cfg);
- init();
}
private void init() {
@@ -4037,7 +4043,9 @@ public class Context implements AutoCloseable {
m_intSort = null;
m_realSort = null;
m_stringSort = null;
-
- Native.delContext(m_ctx);
+
+ synchronized (creation_lock) {
+ Native.delContext(m_ctx);
+ }
}
}
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 478ee0ce3..22b2f60e6 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -9384,6 +9384,7 @@ class SeqSortRef(SortRef):
False
"""
return Z3_is_string_sort(self.ctx_ref(), self.ast)
+
def StringSort(ctx=None):
"""Create a string sort
@@ -9507,8 +9508,29 @@ def Empty(s):
>>> e3 = Empty(SeqSort(IntSort()))
>>> print(e3)
seq.empty
+ >>> e4 = Empty(ReSort(SeqSort(IntSort())))
+ >>> print(e4)
+ re.empty
"""
- return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx)
+ if isinstance(s, SeqSortRef):
+ return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx)
+ if isinstance(s, ReSortRef):
+ return ReRef(Z3_mk_re_empty(s.ctx_ref(), s.ast), s.ctx)
+ raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty")
+
+def Full(s):
+ """Create the regular expression that accepts the universal langauge
+ >>> e = Full(ReSort(SeqSort(IntSort())))
+ >>> print(e)
+ re.all
+ >>> e1 = Full(ReSort(StringSort()))
+ >>> print(e1)
+ re.allchar
+ """
+ if isinstance(s, ReSortRef):
+ return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx)
+ raise Z3Exception("Non-sequence, non-regular expression sort passed to Full")
+
def Unit(a):
"""Create a singleton sequence"""
@@ -9624,10 +9646,10 @@ class ReSortRef(SortRef):
def ReSort(s):
if is_ast(s):
- return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.as_ast()), ctx)
+ return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.ast), s.ctx)
if s is None or isinstance(s, Context):
ctx = _get_ctx(s)
- return ReSortRef(Z3_mk_re_sort(ctx.ref(), Z3_mk_string_sort(ctx.ref())), ctx)
+ return ReSortRef(Z3_mk_re_sort(ctx.ref(), Z3_mk_string_sort(ctx.ref())), s.ctx)
raise Z3Exception("Regular expression sort constructor expects either a string or a context or no argument")
@@ -9698,6 +9720,10 @@ def Option(re):
"""
return ReRef(Z3_mk_re_option(re.ctx_ref(), re.as_ast()), re.ctx)
+def Complement(re):
+ """Create the complement regular expression."""
+ return ReRef(Z3_mk_re_complement(re.ctx_ref(), re.as_ast()), re.ctx)
+
def Star(re):
"""Create the regular expression accepting zero or more repetitions of argument.
>>> re = Star(Re("a"))
@@ -9709,3 +9735,15 @@ def Star(re):
True
"""
return ReRef(Z3_mk_re_star(re.ctx_ref(), re.as_ast()), re.ctx)
+
+def Loop(re, lo, hi=0):
+ """Create the regular expression accepting between a lower and upper bound repetitions
+ >>> re = Loop(Re("a"), 1, 3)
+ >>> print(simplify(InRe("aa", re)))
+ True
+ >>> print(simplify(InRe("aaaa", re)))
+ False
+ >>> print(simplify(InRe("", re)))
+ False
+ """
+ return ReRef(Z3_mk_re_loop(re.ctx_ref(), re.as_ast(), lo, hi), re.ctx)
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index c7749ebef..356f933d4 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1154,6 +1154,12 @@ typedef enum {
Z3_OP_RE_OPTION,
Z3_OP_RE_CONCAT,
Z3_OP_RE_UNION,
+ Z3_OP_RE_RANGE,
+ Z3_OP_RE_LOOP,
+ Z3_OP_RE_INTERSECT,
+ Z3_OP_RE_EMPTY_SET,
+ Z3_OP_RE_FULL_SET,
+ Z3_OP_RE_COMPLEMENT,
// Auxiliary
Z3_OP_LABEL = 0x700,
@@ -3367,6 +3373,60 @@ extern "C" {
*/
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[]);
+
+ /**
+ \brief Create the range regular expression over two sequences of length 1.
+
+ def_API('Z3_mk_re_range' ,AST ,(_in(CONTEXT), _in(AST), _in(AST)))
+ */
+ Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi);
+
+ /**
+ \brief Create a regular expression loop. The supplied regular expression \c r is repated
+ between \c lo and \c hi times. The \c lo should be below \c hi with one exection: when
+ supplying the value \c hi as 0, the meaning is to repeat the argument \c r at least
+ \c lo number of times, and with an unbounded upper bound.
+
+ def_API('Z3_mk_re_loop', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in(UINT)))
+ */
+ Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi);
+
+ /**
+ \brief Create the intersection of the regular languages.
+
+ \pre n > 0
+
+ def_API('Z3_mk_re_intersect' ,AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST)))
+ */
+ Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[]);
+
+ /**
+ \brief Create the complement of the regular language \c re.
+
+ def_API('Z3_mk_re_complement' ,AST ,(_in(CONTEXT), _in(AST)))
+ */
+ Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re);
+
+ /**
+ \brief Create an empty regular expression of sort \c re.
+
+ \pre re is a regular expression sort.
+
+ def_API('Z3_mk_re_empty' ,AST ,(_in(CONTEXT), _in(SORT)))
+ */
+ Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re);
+
+
+ /**
+ \brief Create an universal regular expression of sort \c re.
+
+ \pre re is a regular expression sort.
+
+ def_API('Z3_mk_re_full' ,AST ,(_in(CONTEXT), _in(SORT)))
+ */
+ Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re);
+
+
/*@}*/
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index ba6d436cc..2c0ba1ce1 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -1463,11 +1463,17 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
v6 = z;
// (x is 0) || (y is 0) -> z
+ expr_ref c71(m), xy_sgn(m), xyz_sgn(m);
m_simp.mk_or(x_is_zero, y_is_zero, c7);
- expr_ref ite_c(m), rm_is_not_to_neg(m);
+ m_simp.mk_xor(x_is_neg, y_is_neg, xy_sgn);
+
+ m_simp.mk_xor(xy_sgn, z_is_neg, xyz_sgn);
+ m_simp.mk_and(z_is_zero, xyz_sgn, c71);
+
+ expr_ref zero_cond(m), rm_is_not_to_neg(m);
rm_is_not_to_neg = m.mk_not(rm_is_to_neg);
- m_simp.mk_and(z_is_zero, rm_is_not_to_neg, ite_c);
- mk_ite(ite_c, pzero, z, v7);
+ m_simp.mk_ite(rm_is_to_neg, nzero, pzero, zero_cond);
+ mk_ite(c71, zero_cond, z, v7);
// else comes the fused multiplication.
unsigned ebits = m_util.get_ebits(f->get_range());
diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp
index 91bff5ab5..027cce09d 100644
--- a/src/ast/macros/macro_util.cpp
+++ b/src/ast/macros/macro_util.cpp
@@ -494,7 +494,7 @@ void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const {
tout << "applying substitution to:\n" << mk_ll_pp(t, m_manager) << "\nsubstitution:\n";
for (unsigned i = 0; i < var_mapping.size(); i++) {
if (var_mapping[i] != 0)
- tout << "#" << i << " -> " << mk_ll_pp(var_mapping[i], m_manager);
+ tout << "#" << i << " -> " << mk_ll_pp(var_mapping[i], m_manager);
});
subst(t, var_mapping.size(), var_mapping.c_ptr(), norm_t);
}
diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp
index 18a652859..09f020ca6 100644
--- a/src/ast/pb_decl_plugin.cpp
+++ b/src/ast/pb_decl_plugin.cpp
@@ -91,7 +91,7 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
}
void pb_decl_plugin::get_op_names(svector & op_names, symbol const & logic) {
- if (logic == symbol::null) {
+ if (logic == symbol::null || logic == "QF_FD") {
op_names.push_back(builtin_name(m_at_most_sym.bare_str(), OP_AT_MOST_K));
op_names.push_back(builtin_name(m_at_least_sym.bare_str(), OP_AT_LEAST_K));
op_names.push_back(builtin_name(m_pble_sym.bare_str(), OP_PB_LE));
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
index e8d8c4e4b..68f2a2b8e 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
@@ -66,9 +66,6 @@ struct blaster_cfg {
void mk_nor(expr * a, expr * b, expr_ref & r) { m_rewriter.mk_nor(a, b, r); }
};
-// CMW: GCC/LLVM do not like this definition because a symbol of the same name exists in assert_set_bit_blaster.o
-// template class bit_blaster_tpl;
-
class blaster : public bit_blaster_tpl {
bool_rewriter m_rewriter;
bv_util m_util;
@@ -625,9 +622,6 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
}
};
-// CMW: GCC/LLVM do not like this definition because a symbol of the same name exists in assert_set_bit_blaster.o
-// template class rewriter_tpl;
-
struct bit_blaster_rewriter::imp : public rewriter_tpl {
blaster m_blaster;
blaster_rewriter_cfg m_cfg;
diff --git a/src/ast/rewriter/rewriter.h b/src/ast/rewriter/rewriter.h
index 401d00d89..fc596cabd 100644
--- a/src/ast/rewriter/rewriter.h
+++ b/src/ast/rewriter/rewriter.h
@@ -111,7 +111,7 @@ protected:
void elim_reflex_prs(unsigned spos);
public:
rewriter_core(ast_manager & m, bool proof_gen);
- ~rewriter_core();
+ virtual ~rewriter_core();
ast_manager & m() const { return m_manager; }
void reset();
void cleanup();
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 80fee36d4..26c3e23e4 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -243,9 +243,9 @@ eautomaton* re2automaton::re2aut(expr* e) {
TRACE("seq", tout << "Range expression is not handled: " << mk_pp(e, m) << "\n";);
}
}
- else if (u.re.is_complement(e, e0) && (a = re2aut(e0)) && m_sa) {
- return m_sa->mk_complement(*a);
- }
+ else if (u.re.is_complement(e, e0) && (a = re2aut(e0)) && m_sa) {
+ return m_sa->mk_complement(*a);
+ }
else if (u.re.is_loop(e, e1, lo, hi) && (a = re2aut(e1))) {
scoped_ptr eps = eautomaton::mk_epsilon(sm);
b = eautomaton::mk_epsilon(sm);
@@ -524,7 +524,7 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
result = m().mk_bool_val(c.contains(d));
return BR_DONE;
}
- // check if subsequence of b is in a.
+ // check if subsequence of a is in b.
expr_ref_vector as(m()), bs(m());
m_util.str.get_concat(a, as);
m_util.str.get_concat(b, bs);
@@ -587,6 +587,12 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
SASSERT(sz > offs);
result = m_util.str.mk_contains(m_util.str.mk_concat(sz-offs, as.c_ptr()+offs), b);
return BR_REWRITE2;
+ }
+
+ expr* x, *y, *z;
+ if (m_util.str.is_extract(b, x, y, z) && x == a) {
+ result = m().mk_true();
+ return BR_DONE;
}
return BR_FAILED;
@@ -1715,7 +1721,7 @@ bool seq_rewriter::solve_itos(unsigned szl, expr* const* ls, unsigned szr, expr*
}
}
- if (szr == 1 && m_util.str.is_itos(rs[0], r)) {
+ if (szr == 1 && m_util.str.is_itos(rs[0], r) && !m_util.str.is_itos(ls[0])) {
return solve_itos(szr, rs, szl, ls, rhs, lhs, is_sat);
}
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index e9d87b90b..c645aa1a7 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -601,7 +601,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
match(*m_sigs[k], arity, domain, range, rng);
return m.mk_func_decl(symbol("re.allchar"), arity, domain, rng, func_decl_info(m_family_id, k));
}
- return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
+ return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, range, func_decl_info(m_family_id, k));
case _OP_REGEXP_EMPTY:
@@ -617,7 +617,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
match(*m_sigs[k], arity, domain, range, rng);
return m.mk_func_decl(symbol("re.nostr"), arity, domain, rng, func_decl_info(m_family_id, k));
}
- return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
+ return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, range, func_decl_info(m_family_id, k));
case OP_RE_LOOP:
switch (arity) {
@@ -861,7 +861,7 @@ app* seq_util::re::mk_full(sort* s) {
return m.mk_app(m_fid, OP_RE_FULL_SET, 0, 0, 0, 0, s);
}
-app* seq_util::re::mk_empty(sort* s) {
+app* seq_util::re::mk_empty(sort* s) {
return m.mk_app(m_fid, OP_RE_EMPTY_SET, 0, 0, 0, 0, s);
}
diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp
index d598dfa39..c75c12689 100644
--- a/src/cmd_context/check_logic.cpp
+++ b/src/cmd_context/check_logic.cpp
@@ -21,6 +21,7 @@ Revision History:
#include"array_decl_plugin.h"
#include"bv_decl_plugin.h"
#include"seq_decl_plugin.h"
+#include"pb_decl_plugin.h"
#include"datatype_decl_plugin.h"
#include"ast_pp.h"
#include"for_each_expr.h"
@@ -34,6 +35,7 @@ struct check_logic::imp {
array_util m_ar_util;
seq_util m_seq_util;
datatype_util m_dt_util;
+ pb_util m_pb_util;
bool m_uf; // true if the logic supports uninterpreted functions
bool m_arrays; // true if the logic supports arbitrary arrays
bool m_bv_arrays; // true if the logic supports only bv arrays
@@ -45,7 +47,7 @@ struct check_logic::imp {
bool m_quantifiers; // true if the logic supports quantifiers
bool m_unknown_logic;
- imp(ast_manager & _m):m(_m), m_a_util(m), m_bv_util(m), m_ar_util(m), m_seq_util(m), m_dt_util(m) {
+ imp(ast_manager & _m):m(_m), m_a_util(m), m_bv_util(m), m_ar_util(m), m_seq_util(m), m_dt_util(m), m_pb_util(m) {
reset();
}
@@ -443,6 +445,9 @@ struct check_logic::imp {
else if (fid == m_dt_util.get_family_id() && m_logic == "QF_FD") {
// nothing to check
}
+ else if (fid == m_pb_util.get_family_id() && m_logic == "QF_FD") {
+ // nothing to check
+ }
else {
std::stringstream strm;
strm << "logic does not support theory " << m.get_family_name(fid);
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index eb7b3ff44..67b1df50c 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -519,6 +519,10 @@ bool cmd_context::logic_has_seq() const {
return !has_logic() || smt_logics::logic_has_seq(m_logic);
}
+bool cmd_context::logic_has_pb() const {
+ return !has_logic() || smt_logics::logic_has_pb(m_logic);
+}
+
bool cmd_context::logic_has_fpa() const {
return !has_logic() || smt_logics::logic_has_fpa(m_logic);
}
@@ -547,7 +551,7 @@ void cmd_context::init_manager_core(bool new_manager) {
register_plugin(symbol("array"), alloc(array_decl_plugin), logic_has_array());
register_plugin(symbol("datatype"), alloc(datatype_decl_plugin), logic_has_datatype());
register_plugin(symbol("seq"), alloc(seq_decl_plugin), logic_has_seq());
- register_plugin(symbol("pb"), alloc(pb_decl_plugin), !has_logic());
+ register_plugin(symbol("pb"), alloc(pb_decl_plugin), logic_has_pb());
register_plugin(symbol("fpa"), alloc(fpa_decl_plugin), logic_has_fpa());
register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic());
}
@@ -563,6 +567,7 @@ void cmd_context::init_manager_core(bool new_manager) {
load_plugin(symbol("datatype"), logic_has_datatype(), fids);
load_plugin(symbol("seq"), logic_has_seq(), fids);
load_plugin(symbol("fpa"), logic_has_fpa(), fids);
+ load_plugin(symbol("pb"), logic_has_pb(), fids);
svector::iterator it = fids.begin();
svector::iterator end = fids.end();
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 34d93c97b..8eee632dc 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -251,6 +251,7 @@ protected:
bool logic_has_arith() const;
bool logic_has_bv() const;
+ bool logic_has_pb() const;
bool logic_has_seq() const;
bool logic_has_array() const;
bool logic_has_datatype() const;
diff --git a/src/cmd_context/parametric_cmd.h b/src/cmd_context/parametric_cmd.h
index 3e95832c4..cac5fe38e 100644
--- a/src/cmd_context/parametric_cmd.h
+++ b/src/cmd_context/parametric_cmd.h
@@ -72,6 +72,7 @@ public:
// m_params.set_func_decl(m_last, f);
// m_last = symbol::null;
}
+ virtual void set_next_arg(cmd_context & ctx, sexpr * n) { UNREACHABLE(); }
};
#endif
diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index b3a96aea4..1869b74ce 100644
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -3099,7 +3099,7 @@ namespace Duality {
// Maps nodes of derivation tree into old subtree
hash_map cex_map;
- virtual void ChooseExpand(const std::set &choices, std::set &best){
+ virtual void ChooseExpand(const std::set &choices, std::set &best, bool, bool){
if(old_node == 0){
Heuristic::ChooseExpand(choices,best);
return;
diff --git a/src/math/automata/boolean_algebra.h b/src/math/automata/boolean_algebra.h
index e3977b4cd..4f5527f5e 100644
--- a/src/math/automata/boolean_algebra.h
+++ b/src/math/automata/boolean_algebra.h
@@ -26,6 +26,7 @@ Revision History:
template
class positive_boolean_algebra {
public:
+ virtual ~positive_boolean_algebra() {}
virtual T mk_false() = 0;
virtual T mk_true() = 0;
virtual T mk_and(T x, T y) = 0;
@@ -38,6 +39,7 @@ public:
template
class boolean_algebra : public positive_boolean_algebra {
public:
+ virtual ~boolean_algebra() {}
virtual T mk_not(T x) = 0;
//virtual lbool are_equivalent(T x, T y) = 0;
//virtual T simplify(T x) = 0;
diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp
index 27e096777..2d0199223 100644
--- a/src/math/subpaving/tactic/subpaving_tactic.cpp
+++ b/src/math/subpaving/tactic/subpaving_tactic.cpp
@@ -35,6 +35,8 @@ class subpaving_tactic : public tactic {
display_var_proc(expr2var & e2v):m_inv(e2v.m()) {
e2v.mk_inv(m_inv);
}
+
+ virtual ~display_var_proc() {}
ast_manager & m() const { return m_inv.get_manager(); }
diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp
index bef2e6494..503abac2f 100644
--- a/src/model/model_core.cpp
+++ b/src/model/model_core.cpp
@@ -88,18 +88,20 @@ void model_core::register_decl(func_decl * d, func_interp * fi) {
}
void model_core::unregister_decl(func_decl * d) {
- decl2expr::obj_map_entry * ec = m_interp.find_core(d);
- if (ec && ec->get_data().m_value != 0) {
- m_manager.dec_ref(ec->get_data().m_key);
- m_manager.dec_ref(ec->get_data().m_value);
- m_interp.remove(d);
- return;
- }
-
- decl2finterp::obj_map_entry * ef = m_finterp.find_core(d);
- if (ef && ef->get_data().m_value != 0) {
- m_manager.dec_ref(ef->get_data().m_key);
- dealloc(ef->get_data().m_value);
- m_finterp.remove(d);
- }
-}
\ No newline at end of file
+ decl2expr::obj_map_entry * ec = m_interp.find_core(d);
+ if (ec && ec->get_data().m_value != 0) {
+ m_manager.dec_ref(ec->get_data().m_key);
+ m_manager.dec_ref(ec->get_data().m_value);
+ m_interp.remove(d);
+ m_const_decls.erase(d);
+ return;
+ }
+
+ decl2finterp::obj_map_entry * ef = m_finterp.find_core(d);
+ if (ef && ef->get_data().m_value != 0) {
+ m_manager.dec_ref(ef->get_data().m_key);
+ dealloc(ef->get_data().m_value);
+ m_finterp.remove(d);
+ m_func_decls.erase(d);
+ }
+}
diff --git a/src/model/model_core.h b/src/model/model_core.h
index 371106b05..c42451c5a 100644
--- a/src/model/model_core.h
+++ b/src/model/model_core.h
@@ -60,7 +60,7 @@ public:
void register_decl(func_decl * d, expr * v);
void register_decl(func_decl * f, func_interp * fi);
- void unregister_decl(func_decl * d);
+ void unregister_decl(func_decl * d);
virtual expr * get_some_value(sort * s) = 0;
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index 3c1a7bfaa..ba841c84f 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -119,7 +119,6 @@ namespace datalog {
virtual expr_ref try_get_formula(func_decl * pred) const = 0;
virtual void display_output_facts(rule_set const& rules, std::ostream & out) const = 0;
virtual void display_facts(std::ostream & out) const = 0;
- virtual void display_profile(std::ostream& out) = 0;
virtual void restrict_predicates(func_decl_set const& predicates) = 0;
virtual bool result_contains_fact(relation_fact const& f) = 0;
virtual void add_fact(func_decl* pred, relation_fact const& fact) = 0;
diff --git a/src/muz/base/dl_engine_base.h b/src/muz/base/dl_engine_base.h
index f353fbf2e..9878f3a9e 100644
--- a/src/muz/base/dl_engine_base.h
+++ b/src/muz/base/dl_engine_base.h
@@ -66,7 +66,7 @@ namespace datalog {
}
virtual void reset_statistics() {}
- virtual void display_profile(std::ostream& out) const {}
+ virtual void display_profile(std::ostream& out) {}
virtual void collect_statistics(statistics& st) const {}
virtual unsigned get_num_levels(func_decl* pred) {
throw default_exception(std::string("get_num_levels is not supported for ") + m_name);
diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h
index 1c7a81444..d3422f882 100644
--- a/src/muz/rel/dl_base.h
+++ b/src/muz/rel/dl_base.h
@@ -220,6 +220,8 @@ namespace datalog {
*/
class mutator_fn : public base_fn {
public:
+ virtual ~mutator_fn() {}
+
virtual void operator()(base_object & t) = 0;
virtual bool supports_attachment(base_object& other) { return false; }
@@ -869,6 +871,7 @@ namespace datalog {
class table_row_mutator_fn {
public:
+ virtual ~table_row_mutator_fn() {}
/**
\brief The function is called for a particular table row. The \c func_columns contains
a pointer to an array of functional column values that can be modified. If the function
@@ -882,6 +885,7 @@ namespace datalog {
class table_row_pair_reduce_fn {
public:
+ virtual ~table_row_pair_reduce_fn() {}
/**
\brief The function is called for pair of table rows that became duplicit due to projection.
The values that are in the first array after return from the function will be used for the
diff --git a/src/muz/rel/dl_product_relation.cpp b/src/muz/rel/dl_product_relation.cpp
index 1bc5e3545..817ff194c 100644
--- a/src/muz/rel/dl_product_relation.cpp
+++ b/src/muz/rel/dl_product_relation.cpp
@@ -255,7 +255,7 @@ namespace datalog {
table_plugin & tplugin = rmgr.get_appropriate_plugin(tsig);
relation_plugin & inner_plugin = rmgr.get_table_relation_plugin(tplugin);
- return sieve_relation_plugin::get_plugin(rmgr).mk_full(p, sig, inner_plugin);
+ return sieve_relation_plugin::get_plugin(rmgr).full(p, sig, inner_plugin);
}
void init(relation_signature const& r1_sig, unsigned num_rels1, relation_base const* const* r1,
@@ -294,7 +294,7 @@ namespace datalog {
rel2 = r1_plugin.mk_full(p, r2_sig, r1_kind);
}
else {
- rel2 = sieve_relation_plugin::get_plugin(rmgr).mk_full(p, r2_sig, r1_plugin);
+ rel2 = sieve_relation_plugin::get_plugin(rmgr).full(p, r2_sig, r1_plugin);
}
m_offset1.push_back(i);
m_kind1.push_back(T_INPUT);
@@ -318,7 +318,7 @@ namespace datalog {
rel1 = r2_plugin.mk_full(p, r1_sig, r2_kind);
}
else {
- rel1 = sieve_relation_plugin::get_plugin(rmgr).mk_full(p, r1_sig, r2_plugin);
+ rel1 = sieve_relation_plugin::get_plugin(rmgr).full(p, r1_sig, r2_plugin);
}
m_offset1.push_back(m_full.size());
m_kind1.push_back(T_FULL);
diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp
index 7a73afd03..74206a1f6 100644
--- a/src/muz/rel/dl_relation_manager.cpp
+++ b/src/muz/rel/dl_relation_manager.cpp
@@ -1622,6 +1622,8 @@ namespace datalog {
m_union_fn = plugin.mk_union_fn(t, *m_aux_table, static_cast(0));
}
+ virtual ~default_table_map_fn() {}
+
virtual void operator()(table_base & t) {
SASSERT(t.get_signature()==m_aux_table->get_signature());
if(!m_aux_table->empty()) {
@@ -1678,6 +1680,8 @@ namespace datalog {
m_former_row.resize(get_result_signature().size());
}
+ virtual ~default_table_project_with_reduce_fn() {}
+
virtual void modify_fact(table_fact & f) const {
unsigned ofs=1;
unsigned r_i=1;
diff --git a/src/muz/rel/dl_sieve_relation.cpp b/src/muz/rel/dl_sieve_relation.cpp
index 9f9419089..7729ec2eb 100644
--- a/src/muz/rel/dl_sieve_relation.cpp
+++ b/src/muz/rel/dl_sieve_relation.cpp
@@ -253,7 +253,7 @@ namespace datalog {
return mk_from_inner(s, inner_cols, inner);
}
- sieve_relation * sieve_relation_plugin::mk_full(func_decl* p, const relation_signature & s, relation_plugin & inner_plugin) {
+ sieve_relation * sieve_relation_plugin::full(func_decl* p, const relation_signature & s, relation_plugin & inner_plugin) {
SASSERT(!inner_plugin.is_sieve_relation()); //it does not make sense to make a sieve of a sieve
svector inner_cols(s.size());
extract_inner_columns(s, inner_plugin, inner_cols);
diff --git a/src/muz/rel/dl_sieve_relation.h b/src/muz/rel/dl_sieve_relation.h
index da6c9bbff..4d89a66ae 100644
--- a/src/muz/rel/dl_sieve_relation.h
+++ b/src/muz/rel/dl_sieve_relation.h
@@ -104,8 +104,7 @@ namespace datalog {
sieve_relation * mk_empty(const relation_signature & s, relation_plugin & inner_plugin);
virtual relation_base * mk_full(func_decl* p, const relation_signature & s);
- sieve_relation * mk_full(func_decl* p, const relation_signature & s, relation_plugin & inner_plugin);
-
+ sieve_relation * full(func_decl* p, const relation_signature & s, relation_plugin & inner_plugin);
sieve_relation * mk_from_inner(const relation_signature & s, const bool * inner_columns,
relation_base * inner_rel);
diff --git a/src/muz/rel/dl_table_relation.cpp b/src/muz/rel/dl_table_relation.cpp
index d42d071aa..00a25d169 100644
--- a/src/muz/rel/dl_table_relation.cpp
+++ b/src/muz/rel/dl_table_relation.cpp
@@ -54,7 +54,7 @@ namespace datalog {
return alloc(table_relation, *this, s, t);
}
- relation_base * table_relation_plugin::mk_full(const relation_signature & s, func_decl* p, family_id kind) {
+ relation_base * table_relation_plugin::mk_full_relation(const relation_signature & s, func_decl* p, family_id kind) {
table_signature tsig;
if(!get_manager().relation_signature_to_table(s, tsig)) {
return 0;
diff --git a/src/muz/rel/dl_table_relation.h b/src/muz/rel/dl_table_relation.h
index 8266995da..56ca509fa 100644
--- a/src/muz/rel/dl_table_relation.h
+++ b/src/muz/rel/dl_table_relation.h
@@ -49,7 +49,7 @@ namespace datalog {
virtual bool can_handle_signature(const relation_signature & s);
virtual relation_base * mk_empty(const relation_signature & s);
- virtual relation_base * mk_full(const relation_signature & s, func_decl* p, family_id kind);
+ virtual relation_base * mk_full_relation(const relation_signature & s, func_decl* p, family_id kind);
relation_base * mk_from_table(const relation_signature & s, table_base * t);
protected:
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 7f9183d9a..54e7f351c 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -805,8 +805,9 @@ public:
lbool init_local() {
m_lower.reset();
m_trail.reset();
+ lbool is_sat = l_true;
obj_map new_soft;
- lbool is_sat = find_mutexes(new_soft);
+ is_sat = find_mutexes(new_soft);
if (is_sat != l_true) {
return is_sat;
}
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 85b19e427..21537a570 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -333,8 +333,15 @@ namespace opt {
TRACE("opt", tout << mk_pp(f, m) << " weight: " << w << "\n";);
SASSERT(m.is_bool(f));
SASSERT(w.is_pos());
- m_soft_constraints.push_back(f);
- m_weights.push_back(w);
+ unsigned index = 0;
+ if (m_soft_constraint_index.find(f, index)) {
+ m_weights[index] += w;
+ }
+ else {
+ m_soft_constraint_index.insert(f, m_weights.size());
+ m_soft_constraints.push_back(f);
+ m_weights.push_back(w);
+ }
m_upper += w;
}
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index 5ecb023f6..358ff4995 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -120,6 +120,7 @@ namespace opt {
unsigned m_index;
scoped_ptr m_msolver;
expr_ref_vector m_soft_constraints;
+ obj_map m_soft_constraint_index;
expr_ref_vector m_answer;
vector m_weights;
rational m_lower;
@@ -138,7 +139,6 @@ namespace opt {
expr* operator[](unsigned idx) const { return m_soft_constraints[idx]; }
rational weight(unsigned idx) const { return m_weights[idx]; }
void commit_assignment();
- rational get_value() const;
rational get_lower() const;
rational get_upper() const;
void update_lower(rational const& r);
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 624671e2b..e63e29dc5 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -169,6 +169,11 @@ namespace opt {
r.append(m_labels);
}
+ void context::get_unsat_core(ptr_vector & r) {
+ throw default_exception("Unsat cores are not supported with optimization");
+ }
+
+
void context::set_hard_constraints(ptr_vector& fmls) {
if (m_scoped_state.set(fmls)) {
clear_state();
@@ -355,6 +360,7 @@ namespace opt {
}
if (scoped) get_solver().pop(1);
if (result == l_true && committed) ms.commit_assignment();
+ DEBUG_CODE(if (result == l_true) validate_maxsat(id););
return result;
}
@@ -1443,6 +1449,32 @@ namespace opt {
return out.str();
}
+ void context::validate_maxsat(symbol const& id) {
+ maxsmt& ms = *m_maxsmts.find(id);
+ for (unsigned i = 0; i < m_objectives.size(); ++i) {
+ objective const& obj = m_objectives[i];
+ if (obj.m_id == id) {
+ SASSERT(obj.m_type == O_MAXSMT);
+ rational value(0);
+ expr_ref val(m);
+ for (unsigned i = 0; i < obj.m_terms.size(); ++i) {
+ bool evaluated = m_model->eval(obj.m_terms[i], val);
+ SASSERT(evaluated);
+ CTRACE("opt", evaluated && !m.is_true(val) && !m.is_false(val), tout << mk_pp(obj.m_terms[i], m) << " " << val << "\n";);
+ CTRACE("opt", !evaluated, tout << mk_pp(obj.m_terms[i], m) << "\n";);
+ if (evaluated && !m.is_true(val)) {
+ value += obj.m_weights[i];
+ }
+ // TBD: check that optimal was not changed.
+ }
+ value = obj.m_adjust_value(value);
+ rational value0 = ms.get_lower();
+ TRACE("opt", tout << "value " << value << " " << value0 << "\n";);
+ SASSERT(value == value0);
+ }
+ }
+ }
+
void context::validate_lex() {
rational r1;
expr_ref val(m);
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 18af756bf..461506258 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -190,7 +190,7 @@ namespace opt {
virtual void collect_statistics(statistics& stats) const;
virtual proof* get_proof() { return 0; }
virtual void get_labels(svector & r);
- virtual void get_unsat_core(ptr_vector & r) {}
+ virtual void get_unsat_core(ptr_vector & r);
virtual std::string reason_unknown() const;
virtual void set_reason_unknown(char const* msg) { m_unknown = msg; }
@@ -291,6 +291,7 @@ namespace opt {
void validate_lex();
+ void validate_maxsat(symbol const& id);
void display_benchmark();
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 0d0283232..42129be70 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -57,7 +57,7 @@ namespace opt {
opt_solver::~opt_solver() {
}
- void opt_solver::updt_params(params_ref & _p) {
+ void opt_solver::updt_params(params_ref const & _p) {
opt_params p(_p);
m_dump_benchmarks = p.dump_benchmarks();
m_params.updt_params(_p);
@@ -198,6 +198,10 @@ namespace opt {
return m_context.find_mutexes(vars, mutexes);
}
+ lbool opt_solver::preferred_sat(expr_ref_vector const& asms, vector& cores) {
+ return m_context.preferred_sat(asms, cores);
+ }
+
/**
@@ -379,13 +383,13 @@ namespace opt {
if (typeid(smt::theory_idl) == typeid(opt)) {
smt::theory_idl& th = dynamic_cast(opt);
- return th.mk_ge(m_fm, v, val.get_rational());
+ return th.mk_ge(m_fm, v, val);
}
if (typeid(smt::theory_rdl) == typeid(opt) &&
val.get_infinitesimal().is_zero()) {
smt::theory_rdl& th = dynamic_cast(opt);
- return th.mk_ge(m_fm, v, val.get_rational());
+ return th.mk_ge(m_fm, v, val);
}
// difference logic?
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index 16c2061c7..cdaad3cf2 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -88,7 +88,7 @@ namespace opt {
virtual ~opt_solver();
virtual solver* translate(ast_manager& m, params_ref const& p);
- virtual void updt_params(params_ref & p);
+ virtual void updt_params(params_ref const& p);
virtual void collect_param_descrs(param_descrs & r);
virtual void collect_statistics(statistics & st) const;
virtual void assert_expr(expr * t);
@@ -107,6 +107,7 @@ namespace opt {
virtual std::ostream& display(std::ostream & out) const;
virtual ast_manager& get_manager() const { return m; }
virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes);
+ virtual lbool preferred_sat(expr_ref_vector const& asms, vector& cores);
void set_logic(symbol const& logic);
smt::theory_var add_objective(app* term);
diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp
index d8ffe9f66..228e14cd6 100644
--- a/src/opt/wmax.cpp
+++ b/src/opt/wmax.cpp
@@ -32,64 +32,286 @@ namespace opt {
class wmax : public maxsmt_solver_base {
+ obj_map m_weights;
+ obj_map m_keys;
+ expr_ref_vector m_trail, m_defs;
+
+ void reset() {
+ m_weights.reset();
+ m_keys.reset();
+ m_trail.reset();
+ m_defs.reset();
+ }
+
public:
wmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft):
- maxsmt_solver_base(c, ws, soft) {}
+ maxsmt_solver_base(c, ws, soft),
+ m_trail(m),
+ m_defs(m) {}
+
virtual ~wmax() {}
lbool operator()() {
TRACE("opt", tout << "weighted maxsat\n";);
scoped_ensure_theory wth(*this);
obj_map soft;
+ reset();
lbool is_sat = find_mutexes(soft);
if (is_sat != l_true) {
return is_sat;
}
- rational offset = m_lower;
- m_upper = offset;
+ m_upper = m_lower;
bool was_sat = false;
- expr_ref_vector disj(m);
+ expr_ref_vector disj(m), asms(m);
+ vector cores;
obj_map::iterator it = soft.begin(), end = soft.end();
for (; it != end; ++it) {
- expr_ref tmp(m);
- bool is_true = m_model->eval(it->m_key, tmp) && m.is_true(tmp);
- expr* c = wth().assert_weighted(it->m_key, it->m_value, is_true);
- if (!is_true) {
+ expr* c = assert_weighted(wth(), it->m_key, it->m_value);
+ if (!is_true(it->m_key)) {
+ disj.push_back(m.mk_not(c));
m_upper += it->m_value;
- disj.push_back(c);
}
}
+ wth().init_min_cost(m_upper - m_lower);
s().assert_expr(mk_or(disj));
trace_bounds("wmax");
- while (l_true == is_sat && m_lower < m_upper) {
+
+ while (!m.canceled() && m_lower < m_upper) {
+ //mk_assumptions(asms);
+ //is_sat = s().preferred_sat(asms, cores);
is_sat = s().check_sat(0, 0);
if (m.canceled()) {
is_sat = l_undef;
}
+ if (is_sat == l_false) {
+ break;
+ }
if (is_sat == l_true) {
if (wth().is_optimal()) {
- m_upper = offset + wth().get_min_cost();
+ m_upper = m_lower + wth().get_cost();
s().get_model(m_model);
}
expr_ref fml = wth().mk_block();
+ //DEBUG_CODE(verify_cores(cores););
s().assert_expr(fml);
was_sat = true;
}
+ else {
+ //DEBUG_CODE(verify_cores(cores););
+ }
+ update_cores(wth(), cores);
+ wth().init_min_cost(m_upper - m_lower);
trace_bounds("wmax");
+ SASSERT(m_lower <= m_upper);
}
- if (was_sat) {
- wth().get_assignment(m_assignment);
- m_upper = offset + wth().get_min_cost();
- }
- if (is_sat == l_false && was_sat) {
+
+ update_assignment();
+
+ if (!m.canceled() && is_sat == l_undef && m_lower == m_upper) {
is_sat = l_true;
}
- if (is_sat == l_true) {
+ if (is_sat == l_false) {
+ is_sat = l_true;
m_lower = m_upper;
}
TRACE("opt", tout << "min cost: " << m_upper << "\n";);
return is_sat;
}
+
+ bool is_true(expr* e) {
+ expr_ref tmp(m);
+ return m_model->eval(e, tmp) && m.is_true(tmp);
+ }
+
+ void update_assignment() {
+ m_assignment.reset();
+ for (unsigned i = 0; i < m_soft.size(); ++i) {
+ m_assignment.push_back(is_true(m_soft[i]));
+ }
+ }
+
+ struct compare_asm {
+ wmax& max;
+ compare_asm(wmax& max):max(max) {}
+ bool operator()(expr* a, expr* b) const {
+ return max.m_weights[a] > max.m_weights[b];
+ }
+ };
+
+ void mk_assumptions(expr_ref_vector& asms) {
+ ptr_vector _asms;
+ obj_map::iterator it = m_weights.begin(), end = m_weights.end();
+ for (; it != end; ++it) {
+ _asms.push_back(it->m_key);
+ }
+ compare_asm comp(*this);
+ std::sort(_asms.begin(),_asms.end(), comp);
+ asms.reset();
+ for (unsigned i = 0; i < _asms.size(); ++i) {
+ asms.push_back(m.mk_not(_asms[i]));
+ }
+ }
+
+ void verify_cores(vector const& cores) {
+ for (unsigned i = 0; i < cores.size(); ++i) {
+ verify_core(cores[i]);
+ }
+ }
+
+ void verify_core(expr_ref_vector const& core) {
+ s().push();
+ s().assert_expr(core);
+ VERIFY(l_false == s().check_sat(0, 0));
+ s().pop(1);
+ }
+
+ void update_cores(smt::theory_wmaxsat& th, vector const& cores) {
+ obj_hashtable seen;
+ bool updated = false;
+ unsigned min_core_size = UINT_MAX;
+ for (unsigned i = 0; i < cores.size(); ++i) {
+ expr_ref_vector const& core = cores[i];
+ if (core.size() <= 20) {
+ s().assert_expr(m.mk_not(mk_and(core)));
+ }
+ min_core_size = std::min(core.size(), min_core_size);
+ if (core.size() >= 11) {
+ continue;
+ }
+ bool found = false;
+ for (unsigned j = 0; !found && j < core.size(); ++j) {
+ found = seen.contains(core[j]);
+ }
+ if (found) {
+ continue;
+ }
+ for (unsigned j = 0; j < core.size(); ++j) {
+ seen.insert(core[j]);
+ }
+ update_core(th, core);
+ updated = true;
+ }
+ // if no core was selected, then take the smallest cores.
+ for (unsigned i = 0; !updated && i < cores.size(); ++i) {
+ expr_ref_vector const& core = cores[i];
+ if (core.size() > min_core_size + 2) {
+ continue;
+ }
+ bool found = false;
+ for (unsigned j = 0; !found && j < core.size(); ++j) {
+ found = seen.contains(core[j]);
+ }
+ if (found) {
+ continue;
+ }
+ for (unsigned j = 0; j < core.size(); ++j) {
+ seen.insert(core[j]);
+ }
+ update_core(th, core);
+ }
+ }
+
+
+ rational remove_negations(smt::theory_wmaxsat& th, expr_ref_vector const& core, ptr_vector& keys, vector& weights) {
+ rational min_weight(-1);
+ for (unsigned i = 0; i < core.size(); ++i) {
+ expr* e;
+ VERIFY(m.is_not(core[i], e));
+ keys.push_back(m_keys[e]);
+ rational weight = m_weights[e];
+ if (i == 0 || weight < min_weight) {
+ min_weight = weight;
+ }
+ weights.push_back(weight);
+ m_weights.erase(e);
+ m_keys.erase(e);
+ th.disable_var(e);
+ }
+ for (unsigned i = 0; i < core.size(); ++i) {
+ rational weight = weights[i];
+ if (weight > min_weight) {
+ weight -= min_weight;
+ assert_weighted(th, keys[i], weight);
+ }
+ }
+ return min_weight;
+ }
+
+ // assert maxres clauses
+ // assert new core members with value of current model.
+ // update lower bound
+ // bounds get re-normalized when solver is invoked.
+ // each element of core is negated literal from theory_wmaxsat
+ // disable those literals from th
+
+ void update_core(smt::theory_wmaxsat& th, expr_ref_vector const& core) {
+ ptr_vector keys;
+ vector weights;
+ rational min_weight = remove_negations(th, core, keys, weights);
+ max_resolve(th, keys, min_weight);
+ m_lower += min_weight;
+ // std::cout << core << " " << min_weight << "\n";
+ }
+
+ void max_resolve(smt::theory_wmaxsat& th, ptr_vector const& core, rational const& w) {
+ SASSERT(!core.empty());
+ expr_ref fml(m), asum(m);
+ app_ref cls(m), d(m), dd(m);
+ //
+ // d_0 := true
+ // d_i := b_{i-1} and d_{i-1} for i = 1...sz-1
+ // soft (b_i or !d_i)
+ // == (b_i or !(!b_{i-1} or d_{i-1}))
+ // == (b_i or b_0 & b_1 & ... & b_{i-1})
+ //
+ // Soft constraint is satisfied if previous soft constraint
+ // holds or if it is the first soft constraint to fail.
+ //
+ // Soundness of this rule can be established using MaxRes
+ //
+ for (unsigned i = 1; i < core.size(); ++i) {
+ expr* b_i = core[i-1];
+ expr* b_i1 = core[i];
+ if (i == 1) {
+ d = to_app(b_i);
+ }
+ else if (i == 2) {
+ d = m.mk_and(b_i, d);
+ m_trail.push_back(d);
+ }
+ else {
+ dd = mk_fresh_bool("d");
+ fml = m.mk_implies(dd, d);
+ s().assert_expr(fml);
+ m_defs.push_back(fml);
+ fml = m.mk_implies(dd, b_i);
+ s().assert_expr(fml);
+ m_defs.push_back(fml);
+ fml = m.mk_and(d, b_i);
+ update_model(dd, fml);
+ d = dd;
+ }
+ cls = m.mk_or(b_i1, d);
+ m_trail.push_back(cls);
+ assert_weighted(th, cls, w);
+ }
+ }
+
+ expr* assert_weighted(smt::theory_wmaxsat& th, expr* key, rational const& w) {
+ expr* c = th.assert_weighted(key, w);
+ m_weights.insert(c, w);
+ m_keys.insert(c, key);
+ m_trail.push_back(c);
+ return c;
+ }
+
+ void update_model(expr* def, expr* value) {
+ expr_ref val(m);
+ if (m_model && m_model->eval(value, val, true)) {
+ m_model->register_decl(to_app(def)->get_decl(), val);
+ }
+ }
+
};
maxsmt_solver_base* mk_wmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) {
diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp
index f8f44b6d9..a010c4ae4 100644
--- a/src/qe/qe_arrays.cpp
+++ b/src/qe/qe_arrays.cpp
@@ -110,7 +110,7 @@ namespace qe {
imp(ast_manager& m): m(m), a(m) {}
~imp() {}
- virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
+ bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
return false;
}
diff --git a/src/qe/qe_datatypes.cpp b/src/qe/qe_datatypes.cpp
index aa67d28a3..8536e337f 100644
--- a/src/qe/qe_datatypes.cpp
+++ b/src/qe/qe_datatypes.cpp
@@ -37,7 +37,7 @@ namespace qe {
imp(ast_manager& m):
m(m), dt(m), m_val(m) {}
- virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
+ bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
return lift_foreign(vars, lits);
}
diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index eaedc470b..f4c0c9339 100644
--- a/src/qe/qe_mbp.cpp
+++ b/src/qe/qe_mbp.cpp
@@ -29,6 +29,7 @@ Revision History:
#include "model_v2_pp.h"
#include "expr_functors.h"
#include "for_each_expr.h"
+#include "model_evaluator.h"
using namespace qe;
@@ -125,6 +126,7 @@ class mbp::impl {
th_rewriter m_rw;
ptr_vector m_plugins;
expr_mark m_visited;
+ expr_mark m_bool_visited;
void add_plugin(project_plugin* p) {
family_id fid = p->get_family_id();
@@ -212,10 +214,12 @@ class mbp::impl {
}
}
-
- void extract_bools(model& model, expr_ref_vector& fmls, expr* fml) {
+ bool extract_bools(model_evaluator& eval, expr_ref_vector& fmls, expr* fml) {
TRACE("qe", tout << "extract bools: " << mk_pp(fml, m) << "\n";);
ptr_vector todo;
+ expr_safe_replace sub(m);
+ m_visited.reset();
+ bool found_bool = false;
if (is_app(fml)) {
todo.append(to_app(fml)->get_num_args(), to_app(fml)->get_args());
}
@@ -226,16 +230,16 @@ class mbp::impl {
continue;
}
m_visited.mark(e);
- if (m.is_bool(e)) {
- expr_ref val(m);
- VERIFY(model.eval(e, val));
+ if (m.is_bool(e) && !m.is_true(e) && !m.is_false(e)) {
+ expr_ref val = eval(e);
TRACE("qe", tout << "found: " << mk_pp(e, m) << "\n";);
- if (m.is_true(val)) {
- fmls.push_back(e);
- }
- else {
- fmls.push_back(mk_not(m, e));
+ SASSERT(m.is_true(val) || m.is_false(val));
+ if (!m_bool_visited.is_marked(e)) {
+ fmls.push_back(m.is_true(val) ? e : mk_not(m, e));
}
+ sub.insert(e, val);
+ m_bool_visited.mark(e);
+ found_bool = true;
}
else if (is_app(e)) {
todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
@@ -244,6 +248,14 @@ class mbp::impl {
TRACE("qe", tout << "expression not handled " << mk_pp(e, m) << "\n";);
}
}
+ if (found_bool) {
+ expr_ref tmp(m);
+ sub(fml, tmp);
+ expr_ref val = eval(tmp);
+ SASSERT(m.is_true(val) || m.is_false(val));
+ fmls.push_back(m.is_true(val) ? tmp : mk_not(m, tmp));
+ }
+ return found_bool;
}
void project_bools(model& model, app_ref_vector& vars, expr_ref_vector& fmls) {
@@ -294,6 +306,8 @@ public:
void extract_literals(model& model, expr_ref_vector& fmls) {
expr_ref val(m);
+ model_evaluator eval(model);
+ TRACE("qe", tout << fmls << "\n";);
for (unsigned i = 0; i < fmls.size(); ++i) {
expr* fml = fmls[i].get(), *nfml, *f1, *f2, *f3;
SASSERT(m.is_bool(fml));
@@ -303,7 +317,7 @@ public:
}
else if (m.is_or(fml)) {
for (unsigned j = 0; j < to_app(fml)->get_num_args(); ++j) {
- VERIFY (model.eval(to_app(fml)->get_arg(j), val));
+ val = eval(to_app(fml)->get_arg(j));
if (m.is_true(val)) {
fmls[i] = to_app(fml)->get_arg(j);
--i;
@@ -316,7 +330,7 @@ public:
project_plugin::erase(fmls, i);
}
else if (m.is_iff(fml, f1, f2) || (m.is_not(fml, nfml) && m.is_xor(nfml, f1, f2))) {
- VERIFY (model.eval(f1, val));
+ val = eval(f1);
if (m.is_false(val)) {
f1 = mk_not(m, f1);
f2 = mk_not(m, f2);
@@ -326,7 +340,7 @@ public:
--i;
}
else if (m.is_implies(fml, f1, f2)) {
- VERIFY (model.eval(f2, val));
+ val = eval(f2);
if (m.is_true(val)) {
fmls[i] = f2;
}
@@ -336,7 +350,7 @@ public:
--i;
}
else if (m.is_ite(fml, f1, f2, f3)) {
- VERIFY (model.eval(f1, val));
+ val = eval(f1);
if (m.is_true(val)) {
project_plugin::push_back(fmls, f1);
project_plugin::push_back(fmls, f2);
@@ -353,7 +367,7 @@ public:
}
else if (m.is_not(fml, nfml) && m.is_and(nfml)) {
for (unsigned j = 0; j < to_app(nfml)->get_num_args(); ++j) {
- VERIFY (model.eval(to_app(nfml)->get_arg(j), val));
+ val = eval(to_app(nfml)->get_arg(j));
if (m.is_false(val)) {
fmls[i] = mk_not(m, to_app(nfml)->get_arg(j));
--i;
@@ -368,7 +382,7 @@ public:
project_plugin::erase(fmls, i);
}
else if ((m.is_not(fml, nfml) && m.is_iff(nfml, f1, f2)) || m.is_xor(fml, f1, f2)) {
- VERIFY (model.eval(f1, val));
+ val = eval(f1);
if (m.is_true(val)) {
f2 = mk_not(m, f2);
}
@@ -385,7 +399,7 @@ public:
project_plugin::erase(fmls, i);
}
else if (m.is_not(fml, nfml) && m.is_ite(nfml, f1, f2, f3)) {
- VERIFY (model.eval(f1, val));
+ val = eval(f1);
if (m.is_true(val)) {
project_plugin::push_back(fmls, f1);
project_plugin::push_back(fmls, mk_not(m, f2));
@@ -397,14 +411,19 @@ public:
project_plugin::erase(fmls, i);
}
else if (m.is_not(fml, nfml)) {
- extract_bools(model, fmls, nfml);
+ if (extract_bools(eval, fmls, nfml)) {
+ project_plugin::erase(fmls, i);
+ }
}
else {
- extract_bools(model, fmls, fml);
+ if (extract_bools(eval, fmls, fml)) {
+ project_plugin::erase(fmls, i);
+ }
// TBD other Boolean operations.
}
}
- m_visited.reset();
+ TRACE("qe", tout << fmls << "\n";);
+ m_bool_visited.reset();
}
impl(ast_manager& m):m(m), m_rw(m) {
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 1bfd53597..841bdde9b 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -909,6 +909,7 @@ namespace qe {
num_scopes = 2;
}
else {
+ if (level.max() + 2 > m_level) return false;
SASSERT(level.max() + 2 <= m_level);
num_scopes = m_level - level.max();
SASSERT(num_scopes >= 2);
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 9cf13afe4..e6fa15a4c 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -2917,6 +2917,7 @@ namespace sat {
++max_weight;
out << "p wcnf " << num_vars() << " " << num_clauses() + sz << " " << max_weight << "\n";
+ out << "c soft " << sz << "\n";
for (unsigned i = 0; i < m_trail.size(); i++) {
out << max_weight << " " << dimacs_lit(m_trail[i]) << " 0\n";
@@ -2940,9 +2941,9 @@ namespace sat {
clause_vector::const_iterator end = cs.end();
for (; it != end; ++it) {
clause const & c = *(*it);
- unsigned sz = c.size();
+ unsigned clsz = c.size();
out << max_weight << " ";
- for (unsigned j = 0; j < sz; j++)
+ for (unsigned j = 0; j < clsz; j++)
out << dimacs_lit(c[j]) << " ";
out << "0\n";
}
@@ -2950,6 +2951,7 @@ namespace sat {
for (unsigned i = 0; i < sz; ++i) {
out << weights[i] << " " << lits[i] << " 0\n";
}
+ out.flush();
}
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index e56abc50c..e3a220cd2 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -115,10 +115,18 @@ public:
if (weights != 0) {
for (unsigned i = 0; i < sz; ++i) m_weights.push_back(weights[i]);
}
+ init_preprocess();
m_solver.pop_to_base_level();
dep2asm_t dep2asm;
+ expr_ref_vector asms(m);
+ for (unsigned i = 0; i < sz; ++i) {
+ expr_ref a(m.mk_fresh_const("s", m.mk_bool_sort()), m);
+ expr_ref fml(m.mk_implies(a, assumptions[i]), m);
+ assert_expr(fml);
+ asms.push_back(a);
+ }
VERIFY(l_true == internalize_formulas());
- VERIFY(l_true == internalize_assumptions(sz, assumptions, dep2asm));
+ VERIFY(l_true == internalize_assumptions(sz, asms.c_ptr(), dep2asm));
svector nweights;
for (unsigned i = 0; i < m_asms.size(); ++i) {
nweights.push_back((unsigned) m_weights[i]);
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 136921914..742a4fb1d 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -174,6 +174,7 @@ struct goal2sat::imp {
switch (to_app(t)->get_decl_kind()) {
case OP_NOT:
case OP_OR:
+ case OP_AND:
case OP_IFF:
m_frame_stack.push_back(frame(to_app(t), root, sign, 0));
return false;
@@ -185,7 +186,6 @@ struct goal2sat::imp {
}
convert_atom(t, root, sign);
return true;
- case OP_AND:
case OP_XOR:
case OP_IMPLIES:
case OP_DISTINCT: {
@@ -215,8 +215,8 @@ struct goal2sat::imp {
}
else {
mk_clause(m_result_stack.size(), m_result_stack.c_ptr());
- m_result_stack.reset();
}
+ m_result_stack.reset();
}
else {
SASSERT(num <= m_result_stack.size());
@@ -240,6 +240,48 @@ struct goal2sat::imp {
}
}
+ void convert_and(app * t, bool root, bool sign) {
+ TRACE("goal2sat", tout << "convert_and:\n" << mk_ismt2_pp(t, m) << "\n";);
+ unsigned num = t->get_num_args();
+ if (root) {
+ if (sign) {
+ for (unsigned i = 0; i < num; ++i) {
+ m_result_stack[i].neg();
+ }
+ }
+ else {
+ for (unsigned i = 0; i < num; ++i) {
+ mk_clause(m_result_stack[i]);
+ }
+ }
+ m_result_stack.reset();
+ }
+ else {
+ SASSERT(num <= m_result_stack.size());
+ sat::bool_var k = m_solver.mk_var();
+ sat::literal l(k, false);
+ m_cache.insert(t, l);
+ // l => /\ lits
+ sat::literal * lits = m_result_stack.end() - num;
+ for (unsigned i = 0; i < num; i++) {
+ mk_clause(~l, lits[i]);
+ }
+ // /\ lits => l
+ for (unsigned i = 0; i < num; ++i) {
+ m_result_stack[m_result_stack.size() - num + i].neg();
+ }
+ m_result_stack.push_back(l);
+ lits = m_result_stack.end() - num - 1;
+ mk_clause(num+1, lits);
+ unsigned old_sz = m_result_stack.size() - num - 1;
+ m_result_stack.shrink(old_sz);
+ if (sign)
+ l.neg();
+ m_result_stack.push_back(l);
+ }
+ }
+
+
void convert_ite(app * n, bool root, bool sign) {
unsigned sz = m_result_stack.size();
SASSERT(sz >= 3);
@@ -316,6 +358,9 @@ struct goal2sat::imp {
case OP_OR:
convert_or(t, root, sign);
break;
+ case OP_AND:
+ convert_and(t, root, sign);
+ break;
case OP_ITE:
convert_ite(t, root, sign);
break;
@@ -456,7 +501,6 @@ struct unsupported_bool_proc {
void operator()(app * n) {
if (n->get_family_id() == m.get_basic_family_id()) {
switch (n->get_decl_kind()) {
- case OP_AND:
case OP_XOR:
case OP_IMPLIES:
case OP_DISTINCT:
diff --git a/src/smt/proto_model/numeral_factory.cpp b/src/smt/proto_model/numeral_factory.cpp
index a67b6c075..49ff15167 100644
--- a/src/smt/proto_model/numeral_factory.cpp
+++ b/src/smt/proto_model/numeral_factory.cpp
@@ -31,7 +31,7 @@ arith_factory::arith_factory(ast_manager & m):
arith_factory::~arith_factory() {
}
-app * arith_factory::mk_value(rational const & val, bool is_int) {
+app * arith_factory::mk_num_value(rational const & val, bool is_int) {
return numeral_factory::mk_value(val, is_int ? m_util.mk_int() : m_util.mk_real());
}
@@ -47,6 +47,6 @@ app * bv_factory::mk_value_core(rational const & val, sort * s) {
return m_util.mk_numeral(val, s);
}
-app * bv_factory::mk_value(rational const & val, unsigned bv_size) {
+app * bv_factory::mk_num_value(rational const & val, unsigned bv_size) {
return numeral_factory::mk_value(val, m_util.mk_sort(bv_size));
}
diff --git a/src/smt/proto_model/numeral_factory.h b/src/smt/proto_model/numeral_factory.h
index 3c5d41040..9b1ff6a81 100644
--- a/src/smt/proto_model/numeral_factory.h
+++ b/src/smt/proto_model/numeral_factory.h
@@ -38,7 +38,7 @@ public:
arith_factory(ast_manager & m);
virtual ~arith_factory();
- app * mk_value(rational const & val, bool is_int);
+ app * mk_num_value(rational const & val, bool is_int);
};
class bv_factory : public numeral_factory {
@@ -50,7 +50,7 @@ public:
bv_factory(ast_manager & m);
virtual ~bv_factory();
- app * mk_value(rational const & val, unsigned bv_size);
+ app * mk_num_value(rational const & val, unsigned bv_size);
};
#endif /* NUMERAL_FACTORY_H_ */
diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
index c872a7139..9558f6a3b 100644
--- a/src/smt/smt_consequences.cpp
+++ b/src/smt/smt_consequences.cpp
@@ -56,36 +56,7 @@ namespace smt {
s.insert(lit.var());
}
else {
- b_justification js = get_justification(lit.var());
- switch (js.get_kind()) {
- case b_justification::CLAUSE: {
- clause * cls = js.get_clause();
- if (!cls) break;
- unsigned num_lits = cls->get_num_literals();
- for (unsigned j = 0; j < num_lits; ++j) {
- literal lit2 = cls->get_literal(j);
- if (lit2.var() != lit.var()) {
- s |= m_antecedents.find(lit2.var());
- }
- }
- break;
- }
- case b_justification::BIN_CLAUSE: {
- s |= m_antecedents.find(js.get_literal().var());
- break;
- }
- case b_justification::AXIOM: {
- break;
- }
- case b_justification::JUSTIFICATION: {
- literal_vector literals;
- m_conflict_resolution->justification2literals(js.get_justification(), literals);
- for (unsigned j = 0; j < literals.size(); ++j) {
- s |= m_antecedents.find(literals[j].var());
- }
- break;
- }
- }
+ justify(lit, s);
}
m_antecedents.insert(lit.var(), s);
TRACE("context", display_literal_verbose(tout, lit);
@@ -122,6 +93,39 @@ namespace smt {
}
}
+ void context::justify(literal lit, index_set& s) {
+ b_justification js = get_justification(lit.var());
+ switch (js.get_kind()) {
+ case b_justification::CLAUSE: {
+ clause * cls = js.get_clause();
+ if (!cls) break;
+ unsigned num_lits = cls->get_num_literals();
+ for (unsigned j = 0; j < num_lits; ++j) {
+ literal lit2 = cls->get_literal(j);
+ if (lit2.var() != lit.var()) {
+ s |= m_antecedents.find(lit2.var());
+ }
+ }
+ break;
+ }
+ case b_justification::BIN_CLAUSE: {
+ s |= m_antecedents.find(js.get_literal().var());
+ break;
+ }
+ case b_justification::AXIOM: {
+ break;
+ }
+ case b_justification::JUSTIFICATION: {
+ literal_vector literals;
+ m_conflict_resolution->justification2literals(js.get_justification(), literals);
+ for (unsigned j = 0; j < literals.size(); ++j) {
+ s |= m_antecedents.find(literals[j].var());
+ }
+ break;
+ }
+ }
+ }
+
void context::extract_fixed_consequences(unsigned& start, obj_map& vars, index_set const& assumptions, expr_ref_vector& conseq) {
pop_to_search_lvl();
SASSERT(!inconsistent());
@@ -369,6 +373,142 @@ namespace smt {
<< ")\n";
}
+ void context::extract_cores(expr_ref_vector const& asms, vector& cores, unsigned& min_core_size) {
+ index_set _asms, _nasms;
+ u_map var2expr;
+ for (unsigned i = 0; i < asms.size(); ++i) {
+ literal lit = get_literal(asms[i]);
+ _asms.insert(lit.index());
+ _nasms.insert((~lit).index());
+ var2expr.insert(lit.var(), asms[i]);
+ }
+
+ m_antecedents.reset();
+ literal_vector const& lits = assigned_literals();
+ for (unsigned i = 0; i < lits.size(); ++i) {
+ literal lit = lits[i];
+ index_set s;
+ if (_asms.contains(lit.index())) {
+ s.insert(lit.var());
+ }
+ else {
+ justify(lit, s);
+ }
+ m_antecedents.insert(lit.var(), s);
+ if (_nasms.contains(lit.index())) {
+ expr_ref_vector core(m_manager);
+ index_set::iterator it = s.begin(), end = s.end();
+ for (; it != end; ++it) {
+ core.push_back(var2expr[*it]);
+ }
+ core.push_back(var2expr[lit.var()]);
+ cores.push_back(core);
+ min_core_size = std::min(min_core_size, core.size());
+ }
+ }
+ }
+
+ void context::preferred_sat(literal_vector& lits) {
+ bool retry = true;
+ while (retry) {
+ retry = false;
+ for (unsigned i = 0; i < lits.size(); ++i) {
+ literal lit = lits[i];
+ if (lit == null_literal || get_assignment(lit) != l_undef) {
+ continue;
+ }
+ push_scope();
+ assign(lit, b_justification::mk_axiom(), true);
+ while (!propagate()) {
+ lits[i] = null_literal;
+ retry = true;
+ if (!resolve_conflict() || inconsistent()) {
+ SASSERT(inconsistent());
+ return;
+ }
+ }
+ }
+ }
+ }
+
+ void context::display_partial_assignment(std::ostream& out, expr_ref_vector const& asms, unsigned min_core_size) {
+ unsigned num_true = 0, num_false = 0, num_undef = 0;
+ for (unsigned i = 0; i < asms.size(); ++i) {
+ literal lit = get_literal(asms[i]);
+ if (get_assignment(lit) == l_false) {
+ ++num_false;
+ }
+ if (get_assignment(lit) == l_true) {
+ ++num_true;
+ }
+ if (get_assignment(lit) == l_undef) {
+ ++num_undef;
+ }
+ }
+ out << "(smt.preferred-sat true: " << num_true << " false: " << num_false << " undef: " << num_undef << " min core: " << min_core_size << ")\n";
+ }
+
+ lbool context::preferred_sat(expr_ref_vector const& asms, vector& cores) {
+ pop_to_base_lvl();
+ cores.reset();
+ setup_context(false);
+ internalize_assertions();
+ if (m_asserted_formulas.inconsistent() || inconsistent()) {
+ return l_false;
+ }
+ scoped_mk_model smk(*this);
+ init_search();
+ flet l(m_searching, true);
+ unsigned level = m_scope_lvl;
+ unsigned min_core_size = UINT_MAX;
+ lbool is_sat = l_true;
+ unsigned num_restarts = 0;
+
+ while (true) {
+ if (m_manager.canceled()) {
+ is_sat = l_undef;
+ break;
+ }
+ literal_vector lits;
+ for (unsigned i = 0; i < asms.size(); ++i) {
+ lits.push_back(get_literal(asms[i]));
+ }
+ preferred_sat(lits);
+ if (inconsistent()) {
+ SASSERT(m_scope_lvl == level);
+ is_sat = l_false;
+ break;
+ }
+ extract_cores(asms, cores, min_core_size);
+ IF_VERBOSE(1, display_partial_assignment(verbose_stream(), asms, min_core_size););
+
+ if (min_core_size <= 10) {
+ is_sat = l_undef;
+ break;
+ }
+
+ is_sat = bounded_search();
+ if (!restart(is_sat, level)) {
+ break;
+ }
+ ++num_restarts;
+ if (num_restarts >= min_core_size) {
+ is_sat = l_undef;
+ while (num_restarts <= 10*min_core_size) {
+ is_sat = bounded_search();
+ if (!restart(is_sat, level)) {
+ break;
+ }
+ ++num_restarts;
+ }
+ break;
+ }
+ }
+ end_search();
+
+ return check_finalize(is_sat);
+ }
+
struct neg_literal {
unsigned negate(unsigned i) {
return (~to_literal(i)).index();
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 6b3d92602..e6d4d0c07 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1111,6 +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;
+
theory_id t1 = r1->m_th_var_list.get_th_id();
if (t1 == null_theory_id) return false;
return get_theory(t1)->use_diseqs();
@@ -3293,19 +3295,6 @@ namespace smt {
m_num_conflicts_since_restart = 0;
}
- struct context::scoped_mk_model {
- context & m_ctx;
- scoped_mk_model(context & ctx):m_ctx(ctx) {
- m_ctx.m_proto_model = 0;
- m_ctx.m_model = 0;
- }
- ~scoped_mk_model() {
- if (m_ctx.m_proto_model.get() != 0) {
- m_ctx.m_model = m_ctx.m_proto_model->mk_model();
- m_ctx.m_proto_model = 0; // proto_model is not needed anymore.
- }
- }
- };
lbool context::search() {
#ifndef _EXTERNAL_RELEASE
@@ -3333,79 +3322,10 @@ namespace smt {
TRACE("search_bug", tout << "status: " << status << ", inconsistent: " << inconsistent() << "\n";);
TRACE("assigned_literals_per_lvl", display_num_assigned_literals_per_lvl(tout);
tout << ", num_assigned: " << m_assigned_literals.size() << "\n";);
-
- if (m_last_search_failure != OK) {
- if (status != l_false) {
- // build candidate model before returning
- mk_proto_model(status);
- // status = l_undef;
- }
+
+ if (!restart(status, curr_lvl)) {
break;
}
-
- bool force_restart = false;
-
- if (status == l_false) {
- break;
- }
- else if (status == l_true) {
- SASSERT(!inconsistent());
- mk_proto_model(l_true);
- // possible outcomes DONE l_true, DONE l_undef, CONTINUE
- quantifier_manager::check_model_result cmr = m_qmanager->check_model(m_proto_model.get(), m_model_generator->get_root2value());
- if (cmr == quantifier_manager::SAT) {
- // done
- break;
- }
- if (cmr == quantifier_manager::UNKNOWN) {
- IF_VERBOSE(1, verbose_stream() << "(smt.giveup quantifiers)\n";);
- // giving up
- m_last_search_failure = QUANTIFIERS;
- status = l_undef;
- break;
- }
- status = l_undef;
- force_restart = true;
- }
-
- SASSERT(status == l_undef);
- inc_limits();
- if (force_restart || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) {
- SASSERT(!inconsistent());
- IF_VERBOSE(1, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations
- << " :decisions " << m_stats.m_num_decisions
- << " :conflicts " << m_stats.m_num_conflicts << " :restart " << m_restart_threshold;
- if (m_fparams.m_restart_strategy == RS_IN_OUT_GEOMETRIC) {
- verbose_stream() << " :restart-outer " << m_restart_outer_threshold;
- }
- if (m_fparams.m_restart_adaptive) {
- verbose_stream() << " :agility " << m_agility;
- }
- verbose_stream() << ")" << std::endl; verbose_stream().flush(););
- // execute the restart
- m_stats.m_num_restarts++;
- if (m_scope_lvl > curr_lvl) {
- pop_scope(m_scope_lvl - curr_lvl);
- SASSERT(at_search_level());
- }
- ptr_vector::iterator it = m_theory_set.begin();
- ptr_vector::iterator end = m_theory_set.end();
- for (; it != end && !inconsistent(); ++it)
- (*it)->restart_eh();
- TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";);
- if (!inconsistent()) {
- m_qmanager->restart_eh();
- }
- if (inconsistent()) {
- VERIFY(!resolve_conflict());
- status = l_false;
- break;
- }
- }
- if (m_fparams.m_simplify_clauses)
- simplify_clauses();
- if (m_fparams.m_lemma_gc_strategy == LGC_AT_RESTART)
- del_inactive_lemmas();
}
TRACE("search_lite", tout << "status: " << status << "\n";);
@@ -3419,6 +3339,80 @@ namespace smt {
end_search();
return status;
}
+
+ bool context::restart(lbool& status, unsigned curr_lvl) {
+
+ if (m_last_search_failure != OK) {
+ if (status != l_false) {
+ // build candidate model before returning
+ mk_proto_model(status);
+ // status = l_undef;
+ }
+ return false;
+ }
+
+ if (status == l_false) {
+ return false;
+ }
+ if (status == l_true) {
+ SASSERT(!inconsistent());
+ mk_proto_model(l_true);
+ // possible outcomes DONE l_true, DONE l_undef, CONTINUE
+ quantifier_manager::check_model_result cmr = m_qmanager->check_model(m_proto_model.get(), m_model_generator->get_root2value());
+ if (cmr == quantifier_manager::SAT) {
+ // done
+ status = l_true;
+ return false;
+ }
+ if (cmr == quantifier_manager::UNKNOWN) {
+ IF_VERBOSE(1, verbose_stream() << "(smt.giveup quantifiers)\n";);
+ // giving up
+ m_last_search_failure = QUANTIFIERS;
+ status = l_undef;
+ return false;
+ }
+ }
+ inc_limits();
+ if (status == l_true || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) {
+ SASSERT(!inconsistent());
+ IF_VERBOSE(1, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations
+ << " :decisions " << m_stats.m_num_decisions
+ << " :conflicts " << m_stats.m_num_conflicts << " :restart " << m_restart_threshold;
+ if (m_fparams.m_restart_strategy == RS_IN_OUT_GEOMETRIC) {
+ verbose_stream() << " :restart-outer " << m_restart_outer_threshold;
+ }
+ if (m_fparams.m_restart_adaptive) {
+ verbose_stream() << " :agility " << m_agility;
+ }
+ verbose_stream() << ")" << std::endl; verbose_stream().flush(););
+ // execute the restart
+ m_stats.m_num_restarts++;
+ if (m_scope_lvl > curr_lvl) {
+ pop_scope(m_scope_lvl - curr_lvl);
+ SASSERT(at_search_level());
+ }
+ ptr_vector::iterator it = m_theory_set.begin();
+ ptr_vector::iterator end = m_theory_set.end();
+ for (; it != end && !inconsistent(); ++it)
+ (*it)->restart_eh();
+ TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";);
+ if (!inconsistent()) {
+ m_qmanager->restart_eh();
+ }
+ if (inconsistent()) {
+ VERIFY(!resolve_conflict());
+ status = l_false;
+ return false;
+ }
+ }
+ if (m_fparams.m_simplify_clauses)
+ simplify_clauses();
+ if (m_fparams.m_lemma_gc_strategy == LGC_AT_RESTART)
+ del_inactive_lemmas();
+
+ status = l_undef;
+ return true;
+ }
void context::tick(unsigned & counter) const {
counter++;
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 21d628e1a..c63d0614d 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -200,7 +200,20 @@ namespace smt {
model_ref m_model;
std::string m_unknown;
void mk_proto_model(lbool r);
- struct scoped_mk_model;
+ struct scoped_mk_model {
+ context & m_ctx;
+ scoped_mk_model(context & ctx):m_ctx(ctx) {
+ m_ctx.m_proto_model = 0;
+ m_ctx.m_model = 0;
+ }
+ ~scoped_mk_model() {
+ if (m_ctx.m_proto_model.get() != 0) {
+ m_ctx.m_model = m_ctx.m_proto_model->mk_model();
+ m_ctx.m_proto_model = 0; // proto_model is not needed anymore.
+ }
+ }
+ };
+
// -----------------------------------
//
@@ -234,7 +247,6 @@ namespace smt {
return m_params;
}
-
bool get_cancel_flag() { return !m_manager.limit().inc(); }
region & get_region() {
@@ -1056,6 +1068,8 @@ namespace smt {
void inc_limits();
+ bool restart(lbool& status, unsigned curr_lvl);
+
void tick(unsigned & counter) const;
lbool bounded_search();
@@ -1367,6 +1381,13 @@ namespace smt {
void validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars,
expr_ref_vector const& conseq, expr_ref_vector const& unfixed);
+ void justify(literal lit, index_set& s);
+
+ void extract_cores(expr_ref_vector const& asms, vector& cores, unsigned& min_core_size);
+
+ void preferred_sat(literal_vector& literals);
+
+ void display_partial_assignment(std::ostream& out, expr_ref_vector const& asms, unsigned min_core_size);
public:
context(ast_manager & m, smt_params & fp, params_ref const & p = params_ref());
@@ -1410,6 +1431,8 @@ namespace smt {
lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed);
lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes);
+
+ lbool preferred_sat(expr_ref_vector const& asms, vector& cores);
lbool setup_and_check(bool reset_cancel = true);
diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp
index 6b626c2de..5e3b091bc 100644
--- a/src/smt/smt_context_inv.cpp
+++ b/src/smt/smt_context_inv.cpp
@@ -322,6 +322,9 @@ namespace smt {
bool context::check_th_diseq_propagation() const {
TRACE("check_th_diseq_propagation", tout << "m_propagated_th_diseqs.size() " << m_propagated_th_diseqs.size() << "\n";);
int num = get_num_bool_vars();
+ if (inconsistent()) {
+ return true;
+ }
for (bool_var v = 0; v < num; v++) {
if (has_enode(v)) {
enode * n = bool_var2enode(v);
diff --git a/src/smt/smt_context_stat.cpp b/src/smt/smt_context_stat.cpp
index 5e82923f0..3838a88b5 100644
--- a/src/smt/smt_context_stat.cpp
+++ b/src/smt/smt_context_stat.cpp
@@ -32,7 +32,7 @@ namespace smt {
return static_cast(acc / m_lemmas.size());
}
- void acc_num_occs(clause * cls, unsigned_vector & lit2num_occs) {
+ static void acc_num_occs(clause * cls, unsigned_vector & lit2num_occs) {
unsigned num_lits = cls->get_num_literals();
for (unsigned i = 0; i < num_lits; i++) {
literal l = cls->get_literal(i);
@@ -40,7 +40,7 @@ namespace smt {
}
}
- void acc_num_occs(clause_vector const & v, unsigned_vector & lit2num_occs) {
+ static void acc_num_occs(clause_vector const & v, unsigned_vector & lit2num_occs) {
clause_vector::const_iterator it = v.begin();
clause_vector::const_iterator end = v.end();
for (; it != end; ++it)
@@ -79,7 +79,7 @@ namespace smt {
out << (m_assigned_literals.size() - n) << "]";
}
- void acc_var_num_occs(clause * cls, unsigned_vector & var2num_occs) {
+ static void acc_var_num_occs(clause * cls, unsigned_vector & var2num_occs) {
unsigned num_lits = cls->get_num_literals();
for (unsigned i = 0; i < num_lits; i++) {
literal l = cls->get_literal(i);
@@ -87,7 +87,7 @@ namespace smt {
}
}
- void acc_var_num_occs(clause_vector const & v, unsigned_vector & var2num_occs) {
+ static void acc_var_num_occs(clause_vector const & v, unsigned_vector & var2num_occs) {
clause_vector::const_iterator it = v.begin();
clause_vector::const_iterator end = v.end();
for (; it != end; ++it)
@@ -114,7 +114,7 @@ namespace smt {
out << "\n";
}
- void acc_var_num_min_occs(clause * cls, unsigned_vector & var2num_min_occs) {
+ static void acc_var_num_min_occs(clause * cls, unsigned_vector & var2num_min_occs) {
unsigned num_lits = cls->get_num_literals();
bool_var min_var = cls->get_literal(0).var();
for (unsigned i = 1; i < num_lits; i++) {
@@ -125,7 +125,7 @@ namespace smt {
var2num_min_occs[min_var]++;
}
- void acc_var_num_min_occs(clause_vector const & v, unsigned_vector & var2num_min_occs) {
+ static void acc_var_num_min_occs(clause_vector const & v, unsigned_vector & var2num_min_occs) {
clause_vector::const_iterator it = v.begin();
clause_vector::const_iterator end = v.end();
for (; it != end; ++it)
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 8028feae6..ad1e55ba6 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -335,7 +335,7 @@ namespace smt {
}
}
- bool find_arg(app * n, expr * t, expr * & other) {
+ static bool find_arg(app * n, expr * t, expr * & other) {
SASSERT(n->get_num_args() == 2);
if (n->get_arg(0) == t) {
other = n->get_arg(1);
@@ -348,7 +348,7 @@ namespace smt {
return false;
}
- bool check_args(app * n, expr * t1, expr * t2) {
+ static bool check_args(app * n, expr * t1, expr * t2) {
SASSERT(n->get_num_args() == 2);
return (n->get_arg(0) == t1 && n->get_arg(1) == t2) || (n->get_arg(1) == t1 && n->get_arg(0) == t2);
}
diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp
index df39b4186..9bdf962ec 100644
--- a/src/smt/smt_kernel.cpp
+++ b/src/smt/smt_kernel.cpp
@@ -115,6 +115,11 @@ namespace smt {
return m_kernel.get_consequences(assumptions, vars, conseq, unfixed);
}
+ lbool preferred_sat(expr_ref_vector const& asms, vector& cores) {
+ return m_kernel.preferred_sat(asms, cores);
+ }
+
+
lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) {
return m_kernel.find_mutexes(vars, mutexes);
}
@@ -282,6 +287,10 @@ namespace smt {
return m_imp->get_consequences(assumptions, vars, conseq, unfixed);
}
+ lbool kernel::preferred_sat(expr_ref_vector const& asms, vector& cores) {
+ return m_imp->preferred_sat(asms, cores);
+ }
+
lbool kernel::find_mutexes(expr_ref_vector const& vars, vector& mutexes) {
return m_imp->find_mutexes(vars, mutexes);
}
diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h
index ea09081ec..264fae011 100644
--- a/src/smt/smt_kernel.h
+++ b/src/smt/smt_kernel.h
@@ -133,11 +133,16 @@ namespace smt {
lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars,
expr_ref_vector& conseq, expr_ref_vector& unfixed);
- /*
+ /**
\brief find mutually exclusive variables.
*/
lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes);
+ /**
+ \brief Preferential SAT.
+ */
+ lbool preferred_sat(expr_ref_vector const& asms, vector& cores);
+
/**
\brief Return the model associated with the last check command.
*/
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index a7f415aad..5329cd80f 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -363,9 +363,6 @@ namespace smt {
}
}
- struct scoped_set_relevancy {
- };
-
bool model_checker::check(proto_model * md, obj_map const & root2value) {
SASSERT(md != 0);
m_root2value = &root2value;
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index b8320f329..ff84992e1 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -498,7 +498,7 @@ namespace smt {
m_bvsimp = static_cast(s.get_plugin(m.mk_family_id("bv")));
}
- ~auf_solver() {
+ virtual ~auf_solver() {
flush_nodes();
reset_eval_cache();
}
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 9f7656471..ee92c4f61 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -188,7 +188,7 @@ namespace smt {
}
}
- void check_no_arithmetic(static_features const & st, char const * logic) {
+ static void check_no_arithmetic(static_features const & st, char const * logic) {
if (st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0)
throw default_exception("Benchmark constains arithmetic, but specified loging does not support it.");
}
@@ -231,21 +231,21 @@ namespace smt {
(st.m_num_arith_eqs + st.m_num_arith_ineqs) > st.m_num_uninterpreted_constants * 9;
}
- bool is_in_diff_logic(static_features const & st) {
+ static bool is_in_diff_logic(static_features const & st) {
return
st.m_num_arith_eqs == st.m_num_diff_eqs &&
st.m_num_arith_terms == st.m_num_diff_terms &&
st.m_num_arith_ineqs == st.m_num_diff_ineqs;
}
- bool is_diff_logic(static_features const & st) {
+ static bool is_diff_logic(static_features const & st) {
return
is_in_diff_logic(st) &&
(st.m_num_diff_ineqs > 0 || st.m_num_diff_eqs > 0 || st.m_num_diff_terms > 0)
;
}
- void check_no_uninterpreted_functions(static_features const & st, char const * logic) {
+ static void check_no_uninterpreted_functions(static_features const & st, char const * logic) {
if (st.m_num_uninterpreted_functions != 0)
throw default_exception("Benchmark contains uninterpreted function symbols, but specified logic does not support them.");
}
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 39f991c72..5a0f8db95 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -1080,7 +1080,7 @@ namespace smt {
virtual inf_eps_rational maximize(theory_var v, expr_ref& blocker, bool& has_shared);
virtual inf_eps_rational value(theory_var v);
virtual theory_var add_objective(app* term);
- virtual expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_numeral const& val);
+ expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_numeral const& val);
void enable_record_conflict(expr* bound);
void record_conflict(unsigned num_lits, literal const * lits,
unsigned num_eqs, enode_pair const * eqs,
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index 50bfee20e..de357c8d3 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -417,8 +417,8 @@ namespace smt {
template
void theory_arith::atom::display(theory_arith const& th, std::ostream& out) const {
literal l(get_bool_var(), !m_is_true);
- out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << get_k() << " ";
- out << l << ":";
+ // out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << get_k() << " ";
+ // out << l << ":";
th.get_context().display_detailed_literal(out, l);
}
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 07d30222b..a8d771d1a 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -1069,7 +1069,7 @@ namespace smt {
template
void theory_arith::flush_bound_axioms() {
- CTRACE("arith", !m_new_atoms.empty(), tout << "flush bound axioms\n";);
+ CTRACE("arith_verbose", !m_new_atoms.empty(), tout << "flush bound axioms\n";);
while (!m_new_atoms.empty()) {
ptr_vector atoms;
@@ -1084,7 +1084,7 @@ namespace smt {
--i;
}
}
- CTRACE("arith", !atoms.empty(),
+ CTRACE("arith", atoms.size() > 1,
for (unsigned i = 0; i < atoms.size(); ++i) {
atoms[i]->display(*this, tout); tout << "\n";
});
@@ -1292,7 +1292,7 @@ namespace smt {
template
void theory_arith::assign_eh(bool_var v, bool is_true) {
- TRACE("arith", tout << "p" << v << " := " << (is_true?"true":"false") << "\n";);
+ TRACE("arith_verbose", tout << "p" << v << " := " << (is_true?"true":"false") << "\n";);
atom * a = get_bv2a(v);
if (!a) return;
SASSERT(get_context().get_assignment(a->get_bool_var()) != l_undef);
@@ -3043,12 +3043,14 @@ namespace smt {
m_stats.m_conflicts++;
m_num_conflicts++;
TRACE("arith_conflict",
+ tout << "scope: " << ctx.get_scope_level() << "\n";
for (unsigned i = 0; i < num_literals; i++) {
ctx.display_detailed_literal(tout, lits[i]);
tout << " ";
if (coeffs_enabled()) {
tout << "bound: " << bounds.lit_coeffs()[i] << "\n";
}
+ tout << "\n";
}
for (unsigned i = 0; i < num_eqs; i++) {
tout << "#" << eqs[i].first->get_owner_id() << "=#" << eqs[i].second->get_owner_id() << " ";
@@ -3229,7 +3231,7 @@ namespace smt {
TRACE("arith", tout << "Truncating non-integer value. This is possible for non-linear constraints v" << v << " " << num << "\n";);
num = floor(num);
}
- return alloc(expr_wrapper_proc, m_factory->mk_value(num, m_util.is_int(var2expr(v))));
+ return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, m_util.is_int(var2expr(v))));
}
// -----------------------------------
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index a53580b73..a886c8a1e 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -1583,7 +1583,7 @@ namespace smt {
#endif
get_fixed_value(v, val);
SASSERT(r);
- return alloc(expr_wrapper_proc, m_factory->mk_value(val, get_bv_size(v)));
+ return alloc(expr_wrapper_proc, m_factory->mk_num_value(val, get_bv_size(v)));
}
void theory_bv::display_var(std::ostream & out, theory_var v) const {
diff --git a/src/smt/theory_dense_diff_logic.h b/src/smt/theory_dense_diff_logic.h
index 1b1653eb7..c2be89bc3 100644
--- a/src/smt/theory_dense_diff_logic.h
+++ b/src/smt/theory_dense_diff_logic.h
@@ -198,7 +198,7 @@ namespace smt {
void del_vars(unsigned old_num_vars);
void init_model();
bool internalize_objective(expr * n, rational const& m, rational& r, objective_term & objective);
- expr_ref mk_ineq(theory_var v, inf_rational const& val, bool is_strict);
+ expr_ref mk_ineq(theory_var v, inf_eps const& val, bool is_strict);
#ifdef Z3DEBUG
bool check_vector_sizes() const;
bool check_matrix() const;
@@ -270,8 +270,8 @@ namespace smt {
virtual inf_eps_rational maximize(theory_var v, expr_ref& blocker, bool& has_shared);
virtual inf_eps_rational value(theory_var v);
virtual theory_var add_objective(app* term);
- virtual expr_ref mk_gt(theory_var v, inf_rational const& val);
- virtual expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_rational const& val);
+ virtual expr_ref mk_gt(theory_var v, inf_eps const& val);
+ expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val);
// -----------------------------------
//
diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h
index fd388b5bd..877d4f659 100644
--- a/src/smt/theory_dense_diff_logic_def.h
+++ b/src/smt/theory_dense_diff_logic_def.h
@@ -828,7 +828,7 @@ namespace smt {
SASSERT(v != null_theory_var);
numeral const & val = m_assignment[v];
rational num = val.get_rational().to_rational() + m_epsilon * val.get_infinitesimal().to_rational();
- return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int(v)));
+ return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, is_int(v)));
}
// TBD: code is common to both sparse and dense difference logic solvers.
@@ -1002,9 +1002,10 @@ namespace smt {
m_assignment[i] = a;
// TBD: if epsilon is != 0, then adjust a by some small fraction.
}
- blocker = mk_gt(v, r);
+ inf_eps result(rational(0), r);
+ blocker = mk_gt(v, result);
IF_VERBOSE(10, verbose_stream() << blocker << "\n";);
- return inf_eps(rational(0), r);
+ return result;
}
default:
TRACE("opt", tout << "unbounded\n"; );
@@ -1034,18 +1035,18 @@ namespace smt {
}
template
- expr_ref theory_dense_diff_logic::mk_gt(theory_var v, inf_rational const& val) {
+ expr_ref theory_dense_diff_logic::mk_gt(theory_var v, inf_eps const& val) {
return mk_ineq(v, val, true);
}
template
expr_ref theory_dense_diff_logic::mk_ge(
- filter_model_converter& fm, theory_var v, inf_rational const& val) {
+ filter_model_converter& fm, theory_var v, inf_eps const& val) {
return mk_ineq(v, val, false);
}
template
- expr_ref theory_dense_diff_logic::mk_ineq(theory_var v, inf_rational const& val, bool is_strict) {
+ expr_ref theory_dense_diff_logic::mk_ineq(theory_var v, inf_eps const& val, bool is_strict) {
ast_manager& m = get_manager();
objective_term const& t = m_objectives[v];
expr_ref e(m), f(m), f2(m);
diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h
index 6fb9e6454..f47e61548 100644
--- a/src/smt/theory_diff_logic.h
+++ b/src/smt/theory_diff_logic.h
@@ -324,14 +324,15 @@ namespace smt {
virtual inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared);
virtual inf_eps value(theory_var v);
virtual theory_var add_objective(app* term);
- virtual expr_ref mk_gt(theory_var v, inf_rational const& val);
- virtual expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_rational const& val);
+ expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val);
bool internalize_objective(expr * n, rational const& m, rational& r, objective_term & objective);
private:
- expr_ref mk_ineq(theory_var v, inf_rational const& val, bool is_strict);
+ expr_ref mk_gt(theory_var v, inf_eps const& val);
+
+ expr_ref mk_ineq(theory_var v, inf_eps const& val, bool is_strict);
virtual void new_eq_eh(theory_var v1, theory_var v2, justification& j);
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 98f94c6d2..372786c01 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -905,7 +905,7 @@ model_value_proc * theory_diff_logic::mk_value(enode * n, model_generator &
numeral val = m_graph.get_assignment(v);
rational num = val.get_rational().to_rational() + m_delta * val.get_infinitesimal().to_rational();
TRACE("arith", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";);
- return alloc(expr_wrapper_proc, m_factory->mk_value(num, m_util.is_int(n->get_owner())));
+ return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, m_util.is_int(n->get_owner())));
}
template
@@ -1242,7 +1242,8 @@ theory_diff_logic::maximize(theory_var v, expr_ref& blocker, bool& has_shar
rational r = rational(val.first) + m_delta*rational(val.second);
m_graph.set_assignment(i, numeral(r));
}
- blocker = mk_gt(v, r);
+ inf_eps r1(rational(0), r);
+ blocker = mk_gt(v, r1);
return inf_eps(rational(0), r + m_objective_consts[v]);
}
default:
@@ -1273,7 +1274,7 @@ theory_var theory_diff_logic::add_objective(app* term) {
}
template
-expr_ref theory_diff_logic::mk_ineq(theory_var v, inf_rational const& val, bool is_strict) {
+expr_ref theory_diff_logic::mk_ineq(theory_var v, inf_eps const& val, bool is_strict) {
ast_manager& m = get_manager();
objective_term const& t = m_objectives[v];
expr_ref e(m), f(m), f2(m);
@@ -1304,7 +1305,7 @@ expr_ref theory_diff_logic::mk_ineq(theory_var v, inf_rational const& val,
return f;
}
- inf_rational new_val = val; // - inf_rational(m_objective_consts[v]);
+ inf_eps new_val = val; // - inf_rational(m_objective_consts[v]);
e = m_util.mk_numeral(new_val.get_rational(), m.get_sort(f));
if (new_val.get_infinitesimal().is_neg()) {
@@ -1328,12 +1329,12 @@ expr_ref theory_diff_logic::mk_ineq(theory_var v, inf_rational const& val,
}
template
-expr_ref theory_diff_logic::mk_gt(theory_var v, inf_rational const& val) {
+expr_ref theory_diff_logic::mk_gt(theory_var v, inf_eps const& val) {
return mk_ineq(v, val, true);
}
template
-expr_ref theory_diff_logic::mk_ge(filter_model_converter& fm, theory_var v, inf_rational const& val) {
+expr_ref theory_diff_logic::mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val) {
return mk_ineq(v, val, false);
}
diff --git a/src/smt/theory_opt.h b/src/smt/theory_opt.h
index 58e039140..421e6feca 100644
--- a/src/smt/theory_opt.h
+++ b/src/smt/theory_opt.h
@@ -33,7 +33,6 @@ namespace smt {
virtual inf_eps value(theory_var) = 0;
virtual inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared) = 0;
virtual theory_var add_objective(app* term) = 0;
- virtual expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val) { UNREACHABLE(); return expr_ref(*((ast_manager*)0)); }
bool is_linear(ast_manager& m, expr* term);
bool is_numeral(arith_util& a, expr* term);
};
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 245ffe438..ed95ef8d7 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2235,8 +2235,9 @@ bool theory_seq::add_stoi_axiom(expr* e) {
context& ctx = get_context();
expr* n;
rational val;
+ TRACE("seq", tout << mk_pp(e, m) << "\n";);
VERIFY(m_util.str.is_stoi(e, n));
- if (get_value(e, val) && !m_stoi_axioms.contains(val)) {
+ if (get_num_value(e, val) && !m_stoi_axioms.contains(val)) {
m_stoi_axioms.insert(val);
if (!val.is_minus_one()) {
app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m);
@@ -2252,15 +2253,72 @@ bool theory_seq::add_stoi_axiom(expr* e) {
return true;
}
}
+ if (upper_bound(n, val) && get_length(n, val) && val.is_pos() && !m_stoi_axioms.contains(val)) {
+ zstring s;
+ SASSERT(val.is_unsigned());
+ unsigned sz = val.get_unsigned();
+ expr_ref len1(m), len2(m), ith_char(m), num(m), coeff(m);
+ expr_ref_vector nums(m);
+ len1 = m_util.str.mk_length(n);
+ len2 = m_autil.mk_int(sz);
+ literal lit = mk_eq(len1, len2, false);
+ literal_vector lits;
+ lits.push_back(~lit);
+ for (unsigned i = 0; i < sz; ++i) {
+ ith_char = mk_nth(n, m_autil.mk_int(i));
+ lits.push_back(~is_digit(ith_char));
+ nums.push_back(digit2int(ith_char));
+ }
+ for (unsigned i = sz-1, c = 1; i > 0; c *= 10) {
+ --i;
+ coeff = m_autil.mk_int(c);
+ nums[i] = m_autil.mk_mul(coeff, nums[i].get());
+ }
+ num = m_autil.mk_add(nums.size(), nums.c_ptr());
+ lits.push_back(mk_eq(e, num, false));
+ ++m_stats.m_add_axiom;
+ m_new_propagation = true;
+ for (unsigned i = 0; i < lits.size(); ++i) {
+ ctx.mark_as_relevant(lits[i]);
+ }
+ ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
+ m_stoi_axioms.insert(val);
+ m_trail_stack.push(insert_map(m_stoi_axioms, val));
+ m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));
+ return true;
+ }
+
return false;
}
+literal theory_seq::is_digit(expr* ch) {
+ bv_util bv(m);
+ literal isd = mk_literal(mk_skolem(symbol("seq.is_digit"), ch, 0, 0, m.mk_bool_sort()));
+ expr_ref d2i = digit2int(ch);
+ expr_ref _lo(bv.mk_ule(bv.mk_numeral(rational('0'), bv.mk_sort(8)), ch), m);
+ expr_ref _hi(bv.mk_ule(ch, bv.mk_numeral(rational('9'), bv.mk_sort(8))), m);
+ literal lo = mk_literal(_lo);
+ literal hi = mk_literal(_hi);
+ add_axiom(~lo, ~hi, isd);
+ add_axiom(~isd, lo);
+ add_axiom(~isd, hi);
+ for (unsigned i = 0; i < 10; ++i) {
+ add_axiom(~mk_eq(ch, bv.mk_numeral(rational('0'+i), bv.mk_sort(8)), false), mk_eq(d2i, m_autil.mk_int(i), false));
+ }
+ return isd;
+}
+
+expr_ref theory_seq::digit2int(expr* ch) {
+ return expr_ref(mk_skolem(symbol("seq.digit2int"), ch, 0, 0, m_autil.mk_int()), m);
+}
+
bool theory_seq::add_itos_axiom(expr* e) {
context& ctx = get_context();
rational val;
expr* n;
+ TRACE("seq", tout << mk_pp(e, m) << "\n";);
VERIFY(m_util.str.is_itos(e, n));
- if (get_value(n, val)) {
+ if (get_num_value(n, val)) {
if (!m_itos_axioms.contains(val)) {
m_itos_axioms.insert(val);
app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m);
@@ -2282,6 +2340,9 @@ bool theory_seq::add_itos_axiom(expr* e) {
else {
// stoi(itos(n)) = n
app_ref e2(m_util.str.mk_stoi(e), m);
+ if (ctx.e_internalized(e2) && ctx.get_enode(e2)->get_root() == ctx.get_enode(n)->get_root()) {
+ return false;
+ }
add_axiom(mk_eq(e2, n, false));
m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));
return true;
@@ -2464,22 +2525,27 @@ void theory_seq::init_model(model_generator & mg) {
class theory_seq::seq_value_proc : public model_value_proc {
+ enum source_t { unit_source, int_source, string_source };
theory_seq& th;
sort* m_sort;
svector m_dependencies;
ptr_vector m_strings;
- svector m_source;
+ svector m_source;
public:
seq_value_proc(theory_seq& th, sort* s): th(th), m_sort(s) {
}
virtual ~seq_value_proc() {}
- void add_dependency(enode* n) {
+ void add_unit(enode* n) {
m_dependencies.push_back(model_value_dependency(n));
- m_source.push_back(true);
+ m_source.push_back(unit_source);
+ }
+ void add_int(enode* n) {
+ m_dependencies.push_back(model_value_dependency(n));
+ m_source.push_back(int_source);
}
void add_string(expr* n) {
m_strings.push_back(n);
- m_source.push_back(false);
+ m_source.push_back(string_source);
}
virtual void get_dependencies(buffer & result) {
result.append(m_dependencies.size(), m_dependencies.c_ptr());
@@ -2504,11 +2570,13 @@ public:
unsigned sz;
for (unsigned i = 0; i < m_source.size(); ++i) {
- if (m_source[i]) {
+ switch (m_source[i]) {
+ case unit_source: {
VERIFY(bv.is_numeral(values[j++], val, sz));
sbuffer.push_back(val.get_unsigned());
+ break;
}
- else {
+ case string_source: {
dependency* deps = 0;
expr_ref tmp = th.canonize(m_strings[k], deps);
zstring zs;
@@ -2519,17 +2587,34 @@ public:
TRACE("seq", tout << "Not a string: " << tmp << "\n";);
}
++k;
+ break;
+ }
+ case int_source: {
+ std::ostringstream strm;
+ arith_util arith(th.m);
+ VERIFY(arith.is_numeral(values[j++], val));
+ if (val.is_neg()) strm << "-";
+ strm << abs(val);
+ zstring zs(strm.str().c_str());
+ add_buffer(sbuffer, zs);
+ break;
+ }
}
}
result = th.m_util.str.mk_string(zstring(sbuffer.size(), sbuffer.c_ptr()));
}
else {
for (unsigned i = 0; i < m_source.size(); ++i) {
- if (m_source[i]) {
+ switch (m_source[i]) {
+ case unit_source:
args.push_back(th.m_util.str.mk_unit(values[j++]));
- }
- else {
+ break;
+ case string_source:
args.push_back(m_strings[k++]);
+ break;
+ case int_source:
+ UNREACHABLE();
+ break;
}
}
result = th.mk_concat(args, m_sort);
@@ -2567,7 +2652,12 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
TRACE("seq", tout << mk_pp(c, m) << "\n";);
if (m_util.str.is_unit(c, c1)) {
if (ctx.e_internalized(c1)) {
- sv->add_dependency(ctx.get_enode(c1));
+ sv->add_unit(ctx.get_enode(c1));
+ }
+ }
+ else if (m_util.str.is_itos(c, c1)) {
+ if (ctx.e_internalized(c1)) {
+ sv->add_int(ctx.get_enode(c1));
}
}
else if (m_util.str.is_string(c)) {
@@ -2741,7 +2831,8 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
}
else if (m_util.str.is_itos(e, e1)) {
rational val;
- if (get_value(e1, val)) {
+ TRACE("seq", tout << mk_pp(e, m) << "\n";);
+ if (get_num_value(e1, val)) {
TRACE("seq", tout << mk_pp(e, m) << " -> " << val << "\n";);
expr_ref num(m), res(m);
num = m_autil.mk_numeral(val, true);
@@ -2916,7 +3007,7 @@ void theory_seq::add_indexof_axiom(expr* i) {
expr_ref len_t(m_util.str.mk_length(t), m);
literal offset_ge_len = mk_literal(m_autil.mk_ge(mk_sub(offset, len_t), zero));
- add_axiom(offset_ge_len, mk_eq(i, minus_one, false));
+ add_axiom(~offset_ge_len, mk_eq(i, minus_one, false));
expr_ref x = mk_skolem(m_indexof_left, t, s, offset);
expr_ref y = mk_skolem(m_indexof_right, t, s, offset);
@@ -3024,7 +3115,7 @@ void theory_seq::add_itos_length_axiom(expr* len) {
unsigned num_char1 = 1, num_char2 = 1;
rational len1, len2;
rational ten(10);
- if (get_value(n, len1)) {
+ if (get_num_value(n, len1)) {
bool neg = len1.is_neg();
if (neg) len1.neg();
num_char1 = neg?2:1;
@@ -3038,7 +3129,7 @@ void theory_seq::add_itos_length_axiom(expr* len) {
}
SASSERT(len1 <= upper);
}
- if (get_value(len, len2) && len2.is_unsigned()) {
+ if (get_num_value(len, len2) && len2.is_unsigned()) {
num_char2 = len2.get_unsigned();
}
unsigned num_char = std::max(num_char1, num_char2);
@@ -3172,18 +3263,17 @@ static theory_mi_arith* get_th_arith(context& ctx, theory_id afid, expr* e) {
}
}
-bool theory_seq::get_value(expr* e, rational& val) const {
+bool theory_seq::get_num_value(expr* e, rational& val) const {
context& ctx = get_context();
theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e);
expr_ref _val(m);
if (!tha) return false;
- enode* next = ctx.get_enode(e), *n;
+ enode* next = ctx.get_enode(e), *n = next;
do {
- n = next;
- if (tha->get_value(n, _val) && m_autil.is_numeral(_val, val) && val.is_int()) {
+ if (tha->get_value(next, _val) && m_autil.is_numeral(_val, val) && val.is_int()) {
return true;
}
- next = n->get_next();
+ next = next->get_next();
}
while (next != n);
return false;
@@ -3692,7 +3782,10 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
else if (is_skolem(symbol("seq.split"), e)) {
// propagate equalities
}
+ else if (is_skolem(symbol("seq.is_digit"), e)) {
+ }
else {
+ TRACE("seq", tout << mk_pp(e, m) << "\n";);
UNREACHABLE();
}
}
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 21955bf30..aa7ddec1b 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -499,6 +499,8 @@ namespace smt {
void add_in_re_axiom(expr* n);
bool add_stoi_axiom(expr* n);
bool add_itos_axiom(expr* n);
+ literal is_digit(expr* ch);
+ expr_ref digit2int(expr* ch);
void add_itos_length_axiom(expr* n);
literal mk_literal(expr* n);
literal mk_eq_empty(expr* n, bool phase = true);
@@ -512,7 +514,7 @@ namespace smt {
// arithmetic integration
- bool get_value(expr* s, rational& val) const;
+ bool get_num_value(expr* s, rational& val) const;
bool lower_bound(expr* s, rational& lo) const;
bool upper_bound(expr* s, rational& hi) const;
bool get_length(expr* s, rational& val) const;
diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h
index ff295d5a3..5f370c29c 100644
--- a/src/smt/theory_utvpi_def.h
+++ b/src/smt/theory_utvpi_def.h
@@ -901,7 +901,7 @@ namespace smt {
bool is_int = a.is_int(n->get_owner());
rational num = mk_value(v, is_int);
TRACE("utvpi", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";);
- return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int));
+ return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, is_int));
}
/**
diff --git a/src/smt/theory_wmaxsat.cpp b/src/smt/theory_wmaxsat.cpp
index fd07188e5..b665c2a94 100644
--- a/src/smt/theory_wmaxsat.cpp
+++ b/src/smt/theory_wmaxsat.cpp
@@ -21,294 +21,351 @@ Notes:
#include "smt_context.h"
#include "ast_pp.h"
#include "theory_wmaxsat.h"
+#include "smt_justification.h"
namespace smt {
-theory_wmaxsat::theory_wmaxsat(ast_manager& m, filter_model_converter& mc):
- theory(m.mk_family_id("weighted_maxsat")),
- m_mc(mc),
- m_vars(m),
- m_fmls(m),
- m_zweights(m_mpz),
- m_old_values(m_mpz),
- m_zcost(m_mpz),
- m_zmin_cost(m_mpz),
- m_found_optimal(false),
- m_propagate(false),
- m_normalize(false),
- m_den(1)
-{}
-
-theory_wmaxsat::~theory_wmaxsat() {
- m_old_values.reset();
-}
-
-/**
- \brief return the complement of variables that are currently assigned.
-*/
-void theory_wmaxsat::get_assignment(svector& result) {
- result.reset();
+ theory_wmaxsat::theory_wmaxsat(ast_manager& m, filter_model_converter& mc):
+ theory(m.mk_family_id("weighted_maxsat")),
+ m_mc(mc),
+ m_vars(m),
+ m_fmls(m),
+ m_zweights(m_mpz),
+ m_old_values(m_mpz),
+ m_zcost(m_mpz),
+ m_zmin_cost(m_mpz),
+ m_found_optimal(false),
+ m_propagate(false),
+ m_normalize(false),
+ m_den(1)
+ {}
- if (!m_found_optimal) {
- for (unsigned i = 0; i < m_vars.size(); ++i) {
- result.push_back(false);
- }
+ theory_wmaxsat::~theory_wmaxsat() {
+ m_old_values.reset();
}
- else {
- std::sort(m_cost_save.begin(), m_cost_save.end());
- for (unsigned i = 0,j = 0; i < m_vars.size(); ++i) {
- if (j < m_cost_save.size() && m_cost_save[j] == static_cast(i)) {
+
+ /**
+ \brief return the complement of variables that are currently assigned.
+ */
+ void theory_wmaxsat::get_assignment(svector& result) {
+ result.reset();
+
+ if (!m_found_optimal) {
+ for (unsigned i = 0; i < m_vars.size(); ++i) {
result.push_back(false);
- ++j;
- }
- else {
- result.push_back(true);
}
}
+ else {
+ std::sort(m_cost_save.begin(), m_cost_save.end());
+ for (unsigned i = 0,j = 0; i < m_vars.size(); ++i) {
+ if (j < m_cost_save.size() && m_cost_save[j] == static_cast(i)) {
+ result.push_back(false);
+ ++j;
+ }
+ else {
+ result.push_back(true);
+ }
+ }
+ }
+ TRACE("opt",
+ tout << "cost save: ";
+ for (unsigned i = 0; i < m_cost_save.size(); ++i) {
+ tout << m_cost_save[i] << " ";
+ }
+ tout << "\nvars: ";
+ for (unsigned i = 0; i < m_vars.size(); ++i) {
+ tout << mk_pp(m_vars[i].get(), get_manager()) << " ";
+ }
+ tout << "\nassignment: ";
+ for (unsigned i = 0; i < result.size(); ++i) {
+ tout << result[i] << " ";
+ }
+ tout << "\n";);
}
- TRACE("opt",
- tout << "cost save: ";
- for (unsigned i = 0; i < m_cost_save.size(); ++i) {
- tout << m_cost_save[i] << " ";
- }
- tout << "\nvars: ";
- for (unsigned i = 0; i < m_vars.size(); ++i) {
- tout << mk_pp(m_vars[i].get(), get_manager()) << " ";
- }
- tout << "\nassignment: ";
- for (unsigned i = 0; i < result.size(); ++i) {
- tout << result[i] << " ";
- }
- tout << "\n";);
-}
-
-void theory_wmaxsat::init_search_eh() {
- m_propagate = true;
-}
-
-expr* theory_wmaxsat::assert_weighted(expr* fml, rational const& w, bool is_true) {
- context & ctx = get_context();
- ast_manager& m = get_manager();
- app_ref var(m), wfml(m);
- var = m.mk_fresh_const("w", m.mk_bool_sort());
- m_mc.insert(var->get_decl());
- wfml = m.mk_or(var, fml);
- ctx.assert_expr(wfml);
- m_rweights.push_back(w);
- m_vars.push_back(var);
- m_fmls.push_back(fml);
- m_assigned.push_back(false);
- if (!is_true) {
- m_rmin_cost += w;
+ void theory_wmaxsat::init_search_eh() {
+ m_propagate = true;
}
- m_normalize = true;
- return ctx.bool_var2expr(register_var(var, true));
-}
-
-bool_var theory_wmaxsat::register_var(app* var, bool attach) {
- context & ctx = get_context();
- bool_var bv;
- SASSERT(!ctx.e_internalized(var));
- enode* x = ctx.mk_enode(var, false, true, true);
- if (ctx.b_internalized(var)) {
- bv = ctx.get_bool_var(var);
+
+ expr* theory_wmaxsat::assert_weighted(expr* fml, rational const& w) {
+ context & ctx = get_context();
+ ast_manager& m = get_manager();
+ app_ref var(m), wfml(m);
+ var = m.mk_fresh_const("w", m.mk_bool_sort());
+ m_mc.insert(var->get_decl());
+ wfml = m.mk_or(var, fml);
+ ctx.assert_expr(wfml);
+ m_rweights.push_back(w);
+ m_vars.push_back(var);
+ m_fmls.push_back(fml);
+ m_assigned.push_back(false);
+ m_enabled.push_back(true);
+ m_normalize = true;
+ bool_var bv = register_var(var, true);
+ TRACE("opt", tout << "enable: v" << m_bool2var[bv] << " b" << bv << " " << mk_pp(var, get_manager()) << "\n";
+ tout << wfml << "\n";);
+ return var;
}
- else {
- bv = ctx.mk_bool_var(var);
- }
- ctx.set_enode_flag(bv, true);
- if (attach) {
- ctx.set_var_theory(bv, get_id());
- theory_var v = mk_var(x);
- ctx.attach_th_var(x, this, v);
- m_bool2var.insert(bv, v);
- SASSERT(v == static_cast(m_var2bool.size()));
- m_var2bool.push_back(bv);
- SASSERT(ctx.bool_var2enode(bv));
- }
- return bv;
-}
-rational const& theory_wmaxsat::get_min_cost() {
- unsynch_mpq_manager mgr;
- scoped_mpq q(mgr);
- mgr.set(q, m_zmin_cost, m_den.to_mpq().numerator());
- m_rmin_cost = rational(q);
- return m_rmin_cost;
-}
-
-void theory_wmaxsat::assign_eh(bool_var v, bool is_true) {
- TRACE("opt", tout << "Assign " << mk_pp(m_vars[m_bool2var[v]].get(), get_manager()) << " " << is_true << "\n";);
- if (is_true) {
- if (m_normalize) normalize();
+ void theory_wmaxsat::disable_var(expr* var) {
context& ctx = get_context();
- theory_var tv = m_bool2var[v];
- if (m_assigned[tv]) return;
- scoped_mpz w(m_mpz);
- w = m_zweights[tv];
- ctx.push_trail(numeral_trail(m_zcost, m_old_values));
- ctx.push_trail(push_back_vector >(m_costs));
- ctx.push_trail(value_trail(m_assigned[tv]));
- m_zcost += w;
- m_costs.push_back(tv);
- m_assigned[tv] = true;
- if (m_zcost > m_zmin_cost) {
- block();
+ SASSERT(ctx.b_internalized(var));
+ bool_var bv = ctx.get_bool_var(var);
+ theory_var tv = m_bool2var[bv];
+ m_enabled[tv] = false;
+ TRACE("opt", tout << "disable: v" << tv << " b" << bv << " " << mk_pp(var, get_manager()) << "\n";);
+ }
+
+ bool_var theory_wmaxsat::register_var(app* var, bool attach) {
+ context & ctx = get_context();
+ bool_var bv;
+ SASSERT(!ctx.e_internalized(var));
+ enode* x = ctx.mk_enode(var, false, true, true);
+ if (ctx.b_internalized(var)) {
+ bv = ctx.get_bool_var(var);
}
- }
-}
-
-final_check_status theory_wmaxsat::final_check_eh() {
- if (m_normalize) normalize();
- return FC_DONE;
-}
-
-
-void theory_wmaxsat::reset_eh() {
- theory::reset_eh();
- reset_local();
-}
-
-void theory_wmaxsat::reset_local() {
- m_vars.reset();
- m_fmls.reset();
- m_rweights.reset();
- m_rmin_cost.reset();
- m_rcost.reset();
- m_zweights.reset();
- m_zcost.reset();
- m_zmin_cost.reset();
- m_cost_save.reset();
- m_bool2var.reset();
- m_var2bool.reset();
- m_propagate = false;
- m_found_optimal = false;
- m_assigned.reset();
-}
-
-
-void theory_wmaxsat::propagate() {
- context& ctx = get_context();
- for (unsigned i = 0; m_propagate && i < m_vars.size(); ++i) {
- bool_var bv = m_var2bool[i];
- lbool asgn = ctx.get_assignment(bv);
- if (asgn == l_true) {
- assign_eh(bv, true);
+ else {
+ bv = ctx.mk_bool_var(var);
}
+ ctx.set_enode_flag(bv, true);
+ if (attach) {
+ ctx.set_var_theory(bv, get_id());
+ theory_var v = mk_var(x);
+ ctx.attach_th_var(x, this, v);
+ m_bool2var.insert(bv, v);
+ SASSERT(v == static_cast(m_var2bool.size()));
+ m_var2bool.push_back(bv);
+ SASSERT(ctx.bool_var2enode(bv));
+ }
+ return bv;
}
- m_propagate = false;
-}
-
-bool theory_wmaxsat::is_optimal() const {
- return !m_found_optimal || m_zcost < m_zmin_cost;
-}
-
-expr_ref theory_wmaxsat::mk_block() {
- ++m_stats.m_num_blocks;
- ast_manager& m = get_manager();
- expr_ref_vector disj(m);
- compare_cost compare_cost(*this);
- svector costs(m_costs);
- std::sort(costs.begin(), costs.end(), compare_cost);
- scoped_mpz weight(m_mpz);
- m_mpz.reset(weight);
- for (unsigned i = 0; i < costs.size() && m_mpz.lt(weight, m_zmin_cost); ++i) {
- weight += m_zweights[costs[i]];
- disj.push_back(m.mk_not(m_vars[costs[i]].get()));
- }
- if (is_optimal()) {
+
+ rational theory_wmaxsat::get_cost() {
unsynch_mpq_manager mgr;
scoped_mpq q(mgr);
- mgr.set(q, m_zmin_cost, m_den.to_mpq().numerator());
- rational rw = rational(q);
- m_zmin_cost = weight;
- m_found_optimal = true;
+ mgr.set(q, m_zcost, m_den.to_mpq().numerator());
+ return rational(q);
+ }
+
+ void theory_wmaxsat::init_min_cost(rational const& r) {
+ m_rmin_cost = r;
+ m_zmin_cost = (m_rmin_cost * m_den).to_mpq().numerator();
+ }
+
+
+ void theory_wmaxsat::assign_eh(bool_var v, bool is_true) {
+ if (is_true) {
+ if (m_normalize) normalize();
+ context& ctx = get_context();
+ theory_var tv = m_bool2var[v];
+ if (m_assigned[tv] || !m_enabled[tv]) return;
+ scoped_mpz w(m_mpz);
+ w = m_zweights[tv];
+ ctx.push_trail(numeral_trail(m_zcost, m_old_values));
+ ctx.push_trail(push_back_vector >(m_costs));
+ ctx.push_trail(value_trail(m_assigned[tv]));
+ m_zcost += w;
+ TRACE("opt", tout << "Assign v" << tv << " weight: " << w << " cost: " << m_zcost << " " << mk_pp(m_vars[m_bool2var[v]].get(), get_manager()) << "\n";);
+ m_costs.push_back(tv);
+ m_assigned[tv] = true;
+ if (m_zcost >= m_zmin_cost) {
+ block();
+ }
+ else {
+ m_can_propagate = true;
+ }
+ }
+ }
+
+ final_check_status theory_wmaxsat::final_check_eh() {
+ if (m_normalize) normalize();
+ // std::cout << "cost: " << m_zcost << " min cost: " << m_zmin_cost << "\n";
+ return FC_DONE;
+ }
+
+
+ void theory_wmaxsat::reset_eh() {
+ theory::reset_eh();
+ reset_local();
+ }
+
+ void theory_wmaxsat::reset_local() {
+ m_vars.reset();
+ m_fmls.reset();
+ m_rweights.reset();
+ m_rmin_cost.reset();
+ m_zweights.reset();
+ m_zcost.reset();
+ m_zmin_cost.reset();
m_cost_save.reset();
- m_cost_save.append(m_costs);
+ m_bool2var.reset();
+ m_var2bool.reset();
+ m_propagate = false;
+ m_can_propagate = false;
+ m_found_optimal = false;
+ m_assigned.reset();
+ m_enabled.reset();
+ }
+
+
+ void theory_wmaxsat::propagate() {
+ context& ctx = get_context();
+ for (unsigned i = 0; m_propagate && i < m_vars.size(); ++i) {
+ bool_var bv = m_var2bool[i];
+ lbool asgn = ctx.get_assignment(bv);
+ if (asgn == l_true) {
+ assign_eh(bv, true);
+ }
+ }
+ m_propagate = false;
+ //while (m_found_optimal && max_unassigned_is_blocked() && !ctx.inconsistent()) { }
+
+ m_can_propagate = false;
+ }
+
+ bool theory_wmaxsat::is_optimal() const {
+ return !m_found_optimal || m_zcost < m_zmin_cost;
+ }
+
+ expr_ref theory_wmaxsat::mk_block() {
+ ++m_stats.m_num_blocks;
+ ast_manager& m = get_manager();
+ expr_ref_vector disj(m);
+ compare_cost compare_cost(*this);
+ svector costs(m_costs);
+ std::sort(costs.begin(), costs.end(), compare_cost);
+ scoped_mpz weight(m_mpz);
+ m_mpz.reset(weight);
+ for (unsigned i = 0; i < costs.size() && m_mpz.lt(weight, m_zmin_cost); ++i) {
+ theory_var tv = costs[i];
+ if (m_enabled[tv]) {
+ weight += m_zweights[tv];
+ disj.push_back(m.mk_not(m_vars[tv].get()));
+ }
+ }
+ if (is_optimal()) {
+ m_found_optimal = true;
+ m_cost_save.reset();
+ m_cost_save.append(m_costs);
+ TRACE("opt",
+ tout << "costs: ";
+ for (unsigned i = 0; i < m_costs.size(); ++i) {
+ tout << mk_pp(get_enode(m_costs[i])->get_owner(), get_manager()) << " ";
+ }
+ tout << "\n";
+ //get_context().display(tout);
+ );
+ }
+ expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m);
TRACE("opt",
- tout << "costs: ";
- for (unsigned i = 0; i < m_costs.size(); ++i) {
- tout << mk_pp(get_enode(m_costs[i])->get_owner(), get_manager()) << " ";
- }
- tout << "\n";
- get_context().display(tout);
- );
+ tout << result << " weight: " << weight << "\n";
+ tout << "cost: " << m_zcost << " min-cost: " << m_zmin_cost << "\n";);
+ return result;
}
- expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m);
- TRACE("opt",
- tout << result << " weight: " << weight << "\n";
- tout << "cost: " << m_zcost << " min-cost: " << m_zmin_cost << "\n";);
- return result;
-}
-expr_ref theory_wmaxsat::mk_optimal_block(svector const& ws, rational const& weight) {
- ast_manager& m = get_manager();
- expr_ref_vector disj(m);
- rational new_w = weight*m_den;
- m_zmin_cost = new_w.to_mpq().numerator();
- m_cost_save.reset();
- for (unsigned i = 0; i < ws.size(); ++i) {
- bool_var bv = ws[i];
- theory_var v = m_bool2var[bv];
- m_cost_save.push_back(v);
- disj.push_back(m.mk_not(m_vars[v].get()));
- }
- expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m);
- return result;
-}
+ void theory_wmaxsat::restart_eh() {}
-void theory_wmaxsat::block() {
- if (m_vars.empty()) {
- return;
+ void theory_wmaxsat::block() {
+ if (m_vars.empty()) {
+ return;
+ }
+ ++m_stats.m_num_blocks;
+ context& ctx = get_context();
+ literal_vector lits;
+ compare_cost compare_cost(*this);
+ svector costs(m_costs);
+ std::sort(costs.begin(), costs.end(), compare_cost);
+
+ scoped_mpz weight(m_mpz);
+ m_mpz.reset(weight);
+ for (unsigned i = 0; i < costs.size() && weight < m_zmin_cost; ++i) {
+ weight += m_zweights[costs[i]];
+ lits.push_back(literal(m_var2bool[costs[i]]));
+ }
+ TRACE("opt", ctx.display_literals_verbose(tout, lits); tout << "\n";);
+
+ ctx.set_conflict(
+ ctx.mk_justification(
+ ext_theory_conflict_justification(get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), 0, 0, 0, 0)));
+ }
+
+ bool theory_wmaxsat::max_unassigned_is_blocked() {
+ context& ctx = get_context();
+ unsigned max_unassigned = m_max_unassigned_index;
+ if (max_unassigned < m_sorted_vars.size() &&
+ m_zcost + m_zweights[m_sorted_vars[max_unassigned]] < m_zmin_cost) {
+ return false;
+ }
+ // update value of max-unassigned
+ while (max_unassigned < m_sorted_vars.size() &&
+ ctx.get_assignment(m_var2bool[m_sorted_vars[max_unassigned]]) != l_undef) {
+ ++max_unassigned;
+ }
+ //
+ if (max_unassigned > m_max_unassigned_index) {
+ ctx.push_trail(value_trail(m_max_unassigned_index));
+ m_max_unassigned_index = max_unassigned;
+ }
+ if (max_unassigned < m_sorted_vars.size() &&
+ m_zcost + m_zweights[m_sorted_vars[max_unassigned]] >= m_zmin_cost) {
+ theory_var tv = m_sorted_vars[max_unassigned];
+ propagate(m_var2bool[tv]);
+ m_max_unassigned_index++;
+ return true;
+ }
+
+ return false;
}
- ++m_stats.m_num_blocks;
- context& ctx = get_context();
- literal_vector lits;
- compare_cost compare_cost(*this);
- svector costs(m_costs);
- std::sort(costs.begin(), costs.end(), compare_cost);
- scoped_mpz weight(m_mpz);
- m_mpz.reset(weight);
- for (unsigned i = 0; i < costs.size() && weight < m_zmin_cost; ++i) {
- weight += m_zweights[costs[i]];
- lits.push_back(~literal(m_var2bool[costs[i]]));
- }
- TRACE("opt",
- ast_manager& m = get_manager();
- tout << "block: ";
- for (unsigned i = 0; i < lits.size(); ++i) {
- expr_ref tmp(m);
- ctx.literal2expr(lits[i], tmp);
- tout << tmp << " ";
- }
- tout << "\n";
- );
-
- ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
-}
+ void theory_wmaxsat::propagate(bool_var v) {
+ ++m_stats.m_num_propagations;
+ context& ctx = get_context();
+ literal_vector lits;
+ literal lit(v, true);
+
+ SASSERT(ctx.get_assignment(lit) == l_undef);
+
+ for (unsigned i = 0; i < m_costs.size(); ++i) {
+ bool_var w = m_var2bool[m_costs[i]];
+ lits.push_back(literal(w));
+ }
+ TRACE("opt",
+ ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr());
+ ctx.display_literal_verbose(tout << " --> ", lit););
+
+ region& r = ctx.get_region();
+ ctx.assign(lit, ctx.mk_justification(
+ ext_theory_propagation_justification(
+ get_id(), r, lits.size(), lits.c_ptr(), 0, 0, lit, 0, 0)));
+ }
-void theory_wmaxsat::normalize() {
- m_den = rational::one();
- for (unsigned i = 0; i < m_rweights.size(); ++i) {
- m_den = lcm(m_den, denominator(m_rweights[i]));
+ void theory_wmaxsat::normalize() {
+ m_den = rational::one();
+ for (unsigned i = 0; i < m_rweights.size(); ++i) {
+ if (m_enabled[i]) {
+ m_den = lcm(m_den, denominator(m_rweights[i]));
+ }
+ }
+ m_den = lcm(m_den, denominator(m_rmin_cost));
+ SASSERT(!m_den.is_zero());
+ m_zweights.reset();
+ m_sorted_vars.reset();
+ for (unsigned i = 0; i < m_rweights.size(); ++i) {
+ rational r = m_rweights[i]*m_den;
+ SASSERT(r.is_int());
+ mpq const& q = r.to_mpq();
+ m_zweights.push_back(q.numerator());
+ m_sorted_vars.push_back(i);
+ }
+ compare_cost compare_cost(*this);
+ std::sort(m_sorted_vars.begin(), m_sorted_vars.end(), compare_cost);
+ m_max_unassigned_index = 0;
+
+ m_zcost.reset();
+ rational r = m_rmin_cost * m_den;
+ m_zmin_cost = r.to_mpq().numerator();
+ m_normalize = false;
}
- m_den = lcm(m_den, denominator(m_rmin_cost));
- SASSERT(!m_den.is_zero());
- m_zweights.reset();
- for (unsigned i = 0; i < m_rweights.size(); ++i) {
- rational r = m_rweights[i]*m_den;
- SASSERT(r.is_int());
- mpq const& q = r.to_mpq();
- m_zweights.push_back(q.numerator());
- }
- rational r = m_rcost* m_den;
- m_zcost = r.to_mpq().numerator();
- r = m_rmin_cost * m_den;
- m_zmin_cost = r.to_mpq().numerator();
- m_normalize = false;
-}
};
diff --git a/src/smt/theory_wmaxsat.h b/src/smt/theory_wmaxsat.h
index 0804c4b68..0f711b9f8 100644
--- a/src/smt/theory_wmaxsat.h
+++ b/src/smt/theory_wmaxsat.h
@@ -28,6 +28,7 @@ namespace smt {
class theory_wmaxsat : public theory {
struct stats {
unsigned m_num_blocks;
+ unsigned m_num_propagations;
void reset() { memset(this, 0, sizeof(*this)); }
stats() { reset(); }
};
@@ -39,27 +40,31 @@ namespace smt {
scoped_mpz_vector m_zweights;
scoped_mpz_vector m_old_values;
svector m_costs; // set of asserted theory variables
+ unsigned m_max_unassigned_index; // index of literal that is not yet assigned and has maximal weight.
+ svector m_sorted_vars; // set of all theory variables, sorted by cost
svector m_cost_save; // set of asserted theory variables
- rational m_rcost; // current sum of asserted costs
rational m_rmin_cost; // current maximal cost assignment.
scoped_mpz m_zcost; // current sum of asserted costs
scoped_mpz m_zmin_cost; // current maximal cost assignment.
bool m_found_optimal;
u_map m_bool2var; // bool_var -> theory_var
svector m_var2bool; // theory_var -> bool_var
- bool m_propagate;
+ bool m_propagate;
+ bool m_can_propagate;
bool m_normalize;
rational m_den; // lcm of denominators for rational weights.
- svector m_assigned;
+ svector m_assigned, m_enabled;
stats m_stats;
public:
theory_wmaxsat(ast_manager& m, filter_model_converter& mc);
virtual ~theory_wmaxsat();
void get_assignment(svector& result);
- virtual void init_search_eh();
- expr* assert_weighted(expr* fml, rational const& w, bool is_true);
+ expr* assert_weighted(expr* fml, rational const& w);
+ void disable_var(expr* var);
bool_var register_var(app* var, bool attach);
- rational const& get_min_cost();
+ rational get_cost();
+ void init_min_cost(rational const& r);
+
class numeral_trail : public trail {
typedef scoped_mpz T;
T & m_value;
@@ -79,6 +84,8 @@ namespace smt {
m_old_values.shrink(m_old_values.size() - 1);
}
};
+
+ virtual void init_search_eh();
virtual void assign_eh(bool_var v, bool is_true);
virtual final_check_status final_check_eh();
virtual bool use_diseqs() const {
@@ -95,23 +102,30 @@ namespace smt {
virtual void new_eq_eh(theory_var v1, theory_var v2) { }
virtual void new_diseq_eh(theory_var v1, theory_var v2) { }
virtual void display(std::ostream& out) const {}
+ virtual void restart_eh();
virtual void collect_statistics(::statistics & st) const {
st.update("wmaxsat num blocks", m_stats.m_num_blocks);
+ st.update("wmaxsat num props", m_stats.m_num_propagations);
}
virtual bool can_propagate() {
- return m_propagate;
+ return m_propagate || m_can_propagate;
}
virtual void propagate();
+
bool is_optimal() const;
expr_ref mk_block();
- expr_ref mk_optimal_block(svector const& ws, rational const& weight);
+
+
private:
void block();
+ void propagate(bool_var v);
void normalize();
+
+ bool max_unassigned_is_blocked();
class compare_cost {
theory_wmaxsat& m_th;
diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp
index 9ee047839..210a09f96 100644
--- a/src/solver/smt_logics.cpp
+++ b/src/solver/smt_logics.cpp
@@ -144,6 +144,10 @@ bool smt_logics::logic_has_horn(symbol const& s) {
return s == "HORN";
}
+bool smt_logics::logic_has_pb(symbol const& s) {
+ return s == "QF_FD" || s == "ALL";
+}
+
bool smt_logics::logic_has_datatype(symbol const& s) {
return s == "QF_FD";
}
diff --git a/src/solver/smt_logics.h b/src/solver/smt_logics.h
index f283040d9..72c3b8764 100644
--- a/src/solver/smt_logics.h
+++ b/src/solver/smt_logics.h
@@ -32,6 +32,7 @@ public:
static bool logic_has_seq(symbol const & s);
static bool logic_has_fpa(symbol const & s);
static bool logic_has_horn(symbol const& s);
+ static bool logic_has_pb(symbol const& s);
static bool logic_has_fd(symbol const& s) { return s == "QF_FD"; }
static bool logic_has_datatype(symbol const& s);
};
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index 441ece429..9163cfeda 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -154,6 +154,10 @@ lbool solver::find_mutexes(expr_ref_vector const& vars, vector&
return l_true;
}
+lbool solver::preferred_sat(expr_ref_vector const& asms, vector& cores) {
+ return check_sat(0, 0);
+}
+
bool solver::is_literal(ast_manager& m, expr* e) {
return is_uninterp_const(e) || (m.is_not(e, e) && is_uninterp_const(e));
}
diff --git a/src/solver/solver.h b/src/solver/solver.h
index 15932fd5d..d5d9ccfd5 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -151,9 +151,9 @@ public:
/**
\brief under assumptions, asms, retrieve set of consequences that
- fix values for expressions that can be built from vars.
- The consequences are clauses whose first literal constrain one of the
- functions from vars and the other literals are negations of literals from asms.
+ fix values for expressions that can be built from vars.
+ The consequences are clauses whose first literal constrain one of the
+ functions from vars and the other literals are negations of literals from asms.
*/
virtual lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences);
@@ -166,6 +166,12 @@ public:
virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes);
+ /**
+ \brief Preferential SAT. Prefer assumptions to be true, produce cores that witness cases when not all assumptions can be met.
+ by default, preferred sat ignores the assumptions.
+ */
+ virtual lbool preferred_sat(expr_ref_vector const& asms, vector& cores);
+
/**
\brief Display the content of this solver.
*/
diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp
index dddb0c636..6e289d969 100644
--- a/src/tactic/aig/aig.cpp
+++ b/src/tactic/aig/aig.cpp
@@ -68,7 +68,8 @@ inline aig_lit right(aig_lit const & n) { return right(n.ptr()); }
inline unsigned to_idx(aig * p) { SASSERT(!is_var(p)); return p->m_id - FIRST_NODE_ID; }
-void unmark(unsigned sz, aig * const * ns) {
+
+static void unmark(unsigned sz, aig * const * ns) {
for (unsigned i = 0; i < sz; i++) {
ns[i]->m_mark = false;
}
diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp
index 950248698..8ff82af17 100644
--- a/src/tactic/arith/add_bounds_tactic.cpp
+++ b/src/tactic/arith/add_bounds_tactic.cpp
@@ -51,6 +51,7 @@ public:
virtual result operator()(goal const & g) {
return is_unbounded(g);
}
+ virtual ~is_unbounded_probe() {}
};
probe * mk_is_unbounded_probe() {
@@ -109,11 +110,11 @@ class add_bounds_tactic : public tactic {
void operator()(quantifier*) {}
};
- virtual void operator()(goal_ref const & g,
- goal_ref_buffer & result,
- model_converter_ref & mc,
- proof_converter_ref & pc,
- expr_dependency_ref & core) {
+ void operator()(goal_ref const & g,
+ goal_ref_buffer & result,
+ model_converter_ref & mc,
+ proof_converter_ref & pc,
+ expr_dependency_ref & core) {
mc = 0; pc = 0; core = 0;
tactic_report report("add-bounds", *g);
bound_manager bm(m);
diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp
index 410185cf8..d63c2fcf4 100644
--- a/src/tactic/arith/diff_neq_tactic.cpp
+++ b/src/tactic/arith/diff_neq_tactic.cpp
@@ -312,11 +312,11 @@ class diff_neq_tactic : public tactic {
return md;
}
- virtual void operator()(goal_ref const & g,
- goal_ref_buffer & result,
- model_converter_ref & mc,
- proof_converter_ref & pc,
- expr_dependency_ref & core) {
+ void operator()(goal_ref const & g,
+ goal_ref_buffer & result,
+ model_converter_ref & mc,
+ proof_converter_ref & pc,
+ expr_dependency_ref & core) {
SASSERT(g->is_well_sorted());
m_produce_models = g->models_enabled();
mc = 0; pc = 0; core = 0; result.reset();
diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp
index 5c82bbbc3..6db0f5ad3 100644
--- a/src/tactic/arith/fm_tactic.cpp
+++ b/src/tactic/arith/fm_tactic.cpp
@@ -1549,11 +1549,11 @@ class fm_tactic : public tactic {
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
}
- virtual void operator()(goal_ref const & g,
- goal_ref_buffer & result,
- model_converter_ref & mc,
- proof_converter_ref & pc,
- expr_dependency_ref & core) {
+ void operator()(goal_ref const & g,
+ goal_ref_buffer & result,
+ model_converter_ref & mc,
+ proof_converter_ref & pc,
+ expr_dependency_ref & core) {
SASSERT(g->is_well_sorted());
mc = 0; pc = 0; core = 0;
tactic_report report("fm", *g);
diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp
index 8d637bada..2b54dd463 100644
--- a/src/tactic/arith/lia2pb_tactic.cpp
+++ b/src/tactic/arith/lia2pb_tactic.cpp
@@ -188,11 +188,11 @@ class lia2pb_tactic : public tactic {
return true;
}
- virtual void operator()(goal_ref const & g,
- goal_ref_buffer & result,
- model_converter_ref & mc,
- proof_converter_ref & pc,
- expr_dependency_ref & core) {
+ void operator()(goal_ref const & g,
+ goal_ref_buffer & result,
+ model_converter_ref & mc,
+ proof_converter_ref & pc,
+ expr_dependency_ref & core) {
SASSERT(g->is_well_sorted());
fail_if_proof_generation("lia2pb", g);
m_produce_models = g->models_enabled();
diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp
index b3ec505ea..06f1368a2 100644
--- a/src/tactic/arith/normalize_bounds_tactic.cpp
+++ b/src/tactic/arith/normalize_bounds_tactic.cpp
@@ -80,11 +80,11 @@ class normalize_bounds_tactic : public tactic {
return false;
}
- virtual void operator()(goal_ref const & in,
- goal_ref_buffer & result,
- model_converter_ref & mc,
- proof_converter_ref & pc,
- expr_dependency_ref & core) {
+ void operator()(goal_ref const & in,
+ goal_ref_buffer & result,
+ model_converter_ref & mc,
+ proof_converter_ref & pc,
+ expr_dependency_ref & core) {
mc = 0; pc = 0; core = 0;
bool produce_models = in->models_enabled();
bool produce_proofs = in->proofs_enabled();
diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp
index 6348ddd74..3931a1ea4 100644
--- a/src/tactic/arith/pb2bv_tactic.cpp
+++ b/src/tactic/arith/pb2bv_tactic.cpp
@@ -885,11 +885,11 @@ private:
r.erase("elim_and");
}
- virtual void operator()(goal_ref const & g,
- goal_ref_buffer & result,
- model_converter_ref & mc,
- proof_converter_ref & pc,
- expr_dependency_ref & core) {
+ void operator()(goal_ref const & g,
+ goal_ref_buffer & result,
+ model_converter_ref & mc,
+ proof_converter_ref & pc,
+ expr_dependency_ref & core) {
TRACE("pb2bv", g->display(tout););
SASSERT(g->is_well_sorted());
fail_if_proof_generation("pb2bv", g);
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index 156f69388..df3b9f0f5 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -819,7 +819,7 @@ class elim_uncnstr_tactic : public tactic {
m_rw = alloc(rw, m(), produce_proofs, m_vars, m_mc.get(), m_max_memory, m_max_steps);
}
- virtual void operator()(goal_ref const & g,
+ void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp
index 28597c6ec..d55a2e25c 100644
--- a/src/tactic/fpa/fpa2bv_tactic.cpp
+++ b/src/tactic/fpa/fpa2bv_tactic.cpp
@@ -46,11 +46,11 @@ class fpa2bv_tactic : public tactic {
m_rw.cfg().updt_params(p);
}
- virtual void operator()(goal_ref const & g,
- goal_ref_buffer & result,
- model_converter_ref & mc,
- proof_converter_ref & pc,
- expr_dependency_ref & core) {
+ void operator()(goal_ref const & g,
+ goal_ref_buffer & result,
+ model_converter_ref & mc,
+ proof_converter_ref & pc,
+ expr_dependency_ref & core) {
SASSERT(g->is_well_sorted());
m_proofs_enabled = g->proofs_enabled();
m_produce_models = g->models_enabled();
diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp
index 4e49e0d76..f4ef300e4 100644
--- a/src/tactic/sls/sls_tactic.cpp
+++ b/src/tactic/sls/sls_tactic.cpp
@@ -94,13 +94,13 @@ public:
};
-tactic * mk_sls_tactic(ast_manager & m, params_ref const & p) {
+static tactic * mk_sls_tactic(ast_manager & m, params_ref const & p) {
return and_then(fail_if_not(mk_is_qfbv_probe()), // Currently only QF_BV is supported.
clean(alloc(sls_tactic, m, p)));
}
-tactic * mk_preamble(ast_manager & m, params_ref const & p) {
+static tactic * mk_preamble(ast_manager & m, params_ref const & p) {
params_ref main_p;
main_p.set_bool("elim_and", true);
// main_p.set_bool("pull_cheap_ite", true);
diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp
index 7cc875fba..918e0fc6d 100644
--- a/src/tactic/smtlogics/qfbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfbv_tactic.cpp
@@ -32,7 +32,7 @@ Notes:
#define MEMLIMIT 300
-tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
+static tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
params_ref solve_eq_p;
// conservative guassian elimination.
@@ -80,7 +80,7 @@ static tactic * main_p(tactic* t) {
}
-tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tactic* smt) {
+static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tactic* smt) {
params_ref local_ctx_p = p;
local_ctx_p.set_bool("local_ctx", true);
diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp
index 950291221..5a71281fb 100644
--- a/src/tactic/smtlogics/qfnia_tactic.cpp
+++ b/src/tactic/smtlogics/qfnia_tactic.cpp
@@ -29,7 +29,7 @@ Notes:
#include"ctx_simplify_tactic.h"
#include"cofactor_term_ite_tactic.h"
-tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) {
+static tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) {
params_ref p = p_ref;
p.set_bool("flat", false);
p.set_bool("hi_div0", true);
@@ -51,7 +51,7 @@ tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) {
return r;
}
-tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) {
+static tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) {
params_ref pull_ite_p = p_ref;
pull_ite_p.set_bool("pull_cheap_ite", true);
pull_ite_p.set_bool("local_ctx", true);
@@ -77,7 +77,7 @@ tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) {
using_params(mk_simplify_tactic(m), simp_p));
}
-tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) {
+static tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) {
params_ref nia2sat_p = p;
nia2sat_p.set_uint("nla2bv_max_bv_size", 64);
diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp
index bc3585d09..044511c33 100644
--- a/src/tactic/smtlogics/quant_tactics.cpp
+++ b/src/tactic/smtlogics/quant_tactics.cpp
@@ -104,21 +104,12 @@ tactic * mk_aufnira_tactic(ast_manager & m, params_ref const & p) {
}
tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
-#if 0
- tactic * st = and_then(mk_quant_preprocessor(m),
- or_else(try_for(mk_smt_tactic(), 100),
- try_for(qe::mk_sat_tactic(m), 1000),
- try_for(mk_smt_tactic(), 1000),
- and_then(mk_qe_tactic(m), mk_smt_tactic())
- ));
-#else
tactic * st = and_then(mk_quant_preprocessor(m),
mk_qe_lite_tactic(m, p),
cond(mk_has_quantifier_probe(),
or_else(mk_qsat_tactic(m, p),
and_then(mk_qe_tactic(m), mk_smt_tactic())),
mk_smt_tactic()));
-#endif
st->updt_params(p);
return st;
}
diff --git a/src/tactic/ufbv/ufbv_tactic.cpp b/src/tactic/ufbv/ufbv_tactic.cpp
index 7a185c854..19d41be68 100644
--- a/src/tactic/ufbv/ufbv_tactic.cpp
+++ b/src/tactic/ufbv/ufbv_tactic.cpp
@@ -31,11 +31,11 @@ Notes:
#include"ufbv_tactic.h"
-tactic * mk_der_fp_tactic(ast_manager & m, params_ref const & p) {
+static tactic * mk_der_fp_tactic(ast_manager & m, params_ref const & p) {
return repeat(and_then(mk_der_tactic(m), mk_simplify_tactic(m, p)));
}
-tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) {
+static tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) {
params_ref no_elim_and(p);
no_elim_and.set_bool("elim_and", false);
diff --git a/src/tactic/ufbv/ufbv_tactic.h b/src/tactic/ufbv/ufbv_tactic.h
index 2d5454de5..300fdd84a 100644
--- a/src/tactic/ufbv/ufbv_tactic.h
+++ b/src/tactic/ufbv/ufbv_tactic.h
@@ -23,8 +23,6 @@ Notes:
class ast_manager;
class tactic;
-tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p = params_ref());
-
tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp
index 03b720ae1..e9d108cec 100644
--- a/src/util/mpf.cpp
+++ b/src/util/mpf.cpp
@@ -795,8 +795,9 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
set(o, z);
}
else if (is_zero(x) || is_zero(y)) {
- if (is_zero(z) && rm != MPF_ROUND_TOWARD_NEGATIVE)
- mk_pzero(x.ebits, x.sbits, o);
+ bool xy_sgn = is_neg(x) ^ is_neg(y);
+ if (is_zero(z) && xy_sgn ^ is_neg(z))
+ mk_zero(x.ebits, x.sbits, rm != MPF_ROUND_TOWARD_NEGATIVE, o);
else
set(o, z);
}
@@ -1224,7 +1225,7 @@ void mpf_manager::renormalize(unsigned ebits, unsigned sbits, mpf_exp_t & exp, m
m_mpz_manager.machine_div2k(sig, 1);
exp++;
}
-
+
const mpz & pl = m_powers2(sbits-1);
while (m_mpz_manager.lt(sig, pl)) {
m_mpz_manager.mul2k(sig, 1);
@@ -1235,7 +1236,7 @@ void mpf_manager::renormalize(unsigned ebits, unsigned sbits, mpf_exp_t & exp, m
void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & exp_diff, bool partial) {
unsigned ebits = x.ebits;
unsigned sbits = x.sbits;
-
+
SASSERT(-1 <= exp_diff && exp_diff < INT64_MAX);
SASSERT(exp_diff < ebits+sbits || partial);
@@ -1252,7 +1253,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
SASSERT(m_mpz_manager.lt(y.significand, m_powers2(sbits)));
SASSERT(m_mpz_manager.ge(y.significand, m_powers2(sbits - 1)));
- // 1. Compute a/b
+ // 1. Compute a/b
bool x_div_y_sgn = x.sign != y.sign;
mpf_exp_t x_div_y_exp = D;
scoped_mpz x_sig_shifted(m_mpz_manager), x_div_y_sig_lrg(m_mpz_manager), x_div_y_rem(m_mpz_manager);
@@ -1271,7 +1272,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
mpf_exp_t Q_exp = x_div_y_exp;
scoped_mpz Q_sig(m_mpz_manager), Q_rem(m_mpz_manager);
unsigned Q_shft = (sbits-1) + (sbits+3) - (unsigned) (partial ? N :Q_exp);
- if (partial) {
+ if (partial) {
// Round according to MPF_ROUND_TOWARD_ZERO
SASSERT(0 < N && N < Q_exp && Q_exp < INT_MAX);
m_mpz_manager.machine_div2k(x_div_y_sig_lrg, Q_shft, Q_sig);
@@ -1294,7 +1295,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
TRACE("mpf_dbg_rem", tout << "Q_exp=" << Q_exp << std::endl;
tout << "Q_sig=" << m_mpz_manager.to_string(Q_sig) << std::endl;
tout << "Q=" << to_string_hexfloat(Q_sgn, Q_exp, Q_sig, ebits, sbits, 0) << std::endl;);
-
+
if ((D == -1 || partial) && m_mpz_manager.is_zero(Q_sig))
return; // This means x % y = x.
@@ -1308,7 +1309,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
bool YQ_sgn = x.sign;
scoped_mpz YQ_sig(m_mpz_manager);
mpf_exp_t YQ_exp = Q_exp + y.exponent;
- m_mpz_manager.mul(y.significand, Q_sig, YQ_sig);
+ m_mpz_manager.mul(y.significand, Q_sig, YQ_sig);
renormalize(ebits, 2*sbits-1, YQ_exp, YQ_sig); // YQ_sig has `sbits-1' extra bits.
(void)YQ_sgn;
@@ -1317,11 +1318,11 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
tout << "YQ_sig=" << m_mpz_manager.to_string(YQ_sig) << std::endl;
tout << "YQ=" << to_string_hexfloat(YQ_sgn, YQ_exp, YQ_sig, ebits, sbits, sbits-1) << std::endl;);
- // `sbits-1' extra bits in YQ_sig.
+ // `sbits-1' extra bits in YQ_sig.
SASSERT(m_mpz_manager.lt(YQ_sig, m_powers2(2*sbits-1)));
SASSERT(m_mpz_manager.ge(YQ_sig, m_powers2(2*sbits-2)) || YQ_exp <= mk_bot_exp(ebits));
- // 4. Compute X-Y*Q
+ // 4. Compute X-Y*Q
mpf_exp_t X_YQ_exp = x.exponent;
scoped_mpz X_YQ_sig(m_mpz_manager);
mpf_exp_t exp_delta = exp(x) - YQ_exp;
@@ -1339,14 +1340,14 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
SASSERT(m_mpz_manager.ge(minuend, m_powers2(2*sbits-2)));
SASSERT(m_mpz_manager.lt(subtrahend, m_powers2(2*sbits-1)));
SASSERT(m_mpz_manager.ge(subtrahend, m_powers2(2*sbits-2)));
-
+
if (exp_delta != 0) {
scoped_mpz sticky_rem(m_mpz_manager);
m_mpz_manager.set(sticky_rem, 0);
if (exp_delta > sbits+5)
- sticky_rem.swap(subtrahend);
+ sticky_rem.swap(subtrahend);
else if (exp_delta > 0)
- m_mpz_manager.machine_div_rem(subtrahend, m_powers2((unsigned)exp_delta), subtrahend, sticky_rem);
+ m_mpz_manager.machine_div_rem(subtrahend, m_powers2((unsigned)exp_delta), subtrahend, sticky_rem);
else {
SASSERT(exp_delta < 0);
exp_delta = -exp_delta;
@@ -1356,7 +1357,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
m_mpz_manager.inc(subtrahend);
TRACE("mpf_dbg_rem", tout << "aligned subtrahend=" << m_mpz_manager.to_string(subtrahend) << std::endl;);
}
-
+
m_mpz_manager.sub(minuend, subtrahend, X_YQ_sig);
TRACE("mpf_dbg_rem", tout << "X_YQ_sig'=" << m_mpz_manager.to_string(X_YQ_sig) << std::endl;);
@@ -1374,7 +1375,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
tout << "subtrahend=" << m_mpz_manager.to_string(subtrahend) << std::endl;
tout << "X_YQ_sgn=" << X_YQ_sgn << std::endl;
tout << "X_YQ_exp=" << X_YQ_exp << std::endl;
- tout << "X_YQ_sig=" << m_mpz_manager.to_string(X_YQ_sig) << std::endl;
+ tout << "X_YQ_sig=" << m_mpz_manager.to_string(X_YQ_sig) << std::endl;
tout << "X-YQ=" << to_string_hexfloat(X_YQ_sgn, X_YQ_exp, X_YQ_sig, ebits, sbits, sbits-1) << std::endl;);
// `sbits-1' extra bits in X_YQ_sig
@@ -1384,7 +1385,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
TRACE("mpf_dbg_rem", tout << "final sticky=" << m_mpz_manager.to_string(rnd_bits) << std::endl; );
// Round to nearest, ties to even.
- if (m_mpz_manager.eq(rnd_bits, mpz(32))) { // tie.
+ if (m_mpz_manager.eq(rnd_bits, mpz(32))) { // tie.
if (m_mpz_manager.is_odd(X_YQ_sig)) {
m_mpz_manager.inc(X_YQ_sig);
}
@@ -1430,7 +1431,7 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) {
mpf_exp_t D;
do {
if (ST0.exponent() < ST1.exponent() - 1) {
- D = 0;
+ D = 0;
}
else {
D = ST0.exponent() - ST1.exponent();
@@ -1889,7 +1890,7 @@ void mpf_manager::round(mpf_rounding_mode rm, mpf & o) {
const mpz & p_m1 = m_powers2(o.sbits+2);
const mpz & p_m2 = m_powers2(o.sbits+3);
- (void)p_m1;
+ (void)p_m1;
TRACE("mpf_dbg", tout << "p_m1 = " << m_mpz_manager.to_string(p_m1) << std::endl <<
"p_m2 = " << m_mpz_manager.to_string(p_m2) << std::endl;);
diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp
index 9f6c692cc..bda06157d 100644
--- a/src/util/rlimit.cpp
+++ b/src/util/rlimit.cpp
@@ -20,7 +20,7 @@ Revision History:
#include "common_msgs.h"
reslimit::reslimit():
- m_cancel(false),
+ m_cancel(0),
m_count(0),
m_limit(0) {
}
@@ -29,7 +29,6 @@ uint64 reslimit::count() const {
return m_count;
}
-
bool reslimit::inc() {
++m_count;
return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit);
@@ -46,7 +45,7 @@ void reslimit::push(unsigned delta_limit) {
new_limit = 0;
}
m_limits.push_back(m_limit);
- m_limit = m_limit==0?new_limit:std::min(new_limit, m_limit);
+ m_limit = m_limit==0 ? new_limit : std::min(new_limit, m_limit);
m_cancel = 0;
}
@@ -71,14 +70,14 @@ char const* reslimit::get_cancel_msg() const {
void reslimit::push_child(reslimit* r) {
#pragma omp critical (reslimit_cancel)
{
- m_children.push_back(r);
+ m_children.push_back(r);
}
}
void reslimit::pop_child() {
#pragma omp critical (reslimit_cancel)
{
- m_children.pop_back();
+ m_children.pop_back();
}
}
@@ -99,7 +98,7 @@ void reslimit::reset_cancel() {
void reslimit::inc_cancel() {
#pragma omp critical (reslimit_cancel)
- {
+ {
set_cancel(m_cancel+1);
}
}
@@ -114,8 +113,8 @@ void reslimit::dec_cancel() {
}
}
-void reslimit::set_cancel(unsigned f) {
- m_cancel = f;
+void reslimit::set_cancel(unsigned f) {
+ m_cancel = f;
for (unsigned i = 0; i < m_children.size(); ++i) {
m_children[i]->set_cancel(f);
}
diff --git a/src/util/rlimit.h b/src/util/rlimit.h
index ac5db6136..913984768 100644
--- a/src/util/rlimit.h
+++ b/src/util/rlimit.h
@@ -29,8 +29,8 @@ class reslimit {
ptr_vector m_children;
void set_cancel(unsigned f);
-
-public:
+
+public:
reslimit();
void push(unsigned delta_limit);
void pop();
@@ -39,7 +39,7 @@ public:
bool inc();
bool inc(unsigned offset);
- uint64 count() const;
+ uint64 count() const;
bool get_cancel_flag() const { return m_cancel > 0; }
diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp
index 335b2c3bb..f6b0429d9 100644
--- a/src/util/scoped_timer.cpp
+++ b/src/util/scoped_timer.cpp
@@ -73,6 +73,7 @@ struct scoped_timer::imp {
pthread_cond_t m_cond;
unsigned m_ms;
bool m_initialized;
+ bool m_signal_sent;
#else
// Other
#endif
@@ -119,10 +120,18 @@ struct scoped_timer::imp {
pthread_mutex_lock(&st->m_mutex);
st->m_initialized = true;
- int e = pthread_cond_timedwait(&st->m_cond, &st->m_mutex, &end_time);
- ENSURE(e == 0 || e == ETIMEDOUT);
-
+ int e = 0;
+ // `pthread_cond_timedwait()` may spuriously wake even if the signal
+ // was not sent so we loop until a timeout occurs or the signal was
+ // **really** sent.
+ while (!(e == 0 && st->m_signal_sent)) {
+ e = pthread_cond_timedwait(&st->m_cond, &st->m_mutex, &end_time);
+ ENSURE(e == 0 || e == ETIMEDOUT);
+ if (e == ETIMEDOUT)
+ break;
+ }
pthread_mutex_unlock(&st->m_mutex);
+
if (e == ETIMEDOUT)
st->m_eh->operator()();
return 0;
@@ -170,6 +179,7 @@ struct scoped_timer::imp {
// Linux & FreeBSD
m_ms = ms;
m_initialized = false;
+ m_signal_sent = false;
ENSURE(pthread_mutex_init(&m_mutex, NULL) == 0);
ENSURE(pthread_cond_init(&m_cond, NULL) == 0);
ENSURE(pthread_create(&m_thread_id, NULL, &thread_func, this) == 0);
@@ -218,6 +228,10 @@ struct scoped_timer::imp {
if (!init)
sched_yield();
}
+ pthread_mutex_lock(&m_mutex);
+ m_signal_sent = true;
+ pthread_mutex_unlock(&m_mutex);
+ // Perform signal outside of lock to avoid waking timing thread twice.
pthread_cond_signal(&m_cond);
pthread_join(m_thread_id, NULL);