From 06b415c0f28991e66fdabeeb2a3637e96ed21586 Mon Sep 17 00:00:00 2001 From: Gilles Chabert Date: Fri, 1 Mar 2019 22:55:46 +0100 Subject: [PATCH] Changing interface of Solver::next. Updating java plugin --- plugins/java/src/ibex_Java.cpp.in | 12 +++--- plugins/solver/src/ibex_Solver.cpp | 52 ++++++++++++++------------ plugins/solver/src/ibex_Solver.h | 38 +++++++++---------- tests/TestSolver.cpp | 59 +++++++++++++++++------------- 4 files changed, 87 insertions(+), 74 deletions(-) diff --git a/plugins/java/src/ibex_Java.cpp.in b/plugins/java/src/ibex_Java.cpp.in index a1ce6379d..91ec856cf 100644 --- a/plugins/java/src/ibex_Java.cpp.in +++ b/plugins/java/src/ibex_Java.cpp.in @@ -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 @@ -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; } diff --git a/plugins/solver/src/ibex_Solver.cpp b/plugins/solver/src/ibex_Solver.cpp index 52a5dbc07..7560313e5 100644 --- a/plugins/solver/src/ibex_Solver.cpp +++ b/plugins/solver/src/ibex_Solver.cpp @@ -164,7 +164,7 @@ 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()) { @@ -172,9 +172,10 @@ Solver::Status Solver::next() { try { timer.check(time_limit); } - catch(TimeOutException&) { + catch(TimeOutException& e) { flush(); - return TIME_OUT; + if (sol) *sol=NULL; + throw e; } } @@ -199,10 +200,11 @@ Solver::Status Solver::next() { // each intermediate step only if the system is under constrained if (m==0 || (mbox))) { // 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... @@ -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&) { @@ -247,7 +247,8 @@ Solver::Status Solver::next() { } } - return INFEASIBLE; + if (sol) *sol=NULL; + return false; } Solver::Status Solver::solve(const IntervalVector& init_box) { @@ -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); @@ -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) { diff --git a/plugins/solver/src/ibex_Solver.h b/plugins/solver/src/ibex_Solver.h index 32f0fc1f2..f3bac1b3a 100644 --- a/plugins/solver/src/ibex_Solver.h +++ b/plugins/solver/src/ibex_Solver.h @@ -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(). @@ -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(...). diff --git a/tests/TestSolver.cpp b/tests/TestSolver.cpp index afb482fae..e3c278954 100644 --- a/tests/TestSolver.cpp +++ b/tests/TestSolver.cpp @@ -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() { @@ -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() { @@ -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() { @@ -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); }