From 54f145b364df0611a416aaeaa6733f94fe2b090d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 22 Feb 2017 15:11:18 -0800
Subject: [PATCH] initialize

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_local_search.cpp  | 6 +++++-
 src/sat/sat_params.pyg        | 1 +
 src/test/sat_local_search.cpp | 7 ++++++-
 3 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index 84e1355b1..e1fad2740 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -20,6 +20,7 @@
 #include "sat_local_search.h"
 #include "sat_solver.h"
 #include "card_extension.h"
+#include "sat_params.hpp"
 
 namespace sat {
 
@@ -42,6 +43,7 @@ namespace sat {
                 }
             }
 	}
+        set_parameters();
     }
 
     void local_search::reinit() {
@@ -285,6 +287,8 @@ namespace sat {
     }
     
     lbool local_search::operator()() {
+        sat_params params;
+        std::cout << "my parameter value: " << params.cliff() << "\n";
         init();
         bool reach_cutoff_time = false;
         bool reach_known_best_value = false;
@@ -294,7 +298,7 @@ namespace sat {
         srand(0);                       // TBD, use random facility and parameters to set random seed.
         set_parameters();
         // ################## start ######################
-        //cout << "Start initialize and local search, restart in every " << max_steps << " steps" << endl;
+        std::cout << "Start initialize and local search, restart in every " << max_steps << " steps\n";
         for (unsigned tries = 0; ; ++tries) {
             reinit();
             for (int step = 1; step <= max_steps; ++step) {
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index a51e72e25..5e68d2f42 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -27,4 +27,5 @@ def_module_params('sat',
                           ('drat.file', SYMBOL, '', 'file to dump DRAT proofs'),
                           ('drat.check', BOOL, False, 'build up internal proof and check'),
                           ('cardinality.solver', BOOL, False, 'use cardinality/xor solver'),
+                          ('cliff', UINT, 0, 'my favorite parameter'),
                        ))
diff --git a/src/test/sat_local_search.cpp b/src/test/sat_local_search.cpp
index 83c8e7b14..53720d094 100644
--- a/src/test/sat_local_search.cpp
+++ b/src/test/sat_local_search.cpp
@@ -65,7 +65,7 @@ static bool build_instance(char const * filename, sat::solver& s, sat::local_sea
 }
 
 void tst_sat_local_search(char ** argv, int argc, int& i) {
-    if (argc != i + 2) {
+    if (argc < i + 2) {
         std::cout << "require dimacs file name\n";
         return;
     }
@@ -75,6 +75,11 @@ void tst_sat_local_search(char ** argv, int argc, int& i) {
     sat::local_search local_search(solver);
     char const* file_name = argv[i + 1];
     ++i;
+    while (i + 1 < argc) {
+        // set other ad hoc parameters.
+        std::cout << argv[i + 1] << "\n";
+        ++i;
+    }
 
     if (!build_instance(file_name, solver, local_search)) {
         return;