fix distinct operator

This adds support for the distinct operator in SMTlib, by directly translating it into "not equal"

Prior to this change, the distinct operator was ignored, giving incorrect results

Author: polgreen

regression/smt2_solver/distinct/distinct.smt2

@@ -0,0 +1,2 @@
+(assert (distinct (_ bv0 8) (_ bv1 8)))
+(check-sat)

regression/smt2_solver/distinct/test.desc

@@ -0,0 +1,6 @@
+CORE
+distinct.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$

regression/smt2_solver/distinct2/distinct2.smt2

@@ -0,0 +1,2 @@
+(assert (distinct (_ bv0 8) (_ bv1 8)(_ bv2 8) (_ bv1 8)))
+(check-sat)

regression/smt2_solver/distinct2/test.desc

@@ -0,0 +1,6 @@
+CORE
+distinct2.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$

regression/smt2_solver/distinct3/distinct3.smt2

@@ -0,0 +1,2 @@
+(assert (distinct (_ bv0 8)(_ bv0 8)(_ bv2 8) (_ bv2 8)))
+(check-sat)

regression/smt2_solver/distinct3/test.desc

@@ -0,0 +1,6 @@
+CORE
+distinct3.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$

src/solvers/smt2/smt2_parser.cpp

@@ -950,7 +950,23 @@ void smt2_parsert::setup_expressions()
 
   expressions["distinct"] = [this] {
     // pair-wise different constraint, multi-ary
-    return multi_ary("distinct", operands());
+    auto op = operands();
+    if(op.size() == 2)
+      return binary_predicate(ID_notequal, op);
+    else
+    {
+      std::vector<exprt> pairwise_constraints;
+      for(std::size_t i = 0; i < op.size(); i++)
+      {
+        for(std::size_t j = i; j < op.size(); j++)
+        {
+          if(i != j)
+            pairwise_constraints.push_back(
+              binary_exprt(op[i], ID_notequal, op[j], bool_typet()));
+        }
+      }
+      return multi_ary(ID_and, pairwise_constraints);
+    }
   };
 
   expressions["ite"] = [this] {