diff --git a/.gitignore b/.gitignore index 96f6e8df..ae36f054 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,6 @@ +*~ +#* + # Prerequisites *.d diff --git a/CMakeLists.txt b/CMakeLists.txt index 01d38281..7d1f8148 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -66,6 +66,8 @@ set(SMT_SWITCH_DIR "${PROJECT_SOURCE_DIR}/deps/smt-switch") # rely on cmake modules from smt-switch (required anyway) set(CMAKE_MODULE_PATH ${SMT_SWITCH_DIR}/cmake) +set(CMAKE_FIND_LIBRARY_SUFFIXES ".a") + find_package(GMP REQUIRED) # Check that dependencies are there @@ -155,6 +157,8 @@ set(SOURCES "${PROJECT_SOURCE_DIR}/engines/kinduction.cpp" "${PROJECT_SOURCE_DIR}/engines/mbic3.cpp" "${PROJECT_SOURCE_DIR}/engines/syguspdr.cpp" + "${PROJECT_SOURCE_DIR}/engines/local_searcher.cpp" + "${PROJECT_SOURCE_DIR}/engines/options_handler.cpp" "${PROJECT_SOURCE_DIR}/frontends/btor2_encoder.cpp" "${PROJECT_SOURCE_DIR}/frontends/smv_encoder.cpp" "${PROJECT_SOURCE_DIR}/frontends/smv_node.cpp" diff --git a/contrib/setup-smt-switch.sh b/contrib/setup-smt-switch.sh index 0fa4c3b8..ea793358 100755 --- a/contrib/setup-smt-switch.sh +++ b/contrib/setup-smt-switch.sh @@ -3,7 +3,7 @@ DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" DEPS=$DIR/../deps -SMT_SWITCH_VERSION=445b5bc5172cc4a56db121e5ba4c7a5e14147bd5 +SMT_SWITCH_VERSION=c9a72faa99dca7b8d3ba16e37 usage () { cat < + #include "bmc.h" + #include "utils/logger.h" using namespace smt; @@ -50,6 +53,71 @@ void Bmc::initialize() solver_->assert_formula(unroller_.at_time(ts_.init(), 0)); } +void Bmc::dump_query_until(int reached_k, int k) +{ + initialize(); + + //NOTE: there is a corner case where an instance is trivially + //unsatisfiable, i.e., safe, when the conjunction of initial state + //predicate and transition (+ any constraints) is already unsat. We + //could also check this using unsat core functionality of solver (if + //supported), and check if bad state predicate is in core + + logger.log(1, "BMC bound_start_: {} ", bound_start_); + logger.log(1, "BMC bound_step_: {} ", bound_step_); + + // Options 'bmc_exponential_step_' results in doubling the bound in every step + const bool exp_step = options_.bmc_exponential_step_; + + for (int i = 0; i <= k; ++i) { + if (i > 0) { + logger.log(2, " BMC adding transition for i-1 = {}", i-1); + solver_->assert_formula(unroller_.at_time(ts_.trans(), i-1)); + if (options_.bmc_neg_init_step_) { + logger.log(2, " BMC adding negated init constraint for step {}", i); + Term not_init = solver_->make_term(PrimOp::Not, unroller_.at_time(ts_.init(), i)); + solver_->assert_formula(not_init); + } + } + + if (i <= reached_k) { + // Optional: add negated bad state predicates to bounds where no cex was found + assert(!options_.bmc_neg_bad_step_); + if (options_.bmc_neg_bad_step_all_) { + Term not_bad; + logger.log(2, " BMC adding negated bad state constraint for i = {}", i); + not_bad = solver_->make_term(PrimOp::Not, unroller_.at_time(bad_, i)); + solver_->assert_formula(not_bad); + } + } + } + + // BMC is guaranteed to find a cex if we make sure to check all bounds (default). + // This behavior can be overridden by 'options_.bmc_single_bad_state_' + const int cex_guarantee = !options_.bmc_single_bad_state_; + + Term clause; + if (cex_guarantee) { + // Make sure we cover *all* states by adding disjunctive bad state predicate + clause = solver_->make_term(false); + for (int j = reached_k + 1; j <= k; j++) { + logger.log(2, " BMC adding bad state constraint for j = {}", j); + clause = solver_->make_term(PrimOp::Or, clause, unroller_.at_time(bad_, j)); + } + } else { + // Add a single bad state predicate (bugs might be missed) + logger.log(2, " BMC adding bad state constraint for k = {}", k); + clause = unroller_.at_time(bad_, k); + } + + solver_->assert_formula(clause); + + std::string filename = options_.working_directory_ + "/step" + std::to_string(k) + + "_reached" + std::to_string(reached_k) + ".smt2"; + logger.log(2, " Dumping full BMC problem for k = {}, {}", k, filename); + solver_->dump_smt2(filename); +} + ProverResult Bmc::check_until(int k) { initialize(); @@ -79,7 +147,7 @@ ProverResult Bmc::check_until(int k) bool Bmc::step(int i) { logger.log(1, "\nBMC checking at bound: {}", i); - + if (i <= reached_k_) { return true; } @@ -118,9 +186,9 @@ bool Bmc::step(int i) logger.log(2, " BMC adding bad state constraint for i = {}", i); clause = unroller_.at_time(bad_, i); } - - solver_->assert_formula(clause); - + + solver_->assert_formula(clause); + Result r = solver_->check_sat(); if (r.is_sat()) { logger.log(1, " BMC check at bound {} satisfiable", i); @@ -198,9 +266,9 @@ int Bmc::bmc_interval_get_cex_ub(const int lb, const int ub) { const Term true_term = solver_->make_term(true); assert(lb <= ub); - + logger.log(2, " BMC get cex upper bound: lower bound = {}, upper bound = {} ", lb, ub); - + int j; for (j = lb; j <= ub; j++) { Term bad_state_at_j = unroller_.at_time(bad_, j); diff --git a/engines/bmc.h b/engines/bmc.h index 6476a6fc..74e09278 100644 --- a/engines/bmc.h +++ b/engines/bmc.h @@ -34,6 +34,7 @@ class Bmc : public Prover void initialize() override; ProverResult check_until(int k) override; + void dump_query_until(int reached_k, int k) override; protected: bool step(int i); @@ -45,6 +46,7 @@ class Bmc : public Prover unsigned int bound_step_; // Used in binary search for cex: number of times we called 'solver->push()' unsigned int bin_search_frames_; + // Get an upper bound on the cex, which is located in interval '[lb,ub]' int bmc_interval_get_cex_ub(const int lb, const int ub); // Add negated bad state predicate for all bounds in interval '[start,end]'. diff --git a/engines/local_searcher.cpp b/engines/local_searcher.cpp new file mode 100644 index 00000000..fc1d40b0 --- /dev/null +++ b/engines/local_searcher.cpp @@ -0,0 +1,209 @@ +#include "engines/local_searcher.h" + +#include "engines/options_handler.h" +#include "utils/logger.h" + +#include "smt-switch/smtlib_reader.h" +#include "smt/available_solvers.h" + +#include +#include +#include + +using namespace smt; + +namespace pono { +LocalSearcher::LocalSearcher(const PonoOptions &opt) + : opt_(opt) +{ + initializeConfig(); +} + +LocalSearcher::~LocalSearcher(){ + for (auto &option : options_) + delete option; + options_.clear(); +} + +void LocalSearcher::initializeConfig() { + OptionsHandler::loadOptions(opt_.config_input_, options_); + + sumOfWeights_ = 0; + for (auto &option : options_) { + currentConfig_[option] = option->default_value_; + if (option->weight_) + sumOfWeights_ += std::pow(WEIGHT_BASE_, option->weight_); + } + + logger.log(2, "Config initialized"); + dumpCurrentConfig(); +} + +void LocalSearcher::localSearch(std::string filename, unsigned iterations) { + logger.log(1, "Optimizing local search for {} iterations (repeat: {})", iterations, opt_.solver_runs_); + double currentCost = evaluateCurrentConfig(filename, 3); + double lastAcceptedCost = currentCost; + acceptCurrentConfig(); + bestConfig_ = currentConfig_; bestIter_ = 0; bestCost_ = currentCost; + initialCost_ = currentCost; + + printStatus(0, currentCost); + + unsigned printEvery = 5; + // MCMC Sampling + for (unsigned iter = 1; iter <= iterations; ++iter) { + proposeConfigUpdate(); + currentCost = evaluateCurrentConfig(filename, opt_.solver_runs_); + if (decideToAcceptCurrentProposal(currentCost, lastAcceptedCost)) { + lastAcceptedCost = currentCost; + acceptCurrentConfig(); + if (currentCost < bestCost_) { + bestConfig_ = currentConfig_; bestIter_ = iter; bestCost_ = currentCost; + } + } + if (iter % printEvery == 0) + printStatus(iter, currentCost); + } +} + +void LocalSearcher::writeBestConfig(std::string filename) { + logger.log(1, "Writing best configuration to {}", filename); + logger.log(1, "\tIteration: {}, initial cost: {}, best cost: {}", + bestIter_, initialCost_, bestCost_); + std::vector options; + for (const auto &option : options_) { + options.push_back(new SolverOption + (option->option_name_, + lastAcceptedConfig_[option], + option->values_, + option->weight_)); + } + OptionsHandler::writeOptions(filename, options); + for (auto &option : options) + delete option; +} + + +void LocalSearcher::proposeConfigUpdate() { + logger.log(2, "Proposing configuration update"); + currentConfig_ = lastAcceptedConfig_; + + // Select an option + int rnd = (int) rand() % sumOfWeights_; + SolverOption *option = nullptr; + for (auto &o : options_) { + if (o->weight_) { + int v = std::pow(WEIGHT_BASE_, o->weight_); + if (rnd < v) { + option = o; + break; + } + rnd -= v; + } + } + + if (option->weight_ == 0) { + logger.log(0, "Cannot select option with zero weights"); + exit(0); + } + + // Select a value + std::string val1 = currentConfig_[option]; + std::string val2 = option->alternative(val1); + currentConfig_[option] = val2; + logger.log(2, "Proposed update for {}: {} -> {} ", + option->option_name_, val1, val2); +} + +double LocalSearcher::evaluateCurrentConfig(std::string filename, unsigned solverRuns) { + logger.log(2, "Evaluating configuration..."); + + std::string configStr = currentConfigtoString(); + if (configToCost_.count(configStr)) { + double score = configToCost_[configStr]; + logger.log(2, "Configuration cached, cost: {}", score); + return score; + } else { + unsigned long long sum = 0; + unsigned long long runtime; + for (unsigned i = 0; i < solverRuns; ++i) { + SmtSolver s = create_solver_for(opt_.smt_solver_, + opt_.engine_, + false, + opt_.ceg_prophecy_arrays_); + + loadConfig(s, currentConfig_); + SmtLibReader reader(s); + auto begin = std::chrono::high_resolution_clock::now(); + reader.parse(opt_.filename_); + + auto end = std::chrono::high_resolution_clock::now(); + + runtime = std::chrono::duration_cast(end-begin).count(); + logger.log(2, "\tAttempt {}: cost {}", i, runtime); + sum += runtime; + } + sum /= solverRuns; + + configToCost_[configStr] = sum; + logger.log(2, "Evaluating configuration - done, cost: {}", sum); + return sum; + } +} +void LocalSearcher::loadConfig(smt::SmtSolver &solver, + const std::unordered_map &config) const { + for (const auto &pair : config) { + solver->set_opt(pair.first->option_name_, pair.second); + } +} + +bool LocalSearcher::decideToAcceptCurrentProposal(double currentCost, + double lastAcceptedCost) const { + double mcmcBeta = 1; + + logger.log(2, "Current cost: {}, last accepted cost: {}", + currentCost, lastAcceptedCost); + if (currentCost < lastAcceptedCost) { + logger.log(2, "\tPobability to accept: {}", 1); + return true; + } else { + // The smaller the difference between the proposed phase pattern and the + // current phase pattern, the more likely to accept the proposal. + double prob = std::exp(- currentCost / lastAcceptedCost * mcmcBeta); + logger.log(2, "\tPobability to accept: {}", prob); + + return ((double)rand() / RAND_MAX) < prob; + } +} + +void LocalSearcher::acceptCurrentConfig() { + lastAcceptedConfig_ = currentConfig_; + logger.log(2, "\tCurrent configuration accepted"); +} + +void LocalSearcher::dumpCurrentConfig() const { + logger.log(0, "Dumping current configuration:"); + for (auto &pair : currentConfig_) { + std::string s; + pair.first->dump(s); + logger.log(0, s); + logger.log(0, " current value: {}", pair.second); + } +} + +std::string LocalSearcher::currentConfigtoString() const { + std::string s = ""; + for (auto &pair : currentConfig_) { + s += pair.second + ","; + } + return s; +} + +void LocalSearcher::printStatus(unsigned iter, + double currentCost) const { + logger.log(1, "---- Iteration: {}, current cost: {}, best cost: {} ----\n", + iter, currentCost, bestCost_); +} + + +} // namespace pono diff --git a/engines/local_searcher.h b/engines/local_searcher.h new file mode 100644 index 00000000..dca8786a --- /dev/null +++ b/engines/local_searcher.h @@ -0,0 +1,56 @@ +#pragma once + +#include "engines/solver_option.h" +#include "options/options.h" + +#include "smt-switch/smt.h" + +#include + +namespace pono { + +class LocalSearcher { + public: + LocalSearcher(const PonoOptions &opt); + ~LocalSearcher(); + void localSearch(std::string filename, unsigned iterations); + void writeBestConfig(std::string filename); + + private: + const PonoOptions &opt_; + + std::vector options_; + std::unordered_map currentConfig_; + std::unordered_map lastAcceptedConfig_; + + std::unordered_map bestConfig_; + unsigned bestIter_ = 0; + double bestCost_ = 0; + + double initialCost_ = 0; + + std::unordered_map configToCost_; + + static const int WEIGHT_BASE_ = 10; + int sumOfWeights_; + + void initializeConfig(); + + void proposeConfigUpdate(); + + double evaluateCurrentConfig(std::string filename, unsigned solverRuns); + void loadConfig(smt::SmtSolver &solver, + const std::unordered_map &config) const; + + bool decideToAcceptCurrentProposal(double currentCost, + double lastAcceptedCost) const; + void acceptCurrentConfig(); + + void dumpCurrentConfig() const; + + std::string currentConfigtoString() const; + + void printStatus(unsigned iter, double currentCost) const; +}; + +} diff --git a/engines/options_handler.cpp b/engines/options_handler.cpp new file mode 100644 index 00000000..0e802914 --- /dev/null +++ b/engines/options_handler.cpp @@ -0,0 +1,79 @@ +#include "engines/solver_option.h" +#include "engines/options_handler.h" +#include "utils/logger.h" + +#include +#include +#include +#include + +using namespace std; + +namespace pono { + + +void OptionsHandler::loadOptions(string filename, + vector &options){ + options.clear(); + + vector> content; + vector row; + string line, word; + fstream file (filename, ios::in); + if(file.is_open()) + { + while(getline(file, line)) + { + row.clear(); + stringstream str(line); + while(getline(str, word, ',')) + row.push_back(word); + content.push_back(row); + } + } + else { + logger.log(0, "Unable to read config file {}", filename); + exit(0); + } + + for(int i=0;i values; + for(int j=3;j &options){ + ofstream myfile (filename); + if (myfile.is_open()) { + for (auto &option : options) { + string s; + option->dump(s); + myfile << s << "\n"; + } + myfile.close(); + } else { + logger.log(0, "Cannot write to {}", filename); + exit(0); + } +} + +void OptionsHandler::printOptions(string filename){ + logger.log(0, "Printing options in {}", filename); + vector options; + loadOptions(filename, options); + for (auto &option : options) { + string s = "\t"; + option->dump(s); + logger.log(0, s); + delete option; + } +} + +} diff --git a/engines/options_handler.h b/engines/options_handler.h new file mode 100644 index 00000000..e4c8a63a --- /dev/null +++ b/engines/options_handler.h @@ -0,0 +1,26 @@ +#pragma once + +#include +#include +#include + + +namespace pono { + +class SolverOption; + +class OptionsHandler +{ + public: + // An option file is a CSV file that represent a solver configuration + // [option name],[default value],[weight],[possible,values,...] + OptionsHandler(); + + static void loadOptions(std::string filename, + std::vector &options); + static void writeOptions(std::string filename, + const std::vector &options); + static void printOptions(std::string filename); +}; + +} // namespace pono diff --git a/engines/prover.h b/engines/prover.h index 62f68415..2a415267 100644 --- a/engines/prover.h +++ b/engines/prover.h @@ -48,6 +48,8 @@ class Prover virtual ProverResult prove(); + virtual void dump_query_until(int reached_k, int k) {}; + virtual ProverResult check_until(int k) = 0; virtual bool witness(std::vector & out); diff --git a/engines/solver_option.h b/engines/solver_option.h new file mode 100644 index 00000000..577a5897 --- /dev/null +++ b/engines/solver_option.h @@ -0,0 +1,63 @@ +#pragma once + +#include "utils/logger.h" + +#include +#include + +namespace pono { + +struct SolverOption +{ + public: + SolverOption(std::string option_name, + std::string default_value, + std::vector values, + unsigned weight = 1) + : option_name_(option_name) + , default_value_(default_value) + , values_(values) + , weight_(weight) + {}; + + const std::string option_name_; + const std::string default_value_; + const std::vector values_; + const unsigned weight_; // How important this option is (1,2,3) + + /* + Alternative option to the given one + */ + std::string alternative(const std::string &value) const { + std::vector values = values_; + for (auto it = values.begin(); it != values.end(); ++it) { + if ((*it) == value) { + values.erase(it); + break; + } + } + + if (values.size() == 0) { + logger.log(0, "Error! No alternative to current option!"); + exit(0); + } else if (values.size() == 1) return *(values.begin()); + else { + unsigned index = (unsigned)rand() % values.size(); + return values[index]; + } + } + + void dump(std::string &s) { + s += option_name_; + s += ","; + s += default_value_; + s += ","; + s += std::to_string(weight_); + for (const auto &value : values_) { + s += ","; + s += value; + } + } +}; + +} // namespace pono diff --git a/options/options.cpp b/options/options.cpp index eac4acf3..13f52f3c 100644 --- a/options/options.cpp +++ b/options/options.cpp @@ -90,7 +90,15 @@ enum optionIndex KIND_NO_IND_CHECK, KIND_NO_IND_CHECK_PROPERTY, KIND_ONE_TIME_BASE_CHECK, - KIND_BOUND_STEP + KIND_BOUND_STEP, + WORKING_DIRECTORY, + REACHED_K, + DUMP, + CONFIG_SEARCH, + CONFIG_INPUT, + CONFIG_OUTPUT, + LOCAL_SEARCH_ITERATIONS, + SOLVER_RUNS, }; struct Arg : public option::Arg @@ -586,6 +594,54 @@ const option::Descriptor usage[] = { " --kind-bound-step \tAmount by which bound (unrolling depth) " "is increased in k-induction (default: 1)" }, + { WORKING_DIRECTORY, + 0, + "", + "working-dir", + Arg::NonEmpty, + " --working-dir \tWorking directory." }, + { REACHED_K, + 0, + "", + "reached-k", + Arg::Numeric, + " --reached-k \tReached K." }, + { DUMP, + 0, + "", + "dump", + Arg::None, + " --dump \tDump the BMC query." }, + { CONFIG_SEARCH, + 0, + "", + "config-search", + Arg::None, + " --config-search \tSearch for best configurations." }, + { CONFIG_INPUT, + 0, + "", + "config-input", + Arg::NonEmpty, + " --config-input \tInput configuration." }, + { CONFIG_OUTPUT, + 0, + "", + "config-output", + Arg::NonEmpty, + " --config-output \tOutput configuration." }, + { LOCAL_SEARCH_ITERATIONS, + 0, + "", + "iter", + Arg::Numeric, + " --iter \tNumber of local search iterations." }, + { SOLVER_RUNS, + 0, + "", + "solver-runs", + Arg::Numeric, + " --solver-runs \tAverage across N solver runs for each config evalution." }, { 0, 0, 0, 0, 0, 0 } }; /*********************************** end Option Handling setup @@ -605,6 +661,12 @@ const std::unordered_set & ic3_variants() { return ic3_variants_set; } const std::string PonoOptions::default_profiling_log_filename_ = ""; +const std::string PonoOptions::default_working_directory_ = "./"; + +const std::string PonoOptions::default_config_input_ = ""; + +const std::string PonoOptions::default_config_output_ = ""; + Engine PonoOptions::to_engine(std::string s) { if (str2engine.find(s) != str2engine.end()) { @@ -771,7 +833,15 @@ ProverResult PonoOptions::parse_and_set_options(int argc, kind_no_ind_check_init_states_ = true; kind_no_ind_check_property_ = true; break; case KIND_NO_IND_CHECK_PROPERTY: kind_no_ind_check_property_ = true; break; case KIND_ONE_TIME_BASE_CHECK: kind_one_time_base_check_ = true; break; - case KIND_BOUND_STEP: kind_bound_step_ = atoi(opt.arg); + case KIND_BOUND_STEP: kind_bound_step_ = atoi(opt.arg); break; + case WORKING_DIRECTORY: working_directory_ = opt.arg; break; + case REACHED_K: reached_k_ = atoi(opt.arg); break; + case DUMP: dump_ = true; break; + case CONFIG_SEARCH: config_search_ = true; break; + case CONFIG_INPUT: config_input_ = opt.arg; break; + case CONFIG_OUTPUT: config_output_ = opt.arg; break; + case LOCAL_SEARCH_ITERATIONS: local_search_iterations_ = atoi(opt.arg); break; + case SOLVER_RUNS: solver_runs_ = atoi(opt.arg); break; if (kind_bound_step_ == 0) throw PonoException("--kind-bound-step must be greater than 0"); break; diff --git a/options/options.h b/options/options.h index 4baaa2db..8ecd6b64 100644 --- a/options/options.h +++ b/options/options.h @@ -149,7 +149,15 @@ class PonoOptions kind_no_ind_check_(default_kind_no_ind_check_), kind_no_ind_check_property_(default_kind_no_ind_check_property_), kind_one_time_base_check_(default_kind_one_time_base_check_), - kind_bound_step_(default_kind_bound_step_) + kind_bound_step_(default_kind_bound_step_), + working_directory_(default_working_directory_), + reached_k_(default_reached_k_), + dump_(default_dump_), + config_search_(default_config_search_), + config_input_(default_config_input_), + config_output_(default_config_output_), + local_search_iterations_(default_local_search_iterations_), + solver_runs_(default_solver_runs_) { } @@ -291,6 +299,22 @@ class PonoOptions // K-induction: amount of steps by which transition relation is unrolled unsigned kind_bound_step_; + // Working directory, where to dump the smt2 files generated during run + std::string working_directory_; + + // Reached K + int reached_k_; + + // Save + bool dump_; + + // Search for configuration + bool config_search_; + std::string config_input_; + std::string config_output_; + unsigned local_search_iterations_; + unsigned solver_runs_; + private: // Default options static const Engine default_engine_ = BMC; @@ -358,6 +382,17 @@ class PonoOptions static const bool default_kind_no_ind_check_property_ = false; static const bool default_kind_one_time_base_check_ = false; static const unsigned default_kind_bound_step_ = 1; + + static const std::string default_working_directory_; + static const int default_reached_k_ = -1; + static const bool default_dump_ = false; + + static const bool default_config_search_ = false; + static const std::string default_config_input_; + static const std::string default_config_output_; + static const unsigned default_local_search_iterations_ = 20; + static const unsigned default_solver_runs_ = 5; + }; // Useful functions for printing etc... diff --git a/pono.cpp b/pono.cpp index 6f456f9e..67ded408 100644 --- a/pono.cpp +++ b/pono.cpp @@ -16,6 +16,7 @@ #include #include +#include #include "assert.h" #ifdef WITH_PROFILING @@ -23,10 +24,12 @@ #endif #include "smt-switch/boolector_factory.h" +#include "smt-switch/smtlib_reader.h" #ifdef WITH_MSAT #include "smt-switch/msat_factory.h" #endif +#include "engines/local_searcher.h" #include "core/fts.h" #include "frontends/btor2_encoder.h" #include "frontends/smv_encoder.h" @@ -146,7 +149,10 @@ ProverResult check_prop(PonoOptions pono_options, } else { - r = prover->check_until(pono_options.bound_); + if (pono_options.dump_) + prover->dump_query_until(pono_options.reached_k_, pono_options.bound_); + else + r = prover->check_until(pono_options.bound_); } if (r == FALSE && pono_options.witness_) { @@ -224,6 +230,17 @@ int main(int argc, char ** argv) // set logger verbosity -- can only be set once logger.set_verbosity(pono_options.verbosity_); + if (pono_options.config_search_){ + logger.log(0, "Optimizing solver configurations for {}", pono_options.filename_); + logger.log(0, "Starting configuration: {}", pono_options.config_input_); + srand(10); + LocalSearcher ls(pono_options); + ls.localSearch(pono_options.filename_, pono_options.local_search_iterations_); + ls.writeBestConfig(pono_options.config_output_); + return 0; + } + + // For profiling: set signal handlers for common signals to abort // program. This is necessary to gracefully stop profiling when, // e.g., an external time limit is enforced to stop the program. diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index 67441962..599a783c 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -67,4 +67,6 @@ pono_add_test(test_pseudo_init_and_prop) pono_add_test(test_promote_inputvars) pono_add_test(test_partial_model) +pono_add_test(test_solver_option) + add_subdirectory(encoders) diff --git a/tests/test_solver_option.cpp b/tests/test_solver_option.cpp new file mode 100644 index 00000000..0a864130 --- /dev/null +++ b/tests/test_solver_option.cpp @@ -0,0 +1,46 @@ +#include "gtest/gtest.h" + +#include +#include + +#include "engines/solver_option.h" + +using namespace pono; + +namespace pono_tests { + +TEST(SO, t1) +{ + SolverOption opt("test_name", "test_val1", {"test_val1", "test_val2"}, 2); + + ASSERT_EQ(opt.option_name_, "test_name"); + ASSERT_EQ(opt.default_value_, "test_val1"); + ASSERT_EQ(opt.values_.size(), 2u); + ASSERT_EQ(opt.weight_, 2); +} + +TEST(SO, t2) +{ + SolverOption opt("test_name", "test_val2", {"test_val1", "test_val2"}); + + ASSERT_EQ(opt.option_name_, "test_name"); + ASSERT_EQ(opt.default_value_, "test_val2"); + ASSERT_EQ(opt.values_.size(), 2u); + ASSERT_EQ(opt.weight_, 1); + + ASSERT_EQ(opt.alternative("test_val1"), "test_val2"); +} + +TEST(SO, t3) +{ + SolverOption opt("test_name", "test_val2", {"test_val1", "test_val2", "test_val3"}); + + ASSERT_EQ(opt.option_name_, "test_name"); + ASSERT_EQ(opt.default_value_, "test_val2"); + ASSERT_EQ(opt.values_.size(), 3u); + ASSERT_EQ(opt.weight_, 1); + + ASSERT_NE(opt.alternative("test_val2"), "test_val1"); +} + +} // namespace pono_tests