From e9112a4df034c942caa4f3482bd7bfc2f03da931 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 24 May 2010 05:50:57 +0000
Subject: [PATCH] bugfix. Allow distinct to be used for both formulae and
 terms.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@790 e59a4935-1847-0410-ae03-e826735625c1
---
 src/parser/smtlib2.y | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/src/parser/smtlib2.y b/src/parser/smtlib2.y
index 266b083..af67a13 100644
--- a/src/parser/smtlib2.y
+++ b/src/parser/smtlib2.y
@@ -390,6 +390,30 @@ TRUE_TOK
 
   delete $3;
 }
+| LPAREN_TOK DISTINCT_TOK an_formulas RPAREN_TOK
+{
+  using namespace BEEV;
+
+  ASTVec terms = *$3;
+  ASTVec forms;
+
+  for(ASTVec::const_iterator it=terms.begin(),itend=terms.end();
+      it!=itend; it++) {
+    for(ASTVec::const_iterator it2=it+1; it2!=itend; it2++) {
+      ASTNode n = (parserInterface->nf->CreateNode(NOT, parserInterface->nf->CreateNode(IFF, *it, *it2)));
+      forms.push_back(n); 
+    }
+  }
+
+  if(forms.size() == 0) 
+    FatalError("empty distinct");
+ 
+  $$ = (forms.size() == 1) ?
+    new ASTNode(forms[0]) :
+    new ASTNode(parserInterface->nf->CreateNode(AND, forms));
+
+  delete $3;
+}
 | LPAREN_TOK BVSLT_TOK an_term an_term RPAREN_TOK
 {
   ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVSLT, *$3, *$4));
-- 
2.47.3