handle case input format

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/cmd_context/extra_cmds/dbg_cmds.cpp

@@ -91,6 +91,11 @@ UNARY_CMD(pp_shared_cmd, "dbg-pp-shared", "<term>", "display shared subterms of
     ctx.regular_stream() << ")" << std::endl;
 });
 
+UNARY_CMD(assert_not_cmd, "assert-not", "<term>", "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", "<term>", "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));

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<symbol, expr*> 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)))         
+         *
+         * precursor form is
+         *
+         *   (match t (case p1 t1) (case p2 t2) ... )
+         *
          */
         void push_match_frame() {
             SASSERT(curr_is_identifier());
@@ -1336,10 +1346,11 @@ namespace smt2 {
             sort* srt = m().get_sort(t);
 
             check_lparen_next("pattern bindings should be enclosed in a parenthesis");
-            while (!curr_is_rparen()) {
+            if (curr_id_is_case()) {
+                while (curr_id_is_case()) {
+                    next();
                     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();
@@ -1349,8 +1360,28 @@ namespace smt2 {
                     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();
+            }
             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) {

src/smt/smt_context.h

@@ -1010,10 +1010,10 @@ namespace smt {
         void restore_theory_vars(enode * r2, enode * r1);
 
         void push_eq(enode * lhs, enode * rhs, eq_justification const & js) {
-            SASSERT(lhs != rhs);
+            if (lhs->get_root() != rhs->get_root()) {
-            SASSERT(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) {
             SASSERT(n1->m_cg == n2);