Skip to content

Commit

Permalink
java: add threshold in 'contract' (fix issue #435)
Browse files Browse the repository at this point in the history
  • Loading branch information
CHABERT Gilles committed Mar 2, 2020
1 parent e478f10 commit a15497d
Show file tree
Hide file tree
Showing 4 changed files with 51 additions and 23 deletions.
13 changes: 10 additions & 3 deletions plugins/java/src/Ibex.java.in
View file
Original file line number Diff line number Diff line change
Expand Up @@ -112,6 +112,13 @@ public class Ibex {
* lower (resp. upper) bound of the domain of x_i.
* @param reif - Domain of the reification variable b with the following accepted values:
* FALSE, TRUE, FALSE_OR_TRUE.
*
* @param rel_eps- Threshold under which a contraction is considered as unsufficient and
* therefore ignored.
* If we denote by w_i the width of the initial domain of the ith variable
* and by w_i' the width of the contracted domain, all contractions
* will be discarded (and the return status will be NOTHING) if for all i,
* (w_i - w_i') < rel_eps * w_i.
*
* @return The status of contraction or fail/entailment test. Note that the name of the
* constant in return refers to the constraint c, not R. Hence "FAIL" means that
Expand All @@ -136,13 +143,13 @@ public class Ibex {
* removed part of the domain is inside c. If reif==TRUE, the removed part
* is outside.
*
* NOTHING - No bound has been reduced and nothing could be proven.
* NOTHING - No bound has been significantly reduced and nothing could be proven.
*
* BAD_DOMAIN - The domain has not the expected number of dimensions.
*
* NOT_BUILT - Object not built (build() must be called before)
*/
public native int contract(int i, double bounds[], int reif);
public native int contract(int i, double bounds[], int reif, double rel_eps);

/**
* Inflate a point to a box with respect to a constraint or its negation.
Expand Down Expand Up @@ -197,7 +204,7 @@ public class Ibex {
/**
* Same as contract(int, double bounds[], int reif) with reif=TRUE.
*/
public native int contract(int i, double bounds[]);
public native int contract(int i, double bounds[], double rel_eps);

/**
* Let IBEX terminates the solving process for the CSP, once all the integer
Expand Down
10 changes: 5 additions & 5 deletions plugins/java/src/ibex_Java.cpp.in
View file
Original file line number Diff line number Diff line change
Expand Up @@ -290,7 +290,7 @@ JNIEXPORT jboolean JNICALL Java_@JAVA_SIGNATURE@_Ibex_build(JNIEnv* env, jobject
}
}

JNIEXPORT jint JNICALL Java_@JAVA_SIGNATURE@_Ibex_contract__I_3DI(JNIEnv* env, jobject obj, jint n, jdoubleArray _d, jint reif) {
JNIEXPORT jint JNICALL Java_@JAVA_SIGNATURE@_Ibex_contract__I_3DID(JNIEnv* env, jobject obj, jint n, jdoubleArray _d, jint reif, jdouble rel_eps) {


Instance& inst = *get_instance(env,obj);
Expand Down Expand Up @@ -323,7 +323,7 @@ JNIEXPORT jint JNICALL Java_@JAVA_SIGNATURE@_Ibex_contract__I_3DI(JNIEnv* env, j
}

else {
if (reif==TRUE_ && savebox.rel_distance(box) >= EPS_CONTRACT) {
if (reif==TRUE_ && savebox.rel_distance(box) >= rel_eps) {

//cout << " [ibex] --> CONTRACT to " << box << "\n";
savebox = box;
Expand Down Expand Up @@ -354,7 +354,7 @@ JNIEXPORT jint JNICALL Java_@JAVA_SIGNATURE@_Ibex_contract__I_3DI(JNIEnv* env, j
result=ENTAILED;
} else {

if (reif==FALSE_ && savebox.rel_distance(box) >= EPS_CONTRACT) {
if (reif==FALSE_ && savebox.rel_distance(box) >= rel_eps) {
savebox = box;
result=CONTRACT; // temporary assignment (final result may be FAIL)
}
Expand All @@ -374,8 +374,8 @@ JNIEXPORT jint JNICALL Java_@JAVA_SIGNATURE@_Ibex_contract__I_3DI(JNIEnv* env, j
return result;
}

JNIEXPORT jint JNICALL Java_@JAVA_SIGNATURE@_Ibex_contract__I_3D(JNIEnv* env, jobject obj, jint n, jdoubleArray _d) {
return Java_@JAVA_SIGNATURE@_Ibex_contract__I_3DI(env,obj,n,_d,1);
JNIEXPORT jint JNICALL Java_@JAVA_SIGNATURE@_Ibex_contract__I_3DD(JNIEnv* env, jobject obj, jint n, jdoubleArray _d, jdouble rel_eps) {
return Java_@JAVA_SIGNATURE@_Ibex_contract__I_3DID(env,obj,n,_d,1,rel_eps);
}

JNIEXPORT jint JNICALL Java_@JAVA_SIGNATURE@_Ibex_inflate(JNIEnv* env, jobject obj, jint n, jdoubleArray _din, jdoubleArray _d, jboolean in) {
Expand Down
49 changes: 35 additions & 14 deletions plugins/java/tests/IbexTest.java.in
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ import java.util.*;
public class IbexTest {

public final static double DEFAULT_DELTA=1e-10;
public final static double DEFAULT_REL_EPS=1e-3;

public static String strDomain(double[] a) {
String s="";
Expand Down Expand Up @@ -37,13 +38,13 @@ public class IbexTest {

double domains[] = {1.0, 10.0, 1.0, 10.0};

Assert.assertEquals(Ibex.NOT_BUILT, ibex.contract(0, domains));
Assert.assertEquals(Ibex.NOT_BUILT, ibex.contract(0, domains, DEFAULT_REL_EPS));

Assert.assertTrue(ibex.build());

Assert.assertFalse(ibex.add_ctr("{0}=0")); // already built

int result = ibex.contract(0, domains);
int result = ibex.contract(0, domains, DEFAULT_REL_EPS);

Assert.assertEquals(Ibex.CONTRACT, result);

Expand All @@ -64,28 +65,28 @@ public class IbexTest {
double vv = Math.sqrt(2.) / 2.;

// CASE 1: the boolean is set to TRUE
Assert.assertEquals(Ibex.FAIL, ibex.contract(0, new double[]{2., 3., 2., 3.}, Ibex.TRUE));
Assert.assertEquals(Ibex.ENTAILED, ibex.contract(0, new double[]{-.5, .5, -.5, .5}, Ibex.TRUE));
Assert.assertEquals(Ibex.FAIL, ibex.contract(0, new double[]{2., 3., 2., 3.}, Ibex.TRUE, DEFAULT_REL_EPS));
Assert.assertEquals(Ibex.ENTAILED, ibex.contract(0, new double[]{-.5, .5, -.5, .5}, Ibex.TRUE, DEFAULT_REL_EPS));
domains = new double[]{-2., 1., -2., 1.};
Assert.assertEquals(Ibex.CONTRACT, ibex.contract(0, domains, Ibex.TRUE));
Assert.assertEquals(Ibex.CONTRACT, ibex.contract(0, domains, Ibex.TRUE, DEFAULT_REL_EPS));
cmpDomains(domains, new double[]{-1., 1., -1., 1.});
Assert.assertEquals(Ibex.NOTHING, ibex.contract(0, domains, Ibex.TRUE));
Assert.assertEquals(Ibex.NOTHING, ibex.contract(0, domains, Ibex.TRUE, DEFAULT_REL_EPS));


// CASE 2: the boolean is set to FALSE
Assert.assertEquals(Ibex.FAIL, ibex.contract(0, new double[]{2., 3., 2., 3.}, Ibex.FALSE));
Assert.assertEquals(Ibex.ENTAILED, ibex.contract(0, new double[]{-.5, .5, -.5, .5}, Ibex.FALSE));
Assert.assertEquals(Ibex.NOTHING, ibex.contract(0, new double[]{-2., 1., -2., -1.}, Ibex.FALSE));
Assert.assertEquals(Ibex.FAIL, ibex.contract(0, new double[]{2., 3., 2., 3.}, Ibex.FALSE, DEFAULT_REL_EPS));
Assert.assertEquals(Ibex.ENTAILED, ibex.contract(0, new double[]{-.5, .5, -.5, .5}, Ibex.FALSE, DEFAULT_REL_EPS));
Assert.assertEquals(Ibex.NOTHING, ibex.contract(0, new double[]{-2., 1., -2., -1.}, Ibex.FALSE, DEFAULT_REL_EPS));
domains = new double[]{0., 2., -vv, vv};
Assert.assertEquals(Ibex.CONTRACT, ibex.contract(0, domains, Ibex.FALSE));
Assert.assertEquals(Ibex.CONTRACT, ibex.contract(0, domains, Ibex.FALSE, DEFAULT_REL_EPS));
cmpDomains(domains, new double[]{vv, 2., -vv, vv});

// CASE 3: the boolean is set to UNKNOWN
Assert.assertEquals(Ibex.FAIL, ibex.contract(0, new double[]{2., 3., 2., 3.}, Ibex.FALSE_OR_TRUE));
Assert.assertEquals(Ibex.ENTAILED, ibex.contract(0, new double[]{-.5, .5, -.5, .5}, Ibex.FALSE_OR_TRUE));
Assert.assertEquals(Ibex.NOTHING, ibex.contract(0, new double[]{-2., 1., -2., -1.}, Ibex.FALSE_OR_TRUE));
Assert.assertEquals(Ibex.FAIL, ibex.contract(0, new double[]{2., 3., 2., 3.}, Ibex.FALSE_OR_TRUE, DEFAULT_REL_EPS));
Assert.assertEquals(Ibex.ENTAILED, ibex.contract(0, new double[]{-.5, .5, -.5, .5}, Ibex.FALSE_OR_TRUE, DEFAULT_REL_EPS));
Assert.assertEquals(Ibex.NOTHING, ibex.contract(0, new double[]{-2., 1., -2., -1.}, Ibex.FALSE_OR_TRUE, DEFAULT_REL_EPS));
domains = new double[]{0., 2., -vv, vv};
Assert.assertEquals(Ibex.NOTHING, ibex.contract(0, domains, Ibex.FALSE_OR_TRUE));
Assert.assertEquals(Ibex.NOTHING, ibex.contract(0, domains, Ibex.FALSE_OR_TRUE, DEFAULT_REL_EPS));
cmpDomains(domains, new double[]{0., 2., -vv, vv});

ibex.release();
Expand Down Expand Up @@ -239,6 +240,26 @@ public class IbexTest {
ibex.release();
}

@Test
public void test_rel_prec() {
// see issue #435
Ibex ibex = new Ibex(new double[]{1e-3,1e-3});
ibex.add_ctr("{0}={1}");

Assert.assertTrue(ibex.build());

double domains[]={0,1,0,0.899999};
Assert.assertEquals(Ibex.NOTHING, ibex.contract(0, domains, 0.5));
cmpDomains(new double[]{0,1,0,0.899999}, domains);
Assert.assertEquals(Ibex.NOTHING, ibex.contract(0, domains, 0.11));
cmpDomains(new double[]{0,1,0,0.899999}, domains);
Assert.assertEquals(Ibex.CONTRACT, ibex.contract(0, domains, 0.1));
cmpDomains(new double[]{0,0.899999,0,0.899999}, domains);

ibex.release();

}

public static void main(String args[]) {
org.junit.runner.JUnitCore.main("IbexTest");
}
Expand Down
2 changes: 1 addition & 1 deletion plugins/java/tests/Test.java.in
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ class Test {
System.out.println("Before contract:");
System.out.println("(["+domains[0]+","+domains[1]+"] ; ["+domains[2]+","+domains[3]+"])");

int result=ibex.contract(0,domains);
int result=ibex.contract(0,domains,1e-3);

if (result==Ibex.FAIL) {
System.out.println("Failed!");
Expand Down

0 comments on commit a15497d

Please sign in to comment.