Open danbryce opened 9 years ago
Looking at Enode.C, the print_infix method specifically looks for negated equality constraints and prints them as "0 = 0".
Yes, this is the case. Here is the related code: https://github.com/dreal/dreal/blob/master/src/opensmt/egraph/Enode.C#L356-L359
It's because under delta-perturbation, an expression of the form "X != Y" always evaluates to true. We don't really have "true" in realpaver, so it outputs "0 = 0" instead.
I believe this is meant to remove literals like the integral literals.
No. Removing integral literals and forall_t literals is done in different part of the code: https://github.com/dreal/dreal/blob/master/src/dsolvers/icp_solver.cpp#L299
This is causing me to get some wrong solutions. Am I missing something?
Well.. I don't really see a problem yet. Could you elaborate your problem more specifically?
This actually follows from the theory of delta-decision. The idea is any measure zero set would be ignored by the solver. The negation of an equality is consequently always delta sat -- it's only false at exactly 0, which means it's true almost everywhere. This is equivalent to treating strict and nonstrict inequalities as the same.
On Mar 12, 2015, at 09:36, Daniel Bryce notifications@github.com wrote:
In constructing the rp_constraints, the icp solver prints the literals to strings and compares them to "0 = 0". I believe this is meant to remove literals like the integral literals. Looking at Enode.C, the print_infix method specifically looks for negated equality constraints and prints them as "0 = 0". This is causing me to get some wrong solutions. Am I missing something?
— Reply to this email directly or view it on GitHub.
I don't have a small smt2 example just yet that illustrates the issue, but its something like this:
(= x_0_0 0) (flow (d/dt[x] = 0)) (not (= x_0_t 0))
This should be unsat b/c we will infer that x_0_t is zero and it cannot be zero.
This is the corner case which Sean mentioned. You have two point values x = 0
and y = 0
and evaluate !(= x y)
which should be false but we return true.
In dReal3, I've added an eval contractor
which literally evaluates a constraint with a given box and rejects it if the evaluated result violates the constraint. https://github.com/dreal/dreal3/blob/master/src/util/constraint.cpp#L137-L168 Using this, for example, we can reject abs(x) < 0
with an assignment x = 0
. So far, it supports >
, <
, >=
, <=
, ==
but not !=
simply because IBEX doesn't even have !=
in its data structure. But it's not so difficult to add support for !=
there using some hack.
In dReal2, if you really need this, you can implement one using realpaver and add the checking routine at the end of check as a final sweeper.
FYI, the following is UNSAT in dReal3 now:
(set-logic QF_NRA_ODE)
(declare-fun x_0 () Real)
(declare-fun x_t () Real)
(declare-fun time_0 () Real)
(define-ode flow_0 ((= d/dt[x] 0)))
(assert (>= time_0 0))
(assert (<= time_0 0.01))
(assert (= x_0 0))
(assert (not (= x_t 0)))
(assert (= [x_t]
(integral 0. time_0 [x_0] flow_0)))
(check-sat)
(exit)
Great. I’m going to wait for dreal3 instead of fixing dreal2. I was able to use an inequality for the same effect because the variable in question is an integer. I.e., x >= 1 has the same effect as x =/= 0.
On Mar 13, 2015, at 3:26 AM, Soonho Kong notifications@github.com wrote:
FYI, the following is UNSAT in dReal3 now:
(set-logic QF_NRA_ODE) (declare-fun x_0 () Real) (declare-fun x_t () Real) (declare-fun time_0 () Real) (define-ode flow_0 ((= d/dt[x] 0 ))) (assert (>= time_0 0 )) (assert (<= time_0 0.01 )) (assert (= x_0 0 )) (assert (not (= x_t 0 ))) (assert (= [x_t](integral 0 . time_0 [x_0] flow_0))) (check-sat) (exit)
— Reply to this email directly or view it on GitHub.
OK. I'll let you know when ODE part of dReal3 is as good as the one in dReal2.
In constructing the rp_constraints, the icp solver prints the literals to strings and compares them to "0 = 0". Looking at Enode.C, the print_infix method specifically looks for negated equality constraints and prints them as "0 = 0". This is causing me to get some wrong solutions. Am I missing something?