diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 681c3d597..fd32a63cc 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -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 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(fr)); break; + case EF_MATCH: + pop_match_frame(static_cast(fr)); + break; case EF_ATTR_EXPR: pop_attr_expr_frame(static_cast(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) { diff --git a/src/tactic/arith/probe_arith.cpp b/src/tactic/arith/probe_arith.cpp index c2de64484..edd4483e7 100644 --- a/src/tactic/arith/probe_arith.cpp +++ b/src/tactic/arith/probe_arith.cpp @@ -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); } };