reHC*, be more verbose by default.

yp · Jun 9, 2011 · 13fdf61 · 13fdf61
1 parent e223c11
commit 13fdf61
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 1 deletion.
diff --git a/CMakeOptions.txt b/CMakeOptions.txt
@@ -33,4 +33,17 @@ if (INTEGRATE_SAT_SOLVER)
      OFF
    )
 
+   ## ####################
+   ##
+   ## Specific options for the solvers
+   ##
+   ## ####################
+
+   ## Solver: CryptoMiniSat
+
+   ### Uncomment the following to (try to) lower the memory usage
+   ### (speed will be affected)
+   # add_definitions("-DTRY_LOW_MEMORY_USAGE")
+
+
 endif()
diff --git a/include/cms_sat_solver_interface.hpp b/include/cms_sat_solver_interface.hpp
@@ -64,12 +64,15 @@ class SAT_solver_iface_t
 		:_solver(new Solver()), _solved(false), _sat(false)
   {
 	 SolverConf& conf= _solver->conf;
-	 conf.verbosity= 1;
+	 conf.verbosity= 3;
 	 conf.doFindXors= false;
 	 conf.doFindEqLits= false;
 	 conf.doRegFindEqLits= false;
 	 conf.libraryUsage= true;
 	 conf.restrictPickBranch= 0;
+#ifdef TRY_LOW_MEMORY_USAGE
+	 conf.doSatELite= false;
+#endif
   };
 
   ~SAT_solver_iface_t() {