diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-29 03:08:05 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-29 03:08:05 +0000 |
commit | 6ba22cdd0e38f9811daefd2aee8218b8b8cf9e0e (patch) | |
tree | 435b1c90d00fd4f6cd05e29ebbdf8e735d8aa68e /src/prop/cryptominisat/Solver/StateSaver.cpp | |
parent | 6e5f551507a2a9af33e7b56107471a096a495862 (diff) |
bringing cryptominisat into the main branch
Diffstat (limited to 'src/prop/cryptominisat/Solver/StateSaver.cpp')
-rw-r--r-- | src/prop/cryptominisat/Solver/StateSaver.cpp | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/src/prop/cryptominisat/Solver/StateSaver.cpp b/src/prop/cryptominisat/Solver/StateSaver.cpp new file mode 100644 index 000000000..379fec2c4 --- /dev/null +++ b/src/prop/cryptominisat/Solver/StateSaver.cpp @@ -0,0 +1,50 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see <http://www.gnu.org/licenses/>. +**************************************************************************************************/ + +#include "StateSaver.h" + +using namespace CMSat; + +StateSaver::StateSaver(Solver& _solver) : + solver(_solver) + , backup_order_heap(Solver::VarOrderLt(solver.activity)) +{ + //Saving Solver state + backup_var_inc = solver.var_inc; + backup_activity.growTo(solver.activity.size()); + std::copy(solver.activity.getData(), solver.activity.getDataEnd(), backup_activity.getData()); + backup_order_heap = solver.order_heap; + backup_polarities = solver.polarity; + backup_restartType = solver.restartType; + backup_propagations = solver.propagations; + backup_random_var_freq = solver.conf.random_var_freq; +} + +void StateSaver::restore() +{ + //Restore Solver state + solver.var_inc = backup_var_inc; + std::copy(backup_activity.getData(), backup_activity.getDataEnd(), solver.activity.getData()); + solver.order_heap = backup_order_heap; + solver.polarity = backup_polarities; + solver.restartType = backup_restartType; + solver.propagations = backup_propagations; + solver.conf.random_var_freq = backup_random_var_freq; + + //Finally, clear the order_heap from variables set/non-decisionned + solver.order_heap.filter(Solver::VarFilter(solver)); +} |