From 1e32f1fbb57748138dd7b4cf98f3c6236cf717da Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 2 Mar 2017 13:36:05 -0800
Subject: [PATCH] parameter example

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_config.cpp       | 2 ++
 src/sat/sat_config.h         | 1 +
 src/sat/sat_local_search.cpp | 1 +
 src/sat/sat_params.pyg       | 1 +
 4 files changed, 5 insertions(+)

diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 190e76ef8..5102511e8 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -37,6 +37,7 @@ namespace sat {
         m_psm_glue("psm_glue") {
         m_num_threads = 1;
         m_local_search = false;
+        m_local_search_parameter1 = 0;
         updt_params(p); 
     }
 
@@ -81,6 +82,7 @@ namespace sat {
         m_max_conflicts   = p.max_conflicts();
         m_num_threads     = p.threads();
         m_local_search    = p.local_search();
+        m_local_search_parameter1 = p.local_search_int();
         
         // These parameters are not exposed
         m_simplify_mult1  = _p.get_uint("simplify_mult1", 300);
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index 38805bc90..dd32fc28d 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -59,6 +59,7 @@ namespace sat {
         unsigned           m_max_conflicts;
         unsigned           m_num_threads;
         bool               m_local_search;
+        unsigned           m_local_search_parameter1;
 
         unsigned           m_simplify_mult1;
         double             m_simplify_mult2;
diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index ace89c04d..5c8b7f52f 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -226,6 +226,7 @@ namespace sat {
     local_search::local_search(solver& s) : 
         m_par(0) {
 
+        std::cout << "Parameter1: " << s.m_config.m_local_search_parameter1 << "\n";
         m_vars.reserve(s.num_vars());
 
         // copy units
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index a8fe3295b..d95e5fc30 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -29,4 +29,5 @@ def_module_params('sat',
                           ('cardinality.solver', BOOL, False, 'use cardinality solver'),
 	                  ('xor.solver', BOOL, False, 'use xor solver'),
                           ('local_search', BOOL, False, 'add local search co-processor to find satisfiable solution'),
+                          ('local_search.int', UINT, 0, 'arbitrary integer'),
                        ))