mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

throw exceptions when internalizing expressions with free variables, issue #663

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-06-29 16:53:28 -07:00
parent 5d5004193b
commit c2f9d35d59
2 changed files with 21 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_internalizer.cpp
View file

@ -321,10 +321,10 @@ namespace smt {
void context::internalize(expr * n, bool gate_ctx) { void context::internalize(expr * n, bool gate_ctx) {
TRACE("internalize", tout << "internalizing:\n" << mk_pp(n, m_manager) << "\n";); TRACE("internalize", tout << "internalizing:\n" << mk_pp(n, m_manager) << "\n";);
TRACE("internalize_bug", tout << "internalizing:\n" << mk_bounded_pp(n, m_manager) << "\n";); TRACE("internalize_bug", tout << "internalizing:\n" << mk_bounded_pp(n, m_manager) << "\n";);
if (is_var(n)) {
throw default_exception("Formulas should not contain unbound variables");
}
if (m_manager.is_bool(n)) { if (m_manager.is_bool(n)) {
if (is_var(n)) {
throw default_exception("Formulas should not contain unbound variables");
}
SASSERT(is_quantifier(n) || is_app(n)); SASSERT(is_quantifier(n) || is_app(n));
internalize_formula(n, gate_ctx); internalize_formula(n, gate_ctx);
} }

22
src/smt/theory_arith_core.h
View file

@ -268,7 +268,7 @@ namespace smt {
} }
rational _val; rational _val;
expr* arg1, *arg2; expr* arg1, *arg2;
if (m_util.is_mul(m, arg1, arg2) && m_util.is_numeral(arg1, _val)) { if (m_util.is_mul(m, arg1, arg2) && m_util.is_numeral(arg1, _val) && is_app(arg1) && is_app(arg2)) {
SASSERT(m->get_num_args() == 2); SASSERT(m->get_num_args() == 2);
numeral val(_val); numeral val(_val);
theory_var v = internalize_term_core(to_app(arg2)); theory_var v = internalize_term_core(to_app(arg2));
@ -297,6 +297,11 @@ namespace smt {
scoped_row_vars _sc(m_row_vars, m_row_vars_top); scoped_row_vars _sc(m_row_vars, m_row_vars_top);
unsigned num_args = n->get_num_args(); unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) { for (unsigned i = 0; i < num_args; i++) {
if (is_var(n->get_arg(i))) {
std::ostringstream strm;
strm << mk_pp(n, get_manager()) << " contains a free variable";
throw default_exception(strm.str());
}
internalize_internal_monomial(to_app(n->get_arg(i)), r_id); internalize_internal_monomial(to_app(n->get_arg(i)), r_id);
} }
enode * e = mk_enode(n); enode * e = mk_enode(n);
@ -356,6 +361,11 @@ namespace smt {
SASSERT(!val.is_one()); SASSERT(!val.is_one());
unsigned r_id = mk_row(); unsigned r_id = mk_row();
scoped_row_vars _sc(m_row_vars, m_row_vars_top); scoped_row_vars _sc(m_row_vars, m_row_vars_top);
if (is_var(m->get_arg(1))) {
std::ostringstream strm;
strm << mk_pp(m, get_manager()) << " contains a free variable";
throw default_exception(strm.str());
}
if (reflection_enabled()) if (reflection_enabled())
internalize_term_core(to_app(m->get_arg(0))); internalize_term_core(to_app(m->get_arg(0)));
theory_var v = internalize_mul_core(to_app(m->get_arg(1))); theory_var v = internalize_mul_core(to_app(m->get_arg(1)));
@ -1204,6 +1214,9 @@ namespace smt {
kind = A_UPPER; kind = A_UPPER;
else else
kind = A_LOWER; kind = A_LOWER;
if (!is_app(n->get_arg(0)) || !is_app(n->get_arg(1))) {
return false;
}
app * lhs = to_app(n->get_arg(0)); app * lhs = to_app(n->get_arg(0));
app * rhs = to_app(n->get_arg(1)); app * rhs = to_app(n->get_arg(1));
expr * rhs2; expr * rhs2;
@ -1245,10 +1258,11 @@ namespace smt {
template<typename Ext> template<typename Ext>
void theory_arith<Ext>::internalize_eq_eh(app * atom, bool_var v) { void theory_arith<Ext>::internalize_eq_eh(app * atom, bool_var v) {
if (m_params.m_arith_eager_eq_axioms) { expr* _lhs, *_rhs;
if (m_params.m_arith_eager_eq_axioms && get_manager().is_eq(atom, _lhs, _rhs) && is_app(_lhs) && is_app(_rhs)) {
context & ctx = get_context(); context & ctx = get_context();
app * lhs = to_app(atom->get_arg(0)); app * lhs = to_app(_lhs);
app * rhs = to_app(atom->get_arg(1)); app * rhs = to_app(_rhs);
enode * n1 = ctx.get_enode(lhs); enode * n1 = ctx.get_enode(lhs);
enode * n2 = ctx.get_enode(rhs); enode * n2 = ctx.get_enode(rhs);
// The expression atom may be a theory axiom. In this case, it may not be in simplified form. // The expression atom may be a theory axiom. In this case, it may not be in simplified form.