Permalink
Browse files

Simple way to disable extending models.

  • Loading branch information...
1 parent 0c0bb0d commit 1d2e1fc9d1549b56e19a6649c3dafaa1b8131633 @niklasso committed Sep 26, 2011
Showing with 3 additions and 1 deletion.
  1. +2 −1 minisat/simp/SimpSolver.cc
  2. +1 −0 minisat/simp/SimpSolver.h
@@ -51,6 +51,7 @@ SimpSolver::SimpSolver() :
, use_asymm (opt_use_asymm)
, use_rcheck (opt_use_rcheck)
, use_elim (opt_use_elim)
+ , extend_model (true)
, merges (0)
, asymm_lits (0)
, eliminated_vars (0)
@@ -131,7 +132,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
else if (verbosity >= 1)
printf("===============================================================================\n");
- if (result == l_True)
+ if (result == l_True && extend_model)
extendModel();
if (do_simp)
@@ -95,6 +95,7 @@ class SimpSolver : public Solver {
bool use_asymm; // Shrink clauses by asymmetric branching.
bool use_rcheck; // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)
bool use_elim; // Perform variable elimination.
+ bool extend_model; // Flag to indicate whether the user needs to look at the full model.
// Statistics:
//

0 comments on commit 1d2e1fc

Please sign in to comment.