forall causes a runtime error

[rohit507]

from dreal.symbolic import *
from dreal.api import CheckSatisfiability, Minimize

def test_dreal_interface_find_othrogonal():
    """
    Just an empty test to make pytest force a parse check.
    """
    t = Variable('theta',Variable.Real)
    a = Variable('a',Variable.Int)
    b = Variable('b',Variable.Int)
    c = Variable('c',Variable.Int)
    d = Variable('d',Variable.Int)
    fun = forall([t], logical_imply(logical_and(t < 3,t > -3),
                                      (((sin(t)
                                         * if_then_else(b == True, 1 , -1)
                                         * if_then_else(a == True,sin(t),cos(t)))
                                        + (cos(t)
                                           * if_then_else(d == True, 1 , -1)
                                           * if_then_else(c == True,sin(t),cos(t))))
            == 0)))
    result = CheckSatisfiability(fun, 0.01)
    print(result)

test_dreal_interface_find_othrogonal()

The above equation, which should be true for (a = False, b = True, c = True, d = False), instead causes an error RuntimeError: Not yet supported.

There's also a similar error when I initialize any of the integer variables with Variable.Bool but things seem to work fine if I initialize them as integers and decode them back into floats myself.

What unimplemented feature is causing this error? It might be something I can work around, but I'm having trouble finding it.

[soonho-tri]

I guess the issue is that I didn't consider the case where we have Boolean variables inside of the universal quantifiers which we have in your example (via if_then_else).

I'll take a closer look later today.

[soonho-tri]

BTW,

    if_then_else(b == True, 1 , -1)

b == True doesn't sound correct given the fact b : Int.

[rohit507]

It is not, but without it I get an error saying that Variables are not allowed in that position of if_then_else. In practice True == 1 and False == 0 but I've written it as above for readability.

Edit: There's also no good way to promote a constant or variable to a Function, so I have to use foo * 1.0 or bar == True or achieve the same effect. Is there a helper function I can use somewhere?

[soonho-tri]

There are two issues here:

1) If-then-else eliminator does not support forall formulas yet. https://github.com/dreal/dreal4/blob/5e7c80ab49ac976718da020acc959480640a31d7/dreal/util/if_then_else_eliminator.cc#L336-L357

2) There is an ambiguity in formula == formula (i.e. iff) and expr == expr (i.e. eq).

I'll address them later this week (probably after Wed). Thanks for the patience.

[rohit507]

So, I've got a more representative example of what I'm working with dreal to do. Or at least one possible version thereof. Here's a gist with a toy problem.

It produces an identical runtime error as the above, but likely for different reasons.

Long story short, I can take coordinate transforms and other relationships between mechanical systems and flatten them into statements within DReal's theory (at least, I think they are). I want to be able to find a set of parameters for a mechanical system that which can be actuated to meet some requirements over its entire operating range.

The gist has a simple example where I want to find the size and origin of an arm so that it is possible for it to reach all the points within a circle. The example is in 2D, though the tool I'm working on is for problems in 3D.

Note, any thoughts on how to reformulate things would be very appreciated.

TL;DR: Grad school is fun, arbitrary end-of-semester deadlines even more so,

[rohit507]

Oh, if the nested forall isn't in your roadmap, I'd appreciate some heads up so I can switch to a more symbolic approach to eliminate the internal quantifier. Thanks.

[scungao]

Hi, right now the solver only supports exists-forall queries (one quantifier alternation). More nesting would require other algorithms.

On Thu, Apr 26, 2018 at 4:17 PM rohit507 notifications@github.com wrote:

Oh, if the nested forall isn't in your roadmap, I'd appreciate some heads up so I can switch to a more symbolic approach to eliminate the internal quantifier. Thanks.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/dreal/dreal4/issues/86#issuecomment-384817186, or mute the thread https://github.com/notifications/unsubscribe-auth/AFGzEhwfNsLQa5v8goiAwhgssm8U-c68ks5tslV-gaJpZM4TgRBV .

[soonho-tri]

Hi @rohit507 , as Sean mentioned we only support one alternation of quantifiers (exists-forall). If you mean nested "universal" quantifiers, then it's easy to collapse them into a single quantifier with a block of variables.

I'll work on this issue as my time allows.

[soonho-tri]

FTR, ITE elimination introduces a fresh (existentially-quantified) variable. For example, ITE(f, e₁, e₂) > 0 will be translated into ∃v. (v > 0) ∧ (f => (v = e₁)) ∧ (¬f => (v = e₂)).

In case of ∃∀-problems, this is not desirable since we end up with ∃∀∃-formulas. I think a better approach is to defer the elimination process to the ContractorForall where we only handle ground formulas.

[soonho-tri]

