Repository: dreal/dreal4 (language: python)

Issue:
The argument order to define-fun is not respected
Hello,

It seems like dReal is not respecting the argument order passed to functions. Below is an example. We are expecting the solution for R would be the same for line 9 and 10. But it seems like dReal inverses the arguments passed to `get_R`.  You can comment and uncomment line 9 and 10 to see the result.

`(set-logic QF_NRA)`
`(declare-fun a () Real)`
`(declare-fun b () Real)`
`(define-fun get_R ((x Real) (y Real)) Real`
`                   (* x (cos y)))`
`(assert (= a 12))`
`(assert (= b -0.7853981633974483))`
`(declare-fun R () Real)`
`;(assert (= R (* a (cos b))))`
`(assert (= R (get_R a b)))`
`(check-sat)`
`(get-model)`

 The version of dReal used is: dReal v4.20.09.1 (Release Build) for Mac and also the latest dReal docker image for Windows.


Discussion / hints:

Fix patch:
diff --git a/dreal/smt2/parser.yy b/dreal/smt2/parser.yy
index 297e4e87..b3f8d5ab 100644
--- a/dreal/smt2/parser.yy
+++ b/dreal/smt2/parser.yy
@@ -522,10 +522,10 @@ name_sort: '(' SYMBOL sort ')' {
         ;
 
 name_sort_list: /* empty list */ { $$ = std::vector<Variable>{}; }
-        |       name_sort name_sort_list {
-            const Variable& v = $1;
-	    $2.push_back(v);
-	    $$ = $2;
+        |       name_sort_list name_sort {
+            const Variable& v = $2;
+	    $1.push_back(v);
+	    $$ = $1;
         }
         ;
 


Test patch:
diff --git a/dreal/test/smt2/define_fun_02.smt2.expected b/dreal/test/smt2/define_fun_02.smt2.expected
index d3e05819..9416a9b9 100644
--- a/dreal/test/smt2/define_fun_02.smt2.expected
+++ b/dreal/test/smt2/define_fun_02.smt2.expected
@@ -1,5 +1,5 @@
 delta-sat with delta = 0.001
-z : [-1, -1]
+z : [1, 1]
 (model
-  (define-fun z () Real -1)
+  (define-fun z () Real 1)
 )
diff --git a/dreal/test/smt2/github_245.smt2 b/dreal/test/smt2/github_245.smt2
new file mode 100644
index 00000000..ebae292b
--- /dev/null
+++ b/dreal/test/smt2/github_245.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_NRA)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(define-fun get_R ((x Real) (y Real)) Real
+(* x (cos y)))
+(assert (= a 12))
+(assert (= b -0.7853981633974483))
+(declare-fun R () Real)
+;(assert (= R (* a (cos b))))
+(assert (= R (get_R a b)))
+(check-sat)
+(get-model)
+
diff --git a/dreal/test/smt2/github_245.smt2.expected b/dreal/test/smt2/github_245.smt2.expected
new file mode 100644
index 00000000..f6203e9e
--- /dev/null
+++ b/dreal/test/smt2/github_245.smt2.expected
@@ -0,0 +1,6 @@
+delta-sat with delta = 0.001
+(model
+  (define-fun a () Real 12)
+  (define-fun b () Real [-0.78539816339744839, -0.78539816339744828])
+  (define-fun R () Real [8.4852813742385571, 8.4852813742385855])
+)
diff --git a/dreal/test/smt2/option_smtlib2_compliant_01.smt2.expected b/dreal/test/smt2/option_smtlib2_compliant_01.smt2.expected
index ac2fad50..830ed24f 100644
--- a/dreal/test/smt2/option_smtlib2_compliant_01.smt2.expected
+++ b/dreal/test/smt2/option_smtlib2_compliant_01.smt2.expected
@@ -1,5 +1,5 @@
 delta-sat
 0.001
 (
-	(z (- 1))
+	(z 1)
 )