diff options
Diffstat (limited to 'src/prop/cryptominisat/Solver/SolverConf.h')
| -rw-r--r-- | src/prop/cryptominisat/Solver/SolverConf.h | 102 |
1 files changed, 0 insertions, 102 deletions
diff --git a/src/prop/cryptominisat/Solver/SolverConf.h b/src/prop/cryptominisat/Solver/SolverConf.h deleted file mode 100644 index 0edaf3745..000000000 --- a/src/prop/cryptominisat/Solver/SolverConf.h +++ /dev/null @@ -1,102 +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 SOLVERCONF_H -#define SOLVERCONF_H - -#include "SolverTypes.h" -#include "constants.h" - -namespace CMSat { - -class SolverConf -{ - public: - SolverConf(); - - double random_var_freq; ///<The frequency with which the decision heuristic tries to choose a random variable. (default 0.02) NOTE: This is really strange. If the number of variables set is large, then the random chance is in fact _far_ lower than this value. This is because the algorithm tries to set one variable randomly, but if that variable is already set, then it _silently_ fails, and moves on (doing non-random flip)! - double clause_decay; ///<Inverse of the clause activity decay factor. Only applies if using MiniSat-style clause activities (default: 1 / 0.999) - int restart_first; ///<The initial restart limit. (default 100) - double restart_inc; ///<The factor with which the restart limit is multiplied in each restart. (default 1.5) - double learntsize_factor; ///<The intitial limit for learnt clauses is a factor of the original clauses. (default 1 / 3) - double learntsize_inc; ///<The limit for learnt clauses is multiplied with this factor each restart. (default 1.1) - bool expensive_ccmin; ///<Should clause minimisation by Sorensson&Biere be used? (default TRUE) - int polarity_mode; ///<Controls which polarity the decision heuristic chooses. Auto means Jeroslow-Wang (default: polarity_auto) - int verbosity; ///<Verbosity level. 0=silent, 1=some progress report, 2=lots of report, 3 = all report (default 2) - Var restrictPickBranch; ///<Pick variables to branch on preferentally from the highest [0, restrictedPickBranch]. If set to 0, preferentiality is turned off (i.e. picked randomly between [0, all]) - uint32_t simpBurstSConf; - double simpStartMult; - double simpStartMMult; - bool doPerformPreSimp; - double failedLitMultiplier; - - //Optimisations to do - bool doFindXors; ///<Automatically find non-binary xor clauses and convert them to xor clauses - bool doFindEqLits; ///<Automatically find binary xor clauses (i.e. variable equi- and antivalences) - bool doRegFindEqLits; ///<Regularly find binary xor clauses (i.e. variable equi- and antivalences) - bool doReplace; ///<Should var-replacing be performed? If set to FALSE, equi- and antivalent variables will not be replaced with one another. NOTE: This precludes using a lot of the algorithms! - bool doConglXors; ///<Do variable elimination at the XOR-level (xor-ing 2 xor clauses thereby removing a variable) - bool doHeuleProcess; ///<Perform local subsitutuion as per Heule's theis - bool doSchedSimp; ///<Should simplifyProblem() be scheduled regularly? (if set to FALSE, a lot of opmitisations are disabled) - bool doSatELite; ///<Should try to subsume & self-subsuming resolve & variable-eliminate & block-clause eliminate? - bool doXorSubsumption; ///<Should try to subsume & local-subsitute xor clauses - bool doHyperBinRes; ///<Should try carry out hyper-binary resolution - bool doBlockedClause; ///<Should try to remove blocked clauses - bool doVarElim; ///<Perform variable elimination - bool doSubsume1; ///<Perform self-subsuming resolution - bool doClausVivif; ///<Perform asymmetric branching at the beginning of the solving - bool doSortWatched; ///<Sort watchlists according to size&type: binary, tertiary, normal (>3-long), xor clauses - bool doMinimLearntMore; ///<Perform learnt-clause minimisation using watchists' binary and tertiary clauses? ("strong minimization" in PrecoSat) - bool doMinimLMoreRecur; ///<Always perform recursive/transitive on-the-fly self self-subsuming resolution --> an enhancement of "strong minimization" of PrecoSat - bool doFailedLit; ///<Carry out Failed literal probing + doubly propagated literal detection + 2-long xor clause detection during failed literal probing + hyper-binary resoolution - bool doRemUselessBins; ///<Should try to remove useless binary clauses at the beginning of solving? - bool doSubsWBins; - bool doSubsWNonExistBins; ///<Try to do subsumption and self-subsuming resolution with non-existent binary clauses (i.e. binary clauses that don't exist but COULD exists) - bool doRemUselessLBins; ///<Try to remove useless learnt binary clauses - #ifdef ENABLE_UNWIND_GLUE - bool doMaxGlueDel; - #endif //ENABLE_UNWIND_GLUE - bool doPrintAvgBranch; - bool doCacheOTFSSR; - bool doCacheOTFSSRSet; - bool doExtendedSCC; - bool doCalcReach; ///<Calculate reachability, and influence variable decisions with that - bool doBXor; - bool doOTFSubsume; ///On-the-fly subsumption - uint64_t maxConfl; - bool isPlain; ///<We are in 'plain' mode: glues can never be 1 - - //interrupting & dumping - uint32_t maxRestarts; - bool needToDumpLearnts; ///<If set to TRUE, learnt clauses will be dumped to the file speified by "learntsFilename" - bool needToDumpOrig; ///<If set to TRUE, a simplified version of the original clause-set will be dumped to the file speified by "origFilename". The solution to this file should perfectly satisfy the problem - std::string learntsFilename; ///<Dump sorted learnt clauses to this file. Only active if "needToDumpLearnts" is set to TRUE - std::string origFilename; ///<Dump simplified original problem CNF to this file. Only active if "needToDumpOrig" is set to TRUE - uint32_t maxDumpLearntsSize; ///<When dumping the learnt clauses, this is the maximum clause size that should be dumped - bool libraryUsage; ///<Set to true if not used as a library. In fact, this is TRUE by default, and Main.cpp sets it to "FALSE". Disables some simplifications at the beginning of solving (mostly performStepsBeforeSolve() ) - bool greedyUnbound; ///<If set, then variables will be greedily unbounded (set to l_Undef). This is EXPERIMENTAL - #ifdef ENABLE_UNWIND_GLUE - uint32_t maxGlue; ///< Learnt clauses (when doing dynamic restarts) with glue above this value will be removed immediately on backtracking - #endif //ENABLE_UNWIND_GLUE - RestartType fixRestartType; ///<If set, the solver will always choose the given restart strategy instead of automatically trying to guess a strategy. Note that even if set to dynamic_restart, there will be a few restarts made statically after each full restart. - - uint32_t origSeed; -}; - -} - -#endif //SOLVERCONF_H |