From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Tue, 9 Mar 2010 23:43:35 +0000 (+0000)
Subject: Adding support for "distinct" builtin in SMT parser
X-Git-Tag: cvc5-1.0.0~9190
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8d85fb035b92f0fa0d852257dc00c9a85b1a350e;p=cvc5.git

Adding support for "distinct" builtin in SMT parser
---

diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index 301859a37..7759cf965 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -126,6 +126,27 @@ annotatedFormula returns [CVC4::Expr formula]
     { checkArity(kind, args.size());
       formula = mkExpr(kind,args); }
 
+  | /* a "distinct" expr */
+    LPAREN DISTINCT annotatedFormulas[args] RPAREN
+    { std::vector<Expr> diseqs;
+      for(unsigned i = 0; i < args.size(); ++i) {
+        for(unsigned j = i+1; j < args.size(); ++j) {
+          diseqs.push_back(mkExpr(CVC4::kind::NOT, 
+                                  mkExpr(CVC4::kind::EQUAL,args[i],args[j])));
+        }
+      }
+      formula = mkExpr(CVC4::kind::AND, diseqs); }
+
+  | /* An ite expression */
+    LPAREN (ITE | IF_THEN_ELSE) 
+    { Expr test, trueExpr, falseExpr; }
+    test = annotatedFormula 
+    trueExpr = annotatedFormula
+    falseExpr = annotatedFormula
+    RPAREN
+    { formula = mkExpr(CVC4::kind::ITE, test, trueExpr, falseExpr); }
+
+
   | /* A non-built-in function application */
 
     // Semantic predicate not necessary if parenthesized subexpressions
@@ -139,15 +160,6 @@ annotatedFormula returns [CVC4::Expr formula]
     // TODO: check arity
     { formula = mkExpr(CVC4::kind::APPLY,args); }
 
-  | /* An ite expression */
-    LPAREN (ITE | IF_THEN_ELSE) 
-    { Expr test, trueExpr, falseExpr; }
-    test = annotatedFormula 
-    trueExpr = annotatedFormula
-    falseExpr = annotatedFormula
-    RPAREN
-    { formula = mkExpr(CVC4::kind::ITE, test, trueExpr, falseExpr); }
-
   | /* a variable */
     { std::string name; }
     name = identifier[CHECK_DECLARED]
diff --git a/test/regress/regress0/distinct.smt b/test/regress/regress0/distinct.smt
new file mode 100644
index 000000000..3c3578edc
--- /dev/null
+++ b/test/regress/regress0/distinct.smt
@@ -0,0 +1,5 @@
+(benchmark distinct_test
+  :logic QF_UF
+  :status unsat
+  :extrafuns ((x U) (y U) (z U))
+  :formula (not (iff (distinct x y z) (and (not (= x y)) (not (= x z)) (not (= y z))))))
\ No newline at end of file