diff options
Diffstat (limited to 'src/prop/cryptominisat/Solver/Gaussian.h')
| -rw-r--r-- | src/prop/cryptominisat/Solver/Gaussian.h | 243 |
1 files changed, 0 insertions, 243 deletions
diff --git a/src/prop/cryptominisat/Solver/Gaussian.h b/src/prop/cryptominisat/Solver/Gaussian.h deleted file mode 100644 index 6e4151811..000000000 --- a/src/prop/cryptominisat/Solver/Gaussian.h +++ /dev/null @@ -1,243 +0,0 @@ -/*********************************************************************************** -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/>. -**************************************************************************************************/ - -#ifndef GAUSSIAN_H -#define GAUSSIAN_H - -#include <vector> -#include <limits> -#include <string> -#include <utility> - -#ifdef _MSC_VER -#include <msvc/stdint.h> -#else -#include <stdint.h> -#endif //_MSC_VER - -#include "SolverTypes.h" -#include "Solver.h" -#include "GaussianConfig.h" -#include "PackedMatrix.h" -#include "BitArray.h" - -//#define VERBOSE_DEBUG -//#define DEBUG_GAUSS - -namespace CMSat { - -using std::string; -using std::pair; -using std::vector; - -class Clause; - -class Gaussian -{ -public: - Gaussian(Solver& solver, const GaussConf& config, const uint32_t matrix_no, const vector<XorClause*>& xorclauses); - ~Gaussian(); - - bool full_init(); - llbool find_truths(vec<Lit>& learnt_clause, uint64_t& conflictC); - - //statistics - void print_stats() const; - void print_matrix_stats() const; - uint32_t get_called() const; - uint32_t get_useful_prop() const; - uint32_t get_useful_confl() const; - bool get_disabled() const; - uint32_t get_unit_truths() const; - void set_disabled(const bool toset); - - //functions used throughout the Solver - void canceling(const uint32_t sublevel); - - friend class ClauseAllocator; - -protected: - Solver& solver; - - //Gauss high-level configuration - const GaussConf& config; - const uint32_t matrix_no; - vector<XorClause*> xorclauses; - - enum gaussian_ret {conflict, unit_conflict, propagation, unit_propagation, nothing}; - gaussian_ret gaussian(PropBy& confl); - - vector<Var> col_to_var_original; //Matches columns to variables - BitArray var_is_in; //variable is part of the the matrix. var_is_in's size is _minimal_ so you should check whether var_is_in.getSize() < var before issuing var_is_in[var] - uint32_t badlevel; - - class matrixset - { - public: - PackedMatrix matrix; // The matrix, updated to reflect variable assignements - BitArray var_is_set; - vector<Var> col_to_var; // col_to_var[COL] tells which variable is at a given column in the matrix. Gives unassigned_var if the COL has been zeroed (i.e. the variable assigned) - uint16_t num_rows; // number of active rows in the matrix. Unactive rows are rows that contain only zeros (and if they are conflicting, then the conflict has been treated) - uint32_t num_cols; // number of active columns in the matrix. The columns at the end that have all be zeroed are no longer active - int least_column_changed; // when updating the matrix, this value contains the smallest column number that has been updated (Gauss elim. can start from here instead of from column 0) - vector<uint16_t> last_one_in_col; //last_one_in_col[COL] tells the last row+1 that has a '1' in that column. Used to reduce the burden of Gauss elim. (it only needs to look until that row) - vector<uint16_t> first_one_in_row; - uint32_t removeable_cols; // the number of columns that have been zeroed out (i.e. assigned) - }; - - //Saved states - vector<matrixset> matrix_sets; // The matrixsets for depths 'decision_from' + 0, 'decision_from' + only_nth_gaussian_save, 'decision_from' + 2*only_nth_gaussian_save, ... 'decision_from' + 'decision_until'. - matrixset cur_matrixset; // The current matrixset, i.e. the one we are working on, or the last one we worked on - - //Varibales to keep Gauss state - bool messed_matrix_vars_since_reversal; - int gauss_last_level; - vector<pair<Clause*, uint32_t> > clauses_toclear; - bool disabled; // Gauss is disabled - - //State of current elimnation - vec<uint32_t> propagatable_rows; //used to store which rows were deemed propagatable during elimination - vector<unsigned char> changed_rows; //used to store which rows were deemed propagatable during elimination - - //Statistics - uint32_t useful_prop; //how many times Gauss gave propagation as a result - uint32_t useful_confl; //how many times Gauss gave conflict as a result - uint32_t called; //how many times called the Gauss - uint32_t unit_truths; //how many unitary (i.e. decisionLevel 0) truths have been found - - //gauss init functions - void init(); // Initalise gauss state - void fill_matrix(matrixset& origMat); // Fills the origMat matrix - uint32_t select_columnorder(vector<uint16_t>& var_to_col, matrixset& origMat); // Fills var_to_col and col_to_var of the origMat matrix. - - //Main function - uint32_t eliminate(matrixset& matrix); //does the actual gaussian elimination - - //matrix update functions - void update_matrix_col(matrixset& matrix, const Var x, const uint32_t col); // Update one matrix column - void update_matrix_by_col_all(matrixset& m); // Update all columns, column-by-column (and not row-by-row) - void set_matrixset_to_cur(); // Save the current matrixset, the cur_matrixset to matrix_sets - //void update_matrix_by_row(matrixset& matrix) const; - //void update_matrix_by_col(matrixset& matrix, const uint32_t last_level) const; - - //conflict&propagation handling - gaussian_ret handle_matrix_prop_and_confl(matrixset& m, uint32_t row, PropBy& confl); - void analyse_confl(const matrixset& m, const uint32_t row, int32_t& maxlevel, uint32_t& size, uint32_t& best_row) const; // analyse conflcit to find the best conflict. Gets & returns the best one in 'maxlevel', 'size' and 'best row' (these are all UINT_MAX when calling this function first, i.e. when there is no other possible conflict to compare to the new in 'row') - gaussian_ret handle_matrix_confl(PropBy& confl, const matrixset& m, const uint32_t maxlevel, const uint32_t best_row); - gaussian_ret handle_matrix_prop(matrixset& m, const uint32_t row); // Handle matrix propagation at row 'row' - vec<Lit> tmp_clause; - - //propagation&conflict handling - void cancel_until_sublevel(const uint32_t until_sublevel); // cancels until sublevel 'until_sublevel'. The var 'until_sublevel' must NOT go over the current level. I.e. this function is ONLY for moving inside the current level - uint32_t find_sublevel(const Var v) const; // find the sublevel (i.e. trail[X]) of a given variable - - //helper functions - bool at_first_init() const; - bool should_init() const; - bool should_check_gauss(const uint32_t decisionlevel) const; - void disable_if_necessary(); - void reset_stats(); - void update_last_one_in_col(matrixset& m); - -private: - - //debug functions - bool check_no_conflict(matrixset& m) const; // Are there any conflicts that the matrixset 'm' causes? - bool nothing_to_propagate(matrixset& m) const; // Are there any conflicts of propagations that matrixset 'm' clauses? - template<class T> - void print_matrix_row(const T& row) const; // Print matrix row 'row' - template<class T> - void print_matrix_row_with_assigns(const T& row) const; - void check_matrix_against_varset(PackedMatrix& matrix,const matrixset& m) const; - bool check_last_one_in_cols(matrixset& m) const; - void check_first_one_in_row(matrixset& m, const uint32_t j); - void print_matrix(matrixset& m) const; - void print_last_one_in_cols(matrixset& m) const; - static string lbool_to_string(const lbool toprint); -}; - -inline bool Gaussian::should_init() const -{ - return (config.decision_until > 0); -} - -inline bool Gaussian::should_check_gauss(const uint32_t decisionlevel) const -{ - return (!disabled - && decisionlevel < config.decision_until); -} - -inline void Gaussian::canceling(const uint32_t sublevel) -{ - if (disabled) - return; - uint32_t a = 0; - for (int i = clauses_toclear.size()-1; i >= 0 && clauses_toclear[i].second > sublevel; i--) { - solver.clauseAllocator.clauseFree(clauses_toclear[i].first); - a++; - } - clauses_toclear.resize(clauses_toclear.size()-a); - - if (messed_matrix_vars_since_reversal) - return; - int c = std::min((int)gauss_last_level, (int)(solver.trail.size())-1); - for (; c >= (int)sublevel; c--) { - Var var = solver.trail[c].var(); - if (var < var_is_in.getSize() - && var_is_in[var] - && cur_matrixset.var_is_set[var]) { - messed_matrix_vars_since_reversal = true; - return; - } - } -} - -inline uint32_t Gaussian::get_unit_truths() const -{ - return unit_truths; -} - -inline uint32_t Gaussian::get_called() const -{ - return called; -} - -inline uint32_t Gaussian::get_useful_prop() const -{ - return useful_prop; -} - -inline uint32_t Gaussian::get_useful_confl() const -{ - return useful_confl; -} - -inline bool Gaussian::get_disabled() const -{ - return disabled; -} - -inline void Gaussian::set_disabled(const bool toset) -{ - disabled = toset; -} - -//std::ostream& operator << (std::ostream& os, const vec<Lit>& v); - -} - -#endif //GAUSSIAN_H |