diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 856060a52..64df1d830 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -2883,9 +2883,9 @@ proof* ast_manager::mk_hyper_resolve(unsigned num_premises, proof* const* premis
ptr_vector<expr> fmls;
SASSERT(positions.size() + 1 == substs.size());
for (unsigned i = 0; i < num_premises; ++i) {
- TRACE("dl", tout << mk_pp(premises[i], *this) << "\n";);
+ TRACE("hyper_res", tout << mk_pp(premises[i], *this) << "\n";);
fmls.push_back(get_fact(premises[i]));
- }
+ }
SASSERT(is_bool(concl));
vector<parameter> params;
for (unsigned i = 0; i < substs.size(); ++i) {
@@ -2898,6 +2898,10 @@ proof* ast_manager::mk_hyper_resolve(unsigned num_premises, proof* const* premis
params.push_back(parameter(positions[i].second));
}
}
+ TRACE("hyper_res",
+ for (unsigned i = 0; i < params.size(); ++i) {
+ params[i].display(tout); tout << "\n";
+ });
ptr_vector<sort> sorts;
ptr_vector<expr> args;
for (unsigned i = 0; i < num_premises; ++i) {
diff --git a/src/muz_qe/dl_util.cpp b/src/muz_qe/dl_util.cpp
index 52080ba73..4b48a1687 100644
--- a/src/muz_qe/dl_util.cpp
+++ b/src/muz_qe/dl_util.cpp
@@ -638,7 +638,16 @@ namespace datalog {
TRACE("dl",
tout << premises[0]->get_id() << " " << mk_pp(premises[0].get(), m) << "\n";
- tout << premises[1]->get_id() << " " << mk_pp(premises[1].get(), m) << "\n";);
+ for (unsigned i = 0; i < s1.size(); ++i) {
+ tout << mk_pp(s1[i], m) << " ";
+ }
+ tout << "\n";
+ tout << premises[1]->get_id() << " " << mk_pp(premises[1].get(), m) << "\n";
+ for (unsigned i = 0; i < s2.size(); ++i) {
+ tout << mk_pp(s2[i], m) << " ";
+ }
+ tout << "\n";
+ );
pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml3, positions, substs);
pc->insert(pr);
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index 629ebaaae..b89e7852f 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -42,6 +42,7 @@ Notes:
#include "dl_mk_rule_inliner.h"
#include "ast_smt2_pp.h"
#include "qe_lite.h"
+#include "ast_ll_pp.h"
namespace pdr {
@@ -398,6 +399,9 @@ namespace pdr {
lbool is_sat = m_solver.check_conjunction_as_assumptions(n.state());
if (is_sat == l_true && core) {
core->reset();
+ TRACE("pdr", tout << "updating model\n";
+ model_smt2_pp(tout, m, *model, 0);
+ tout << mk_pp(n.state(), m) << "\n";);
n.set_model(model);
}
return is_sat;
@@ -758,7 +762,7 @@ namespace pdr {
}
r0 = const_cast<datalog::rule*>(&pt().find_rule(*m_model.get()));
app_ref_vector& inst = pt().get_inst(r0);
- TRACE("pdr", tout << mk_pp(state(), m) << "\n";);
+ TRACE("pdr", tout << mk_pp(state(), m) << " instance: " << inst.size() << "\n";);
for (unsigned i = 0; i < inst.size(); ++i) {
expr* v;
if (model.find(inst[i].get(), v)) {
@@ -1421,6 +1425,7 @@ namespace pdr {
proof_ref proof(m);
SASSERT(m_last_result == l_true);
proof = m_search.get_proof_trace(*this);
+ TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
apply(m, m_pc.get(), proof);
return proof;
}
@@ -1844,7 +1849,7 @@ namespace pdr {
break;
}
case l_true: {
- strm << mk_ismt2_pp(mk_sat_answer(), m);
+ strm << mk_pp(mk_sat_answer(), m);
break;
}
case l_undef: {
diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp
index 3e1ebac46..c4a897503 100644
--- a/src/muz_qe/pdr_util.cpp
+++ b/src/muz_qe/pdr_util.cpp
@@ -126,9 +126,6 @@ void model_evaluator::setup_model(model_ref& model) {
m_refs.push_back(e);
assign_value(e, val);
}
-
- m_level1 = m1.get_level();
- m_level2 = m2.get_level();
}
void model_evaluator::reset() {
@@ -170,11 +167,11 @@ expr_ref_vector model_evaluator::minimize_literals(ptr_vector<expr> const& formu
tout << "formulas:\n";
for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n";
);
-
- setup_model(mdl);
+
expr_ref_vector result(m);
ptr_vector<expr> tocollect;
-
+
+ setup_model(mdl);
collect(formulas, tocollect);
for (unsigned i = 0; i < tocollect.size(); ++i) {
expr* e = tocollect[i];
@@ -301,8 +298,6 @@ void model_evaluator::collect(ptr_vector<expr> const& formulas, ptr_vector<expr>
ptr_vector<expr> todo;
todo.append(formulas);
m_visited.reset();
- m1.set_level(m_level1);
- m2.set_level(m_level2);
VERIFY(check_model(formulas));
@@ -923,13 +918,32 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
arith_util a;
bool m_is_dl;
- // NB. ite terms are non-arihmetical but their then/else branches can be.
- // this gets ignored (also in static_features)
+ bool is_numeric(expr* e) const {
+ if (a.is_numeral(e)) {
+ return true;
+ }
+ expr* cond, *th, *el;
+ if (m.is_ite(e, cond, th, el)) {
+ return is_numeric(th) && is_numeric(el);
+ }
+ return false;
+ }
bool is_arith_expr(expr *e) const {
return is_app(e) && a.get_family_id() == to_app(e)->get_family_id();
}
+ bool is_var_or_numeric(expr* e) const {
+ if (a.is_numeral(e)) {
+ return true;
+ }
+ expr* cond, *th, *el;
+ if (m.is_ite(e, cond, th, el)) {
+ return is_var_or_numeric(th) && is_var_or_numeric(el);
+ }
+ return !is_arith_expr(e);
+ }
+
bool is_minus_one(expr const * e) const {
rational r; return a.is_numeral(e, r) && r.is_minus_one();
}
@@ -939,14 +953,14 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
SASSERT(to_app(e)->get_num_args() == 2);
expr * lhs = to_app(e)->get_arg(0);
expr * rhs = to_app(e)->get_arg(1);
- if (!is_arith_expr(lhs) && !is_arith_expr(rhs))
+ if (is_var_or_numeric(lhs) && is_var_or_numeric(rhs))
return true;
- if (!a.is_numeral(rhs))
+ if (!is_numeric(rhs))
std::swap(lhs, rhs);
- if (!a.is_numeral(rhs))
+ if (!is_numeric(rhs))
return false;
// lhs can be 'x' or '(+ x (* -1 y))'
- if (!is_arith_expr(lhs))
+ if (is_var_or_numeric(lhs))
return true;
expr* arg1, *arg2;
if (!a.is_add(lhs, arg1, arg2))
@@ -960,7 +974,7 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
expr* m1, *m2;
if (!a.is_mul(arg2, m1, m2))
return false;
- return is_minus_one(m1) && !is_arith_expr(m2);
+ return is_minus_one(m1) && is_var_or_numeric(m2);
}
bool test_eq(expr* e) const {
@@ -976,21 +990,21 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
}
bool test_term(expr* e) const {
- if (!is_arith_expr(e)) {
- return true;
- }
if (m.is_bool(e)) {
return true;
}
if (a.is_numeral(e)) {
return true;
}
+ if (is_var_or_numeric(e)) {
+ return true;
+ }
expr* lhs, *rhs;
if (a.is_add(e, lhs, rhs)) {
if (!a.is_numeral(lhs)) {
std::swap(lhs, rhs);
}
- return a.is_numeral(lhs) && !is_arith_expr(rhs);
+ return a.is_numeral(lhs) && is_var_or_numeric(rhs);
}
if (a.is_mul(e, lhs, rhs)) {
return is_minus_one(lhs) || is_minus_one(rhs);
@@ -998,6 +1012,17 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
return false;
}
+ bool is_non_arith_or_basic(expr* e) {
+ if (!is_app(e)) {
+ return false;
+ }
+ family_id fid = to_app(e)->get_family_id();
+ return
+ fid != m.get_basic_family_id() &&
+ fid != null_family_id &&
+ fid != a.get_family_id();
+ }
+
public:
test_diff_logic(ast_manager& m): m(m), a(m), m_is_dl(true) {}
@@ -1011,8 +1036,11 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
else if (m.is_eq(e)) {
m_is_dl = test_eq(e);
}
+ else if (is_non_arith_or_basic(e)) {
+ m_is_dl = false;
+ }
else if (is_app(e)) {
- app* a = to_app(e);
+ app* a = to_app(e);
for (unsigned i = 0; m_is_dl && i < a->get_num_args(); ++i) {
m_is_dl = test_term(a->get_arg(i));
}
diff --git a/src/muz_qe/pdr_util.h b/src/muz_qe/pdr_util.h
index 810831592..1d1e86262 100644
--- a/src/muz_qe/pdr_util.h
+++ b/src/muz_qe/pdr_util.h
@@ -65,10 +65,8 @@ namespace pdr {
//01 -- X
//10 -- false
//11 -- true
- ast_fast_mark1 m1;
- ast_fast_mark2 m2;
- unsigned m_level1;
- unsigned m_level2;
+ expr_mark m1;
+ expr_mark m2;
expr_mark m_visited;
@@ -84,7 +82,7 @@ namespace pdr {
void inherit_value(expr* e, expr* v);
inline bool is_unknown(expr* x) { return !m1.is_marked(x) && !m2.is_marked(x); }
- inline void set_unknown(expr* x) { m1.reset_mark(x); m2.reset_mark(x); }
+ inline void set_unknown(expr* x) { m1.mark(x, false); m2.mark(x, false); }
inline bool is_x(expr* x) { return !m1.is_marked(x) && m2.is_marked(x); }
inline bool is_false(expr* x) { return m1.is_marked(x) && !m2.is_marked(x); }
inline bool is_true(expr* x) { return m1.is_marked(x) && m2.is_marked(x); }
diff --git a/src/muz_qe/qe_datatype_plugin.cpp b/src/muz_qe/qe_datatype_plugin.cpp
index f200262be..c280df964 100644
--- a/src/muz_qe/qe_datatype_plugin.cpp
+++ b/src/muz_qe/qe_datatype_plugin.cpp
@@ -107,6 +107,7 @@ namespace qe {
ast_manager& m;
app_ref_vector m_recognizers;
expr_ref_vector m_eqs;
+ expr_ref_vector m_neqs;
app_ref_vector m_eq_atoms;
app_ref_vector m_neq_atoms;
app_ref_vector m_unsat_atoms;
@@ -117,7 +118,8 @@ namespace qe {
datatype_atoms(ast_manager& m) :
m(m),
m_recognizers(m),
- m_eqs(m),
+ m_eqs(m),
+ m_neqs(m),
m_eq_atoms(m), m_neq_atoms(m), m_unsat_atoms(m), m_eq_conds(m),
m_util(m) {}
@@ -291,6 +293,7 @@ namespace qe {
}
app* a = to_app(a0);
if (a == x) {
+ m_neqs.push_back(b);
return true;
}
if (!m_util.is_constructor(a)) {
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 779960361..f7d75be8c 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -972,6 +972,7 @@ model_value_proc * theory_diff_logic<Ext>::mk_value(enode * n, model_generator &
SASSERT(v != null_theory_var);
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())));
}