Basic ideas

[scungao]

@zenna Here's some pseudo-code I talked about. Here I'm just dealing with

\exists x \forall y. c(x,y)

where c is a simple constraint.

The idea is to use the \forall part as a normal contractor on the value of x. The contractor takes in the constraint c, the current box B_x on x, the full domain B_y of y (which won't be contracted), and returns an updated box on x.

box forall_contractor(c, box B_x, box B_y) {
    B_result = B_x;
    while ( ||B_result|| > delta ) {
        a = random y in B_y; //pick arbitrary y
        B_temp = contractor(c(a), B_result);
        if  ( B_temp == B_result ) 
            return B_result;
            //note that c(a) is now a constraint in x, doesn't have y   
        y = dreal_solve( not(c) \and x\in B_temp ); //making a recursive call to the solver itself
        if (y is an empty vector)  //unsat from dreal_solve
            return B_temp;
        else 
            B_result = B_temp;
    }
    return B_result;
}