(set-option :precision 0.01)
(declare-const c Real)
(declare-const d Real)
(declare-const e Real)
(declare-const f Real)
(assert (and (> d -50) (< d 50)))
(assert (and (> e -50) (< e 50)))
(assert (and (> c -50) (< c 50)))
(assert (and (> f -50) (< f 50)))
(assert (forall ( (p Real [0, 1]) (q Real [0, 1])) true))
(assert (forall ( (p Real [0, 1])) (and (<= 0 (+ f (* (/ 1 2) e) (* (/ 1 4) c) (* p e) (* c (pow p 2)) (* (/ 1 2) p d))) (<= (+ f (* (/ 1 2) e) (* (/ 1 4) c) (* p e) (* c (pow p 2)) (* (/ 1 2) p d)) 1))))
(assert (forall ( (p Real [-0.1, 1.1])) (= (+ f (* p e) (* c (pow p 2))) 1)))
(assert (= (+ d f (* 2 c) (* 2 e)) 0))
(assert (>= (+ e f (* (/ 1 2) c) (* (/ 1 4) d)) (/ 1 2)))
(assert (forall ( (p Real [0.6, 1]) (q Real [0.6, 1])) (< (+ f (* p e) (* q e) (* c (pow p 2)) (* c (pow q 2)) (* p q d)) (/ 1 2))))
(check-sat)
(get-model)
unsat
(error "model is not available")
(set-option :precision 0.01)
(declare-const c Int)
(declare-const d Int)
(declare-const e Int)
(declare-const f Int)
(assert (and (> d -50) (< d 50)))
(assert (and (> e -50) (< e 50)))
(assert (and (> c -50) (< c 50)))
(assert (and (> f -50) (< f 50)))
(assert (forall ( (p Real [0, 1]) (q Real [0, 1])) true))
(assert (forall ( (p Real [0, 1])) (and (<= 0 (+ f (* (/ 1 2) e) (* (/ 1 4) c) (* p e) (* c (pow p 2)) (* (/ 1 2) p d))) (<= (+ f (* (/ 1 2) e) (* (/ 1 4) c) (* p e) (* c (pow p 2)) (* (/ 1 2) p d)) 1))))
(assert (forall ( (p Real [-0.1, 1.1])) (= (+ f (* p e) (* c (pow p 2))) 1)))
(assert (= (+ d f (* 2 c) (* 2 e)) 0))
(assert (>= (+ e f (* (/ 1 2) c) (* (/ 1 4) d)) (/ 1 2)))
(assert (forall ( (p Real [0.6, 1]) (q Real [0.6, 1])) (< (+ f (* p e) (* q e) (* c (pow p 2)) (* c (pow q 2)) (* p q d)) (/ 1 2))))
(check-sat)
(get-model)
delta-sat with delta = 0.01
(model
(define-fun c () Int 1)
(define-fun d () Int 16)
(define-fun e () Int -14)
(define-fun f () Int 10)
)
The only difference is the variable types:
2,5c2,5
< (declare-const c Real)
< (declare-const d Real)
< (declare-const e Real)
< (declare-const f Real)
---
> (declare-const c Int)
> (declare-const d Int)
> (declare-const e Int)
> (declare-const f Int)
18,19c18,24
< unsat
< (error "model is not available")
---
> delta-sat with delta = 0.01
> (model
> (define-fun c () Int 1)
> (define-fun d () Int 16)
> (define-fun e () Int -14)
> (define-fun f () Int 10)
> )
Also note— the SAT result is pretty wrong / inaccurate.
The formula is asking dReal to find coefficients for a function of the form c*p**2 + c*q**2 + d*p*q + e*p + e*q + f.
dReal gives the result p**2 + 16*p*q - 14*p + q**2 - 14*q + 10, which plotted, looks like:
This is pretty wrong because I explicitly ask
(assert (forall ( (p Real [-0.1, 1.1])) (= (+ f (* p e) (* c (pow p 2))) 1)))
The simplification is correct, because when q=0, c*p**2 + c*q**2 + d*p*q + e*p + e*q + f = c*p**2 + e*p + f.
However, in the resulting model, when (p,q)=0, p**2 + 16*p*q - 14*p + q**2 - 14*q + 10=10 violating my assertion that it should be =1.
Queries generated by https://github.com/sympy/sympy/pull/23961
The only difference is the variable types:
Also note— the SAT result is pretty wrong / inaccurate. The formula is asking dReal to find coefficients for a function of the form
c*p**2 + c*q**2 + d*p*q + e*p + e*q + f. dReal gives the resultp**2 + 16*p*q - 14*p + q**2 - 14*q + 10, which plotted, looks like:This is pretty wrong because I explicitly ask
The simplification is correct, because when q=0,
c*p**2 + c*q**2 + d*p*q + e*p + e*q + f=c*p**2 + e*p + f. However, in the resulting model, when (p,q)=0,p**2 + 16*p*q - 14*p + q**2 - 14*q + 10=10violating my assertion that it should be=1.