diff options
Diffstat (limited to 'src/prop/cryptominisat/Solver/Solver.h')
| -rw-r--r-- | src/prop/cryptominisat/Solver/Solver.h | 859 |
1 files changed, 0 insertions, 859 deletions
diff --git a/src/prop/cryptominisat/Solver/Solver.h b/src/prop/cryptominisat/Solver/Solver.h deleted file mode 100644 index 9276823dd..000000000 --- a/src/prop/cryptominisat/Solver/Solver.h +++ /dev/null @@ -1,859 +0,0 @@ -/****************************************************************************************[Solver.h] -MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson -CryptoMiniSat -- Copyright (c) 2009 Mate Soos -glucose -- Gilles Audemard, Laurent Simon (2008) - -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 SOLVER_H -#define SOLVER_H - -#include <cstdio> -#include <string.h> -#include <stdio.h> -#include <stack> -#include <stdexcept> - -//#define ANIMATE3D - -#include "PropBy.h" -#include "Vec.h" -#include "Heap.h" -#include "Alg.h" -#include "MersenneTwister.h" -#include "SolverTypes.h" -#include "Clause.h" -#include "constants.h" -#include "BoundedQueue.h" -#include "GaussianConfig.h" -#include "ClauseAllocator.h" -#include "SolverConf.h" - -namespace CMSat { - -class Gaussian; -class MatrixFinder; -class Conglomerate; -class VarReplacer; -class XorFinder; -class FindUndef; -class ClauseCleaner; -class FailedLitSearcher; -class Subsumer; -class XorSubsumer; -class RestartTypeChooser; -class StateSaver; -class UselessBinRemover; -class SCCFinder; -class ClauseVivifier; -class SharedData; -class DataSync; -class BothCache; - -#ifdef VERBOSE_DEBUG -#define DEBUG_UNCHECKEDENQUEUE_LEVEL0 -using std::cout; -using std::endl; -#endif - -struct reduceDB_ltMiniSat -{ - bool operator () (const Clause* x, const Clause* y); -}; - -struct reduceDB_ltGlucose -{ - bool operator () (const Clause* x, const Clause* y); -}; - -struct PolaritySorter -{ - PolaritySorter(vector<char>& polarity) : - pol(polarity) - {} - - bool operator()(const Lit lit1, const Lit lit2) const - { - return (((((bool)pol[lit1.var()])^(lit1.sign())) == false) - && ((((bool)pol[lit2.var()])^(lit2.sign())) == true)); - } - vector<char>& pol; -}; - -/** -@brief The main solver class - -This class creates and manages all the others. It is here that settings must -be set, and it is here that all data enter and leaves the system. The basic -use is to add normal and XOR clauses, and then solve(). The solver will then -solve the problem, and return with either a SAT solution with corresponding -variable settings, or report that the problem in UNSATisfiable. - -The prolbem-solving can be interrupted with the "interrupt" varible, and can -also be pre-set to stop after a certain number of restarts. The data until the -interruption can be dumped by previously setting parameters like -dumpSortedLearnts -*/ -class Solver -{ -public: - - // Constructor/Destructor: - // - Solver(const SolverConf& conf = SolverConf(), const GaussConf& _gaussconfig = GaussConf(), SharedData* sharedUnitData = NULL); - ~Solver(); - - // Problem specification: - // - Var newVar (bool dvar = true) throw (std::out_of_range); // Add a new variable with parameters specifying variable mode. - template<class T> - bool addClause (T& ps); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method! - template<class T> - bool addLearntClause(T& ps, const uint32_t glue = 10, const float miniSatActivity = 10.0); - template<class T> - bool addXorClause (T& ps, bool xorEqualFalse) throw (std::out_of_range); // Add a xor-clause to the solver. NOTE! 'ps' may be shrunk by this method! - - // Solving: - // - lbool solve (const vec<Lit>& assumps); ///<Search for a model that respects a given set of assumptions. - lbool solve (); ///<Search without assumptions. - void handleSATSolution(); ///<Extends model, if needed, and fills "model" - void handleUNSATSolution(); ///<If conflict really was zero-length, sets OK to false - bool okay () const; ///<FALSE means solver is in a conflicting state - - // Variable mode: - // - void setDecisionVar (Var v, bool b); ///<Declare if a variable should be eligible for selection in the decision heuristic. - void addBranchingVariable (Var v); - - // Read state: - // - lbool value (const Var x) const; ///<The current value of a variable. - lbool value (const Lit p) const; ///<The current value of a literal. - lbool modelValue (const Lit p) const; ///<The value of a literal in the last model. The last call to solve must have been satisfiable. - uint32_t nAssigns () const; ///<The current number of assigned literals. - uint32_t nClauses () const; ///<The current number of original clauses. - uint32_t nLiterals () const; ///<The current number of total literals. - uint32_t nLearnts () const; ///<The current number of learnt clauses. - uint32_t nVars () const; ///<The current number of variables. - - // Extra results: (read-only member variable) - // - vec<lbool> model; ///<If problem is satisfiable, this vector contains the model (if any). - vec<Lit> conflict; ///<If problem is unsatisfiable (possibly under assumptions), this vector represent the final conflict clause expressed in the assumptions. - - // Mode of operation: - // - SolverConf conf; - GaussConf gaussconfig; ///<Configuration for the gaussian elimination can be set here - bool needToInterrupt; ///<Used internally mostly. If set to TRUE, we will interrupt cleanly ASAP. The important thing is "cleanly", since we need to wait until a point when all datastructures are in a sane state (i.e. not in the middle of some algorithm) - - //Logging - void needStats(); // Prepares the solver to output statistics - void needProofGraph(); // Prepares the solver to output proof graphs during solving - const vec<Clause*>& get_sorted_learnts(); //return the set of learned clauses, sorted according to the logic used in MiniSat to distinguish between 'good' and 'bad' clauses - const vec<Clause*>& get_learnts() const; //Get all learnt clauses that are >1 long - vector<Lit> get_unitary_learnts() const; //return the set of unitary learnt clauses - uint32_t get_unitary_learnts_num() const; //return the number of unitary learnt clauses - bool dumpSortedLearnts(const std::string& fileName, const uint32_t maxSize); // Dumps all learnt clauses (including unitary ones) into the file; returns true for success, false for failure - bool needLibraryCNFFile(const std::string& fileName); //creates file in current directory with the filename indicated, and puts all calls from the library into the file. - bool dumpOrigClauses(const std::string& fileName) const; - void printBinClause(const Lit litP1, const Lit litP2, FILE* outfile) const; - - uint32_t get_sum_gauss_called() const; - uint32_t get_sum_gauss_confl() const; - uint32_t get_sum_gauss_prop() const; - uint32_t get_sum_gauss_unit_truths() const; - - //Printing statistics - void printStats(); - uint32_t getNumElimSubsume() const; ///<Get number of variables eliminated - uint32_t getNumElimXorSubsume() const; ///<Get number of variables eliminated with xor-magic - uint32_t getNumXorTrees() const; ///<Get the number of trees built from 2-long XOR-s. This is effectively the number of variables that replace other variables - uint32_t getNumXorTreesCrownSize() const; ///<Get the number of variables being replaced by other variables - /** - @brief Get total time spent in Subsumer. - - This includes: subsumption, self-subsuming resolution, variable elimination, - blocked clause elimination, subsumption and self-subsuming resolution - using non-existent binary clauses. - */ - double getTotalTimeSubsumer() const; - double getTotalTimeFailedLitSearcher() const; - double getTotalTimeSCC() const; - - /** - @brief Get total time spent in XorSubsumer. - - This included subsumption, variable elimination through XOR, and local - substitution (see Heule's Thesis) - */ - double getTotalTimeXorSubsumer() const; - -protected: - //gauss - bool clearGaussMatrixes(); - vector<Gaussian*> gauss_matrixes; - void print_gauss_sum_stats(); - uint32_t sum_gauss_called; - uint32_t sum_gauss_confl; - uint32_t sum_gauss_prop; - uint32_t sum_gauss_unit_truths; - - // Statistics - // - template<class T, class T2> - void printStatsLine(std::string left, T value, T2 value2, std::string extra); - template<class T> - void printStatsLine(std::string left, T value, std::string extra = ""); - uint64_t starts; ///<Num restarts - uint64_t dynStarts; ///<Num dynamic restarts - uint64_t staticStarts; ///<Num static restarts: note that after full restart, we do a couple of static restarts always - /** - @brief Num full restarts - - Full restarts are restarts that are made always, no matter what, after - a certan number of conflicts have passed. The problem will tried to be - decomposed into multiple parts, and then there will be a couple of static - restarts made. Finally, the problem will be determined to be MiniSat-type - or Glucose-type. - - NOTE: I belive there is a point in having full restarts even if the - glue-clause vs. MiniSat clause can be fully resolved - */ - uint64_t fullStarts; ///<Number of full restarts made - uint64_t decisions; ///<Number of decisions made - uint64_t rnd_decisions; ///<Numer of random decisions made - /** - @brief An approximation of accumulated propagation difficulty - - It does not hold the number of propagations made. Rather, it holds a - value that is approximate of the difficulty of the propagations made - This makes sense, since it is not at all the same difficulty to proapgate - a 2-long clause than to propagate a 20-long clause. In certain algorihtms, - there is a need to know how difficult the propagation part was. This value - can be used in these algorihms. However, the reported "statistic" will be - bogus. - */ - uint64_t propagations; - uint64_t conflicts; ///<Num conflicts - uint64_t clauses_literals, learnts_literals, max_literals, tot_literals; - uint64_t nbGlue2; ///<Num learnt clauses that had a glue of 2 when created - uint64_t numNewBin; ///<new binary clauses that have been found through some form of resolution (shrinking, conflicts, etc.) - uint64_t lastNbBin; ///<Last time we seached for SCCs, numBins was this much - uint64_t lastSearchForBinaryXor; ///<Last time we looked for binary xors, this many bogoprops(=propagations) has been done - uint64_t nbReduceDB; ///<Number of times learnt clause have been cleaned - uint64_t improvedClauseNo; ///<Num clauses improved using on-the-fly subsumption - uint64_t improvedClauseSize; ///<Num literals removed using on-the-fly subsumption - uint64_t numShrinkedClause; ///<Num clauses improved using on-the-fly self-subsuming resolution - uint64_t numShrinkedClauseLits; ///<Num literals removed by on-the-fly self-subsuming resolution - uint64_t moreRecurMinLDo; ///<Decided to carry out transitive on-the-fly self-subsuming resolution on this many clauses - uint64_t updateTransCache; ///<Number of times the transitive OTF-reduction cache has been updated - uint64_t nbClOverMaxGlue; ///<Number or clauses over maximum glue defined in maxGlue - - //Multi-threading - DataSync* dataSync; - - // Helper structures: - // - struct VarOrderLt { - const vec<uint32_t>& activity; - bool operator () (Var x, Var y) const { - return activity[x] > activity[y]; - } - VarOrderLt(const vec<uint32_t>& act) : activity(act) { } - }; - - struct VarFilter { - const Solver& s; - VarFilter(const Solver& _s) : s(_s) {} - bool operator()(Var v) const { - return s.assigns[v].isUndef() && s.decision_var[v]; - } - }; - - // Solver state: - // - bool ok; ///< If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used! - ClauseAllocator clauseAllocator; ///< Handles memory allocation for claues - vec<Clause*> clauses; ///< List of problem clauses that are normally larger than 2. Sometimes, due to on-the-fly self-subsuming resoulution, clauses here become 2-long. They are never purposfully put here such that they are long - vec<XorClause*> xorclauses; ///< List of problem xor-clauses. Will be freed - vec<Clause*> learnts; ///< List of learnt clauses. - uint32_t numBins; - vec<XorClause*> freeLater; ///< xor clauses that need to be freed later (this is needed due to Gauss) \todo Get rid of this - float cla_inc; ///< Amount to bump learnt clause oldActivity with - vec<vec<Watched> > watches; ///< 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). - vec<lbool> assigns; ///< The current assignments - vector<char> decision_var; ///< Declares if a variable is eligible for selection in the decision heuristic. - vec<Lit> trail; ///< Assignment stack; stores all assigments made in the order they were made. - vec<uint32_t> trail_lim; ///< Separator indices for different decision levels in 'trail'. - vec<PropBy> reason; ///< 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. - vec<int32_t> level; ///< 'level[var]' contains the level at which the assignment was made. - vec<BinPropData> binPropData; - uint32_t qhead; ///< Head of queue (as index into the trail) - Lit failBinLit; ///< Used to store which watches[~lit] we were looking through when conflict occured - vec<Lit> assumptions; ///< Current set of assumptions provided to solve by the user. - bqueue<uint32_t> avgBranchDepth; ///< Avg branch depth. We collect this, and use it to do random look-around in the searchspace during simplifyProblem() - MTRand mtrand; ///< random number generator - vector<Var> branching_variables; - - ///////////////// - // Variable activities - ///////////////// - Heap<VarOrderLt> order_heap; ///< A priority queue of variables ordered with respect to the variable activity. All variables here MUST be decision variables. If you changed the decision variables, you MUST filter this - vec<uint32_t> activity; ///< A heuristic measurement of the activity of a variable. - uint32_t var_inc; ///< Amount to bump next variable with. - - ///////////////// - // Learnt clause cleaning - ///////////////// - uint64_t numCleanedLearnts; ///< Number of times learnt clauses have been removed through simplify() up until now - uint32_t nbClBeforeRed; ///< Number of learnt clauses before learnt-clause cleaning - uint32_t nbCompensateSubsumer; ///< Number of learnt clauses that subsumed normal clauses last time subs. was executed (used to delay learnt clause-cleaning) - - ///////////////////////// - // For glue calculation & dynamic restarts - ///////////////////////// - //uint64_t MYFLAG; ///<For glue calculation - template<class T> - uint32_t calcNBLevels(const T& ps); - //vec<uint64_t> permDiff; ///<permDiff[var] is used to count the number of different decision level variables in learnt clause (filled with data from MYFLAG ) - vec<Var> lastDecisionLevel; - bqueue<uint32_t> glueHistory; ///< Set of last decision levels in (glue of) conflict clauses. Used for dynamic restarting - #ifdef ENABLE_UNWIND_GLUE - vec<Clause*> unWindGlue; - #endif //ENABLE_UNWIND_GLUE - - // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is - // used, exept 'seen' wich is used in several places. - // - vector<char> seen; ///<Used in multiple places. Contains 2 * numVars() elements, all zeroed out - vector<Lit> seen_vec; - vec<Lit> analyze_stack; - vec<Lit> analyze_toclear; - - //////////// - // Transitive on-the-fly self-subsuming resolution - /////////// - class TransCache { - public: - TransCache() : - conflictLastUpdated(std::numeric_limits<uint64_t>::max()) - {}; - - vector<Lit> lits; - uint64_t conflictLastUpdated; - }; - class LitReachData { - public: - LitReachData() : - lit(lit_Undef) - , numInCache(0) - {} - Lit lit; - uint32_t numInCache; - }; - vector<char> seen2; ///<To reduce temoprary data creation overhead. Used in minimiseLeartFurther(). contains 2 * numVars() elements, all zeroed out - vec<Lit> allAddedToSeen2; ///<To reduce temoprary data creation overhead. Used in minimiseLeartFurther() - std::stack<Lit> toRecursiveProp; ///<To reduce temoprary data creation overhead. Used in minimiseLeartFurther() - vector<TransCache> transOTFCache; - bqueue<uint32_t> conflSizeHist; - void minimiseLeartFurther(vec<Lit>& cl, const uint32_t glue); - void transMinimAndUpdateCache(const Lit lit, uint32_t& moreRecurProp); - void saveOTFData(); - vector<LitReachData>litReachable; - void calcReachability(); - void cleanCache(); - void cleanCachePart(const Lit vertLit); - - //////////// - //Logging - /////////// - FILE *libraryCNFFile; //The file that all calls from the library are logged - - ///////////////// - // Propagating - //////////////// - Lit pickBranchLit (); // Return the next decision variable. - void newDecisionLevel (); // Begins a new decision level. - void uncheckedEnqueue (const Lit p, const PropBy& from = PropBy()); // Enqueue a literal. Assumes value of literal is undefined. - void uncheckedEnqueueLight (const Lit p); - void uncheckedEnqueueLight2(const Lit p, const uint32_t binPropDatael, const Lit lev1Ancestor, const bool learntLeadHere); - PropBy propagateBin(vec<Lit>& uselessBin); - PropBy propagateNonLearntBin(); - bool multiLevelProp; - bool propagateBinExcept(const Lit exceptLit); - bool propagateBinOneLevel(); - template<bool full> - PropBy propagate(const bool update = true); // Perform unit propagation. Returns possibly conflicting clause. - template<bool full> - bool propTriClause (vec<Watched>::iterator &i, const Lit p, PropBy& confl); - template<bool full> - bool propBinaryClause(vec<Watched>::iterator &i, const Lit p, PropBy& confl); - template<bool full> - bool propNormalClause(vec<Watched>::iterator &i, vec<Watched>::iterator &j, const Lit p, PropBy& confl, const bool update); - template<bool full> - bool propXorClause (vec<Watched>::iterator &i, vec<Watched>::iterator &j, const Lit p, PropBy& confl); - void sortWatched(); - - /////////////// - // Conflicting - /////////////// - void cancelUntil (int level); // Backtrack until a certain level. - void cancelUntilLight(); - Clause* analyze (PropBy confl, vec<Lit>& out_learnt, int& out_btlevel, uint32_t &nblevels, const bool update); - void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? - bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') - void insertVarOrder (Var x); // Insert a variable in the decision order priority queue. - - ///////////////// - // Searching - ///////////////// - lbool search (const uint64_t nof_conflicts, const uint64_t nof_conflicts_fullrestart, const bool update = true); // Search for a given number of conflicts. - llbool handle_conflict (vec<Lit>& learnt_clause, PropBy confl, uint64_t& conflictC, const bool update);// Handles the conflict clause - llbool new_decision (const uint64_t nof_conflicts, const uint64_t nof_conflicts_fullrestart, const uint64_t conflictC); // Handles the case when all propagations have been made, and now a decision must be made - - ///////////////// - // Maintaining Variable/Clause activity: - ///////////////// - void claBumpActivity (Clause& c); - void varDecayActivity (); // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead. - void varBumpActivity (Var v); // Increase a variable with the current 'bump' value. - void claDecayActivity (); // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead. - - ///////////////// - // Operations on clauses: - ///////////////// - template<class T> bool addClauseHelper(T& ps) throw (std::out_of_range); - template <class T> - Clause* addClauseInt(T& ps, const bool learnt = false, const uint32_t glue = 10, const float miniSatActivity = 10.0, const bool inOriginalInput = false); - template<class T> - XorClause* addXorClauseInt(T& ps, bool xorEqualFalse, const bool learnt = false) throw (std::out_of_range); - void attachBinClause(const Lit lit1, const Lit lit2, const bool learnt); - void attachClause (XorClause& c); - void attachClause (Clause& c); // Attach a clause to watcher lists. - void detachClause (const XorClause& c); - void detachClause (const Clause& c); // Detach a clause to watcher lists. - void detachModifiedClause(const Lit lit1, const Lit lit2, const Lit lit3, const uint32_t origSize, const Clause* address); - void detachModifiedClause(const Var var1, const Var var2, const uint32_t origSize, const XorClause* address); - template<class T> - void removeClause(T& c); // Detach and free a clause. - bool locked (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state. - - /////////////////////////// - // Debug clause attachment - /////////////////////////// - void testAllClauseAttach() const; - void findAllAttach() const; - bool findClause(XorClause* c) const; - bool findClause(Clause* c) const; - bool xorClauseIsAttached(const XorClause& c) const; - bool normClauseIsAttached(const Clause& c) const; - - // Misc: - // - uint32_t decisionLevel () const; // Gives the current decisionlevel. - uint32_t abstractLevel (const Var x) const; // Used to represent an abstraction of sets of decision levels. - - ///////////////////////// - //Classes that must be friends, since they accomplish things on our datastructures - ///////////////////////// - friend class VarFilter; - friend class Gaussian; - friend class FindUndef; - friend class XorFinder; - friend class Conglomerate; - friend class MatrixFinder; - friend class VarReplacer; - friend class ClauseCleaner; - friend class RestartTypeChooser; - friend class FailedLitSearcher; - friend class Subsumer; - friend class XorSubsumer; - friend class StateSaver; - friend class UselessBinRemover; - friend class OnlyNonLearntBins; - friend class ClauseAllocator; - friend class CompleteDetachReatacher; - friend class SCCFinder; - friend class ClauseVivifier; - friend class DataSync; - friend class BothCache; - Conglomerate* conglomerate; - VarReplacer* varReplacer; - ClauseCleaner* clauseCleaner; - FailedLitSearcher* failedLitSearcher; - Subsumer* subsumer; - XorSubsumer* xorSubsumer; - RestartTypeChooser* restartTypeChooser; - MatrixFinder* matrixFinder; - SCCFinder* sCCFinder; - ClauseVivifier* clauseVivifier; - - ///////////////////////// - // Restart type handling - ///////////////////////// - bool chooseRestartType(const uint32_t& lastFullRestart); - void setDefaultRestartType(); - bool checkFullRestart(uint64_t& nof_conflicts, uint64_t& nof_conflicts_fullrestart, uint32_t& lastFullRestart); - RestartType restartType; ///<Used internally to determine which restart strategy is currently in use - RestartType lastSelectedRestartType; ///<The last selected restart type. Used when we are just after a full restart, and need to know how to really act - - ////////////////////////// - // Problem simplification - ////////////////////////// - void performStepsBeforeSolve(); - lbool simplifyProblem(const uint32_t numConfls); - void reduceDB(); // Reduce the set of learnt clauses. - bool simplify(); // Removes satisfied clauses and finds binary xors - bool simplifying; ///<We are currently doing burst search - double totalSimplifyTime; - uint32_t simpDB_assigns; ///< Number of top-level assignments since last execution of 'simplify()'. - int64_t simpDB_props; ///< Remaining number of propagations that must be made before next execution of 'simplify()'. - - ///////////////////////////// - // SAT solution verification - ///////////////////////////// - void checkSolution (); - bool verifyModel () const; - bool verifyBinClauses() const; - bool verifyClauses (const vec<Clause*>& cs) const; - bool verifyXorClauses () const; - - // Debug & etc: - void printAllClauses(); - void printLit (const Lit l) const; - void checkLiteralCount(); - void printStatHeader () const; - void printRestartStat (const char* type = "N"); - void printEndSearchStat(); - void addSymmBreakClauses(); - void initialiseSolver(); - - //Misc related binary clauses - void dumpBinClauses(const bool alsoLearnt, const bool alsoNonLearnt, FILE* outfile) const; - uint32_t countNumBinClauses(const bool alsoLearnt, const bool alsoNonLearnt) const; - uint32_t getBinWatchSize(const bool alsoLearnt, const Lit lit); - void printStrangeBinLit(const Lit lit) const; - - ///////////////////// - // Polarity chooser - ///////////////////// - void calculateDefaultPolarities(); //Calculates the default polarity for each var, and fills defaultPolarities[] with it - bool defaultPolarity(); //if polarity_mode is not polarity_auto, this returns the default polarity of the variable - void tallyVotesBin(vec<double>& votes) const; - void tallyVotes(const vec<Clause*>& cs, vec<double>& votes) const; - void tallyVotes(const vec<XorClause*>& cs, vec<double>& votes) const; - void setPolarity(Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'. - vector<char> polarity; // The preferred polarity of each variable. -}; - - - -//********************************** -// Implementation of inline methods -//********************************** - -inline void Solver::insertVarOrder(Var x) -{ - if (!order_heap.inHeap(x) && decision_var[x]) order_heap.insert(x); -} - -inline void Solver::varDecayActivity() -{ - var_inc *= 11; - var_inc /= 10; -} -inline void Solver::varBumpActivity(Var v) -{ - if ( (activity[v] += var_inc) > (0x1U) << 24 ) { - //printf("RESCALE!!!!!!\n"); - //std::cout << "var_inc: " << var_inc << std::endl; - // Rescale: - for (Var var = 0; var != nVars(); var++) { - activity[var] >>= 14; - } - var_inc >>= 14; - //var_inc = 1; - //std::cout << "var_inc: " << var_inc << std::endl; - - /*Heap<VarOrderLt> copy_order_heap2(order_heap); - while(!copy_order_heap2.empty()) { - Var v = copy_order_heap2.getmin(); - if (decision_var[v]) - std::cout << "var_" << v+1 << " act: " << activity[v] << std::endl; - }*/ - } - - // Update order_heap with respect to new activity: - if (order_heap.inHeap(v)) - order_heap.decrease(v); -} - -inline void Solver::claBumpActivity (Clause& c) -{ - if ( (c.getMiniSatAct() += cla_inc) > 1e20 ) { - // Rescale: - for (uint32_t i = 0; i < learnts.size(); i++) - learnts[i]->getMiniSatAct() *= 1e-17; - cla_inc *= 1e-20; - } -} - -inline void Solver::claDecayActivity() -{ - //cla_inc *= clause_decay; -} - -inline bool Solver::locked(const Clause& c) const -{ - if (c.size() <= 3) return true; //we don't know in this case :I - PropBy from(reason[c[0].var()]); - return from.isClause() && !from.isNULL() && from.getClause() == clauseAllocator.getOffset(&c) && value(c[0]) == l_True; -} - -inline void Solver::newDecisionLevel() -{ - trail_lim.push(trail.size()); - #ifdef VERBOSE_DEBUG - cout << "New decision level: " << trail_lim.size() << endl; - #endif -} -/*inline int Solver::nbPropagated(int level) { - if (level == decisionLevel()) - return trail.size() - trail_lim[level-1] - 1; - return trail_lim[level] - trail_lim[level-1] - 1; -}*/ -inline uint32_t Solver::decisionLevel () const -{ - return trail_lim.size(); -} -inline uint32_t Solver::abstractLevel (const Var x) const -{ - return 1 << (level[x] & 31); -} -inline lbool Solver::value (const Var x) const -{ - return assigns[x]; -} -inline lbool Solver::value (const Lit p) const -{ - return assigns[p.var()] ^ p.sign(); -} -inline lbool Solver::modelValue (const Lit p) const -{ - return model[p.var()] ^ p.sign(); -} -inline uint32_t Solver::nAssigns () const -{ - return trail.size(); -} -inline uint32_t Solver::nClauses () const -{ - return clauses.size() + xorclauses.size(); -} -inline uint32_t Solver::nLiterals () const -{ - return clauses_literals + learnts_literals; -} -inline uint32_t Solver::nLearnts () const -{ - return learnts.size(); -} -inline uint32_t Solver::nVars () const -{ - return assigns.size(); -} -inline void Solver::setPolarity (Var v, bool b) -{ - polarity [v] = (char)b; -} -inline void Solver::setDecisionVar(Var v, bool b) -{ - decision_var[v] = b; - if (b) { - insertVarOrder(v); - } -} -inline void Solver::addBranchingVariable(Var v) -{ - branching_variables.push_back(v); -} -inline lbool Solver::solve () -{ - vec<Lit> tmp; - return solve(tmp); -} -inline bool Solver::okay () const -{ - return ok; -} - -inline uint32_t Solver::get_sum_gauss_unit_truths() const -{ - return sum_gauss_unit_truths; -} - -inline uint32_t Solver::get_sum_gauss_called() const -{ - return sum_gauss_called; -} - -inline uint32_t Solver::get_sum_gauss_confl() const -{ - return sum_gauss_confl; -} - -inline uint32_t Solver::get_sum_gauss_prop() const -{ - return sum_gauss_prop; -} - -inline uint32_t Solver::get_unitary_learnts_num() const -{ - if (decisionLevel() > 0) - return trail_lim[0]; - else - return trail.size(); -} - -template<class T> -inline void Solver::removeClause(T& c) -{ - detachClause(c); - clauseAllocator.clauseFree(&c); -} - -//********************************** -// Debug + etc: -//********************************** - -static inline void logLit(FILE* f, Lit l) -{ - fprintf(f, "%sx%d", l.sign() ? "~" : "", l.var()+1); -} - -static inline void logLits(FILE* f, const vec<Lit>& ls) -{ - fprintf(f, "[ "); - if (ls.size() > 0) { - logLit(f, ls[0]); - for (uint32_t i = 1; i < ls.size(); i++) { - fprintf(f, ", "); - logLit(f, ls[i]); - } - } - fprintf(f, "] "); -} - -#ifndef DEBUG_ATTACH_FULL -inline void Solver::testAllClauseAttach() const -{ - return; -} -inline void Solver::findAllAttach() const -{ - return; -} -#endif //DEBUG_ATTACH_FULL - -inline void Solver::uncheckedEnqueueLight(const Lit p) -{ - assert(value(p.var()) == l_Undef); - #if WATCHED_CACHE_NUM > 0 - __builtin_prefetch(watches.getData() + p.toInt()); - #else - if (watches[p.toInt()].size() > 0) __builtin_prefetch(watches[p.toInt()].getData()); - #endif - - assigns [p.var()] = boolToLBool(!p.sign());//lbool(!sign(p)); // <<== abstract but not uttermost effecient - trail.push(p); - if (decisionLevel() == 0) { - level[p.var()] = 0; - #ifdef ANIMATE3D - fprintf(stderr, "s %u %d\n", p.var(), p.sign()); - #endif - } -} - -inline void Solver::uncheckedEnqueueLight2(const Lit p, const uint32_t binSubLevel, const Lit lev1Ancestor, const bool learntLeadHere) -{ - assert(value(p.var()) == l_Undef); - #if WATCHED_CACHE_NUM > 0 - __builtin_prefetch(watches.getData() + p.toInt()); - #else - if (watches[p.toInt()].size() > 0) __builtin_prefetch(watches[p.toInt()].getData()); - #endif - - assigns [p.var()] = boolToLBool(!p.sign());//lbool(!sign(p)); // <<== abstract but not uttermost effecient - trail.push(p); - binPropData[p.var()].lev = binSubLevel; - binPropData[p.var()].lev1Ancestor = lev1Ancestor; - binPropData[p.var()].learntLeadHere = learntLeadHere; -} - -/** -@brief Enqueues&sets a new fact that has been found - -Call this when a fact has been found. Sets the value, enqueues it for -propagation, sets its level, sets why it was propagated, saves the polarity, -and does some logging if logging is enabled. - -@p p the fact to enqueue -@p from Why was it propagated (binary clause, tertiary clause, normal clause) -*/ -inline void Solver::uncheckedEnqueue(const Lit p, const PropBy& from) -{ - #ifdef DEBUG_UNCHECKEDENQUEUE_LEVEL0 - #ifndef VERBOSE_DEBUG - if (decisionLevel() == 0) - #endif //VERBOSE_DEBUG - - std::cout << "uncheckedEnqueue var " << p.var()+1 - << " to val " << !p.sign() - << " level: " << decisionLevel() - << " sublevel: " << trail.size() - << " by: " << from << std::endl; - - if (from.isClause() && !from.isNULL()) { - std::cout << "by clause: " << *clauseAllocator.getPointer(from.getClause()) << std::endl; - } - #endif //DEBUG_UNCHECKEDENQUEUE_LEVEL0 - - //assert(decisionLevel() == 0 || !subsumer->getVarElimed()[p.var()]); - - const Var v = p.var(); - assert(value(v).isUndef()); - #if WATCHED_CACHE_NUM > 0 - __builtin_prefetch(watches.getData() + p.toInt()); - #else - if (watches[p.toInt()].size() > 0) __builtin_prefetch(watches[p.toInt()].getData()); - #endif - - assigns [v] = boolToLBool(!p.sign()); - #ifdef ANIMATE3D - fprintf(stderr, "s %u %d\n", v, p.sign()); - #endif - level [v] = decisionLevel(); - reason [v] = from; - polarity[v] = p.sign(); - trail.push(p); -} - -} - -#endif //SOLVER_H |