diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp index 235576735..bdd2c8b97 100644 --- a/src/cmd_context/extra_cmds/dbg_cmds.cpp +++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp @@ -91,6 +91,11 @@ UNARY_CMD(pp_shared_cmd, "dbg-pp-shared", "", "display shared subterms of ctx.regular_stream() << ")" << std::endl; }); +UNARY_CMD(assert_not_cmd, "assert-not", "", "assert negation", CPK_EXPR, expr *, { + expr_ref ne(ctx.m().mk_not(arg), ctx.m()); + ctx.assert_expr(ne); +}); + UNARY_CMD(num_shared_cmd, "dbg-num-shared", "", "return the number of shared subterms", CPK_EXPR, expr *, { shared_occs s(ctx.m()); s(arg); @@ -537,6 +542,7 @@ void install_dbg_cmds(cmd_context & ctx) { ctx.insert(alloc(shift_vars_cmd)); ctx.insert(alloc(pp_shared_cmd)); ctx.insert(alloc(num_shared_cmd)); + ctx.insert(alloc(assert_not_cmd)); ctx.insert(alloc(size_cmd)); ctx.insert(alloc(subst_cmd)); ctx.insert(alloc(bool_rewriter_cmd)); diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 8db6388ab..7458fc578 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -114,6 +114,7 @@ namespace smt2 { symbol m_define_fun_rec; symbol m_define_funs_rec; symbol m_match; + symbol m_case; symbol m_underscore; typedef std::pair named_expr; @@ -382,7 +383,9 @@ namespace smt2 { next(); return; } - throw parser_exception(msg); + std::ostringstream str; + str << msg << " got " << curr_id(); + throw parser_exception(str.str()); } symbol const & curr_id() const { return m_scanner.get_id(); } @@ -406,6 +409,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_case() const { return curr_id() == m_case; } 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_lambda() const { SASSERT(curr_is_identifier()); return curr_id() == m_lambda; } @@ -1319,7 +1323,13 @@ namespace smt2 { /** * SMT-LIB 2.6 pattern matches are of the form - * (match t ((p1 t1) ... (pm+1 tm+1))) + * + * (match t ((p1 t1) ... (pm+1 tm+1))) + * + * precursor form is + * + * (match t (case p1 t1) (case p2 t2) ... ) + * */ void push_match_frame() { SASSERT(curr_is_identifier()); @@ -1336,21 +1346,42 @@ namespace smt2 { sort* srt = m().get_sort(t); check_lparen_next("pattern bindings should be enclosed in a parenthesis"); - while (!curr_is_rparen()) { - m_env.begin_scope(); - unsigned num_bindings = m_num_bindings; - check_lparen_next("invalid pattern binding, '(' expected"); - parse_match_pattern(srt); - patterns.push_back(expr_stack().back()); - expr_stack().pop_back(); - parse_expr(); - cases.push_back(expr_stack().back()); - expr_stack().pop_back(); - m_num_bindings = num_bindings; - m_env.end_scope(); - check_rparen_next("invalid pattern binding, ')' expected"); + if (curr_id_is_case()) { + while (curr_id_is_case()) { + next(); + m_env.begin_scope(); + unsigned num_bindings = m_num_bindings; + parse_match_pattern(srt); + patterns.push_back(expr_stack().back()); + expr_stack().pop_back(); + parse_expr(); + cases.push_back(expr_stack().back()); + expr_stack().pop_back(); + m_num_bindings = num_bindings; + m_env.end_scope(); + check_rparen_next("invalid pattern binding, ')' expected"); + if (curr_is_lparen()) { + next(); + } + } + } + else { + while (!curr_is_rparen()) { + m_env.begin_scope(); + unsigned num_bindings = m_num_bindings; + parse_match_pattern(srt); + patterns.push_back(expr_stack().back()); + expr_stack().pop_back(); + check_lparen_next("invalid pattern binding, '(' expected"); + parse_expr(); + cases.push_back(expr_stack().back()); + expr_stack().pop_back(); + m_num_bindings = num_bindings; + m_env.end_scope(); + check_rparen_next("invalid pattern binding, ')' expected"); + } + next(); } - next(); m_num_expr_frames = num_frames + 1; expr_stack().push_back(compile_patterns(t, patterns, cases)); } @@ -3013,6 +3044,7 @@ namespace smt2 { m_define_fun_rec("define-fun-rec"), m_define_funs_rec("define-funs-rec"), m_match("match"), + m_case("case"), m_underscore("_"), m_num_open_paren(0), m_current_file(filename) { diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index f275b0ebf..f7b7bdbea 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3207,7 +3207,7 @@ namespace smt { } else { set_conflict(b_justification(tmp_clause.first), null_literal); - } + } VERIFY(!resolve_conflict()); return l_false; next_clause: @@ -3770,7 +3770,7 @@ namespace smt { } m_stats.m_num_final_checks++; - TRACE("final_check_stats", tout << "m_stats.m_num_final_checks = " << m_stats.m_num_final_checks << "\n";); + TRACE("final_check_stats", tout << "m_stats.m_num_final_checks = " << m_stats.m_num_final_checks << "\n";); final_check_status ok = m_qmanager->final_check_eh(false); if (ok != FC_DONE) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index a349880e3..c3e9c3ffc 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1010,9 +1010,9 @@ namespace smt { void restore_theory_vars(enode * r2, enode * r1); void push_eq(enode * lhs, enode * rhs, eq_justification const & js) { - SASSERT(lhs != rhs); - SASSERT(lhs->get_root() != rhs->get_root()); - m_eq_propagation_queue.push_back(new_eq(lhs, rhs, js)); + if (lhs->get_root() != rhs->get_root()) { + m_eq_propagation_queue.push_back(new_eq(lhs, rhs, js)); + } } void push_new_congruence(enode * n1, enode * n2, bool used_commutativity) {