diff options
Diffstat (limited to 'cryptominisat5/cryptominisat-5.6.3/src/compfinder.h')
| -rw-r--r-- | cryptominisat5/cryptominisat-5.6.3/src/compfinder.h | 138 |
1 files changed, 0 insertions, 138 deletions
diff --git a/cryptominisat5/cryptominisat-5.6.3/src/compfinder.h b/cryptominisat5/cryptominisat-5.6.3/src/compfinder.h deleted file mode 100644 index 64e257c71..000000000 --- a/cryptominisat5/cryptominisat-5.6.3/src/compfinder.h +++ /dev/null @@ -1,138 +0,0 @@ -/****************************************** -Copyright (c) 2016, Mate Soos - -Permission is hereby granted, free of charge, to any person obtaining a copy -of this software and associated documentation files (the "Software"), to deal -in the Software without restriction, including without limitation the rights -to use, copy, modify, merge, publish, distribute, sublicense, and/or sell -copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in -all copies or substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR -IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, -FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE -AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER -LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, -OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN -THE SOFTWARE. -***********************************************/ - -#ifndef PARTFINDER_H -#define PARTFINDER_H - -#include <vector> -#include <map> -#include "constants.h" -#include "solvertypes.h" -#include "cloffset.h" - -namespace CMSat { - -class Solver; -class Clause; - -using std::map; -using std::vector; -using std::pair; - -class CompFinder { - - public: - explicit CompFinder(Solver* solver); - void find_components(); - bool getTimedOut() const; - - const map<uint32_t, vector<uint32_t> >& getReverseTable() const; // comp->var - uint32_t getVarComp(const uint32_t var) const; - const vector<uint32_t>& getTable() const; //var -> comp - const vector<uint32_t>& getCompVars(const uint32_t comp); - uint32_t getNumComps() const; - - private: - void addToCompImplicits(); - void add_clauses_to_component(const vector<ClOffset>& cs); - template<class T> - void add_clause_to_component(const T& cl); - template<class T> - bool belong_to_same_component(const T& cl); - template<class T> - void fill_newset_and_tomerge(const T& cl); - void merge_newset_into_single_component(); - - void print_found_components() const; - bool reverse_table_is_correct() const; - void print_and_add_to_sql_result(const double myTime) const; - - struct MySorter - { - bool operator () ( - const pair<uint32_t, uint32_t>& left - , const pair<uint32_t, uint32_t>& right - ) { - return left.second < right.second; - } - }; - - //comp -> vars - map<uint32_t, vector<uint32_t> > reverseTable; - - //var -> comp - vector<uint32_t> table; - - //The comp counter - uint32_t comp_no; - uint32_t used_comp_no; - - //Temporary - vector<uint32_t> newSet; - vector<uint32_t> tomerge; - - //Keep track of time - long long bogoprops_remain; - long long orig_bogoprops; - bool timedout; - - vector<uint16_t>& seen; - Solver* solver; -}; - -inline uint32_t CompFinder::getNumComps() const -{ - return reverseTable.size(); -} - -inline const map<uint32_t, vector<uint32_t> >& CompFinder::getReverseTable() const -{ - assert(!timedout); - return reverseTable; -} - -inline const vector<uint32_t>& CompFinder::getTable() const -{ - assert(!timedout); - return table; -} - -inline uint32_t CompFinder::getVarComp(const uint32_t var) const -{ - assert(!timedout); - return table[var]; -} - -inline const vector<uint32_t>& CompFinder::getCompVars(const uint32_t comp) -{ - assert(!timedout); - return reverseTable[comp]; -} - -inline bool CompFinder::getTimedOut() const -{ - return timedout; -} - -} //End namespace - -#endif //PARTFINDER_H |