diff options
Diffstat (limited to 'src/prop/minisat')
| -rw-r--r-- | src/prop/minisat/minisat.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 464a41d74..e550d5ef2 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -110,7 +110,7 @@ void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theory d_context = context; if( options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL ) { - Notice() << "minisat: Incremental solving is disabled" + Notice() << "minisat: Incremental solving is forced on (to avoid variable elimination)" << " unless using internal decision strategy." << std::endl; } @@ -118,12 +118,13 @@ void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theory d_minisat = new Minisat::SimpSolver(theoryProxy, d_context, options::incrementalSolving() || options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL ); - // Setup the verbosity + // Set up the verbosity d_minisat->verbosity = (options::verbosity() > 0) ? 1 : -1; - // Setup the random decision parameters + // Set up the random decision parameters d_minisat->random_var_freq = options::satRandomFreq(); d_minisat->random_seed = options::satRandomSeed(); + // Give access to all possible options in the sat solver d_minisat->var_decay = options::satVarDecay(); d_minisat->clause_decay = options::satClauseDecay(); |