mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
have quantified tactics work with bound Boolean variables. Adding stubs for match
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
8b506375e4
commit
43e47271f7
|
@ -108,6 +108,7 @@ namespace smt2 {
|
|||
symbol m_check_sat_assuming;
|
||||
symbol m_define_fun_rec;
|
||||
symbol m_define_funs_rec;
|
||||
symbol m_match;
|
||||
symbol m_underscore;
|
||||
|
||||
typedef std::pair<symbol, expr*> named_expr;
|
||||
|
@ -135,7 +136,7 @@ namespace smt2 {
|
|||
|
||||
typedef psort_frame sort_frame;
|
||||
|
||||
enum expr_frame_kind { EF_APP, EF_LET, EF_LET_DECL, EF_QUANT, EF_ATTR_EXPR, EF_PATTERN };
|
||||
enum expr_frame_kind { EF_APP, EF_LET, EF_LET_DECL, EF_QUANT, EF_MATCH, EF_ATTR_EXPR, EF_PATTERN };
|
||||
|
||||
struct expr_frame {
|
||||
expr_frame_kind m_kind;
|
||||
|
@ -172,6 +173,12 @@ namespace smt2 {
|
|||
m_expr_spos(expr_spos) {}
|
||||
};
|
||||
|
||||
struct match_frame : public expr_frame {
|
||||
match_frame():
|
||||
expr_frame(EF_MATCH)
|
||||
{}
|
||||
};
|
||||
|
||||
struct let_frame : public expr_frame {
|
||||
bool m_in_decls;
|
||||
unsigned m_sym_spos;
|
||||
|
@ -389,6 +396,7 @@ namespace smt2 {
|
|||
|
||||
bool curr_id_is_underscore() const { SASSERT(curr_is_identifier()); return curr_id() == m_underscore; }
|
||||
bool curr_id_is_as() const { SASSERT(curr_is_identifier()); return curr_id() == m_as; }
|
||||
bool curr_id_is_match() const { SASSERT(curr_is_identifier()); return curr_id() == m_match; }
|
||||
bool curr_id_is_forall() const { SASSERT(curr_is_identifier()); return curr_id() == m_forall; }
|
||||
bool curr_id_is_exists() const { SASSERT(curr_is_identifier()); return curr_id() == m_exists; }
|
||||
bool curr_id_is_bang() const { SASSERT(curr_is_identifier()); return curr_id() == m_bang; }
|
||||
|
@ -1273,6 +1281,47 @@ namespace smt2 {
|
|||
throw parser_exception("invalid quantifier, list of sorted variables is empty");
|
||||
}
|
||||
|
||||
/**
|
||||
* SMT-LIB 2.6 pattern matches are of the form
|
||||
* (match t ((p1 t1) ··· (pm+1 tm+1)))
|
||||
*/
|
||||
void push_match_frame() {
|
||||
next();
|
||||
#if 0
|
||||
// just use the stack for parsing these for now.
|
||||
void * mem = m_stack.allocate(sizeof(match_frame));
|
||||
new (mem) match_frame();
|
||||
m_num_expr_frames++;
|
||||
#endif
|
||||
parse_expr();
|
||||
expr_ref t(expr_stack().back(), m());
|
||||
expr_stack().pop_back();
|
||||
expr_ref_vector patterns(m()), cases(m());
|
||||
|
||||
check_lparen_next("pattern bindings should be enclosed in a parenthesis");
|
||||
while (!curr_is_rparen()) {
|
||||
check_lparen_next("invalid pattern binding, '(' expected");
|
||||
parse_expr(); // TBD need to parse a pattern here. The sort of 't' provides context for how to interpret _.
|
||||
patterns.push_back(expr_stack().back());
|
||||
expr_stack().pop_back();
|
||||
parse_expr();
|
||||
cases.push_back(expr_stack().back());
|
||||
expr_stack().pop_back();
|
||||
check_rparen_next("invalid pattern binding, ')' expected");
|
||||
}
|
||||
next();
|
||||
expr_stack().push_back(compile_patterns(t, patterns, cases));
|
||||
}
|
||||
|
||||
expr_ref compile_patterns(expr* t, expr_ref_vector const& patterns, expr_ref_vector const& cases) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return expr_ref(m());
|
||||
}
|
||||
|
||||
void pop_match_frame(match_frame * fr) {
|
||||
|
||||
}
|
||||
|
||||
symbol parse_indexed_identifier_core() {
|
||||
check_underscore_next("invalid indexed identifier, '_' expected");
|
||||
check_identifier("invalid indexed identifier, symbol expected");
|
||||
|
@ -1599,6 +1648,9 @@ namespace smt2 {
|
|||
else if (curr_id_is_root_obj()) {
|
||||
parse_root_obj();
|
||||
}
|
||||
else if (curr_id_is_match()) {
|
||||
push_match_frame();
|
||||
}
|
||||
else {
|
||||
push_app_frame();
|
||||
}
|
||||
|
@ -1776,6 +1828,9 @@ namespace smt2 {
|
|||
case EF_QUANT:
|
||||
pop_quant_frame(static_cast<quant_frame*>(fr));
|
||||
break;
|
||||
case EF_MATCH:
|
||||
pop_match_frame(static_cast<match_frame*>(fr));
|
||||
break;
|
||||
case EF_ATTR_EXPR:
|
||||
pop_attr_expr_frame(static_cast<attr_expr_frame*>(fr));
|
||||
break;
|
||||
|
@ -2730,6 +2785,7 @@ namespace smt2 {
|
|||
m_check_sat_assuming("check-sat-assuming"),
|
||||
m_define_fun_rec("define-fun-rec"),
|
||||
m_define_funs_rec("define-funs-rec"),
|
||||
m_match("match"),
|
||||
m_underscore("_"),
|
||||
m_num_open_paren(0),
|
||||
m_current_file(filename) {
|
||||
|
|
|
@ -392,24 +392,27 @@ struct is_non_nira_functor {
|
|||
|
||||
is_non_nira_functor(ast_manager & _m, bool _int, bool _real, bool _quant, bool linear):m(_m), u(m), m_int(_int), m_real(_real), m_quant(_quant), m_linear(linear) {}
|
||||
|
||||
void throw_found() {
|
||||
void throw_found(expr* e) {
|
||||
TRACE("probe", tout << expr_ref(e, m) << ": " << sort_ref(m.get_sort(e), m) << "\n";);
|
||||
throw found();
|
||||
}
|
||||
|
||||
void operator()(var * x) {
|
||||
if (!m_quant)
|
||||
throw_found();
|
||||
throw_found(x);
|
||||
sort * s = x->get_sort();
|
||||
if (m_int && u.is_int(s))
|
||||
return;
|
||||
if (m_real && u.is_real(s))
|
||||
return;
|
||||
throw_found();
|
||||
if (m.is_bool(s))
|
||||
return;
|
||||
throw_found(x);
|
||||
}
|
||||
|
||||
void operator()(quantifier *) {
|
||||
void operator()(quantifier * q) {
|
||||
if (!m_quant)
|
||||
throw_found();
|
||||
throw_found(q);
|
||||
}
|
||||
|
||||
bool compatible_sort(app * n) const {
|
||||
|
@ -424,7 +427,7 @@ struct is_non_nira_functor {
|
|||
|
||||
void operator()(app * n) {
|
||||
if (!compatible_sort(n))
|
||||
throw_found();
|
||||
throw_found(n);
|
||||
family_id fid = n->get_family_id();
|
||||
if (fid == m.get_basic_family_id())
|
||||
return;
|
||||
|
@ -437,39 +440,39 @@ struct is_non_nira_functor {
|
|||
case OP_MUL:
|
||||
if (m_linear) {
|
||||
if (n->get_num_args() != 2)
|
||||
throw_found();
|
||||
throw_found(n);
|
||||
if (!u.is_numeral(n->get_arg(0)))
|
||||
throw_found();
|
||||
throw_found(n);
|
||||
}
|
||||
return;
|
||||
case OP_IDIV: case OP_DIV: case OP_REM: case OP_MOD:
|
||||
if (m_linear && !u.is_numeral(n->get_arg(1)))
|
||||
throw_found();
|
||||
throw_found(n);
|
||||
return;
|
||||
case OP_IS_INT:
|
||||
if (m_real)
|
||||
throw_found();
|
||||
throw_found(n);
|
||||
return;
|
||||
case OP_TO_INT:
|
||||
case OP_TO_REAL:
|
||||
return;
|
||||
case OP_POWER:
|
||||
if (m_linear)
|
||||
throw_found();
|
||||
throw_found(n);
|
||||
return;
|
||||
case OP_IRRATIONAL_ALGEBRAIC_NUM:
|
||||
if (m_linear || !m_real)
|
||||
throw_found();
|
||||
throw_found(n);
|
||||
return;
|
||||
default:
|
||||
throw_found();
|
||||
throw_found(n);
|
||||
}
|
||||
return;
|
||||
}
|
||||
|
||||
if (is_uninterp_const(n))
|
||||
return;
|
||||
throw_found();
|
||||
throw_found(n);
|
||||
}
|
||||
};
|
||||
|
||||
|
|
Loading…
Reference in a new issue