Skip to content

Commit

Permalink
Changing interface of Solver::next. Updating java plugin
Browse files Browse the repository at this point in the history
  • Loading branch information
Gilles Chabert committed Mar 1, 2019
1 parent a7e818d commit 06b415c
Show file tree
Hide file tree
Showing 4 changed files with 87 additions and 74 deletions.
12 changes: 7 additions & 5 deletions plugins/java/src/ibex_Java.cpp.in
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,6 @@
#include "ibex_VarSet.h"
#include "ibex_SmearFunction.h"
#include "ibex_Solver.h"
#include "ibex_QualifiedBox.h"
#include "ibex_CellStack.h"

#include <stdio.h>
Expand Down Expand Up @@ -520,12 +519,15 @@ JNIEXPORT jint JNICALL Java_@JAVA_SIGNATURE@_Ibex_next_1solution(JNIEnv* env, jo
return BAD_DOMAIN;
}

const QualifiedBox* sol;
const IntervalVector* sol = NULL;

CovSolverData::BoxStatus status;

inst.solver->next(status,&sol);

sol=inst.solver->next();
if (sol!=NULL) {
inst.write_box(env,sol->existence(),d);
result = sol->status==QualifiedBox::UNKNOWN? UNKNOWN : SOLUTION;
inst.write_box(env,*sol,d);
result = status==CovSolverData::UNKNOWN? UNKNOWN : SOLUTION;
} else {
result = SEARCH_OVER;
}
Expand Down
52 changes: 28 additions & 24 deletions plugins/solver/src/ibex_Solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -164,17 +164,18 @@ void Solver::start(const char* input_paving) {
start(data);
}

