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

diff --git a/src/parser/smtlib2.y b/src/parser/smtlib2.y
index 266b08301a45e62afd01645850e6de09b1a82612..af67a134bece12fa87f0189e1acdeb8ddd66efa5 100644 (file)
--- 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));