From eeb52fe05d3d8d0c024a192a18e3706a17a85351 Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Mon, 17 Aug 2020 17:08:58 +0100 Subject: [PATCH 1/8] Extend sat_hardnesst struct to keep track of the actual clauses, not just number of clauses Currently, solver hardness tracks number of clauses and not the actual clauses for an instruction. This mapping will help identfy code hotspots based on which of the clauses belong to the SAT core. This commit extends the sat_hardnesst structure to include mapping between clauses and ssa expression. --- src/solvers/solver_hardness.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/solvers/solver_hardness.h b/src/solvers/solver_hardness.h index 2d69600ad02..b78cd9c1857 100644 --- a/src/solvers/solver_hardness.h +++ b/src/solvers/solver_hardness.h @@ -50,6 +50,7 @@ struct solver_hardnesst size_t clauses = 0; size_t literals = 0; std::unordered_set variables = {}; + std::vector> clause_set = {}; sat_hardnesst &operator+=(const sat_hardnesst &other); }; From 2d0c2e995724f40ede479a5ecc881b95273f3785 Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Mon, 17 Aug 2020 17:10:25 +0100 Subject: [PATCH 2/8] Add utility to collect clauses and display the clause set in json output for write-solver-stats-to Clauses are stored as a sorted vector of integers. --- .../solver-hardness-simple/test.desc | 3 +- src/solvers/solver_hardness.cpp | 33 +++++++++++++++++++ 2 files changed, 35 insertions(+), 1 deletion(-) diff --git a/regression/solver-hardness/solver-hardness-simple/test.desc b/regression/solver-hardness/solver-hardness-simple/test.desc index e3542a989f6..7a27a60659e 100644 --- a/regression/solver-hardness/solver-hardness-simple/test.desc +++ b/regression/solver-hardness/solver-hardness-simple/test.desc @@ -5,6 +5,7 @@ main.c ^SIGNAL=0$ ^\[main.assertion.\d+\] line \d+ assertion a \+ b \< 10: FAILURE$ ^VERIFICATION FAILED$ -\"SAT_hardness\":\{(\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+)\} +^Valid JSON File$ +\"SAT_hardness\": \{(\"ClauseSet\": \[.*\]|\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+), (\"ClauseSet\": \[.*\]|\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+), (\"ClauseSet\": \[.*\]|\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+), (\"ClauseSet\": \[.*\]|\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+)\} -- ^warning: ignoring diff --git a/src/solvers/solver_hardness.cpp b/src/solvers/solver_hardness.cpp index 571586b73f7..c831c217f1c 100644 --- a/src/solvers/solver_hardness.cpp +++ b/src/solvers/solver_hardness.cpp @@ -26,6 +26,8 @@ operator+=(const solver_hardnesst::sat_hardnesst &other) clauses += other.clauses; literals += other.literals; variables.insert(other.variables.begin(), other.variables.end()); + clause_set.insert(clause_set.end(), + other.clause_set.begin(), other.clause_set.end()); return *this; } @@ -91,10 +93,20 @@ void solver_hardnesst::register_clause(const bvt &bv) { current_hardness.clauses++; current_hardness.literals += bv.size(); + std::vector clause; + for(const auto &literal : bv) { current_hardness.variables.insert(literal.var_no()); + + int signed_literal = literal.var_no(); + if(literal.sign()) + signed_literal = -signed_literal; + clause.push_back(signed_literal); } + clause.push_back(0); + std::sort(clause.begin(), clause.end()); + current_hardness.clause_set.push_back(clause); } void solver_hardnesst::set_outfile(const std::string &file_name) @@ -151,6 +163,16 @@ void solver_hardnesst::produce_report() sat_hardness_json["Variables"] = json_numbert{std::to_string(hardness.variables.size())}; + json_arrayt sat_hardness_clause_set_json; + for(auto const &clause : hardness.clause_set) + { + json_arrayt clause_json; + for(auto const &lit : clause) + clause_json.push_back(json_numbert{std::to_string(lit)}); + sat_hardness_clause_set_json.push_back(clause_json); + } + sat_hardness_json["ClauseSet"] = sat_hardness_clause_set_json; + hardness_stats_json["SAT_hardness"] = sat_hardness_json; json_stream_array.push_back(hardness_stats_json); @@ -183,6 +205,17 @@ void solver_hardnesst::produce_report() assertion_hardness_json["Variables"] = json_numbert{ std::to_string(assertion_stats.sat_hardness.variables.size())}; + json_arrayt assertion_sat_hardness_clause_set_json; + for(auto const &clause : assertion_stats.sat_hardness.clause_set) + { + json_arrayt clause_json; + for(auto const &lit : clause) + clause_json.push_back(json_numbert{std::to_string(lit)}); + assertion_sat_hardness_clause_set_json.push_back(clause_json); + } + assertion_hardness_json["ClauseSet"] = + assertion_sat_hardness_clause_set_json; + assertion_stats_json["SAT_hardness"] = assertion_hardness_json; json_stream_array.push_back(assertion_stats_json); From 4b9490ba4effe7fefea20b1ce18447683698409c Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Mon, 17 Aug 2020 17:10:25 +0100 Subject: [PATCH 3/8] Add utility to collect clauses and display the clause set in json output for write-solver-stats-to Clauses are stored as a sorted vector of integers. clang format solver_hardness.cpp --- src/solvers/solver_hardness.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/solvers/solver_hardness.cpp b/src/solvers/solver_hardness.cpp index c831c217f1c..11f6afb152a 100644 --- a/src/solvers/solver_hardness.cpp +++ b/src/solvers/solver_hardness.cpp @@ -26,8 +26,8 @@ operator+=(const solver_hardnesst::sat_hardnesst &other) clauses += other.clauses; literals += other.literals; variables.insert(other.variables.begin(), other.variables.end()); - clause_set.insert(clause_set.end(), - other.clause_set.begin(), other.clause_set.end()); + clause_set.insert( + clause_set.end(), other.clause_set.begin(), other.clause_set.end()); return *this; } From 1cb2d40f083e979c9ae7fe692afc79171e1ffe42 Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Wed, 2 Sep 2020 13:38:48 +0100 Subject: [PATCH 4/8] Store clause counter value from satcheck_minisat instead of storing the clause itself --- src/solvers/sat/satcheck_minisat2.cpp | 6 +++-- src/solvers/solver_hardness.cpp | 36 +++++++++++++-------------- src/solvers/solver_hardness.h | 6 +++-- 3 files changed, 26 insertions(+), 22 deletions(-) diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp index 0c2127e6c0d..176b49524cc 100644 --- a/src/solvers/sat/satcheck_minisat2.cpp +++ b/src/solvers/sat/satcheck_minisat2.cpp @@ -140,8 +140,10 @@ void satcheck_minisat2_baset::lcnf(const bvt &bv) solver->addClause_(c); - with_solver_hardness( - [&bv](solver_hardnesst &hardness) { hardness.register_clause(bv); }); + size_t solver_clause_num = clause_counter; + with_solver_hardness([&bv, &solver_clause_num](solver_hardnesst &hardness) { + hardness.register_clause(bv, solver_clause_num); + }); clause_counter++; } catch(const Minisat::OutOfMemoryException &) diff --git a/src/solvers/solver_hardness.cpp b/src/solvers/solver_hardness.cpp index 11f6afb152a..2cb4c88b24a 100644 --- a/src/solvers/solver_hardness.cpp +++ b/src/solvers/solver_hardness.cpp @@ -89,24 +89,28 @@ void solver_hardnesst::register_assertion_ssas( current_hardness = {}; } -void solver_hardnesst::register_clause(const bvt &bv) +void solver_hardnesst::register_clause( + const bvt &bv, + const size_t solver_clause_num) { current_hardness.clauses++; current_hardness.literals += bv.size(); - std::vector clause; for(const auto &literal : bv) { current_hardness.variables.insert(literal.var_no()); - - int signed_literal = literal.var_no(); - if(literal.sign()) - signed_literal = -signed_literal; - clause.push_back(signed_literal); } - clause.push_back(0); - std::sort(clause.begin(), clause.end()); - current_hardness.clause_set.push_back(clause); + +#ifdef DEBUG + std::cout << solver_clause_num << ": "; + for(const auto &literal : bv) + std::cout << literal.dimacs() << " "; + std::cout << "0\n"; +#endif + + current_hardness.clause_set.push_back(solver_clause_num + 1); + std::sort( + current_hardness.clause_set.begin(), current_hardness.clause_set.end()); } void solver_hardnesst::set_outfile(const std::string &file_name) @@ -166,10 +170,8 @@ void solver_hardnesst::produce_report() json_arrayt sat_hardness_clause_set_json; for(auto const &clause : hardness.clause_set) { - json_arrayt clause_json; - for(auto const &lit : clause) - clause_json.push_back(json_numbert{std::to_string(lit)}); - sat_hardness_clause_set_json.push_back(clause_json); + sat_hardness_clause_set_json.push_back( + json_numbert{std::to_string(clause)}); } sat_hardness_json["ClauseSet"] = sat_hardness_clause_set_json; @@ -208,10 +210,8 @@ void solver_hardnesst::produce_report() json_arrayt assertion_sat_hardness_clause_set_json; for(auto const &clause : assertion_stats.sat_hardness.clause_set) { - json_arrayt clause_json; - for(auto const &lit : clause) - clause_json.push_back(json_numbert{std::to_string(lit)}); - assertion_sat_hardness_clause_set_json.push_back(clause_json); + assertion_sat_hardness_clause_set_json.push_back( + json_numbert{std::to_string(clause)}); } assertion_hardness_json["ClauseSet"] = assertion_sat_hardness_clause_set_json; diff --git a/src/solvers/solver_hardness.h b/src/solvers/solver_hardness.h index b78cd9c1857..7dd562c5026 100644 --- a/src/solvers/solver_hardness.h +++ b/src/solvers/solver_hardness.h @@ -50,7 +50,7 @@ struct solver_hardnesst size_t clauses = 0; size_t literals = 0; std::unordered_set variables = {}; - std::vector> clause_set = {}; + std::vector clause_set = {}; sat_hardnesst &operator+=(const sat_hardnesst &other); }; @@ -106,7 +106,9 @@ struct solver_hardnesst /// Called e.g. from the `satcheck_minisat2::lcnf`, this function adds the /// complexity statistics from the last SAT query to the `current_ssa_key`. /// \param bv: the clause (vector of literals) - void register_clause(const bvt &bv); + /// \param solver_clause_num: clause counter value passed from + /// `satcheck_minisat2::lcnf` + void register_clause(const bvt &bv, const size_t solver_clause_num); void set_outfile(const std::string &file_name); From 3c5ab7a737fdbed2c462acf5c515f5f52217a39e Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Wed, 2 Sep 2020 13:38:48 +0100 Subject: [PATCH 5/8] Store clause counter value from satcheck_minisat instead of storing the clause itself Add comment to explain solver_clause_num + 1 in solver hardness, change to --- src/solvers/solver_hardness.cpp | 2 ++ src/solvers/solver_hardness.h | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/solvers/solver_hardness.cpp b/src/solvers/solver_hardness.cpp index 2cb4c88b24a..58102ee9af3 100644 --- a/src/solvers/solver_hardness.cpp +++ b/src/solvers/solver_hardness.cpp @@ -108,6 +108,8 @@ void solver_hardnesst::register_clause( std::cout << "0\n"; #endif + // The clause_counter is incremented after the call to register_clause. + // Here we add 1 to solver_clause_num to incorporate this increment. current_hardness.clause_set.push_back(solver_clause_num + 1); std::sort( current_hardness.clause_set.begin(), current_hardness.clause_set.end()); diff --git a/src/solvers/solver_hardness.h b/src/solvers/solver_hardness.h index 7dd562c5026..6471aa70993 100644 --- a/src/solvers/solver_hardness.h +++ b/src/solvers/solver_hardness.h @@ -50,7 +50,7 @@ struct solver_hardnesst size_t clauses = 0; size_t literals = 0; std::unordered_set variables = {}; - std::vector clause_set = {}; + std::vector clause_set = {}; sat_hardnesst &operator+=(const sat_hardnesst &other); }; From e7a3e5e823b1477387ab7d6a056219db5268bace Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Wed, 2 Sep 2020 13:38:48 +0100 Subject: [PATCH 6/8] Store clause counter value from satcheck_minisat instead of storing the clause itself Add comment to explain solver_clause_num + 1 in solver hardness, change to Remove sorting of clause set keeping performance in mind --- src/solvers/solver_hardness.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/solvers/solver_hardness.cpp b/src/solvers/solver_hardness.cpp index 58102ee9af3..079df73c6ff 100644 --- a/src/solvers/solver_hardness.cpp +++ b/src/solvers/solver_hardness.cpp @@ -111,8 +111,6 @@ void solver_hardnesst::register_clause( // The clause_counter is incremented after the call to register_clause. // Here we add 1 to solver_clause_num to incorporate this increment. current_hardness.clause_set.push_back(solver_clause_num + 1); - std::sort( - current_hardness.clause_set.begin(), current_hardness.clause_set.end()); } void solver_hardnesst::set_outfile(const std::string &file_name) From 3accf8d8b6220bfc81ee1c4bf4460ff497596377 Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Wed, 2 Sep 2020 13:38:48 +0100 Subject: [PATCH 7/8] Store clause counter value from satcheck_minisat instead of storing the clause itself Add comment to explain solver_clause_num + 1 in solver hardness, change to Remove sorting of clause set keeping performance in mind Add additional utility to map program lines to clauses in --dimacs output clang format --- src/solvers/sat/satcheck_minisat2.cpp | 20 ++++++++++++++++---- src/solvers/solver_hardness.cpp | 20 +++++++++++--------- src/solvers/solver_hardness.h | 6 +++++- 3 files changed, 32 insertions(+), 14 deletions(-) diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp index 176b49524cc..d580159d930 100644 --- a/src/solvers/sat/satcheck_minisat2.cpp +++ b/src/solvers/sat/satcheck_minisat2.cpp @@ -140,10 +140,22 @@ void satcheck_minisat2_baset::lcnf(const bvt &bv) solver->addClause_(c); - size_t solver_clause_num = clause_counter; - with_solver_hardness([&bv, &solver_clause_num](solver_hardnesst &hardness) { - hardness.register_clause(bv, solver_clause_num); - }); + // To map clauses to lines of program code, track clause indices in the + // dimacs cnf output. Dimacs output is generated after processing clauses + // to remove duplicates and clauses that are trivially true. Here, a clause + // is checked to see if it can be thus eliminated. If not, add the clause + // index to list of clauses in solver_hardnesst::register_clause(). + static size_t cnf_clause_index = 0; + bvt cnf; + bool clause_removed = process_clause(bv, cnf); + + if(!clause_removed) + cnf_clause_index++; + + with_solver_hardness( + [&bv, &cnf, &clause_removed](solver_hardnesst &hardness) { + hardness.register_clause(bv, cnf, cnf_clause_index, !clause_removed); + }); clause_counter++; } catch(const Minisat::OutOfMemoryException &) diff --git a/src/solvers/solver_hardness.cpp b/src/solvers/solver_hardness.cpp index 079df73c6ff..192fefa223d 100644 --- a/src/solvers/solver_hardness.cpp +++ b/src/solvers/solver_hardness.cpp @@ -91,7 +91,9 @@ void solver_hardnesst::register_assertion_ssas( void solver_hardnesst::register_clause( const bvt &bv, - const size_t solver_clause_num) + const bvt &cnf, + const size_t cnf_clause_index, + bool register_cnf) { current_hardness.clauses++; current_hardness.literals += bv.size(); @@ -101,16 +103,16 @@ void solver_hardnesst::register_clause( current_hardness.variables.insert(literal.var_no()); } + if(register_cnf) + { #ifdef DEBUG - std::cout << solver_clause_num << ": "; - for(const auto &literal : bv) - std::cout << literal.dimacs() << " "; - std::cout << "0\n"; + std::cout << cnf_clause_index << ": "; + for(const auto &literal : cnf) + std::cout << literal.dimacs() << " "; + std::cout << "0\n"; #endif - - // The clause_counter is incremented after the call to register_clause. - // Here we add 1 to solver_clause_num to incorporate this increment. - current_hardness.clause_set.push_back(solver_clause_num + 1); + current_hardness.clause_set.push_back(cnf_clause_index); + } } void solver_hardnesst::set_outfile(const std::string &file_name) diff --git a/src/solvers/solver_hardness.h b/src/solvers/solver_hardness.h index 6471aa70993..25726c3b6dc 100644 --- a/src/solvers/solver_hardness.h +++ b/src/solvers/solver_hardness.h @@ -108,7 +108,11 @@ struct solver_hardnesst /// \param bv: the clause (vector of literals) /// \param solver_clause_num: clause counter value passed from /// `satcheck_minisat2::lcnf` - void register_clause(const bvt &bv, const size_t solver_clause_num); + void register_clause( + const bvt &bv, + const bvt &cnf, + const size_t cnf_clause_index, + bool register_cnf); void set_outfile(const std::string &file_name); From 2cb743fb0fb0e9e592cecb06b9028f2ba55dcef2 Mon Sep 17 00:00:00 2001 From: Natasha Yogananda Jeppu Date: Wed, 2 Sep 2020 13:38:48 +0100 Subject: [PATCH 8/8] Store clause counter value from satcheck_minisat instead of storing the clause itself Add comment to explain solver_clause_num + 1 in solver hardness, change to Remove sorting of clause set keeping performance in mind Add additional utility to map program lines to clauses in --dimacs output clang format --- regression/solver-hardness/solver-hardness-simple/test.desc | 3 +-- src/solvers/solver_hardness.h | 6 ++++-- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/regression/solver-hardness/solver-hardness-simple/test.desc b/regression/solver-hardness/solver-hardness-simple/test.desc index 7a27a60659e..eddc4702a55 100644 --- a/regression/solver-hardness/solver-hardness-simple/test.desc +++ b/regression/solver-hardness/solver-hardness-simple/test.desc @@ -5,7 +5,6 @@ main.c ^SIGNAL=0$ ^\[main.assertion.\d+\] line \d+ assertion a \+ b \< 10: FAILURE$ ^VERIFICATION FAILED$ -^Valid JSON File$ -\"SAT_hardness\": \{(\"ClauseSet\": \[.*\]|\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+), (\"ClauseSet\": \[.*\]|\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+), (\"ClauseSet\": \[.*\]|\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+), (\"ClauseSet\": \[.*\]|\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+)\} +\"SAT_hardness\":\{(\"ClauseSet\":\[.*\]|\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"ClauseSet\":\[.*\]|\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"ClauseSet\":\[.*\]|\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"ClauseSet\":\[.*\]|\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+)\} -- ^warning: ignoring diff --git a/src/solvers/solver_hardness.h b/src/solvers/solver_hardness.h index 25726c3b6dc..facdd736aa9 100644 --- a/src/solvers/solver_hardness.h +++ b/src/solvers/solver_hardness.h @@ -106,8 +106,10 @@ struct solver_hardnesst /// Called e.g. from the `satcheck_minisat2::lcnf`, this function adds the /// complexity statistics from the last SAT query to the `current_ssa_key`. /// \param bv: the clause (vector of literals) - /// \param solver_clause_num: clause counter value passed from - /// `satcheck_minisat2::lcnf` + /// \param cnf: processed clause + /// \param cnf_clause_index: index of clause in dimacs output + /// \param register_cnf: negation of boolean variable tracking if the clause + /// can be eliminated void register_clause( const bvt &bv, const bvt &cnf,