diff --git a/contrib/cmake/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt
index f12c56f8e..65eef8094 100644
--- a/contrib/cmake/src/CMakeLists.txt
+++ b/contrib/cmake/src/CMakeLists.txt
@@ -117,14 +117,16 @@ else()
set(lib_type "STATIC")
endif()
add_library(libz3 ${lib_type} ${object_files})
-# FIXME: Set "VERSION" and "SOVERSION" properly
set_target_properties(libz3 PROPERTIES
- # FIXME: Should we be using ${Z3_VERSION} here?
- # VERSION: Sets up symlinks, does it do anything else?
+ # VERSION determines the version in the filename of the shared library.
+ # SOVERSION determines the value of the DT_SONAME field on ELF platforms.
+ # On ELF platforms the final compiled filename will be libz3.so.W.X.Y.Z
+ # but symlinks will be made to this file from libz3.so and also from
+ # libz3.so.W.X.
+ # This indicates that no breaking API changes will be made within a single
+ # minor version.
VERSION ${Z3_VERSION}
- # SOVERSION: On platforms that use ELF this sets the API version
- # and should be incremented everytime the API changes
- SOVERSION ${Z3_VERSION})
+ SOVERSION ${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR})
if (NOT MSVC)
# On UNIX like platforms if we don't change the OUTPUT_NAME
diff --git a/contrib/cmake/src/tactic/CMakeLists.txt b/contrib/cmake/src/tactic/CMakeLists.txt
index 318803cd2..324d8089b 100644
--- a/contrib/cmake/src/tactic/CMakeLists.txt
+++ b/contrib/cmake/src/tactic/CMakeLists.txt
@@ -12,6 +12,7 @@ z3_add_component(tactic
probe.cpp
proof_converter.cpp
replace_proof_converter.cpp
+ sine_filter.cpp
tactical.cpp
tactic.cpp
COMPONENT_DEPENDENCIES
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 807a131c1..9451e67c0 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -881,8 +881,8 @@ def is_CXX_gpp():
return is_compiler(CXX, 'g++')
def is_clang_in_gpp_form(cc):
- version_string = check_output([cc, '--version'])
- return str(version_string).find('clang') != -1
+ version_string = check_output([cc, '--version']).encode('utf-8').decode('utf-8')
+ return version_string.find('clang') != -1
def is_CXX_clangpp():
if is_compiler(CXX, 'g++'):
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index fd2776079..c9cdc6ab3 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -1110,29 +1110,32 @@ extern "C" {
if (mk_c(c)->get_seq_fid() == _d->get_family_id()) {
switch (_d->get_decl_kind()) {
- case Z3_OP_SEQ_UNIT: return Z3_OP_SEQ_UNIT;
- case Z3_OP_SEQ_EMPTY: return Z3_OP_SEQ_EMPTY;
- case Z3_OP_SEQ_CONCAT: return Z3_OP_SEQ_CONCAT;
- case Z3_OP_SEQ_PREFIX: return Z3_OP_SEQ_PREFIX;
- case Z3_OP_SEQ_SUFFIX: return Z3_OP_SEQ_SUFFIX;
- case Z3_OP_SEQ_CONTAINS: return Z3_OP_SEQ_CONTAINS;
- case Z3_OP_SEQ_EXTRACT: return Z3_OP_SEQ_EXTRACT;
- case Z3_OP_SEQ_REPLACE: return Z3_OP_SEQ_REPLACE;
- case Z3_OP_SEQ_AT: return Z3_OP_SEQ_AT;
- case Z3_OP_SEQ_LENGTH: return Z3_OP_SEQ_LENGTH;
- case Z3_OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX;
- case Z3_OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE;
- case Z3_OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE;
+ case OP_SEQ_UNIT: return Z3_OP_SEQ_UNIT;
+ case OP_SEQ_EMPTY: return Z3_OP_SEQ_EMPTY;
+ case OP_SEQ_CONCAT: return Z3_OP_SEQ_CONCAT;
+ case OP_SEQ_PREFIX: return Z3_OP_SEQ_PREFIX;
+ case OP_SEQ_SUFFIX: return Z3_OP_SEQ_SUFFIX;
+ case OP_SEQ_CONTAINS: return Z3_OP_SEQ_CONTAINS;
+ case OP_SEQ_EXTRACT: return Z3_OP_SEQ_EXTRACT;
+ case OP_SEQ_REPLACE: return Z3_OP_SEQ_REPLACE;
+ case OP_SEQ_AT: return Z3_OP_SEQ_AT;
+ case OP_SEQ_LENGTH: return Z3_OP_SEQ_LENGTH;
+ case OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX;
+ case OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE;
+ case OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE;
- case Z3_OP_RE_PLUS: return Z3_OP_RE_PLUS;
- case Z3_OP_RE_STAR: return Z3_OP_RE_STAR;
- 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;
+ case OP_STRING_STOI: return Z3_OP_STR_TO_INT;
+ case OP_STRING_ITOS: return Z3_OP_INT_TO_STR;
+
+ case OP_RE_PLUS: return Z3_OP_RE_PLUS;
+ case OP_RE_STAR: return Z3_OP_RE_STAR;
+ case OP_RE_OPTION: return Z3_OP_RE_OPTION;
+ case OP_RE_CONCAT: return Z3_OP_RE_CONCAT;
+ case OP_RE_UNION: return Z3_OP_RE_UNION;
+ case OP_RE_INTERSECT: return Z3_OP_RE_INTERSECT;
+ case OP_RE_LOOP: return Z3_OP_RE_LOOP;
+ case OP_RE_FULL_SET: return Z3_OP_RE_FULL_SET;
+ case 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 478ee6274..986e6f497 100644
--- a/src/api/api_seq.cpp
+++ b/src/api/api_seq.cpp
@@ -141,6 +141,10 @@ 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);
+ MK_UNARY(Z3_mk_int_to_str, mk_c(c)->get_seq_fid(), OP_STRING_ITOS, SKIP);
+ MK_UNARY(Z3_mk_str_to_int, mk_c(c)->get_seq_fid(), OP_STRING_STOI, 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);
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 979d9aed7..e5d0acaab 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -964,6 +964,17 @@ namespace z3 {
check_error();
return expr(ctx(), r);
}
+ expr stoi() const {
+ Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
+ check_error();
+ return expr(ctx(), r);
+ }
+ expr itos() const {
+ Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
+ check_error();
+ return expr(ctx(), r);
+ }
+
friend expr range(expr const& lo, expr const& hi);
/**
\brief create a looping regular expression.
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index f5c4dc99d..a656be3eb 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2420,6 +2420,29 @@ namespace Microsoft.Z3
return new SeqExpr(this, Native.Z3_mk_string(nCtx, s));
}
+ ///
+ /// Convert an integer expression to a string.
+ ///
+ public SeqExpr IntToString(Expr e)
+ {
+ Contract.Requires(e != null);
+ Contract.Requires(e is ArithExpr);
+ Contract.Ensures(Contract.Result() != null);
+ return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject));
+ }
+
+ ///
+ /// Convert an integer expression to a string.
+ ///
+ public IntExpr StringToInt(Expr e)
+ {
+ Contract.Requires(e != null);
+ Contract.Requires(e is SeqExpr);
+ Contract.Ensures(Contract.Result() != null);
+ return new IntExpr(this, Native.Z3_mk_str_to_int(nCtx, e.NativeObject));
+ }
+
+
///
/// Concatentate sequences.
///
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 77b74336e..f1fde1720 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -1011,6 +1011,7 @@ def _coerce_exprs(a, b, ctx=None):
b = s.cast(b)
return (a, b)
+
def _reduce(f, l, a):
r = a
for e in l:
@@ -1296,7 +1297,7 @@ class BoolSortRef(SortRef):
if isinstance(val, bool):
return BoolVal(val, self.ctx)
if __debug__:
- _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected")
+ _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected. Received %s" % val)
_z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
return val
@@ -2012,7 +2013,7 @@ class ArithSortRef(SortRef):
if self.is_real():
return RealVal(val, self.ctx)
if __debug__:
- _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected")
+ _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s" % self)
def is_arith_sort(s):
"""Return `True` if s is an arithmetical sort (type).
@@ -9660,6 +9661,29 @@ def Length(s):
s = _coerce_seq(s)
return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx)
+def StrToInt(s):
+ """Convert string expression to integer
+ >>> a = StrToInt("1")
+ >>> simplify(1 == a)
+ True
+ >>> b = StrToInt("2")
+ >>> simplify(1 == b)
+ False
+ >>> c = StrToInt(IntToStr(2))
+ >>> simplify(1 == c)
+ False
+ """
+ s = _coerce_seq(s)
+ return ArithRef(Z3_mk_str_to_int(s.ctx_ref(), s.as_ast()), s.ctx)
+
+
+def IntToStr(s):
+ """Convert integer expression to string"""
+ if not is_expr(s):
+ s = _py2expr(s)
+ return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx)
+
+
def Re(s, ctx=None):
"""The regular expression that accepts sequence 's'
>>> s1 = Re("ab")
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 65c155d63..ee35c002e 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1152,6 +1152,10 @@ typedef enum {
Z3_OP_SEQ_TO_RE,
Z3_OP_SEQ_IN_RE,
+ // strings
+ Z3_OP_STR_TO_INT,
+ Z3_OP_INT_TO_STR,
+
// regular expressions
Z3_OP_RE_PLUS,
Z3_OP_RE_STAR,
@@ -3325,6 +3329,21 @@ extern "C" {
*/
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset);
+ /**
+ \brief Convert string to integer.
+
+ def_API('Z3_mk_str_to_int' ,AST ,(_in(CONTEXT), _in(AST)))
+ */
+ Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s);
+
+
+ /**
+ \brief Integer to string conversion.
+
+ def_API('Z3_mk_int_to_str' ,AST ,(_in(CONTEXT), _in(AST)))
+ */
+ Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s);
+
/**
\brief Create a regular expression that accepts the sequence \c seq.
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 440179ba8..7be7300a2 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -2326,6 +2326,22 @@ bool ast_manager::is_pattern(expr const * n) const {
return true;
}
+
+bool ast_manager::is_pattern(expr const * n, ptr_vector &args) {
+ if (!is_app_of(n, m_pattern_family_id, OP_PATTERN)) {
+ return false;
+ }
+ for (unsigned i = 0; i < to_app(n)->get_num_args(); ++i) {
+ expr *arg = to_app(n)->get_arg(i);
+ if (!is_app(arg)) {
+ return false;
+ }
+ args.push_back(arg);
+ }
+ return true;
+}
+
+
quantifier * ast_manager::mk_quantifier(bool forall, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names,
expr * body, int weight , symbol const & qid, symbol const & skid,
unsigned num_patterns, expr * const * patterns,
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 47ea0f812..9259d5431 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1840,6 +1840,8 @@ public:
bool is_pattern(expr const * n) const;
+ bool is_pattern(expr const *n, ptr_vector &args);
+
public:
quantifier * mk_quantifier(bool forall, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body,
diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp
index 91963fa0d..2f7b1ea6e 100644
--- a/src/cmd_context/tactic_cmds.cpp
+++ b/src/cmd_context/tactic_cmds.cpp
@@ -165,7 +165,21 @@ public:
}
};
-typedef simple_check_sat_result check_sat_tactic_result;
+struct check_sat_tactic_result : public simple_check_sat_result {
+public:
+ labels_vec labels;
+
+ check_sat_tactic_result(ast_manager & m) : simple_check_sat_result(m) {
+ }
+
+ virtual void get_labels(svector & r) {
+ r.append(labels);
+ }
+
+ virtual void add_labels(svector & r) {
+ labels.append(r);
+ }
+};
class check_sat_using_tactict_cmd : public exec_given_tactic_cmd {
public:
@@ -189,6 +203,7 @@ public:
ast_manager & m = ctx.m();
unsigned timeout = p.get_uint("timeout", ctx.params().m_timeout);
unsigned rlimit = p.get_uint("rlimit", ctx.params().m_rlimit);
+ labels_vec labels;
goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores());
assert_exprs_from(ctx, *g);
TRACE("check_sat_using", g->display(tout););
@@ -208,7 +223,7 @@ public:
cmd_context::scoped_watch sw(ctx);
lbool r = l_undef;
try {
- r = check_sat(t, g, md, pr, core, reason_unknown);
+ r = check_sat(t, g, md, result->labels, pr, core, reason_unknown);
ctx.display_sat_result(r);
result->set_status(r);
if (r == l_undef) {
diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index c9e0ddc69..bd2c72c3e 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -204,7 +204,9 @@ public:
if (in->models_enabled()) {
model_ref md;
m_ctx->get_model(md);
- mc = model2model_converter(md.get());
+ buffer r;
+ m_ctx->get_relevant_labels(0, r);
+ mc = model_and_labels2model_converter(md.get(), r);
mc = concat(fmc.get(), mc.get());
}
return;
@@ -251,7 +253,9 @@ public:
if (in->models_enabled()) {
model_ref md;
m_ctx->get_model(md);
- mc = model2model_converter(md.get());
+ buffer r;
+ m_ctx->get_relevant_labels(0, r);
+ mc = model_and_labels2model_converter(md.get(), r);
}
return;
default:
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 150b19395..b0a4c0e4f 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -146,8 +146,9 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
proof_ref pr(m);
expr_dependency_ref core(m);
std::string reason_unknown = "unknown";
+ labels_vec labels;
try {
- switch (::check_sat(*m_tactic, g, md, pr, core, reason_unknown)) {
+ switch (::check_sat(*m_tactic, g, md, labels, pr, core, reason_unknown)) {
case l_true:
m_result->set_status(l_true);
break;
diff --git a/src/tactic/filter_model_converter.cpp b/src/tactic/filter_model_converter.cpp
index ba6ee4f0d..247f2e91d 100644
--- a/src/tactic/filter_model_converter.cpp
+++ b/src/tactic/filter_model_converter.cpp
@@ -51,6 +51,9 @@ void filter_model_converter::operator()(model_ref & old_model, unsigned goal_idx
TRACE("filter_mc", tout << "after filter_model_converter\n"; model_v2_pp(tout, *old_model););
}
+void filter_model_converter::operator()(svector & labels, unsigned goal_idx) {
+}
+
void filter_model_converter::display(std::ostream & out) {
out << "(filter-model-converter";
for (unsigned i = 0; i < m_decls.size(); i++) {
diff --git a/src/tactic/filter_model_converter.h b/src/tactic/filter_model_converter.h
index 6fc8fdd77..0b67a6c5a 100644
--- a/src/tactic/filter_model_converter.h
+++ b/src/tactic/filter_model_converter.h
@@ -32,6 +32,8 @@ public:
virtual void operator()(model_ref & md, unsigned goal_idx);
+ virtual void operator()(svector & labels, unsigned goal_idx);
+
virtual void operator()(model_ref & md) { operator()(md, 0); } // TODO: delete
virtual void cancel() {}
diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp
index 7ac3e898a..6f6dd3da1 100644
--- a/src/tactic/model_converter.cpp
+++ b/src/tactic/model_converter.cpp
@@ -33,6 +33,12 @@ public:
this->m_c1->operator()(m, 0);
}
+ virtual void operator()(labels_vec & r, unsigned goal_idx) {
+ this->m_c2->operator()(r, goal_idx);
+ this->m_c1->operator()(r, 0);
+ }
+
+
virtual char const * get_name() const { return "concat-model-converter"; }
virtual model_converter * translate(ast_translation & translator) {
@@ -76,6 +82,24 @@ public:
}
UNREACHABLE();
}
+
+ virtual void operator()(labels_vec & r, unsigned goal_idx) {
+ unsigned num = this->m_c2s.size();
+ for (unsigned i = 0; i < num; i++) {
+ if (goal_idx < this->m_szs[i]) {
+ // found the model converter that should be used
+ model_converter * c2 = this->m_c2s[i];
+ if (c2)
+ c2->operator()(r, goal_idx);
+ if (m_c1)
+ this->m_c1->operator()(r, i);
+ return;
+ }
+ // invalid goal
+ goal_idx -= this->m_szs[i];
+ }
+ UNREACHABLE();
+ }
virtual char const * get_name() const { return "concat-star-model-converter"; }
@@ -102,8 +126,12 @@ model_converter * concat(model_converter * mc1, unsigned num, model_converter *
class model2mc : public model_converter {
model_ref m_model;
+ buffer m_labels;
public:
model2mc(model * m):m_model(m) {}
+
+ model2mc(model * m, buffer const & r):m_model(m), m_labels(r) {}
+
virtual ~model2mc() {}
virtual void operator()(model_ref & m) {
@@ -114,7 +142,11 @@ public:
m = m_model;
}
- virtual void cancel() {
+ virtual void operator()(labels_vec & r, unsigned goal_idx) {
+ r.append(m_labels.size(), m_labels.c_ptr());
+ }
+
+ virtual void cancel() {
}
virtual void display(std::ostream & out) {
@@ -135,6 +167,12 @@ model_converter * model2model_converter(model * m) {
return alloc(model2mc, m);
}
+model_converter * model_and_labels2model_converter(model * m, buffer & r) {
+ if (m == 0)
+ return 0;
+ return alloc(model2mc, m, r);
+}
+
void model_converter2model(ast_manager & mng, model_converter * mc, model_ref & m) {
if (mc) {
m = alloc(model, mng);
diff --git a/src/tactic/model_converter.h b/src/tactic/model_converter.h
index 00c50a15f..e2bc3cf83 100644
--- a/src/tactic/model_converter.h
+++ b/src/tactic/model_converter.h
@@ -23,6 +23,8 @@ Notes:
#include"converter.h"
#include"ref.h"
+class labels_vec : public svector {};
+
class model_converter : public converter {
public:
virtual void operator()(model_ref & m) {} // TODO: delete
@@ -32,6 +34,8 @@ public:
SASSERT(goal_idx == 0);
operator()(m);
}
+
+ virtual void operator()(labels_vec & r, unsigned goal_idx) {}
virtual model_converter * translate(ast_translation & translator) = 0;
};
@@ -49,6 +53,8 @@ model_converter * concat(model_converter * mc1, unsigned num, model_converter *
model_converter * model2model_converter(model * m);
+model_converter * model_and_labels2model_converter(model * m, buffer &r);
+
void model_converter2model(ast_manager & mng, model_converter * mc, model_ref & m);
void apply(model_converter_ref & mc, model_ref & m, unsigned gidx);
diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp
new file mode 100644
index 000000000..f2d6a9653
--- /dev/null
+++ b/src/tactic/sine_filter.cpp
@@ -0,0 +1,245 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+ sine_filter.cpp
+
+Abstract:
+
+ Tactic that performs Sine Qua Non premise selection
+
+Author:
+
+ Doug Woos
+
+Revision History:
+--*/
+
+#include "sine_filter.h"
+#include "tactical.h"
+#include "filter_model_converter.h"
+#include "datatype_decl_plugin.h"
+#include "rewriter_def.h"
+#include "filter_model_converter.h"
+#include "extension_model_converter.h"
+#include "var_subst.h"
+#include "ast_util.h"
+#include "obj_pair_hashtable.h"
+#include "ast_pp.h"
+
+class sine_tactic : public tactic {
+
+ ast_manager& m;
+ params_ref m_params;
+
+public:
+
+ sine_tactic(ast_manager& m, params_ref const& p):
+ m(m), m_params(p) {}
+
+ virtual tactic * translate(ast_manager & m) {
+ return alloc(sine_tactic, m, m_params);
+ }
+
+ virtual void updt_params(params_ref const & p) {
+ }
+
+ virtual void collect_param_descrs(param_descrs & r) {
+ }
+
+ virtual 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;
+
+ TRACE("sine", g->display(tout););
+ TRACE("sine", tout << g->size(););
+ ptr_vector new_forms;
+ filter_expressions(g, new_forms);
+ TRACE("sine", tout << new_forms.size(););
+ g->reset();
+ for (unsigned i = 0; i < new_forms.size(); i++) {
+ g->assert_expr(new_forms.get(i), 0, 0);
+ }
+ g->inc_depth();
+ g->updt_prec(goal::OVER);
+ result.push_back(g.get());
+ TRACE("sine", result[0]->display(tout););
+ SASSERT(g->is_well_sorted());
+ filter_model_converter * fmc = alloc(filter_model_converter, m);
+ mc = fmc;
+ }
+
+ virtual void cleanup() {
+ }
+
+private:
+
+ typedef std::pair t_work_item;
+
+ t_work_item work_item(expr *e, expr *root) {
+ return std::pair(e, root);
+ }
+
+ void find_constants(expr *e, obj_hashtable &consts) {
+ ptr_vector stack;
+ stack.push_back(e);
+ expr *curr;
+ while (!stack.empty()) {
+ curr = stack.back();
+ stack.pop_back();
+ if (is_app(curr)) {
+ app *a = to_app(curr);
+ if (is_uninterp(a)) {
+ func_decl *f = a->get_decl();
+ consts.insert_if_not_there(f);
+ }
+ }
+ }
+ }
+
+ bool quantifier_matches(quantifier *q,
+ obj_hashtable const & consts,
+ ptr_vector & next_consts) {
+ TRACE("sine", tout << "size of consts is "; tout << consts.size(); tout << "\n";);
+ for (obj_hashtable::iterator constit = consts.begin(), constend = consts.end(); constit != constend; constit++) {
+ TRACE("sine", tout << *constit; tout << "\n";);
+ }
+ bool matched = false;
+ for (unsigned i = 0; i < q->get_num_patterns(); i++) {
+ bool p_matched = true;
+ ptr_vector stack;
+ expr *curr;
+ // patterns are wrapped with "pattern"
+ if (!m.is_pattern(q->get_pattern(i), stack)) {
+ continue;
+ }
+ while (!stack.empty()) {
+ curr = stack.back();
+ stack.pop_back();
+ if (is_app(curr)) {
+ app *a = to_app(curr);
+ func_decl *f = a->get_decl();
+ if (!consts.contains(f)) {
+ TRACE("sine", tout << mk_pp(f, m) << "\n";);
+ p_matched = false;
+ next_consts.push_back(f);
+ break;
+ }
+ for (unsigned j = 0; j < a->get_num_args(); j++) {
+ stack.push_back(a->get_arg(j));
+ }
+ }
+ }
+ if (p_matched) {
+ matched = true;
+ break;
+ }
+ }
+ return matched;
+ }
+
+ void filter_expressions(goal_ref const & g, ptr_vector & new_exprs) {
+ obj_map > const2exp;
+ obj_map > exp2const;
+ obj_map > const2quantifier;
+ obj_hashtable consts;
+ vector stack;
+ for (unsigned i = 0; i < g->size(); i++) {
+ stack.push_back(work_item(g->form(i), g->form(i)));
+ }
+ t_work_item curr;
+ while (!stack.empty()) {
+ curr = stack.back();
+ stack.pop_back();
+ if (is_app(curr.first)) {
+ app *a = to_app(curr.first);
+ if (is_uninterp(a)) {
+ func_decl *f = a->get_decl();
+ if (!consts.contains(f)) {
+ consts.insert(f);
+ if (const2quantifier.contains(f)) {
+ for (obj_pair_hashtable::iterator it = const2quantifier[f].begin(), end = const2quantifier[f].end(); it != end; it++) {
+ stack.push_back(*it);
+ }
+ const2quantifier.remove(f);
+ }
+ }
+ if (!const2exp.contains(f)) {
+ const2exp.insert(f, obj_hashtable());
+ }
+ if (!const2exp[f].contains(curr.second)) {
+ const2exp[f].insert(curr.second);
+ }
+ if (!exp2const.contains(curr.second)) {
+ exp2const.insert(curr.second, obj_hashtable());
+ }
+ if (!exp2const[curr.second].contains(f)) {
+ exp2const[curr.second].insert(f);
+ }
+ }
+ for (unsigned i = 0; i < a->get_num_args(); i++) {
+ stack.push_back(work_item(a->get_arg(i), curr.second));
+ }
+ }
+ else if (is_quantifier(curr.first)) {
+ quantifier *q = to_quantifier(curr.first);
+ if (q->is_forall()) {
+ if (q->has_patterns()) {
+ ptr_vector next_consts;
+ if (quantifier_matches(q, consts, next_consts)) {
+ stack.push_back(work_item(q->get_expr(), curr.second));
+ }
+ else {
+ for (unsigned i = 0; i < next_consts.size(); i++) {
+ func_decl *c = next_consts.get(i);
+ if (!const2quantifier.contains(c)) {
+ const2quantifier.insert(c, obj_pair_hashtable());
+ }
+ if (!const2quantifier[c].contains(curr)) {
+ const2quantifier[c].insert(curr);
+ }
+ }
+ }
+ }
+ else {
+ stack.push_back(work_item(q->get_expr(), curr.second));
+ }
+ }
+ else if (q->is_exists()) {
+ stack.push_back(work_item(q->get_expr(), curr.second));
+ }
+ }
+ }
+ // ok, now we just need to find the connected component of the last term
+
+ obj_hashtable visited;
+ ptr_vector to_visit;
+ to_visit.push_back(g->form(g->size() - 1));
+ expr *visiting;
+ while (!to_visit.empty()) {
+ visiting = to_visit.back();
+ to_visit.pop_back();
+ visited.insert(visiting);
+ for (obj_hashtable::iterator constit = exp2const[visiting].begin(), constend = exp2const[visiting].end(); constit != constend; constit++) {
+ for (obj_hashtable::iterator exprit = const2exp[*constit].begin(), exprend = const2exp[*constit].end(); exprit != exprend; exprit++) {
+ if (!visited.contains(*exprit)) {
+ to_visit.push_back(*exprit);
+ }
+ }
+ }
+ }
+ for (unsigned i = 0; i < g->size(); i++) {
+ if (visited.contains(g->form(i))) {
+ new_exprs.push_back(g->form(i));
+ }
+ }
+ }
+};
+
+tactic * mk_sine_tactic(ast_manager & m, params_ref const & p) {
+ return alloc(sine_tactic, m, p);
+}
diff --git a/src/tactic/sine_filter.h b/src/tactic/sine_filter.h
new file mode 100644
index 000000000..769ef474f
--- /dev/null
+++ b/src/tactic/sine_filter.h
@@ -0,0 +1,32 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+ sine_filter.h
+
+Abstract:
+
+ Tactic that performs Sine Qua Non premise selection
+
+Author:
+
+ Doug Woos
+
+Revision History:
+
+--*/
+#ifndef SINE_TACTIC_H_
+#define SINE_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_sine_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+/*
+ ADD_TACTIC("sine-filter", "eliminate premises using Sine Qua Non", "mk_sine_tactic(m, p)")
+*/
+
+#endif
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index 2ccb23305..67fce1486 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -175,7 +175,7 @@ void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_conve
}
}
-lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) {
+lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) {
bool models_enabled = g->models_enabled();
bool proofs_enabled = g->proofs_enabled();
bool cores_enabled = g->unsat_core_enabled();
@@ -200,6 +200,8 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_d
if (is_decided_sat(r)) {
if (models_enabled) {
+ if (mc)
+ (*mc)(labels, 0);
model_converter2model(m, mc.get(), md);
if (!md) {
// create empty model.
@@ -216,7 +218,11 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_d
return l_false;
}
else {
- if (models_enabled) model_converter2model(m, mc.get(), md);
+ if (models_enabled) {
+ model_converter2model(m, mc.get(), md);
+ if (mc)
+ (*mc)(labels, 0);
+ }
reason_unknown = "incomplete";
return l_undef;
}
diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h
index a9e50ff10..645b53681 100644
--- a/src/tactic/tactic.h
+++ b/src/tactic/tactic.h
@@ -153,7 +153,7 @@ public:
#define MK_SIMPLE_TACTIC_FACTORY(NAME, ST) MK_TACTIC_FACTORY(NAME, return ST;)
void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core);
-lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown);
+lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown);
// Throws an exception if goal \c in requires proof generation.
void fail_if_proof_generation(char const * tactic_name, goal_ref const & in);