add 'distinct' to MCMT

src/parser/mcmt/mcmt.g

@@ -318,6 +318,8 @@ term returns [expr::term_ref t = expr::term_ref()]
   	  t = STATE->tm().mk_term(expr::TERM_NOT, t);
     }
     ')'
+   // Sally syntactic sugar functions
+  | '(' 'distinct' term_list[children] ')' { t = STATE->mk_distinct(children); }
   ;
 
 let_assignments

src/parser/mcmt/mcmt_state.cpp

@@ -212,6 +212,20 @@ expr::term_ref mcmt_state::mk_cond(const std::vector<expr::term_ref>& children)
   return result;
 }
 
+expr::term_ref mcmt_state::mk_distinct(const std::vector<expr::term_ref>& children) {
+  assert(children.size() >= 2);
+
+  std::vector<expr::term_ref> conjuncts;
+  for (unsigned i = 0; i < children.size(); ++ i) {
+    for (unsigned j = i + 1; j < children.size(); ++ j) {
+      term_ref eq = tm().mk_term(expr::TERM_EQ, children[i], children[j]);
+      conjuncts.push_back(tm().mk_not(eq));
+    }
+  }
+  return tm().mk_and(conjuncts);
+}
+
+
 bool mcmt_state::lsal_extensions() const {
   return ctx().get_options().get_bool("lsal-extensions");
 }

src/parser/mcmt/mcmt_state.h

@@ -117,6 +117,9 @@ class mcmt_state {
    */
   expr::term_ref mk_cond(const std::vector<expr::term_ref>& children);
 
+  /** Make a distinct term */
+  expr::term_ref mk_distinct(const std::vector<expr::term_ref>& children);
+
   /** Get the string of a token begin parsed */
   static
   std::string token_text(pANTLR3_COMMON_TOKEN token);