Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
127 changes: 127 additions & 0 deletions src/strategy/ibex_Solver.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,127 @@
//============================================================================
// I B E X
// File : ibex_Solver.cpp
// Author : Gilles Chabert
// Copyright : Ecole des Mines de Nantes (France)
// License : See the LICENSE file
// Created : May 13, 2012
// Last Update : May 13, 2012
//============================================================================

#include "ibex_Solver.h"
#include "ibex_NoBisectableVariableException.h"
#include <cassert>

using namespace std;

namespace ibex {

Solver::Solver(Ctc& ctc, Bsc& bsc, CellBuffer& buffer) :
ctc(ctc), visitor(NULL), bsc(bsc), buffer(buffer), time_limit(-1), cell_limit(-1), trace(0), time(0), impact(BitSet::all(ctc.nb_var)) {

nb_cells=0;

}

void Solver::setVistor(SolverVisitor *visitor) {
this->visitor = visitor;
}

void Solver::start(const IntervalVector& init_box) {
buffer.flush();

assert(init_box.size()==ctc.nb_var);

Cell* root=new Cell(init_box);

// add data required by this solver
root->add<BisectedVar>();

// add data required by the bisector
bsc.add_backtrackable(*root);
buffer.push(root);

Timer::start();
}

void Solver::iterate(std::vector<IntervalVector>& sols) {
try {
while (!buffer.empty()) {

if (trace==2) cout << buffer << endl;

Cell* c=buffer.top();

int v=c->get<BisectedVar>().var; // last bisected var.

if (v!=-1) // no root node : impact set to 1 for last bisected var only
impact.add(v);
else // root node : impact set to 1 for all variables
impact.fill(0,ctc.nb_var-1);

if(visitor != NULL)
visitor->visit(c->box,EMPTY_BOOL);

ctc.contract(c->box,impact);

if (c->box.is_empty()) {
delete buffer.pop();
impact.remove(v); // note: in case of the root node, we should clear the bitset
// instead but since the search is over, the impact is not used anymore.
continue;
}

if (v!=-1)
impact.remove(v);
else // root node : impact set to 0 for all variables after contraction
impact.clear();

try {

pair<IntervalVector,IntervalVector> boxes=bsc.bisect(*c);
pair<Cell*,Cell*> new_cells=c->bisect(boxes.first,boxes.second);

delete buffer.pop();
buffer.push(new_cells.first);
buffer.push(new_cells.second);
nb_cells+=2;
if (cell_limit >=0 && nb_cells>=cell_limit) throw CellLimitException();}

catch (NoBisectableVariableException&) {
if(visitor != NULL)
visitor->visit(c->box,MAYBE);

sols.push_back(c->box);
delete buffer.pop();
}
time_limit_check();
}
}
catch (TimeOutException&) {
cout << "time limit " << time_limit << "s. reached " << endl;
}
catch (CellLimitException&) {
cout << "cell limit " << cell_limit << " reached " << endl;
}

Timer::stop();
time+= Timer::VIRTUAL_TIMELAPSE();
}

vector<IntervalVector> Solver::solve(const IntervalVector& init_box) {
vector<IntervalVector> sols;

start(init_box);
iterate(sols);

return sols;
}

void Solver::time_limit_check () {
Timer::stop();
time += Timer::VIRTUAL_TIMELAPSE();
if (time_limit >0 && time >=time_limit) throw TimeOutException();
Timer::start();
}

} // end namespace ibex
153 changes: 153 additions & 0 deletions src/strategy/ibex_Solver.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,153 @@
//============================================================================
// I B E X
// File : ibex_Solver.h
// Author : Gilles Chabert
// Copyright : Ecole des Mines de Nantes (France)
// License : See the LICENSE file
// Created : May 13, 2012
// Last Update : August 21, 2013
//============================================================================

#ifndef __IBEX_SOLVER_H__
#define __IBEX_SOLVER_H__

#include "ibex_Ctc.h"
#include "ibex_Pdc.h"
#include "ibex_Bsc.h"
#include "ibex_CellBuffer.h"
#include "ibex_SubPaving.h"
#include "ibex_Timer.h"
#include "ibex_Exception.h"

#include <vector>

namespace ibex {

/**
* \ingroup strategy
*
* \brief Solver.
*
* This class implements an branch and prune algorithm that finds all the solutions of a well constrained systems of equations (the system may contain additional inequalities).
*/


class CellLimitException : public Exception {} ;

/**
* \ingroup set
* \brief Sivia visitor
*/
class SolverVisitor {
public:
/**
* \brief Delete this.
*/
virtual ~SolverVisitor() { }

/**
* \brief Visit
*/
virtual void visit(const IntervalVector& box, BoolInterval status)=0;

};

class Solver {
public:
/**
* \brief Build a solver.
*
* \param ctc - the contractor (for contracting each node of the search tree)
* \param bsc - the bisector (for branching). Contains the stop criterion.
* \param buffer - the cell buffer (a CellStack in a depth first search strategy)
*/
Solver(Ctc& ctc, Bsc& bsc, CellBuffer& buffer);


/**
* \brief Solve the system.
*
* \param init_box - the initial box (the search space)
*
* Return :the vector of solutions (small boxes with the required precision) found by the solver.
*/
std::vector<IntervalVector> solve(const IntervalVector& init_box);


/**
* \brief Set a visitor to provide visibility to Solver process.
*
* \param visitor - The visitor to be reported.
*/
void setVistor(SolverVisitor *visitor);

/**
* \brief The contractor
*
* contractor used by the solver for contracting the current box at each node :
* generally, a sequence (with or without fixpoint) of different contractors (hc4 , acid, Newton , a linear relaxation )
*
*/
Ctc& ctc;

/** Bisector (tests also precision of boxes). */
Bsc& bsc;

/** Cell buffer. */
CellBuffer& buffer;

/** Maximum cpu time used by the solver.
* This parameter allows to bound time complexity.
* The value can be fixed by the user. By default, it is -1 (no limit). */

double time_limit;


/** Maximal number of cells created by the solver.
* This parameter allows to bound the number of nodes in the search tree.
* The value can be fixed by the user. By default, it is -1 (no limit). */
long cell_limit;

/**
* \brief Trace level
*
* the trace level.
* 0 : no trace (default value)
* 1 the solutions are printed each time a new solution is found
* 2 the solutions are printed each time a new solution is found and the current box is printed at each node of the branch and prune algorithm
*/
int trace;

/** Number of nodes in the search tree */
int nb_cells;


/** Remember running time of the last exploration */
double time;

protected :

/**
* \brief Start solving.
*
* Can also be used to restart a new search.
*/
void start(const IntervalVector& init_box);

/**
* \brief Continue solving.
*
* Look for the next solution and push it into the vector.
* \return false if the search is over (true otherwise).
*/
void iterate(std::vector<IntervalVector>& sols);

void time_limit_check();

BitSet impact;
SolverVisitor *visitor;

};

} // end namespace ibex
#endif // __IBEX_SOLVER_H__