There is a way to introduce a fresh universal-variable in the process of ITE-elimination:

   ∃x. ∀y. ITE(f, e₁, e₂) > 0
=> ∃x. ¬∃y. ¬(ITE(f, e₁, e₂) > 0)
=> ∃x. ¬∃y. ∃v. ¬(v > 0) ∧ (f → (v = e₁)) ∧ (¬f → (v = e₂))
=> ∃x. ∀y. ∀v. ¬(¬(v > 0) ∧ (f → (v = e₁)) ∧ (¬f → (v = e₂)))
=> ∃x. ∀y. ∀v. (v > 0) ∨ ¬((f → (v = e₁)) ∧ (¬f → (v = e₂)))
=> ∃x. ∀y. ∀v. ¬((f → (v = e₁)) ∧ (¬f → (v = e₂))) ∨ (v > 0)
=> ∃x. ∀y. ∀v. ((f → (v = e₁)) ∧ (¬f → (v = e₂))) → (v > 0)

Without →, this is ∃x. ∀y. ∀v. (v > 0) ∨ (f ∧ (v ≠ e₁)) ∨ (¬f ∧ (v ≠ e₂)).

[soonho-tri]

@rohit507 , can you check if ff19ce8b8ac1810887983ea93040f16b4d4c24ff works as you expected?

[rohit507]

Sadly nope

from dreal.symbolic import *

def test_dreal_interface_ortho():

    t = Variable('theta',Variable.Real)
    a = Variable('a',Variable.Bool)
    b = Variable('b',Variable.Bool)
    c = Variable('c',Variable.Bool)
    d = Variable('d',Variable.Bool)

    fun = logical_imply(logical_and(t < 6.0,t > -6.0),
                                      (((sin(t)
                                         * if_then_else(b == True, 1 , -1)
                                         * if_then_else(a == True,sin(t),cos(t)))
                                        + (cos(t)
                                           * if_then_else(d == True, 1 , -1)
                                           * if_then_else(c == True,sin(t),cos(t))))
            == 0))

    forall_fun = forall([t], fun) 

    forall_result = CheckSatisfiability(forall_fun, 0.01)
    print()
    print(forall_result)

    counterexample_fun = logical_not(fun)

    counterexample_result = CheckSatisfiability(counterexample_fun, 0.01)
    print()
    print(counterexample_result)

fails with

test/algebra/test_dreal.py::test_dreal_interface_ortho 
a : [1, 1]
b : [1, 1]
c : [1, 1]
d : [1, 1]

________________________________________ test_dreal_interface_ortho _________________________________________

    def test_dreal_interface_ortho():
        """
        Just an empty test to make pytest force a parse check.
        """
        t = Variable('theta',Variable.Real)
        a = Variable('a',Variable.Bool)
        b = Variable('b',Variable.Bool)
        c = Variable('c',Variable.Bool)
        d = Variable('d',Variable.Bool)

        fun = logical_imply(logical_and(t < 6.0,t > -6.0),
                                          (((sin(t)
                                             * if_then_else(b == True, 1 , -1)
                                             * if_then_else(a == True,sin(t),cos(t)))
                                            + (cos(t)
                                               * if_then_else(d == True, 1 , -1)
                                               * if_then_else(c == True,sin(t),cos(t))))
                == 0))

        forall_fun = forall([t], fun)

        forall_result = CheckSatisfiability(forall_fun, 0.01)
        print()
        print(forall_result)

        counterexample_fun = logical_not(fun)

>       counterexample_result = CheckSatisfiability(counterexample_fun, 0.01)
E       RuntimeError: dreal/util/box.cc:157 Should not be reachable.

The first solution, with the forall, reduces to ' ∀t. ((t > -6) ∧ (t < 6)) → ((sin(t)sin(t) + cos(t)sin(t)) == 0)' which is clearly false. The counterexample finding version just fails outright, and the following (when I drop the '== True' terms) also has a failure, which follows.

        fun = logical_imply(
            logical_and(t < 6.0,t > -6.0),
            (((sin(t)
               * if_then_else(b, 1 , -1)
>              * if_then_else(a,sin(t),cos(t)))
              + (cos(t)
                 * if_then_else(d, 1 , -1)
                 * if_then_else(c,sin(t),cos(t))))
             == 0))
E       TypeError: if_then_else(): incompatible function arguments. The following argument types are supported:
E           1. (arg0: dreal::drake::symbolic::Formula, arg1: dreal.symbolic._dreal_symbolic_py.Expression, arg2: dreal.symbolic._dreal_symbolic_py.Expression) -> dreal.symbolic._dreal_symbolic_py.Expression
E       
E       Invoked with: Variable('b'), 1, -1

[soonho-tri]

Got it. I'll check.