From 79b44b874c9527a4ae75b55ec1a1a55a134b7973 Mon Sep 17 00:00:00 2001 From: Guilherme Schvarcz Franco Date: Mon, 28 Nov 2016 17:42:27 +0100 Subject: [PATCH] Solver: Implement visitor pattern & update tests. Fixes: https://github.com/ibex-team/ibex-lib/issues/238 --- src/strategy/ibex_Solver.cpp | 127 +++++++++++++++++++++++++++++ src/strategy/ibex_Solver.h | 153 +++++++++++++++++++++++++++++++++++ 2 files changed, 280 insertions(+) create mode 100644 src/strategy/ibex_Solver.cpp create mode 100644 src/strategy/ibex_Solver.h diff --git a/src/strategy/ibex_Solver.cpp b/src/strategy/ibex_Solver.cpp new file mode 100644 index 000000000..5f3205c38 --- /dev/null +++ b/src/strategy/ibex_Solver.cpp @@ -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 + +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(); + + // add data required by the bisector + bsc.add_backtrackable(*root); + buffer.push(root); + + Timer::start(); +} + +void Solver::iterate(std::vector& sols) { + try { + while (!buffer.empty()) { + + if (trace==2) cout << buffer << endl; + + Cell* c=buffer.top(); + + int v=c->get().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 boxes=bsc.bisect(*c); + pair 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 Solver::solve(const IntervalVector& init_box) { + vector 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 diff --git a/src/strategy/ibex_Solver.h b/src/strategy/ibex_Solver.h new file mode 100644 index 000000000..cd24c803b --- /dev/null +++ b/src/strategy/ibex_Solver.h @@ -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 + +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 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& sols); + + void time_limit_check(); + + BitSet impact; + SolverVisitor *visitor; + +}; + +} // end namespace ibex +#endif // __IBEX_SOLVER_H__