Solver::Status Solver::next() {
bool Solver::next(CovSolverData::BoxStatus& status, const IntervalVector** sol) {

while (!buffer.empty()) {

if (time_limit >0) {
try {
timer.check(time_limit);
}
catch(TimeOutException&) {
catch(TimeOutException& e) {
flush();
return TIME_OUT;
if (sol) *sol=NULL;
throw e;
}
}

Expand All @@ -199,10 +200,11 @@ Solver::Status Solver::next() {
// each intermediate step only if the system is under constrained
if (m==0 || (m<n && !is_too_large(c->box))) {
// note: cannot return PENDING status
CovSolverData::BoxStatus status=check_sol(c->box);
status=check_sol(c->box);
if (status!=CovSolverData::UNKNOWN) { // <=> solution or boundary
delete buffer.pop();
return SUCCESS;
if (sol) *sol=&(*manif)[manif->size()-1];
return true;
} // otherwise: continue search...
} // else: otherwise: continue search...

Expand All @@ -218,23 +220,21 @@ Solver::Status Solver::next() {
buffer.push(new_cells.second);
nb_cells+=2;
if (cell_limit >=0 && nb_cells>=cell_limit) {
//throw CellLimitException();
flush();
return CELL_OVERFLOW;
if (sol) *sol=NULL;
throw CellLimitException();
}
}

catch (NoBisectableVariableException&) {
CovSolverData::BoxStatus status=check_sol(c->box);
status=check_sol(c->box);
if (status==CovSolverData::UNKNOWN) {
if (trace >=1) cout << " [unknown] " << c->box << endl;
manif->add_unknown(c->box);
delete buffer.pop();
return NOT_ALL_VALIDATED;
} else {
delete buffer.pop();
return SUCCESS;
}
delete buffer.pop();
if (sol) *sol=&(*manif)[manif->size()-1];
return true;
}
}
catch (EmptyBoxException&) {
Expand All @@ -247,7 +247,8 @@ Solver::Status Solver::next() {
}
}

return INFEASIBLE;
if (sol) *sol=NULL;
return false;
}

Solver::Status Solver::solve(const IntervalVector& init_box) {
Expand Down Expand Up @@ -275,17 +276,20 @@ Solver::Status Solver::solve() {
else
final_status = SUCCESS;

Solver::Status status = SUCCESS;

while (status==SUCCESS || status==NOT_ALL_VALIDATED) {
CovSolverData::BoxStatus status;

status=next();
try {
while (next(status)) {
if (final_status==INFEASIBLE) // first solution found
final_status=SUCCESS; // by default... may be changed right after

if (status==CELL_OVERFLOW) final_status=CELL_OVERFLOW;
if (status==TIME_OUT) final_status=TIME_OUT;
if (status==NOT_ALL_VALIDATED) final_status=NOT_ALL_VALIDATED;
if (status==SUCCESS)
if (final_status==INFEASIBLE) final_status=SUCCESS;
if (status==CovSolverData::UNKNOWN)
final_status=NOT_ALL_VALIDATED;
}
} catch(CellLimitException&) {
final_status=CELL_OVERFLOW;
} catch(TimeOutException&) {
final_status=TIME_OUT;
}

manif->set_solver_status(final_status);
Expand All @@ -297,7 +301,7 @@ Solver::Status Solver::solve() {

manif->set_nb_cells(manif->nb_cells() + nb_cells);

return status;
return final_status;
}

bool Solver::check_ineq(const IntervalVector& box) {
Expand Down
38 changes: 19 additions & 19 deletions plugins/solver/src/ibex_Solver.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -98,11 +98,14 @@ class Solver {
*
* INFEASIBLE: (complete search) infeasible problem.
*
* NOT_ALL_VALIDATED: (incomplete search) minimal width (eps-min)
* reached
* NOT_ALL_VALIDATED: (incomplete search) a non-validated box
* reaching the minimal width (eps-min)
* has been found.
*
* TIME_OUT: (incomplete search) time out
*
* CELL_OVERFLOW: (incomplete search) cell overflow
* CELL_OVERFLOW: (incomplete search) cell overflow : the number of
* cell has exceeded the limit.
*
* The vector of "solutions" (output boxes) found by the solver
* are retrieved with #get_solutions().
Expand Down Expand Up @@ -152,27 +155,24 @@ class Solver {
void start(const char* input_paving);

/**
* \brief Find the next solution (interactive mode).
*
* \param sol - (output argument) pointer to the new solution (if found). This
* is just the address of the last element in the "solutions" vector.
* Set to NULL if search is over, time is out or the number of cells
* exceeds the limit.
* \brief Find the next covering box (interactive mode).
*
* \return Possible values. For commodity, the same return type is used for next(..)
* and solve(..) but the interpretation slightly differs:
* The next box is either a new solution, a boundary or an unknown box.
*
* SUCCESS: a new validated solution has been found.
* \return true if a new covering box is found.
*
* INFEASIBLE: no more solution (search over).
*
* NOT_ALL_VALIDATED: a non-validated box reaching the minimal width (eps-min)
* has been found.
* TIME_OUT: time is out
* \param status - status of the new box found. Undefined if an exception is
* thrown, or the search is over.
* \param sol - (output argument) pointer to the new box. This parameter is
* ignored if set to NULL (default value). Otherwise, in return, *sol
* is the address of the last element added in the CovSolverData
* structure.
* *sol is set to NULL if search is over, time is out or the number
* of cells exceeds the limit.
*
* CELL_OVERFLOW: the number of cell has exceeded the limit.
* \throw CellLimitException or TimeOutException
*/
Status next();
bool next(CovSolverData::BoxStatus& box_status, const IntervalVector** sol=NULL);

/**
* \brief Displays on standard output a report of the last call to solve(...).
Expand Down
59 changes: 33 additions & 26 deletions tests/TestSolver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,20 +45,22 @@ void TestSolver::circle1() {
Solver solver(sys,hc4,rr,stack,prec,prec);
solver.start(IntervalVector(2,Interval(-10,10)));

Solver::Status res;
CovSolverData::BoxStatus status;

res=solver.next();
CPPUNIT_ASSERT(res==Solver::SUCCESS);
bool res=solver.next(status);
CPPUNIT_ASSERT(res);
CPPUNIT_ASSERT(status==CovSolverData::SOLUTION);
CPPUNIT_ASSERT(solver.get_data().nb_solution()==1);
CPPUNIT_ASSERT(solver.get_data().solution(0).is_superset(sol1));

res=solver.next();
CPPUNIT_ASSERT(res==Solver::SUCCESS);
res=solver.next(status);
CPPUNIT_ASSERT(res);
CPPUNIT_ASSERT(status==CovSolverData::SOLUTION);
CPPUNIT_ASSERT(solver.get_data().nb_solution()==2);
CPPUNIT_ASSERT(solver.get_data().solution(1).is_superset(sol2));

res=solver.next();
CPPUNIT_ASSERT(res==Solver::INFEASIBLE);
res=solver.next(status);
CPPUNIT_ASSERT(!res);
}

void TestSolver::circle2() {
Expand All @@ -81,15 +83,16 @@ void TestSolver::circle2() {

solver.start(IntervalVector(2,Interval(-10,10)));

Solver::Status res;
CovSolverData::BoxStatus status;

res=solver.next();
CPPUNIT_ASSERT(res==Solver::NOT_ALL_VALIDATED);
bool res=solver.next(status);
CPPUNIT_ASSERT(res);
CPPUNIT_ASSERT(status==CovSolverData::UNKNOWN);
CPPUNIT_ASSERT(solver.get_data().nb_unknown()==1);
CPPUNIT_ASSERT(solver.get_data().unknown(0).is_superset(sol1));

res=solver.next();
CPPUNIT_ASSERT(res==Solver::INFEASIBLE);
res=solver.next(status);
CPPUNIT_ASSERT(!res);
}

void TestSolver::circle3() {
Expand Down Expand Up @@ -120,20 +123,23 @@ void TestSolver::circle3() {

solver.start(IntervalVector(2,Interval(-10,10)));

Solver::Status res;

res=solver.next();
CPPUNIT_ASSERT(res==Solver::NOT_ALL_VALIDATED);
CovSolverData::BoxStatus status;

bool res=solver.next(status);
CPPUNIT_ASSERT(res);
CPPUNIT_ASSERT(status==CovSolverData::UNKNOWN);
CPPUNIT_ASSERT(solver.get_data().nb_unknown()==1);
CPPUNIT_ASSERT(solver.get_data().unknown(0).is_superset(sol1));

res=solver.next();
CPPUNIT_ASSERT(res==Solver::SUCCESS);
res=solver.next(status);
CPPUNIT_ASSERT(res);
CPPUNIT_ASSERT(status==CovSolverData::SOLUTION);
CPPUNIT_ASSERT(solver.get_data().nb_solution()==1);
CPPUNIT_ASSERT(solver.get_data().solution(0).is_superset(sol2));

res=solver.next();
CPPUNIT_ASSERT(res==Solver::INFEASIBLE);
res=solver.next(status);
CPPUNIT_ASSERT(!res);
}

void TestSolver::circle4() {
Expand Down Expand Up @@ -172,20 +178,21 @@ void TestSolver::circle4() {
box[2]=Interval(1,1);
solver.start(box);

Solver::Status res;
CovSolverData::BoxStatus status;

res=solver.next();
CPPUNIT_ASSERT(res==Solver::SUCCESS);
bool res=solver.next(status);
CPPUNIT_ASSERT(res);
CPPUNIT_ASSERT(status==CovSolverData::SOLUTION);
CPPUNIT_ASSERT(solver.get_data().nb_solution()==1);
CPPUNIT_ASSERT(solver.get_data().solution(0).is_superset(sol1));

res=solver.next();
CPPUNIT_ASSERT(res==Solver::SUCCESS);
res=solver.next(status);
CPPUNIT_ASSERT(status==CovSolverData::SOLUTION);
CPPUNIT_ASSERT(solver.get_data().nb_solution()==2);
CPPUNIT_ASSERT(solver.get_data().solution(1).is_superset(sol2));

res=solver.next();
CPPUNIT_ASSERT(res==Solver::INFEASIBLE);
res=solver.next(status);
CPPUNIT_ASSERT(!res);
}


Expand Down

0 comments on commit 06b415c

Please sign in to comment.