diff options
Diffstat (limited to 'cryptominisat5/cryptominisat-5.6.3/src/watched.h')
-rw-r--r-- | cryptominisat5/cryptominisat-5.6.3/src/watched.h | 321 |
1 files changed, 0 insertions, 321 deletions
diff --git a/cryptominisat5/cryptominisat-5.6.3/src/watched.h b/cryptominisat5/cryptominisat-5.6.3/src/watched.h deleted file mode 100644 index bf75c5b1e..000000000 --- a/cryptominisat5/cryptominisat-5.6.3/src/watched.h +++ /dev/null @@ -1,321 +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 WATCHED_H -#define WATCHED_H - -//#define DEBUG_WATCHED - -#include "clabstraction.h" -#include "constants.h" -#include "cloffset.h" -#include "solvertypes.h" - -#include <limits> -#include <string.h> - - -namespace CMSat { - -enum WatchType { - watch_clause_t = 0 - , watch_binary_t = 1 - , watch_idx_t = 3 -}; - -/** -@brief An element in the watchlist. Natively contains 2- and 3-long clauses, others are referenced by pointer - -This class contains two 32-bit datapieces. They are either used as: -\li One literal, in the case of binary clauses -\li Two literals, in the case of tertiary clauses -\li One blocking literal (i.e. an example literal from the clause) and a clause -offset (as per ClauseAllocator ), in the case of long clauses -*/ -class Watched { - public: - /** - @brief Constructor for a long (>3) clause - */ - Watched(const ClOffset offset, Lit blockedLit) : - data1(blockedLit.toInt()) - , type(watch_clause_t) - , data2(offset) - { - } - - /** - @brief Constructor for a long (>3) clause - */ - Watched(const ClOffset offset, cl_abst_type abst) : - data1(abst) - , type(watch_clause_t) - , data2(offset) - { - } - - Watched() : - data1 (std::numeric_limits<uint32_t>::max()) - , type(watch_clause_t) // initialize type with most generic type of clause - , data2(std::numeric_limits<uint32_t>::max() >> 2) - {} - - /** - @brief Constructor for a binary clause - */ - Watched(const Lit lit, const bool red) : - data1(lit.toInt()) - , type(watch_binary_t) - , data2(red) - { - } - - /** - @brief Constructor for an Index value - */ - explicit Watched(const uint32_t idx) : - data1(idx) - , type(watch_idx_t) - { - } - - /** - @brief To update the blocked literal of a >3-long normal clause - */ - void setBlockedLit(const Lit blockedLit) - { - #ifdef DEBUG_WATCHED - assert(type == watch_clause_t); - #endif - data1 = blockedLit.toInt(); - } - - WatchType getType() const - { - // we rely that WatchType enum is in [0-3] range and fits into type field two bits - return static_cast<WatchType>(type); - } - - bool isBin() const - { - return (type == watch_binary_t); - } - - bool isClause() const - { - return (type == watch_clause_t); - } - - bool isIdx() const - { - return (type == watch_idx_t); - } - - uint32_t get_idx() const - { - #ifdef DEBUG_WATCHED - assert(type == watch_idx_t); - #endif - return data1; - } - - /** - @brief Get the sole other lit of the binary clause, or get lit2 of the tertiary clause - */ - Lit lit2() const - { - #ifdef DEBUG_WATCHED - assert(isBin()); - #endif - return Lit::toLit(data1); - } - - /** - @brief Set the sole other lit of the binary clause - */ - void setLit2(const Lit lit) - { - #ifdef DEBUG_WATCHED - assert(isBin()); - #endif - data1 = lit.toInt(); - } - - bool red() const - { - #ifdef DEBUG_WATCHED - assert(isBin()); - #endif - return data2 & 1; - } - - void setRed(const bool toSet) - { - #ifdef DEBUG_WATCHED - assert(isBin()); - assert(red()); - #endif - assert(toSet == false); - data2 &= (~(1U)); - } - - void mark_bin_cl() - { - #ifdef DEBUG_WATCHED - assert(isBin()); - #endif - data2 |= 2; - } - - void unmark_bin_cl() - { - #ifdef DEBUG_WATCHED - assert(isBin()); - #endif - data2 &= 1; - } - - bool bin_cl_marked() const - { - #ifdef DEBUG_WATCHED - assert(isBin()); - #endif - return data2&2; - } - - /** - @brief Get example literal (blocked lit) of a normal >3-long clause - */ - Lit getBlockedLit() const - { - #ifdef DEBUG_WATCHED - assert(isClause()); - #endif - return Lit::toLit(data1); - } - - cl_abst_type getAbst() const - { - #ifdef DEBUG_WATCHED - assert(isClause()); - #endif - return data1; - } - - /** - @brief Get offset of a >3-long normal clause or of an xor clause (which may be 3-long) - */ - ClOffset get_offset() const - { - #ifdef DEBUG_WATCHED - assert(isClause()); - #endif - return data2; - } - - bool operator==(const Watched& other) const - { - return data1 == other.data1 && data2 == other.data2 && type == other.type; - } - - bool operator!=(const Watched& other) const - { - return !(*this == other); - } - - private: - uint32_t data1; - // binary, tertiary or long, as per WatchType - // currently WatchType is enum with range [0..3] and fits in type - // in case if WatchType extended type size won't be enough. - ClOffset type:2; - ClOffset data2:EFFECTIVELY_USEABLE_BITS; -}; - -inline std::ostream& operator<<(std::ostream& os, const Watched& ws) -{ - - if (ws.isClause()) { - os << "Clause offset " << ws.get_offset(); - } - - if (ws.isBin()) { - os << "Bin lit " << ws.lit2() << " (red: " << ws.red() << " )"; - } - - return os; -} - -struct OccurClause { - OccurClause(const Lit _lit, const Watched _ws) : - lit(_lit) - , ws(_ws) - {} - - OccurClause() : - lit(lit_Undef) - {} - - bool operator==(const OccurClause& other) const - { - return lit == other.lit && ws == other.ws; - } - - Lit lit; - Watched ws; -}; - -struct WatchSorterBinTriLong { - bool operator()(const Watched& a, const Watched& b) - { - assert(!a.isIdx()); - assert(!b.isIdx()); - - //Anything but clause! - if (a.isClause()) { - //A is definitely not better than B - return false; - } - if (b.isClause()) { - //B is clause, A is NOT a clause. So A is better than B. - return true; - } - - //Both are BIN - assert(a.isBin()); - assert(b.isBin()); - - if (a.lit2() != b.lit2()) { - return a.lit2() < b.lit2(); - } - - if (a.red() != b.red()) { - return !a.red(); - } - return false; - } - }; - - -} //end namespace - -#endif //WATCHED_H |