diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 653e4588b..b73f7a7a8 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -764,7 +764,7 @@ class Component:
out.write('\n')
mk_dir(os.path.join(BUILD_DIR, self.build_dir))
if VS_PAR and IS_WINDOWS:
- cppfiles = get_cpp_files(self.src_dir)
+ cppfiles = list(get_cpp_files(self.src_dir))
dependencies = set()
for cppfile in cppfiles:
dependencies.add(os.path.join(self.to_src_dir, cppfile))
@@ -2591,16 +2591,17 @@ def mk_vs_proj(name, components):
def mk_win_dist(build_path, dist_path):
for c in get_components():
c.mk_win_dist(build_path, dist_path)
- # Add Z3Py to lib directory
- for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(build_path)):
+ # Add Z3Py to bin directory
+ print("Adding to %s\n" % dist_path)
+ for pyc in filter(lambda f: f.endswith('.pyc') or f.endswith('.py'), os.listdir(build_path)):
shutil.copy(os.path.join(build_path, pyc),
os.path.join(dist_path, 'bin', pyc))
def mk_unix_dist(build_path, dist_path):
for c in get_components():
c.mk_unix_dist(build_path, dist_path)
- # Add Z3Py to lib directory
- for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(build_path)):
+ # Add Z3Py to bin directory
+ for pyc in filter(lambda f: f.endswith('.pyc') or f.endswith('.py'), os.listdir(build_path)):
shutil.copy(os.path.join(build_path, pyc),
os.path.join(dist_path, 'bin', pyc))
diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs
index 8c6e6c4c6..3f40b220b 100644
--- a/src/api/dotnet/Fixedpoint.cs
+++ b/src/api/dotnet/Fixedpoint.cs
@@ -269,6 +269,14 @@ namespace Microsoft.Z3
AST.ArrayLength(queries), AST.ArrayToNative(queries));
}
+ BoolExpr[] ToBoolExprs(ASTVector v) {
+ uint n = v.Size;
+ BoolExpr[] res = new BoolExpr[n];
+ for (uint i = 0; i < n; i++)
+ res[i] = new BoolExpr(Context, v[i].NativeObject);
+ return res;
+ }
+
///
/// Retrieve set of rules added to fixedpoint context.
///
@@ -278,12 +286,7 @@ namespace Microsoft.Z3
{
Contract.Ensures(Contract.Result() != null);
- ASTVector v = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject));
- uint n = v.Size;
- BoolExpr[] res = new BoolExpr[n];
- for (uint i = 0; i < n; i++)
- res[i] = new BoolExpr(Context, v[i].NativeObject);
- return res;
+ return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject)));
}
}
@@ -296,15 +299,27 @@ namespace Microsoft.Z3
{
Contract.Ensures(Contract.Result() != null);
- ASTVector v = new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject));
- uint n = v.Size;
- BoolExpr[] res = new BoolExpr[n];
- for (uint i = 0; i < n; i++)
- res[i] = new BoolExpr(Context, v[i].NativeObject);
- return res;
+ return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject)));
}
}
+ ///
+ /// Parse an SMT-LIB2 file with fixedpoint rules.
+ /// Add the rules to the current fixedpoint context.
+ /// Return the set of queries in the file.
+ ///
+ public BoolExpr[] ParseFile(string file) {
+ return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file)));
+ }
+
+ ///
+ /// Similar to ParseFile. Instead it takes as argument a string.
+ ///
+
+ public BoolExpr[] ParseString(string s) {
+ return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s)));
+ }
+
#region Internal
internal Fixedpoint(Context ctx, IntPtr obj)
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index b29a9c87d..94e20eceb 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -5668,7 +5668,8 @@ END_MLAPI_EXCLUDE
Each conjunct encodes values of the bound variables of the query that are satisfied.
In PDR mode, the returned answer is a single conjunction.
- The previous call to Z3_fixedpoint_query must have returned Z3_L_TRUE.
+ When used in Datalog mode the previous call to Z3_fixedpoint_query must have returned Z3_L_TRUE.
+ When used with the PDR engine, the previous call must have been either Z3_L_TRUE or Z3_L_FALSE.
def_API('Z3_fixedpoint_get_answer', AST, (_in(CONTEXT), _in(FIXEDPOINT)))
*/
diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index f684879ae..59e5c04b9 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -569,8 +569,8 @@ class smt_printer {
m_out << ")";
}
- if (m_is_smt2 && q->get_num_patterns() > 0) {
- m_out << "(!";
+ if (m_is_smt2 && (q->get_num_patterns() > 0 || q->get_qid() != symbol::null)) {
+ m_out << "(! ";
}
{
smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, false, m_is_smt2, m_simplify_implies, m_indent, m_num_var_names, m_var_names);
@@ -609,7 +609,11 @@ class smt_printer {
m_out << "}";
}
}
- if (m_is_smt2 && q->get_num_patterns() > 0) {
+
+ if (q->get_qid() != symbol::null)
+ m_out << " :qid " << q->get_qid();
+
+ if (m_is_smt2 && (q->get_num_patterns() > 0 || q->get_qid() != symbol::null)) {
m_out << ")";
}
m_out << ")";
diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp
index 084a33ebf..b26b7faba 100644
--- a/src/ast/macros/quasi_macros.cpp
+++ b/src/ast/macros/quasi_macros.cpp
@@ -41,7 +41,7 @@ void quasi_macros::find_occurrences(expr * e) {
// we remember whether we have seen an expr once, or more than once;
// when we see it the second time, we don't have to visit it another time,
- // as we are only intersted in finding unique function applications.
+ // as we are only interested in finding unique function applications.
m_visited_once.reset();
m_visited_more.reset();
@@ -61,7 +61,7 @@ void quasi_macros::find_occurrences(expr * e) {
case AST_VAR: break;
case AST_QUANTIFIER: m_todo.push_back(to_quantifier(cur)->get_expr()); break;
case AST_APP:
- if (is_uninterp(cur) && !is_ground(cur)) {
+ if (is_non_ground_uninterp(cur)) {
func_decl * f = to_app(cur)->get_decl();
m_occurrences.insert_if_not_there(f, 0);
occurrences_map::iterator it = m_occurrences.find_iterator(f);
@@ -76,6 +76,10 @@ void quasi_macros::find_occurrences(expr * e) {
}
};
+bool quasi_macros::is_non_ground_uninterp(expr const * e) const {
+ return is_non_ground(e) && is_uninterp(e);
+}
+
bool quasi_macros::is_unique(func_decl * f) const {
return m_occurrences.find(f) == 1;
}
@@ -149,6 +153,7 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
// Our definition of a quasi-macro:
// Forall X. f[X] = T[X], where f[X] is a term starting with symbol f, f is uninterpreted,
// f[X] contains all universally quantified variables, and f does not occur in T[X].
+ TRACE("quasi_macros", tout << "Checking for quasi macro: " << mk_pp(e, m_manager) << std::endl;);
if (is_quantifier(e) && to_quantifier(e)->is_forall()) {
quantifier * q = to_quantifier(e);
@@ -157,23 +162,23 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
expr * lhs = to_app(qe)->get_arg(0);
expr * rhs = to_app(qe)->get_arg(1);
- if (is_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) &&
+ if (is_non_ground_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) &&
!depends_on(rhs, to_app(lhs)->get_decl()) && fully_depends_on(to_app(lhs), q)) {
a = to_app(lhs);
t = rhs;
return true;
- } else if (is_uninterp(rhs) && is_unique(to_app(rhs)->get_decl()) &&
+ } else if (is_non_ground_uninterp(rhs) && is_unique(to_app(rhs)->get_decl()) &&
!depends_on(lhs, to_app(rhs)->get_decl()) && fully_depends_on(to_app(rhs), q)) {
a = to_app(rhs);
t = lhs;
return true;
}
- } else if (m_manager.is_not(qe) && is_uninterp(to_app(qe)->get_arg(0)) &&
+ } else if (m_manager.is_not(qe) && is_non_ground_uninterp(to_app(qe)->get_arg(0)) &&
is_unique(to_app(to_app(qe)->get_arg(0))->get_decl())) { // this is like f(...) = false
a = to_app(to_app(qe)->get_arg(0));
t = m_manager.mk_false();
return true;
- } else if (is_uninterp(qe) && is_unique(to_app(qe)->get_decl())) { // this is like f(...) = true
+ } else if (is_non_ground_uninterp(qe) && is_unique(to_app(qe)->get_decl())) { // this is like f(...) = true
a = to_app(qe);
t = m_manager.mk_true();
return true;
diff --git a/src/ast/macros/quasi_macros.h b/src/ast/macros/quasi_macros.h
index c5e6b6d4f..64e72e348 100644
--- a/src/ast/macros/quasi_macros.h
+++ b/src/ast/macros/quasi_macros.h
@@ -45,6 +45,7 @@ class quasi_macros {
expr_mark m_visited_more;
bool is_unique(func_decl * f) const;
+ bool is_non_ground_uninterp(expr const * e) const;
bool fully_depends_on(app * a, quantifier * q) const;
bool depends_on(expr * e, func_decl * f) const;
diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp
index 184a5fa02..017bac724 100644
--- a/src/muz/base/dl_rule.cpp
+++ b/src/muz/base/dl_rule.cpp
@@ -978,13 +978,14 @@ namespace datalog {
}
}
- void rule::get_vars(ptr_vector& sorts) const {
+ void rule::get_vars(ast_manager& m, ptr_vector& sorts) const {
sorts.reset();
used_vars used;
get_used_vars(used);
unsigned sz = used.get_max_found_var_idx_plus_1();
for (unsigned i = 0; i < sz; ++i) {
- sorts.push_back(used.get(i));
+ sort* s = used.get(i);
+ sorts.push_back(s?s:m.mk_bool_sort());
}
}
diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h
index 1c31dc6b4..7104bae1f 100644
--- a/src/muz/base/dl_rule.h
+++ b/src/muz/base/dl_rule.h
@@ -304,7 +304,7 @@ namespace datalog {
void norm_vars(rule_manager & rm);
- void get_vars(ptr_vector& sorts) const;
+ void get_vars(ast_manager& m, ptr_vector& sorts) const;
void to_formula(expr_ref& result) const;
diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp
index 218f9906a..a6647a1d2 100644
--- a/src/muz/base/dl_util.cpp
+++ b/src/muz/base/dl_util.cpp
@@ -290,7 +290,7 @@ namespace datalog {
}
}
TRACE("dl_dr",
- tout << r.get_decl()->get_name() << "\n";
+ tout << mk_pp(r.get_head(), m) << " :- \n";
for (unsigned i = 0; i < body.size(); ++i) {
tout << mk_pp(body[i].get(), m) << "\n";
});
diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp
index 0dcbf4644..51b1a5295 100644
--- a/src/muz/bmc/dl_bmc_engine.cpp
+++ b/src/muz/bmc/dl_bmc_engine.cpp
@@ -148,7 +148,7 @@ namespace datalog {
void mk_qrule_vars(datalog::rule const& r, unsigned rule_id, expr_ref_vector& sub) {
ptr_vector sorts;
- r.get_vars(sorts);
+ r.get_vars(m, sorts);
// populate substitution of bound variables.
sub.reset();
sub.resize(sorts.size());
@@ -421,7 +421,7 @@ namespace datalog {
ptr_vector rule_vars;
expr_ref_vector args(m), conjs(m);
- r.get_vars(rule_vars);
+ r.get_vars(m, rule_vars);
obj_hashtable used_vars;
unsigned num_vars = 0;
for (unsigned i = 0; i < r.get_decl()->get_arity(); ++i) {
@@ -514,7 +514,7 @@ namespace datalog {
unsigned sz = r->get_uninterpreted_tail_size();
ptr_vector rule_vars;
- r->get_vars(rule_vars);
+ r->get_vars(m, rule_vars);
args.append(prop->get_num_args(), prop->get_args());
expr_ref_vector sub = mk_skolem_binding(*r, rule_vars, args);
if (sub.empty() && sz == 0) {
@@ -803,7 +803,7 @@ namespace datalog {
func_decl* p = r.get_decl();
ptr_vector const& succs = *dtu.get_datatype_constructors(m.get_sort(path));
// populate substitution of bound variables.
- r.get_vars(sorts);
+ r.get_vars(m, sorts);
sub.reset();
sub.resize(sorts.size());
for (unsigned k = 0; k < r.get_decl()->get_arity(); ++k) {
@@ -1327,7 +1327,7 @@ namespace datalog {
void mk_rule_vars(rule& r, unsigned level, unsigned rule_id, expr_ref_vector& sub) {
ptr_vector sorts;
- r.get_vars(sorts);
+ r.get_vars(m, sorts);
// populate substitution of bound variables.
sub.reset();
sub.resize(sorts.size());
diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp
index 9303181b6..641d40779 100644
--- a/src/muz/transforms/dl_mk_array_blast.cpp
+++ b/src/muz/transforms/dl_mk_array_blast.cpp
@@ -87,7 +87,7 @@ namespace datalog {
else {
if (m_next_var == 0) {
ptr_vector vars;
- r.get_vars(vars);
+ r.get_vars(m, vars);
m_next_var = vars.size() + 1;
}
v = m.mk_var(m_next_var, m.get_sort(e));
diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp
index 112541541..fd1dbb205 100644
--- a/src/muz/transforms/dl_mk_bit_blast.cpp
+++ b/src/muz/transforms/dl_mk_bit_blast.cpp
@@ -26,6 +26,7 @@ Revision History:
#include "dl_mk_interp_tail_simplifier.h"
#include "fixedpoint_params.hpp"
#include "scoped_proof.h"
+#include "model_v2_pp.h"
namespace datalog {
@@ -67,11 +68,17 @@ namespace datalog {
func_decl* p = m_new_funcs[i].get();
func_decl* q = m_old_funcs[i].get();
func_interp* f = model->get_func_interp(p);
+ if (!f) continue;
expr_ref body(m);
unsigned arity_p = p->get_arity();
unsigned arity_q = q->get_arity();
+ TRACE("dl",
+ model_v2_pp(tout, *model);
+ tout << mk_pp(p, m) << "\n";
+ tout << mk_pp(q, m) << "\n";);
SASSERT(0 < arity_p);
- model->register_decl(p, f);
+ SASSERT(f);
+ model->register_decl(p, f->copy());
func_interp* g = alloc(func_interp, m, arity_q);
if (f) {
@@ -88,11 +95,12 @@ namespace datalog {
for (unsigned j = 0; j < arity_q; ++j) {
sort* s = q->get_domain(j);
arg = m.mk_var(j, s);
+ expr* t = arg;
if (m_bv.is_bv_sort(s)) {
- expr* args[1] = { arg };
unsigned sz = m_bv.get_bv_size(s);
for (unsigned k = 0; k < sz; ++k) {
- proj = m.mk_app(m_bv.get_family_id(), OP_BIT2BOOL, 1, args);
+ parameter p(k);
+ proj = m.mk_app(m_bv.get_family_id(), OP_BIT2BOOL, 1, &p, 1, &t);
sub.insert(m.mk_var(idx++, m.mk_bool_sort()), proj);
}
}
diff --git a/src/muz/transforms/dl_mk_coalesce.cpp b/src/muz/transforms/dl_mk_coalesce.cpp
index 8c7f1d5b4..ac7a58d8d 100644
--- a/src/muz/transforms/dl_mk_coalesce.cpp
+++ b/src/muz/transforms/dl_mk_coalesce.cpp
@@ -62,7 +62,7 @@ namespace datalog {
rule_ref r(const_cast(&rl), rm);
ptr_vector sorts;
expr_ref_vector revsub(m), conjs(m);
- rl.get_vars(sorts);
+ rl.get_vars(m, sorts);
revsub.resize(sorts.size());
svector valid(sorts.size(), true);
for (unsigned i = 0; i < sub.size(); ++i) {
@@ -117,8 +117,8 @@ namespace datalog {
rule_ref res(rm);
bool_rewriter bwr(m);
svector is_neg;
- tgt->get_vars(sorts1);
- src.get_vars(sorts2);
+ tgt->get_vars(m, sorts1);
+ src.get_vars(m, sorts2);
mk_pred(head, src.get_head(), tgt->get_head());
for (unsigned i = 0; i < src.get_uninterpreted_tail_size(); ++i) {
diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
index 9c55ca658..fcb8d7b85 100644
--- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
+++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
@@ -199,7 +199,7 @@ namespace datalog {
expr_ref fml(m), cnst(m);
var_ref var(m);
ptr_vector sorts;
- r.get_vars(sorts);
+ r.get_vars(m, sorts);
m_uf.reset();
m_terms.reset();
m_var2cnst.reset();
@@ -207,9 +207,6 @@ namespace datalog {
fml = m.mk_and(conjs.size(), conjs.c_ptr());
for (unsigned i = 0; i < sorts.size(); ++i) {
- if (!sorts[i]) {
- sorts[i] = m.mk_bool_sort();
- }
var = m.mk_var(i, sorts[i]);
cnst = m.mk_fresh_const("C", sorts[i]);
m_var2cnst.insert(var, cnst);
diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp
index d9dad5c56..522bd2e86 100644
--- a/src/muz/transforms/dl_mk_rule_inliner.cpp
+++ b/src/muz/transforms/dl_mk_rule_inliner.cpp
@@ -143,11 +143,8 @@ namespace datalog {
expr_ref_vector result(m);
ptr_vector sorts;
expr_ref v(m), w(m);
- r.get_vars(sorts);
+ r.get_vars(m, sorts);
for (unsigned i = 0; i < sorts.size(); ++i) {
- if (!sorts[i]) {
- sorts[i] = m.mk_bool_sort();
- }
v = m.mk_var(i, sorts[i]);
m_subst.apply(2, m_deltas, expr_offset(v, is_tgt?0:1), w);
result.push_back(w);
@@ -423,6 +420,11 @@ namespace datalog {
}
TRACE("dl", tout << "inlined rules after mutual inlining:\n" << m_inlined_rules; );
+
+ for (unsigned i = 0; i < m_inlined_rules.get_num_rules(); ++i) {
+ rule* r = m_inlined_rules.get_rule(i);
+ datalog::del_rule(m_mc, *r);
+ }
}
bool mk_rule_inliner::transform_rule(rule_set const& orig, rule * r0, rule_set& tgt) {
diff --git a/src/muz/transforms/dl_mk_scale.cpp b/src/muz/transforms/dl_mk_scale.cpp
index 9ada7be20..271bf5f62 100644
--- a/src/muz/transforms/dl_mk_scale.cpp
+++ b/src/muz/transforms/dl_mk_scale.cpp
@@ -141,7 +141,7 @@ namespace datalog {
m_cache.reset();
m_trail.reset();
m_eqs.reset();
- r.get_vars(vars);
+ r.get_vars(m, vars);
unsigned num_vars = vars.size();
for (unsigned j = 0; j < utsz; ++j) {
tail.push_back(mk_pred(num_vars, r.get_tail(j)));
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index d63f0ae00..770a49c07 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -1120,6 +1120,7 @@ namespace qe {
st->init(fml);
st->m_vars.append(m_vars.size(), m_vars.c_ptr());
SASSERT(invariant());
+ TRACE("qe", tout << mk_pp(m_fml, m) << " child: " << mk_pp(fml, m) << "\n";);
return st;
}
@@ -1133,6 +1134,7 @@ namespace qe {
m_branch_index.insert(branch_id, index);
st->m_vars.append(m_vars.size(), m_vars.c_ptr());
SASSERT(invariant());
+ //TRACE("qe", tout << mk_pp(m_fml, m) << " child: " << mk_pp(st->fml(), m) << "\n";);
return st;
}
@@ -1164,6 +1166,16 @@ namespace qe {
}
}
+ expr_ref abstract_variable(app* x, expr* fml) const {
+ expr_ref result(m);
+ expr* y = x;
+ expr_abstract(m, 0, 1, &y, fml, result);
+ symbol X(x->get_decl()->get_name());
+ sort* s = m.get_sort(x);
+ result = m.mk_exists(1, &s, &X, result);
+ return result;
+ }
+
void display_validate(std::ostream& out) const {
if (m_children.empty()) {
return;
@@ -1171,25 +1183,53 @@ namespace qe {
expr_ref q(m);
expr* x = m_var;
if (x) {
- expr_abstract(m, 0, 1, &x, m_fml, q);
- ptr_vector fmls;
+ q = abstract_variable(m_var, m_fml);
+
+ expr_ref_vector fmls(m);
+ expr_ref fml(m);
for (unsigned i = 0; i < m_children.size(); ++i) {
- expr* fml = m_children[i]->fml();
+ search_tree const& child = *m_children[i];
+ fml = child.fml();
if (fml) {
+ // abstract free variables in children.
+ ptr_vector child_vars, new_vars;
+ child_vars.append(child.m_vars.size(), child.m_vars.c_ptr());
+ if (child.m_var) {
+ child_vars.push_back(child.m_var);
+ }
+ for (unsigned j = 0; j < child_vars.size(); ++j) {
+ if (!m_vars.contains(child_vars[j]) &&
+ !new_vars.contains(child_vars[j])) {
+ fml = abstract_variable(child_vars[j], fml);
+ new_vars.push_back(child_vars[j]);
+ }
+ }
fmls.push_back(fml);
}
}
- symbol X(m_var->get_decl()->get_name());
- sort* s = m.get_sort(x);
- q = m.mk_exists(1, &s, &X, q);
- expr_ref tmp(m);
- bool_rewriter(m).mk_or(fmls.size(), fmls.c_ptr(), tmp);
- expr_ref f(m.mk_not(m.mk_iff(q, tmp)), m);
+ bool_rewriter(m).mk_or(fmls.size(), fmls.c_ptr(), fml);
+
+ fml = m.mk_not(m.mk_iff(q, fml));
ast_smt_pp pp(m);
- out << "(echo " << m_var->get_decl()->get_name() << ")\n";
+ out << "; eliminate " << mk_pp(m_var, m) << "\n";
out << "(push)\n";
- pp.display_smt2(out, f);
+ pp.display_smt2(out, fml);
out << "(pop)\n\n";
+ DEBUG_CODE(
+ smt_params params;
+ params.m_simplify_bit2int = true;
+ params.m_arith_enum_const_mod = true;
+ params.m_bv_enable_int2bv2int = true;
+ params.m_relevancy_lvl = 0;
+ smt::kernel ctx(m, params);
+ ctx.assert_expr(fml);
+ lbool is_sat = ctx.check();
+ if (is_sat == l_true) {
+ std::cout << "; Validation failed:\n";
+ std::cout << mk_pp(fml, m) << "\n";
+ }
+);
+
}
for (unsigned i = 0; i < m_children.size(); ++i) {
if (m_children[i]->fml()) {
@@ -1410,13 +1450,9 @@ namespace qe {
m_solver.assert_expr(m_fml);
if (assumption) m_solver.assert_expr(assumption);
bool is_sat = false;
- while (l_false != m_solver.check()) {
+ while (l_true == m_solver.check()) {
is_sat = true;
- model_ref model;
- m_solver.get_model(model);
- TRACE("qe", model_v2_pp(tout, *model););
- model_evaluator model_eval(*model);
- final_check(model_eval);
+ final_check();
}
if (!is_sat) {
@@ -1466,14 +1502,30 @@ namespace qe {
private:
- void final_check(model_evaluator& model_eval) {
- TRACE("qe", tout << "\n";);
- while (can_propagate_assignment(model_eval)) {
- propagate_assignment(model_eval);
- }
- VERIFY(CHOOSE_VAR == update_current(model_eval, true));
- SASSERT(m_current->fml());
- pop(model_eval);
+ void final_check() {
+ model_ref model;
+ m_solver.get_model(model);
+ scoped_ptr model_eval = alloc(model_evaluator, *model);
+
+ while (true) {
+ TRACE("qe", model_v2_pp(tout, *model););
+ while (can_propagate_assignment(*model_eval)) {
+ propagate_assignment(*model_eval);
+ }
+ VERIFY(CHOOSE_VAR == update_current(*model_eval, true));
+ SASSERT(m_current->fml());
+ if (l_true != m_solver.check()) {
+ return;
+ }
+ m_solver.get_model(model);
+ model_eval = alloc(model_evaluator, *model);
+ search_tree* st = m_current;
+ update_current(*model_eval, false);
+ if (st == m_current) {
+ break;
+ }
+ }
+ pop(*model_eval);
}
ast_manager& get_manager() { return m; }
@@ -1633,6 +1685,7 @@ namespace qe {
nb = m_current->get_num_branches();
expr_ref fml(m_current->fml(), m);
if (!eval(model_eval, b, branch) || branch >= nb) {
+ TRACE("qe", tout << "evaluation failed: setting branch to 0\n";);
branch = rational::zero();
}
SASSERT(!branch.is_neg());
@@ -1694,11 +1747,12 @@ namespace qe {
}
//
- // The current state is satisfiable
- // and the closed portion of the formula
- // can be used as the quantifier-free portion.
+ // The closed portion of the formula
+ // can be used as the quantifier-free portion,
+ // unless the current state is unsatisfiable.
//
if (m.is_true(fml_mixed)) {
+ SASSERT(l_true == m_solver.check());
m_current = m_current->add_child(fml_closed);
for (unsigned i = 0; m_defs && i < m_current->num_free_vars(); ++i) {
expr_ref val(m);
@@ -1708,6 +1762,7 @@ namespace qe {
if (val == x) {
model_ref model;
lbool is_sat = m_solver.check();
+ if (is_sat == l_undef) return;
m_solver.get_model(model);
SASSERT(is_sat == l_true);
model_evaluator model_eval2(*model);
@@ -1890,7 +1945,7 @@ namespace qe {
vars.reset();
closed = closed && (r != l_undef);
}
- TRACE("qe", tout << mk_ismt2_pp(fml, m) << "\n";);
+ TRACE("qe", tout << mk_pp(fml, m) << "\n";);
m_current->add_child(fml)->reset_free_vars();
block_assignment();
}
@@ -1959,7 +2014,7 @@ namespace qe {
class quant_elim_new : public quant_elim {
ast_manager& m;
- smt_params& m_fparams;
+ smt_params& m_fparams;
expr_ref m_assumption;
bool m_produce_models;
ptr_vector m_plugins;
diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp
index 7bf0978f6..83c7b79d8 100644
--- a/src/qe/qe_arith_plugin.cpp
+++ b/src/qe/qe_arith_plugin.cpp
@@ -31,6 +31,7 @@ Revision History:
#include "obj_pair_hashtable.h"
#include "nlarith_util.h"
#include "model_evaluator.h"
+#include "smt_kernel.h"
namespace qe {
@@ -80,9 +81,9 @@ namespace qe {
ast_manager& m;
i_solver_context& m_ctx;
public:
- arith_util m_arith; // initialize before m_zero_i, etc.
+ arith_util m_arith; // initialize before m_zero_i, etc.
+ th_rewriter simplify;
private:
- th_rewriter m_rewriter;
arith_eq_solver m_arith_solver;
bv_util m_bv;
@@ -102,7 +103,7 @@ namespace qe {
m(m),
m_ctx(ctx),
m_arith(m),
- m_rewriter(m),
+ simplify(m),
m_arith_solver(m),
m_bv(m),
m_zero_i(m_arith.mk_numeral(numeral(0), true), m),
@@ -434,7 +435,6 @@ namespace qe {
expr_ref tmp(e, m);
simplify(tmp);
m_arith_rewriter.mk_le(tmp, mk_zero(e), result);
- TRACE("qe_verbose", tout << "mk_le " << mk_pp(result, m) << "\n";);
}
void mk_lt(expr* e, expr_ref& result) {
@@ -521,7 +521,8 @@ namespace qe {
expr_ref result1(m), result2(m);
// a*s + b*t <= 0
- expr_ref as_bt_le_0(result, m), tmp2(m), tmp3(m), tmp4(m);
+ expr_ref as_bt_le_0(result, m), tmp2(m), asz_bt_le_0(m), tmp3(m), tmp4(m);
+ expr_ref b_divides_sz(m);
// a*s + b*t + (a-1)(b-1) <= 0
tmp2 = m_arith.mk_add(as_bt, slack);
@@ -560,30 +561,36 @@ namespace qe {
sz = m_arith.mk_uminus(sz);
}
tmp4 = mk_add(mk_mul(a1, sz), bt);
- mk_le(tmp4, tmp3);
+ mk_le(tmp4, asz_bt_le_0);
- if (to_app(tmp3)->get_arg(0) == x &&
- m_arith.is_zero(to_app(tmp3)->get_arg(1))) {
+ if (to_app(asz_bt_le_0)->get_arg(0) == x &&
+ m_arith.is_zero(to_app(asz_bt_le_0)->get_arg(1))) {
// exists z in [0 .. |b|-2] . |b| | (z + s) && z <= 0
// <=>
// |b| | s
mk_divides(abs_b, s, tmp2);
}
else {
- mk_divides(abs_b, sz, tmp2);
- mk_and(tmp2, tmp3, tmp4);
- mk_big_or(abs_b - numeral(2), x, tmp4, tmp2);
-
+ mk_divides(abs_b, sz, b_divides_sz);
+ mk_and(b_divides_sz, asz_bt_le_0, tmp4);
+ mk_big_or(abs_b - numeral(2), x, tmp4, tmp2);
+ TRACE("qe",
+ tout << "b | s + z: " << mk_pp(b_divides_sz, m) << "\n";
+ tout << "a(s+z) + bt <= 0: " << mk_pp(asz_bt_le_0, m) << "\n";
+ );
}
mk_flat_and(as_bt_le_0, tmp2, result2);
mk_or(result1, result2, result);
simplify(result);
+
+
+ // a*s + b*t + (a-1)(b-1) <= 0
+ // or exists z in [0 .. |b|-2] . |b| | (z + s) && a*n_sign(b)(s + z) + |b|t <= 0
}
TRACE("qe",
{
- expr_ref_vector trail(m);
- tout << "is_strict: " << (is_strict?"true":"false") << "\n";
+ tout << (is_strict?"strict":"non-strict") << "\n";
bound(m, a, t, false).pp(tout, x);
tout << "\n";
bound(m, b, s, false).pp(tout, x);
@@ -592,10 +599,6 @@ namespace qe {
});
}
- void simplify(expr_ref& p) {
- m_rewriter(p);
- }
-
struct mul_lt {
arith_util& u;
mul_lt(arith_qe_util& u): u(u.m_arith) {}
@@ -1052,7 +1055,6 @@ namespace qe {
}
bool reduce_equation(expr* p, expr* fml) {
- TRACE("qe", tout << mk_pp(p, m) << "\n";);
numeral k;
if (m_arith.is_numeral(p, k) && k.is_zero()) {
@@ -1555,9 +1557,10 @@ public:
mk_non_resolve(bounds, true, is_lower, result);
mk_non_resolve(bounds, false, is_lower, result);
+ m_util.simplify(result);
add_cache(x, fml, v, result, x_t.get_coeff(), x_t.get_term());
TRACE("qe",
- tout << vl << " " << mk_pp(x, m) << "\n";
+ tout << vl << " " << mk_pp(x, m) << " infinite case\n";
tout << mk_pp(fml, m) << "\n";
tout << mk_pp(result, m) << "\n";);
return;
@@ -1591,19 +1594,22 @@ public:
SASSERT(index < bounds.size(is_strict, is_lower));
expr_ref t(bounds.exprs(is_strict, is_lower)[index], m);
rational a = bounds.coeffs(is_strict, is_lower)[index];
+
- t = x_t.mk_term(a, t);
- a = x_t.mk_coeff(a);
mk_bounds(bounds, x, true, is_eq, is_strict, is_lower, index, a, t, result);
mk_bounds(bounds, x, false, is_eq, is_strict, is_lower, index, a, t, result);
+
+ t = x_t.mk_term(a, t);
+ a = x_t.mk_coeff(a);
mk_resolve(bounds, x, x_t, true, is_eq, is_strict, is_lower, index, a, t, result);
mk_resolve(bounds, x, x_t, false, is_eq, is_strict, is_lower, index, a, t, result);
+ m_util.simplify(result);
add_cache(x, fml, v, result, x_t.get_coeff(), x_t.get_term());
TRACE("qe",
{
- tout << vl << " " << mk_pp(x, m) << "\n";
+ tout << vl << " " << mk_pp(bounds.atoms(is_strict, is_lower)[index],m) << "\n";
tout << mk_pp(fml, m) << "\n";
tout << mk_pp(result, m) << "\n";
}
@@ -2225,6 +2231,12 @@ public:
}
}
m_util.simplify(result);
+ TRACE("qe",
+ tout << (is_strict?"strict":"non-strict") << "\n";
+ tout << (is_lower?"is-lower":"is-upper") << "\n";
+ tout << "a: " << a << " " << mk_pp(t, m) << "\n";
+ tout << "b: " << b << " " << mk_pp(s, m) << "\n";
+ tout << mk_pp(result, m) << "\n";);
}
//
@@ -2245,10 +2257,12 @@ public:
void mk_bounds(bounds_proc& bounds,
- app* x, bool is_strict, bool is_eq_ctx, bool is_strict_ctx, bool is_lower, unsigned index,
+ app* x, bool is_strict, bool is_eq_ctx,
+ bool is_strict_ctx, bool is_lower, unsigned index,
rational const& a, expr* t,
expr_ref& result)
{
+ TRACE("qe", tout << mk_pp(t, m) << "\n";);
SASSERT(!is_eq_ctx || !is_strict_ctx);
unsigned sz = bounds.size(is_strict, is_lower);
expr_ref tmp(m), eq(m);
@@ -2258,13 +2272,14 @@ public:
for (unsigned i = 0; i < sz; ++i) {
app* e = bounds.atoms(is_strict, is_lower)[i];
- expr* s = bounds.exprs(is_strict, is_lower)[i];
+ expr_ref s(bounds.exprs(is_strict, is_lower)[i], m);
rational b = bounds.coeffs(is_strict, is_lower)[i];
if (same_strict && i == index) {
if (non_strict_real) {
m_util.mk_eq(a, x, t, eq);
- TRACE("qe", tout << "a:" << a << " x: " << mk_pp(x, m) << " t: " << mk_pp(t, m) << " eq: " << mk_pp(eq, m) << "\n";);
+ TRACE("qe", tout << "a:" << a << " x: " << mk_pp(x, m) << "t: " <<
+ mk_pp(t, m) << " eq: " << mk_pp(eq, m) << "\n";);
if (is_eq_ctx) {
m_ctx.add_constraint(true, eq);
}
@@ -2292,6 +2307,7 @@ public:
(non_strict_real && is_eq_ctx && is_strict) ||
(same_strict && i < index);
+
mk_bound(result_is_strict, is_lower, a, t, b, s, tmp);
m_util.m_replace.apply_substitution(e, tmp.get(), result);
@@ -2330,14 +2346,17 @@ public:
s = x_t.mk_term(b, s);
b = x_t.mk_coeff(b);
m_util.mk_resolve(x, strict_resolve, a, t, b, s, tmp);
+ expr_ref save_result(result);
m_util.m_replace.apply_substitution(e, tmp.get(), result);
m_ctx.add_constraint(true, mk_not(e), tmp);
TRACE("qe_verbose",
tout << mk_pp(atm, m) << " ";
- tout << mk_pp(e, m) << " ==> ";
+ tout << mk_pp(e, m) << " ==>\n";
tout << mk_pp(tmp, m) << "\n";
+ tout << "old fml: " << mk_pp(save_result, m) << "\n";
+ tout << "new fml: " << mk_pp(result, m) << "\n";
);
}
}
diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp
index 7281a5daa..7287cac2f 100644
--- a/src/smt/params/theory_arith_params.cpp
+++ b/src/smt/params/theory_arith_params.cpp
@@ -22,6 +22,7 @@ Revision History:
void theory_arith_params::updt_params(params_ref const & _p) {
smt_params_helper p(_p);
m_arith_random_initial_value = p.arith_random_initial_value();
+ m_arith_random_seed = p.random_seed();
m_arith_mode = static_cast(p.arith_solver());
m_nl_arith = p.arith_nl();
m_nl_arith_gb = p.arith_nl_gb();
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index a338be50a..8b3021573 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -1198,6 +1198,7 @@ namespace smt {
void theory_bv::relevant_eh(app * n) {
ast_manager & m = get_manager();
context & ctx = get_context();
+ TRACE("bv", tout << "relevant: " << mk_pp(n, m) << "\n";);
if (m.is_bool(n)) {
bool_var v = ctx.get_bool_var(n);
atom * a = get_bv2a(v);
diff --git a/src/tactic/arith/bv2int_rewriter.cpp b/src/tactic/arith/bv2int_rewriter.cpp
index 872981283..00d2f53ad 100644
--- a/src/tactic/arith/bv2int_rewriter.cpp
+++ b/src/tactic/arith/bv2int_rewriter.cpp
@@ -218,6 +218,7 @@ br_status bv2int_rewriter::mk_mod(expr * s, expr * t, expr_ref & result) {
if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
align_sizes(s1, t1, false);
result = m_bv.mk_bv2int(m_bv.mk_bv_urem(s1, t1));
+ TRACE("bv2int_rewriter", tout << mk_pp(result,m()) << "\n";);
return BR_DONE;
}
@@ -232,6 +233,7 @@ br_status bv2int_rewriter::mk_mod(expr * s, expr * t, expr_ref & result) {
u1 = mk_bv_add(s1, u1, false);
align_sizes(u1, t1, false);
result = m_bv.mk_bv2int(m_bv.mk_bv_urem(u1, t1));
+ TRACE("bv2int_rewriter", tout << mk_pp(result,m()) << "\n";);
return BR_DONE;
}
diff --git a/src/tactic/filter_model_converter.cpp b/src/tactic/filter_model_converter.cpp
index da4c71e54..ba6ee4f0d 100644
--- a/src/tactic/filter_model_converter.cpp
+++ b/src/tactic/filter_model_converter.cpp
@@ -43,6 +43,7 @@ void filter_model_converter::operator()(model_ref & old_model, unsigned goal_idx
if (fs.is_marked(f))
continue;
func_interp * fi = old_model->get_func_interp(f);
+ SASSERT(fi);
new_model->register_decl(f, fi->copy());
}
new_model->copy_usort_interps(*old_model);