Repository: dreal/dreal4 (language: python)

Issue:
Something is not right with user-defined functions
The model produced for the attached SMT-LIB file is not correct when using user-defined functions. 
Please see the comments in the file for a detailed explanation.


[report1.txt](https://github.com/dreal/dreal4/files/6580882/report1.txt)

dReal version: dReal v4.20.12.1 (Release Build) for Mac and the latest docker image for Windows


Discussion / hints:
Thanks for the report, @baoluomeng . I'll check the file and get back to you.
There is a bug in handling `ite`s inside of `declare-fun`:

```smt2
 (define-fun absolute ( (val Real) ) Real
     (ite
         (>= val 0.0)
         val
         (- 0.0 val)
     )
 )
```

I'll fix the bug and close this issue. In the meantime, a workaround is not to define `absolute` by yourself but to use `abs`. You can rewrite `fun1` to:

```smt2
 (define-fun fun1 ( (x Real) ) Bool
     (<= (abs (+ 10 (* -10 (- x a)))) Y)
 )
```

Fix patch:
diff --git a/dreal/smt2/term.cc b/dreal/smt2/term.cc
index e173a1b3..f287a82a 100644
--- a/dreal/smt2/term.cc
+++ b/dreal/smt2/term.cc
@@ -45,10 +45,28 @@ Formula& Term::mutable_formula() { return const_cast<Formula&>(formula()); }
 
 Term Term::Substitute(const Variable& v, const Term& t) {
   switch (type_) {
-    case Type::FORMULA:
-      return Term{f_.Substitute(v, t.f_)};
-    case Type::EXPRESSION:
-      return Term{e_.Substitute(v, t.e_)};
+    case Type::FORMULA: {
+      switch (v.get_type()) {
+        case Variable::Type::CONTINUOUS:
+        case Variable::Type::INTEGER:
+        case Variable::Type::BINARY:
+          return Term{f_.Substitute(v, t.e_)};
+        case Variable::Type::BOOLEAN:
+          return Term{f_.Substitute(v, t.f_)};
+      }
+      DREAL_UNREACHABLE();
+    }
+    case Type::EXPRESSION: {
+      switch (v.get_type()) {
+        case Variable::Type::CONTINUOUS:
+        case Variable::Type::INTEGER:
+        case Variable::Type::BINARY:
+          return Term{e_.Substitute(v, t.e_)};
+        case Variable::Type::BOOLEAN:
+          return Term{e_.Substitute({}, {{v, t.f_}})};
+      }
+      DREAL_UNREACHABLE();
+    }
   }
   DREAL_UNREACHABLE();
 }


Test patch:
diff --git a/dreal/test/smt2/BUILD.bazel b/dreal/test/smt2/BUILD.bazel
index a8d86ae5..5ffd0383 100644
--- a/dreal/test/smt2/BUILD.bazel
+++ b/dreal/test/smt2/BUILD.bazel
@@ -1170,6 +1170,11 @@ smt2_test(
     size = "small",
 )
 
+smt2_test(
+    name = "github_issue_247",
+    size = "small",
+)
+
 smt2_test(
     name = "github_issue_248",
     size = "small",
diff --git a/dreal/test/smt2/github_issue_247.smt2 b/dreal/test/smt2/github_issue_247.smt2
new file mode 100644
index 00000000..b8ea7eee
--- /dev/null
+++ b/dreal/test/smt2/github_issue_247.smt2
@@ -0,0 +1,79 @@
+(set-logic QF_NRA)
+
+
+;--------------- SAMPLE CONTEXT FOR DESCRIBING THE BUG
+
+(declare-fun a () Real)
+(declare-fun b () Real)
+(declare-fun c () Real)
+(declare-fun d () Real)
+(declare-fun e () Real)
+(declare-fun f () Real)
+(declare-fun Y () Real)
+
+
+(assert (= a 8.768685282571274))
+(assert (= b 29.761904761904763))
+(assert (= c 5))
+(assert (= d 15))
+(assert (= e 0))
+(assert (= f 10))
+(assert (= Y 10))
+
+
+(declare-fun Joker () Real)
+(assert (= Joker 12.8313))
+
+
+(define-fun absolute ( (val Real) ) Real
+    (ite
+        (>= val 0.0)
+        val
+        (- 0.0 val)
+    )
+)
+
+
+
+(define-fun fun1 ( (x Real) ) Bool
+    (<= (absolute (+ 10 (* -10 (- x a)))) Y)
+)
+
+
+;-------------  THE BUG/ISSUE
+
+(declare-fun test_print1 () Bool)  ; test variable to print values
+(assert
+    (= test_print1
+        (and (>= (+ a Joker) a) (<= (+ a Joker) b))
+    )
+)
+
+;--- test_print1 EVALUATES TO TRUE
+
+
+(declare-fun test_print2 () Bool)  ; test variable to print values
+(assert
+    (= test_print2
+        (fun1 (+ a Joker))
+    )
+)
+
+;--- test_print2 EVALUATES TO FALSE
+
+
+(declare-fun test_print3 () Bool)  ; test variable to print values
+(assert
+    (= test_print3
+        (and
+            (and (>= (+ a Joker) a) (<= (+ a Joker) b)) ; equivalent to test_print1
+            (fun1 (+ a Joker)) ; equivalent to test_print2
+        )
+    )
+)
+
+;--- test_print3, which is equivalent to the conjuction of test_print1 and test_print2 SHOULD EVALUATE TO FALSE, BUT IT EVALUATES TO TRUE !!!
+
+
+(check-sat)
+(get-model)
diff --git a/dreal/test/smt2/github_issue_247.smt2.expected b/dreal/test/smt2/github_issue_247.smt2.expected
new file mode 100644
index 00000000..a2699f9c
--- /dev/null
+++ b/dreal/test/smt2/github_issue_247.smt2.expected
@@ -0,0 +1,14 @@
+delta-sat with delta = 0.001
+(model
+  (define-fun a () Real [8.7686852825712727, 8.7686852825712744])
+  (define-fun b () Real [29.761904761904763, 29.761904761904766])
+  (define-fun c () Real 5)
+  (define-fun d () Real 15)
+  (define-fun e () Real 0)
+  (define-fun f () Real 10)
+  (define-fun Y () Real 10)
+  (define-fun Joker () Real [12.831299999999999, 12.831300000000001])
+  (define-fun test_print1 () Bool true)
+  (define-fun test_print2 () Bool false)
+  (define-fun test_print3 () Bool false)
+)