From 78bda873077dc3cc3476bde58701cd9c96ad8046 Mon Sep 17 00:00:00 2001 From: panhongyang0 Date: Wed, 14 Dec 2022 06:59:25 -0500 Subject: [PATCH] version 2 - logic synthesis commands --- src/commands/balance.hpp | 76 + src/commands/exprsim.hpp | 108 +- src/commands/load.hpp | 126 +- src/commands/lut_mapping.hpp | 166 +- src/commands/node_resynthesis.hpp | 113 ++ src/commands/refactor.hpp | 113 ++ src/commands/resub.hpp | 144 ++ src/commands/sim.hpp | 141 +- src/commands/stpsat.hpp | 300 ++- src/commands/techmap.hpp | 107 +- src/commands/write_dot.hpp | 91 +- src/core/matrix.hpp | 105 +- src/core/misc.cpp | 158 ++ src/core/misc.hpp | 59 + src/core/properties.cpp | 150 +- src/core/properties.hpp | 35 +- src/core/stp_sat.hpp | 2957 +++++++++++++---------------- src/mcnc.genlib | 26 + src/phyLS.cpp | 15 +- 19 files changed, 2661 insertions(+), 2329 deletions(-) create mode 100644 src/commands/balance.hpp create mode 100644 src/commands/node_resynthesis.hpp create mode 100644 src/commands/refactor.hpp create mode 100644 src/commands/resub.hpp create mode 100644 src/core/misc.cpp create mode 100644 src/core/misc.hpp create mode 100644 src/mcnc.genlib diff --git a/src/commands/balance.hpp b/src/commands/balance.hpp new file mode 100644 index 0000000..2888f41 --- /dev/null +++ b/src/commands/balance.hpp @@ -0,0 +1,76 @@ +/* phyLS: powerful heightened yielded Logic Synthesis + * Copyright (C) 2022 */ + +/** + * @file aig_balancing.hpp + * + * @brief transforms the current network into a well-balanced AIG + * + * @author Homyoung + * @since 2022/12/14 + */ + +#ifndef BALANCE_HPP +#define BALANCE_HPP + +#include +#include +#include +#include +#include + +#include "../core/misc.hpp" + +using namespace std; + +namespace alice { + +class balance_command : public command { + public: + explicit balance_command(const environment::ptr& env) + : command(env, + "transforms the current network into a well-balanced AIG") { + add_flag("--strash, -s", "Balance AND finding structural hashing"); + add_flag("--verbose, -v", "print the information"); + } + + protected: + void execute() { + clock_t begin, end; + double totalTime; + + if (store().size() == 0u) + std::cerr << "Error: Empty AIG network\n"; + else { + auto aig = store().current(); + if (is_set("strash")) { + begin = clock(); + aig_balancing_params ps; + ps.minimize_levels = false; + aig_balance(aig, ps); + end = clock(); + totalTime = (double)(end - begin) / CLOCKS_PER_SEC; + } else { + begin = clock(); + aig_balance(aig); + end = clock(); + totalTime = (double)(end - begin) / CLOCKS_PER_SEC; + } + phyLS::print_stats(aig); + + store().extend(); + store().current() = aig; + } + + cout.setf(ios::fixed); + cout << "[CPU time] " << setprecision(2) << totalTime << " s" << endl; + } + + private: +}; + +ALICE_ADD_COMMAND(balance, "Logic synthesis") + +} // namespace alice + +#endif \ No newline at end of file diff --git a/src/commands/exprsim.hpp b/src/commands/exprsim.hpp index ee84cc0..416138d 100644 --- a/src/commands/exprsim.hpp +++ b/src/commands/exprsim.hpp @@ -15,70 +15,62 @@ #include "../store.hpp" -namespace alice -{ +using namespace std; - class exprsim_command: public command - { - public: - explicit exprsim_command( const environment::ptr& env ) - : command( env, "expression simulation, return a truth table" ) - { - add_flag( "--verbose, -v", "print the information" ); - add_option( "-e,--expression", expression, "creates truth table from expression" ); - add_flag( "-n,--new", "adds new store entry" ); - add_option( "-m,--max_num_vars", max_num_vars, "set the maximum number of variables" ); - } +namespace alice { - protected: - void execute() - { - auto& opt_ntks = store(); - - if ( opt_ntks.empty() || is_set( "new" ) ) - { - opt_ntks.extend(); - } +class exprsim_command : public command { + public: + explicit exprsim_command(const environment::ptr& env) + : command(env, "expression simulation, return a truth table") { + add_flag("--verbose, -v", "print the information"); + add_option("-e,--expression", expression, + "creates truth table from expression"); + add_flag("-n,--new", "adds new store entry"); + add_option("-m,--max_num_vars", max_num_vars, + "set the maximum number of variables"); + } - /* find max var */ - uint32_t num_vars{0u}; - - for (auto c : expression) - { - if (c >= 'a' && c <= 'p') - { - num_vars = std::max( num_vars, c - 'a' + 1u ); - } - } + protected: + void execute() { + clock_t begin, end; + double totalTime; + auto& opt_ntks = store(); + begin = clock(); + if (opt_ntks.empty() || is_set("new")) opt_ntks.extend(); + /* find max var */ + uint32_t num_vars{0u}; + for (auto c : expression) { + if (c >= 'a' && c <= 'p') + num_vars = std::max(num_vars, c - 'a' + 1u); + } + if (is_set("max_num_vars")) + num_vars = max_num_vars > num_vars ? max_num_vars : num_vars; + kitty::dynamic_truth_table tt(num_vars); + if (kitty::create_from_expression(tt, expression)) { + optimum_network opt; + opt.function = tt; + opt.network = expression; + opt_ntks.current() = opt; + std::cout << fmt::format("tt: 0x{}", kitty::to_hex(opt.function)) + << std::endl; - if( is_set( "max_num_vars" ) ) - { - num_vars = max_num_vars > num_vars ? max_num_vars : num_vars; - } + store().extend(); + store().current() = opt; + } + end = clock(); + totalTime = (double)(end - begin) / CLOCKS_PER_SEC; + cout.setf(ios::fixed); + cout << "[CPU time] " << setprecision(2) << totalTime << " s" << endl; + } - kitty::dynamic_truth_table tt( num_vars ); + private: + std::string expression = ""; + uint32_t max_num_vars = 0u; +}; - if ( kitty::create_from_expression( tt, expression ) ) - { - optimum_network opt; - opt.function = tt; - opt.network = expression; - opt_ntks.current() = opt; - std::cout << fmt::format( "tt: 0x{}", kitty::to_hex( opt.function ) ) << std::endl; +ALICE_ADD_COMMAND(exprsim, "I/O") - store().extend(); - store().current() = opt; - } - } - - private: - std::string expression = ""; - uint32_t max_num_vars = 0u; - - }; - - ALICE_ADD_COMMAND( exprsim, "I/O" ) - -} +} // namespace alice #endif diff --git a/src/commands/load.hpp b/src/commands/load.hpp index e3ae755..8a9585f 100644 --- a/src/commands/load.hpp +++ b/src/commands/load.hpp @@ -37,79 +37,67 @@ #include "../store.hpp" -namespace alice -{ +namespace alice { - void add_optimum_network_entry(command &cmd, kitty::dynamic_truth_table &function) - { - if (cmd.env->variable("npn") != "") - { - function = std::get<0>(kitty::exact_npn_canonization(function)); - } - - optimum_network entry(function); - - if (!entry.exists()) - { - cmd.store().extend(); - cmd.store().current() = entry; - } +void add_optimum_network_entry(command &cmd, + kitty::dynamic_truth_table &function) { + if (cmd.env->variable("npn") != "") { + function = std::get<0>(kitty::exact_npn_canonization(function)); } - class load_command : public command - { - public: - load_command(const environment::ptr &env) : command(env, "Load new entry") - { - add_option("truth_table,--tt", truth_table, "truth table in hex format"); - add_flag("--binary,-b", "read truth table as binary string"); - add_option("--majn,-m", odd_inputs, "generate majority-of-n truth table "); - } - - protected: - void execute() override - { - auto function = [this]() - { - if (is_set("binary")) - { - const unsigned num_vars = ::log(truth_table.size()) / ::log(2.0); - kitty::dynamic_truth_table function(num_vars); - kitty::create_from_binary_string(function, truth_table); - return function; - } - else if (is_set("majn")) - { - if (!(odd_inputs & 1)) - { - std::cout << " majority-of-n, n must be an odd number\n "; - assert(false); - } - - kitty::dynamic_truth_table maj(odd_inputs); - kitty::create_majority(maj); - std::cout << " MAJ" << odd_inputs << " : " << kitty::to_hex(maj) << std::endl; - return maj; - } - else - { - const unsigned num_vars = ::log(truth_table.size() * 4) / ::log(2.0); - kitty::dynamic_truth_table function(num_vars); - kitty::create_from_hex_string(function, truth_table); - return function; - } - }(); - - add_optimum_network_entry(*this, function); - } - - private: - std::string truth_table; - unsigned odd_inputs; - }; - - ALICE_ADD_COMMAND(load, "I/O"); + optimum_network entry(function); + if (!entry.exists()) { + cmd.store().extend(); + cmd.store().current() = entry; + } } +class load_command : public command { + public: + load_command(const environment::ptr &env) : command(env, "Load new entry") { + add_option("truth_table,--tt", truth_table, "truth table in hex format"); + add_flag("--binary,-b", "read truth table as binary string"); + add_option("--majn,-m", odd_inputs, "generate majority-of-n truth table "); + } + + protected: + void execute() override { + auto function = [this]() { + if (is_set("binary")) { + const unsigned num_vars = ::log(truth_table.size()) / ::log(2.0); + kitty::dynamic_truth_table function(num_vars); + kitty::create_from_binary_string(function, truth_table); + return function; + } else if (is_set("majn")) { + if (!(odd_inputs & 1)) { + std::cout << " majority-of-n, n must be an odd number\n "; + assert(false); + } + + kitty::dynamic_truth_table maj(odd_inputs); + kitty::create_majority(maj); + std::cout << " MAJ" << odd_inputs << " : " << kitty::to_hex(maj) + << std::endl; + return maj; + } else { + const unsigned num_vars = ::log(truth_table.size() * 4) / ::log(2.0); + kitty::dynamic_truth_table function(num_vars); + kitty::create_from_hex_string(function, truth_table); + return function; + } + }(); + + add_optimum_network_entry(*this, function); + } + + private: + std::string truth_table; + unsigned odd_inputs; +}; + +ALICE_ADD_COMMAND(load, "I/O"); + +} // namespace alice + #endif diff --git a/src/commands/lut_mapping.hpp b/src/commands/lut_mapping.hpp index 6d94da6..1aba6bf 100644 --- a/src/commands/lut_mapping.hpp +++ b/src/commands/lut_mapping.hpp @@ -13,95 +13,107 @@ #ifndef LUT_MAPPING_HPP #define LUT_MAPPING_HPP -#include +#include +#include #include +#include +#include +#include +#include +#include +#include -namespace alice -{ +using namespace mockturtle; +using namespace std; - class lut_mapping_command : public command - { - public: - explicit lut_mapping_command(const environment::ptr &env) : command(env, "LUT mapping : using AIG as default") - { - add_option("cut_size, -k", cut_size, "set the cut size from 2 to 8, default = 4"); - add_flag("--verbose, -v", "print the information"); - add_flag("--satlut, -s", "satlut mapping"); - add_flag("--xag, -g", "LUT mapping for XAG"); - add_flag("--mig, -m", "LUT mapping for MIG"); - } +namespace alice { - protected: - void execute() - { - lut_mapping_params ps; +class lut_mapping_command : public command { + public: + explicit lut_mapping_command(const environment::ptr &env) + : command(env, "LUT mapping : using AIG as default") { + add_option("cut_size, -k", cut_size, + "set the cut size from 2 to 8, default = 4"); + add_flag("--verbose, -v", "print the information"); + add_flag("--satlut, -s", "satlut mapping"); + add_flag("--xag, -g", "LUT mapping for XAG"); + add_flag("--mig, -m", "LUT mapping for MIG"); + } - if (is_set("mig")) - { - /* derive some MIG */ - assert(store().size() > 0); - mig_network mig = store().current(); + protected: + void execute() { + clock_t begin, end; + double totalTime; + lut_mapping_params ps; - mapping_view mapped_mig{mig}; + if (is_set("mig")) { + /* derive some MIG */ + assert(store().size() > 0); + begin = clock(); + mig_network mig = store().current(); + + mapping_view mapped_mig{mig}; + ps.cut_enumeration_ps.cut_size = cut_size; + lut_mapping, true>(mapped_mig, ps); + + /* collapse into k-LUT network */ + const auto klut = *collapse_mapped_network(mapped_mig); + end = clock(); + totalTime = (double)(end - begin) / CLOCKS_PER_SEC; + store().extend(); + store().current() = klut; + } else if (is_set("xag")) { + /* derive some XAG */ + assert(store().size() > 0); + begin = clock(); + xag_network xag = store().current(); + + mapping_view mapped_xag{xag}; + ps.cut_enumeration_ps.cut_size = cut_size; + lut_mapping, true>(mapped_xag, ps); + + /* collapse into k-LUT network */ + const auto klut = *collapse_mapped_network(mapped_xag); + end = clock(); + totalTime = (double)(end - begin) / CLOCKS_PER_SEC; + store().extend(); + store().current() = klut; + } else { + if (store().size() == 0) { + assert(false && "Error: Empty AIG network\n"); + } + /* derive some AIG */ + aig_network aig = store().current(); + begin = clock(); + mapping_view mapped_aig{aig}; + + /* LUT mapping */ + if (is_set("satlut")) { + satlut_mapping_params ps; ps.cut_enumeration_ps.cut_size = cut_size; - lut_mapping, true>(mapped_mig, ps); - - /* collapse into k-LUT network */ - const auto klut = *collapse_mapped_network(mapped_mig); - store().extend(); - store().current() = klut; - } - else if (is_set("xag")) - { - /* derive some XAG */ - assert(store().size() > 0); - xag_network xag = store().current(); - - mapping_view mapped_xag{xag}; + satlut_mapping, true>(mapped_aig, ps); + } else { ps.cut_enumeration_ps.cut_size = cut_size; - lut_mapping, true>(mapped_xag, ps); - - /* collapse into k-LUT network */ - const auto klut = *collapse_mapped_network(mapped_xag); - store().extend(); - store().current() = klut; + lut_mapping, true, + cut_enumeration_mf_cut>(mapped_aig, ps); } - else - { - if (store().size() == 0) - { - assert(false && "no AIG in the store"); - } - /* derive some AIG */ - aig_network aig = store().current(); - mapping_view mapped_aig{aig}; - - /* LUT mapping */ - if (is_set("satlut")) - { - satlut_mapping_params ps; - ps.cut_enumeration_ps.cut_size = cut_size; - satlut_mapping, true>(mapped_aig, ps); - } - else - { - ps.cut_enumeration_ps.cut_size = cut_size; - lut_mapping, true, cut_enumeration_mf_cut>(mapped_aig, ps); - } - - /* collapse into k-LUT network */ - const auto klut = *collapse_mapped_network(mapped_aig); - store().extend(); - store().current() = klut; - } + /* collapse into k-LUT network */ + const auto klut = *collapse_mapped_network(mapped_aig); + end = clock(); + totalTime = (double)(end - begin) / CLOCKS_PER_SEC; + store().extend(); + store().current() = klut; } + cout.setf(ios::fixed); + cout << "[CPU time] " << setprecision(2) << totalTime << " s" << endl; + } - private: - unsigned cut_size = 4u; - }; + private: + unsigned cut_size = 4u; +}; - ALICE_ADD_COMMAND(lut_mapping, "Mapping") -} +ALICE_ADD_COMMAND(lut_mapping, "Mapping") +} // namespace alice #endif diff --git a/src/commands/node_resynthesis.hpp b/src/commands/node_resynthesis.hpp new file mode 100644 index 0000000..3ac97e2 --- /dev/null +++ b/src/commands/node_resynthesis.hpp @@ -0,0 +1,113 @@ +/* phyLS: powerful heightened yielded Logic Synthesis + * Copyright (C) 2022 */ + +/** + * @file node_resynthesis.hpp + * + * @brief Node resynthesis + * + * @author Homyoung + * @since 2022/12/14 + */ + +#ifndef NODE_RESYNTHESIS_HPP +#define NODE_RESYNTHESIS_HPP + +#include + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include "../core/misc.hpp" + +using namespace std; +using namespace mockturtle; + +namespace alice { +class resyn_command : public command { + public: + explicit resyn_command(const environment::ptr& env) + : command(env, + "performs technology-independent restructuring : using MIG as default") { + add_flag("--xmg, -x", "Resubstitution for XMG"); + add_flag("--xag, -g", "Resubstitution for XAG"); + add_flag("--direct, -d", "Node resynthesis with direct synthesis"); + add_flag("--verbose, -v", "print the information"); + } + + protected: + void execute() { + clock_t begin, end; + double totalTime; + if (store().size() == 0u) + std::cerr << "Error: Empty k-LUT network\n"; + else { + auto klut = store().current(); + if (is_set("xmg")) { + begin = clock(); + if (is_set("direct")) { + direct_resynthesis xmg_resyn; + const auto xmg = node_resynthesis(klut, xmg_resyn); + store().extend(); + store().current() = cleanup_dangling(xmg); + phyLS::print_stats(xmg); + } else { + xmg_npn_resynthesis resyn; + const auto xmg = node_resynthesis(klut, resyn); + store().extend(); + store().current() = cleanup_dangling(xmg); + phyLS::print_stats(xmg); + } + end = clock(); + totalTime = (double)(end - begin) / CLOCKS_PER_SEC; + } else if (is_set("xag")) { + begin = clock(); + direct_resynthesis xag_resyn; + const auto xag = node_resynthesis(klut, xag_resyn); + store().extend(); + store().current() = cleanup_dangling(xag); + phyLS::print_stats(xag); + end = clock(); + totalTime = (double)(end - begin) / CLOCKS_PER_SEC; + } else { + begin = clock(); + if (is_set("direct")) { + direct_resynthesis mig_resyn; + const auto mig = node_resynthesis(klut, mig_resyn); + store().extend(); + store().current() = cleanup_dangling(mig); + phyLS::print_stats(mig); + } else { + mig_npn_resynthesis resyn; + const auto mig = node_resynthesis(klut, resyn); + store().extend(); + store().current() = cleanup_dangling(mig); + phyLS::print_stats(mig); + } + end = clock(); + totalTime = (double)(end - begin) / CLOCKS_PER_SEC; + } + + cout.setf(ios::fixed); + cout << "[CPU time] " << setprecision(3) << totalTime << " s" << endl; + } + } +}; + +ALICE_ADD_COMMAND(resyn, "Logic synthesis") + +} // namespace alice + +#endif diff --git a/src/commands/refactor.hpp b/src/commands/refactor.hpp new file mode 100644 index 0000000..8369112 --- /dev/null +++ b/src/commands/refactor.hpp @@ -0,0 +1,113 @@ +/* phyLS: powerful heightened yielded Logic Synthesis + * Copyright (C) 2022 */ + +/** + * @file aig_balancing.hpp + * + * @brief performs technology-independent refactoring + * + * @author Homyoung + * @since 2022/12/14 + */ + +#ifndef REFACTOR_HPP +#define REFACTOR_HPP + +#include +#include +#include +#include +#include +#include +#include + +#include "../core/misc.hpp" + +using namespace mockturtle; +using namespace std; + +namespace alice { + +class refactor_command : public command { + public: + explicit refactor_command(const environment::ptr& env) + : command(env, "performs technology-independent refactoring") { + add_flag("--mig, -m", "refactoring for MIG"); + add_flag("--xag, -g", "refactoring for XAG"); + add_flag("--xmg, -x", "refactoring for XMG"); + add_flag("--akers, -a", "Refactoring with Akers synthesis for MIG"); + add_flag("--verbose, -v", "print the information"); + } + + protected: + void execute() { + clock_t begin, end; + double totalTime; + + if (is_set("mig")) { + if (store().size() == 0u) + std::cerr << "Error: Empty MIG network\n"; + else { + auto mig = store().current(); + if (is_set("akers")) { + akers_resynthesis resyn; + refactoring(mig, resyn); + } else { + mig_npn_resynthesis resyn; + refactoring(mig, resyn); + } + mig = cleanup_dangling(mig); + phyLS::print_stats(mig); + store().extend(); + store().current() = mig; + } + } else if (is_set("xag")) { + if (store().size() == 0u) + std::cerr << "Error: Empty XAG network\n"; + else { + auto xag = store().current(); + bidecomposition_resynthesis resyn; + refactoring(xag, resyn); + xag = cleanup_dangling(xag); + phyLS::print_stats(xag); + store().extend(); + store().current() = xag; + } + } else if (is_set("xmg")) { + if (store().size() == 0u) + std::cerr << "Error: Empty XMG network\n"; + else { + auto xmg = store().current(); + xmg_npn_resynthesis resyn; + refactoring(xmg, resyn); + xmg = cleanup_dangling(xmg); + phyLS::print_stats(xmg); + store().extend(); + store().current() = xmg; + } + } else { + if (store().size() == 0u) + std::cerr << "Error: Empty AIG network\n"; + else { + auto aig = store().current(); + direct_resynthesis aig_resyn; + refactoring(aig, aig_resyn); + aig = cleanup_dangling(aig); + phyLS::print_stats(aig); + store().extend(); + store().current() = aig; + } + } + + cout.setf(ios::fixed); + cout << "[CPU time] " << setprecision(2) << totalTime << " s" << endl; + } + + private: +}; + +ALICE_ADD_COMMAND(refactor, "Logic synthesis") + +} // namespace alice + +#endif \ No newline at end of file diff --git a/src/commands/resub.hpp b/src/commands/resub.hpp new file mode 100644 index 0000000..7718a27 --- /dev/null +++ b/src/commands/resub.hpp @@ -0,0 +1,144 @@ +/* phyLS: powerful heightened yielded Logic Synthesis + * Copyright (C) 2022 */ + +/** + * @file resub.hpp + * + * @brief performs technology-independent restructuring + * + * @author Homyoung + * @since 2022/12/14 + */ + +#ifndef RESUB_HPP +#define RESUB_HPP + +#include + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include "../core/misc.hpp" + +using namespace std; + +namespace alice { +class resub_command : public command { + public: + explicit resub_command(const environment::ptr& env) + : command(env, "performs technology-independent restructuring : using AIG as default") { + add_flag("--xmg, -x", "Resubstitution for XMG"); + add_flag("--mig, -m", "Resubstitution for MIG"); + add_flag("--xag, -g", "Resubstitution for XAG"); + add_flag("--simulation, -s", "Simulation-guided resubstitution for AIG"); + add_flag("--verbose, -v", "print the information"); + } + + protected: + void execute() { + clock_t begin, end; + double totalTime; + + if (is_set("xmg")) { + if (store().size() == 0u) + std::cerr << "Error: Empty XMG network\n"; + else { + auto xmg = store().current(); + begin = clock(); + using view_t = depth_view>; + fanout_view fanout_view{xmg}; + view_t resub_view{fanout_view}; + xmg_resubstitution(resub_view); + xmg = cleanup_dangling(xmg); + end = clock(); + totalTime = (double)(end - begin) / CLOCKS_PER_SEC; + phyLS::print_stats(xmg); + store().extend(); + store().current() = xmg; + } + } else if (is_set("mig")) { + if (store().size() == 0u) + std::cerr << "Error: Empty MIG network\n"; + else { + auto mig = store().current(); + begin = clock(); + using view_t = depth_view>; + fanout_view fanout_view{mig}; + view_t resub_view{fanout_view}; + mig_resubstitution(resub_view); + mig = cleanup_dangling(mig); + end = clock(); + totalTime = (double)(end - begin) / CLOCKS_PER_SEC; + phyLS::print_stats(mig); + store().extend(); + store().current() = mig; + } + } else if (is_set("xag")) { + if (store().size() == 0u) + std::cerr << "Error: Empty XAG network\n"; + else { + auto xag = store().current(); + begin = clock(); + resubstitution_params ps; + using view_t = depth_view>; + fanout_view fanout_view{xag}; + view_t resub_view{fanout_view}; + resubstitution_minmc_withDC(resub_view, ps); + xag = cleanup_dangling(xag); + end = clock(); + totalTime = (double)(end - begin) / CLOCKS_PER_SEC; + phyLS::print_stats(xag); + store().extend(); + store().current() = xag; + } + } else { + if (store().size() == 0u) + std::cerr << "Error: Empty AIG network\n"; + else { + auto aig = store().current(); + if (is_set("simulation")) { + begin = clock(); + sim_resubstitution(aig); + aig = cleanup_dangling(aig); + end = clock(); + totalTime = (double)(end - begin) / CLOCKS_PER_SEC; + } else { + begin = clock(); + using view_t = depth_view>; + fanout_view fanout_view{aig}; + view_t resub_view{fanout_view}; + aig_resubstitution(resub_view); + aig = cleanup_dangling(aig); + end = clock(); + totalTime = (double)(end - begin) / CLOCKS_PER_SEC; + } + phyLS::print_stats(aig); + store().extend(); + store().current() = aig; + } + } + + cout.setf(ios::fixed); + cout << "[CPU time] " << setprecision(2) << totalTime << " s" << endl; + } +}; + +ALICE_ADD_COMMAND(resub, "Logic synthesis") + +} // namespace alice + +#endif diff --git a/src/commands/sim.hpp b/src/commands/sim.hpp index 41f864a..2ee1e00 100644 --- a/src/commands/sim.hpp +++ b/src/commands/sim.hpp @@ -15,72 +15,85 @@ #include -namespace alice -{ +using namespace std; - class sim_command : public command - { - public: - explicit sim_command(const environment::ptr &env) : command(env, "logic network simulation") - { - add_flag("-a, --aig_network", " simulate current aig network"); - add_flag("-x, --xmg_network", " simulate current xmg network"); - add_flag("-p, --partial_simulate", " simulate current logic network using partial simulator "); +namespace alice { + +class sim_command : public command { + public: + explicit sim_command(const environment::ptr &env) + : command(env, "logic network simulation") { + add_flag("-a, --aig_network", " simulate current aig network"); + add_flag("-x, --xmg_network", " simulate current xmg network"); + add_flag("-p, --partial_simulate", + " simulate current logic network using partial simulator "); + } + + protected: + void execute() { + clock_t begin, end; + double totalTime; + if (is_set("xmg_network")) { + begin = clock(); + if (is_set("partial_simulate")) { + xmg_network xmg = store().current(); + std::vector pats(xmg.num_pis()); + for (auto i = 0; i < xmg.num_pis(); i++) + pats[i].add_bits(0x12345678, 32); + partial_simulator sim(pats); + unordered_node_map + node_to_value(xmg); + simulate_nodes(xmg, node_to_value, sim); + + xmg.foreach_po([&](auto const &f) { + std::cout << "tt: 0x" + << (xmg.is_complemented(f) ? ~node_to_value[f] + : node_to_value[f]) + ._bits[0] + << std::endl; + }); + } else { + xmg_network xmg = store().current(); + default_simulator sim(xmg.num_pis()); + unordered_node_map + node_to_value(xmg); + simulate_nodes(xmg, node_to_value, sim); + + xmg.foreach_gate([&](auto const &n) { + std::cout << "node " << n << " tt: " << node_to_value[n]._bits[0] + << std::endl; + }); + + xmg.foreach_po([&](auto const &f) { + std::cout << "PO tt: " + << (xmg.is_complemented(f) ? ~node_to_value[f] + : node_to_value[f]) + ._bits[0] + << std::endl; + }); + // const auto tt = simulate( xmg, sim )[0]; + // std::cout << "tt: 0x" << tt._bits[0] << std::endl; + } + end = clock(); + totalTime = (double)(end - begin) / CLOCKS_PER_SEC; + } else if (is_set("aig_network")) { + begin = clock(); + aig_network aig = store().current(); + default_simulator sim(aig.num_pis()); + const auto tt = simulate(aig, sim)[0]; + std::cout << "tt: " << tt._bits[0] << std::endl; + end = clock(); + totalTime = (double)(end - begin) / CLOCKS_PER_SEC; + } else { + std::cout << "At least one store should be specified, see 'sim -h' for " + "help. \n"; } + cout.setf(ios::fixed); + cout << "[CPU time] " << setprecision(2) << totalTime << " s" << endl; + } +}; - protected: - void execute() - { - if (is_set("xmg_network")) - { - if (is_set("partial_simulate")) - { - xmg_network xmg = store().current(); - std::vector pats(xmg.num_pis()); - for (auto i = 0; i < xmg.num_pis(); i++) - { - pats[i].add_bits(0x12345678, 32); - } - partial_simulator sim(pats); - - unordered_node_map node_to_value(xmg); - simulate_nodes(xmg, node_to_value, sim); - - xmg.foreach_po([&](auto const &f) - { std::cout << "tt: 0x" << (xmg.is_complemented(f) ? ~node_to_value[f] : node_to_value[f])._bits[0] << std::endl; }); - } - else - { - xmg_network xmg = store().current(); - default_simulator sim(xmg.num_pis()); - unordered_node_map node_to_value(xmg); - simulate_nodes(xmg, node_to_value, sim); - - xmg.foreach_gate([&](auto const &n) - { std::cout << "node " << n << " tt: " << node_to_value[n]._bits[0] << std::endl; }); - - xmg.foreach_po([&](auto const &f) - { std::cout << "PO tt: " << (xmg.is_complemented(f) ? ~node_to_value[f] : node_to_value[f])._bits[0] << std::endl; }); - - // const auto tt = simulate( xmg, sim )[0]; - // std::cout << "tt: 0x" << tt._bits[0] << std::endl; - } - } - else if (is_set("aig_network")) - { - aig_network aig = store().current(); - default_simulator sim(aig.num_pis()); - const auto tt = simulate(aig, sim)[0]; - std::cout << "tt: " << tt._bits[0] << std::endl; - } - else - { - std::cout << "At least one store should be specified, see 'sim -h' for help. \n"; - } - } - }; - - ALICE_ADD_COMMAND(sim, "Verification") -} +ALICE_ADD_COMMAND(sim, "Verification") +} // namespace alice #endif diff --git a/src/commands/stpsat.hpp b/src/commands/stpsat.hpp index 76869c1..235dd44 100644 --- a/src/commands/stpsat.hpp +++ b/src/commands/stpsat.hpp @@ -13,187 +13,161 @@ #ifndef STPSAT_HPP #define STPSAT_HPP -#include "../core/stp_sat.hpp" #include #include +#include "../core/stp_sat.hpp" + using namespace std; -namespace alice -{ - class sat_command : public command - { - public: - explicit sat_command(const environment::ptr &env) : command(env, " circuit-based SAT solver") - { - add_option("filename, -f", filename, "the input file name (CNF or BENCH)"); - add_option("single_po, -s", strategy, "select PO to solve (only in BENCH file)"); - add_flag("--verbose, -v", "verbose output"); - } +namespace alice { +class sat_command : public command { + public: + explicit sat_command(const environment::ptr &env) + : command(env, " circuit-based SAT solver") { + add_option("filename, -f", filename, "the input file name (CNF or BENCH)"); + add_option("single_po, -s", strategy, + "select PO to solve (only in BENCH file)"); + add_flag("--verbose, -v", "verbose output"); + } - protected: - void execute() - { - in.clear(); - mtx.clear(); - expre.clear(); - tt.clear(); - vec.clear(); + protected: + void execute() { + in.clear(); + mtx.clear(); + expre.clear(); + tt.clear(); + vec.clear(); - string tmp; - string s_cnf = ".cnf"; - string s_bench = ".bench"; - if (filename.find(s_bench) != string::npos) - flag = 1; - else if (filename.find(s_cnf) != string::npos) - flag = 2; - if (flag == 1) - { - ifstream fin_bench(filename); + string tmp; + string s_cnf = ".cnf"; + string s_bench = ".bench"; + if (filename.find(s_bench) != string::npos) + flag = 1; + else if (filename.find(s_cnf) != string::npos) + flag = 2; + if (flag == 1) { + ifstream fin_bench(filename); - if (fin_bench.is_open()) - { - while (getline(fin_bench, tmp)) - in.push_back(tmp); - fin_bench.close(); - po = strategy; - vector &it = in; - vector> &mtxvec = mtx; - int &po_tmp = po; - stopwatch<>::duration time{0}; - if (po < 0) - { - call_with_stopwatch(time, [&]() - { phyLS::cdccl_for_all(it, mtxvec); }); - if (it.size() == 0) - cout << "UNSAT" << endl; - else - cout << "SAT" << endl; - if (is_set("verbose")) - { - int count = 0; - cout << "SAT Result : " << endl; - for (string i : it) - { - cout << i << " "; - count += 1; - if (count == 10) - { - cout << endl; - count = 0; - } - } - cout << endl - << "Numbers of SAT Result : " << it.size() << endl; - } - } - else - { - call_with_stopwatch(time, [&]() - { phyLS::cdccl_for_single_po(it, mtxvec, po_tmp); }); - if (it.size() == 0) - cout << "UNSAT" << endl; - else - cout << "SAT" << endl; - if (is_set("verbose")) - { - int count = 0; - cout << " SAT Result of " - << "PO" << po << " : " << endl; - for (string i : it) - { - cout << i << " "; - count += 1; - if (count == 10) - { - cout << endl; - count = 0; - } - } - cout << endl - << "Numbers of SAT Result : " << it.size() << endl; - } - } - cout << fmt::format("[CPU time]: {:5.4f} seconds\n", to_seconds(time)); - } - else - { - cerr << "Cannot open input file" << endl; - } - } - else if (flag == 2) - { - ifstream fin_cnf(filename); - - stringstream buffer; - buffer << fin_cnf.rdbuf(); - string str(buffer.str()); - string expression; - vector expre; - for (int i = 6; i < (str.size() - 1); i++) - { - expression += str[i]; - if ((str[i] == ' ') || (str[i] == '\n')) - { - expression.pop_back(); - int intstr = atoi(expression.c_str()); - expre.push_back(intstr); - expression.clear(); - } - } - - fin_cnf.close(); - - vector &exp = expre; - vector &t = tt; - vector &mtxvec = vec; + if (fin_bench.is_open()) { + while (getline(fin_bench, tmp)) in.push_back(tmp); + fin_bench.close(); + po = strategy; + vector &it = in; + vector> &mtxvec = mtx; + int &po_tmp = po; stopwatch<>::duration time{0}; - - call_with_stopwatch(time, [&]() - { phyLS::stp_cnf(exp, t, mtxvec); }); - - if (t.size() == 0) - cout << "UNSAT" << endl; - else - cout << "SAT" << endl; - if (is_set("verbose")) - { - int count = 0; - cout << "SAT Result : " << endl; - for (string i : t) - { - cout << i << " "; - count += 1; - if (count == 10) - { - cout << endl; - count = 0; + if (po < 0) { + call_with_stopwatch(time, + [&]() { phyLS::cdccl_for_all(it, mtxvec); }); + if (it.size() == 0) + cout << "UNSAT" << endl; + else + cout << "SAT" << endl; + if (is_set("verbose")) { + int count = 0; + cout << "SAT Result : " << endl; + for (string i : it) { + cout << i << " "; + count += 1; + if (count == 10) { + cout << endl; + count = 0; + } } + cout << endl << "Numbers of SAT Result : " << it.size() << endl; + } + } else { + call_with_stopwatch( + time, [&]() { phyLS::cdccl_for_single_po(it, mtxvec, po_tmp); }); + if (it.size() == 0) + cout << "UNSAT" << endl; + else + cout << "SAT" << endl; + if (is_set("verbose")) { + int count = 0; + cout << " SAT Result of " + << "PO" << po << " : " << endl; + for (string i : it) { + cout << i << " "; + count += 1; + if (count == 10) { + cout << endl; + count = 0; + } + } + cout << endl << "Numbers of SAT Result : " << it.size() << endl; } - cout << endl - << "Numbers of SAT Result : " << t.size() << endl; } - cout << fmt::format("[CPU time]: {:5.4f} seconds\n", to_seconds(time)); + } else { + cerr << "Cannot open input file" << endl; } + } else if (flag == 2) { + ifstream fin_cnf(filename); + + stringstream buffer; + buffer << fin_cnf.rdbuf(); + string str(buffer.str()); + string expression; + vector expre; + for (int i = 6; i < (str.size() - 1); i++) { + expression += str[i]; + if ((str[i] == ' ') || (str[i] == '\n')) { + expression.pop_back(); + int intstr = atoi(expression.c_str()); + expre.push_back(intstr); + expression.clear(); + } + } + + fin_cnf.close(); + + vector &exp = expre; + vector &t = tt; + vector &mtxvec = vec; + stopwatch<>::duration time{0}; + + call_with_stopwatch(time, [&]() { phyLS::stp_cnf(exp, t, mtxvec); }); + + if (t.size() == 0) + cout << "UNSAT" << endl; + else + cout << "SAT" << endl; + if (is_set("verbose")) { + int count = 0; + cout << "SAT Result : " << endl; + for (string i : t) { + cout << i << " "; + count += 1; + if (count == 10) { + cout << endl; + count = 0; + } + } + cout << endl << "Numbers of SAT Result : " << t.size() << endl; + } + + cout << fmt::format("[CPU time]: {:5.4f} seconds\n", to_seconds(time)); } + } - private: - string filename; - string cnf; - int strategy = -1; - int po; - int flag = 0; + private: + string filename; + string cnf; + int strategy = -1; + int po; + int flag = 0; - vector in; - vector> mtx; + vector in; + vector> mtx; - vector expre; - vector tt; - vector vec; - }; + vector expre; + vector tt; + vector vec; +}; - ALICE_ADD_COMMAND(sat, "Verification") -} // namespace alice +ALICE_ADD_COMMAND(sat, "Verification") +} // namespace alice #endif diff --git a/src/commands/techmap.hpp b/src/commands/techmap.hpp index 5435fd1..2e13a8b 100644 --- a/src/commands/techmap.hpp +++ b/src/commands/techmap.hpp @@ -1,36 +1,35 @@ /* phyLS: powerful heightened yielded Logic Synthesis * Copyright (C) 2022 */ -/** - * @file techmap.hpp - * - * @brief Standard cell mapping - * - * @author Homyoung - * @since 2022/12/14 - */ + /** + * @file techmap.hpp + * + * @brief Standard cell mapping + * + * @author Homyoung + * @since 2022/12/14 + */ #ifndef TECHMAP_HPP #define TECHMAP_HPP #include -#include #include #include -#include #include +#include #include #include +#include + #include "../core/properties.hpp" -namespace alice -{ +namespace alice { - class tech_mapping_command : public command - { + class tech_mapping_command: public command { public: - explicit tech_mapping_command(const environment::ptr &env) : command(env, "Standard cell mapping : using AIG as default") - { + explicit tech_mapping_command(const environment::ptr& env) + : command(env, "Standard cell mapping : using AIG as default") { add_flag("--xmg, -x", "Standard cell mapping for XMG"); add_flag("--mig, -m", "Standard cell mapping for MIG"); add_flag("--lut, -l", "Standard cell mapping for k-LUT"); @@ -38,32 +37,27 @@ namespace alice add_flag("--verbose, -v", "print the information"); } - rules validity_rules() const - { - return {has_store_element>(env)}; + rules validity_rules() const { + return { has_store_element>(env) }; } private: std::string filename = "techmap.v"; protected: - void execute() - { + void execute() { /* derive genlib */ - std::vector gates = store>().current(); + std::vector gates = + store>().current(); mockturtle::tech_library<5> lib(gates); mockturtle::map_params ps; mockturtle::map_stats st; - if (is_set("xmg")) - { + if (is_set("xmg")) { if (store().size() == 0u) - { std::cerr << "[e] no XMG in the store\n"; - } - else - { + else { auto xmg = store().current(); xmg_gate_stats stats; xmg_profile_gates(xmg, stats); @@ -77,72 +71,67 @@ namespace alice auto res = mockturtle::map(xmg, lib, ps, &st); - if (is_set("output")) - { + if (is_set("output")) { write_verilog_with_binding(res, filename); } - std::cout << fmt::format("[i] Mapped XMG into #gates = {} area = {:.2f} delay = {:.2f}\n", res.num_gates(), st.area, st.delay); + std::cout << fmt::format( + "[i] Mapped XMG into #gates = {} area = {:.2f} delay = {:.2f}\n", + res.num_gates(), st.area, st.delay); } } - else if (is_set("mig")) - { - if (store().size() == 0u) - { + else if (is_set("mig")) { + if (store().size() == 0u) { std::cerr << "[e] no MIG in the store\n"; } - else - { + else { auto mig = store().current(); auto res = mockturtle::map(mig, lib, ps, &st); - if (is_set("output")) - { + if (is_set("output")) { write_verilog_with_binding(res, filename); } - std::cout << fmt::format("Mapped MIG into #gates = {} area = {:.2f} delay = {:.2f}\n", res.num_gates(), st.area, st.delay); + std::cout << fmt::format( + "Mapped MIG into #gates = {} area = {:.2f} delay = {:.2f}\n", + res.num_gates(), st.area, st.delay); } } - else if (is_set("lut")) - { - if (store().size() == 0u) - { + else if (is_set("lut")) { + if (store().size() == 0u) { std::cerr << "[e] no k-LUT in the store\n"; } - else - { + else { auto lut = store().current(); auto res = mockturtle::map(lut, lib, ps, &st); - if (is_set("output")) - { + if (is_set("output")) { write_verilog_with_binding(res, filename); } - std::cout << fmt::format("Mapped k-LUT into #gates = {} area = {:.2f} delay = {:.2f}\n", res.num_gates(), st.area, st.delay); + std::cout << fmt::format( + "Mapped k-LUT into #gates = {} area = {:.2f} delay = {:.2f}\n", + res.num_gates(), st.area, st.delay); } } - else - { - if (store().size() == 0u) - { + else { + if (store().size() == 0u) { std::cerr << "[e] no AIG in the store\n"; } - else - { + else { auto aig = store().current(); auto res = mockturtle::map(aig, lib, ps, &st); - if (is_set("output")) - { + if (is_set("output")) { write_verilog_with_binding(res, filename); } - std::cout << fmt::format("Mapped AIG into #gates = {} area = {:.2f} delay = {:.2f}\n", res.num_gates(), st.area, st.delay); + std::cout << fmt::format( + "Mapped AIG into #gates = {} area = {:.2f} delay = {:.2f}\n", + res.num_gates(), st.area, st.delay); } } } @@ -150,6 +139,6 @@ namespace alice ALICE_ADD_COMMAND(tech_mapping, "Mapping") -} +} // namespace alice #endif diff --git a/src/commands/write_dot.hpp b/src/commands/write_dot.hpp index 871c9f9..46bccd8 100644 --- a/src/commands/write_dot.hpp +++ b/src/commands/write_dot.hpp @@ -13,63 +13,52 @@ #ifndef WRITE_DOT_HPP #define WRITE_DOT_HPP -#include #include +#include -namespace alice -{ +namespace alice { - class write_dot_command : public command - { - public: - explicit write_dot_command(const environment::ptr &env) : command(env, "write dot file") - { - add_flag("--xmg_network,-x", "write xmg_network into dot files"); - add_flag("--aig_network,-a", "write aig_network into dot files"); - add_flag("--mig_network,-m", "write mig_network into dot files"); - add_flag("--klut_network,-l", "write klut_network into dot files"); - add_option("--filename, -f", filename, "The path to store dot file, default: /tmp/test.dot"); +class write_dot_command : public command { + public: + explicit write_dot_command(const environment::ptr &env) + : command(env, "write dot file") { + add_flag("--xmg_network,-x", "write xmg_network into dot files"); + add_flag("--aig_network,-a", "write aig_network into dot files"); + add_flag("--mig_network,-m", "write mig_network into dot files"); + add_flag("--klut_network,-l", "write klut_network into dot files"); + add_option("--filename, -f", filename, + "The path to store dot file, default: /tmp/test.dot"); + } + + protected: + void execute() { + if (is_set("xmg_network")) { + xmg_network xmg = store().current(); + + write_dot(xmg, filename, gate_dot_drawer{}); + } else if (is_set("aig_network")) { + aig_network aig = store().current(); + + write_dot(aig, filename, gate_dot_drawer{}); + } else if (is_set("mig_network")) { + mig_network mig = store().current(); + + write_dot(mig, filename, gate_dot_drawer{}); + } else if (is_set("klut_network")) { + klut_network klut = store().current(); + + write_dot(klut, filename, gate_dot_drawer{}); + } else { + assert(false && " at least one store should be specified "); } + } - protected: - void execute() - { - if (is_set("xmg_network")) - { - xmg_network xmg = store().current(); + private: + std::string filename = "/tmp/test.dot"; +}; - write_dot(xmg, filename, gate_dot_drawer{}); - } - else if (is_set("aig_network")) - { - aig_network aig = store().current(); +ALICE_ADD_COMMAND(write_dot, "I/O") - write_dot(aig, filename, gate_dot_drawer{}); - } - else if (is_set("mig_network")) - { - mig_network mig = store().current(); - - write_dot(mig, filename, gate_dot_drawer{}); - } - else if (is_set("klut_network")) - { - klut_network klut = store().current(); - - write_dot(klut, filename, gate_dot_drawer{}); - } - else - { - assert(false && " at least one store should be specified "); - } - } - - private: - std::string filename = "/tmp/test.dot"; - }; - - ALICE_ADD_COMMAND(write_dot, "I/O") - -} +} // namespace alice #endif diff --git a/src/core/matrix.hpp b/src/core/matrix.hpp index 9d05a5a..884d747 100644 --- a/src/core/matrix.hpp +++ b/src/core/matrix.hpp @@ -10,14 +10,10 @@ using namespace std; -class MatrixXi -{ - friend ostream &operator<<(ostream &os, const MatrixXi &m) - { - for (size_t i = 0; i < m.row; i++) - { - for (size_t j = 0; j < m.col; j++) - { +class MatrixXi { + friend ostream &operator<<(ostream &os, const MatrixXi &m) { + for (size_t i = 0; i < m.row; i++) { + for (size_t j = 0; j < m.col; j++) { os << m.data[i][j] << " "; } os << endl; @@ -25,60 +21,49 @@ class MatrixXi return os; } - friend istream &operator>>(istream &is, MatrixXi &m) - { - for (size_t i = 0; i < m.row; i++) - { - for (size_t j = 0; j < m.col; j++) - { + friend istream &operator>>(istream &is, MatrixXi &m) { + for (size_t i = 0; i < m.row; i++) { + for (size_t j = 0; j < m.col; j++) { is >> m.data[i][j]; } } return is; } -public: + public: typedef int value_type; typedef vector::size_type size_type; - MatrixXi() - { + MatrixXi() { row = 0; col = 0; data.clear(); } - MatrixXi(size_t i, size_t j) - { + MatrixXi(size_t i, size_t j) { row = i; col = j; vector> vdata(row, vector(col, 0)); data = move(vdata); } - MatrixXi(const MatrixXi &m) - { + MatrixXi(const MatrixXi &m) { row = m.row; col = m.col; data = m.data; } - MatrixXi &operator=(const MatrixXi &m) - { + MatrixXi &operator=(const MatrixXi &m) { row = m.row; col = m.col; data = m.data; return *this; } - static MatrixXi product(MatrixXi &m, MatrixXi &n) - { + static MatrixXi product(MatrixXi &m, MatrixXi &n) { MatrixXi t(m.row, n.col); - for (size_t i = 0; i < m.row; i++) - { - for (size_t j = 0; j < n.col; j++) - { - for (size_t k = 0; k < m.col; k++) - { + for (size_t i = 0; i < m.row; i++) { + for (size_t j = 0; j < n.col; j++) { + for (size_t k = 0; k < m.col; k++) { t.data[i][j] += (m.data[i][k] * n.data[k][j]); } } @@ -86,19 +71,13 @@ public: return t; } - static MatrixXi eye(size_t n) - { + static MatrixXi eye(size_t n) { MatrixXi A(n, n); - for (size_t i = 0; i < n; i++) - { - for (size_t j = 0; j < n; j++) - { - if (i == j) - { + for (size_t i = 0; i < n; i++) { + for (size_t j = 0; j < n; j++) { + if (i == j) { A.data[i][j] = 1; - } - else - { + } else { A.data[i][j] = 0; } } @@ -106,57 +85,37 @@ public: return A; } - static MatrixXi kron(const MatrixXi &m, const MatrixXi &n) - { + static MatrixXi kron(const MatrixXi &m, const MatrixXi &n) { size_t a = m.row; size_t b = m.col; size_t c = n.row; size_t d = n.col; MatrixXi t(a * c, b * d); - for (size_t i = 0; i < a * c; i++) - { - for (size_t j = 0; j < b * d; j++) - { + for (size_t i = 0; i < a * c; i++) { + for (size_t j = 0; j < b * d; j++) { t.data[i][j] = m.data[i / c][j / d] * n.data[i % c][j % d]; } } return t; } - ~MatrixXi() - { - data.clear(); - } + ~MatrixXi() { data.clear(); } - int &operator()(size_t i, size_t j) - { - return data[i][j]; - } - const int &operator()(size_t i, size_t j) const - { - return data[i][j]; - } - size_t rows() const - { - return row; - } - size_t cols() const - { - return col; - } + int &operator()(size_t i, size_t j) { return data[i][j]; } + const int &operator()(size_t i, size_t j) const { return data[i][j]; } + size_t rows() const { return row; } + size_t cols() const { return col; } - void resize(size_t nr, size_t nc) - { + void resize(size_t nr, size_t nc) { data.resize(nr); - for (size_t i = 0; i < nr; i++) - { + for (size_t i = 0; i < nr; i++) { data[i].resize(nc); } col = nc; row = nr; } -private: + private: size_t row; size_t col; vector> data; diff --git a/src/core/misc.cpp b/src/core/misc.cpp new file mode 100644 index 0000000..f0f8557 --- /dev/null +++ b/src/core/misc.cpp @@ -0,0 +1,158 @@ +#include +#include +#include +#include + +#include "misc.hpp" + +using namespace percy; +using namespace mockturtle; + +namespace phyLS +{ + std::vector split_by_delim(const std::string& s, char delim) + { + std::vector elems; + split_by_delim(s, delim, std::back_inserter(elems)); + return elems; + } + + template + inline bool next_combination(const Iterator first, Iterator k, const Iterator last) + { + /* Credits: Thomas Draper */ + if ((first == last) || (first == k) || (last == k)) + return false; + Iterator itr1 = first; + Iterator itr2 = last; + ++itr1; + if (last == itr1) + return false; + itr1 = last; + --itr1; + itr1 = k; + --itr2; + while (first != itr1) + { + if (*--itr1 < *itr2) + { + Iterator j = k; + while (!(*itr1 < *j)) ++j; + std::iter_swap(itr1, j); + ++itr1; + ++j; + itr2 = k; + std::rotate(itr1, j, last); + while (last != j) + { + ++j; + ++itr2; + } + std::rotate(k, itr2, last); + return true; + } + } + std::rotate(first, k, last); + return false; + } + + std::vector> get_all_combination_index(std::vector& vars, + const unsigned& n, + const unsigned& k) + { + std::vector> index; + std::vector tmp; + + do + { + tmp.clear(); + for (unsigned i = 0; i < k; ++i) + { + tmp.push_back(vars[i]); + } + index.push_back(tmp); + } while (next_combination(vars.begin(), vars.begin() + k, vars.end())); + + return index; + } + + std::vector> get_all_permutation(const std::vector& vars) + { + std::vector> v; + auto vec_copy = vars; + + std::sort(vec_copy.begin(), vec_copy.end()); + + do + { + v.push_back(vec_copy); + } while (std::next_permutation(vec_copy.begin(), vec_copy.end())); + + return v; + } + + void print_sat_clause(solver_wrapper* solver, pabc::lit* begin, pabc::lit* end) + { + printf("Add clause: "); + pabc::lit* i; + for (i = begin; i < end; i++) + printf("%s%d ", (*i) & 1 ? "!" : "", (*i) >> 1); + printf("\n"); + } + + int add_print_clause(std::vector>& clauses, pabc::lit* begin, pabc::lit* end) + { + std::vector clause; + while (begin != end) { + clause.push_back(*begin); + begin++; + } + clauses.push_back(clause); + + return 1; + } + + std::vector split(const std::string& s, char delimiter) + { + std::vector tokens; + std::string token; + std::istringstream tokenStream(s); + while (std::getline(tokenStream, token, delimiter)) + { + tokens.push_back(token); + std::cout << token << std::endl; + } + return tokens; + } + + std::vector split(const std::string& str, const std::string& sep) + { + std::vector result; + + size_t last = 0; + size_t next = 0; + while ((next = str.find(sep, last)) != std::string::npos) + { + result.push_back(str.substr(last, next - last)); + last = next + 1; + } + result.push_back(str.substr(last)); + + return result; + } + + void to_dimacs(FILE* f, solver_wrapper* solver, std::vector>& clauses) + { + fprintf(f, "p cnf %d %d\n", solver->nr_vars(), clauses.size()); + for (const auto& clause : clauses) { + for (const auto lit : clause) { + // NOTE: variable 0 does not exist in DIMACS format + const auto var = pabc::Abc_Lit2Var(lit) + 1; + const auto is_c = pabc::Abc_LitIsCompl(lit); + fprintf(f, "%d ", is_c ? -var : var); + } + fprintf(f, "0\n"); + } + } + +} \ No newline at end of file diff --git a/src/core/misc.hpp b/src/core/misc.hpp new file mode 100644 index 0000000..1db9960 --- /dev/null +++ b/src/core/misc.hpp @@ -0,0 +1,59 @@ +#pragma once + +#include +#include + +using namespace percy; +using namespace mockturtle; + +namespace phyLS +{ + template + void split_by_delim(const std::string& s, char delim, Out result) + { + std::stringstream ss(s); + std::string item; + while (std::getline(ss, item, delim)) { + *(result++) = item; + } + } + + std::vector split_by_delim(const std::string& s, char delim); + + template + inline bool next_combination(const Iterator first, Iterator k, const Iterator last); + + std::vector> get_all_combination_index(std::vector& vars, + const unsigned& n, + const unsigned& k); + + std::vector> get_all_permutation(const std::vector& vars); + + template + void show_array(const std::vector& array) + { + std::cout << "Elements: "; + for (const auto& x : array) + { + std::cout << " " << x; + } + std::cout << std::endl; + } + + void print_sat_clause(solver_wrapper* solver, pabc::lit* begin, pabc::lit* end); + int add_print_clause(std::vector>& clauses, pabc::lit* begin, pabc::lit* end); + std::vector split(const std::string& s, char delimiter); + + std::vector split(const std::string& str, const std::string& sep); + void to_dimacs(FILE* f, solver_wrapper* solver, std::vector>& clauses); + + template + void print_stats(const Ntk& ntk) + { + //auto copy = ntk; + //depth_view depth_ntk{ ntk }; + using depth_ntk = depth_view; + std::cout << fmt::format("ntk i/o = {}/{} gates = {} level = {}\n", ntk.num_pis(), ntk.num_pos(), ntk.num_gates(), depth_ntk{ ntk }.depth()); + } +} + diff --git a/src/core/properties.cpp b/src/core/properties.cpp index 14005df..e97415c 100644 --- a/src/core/properties.cpp +++ b/src/core/properties.cpp @@ -3,95 +3,77 @@ #include "properties.hpp" +namespace phyLS { +std::vector split_xmg_critical_path(xmg_network const& xmg) { + uint32_t xor3{0}, xor2{0}, maj{0}, and_or{0}; + depth_view dxmg{xmg}; -namespace phyLS -{ - std::vector split_xmg_critical_path( xmg_network const& xmg ) - { - uint32_t xor3{ 0 }, xor2{ 0 }, maj{ 0 }, and_or{ 0 }; - depth_view dxmg{ xmg }; + node cp_node; - node cp_node; + /* find the po on critical path */ + xmg.foreach_po([&](auto const& f) { + auto level = dxmg.level(xmg.get_node(f)); - /* find the po on critical path */ - xmg.foreach_po( [&]( auto const& f ) { - auto level = dxmg.level( xmg.get_node( f ) ); - - if( level == dxmg.depth() ) - { - cp_node = xmg.get_node( f ); - return false; - } - - return true; - } ); - - /* recursive until reach the primary inputs */ - while( !xmg.is_constant( cp_node ) && !xmg.is_pi( cp_node ) ) - { - bool has_constant_fanin = false; - - /* check if all the fanin nodes are not constant */ - xmg.foreach_fanin( cp_node, [&]( auto const& f ) { - if( xmg.is_constant( xmg.get_node( f ) ) ) - { - has_constant_fanin = true; - return false; - } - return true; - } ); - - if( xmg.is_maj( cp_node ) ) - { - if( has_constant_fanin ) - { - ++and_or; - } - else - { - ++maj; - } - } - else if( xmg.is_xor3( cp_node ) ) - { - if( has_constant_fanin ) - { - ++xor2; - } - else - { - ++xor3; - } - } - else - { - assert( false && "UNKNOWN operator" ); - } - - /* continue process fanin node */ - xmg.foreach_fanin( cp_node, [&]( auto const& f ) { - auto level = dxmg.level( xmg.get_node( f ) ); - - if( level + 1 == dxmg.level( cp_node ) ) - { - cp_node = xmg.get_node( f ); - return false; - } - return true; - } ); + if (level == dxmg.depth()) { + cp_node = xmg.get_node(f); + return false; } - std::vector v{ xor3, xor2, maj, and_or }; - return v; - } - - void xmg_critical_path_profile_gates( xmg_network const& xmg, xmg_critical_path_stats& stats ) - { - auto v = split_xmg_critical_path( xmg ); - stats.xor3 = v[0]; - stats.xor2 = v[1]; - stats.maj = v[2]; - stats.and_or = v[3]; + return true; + }); + + /* recursive until reach the primary inputs */ + while (!xmg.is_constant(cp_node) && !xmg.is_pi(cp_node)) { + bool has_constant_fanin = false; + + /* check if all the fanin nodes are not constant */ + xmg.foreach_fanin(cp_node, [&](auto const& f) { + if (xmg.is_constant(xmg.get_node(f))) { + has_constant_fanin = true; + return false; + } + return true; + }); + + if (xmg.is_maj(cp_node)) { + if (has_constant_fanin) { + ++and_or; + } else { + ++maj; + } + } else if (xmg.is_xor3(cp_node)) { + if (has_constant_fanin) { + ++xor2; + } else { + ++xor3; + } + } else { + assert(false && "UNKNOWN operator"); + } + + /* continue process fanin node */ + xmg.foreach_fanin(cp_node, [&](auto const& f) { + auto level = dxmg.level(xmg.get_node(f)); + + if (level + 1 == dxmg.level(cp_node)) { + cp_node = xmg.get_node(f); + return false; + } + return true; + }); } + std::vector v{xor3, xor2, maj, and_or}; + return v; } + +void xmg_critical_path_profile_gates(xmg_network const& xmg, + xmg_critical_path_stats& stats) { + auto v = split_xmg_critical_path(xmg); + stats.xor3 = v[0]; + stats.xor2 = v[1]; + stats.maj = v[2]; + stats.and_or = v[3]; +} + +} // namespace phyLS diff --git a/src/core/properties.hpp b/src/core/properties.hpp index e09d6a6..a2cbdf1 100644 --- a/src/core/properties.hpp +++ b/src/core/properties.hpp @@ -13,30 +13,29 @@ #ifndef PROPERTIES_HPP #define PROPERTIES_HPP +#include + #include #include -#include using namespace mockturtle; -namespace phyLS -{ - struct xmg_critical_path_stats - { - uint32_t xor3{ 0 }; - uint32_t xor2{ 0 }; - uint32_t maj{ 0 }; - uint32_t and_or{ 0 }; +namespace phyLS { +struct xmg_critical_path_stats { + uint32_t xor3{0}; + uint32_t xor2{0}; + uint32_t maj{0}; + uint32_t and_or{0}; - void report() const - { - fmt::print( "On critical path: XOR3: {}, XOR2: {}, MAJ: {}, AND/OR: {}\n", - xor3, xor2, maj, and_or ); - } - }; - - void xmg_critical_path_profile_gates( xmg_network const& xmg, xmg_critical_path_stats& stats ); + void report() const { + fmt::print("On critical path: XOR3: {}, XOR2: {}, MAJ: {}, AND/OR: {}\n", + xor3, xor2, maj, and_or); + } +}; -} +void xmg_critical_path_profile_gates(xmg_network const& xmg, + xmg_critical_path_stats& stats); + +} // namespace phyLS #endif diff --git a/src/core/stp_sat.hpp b/src/core/stp_sat.hpp index 1fc06a7..fa95ca1 100644 --- a/src/core/stp_sat.hpp +++ b/src/core/stp_sat.hpp @@ -12,99 +12,84 @@ #pragma once -#include "matrix.hpp" +#include + #include #include #include -#include #include #include #include +#include "matrix.hpp" + using namespace std; -namespace phyLS -{ - struct coordinate - { - int Abscissa; - int Ordinate; - int parameter_Intermediate; - int parameter_Gate; - }; +namespace phyLS { +struct coordinate { + int Abscissa; + int Ordinate; + int parameter_Intermediate; + int parameter_Gate; +}; - struct cdccl_impl - { - vector Intermediate; - string Result; - vector Gate; - vector Level; // Define the network as a coordinate system - }; +struct cdccl_impl { + vector Intermediate; + string Result; + vector Gate; + vector Level; // Define the network as a coordinate system +}; - class stp_cdccl_impl - { - public: - stp_cdccl_impl(vector &in, vector> &mtxvec) - : in(in), mtxvec(mtxvec) - { - } +class stp_cdccl_impl { + public: + stp_cdccl_impl(vector &in, vector> &mtxvec) + : in(in), mtxvec(mtxvec) {} - void run_normal() - { - parser_from_bench(in, mtxvec); - bench_solve(in); - } + void run_normal() { + parser_from_bench(in, mtxvec); + bench_solve(in); + } - private: - void parser_from_bench(vector &in, vector> &mtxvec) - { - vector tt; - string s1 = "INPUT"; - string s2 = "OUTPUT"; - string s3 = "LUT"; - string s4 = ","; - int count1 = 0, count2 = 0; - for (int i = 0; i < in.size(); i++) - { - if (in[i].find(s1) != string::npos) - { - count1 += 1; - } - else if (in[i].find(s2) != string::npos) - { - count2 += 1; - } - else if (in[i].find(s3) != string::npos) - { - if (in[i].find(s4) != string::npos) - { - vector temp; - string flag0 = "="; - string flag1 = "x"; - string flag2 = "("; - string flag3 = ","; - string flag4 = ")"; - int p0 = in[i].find(flag0); - int p1 = in[i].find(flag1); - int p2 = in[i].find(flag2); - int p3 = in[i].find(flag3); - int p4 = in[i].find(flag4); - string temp0 = in[i].substr(1, p0 - 2); - string temp1 = in[i].substr(p1 + 1, p2 - p1 - 2); - string temp2 = in[i].substr(p2 + 2, p3 - p2 - 2); - string temp3 = in[i].substr(p3 + 3, p4 - p3 - 3); - int intstr0 = atoi(temp0.c_str()); - int intstr1 = atoi(temp2.c_str()); - int intstr2 = atoi(temp3.c_str()); - temp.push_back(intstr1); - temp.push_back(intstr2); - temp.push_back(intstr0); - string temp4; - int len = temp1.length(); - for (int i = 0; i < len; i++) - { - switch (temp1[i]) - { + private: + void parser_from_bench(vector &in, vector> &mtxvec) { + vector tt; + string s1 = "INPUT"; + string s2 = "OUTPUT"; + string s3 = "LUT"; + string s4 = ","; + int count1 = 0, count2 = 0; + for (int i = 0; i < in.size(); i++) { + if (in[i].find(s1) != string::npos) { + count1 += 1; + } else if (in[i].find(s2) != string::npos) { + count2 += 1; + } else if (in[i].find(s3) != string::npos) { + if (in[i].find(s4) != string::npos) { + vector temp; + string flag0 = "="; + string flag1 = "x"; + string flag2 = "("; + string flag3 = ","; + string flag4 = ")"; + int p0 = in[i].find(flag0); + int p1 = in[i].find(flag1); + int p2 = in[i].find(flag2); + int p3 = in[i].find(flag3); + int p4 = in[i].find(flag4); + string temp0 = in[i].substr(1, p0 - 2); + string temp1 = in[i].substr(p1 + 1, p2 - p1 - 2); + string temp2 = in[i].substr(p2 + 2, p3 - p2 - 2); + string temp3 = in[i].substr(p3 + 3, p4 - p3 - 3); + int intstr0 = atoi(temp0.c_str()); + int intstr1 = atoi(temp2.c_str()); + int intstr2 = atoi(temp3.c_str()); + temp.push_back(intstr1); + temp.push_back(intstr2); + temp.push_back(intstr0); + string temp4; + int len = temp1.length(); + for (int i = 0; i < len; i++) { + switch (temp1[i]) { case '0': temp4.append("0000"); continue; @@ -153,30 +138,26 @@ namespace phyLS case 'f': temp4.append("1111"); continue; - } } - tt.push_back(temp4); - mtxvec.push_back(temp); } - else - { - vector temp; - string flag1 = "x"; - string flag2 = "("; - string flag3 = ")"; - int p1 = in[i].find(flag1); - int p2 = in[i].find(flag2); - int p3 = in[i].find(flag3); - string temp1 = in[i].substr(p1 + 1, p2 - p1 - 1); - string temp2 = in[i].substr(p2 + 2, p3 - p2 - 2); - int intstr1 = atoi(temp2.c_str()); - temp.push_back(intstr1); - string temp3; - int len = temp1.length(); - for (int i = 0; i < len; i++) - { - switch (temp1[i]) - { + tt.push_back(temp4); + mtxvec.push_back(temp); + } else { + vector temp; + string flag1 = "x"; + string flag2 = "("; + string flag3 = ")"; + int p1 = in[i].find(flag1); + int p2 = in[i].find(flag2); + int p3 = in[i].find(flag3); + string temp1 = in[i].substr(p1 + 1, p2 - p1 - 1); + string temp2 = in[i].substr(p2 + 2, p3 - p2 - 2); + int intstr1 = atoi(temp2.c_str()); + temp.push_back(intstr1); + string temp3; + int len = temp1.length(); + for (int i = 0; i < len; i++) { + switch (temp1[i]) { case '0': temp3.append("00"); break; @@ -186,894 +167,765 @@ namespace phyLS case '2': temp3.append("10"); break; - } } - tt.push_back(temp3); - mtxvec.push_back(temp); } + tt.push_back(temp3); + mtxvec.push_back(temp); } } - vector temp; - temp.push_back(count1); - temp.push_back(count2); - mtxvec.push_back(temp); - in.assign(tt.begin(), tt.end()); } + vector temp; + temp.push_back(count1); + temp.push_back(count2); + mtxvec.push_back(temp); + in.assign(tt.begin(), tt.end()); + } - void bench_solve(vector &in) + void bench_solve(vector &in) { + int length1 = mtxvec[mtxvec.size() - 1][0]; // number of primary input + int length2 = mtxvec[mtxvec.size() - 1][1]; // number of primary output + int length3 = mtxvec[0][2]; // the minimum minuend + int length4 = + mtxvec[mtxvec.size() - 2 - length2][2]; // the maximum variable + vector> + list; // the solution space is two dimension vector + vector list_temp; + cdccl_impl list_temp_temp; + + string Result_temp(length1, '2'); // temporary result + coordinate Level_temp; + Level_temp.Abscissa = -1; + Level_temp.Ordinate = -1; + Level_temp.parameter_Intermediate = -1; + Level_temp.parameter_Gate = -1; + list_temp_temp.Level.resize( + length4, Level_temp); // Initialize level as a space with the size of + // variables(length4) + /* + * initialization + */ + coordinate Gate_level; + Gate_level.Abscissa = 0; + Gate_level.Ordinate = 0; + Gate_level.parameter_Intermediate = -1; + Gate_level.parameter_Gate = -1; + string Intermediate_temp; + for (int i = mtxvec.size() - 1 - length2; i < mtxvec.size() - 1; + i++) // the original intermediate { - int length1 = mtxvec[mtxvec.size() - 1][0]; // number of primary input - int length2 = mtxvec[mtxvec.size() - 1][1]; // number of primary output - int length3 = mtxvec[0][2]; // the minimum minuend - int length4 = mtxvec[mtxvec.size() - 2 - length2][2]; // the maximum variable - vector> list; // the solution space is two dimension vector - vector list_temp; - cdccl_impl list_temp_temp; - - string Result_temp(length1, '2'); // temporary result - coordinate Level_temp; - Level_temp.Abscissa = -1; - Level_temp.Ordinate = -1; - Level_temp.parameter_Intermediate = -1; - Level_temp.parameter_Gate = -1; - list_temp_temp.Level.resize(length4, Level_temp); // Initialize level as a space with the size of variables(length4) - /* - * initialization - */ - coordinate Gate_level; - Gate_level.Abscissa = 0; - Gate_level.Ordinate = 0; - Gate_level.parameter_Intermediate = -1; - Gate_level.parameter_Gate = -1; - string Intermediate_temp; - for (int i = mtxvec.size() - 1 - length2; i < mtxvec.size() - 1; i++) // the original intermediate - { - if (mtxvec[i][0] < length3) - { - if (in[i][0] == '1') - { - Result_temp[mtxvec[i][0] - 1] = '1'; - } - else - { - Result_temp[mtxvec[i][0] - 1] = '0'; - } + if (mtxvec[i][0] < length3) { + if (in[i][0] == '1') { + Result_temp[mtxvec[i][0] - 1] = '1'; + } else { + Result_temp[mtxvec[i][0] - 1] = '0'; } - else - { - list_temp_temp.Gate.push_back(mtxvec[i][0]); - if (in[i][0] == '1') - { - Intermediate_temp += "1"; - } - else - { - Intermediate_temp += "0"; - } + } else { + list_temp_temp.Gate.push_back(mtxvec[i][0]); + if (in[i][0] == '1') { + Intermediate_temp += "1"; + } else { + Intermediate_temp += "0"; } - list_temp_temp.Level[mtxvec[i][0] - 1] = Gate_level; } - list_temp_temp.Result = Result_temp; - list_temp_temp.Intermediate.push_back(Intermediate_temp); - list_temp.push_back(list_temp_temp); // level 0 - list.push_back(list_temp); - /* - * The first level information - */ - int count1 = 0; - for (int level = 0;; level++) // the computation process - { - int flag = 0, ordinate = 0; // the flag of the end of the loop & the ordinate of each level's gate - vector list_temp1; - for (int k = 0; k < list[level].size(); k++) - { - cdccl_impl temp1; // temporary gate - temp1.Result = list[level][k].Result; // first, next level's Result is same as the front level - for (int j = 0; j < list[level][k].Intermediate.size(); j++) - { - temp1.Level = list[level][k].Level; // next level's Level information - for (int j1 = 0; j1 < list[level][k].Gate.size(); j1++) - { - temp1.Level[list[level][k].Gate[j1] - 1].parameter_Intermediate = j; - temp1.Level[list[level][k].Gate[j1] - 1].parameter_Gate = j1; + list_temp_temp.Level[mtxvec[i][0] - 1] = Gate_level; + } + list_temp_temp.Result = Result_temp; + list_temp_temp.Intermediate.push_back(Intermediate_temp); + list_temp.push_back(list_temp_temp); // level 0 + list.push_back(list_temp); + /* + * The first level information + */ + int count1 = 0; + for (int level = 0;; level++) // the computation process + { + int flag = 0, ordinate = 0; // the flag of the end of the loop & the + // ordinate of each level's gate + vector list_temp1; + for (int k = 0; k < list[level].size(); k++) { + cdccl_impl temp1; // temporary gate + temp1.Result = list[level][k].Result; // first, next level's Result is + // same as the front level + for (int j = 0; j < list[level][k].Intermediate.size(); j++) { + temp1.Level = list[level][k].Level; // next level's Level information + for (int j1 = 0; j1 < list[level][k].Gate.size(); j1++) { + temp1.Level[list[level][k].Gate[j1] - 1].parameter_Intermediate = j; + temp1.Level[list[level][k].Gate[j1] - 1].parameter_Gate = j1; + } + + coordinate level_current; // new level + level_current.Abscissa = level + 1; + level_current.parameter_Intermediate = -1; + level_current.parameter_Gate = -1; + level_current.Ordinate = ordinate; + + temp1.Gate.assign(list[level][k].Gate.begin(), + list[level][k].Gate.end()); // need more!!!!! + temp1.Intermediate.push_back(list[level][k].Intermediate[j]); + + vector Intermediate_temp; + vector Gate_temp; + vector Gate_judge(length4, -1); + int count_cdccl = 0; + for (int i = 0; i < temp1.Gate.size(); i++) { + int length = temp1.Gate[i] - length3; + int Gate_f = mtxvec[length][0]; // the front Gate variable + int Gate_b = mtxvec[length][1]; // the behind Gate variable + string tt = in[length]; // the correndsponding Truth Table + char target = temp1.Intermediate[0][i]; // the SAT target + vector Intermediate_temp_temp; + + int flag_cdccl = 0; + string Intermediate_temp_temp_F, Intermediate_temp_temp_B; + if (temp1.Level[Gate_f - 1].Abscissa >= 0) { + if (Gate_f < length3) { + char contrast_R1 = list[temp1.Level[Gate_f - 1].Abscissa] + [temp1.Level[Gate_f - 1].Ordinate] + .Result[Gate_f - 1]; + Intermediate_temp_temp_F.push_back(contrast_R1); + } else { + char contrast_I1 = + list[temp1.Level[Gate_f - 1].Abscissa] + [temp1.Level[Gate_f - 1].Ordinate] + .Intermediate + [temp1.Level[Gate_f - 1].parameter_Intermediate] + [temp1.Level[Gate_f - 1].parameter_Gate]; + Intermediate_temp_temp_F.push_back(contrast_I1); + } + flag_cdccl += 1; } - - coordinate level_current; // new level - level_current.Abscissa = level + 1; - level_current.parameter_Intermediate = -1; - level_current.parameter_Gate = -1; - level_current.Ordinate = ordinate; - - temp1.Gate.assign(list[level][k].Gate.begin(), list[level][k].Gate.end()); // need more!!!!! - temp1.Intermediate.push_back(list[level][k].Intermediate[j]); - - vector Intermediate_temp; - vector Gate_temp; - vector Gate_judge(length4, -1); - int count_cdccl = 0; - for (int i = 0; i < temp1.Gate.size(); i++) - { - int length = temp1.Gate[i] - length3; - int Gate_f = mtxvec[length][0]; // the front Gate variable - int Gate_b = mtxvec[length][1]; // the behind Gate variable - string tt = in[length]; // the correndsponding Truth Table - char target = temp1.Intermediate[0][i]; // the SAT target - vector Intermediate_temp_temp; - - int flag_cdccl = 0; - string Intermediate_temp_temp_F, Intermediate_temp_temp_B; - if (temp1.Level[Gate_f - 1].Abscissa >= 0) - { - if (Gate_f < length3) - { - char contrast_R1 = list[temp1.Level[Gate_f - 1].Abscissa][temp1.Level[Gate_f - 1].Ordinate].Result[Gate_f - 1]; - Intermediate_temp_temp_F.push_back(contrast_R1); - } - else - { - char contrast_I1 = list[temp1.Level[Gate_f - 1].Abscissa][temp1.Level[Gate_f - 1].Ordinate].Intermediate[temp1.Level[Gate_f - 1].parameter_Intermediate][temp1.Level[Gate_f - 1].parameter_Gate]; - Intermediate_temp_temp_F.push_back(contrast_I1); - } - flag_cdccl += 1; + if (temp1.Level[Gate_b - 1].Abscissa >= 0) { + if (Gate_b < length3) { + char contrast_R2 = list[temp1.Level[Gate_b - 1].Abscissa] + [temp1.Level[Gate_b - 1].Ordinate] + .Result[Gate_b - 1]; + Intermediate_temp_temp_B.push_back(contrast_R2); + } else { + char contrast_I2 = + list[temp1.Level[Gate_b - 1].Abscissa] + [temp1.Level[Gate_b - 1].Ordinate] + .Intermediate + [temp1.Level[Gate_b - 1].parameter_Intermediate] + [temp1.Level[Gate_b - 1].parameter_Gate]; + Intermediate_temp_temp_B.push_back(contrast_I2); } - if (temp1.Level[Gate_b - 1].Abscissa >= 0) - { - if (Gate_b < length3) - { - char contrast_R2 = list[temp1.Level[Gate_b - 1].Abscissa][temp1.Level[Gate_b - 1].Ordinate].Result[Gate_b - 1]; - Intermediate_temp_temp_B.push_back(contrast_R2); + flag_cdccl += 2; + } + if (Intermediate_temp.size() == 0) { + if (flag_cdccl == 0) { + Gate_judge[Gate_f - 1] = count_cdccl; + count_cdccl += 1; + Gate_judge[Gate_b - 1] = count_cdccl; + count_cdccl += 1; + Gate_temp.push_back(Gate_f); + Gate_temp.push_back(Gate_b); + if (tt[0] == target) { + Intermediate_temp_temp.push_back("11"); } - else - { - char contrast_I2 = list[temp1.Level[Gate_b - 1].Abscissa][temp1.Level[Gate_b - 1].Ordinate].Intermediate[temp1.Level[Gate_b - 1].parameter_Intermediate][temp1.Level[Gate_b - 1].parameter_Gate]; - Intermediate_temp_temp_B.push_back(contrast_I2); + if (tt[1] == target) { + Intermediate_temp_temp.push_back("01"); } - flag_cdccl += 2; - } - if (Intermediate_temp.size() == 0) - { - if (flag_cdccl == 0) - { + if (tt[2] == target) { + Intermediate_temp_temp.push_back("10"); + } + if (tt[3] == target) { + Intermediate_temp_temp.push_back("00"); + } + } else if (flag_cdccl == 1) { + Gate_judge[Gate_b - 1] = count_cdccl; + count_cdccl += 1; + Gate_temp.push_back(Gate_b); + if (tt[0] == target) { + if (Intermediate_temp_temp_F == "1") { + Intermediate_temp_temp.push_back("1"); + } + } + if (tt[1] == target) { + if (Intermediate_temp_temp_F == "0") { + Intermediate_temp_temp.push_back("1"); + } + } + if (tt[2] == target) { + if (Intermediate_temp_temp_F == "1") { + Intermediate_temp_temp.push_back("0"); + } + } + if (tt[3] == target) { + if (Intermediate_temp_temp_F == "0") { + Intermediate_temp_temp.push_back("0"); + } + } + } else if (flag_cdccl == 2) { + Gate_judge[Gate_f - 1] = count_cdccl; + count_cdccl += 1; + Gate_temp.push_back(Gate_f); + if (tt[0] == target) { + if (Intermediate_temp_temp_B == "1") { + Intermediate_temp_temp.push_back("1"); + } + } + if (tt[1] == target) { + if (Intermediate_temp_temp_B == "1") { + Intermediate_temp_temp.push_back("0"); + } + } + if (tt[2] == target) { + if (Intermediate_temp_temp_B == "0") { + Intermediate_temp_temp.push_back("1"); + } + } + if (tt[3] == target) { + if (Intermediate_temp_temp_B == "0") { + Intermediate_temp_temp.push_back("0"); + } + } + } else { + int t0 = 0, t1 = 0, t2 = 0, t3 = 0; + if (tt[0] == target) { + if ((Intermediate_temp_temp_F == "1") && + (Intermediate_temp_temp_B == "1")) { + t0 = 1; + } + } + if (tt[1] == target) { + if ((Intermediate_temp_temp_F == "0") && + (Intermediate_temp_temp_B == "1")) { + t1 = 1; + } + } + if (tt[2] == target) { + if ((Intermediate_temp_temp_F == "1") && + (Intermediate_temp_temp_B == "0")) { + t2 = 1; + } + } + if (tt[3] == target) { + if ((Intermediate_temp_temp_F == "0") && + (Intermediate_temp_temp_B == "0")) { + t3 = 1; + } + } + if ((t0 == 1) || (t1 == 1) || (t2 == 1) || (t3 == 1)) { Gate_judge[Gate_f - 1] = count_cdccl; count_cdccl += 1; Gate_judge[Gate_b - 1] = count_cdccl; count_cdccl += 1; Gate_temp.push_back(Gate_f); Gate_temp.push_back(Gate_b); - if (tt[0] == target) - { + if (t0 == 1) { Intermediate_temp_temp.push_back("11"); } - if (tt[1] == target) - { + if (t1 == 1) { Intermediate_temp_temp.push_back("01"); } - if (tt[2] == target) - { + if (t2 == 1) { Intermediate_temp_temp.push_back("10"); } - if (tt[3] == target) - { + if (t3 == 1) { Intermediate_temp_temp.push_back("00"); } } - else if (flag_cdccl == 1) - { - Gate_judge[Gate_b - 1] = count_cdccl; - count_cdccl += 1; - Gate_temp.push_back(Gate_b); - if (tt[0] == target) - { - if (Intermediate_temp_temp_F == "1") - { - Intermediate_temp_temp.push_back("1"); + } + } else { + if (flag_cdccl == 0) { + int count_Gate_f = 0, count_Gate_b = 0; + for (int j = 0; j < Intermediate_temp.size(); j++) { + int flag; + string t1, t2, t3, t4; + if (Gate_judge[Gate_f - 1] < 0) { + count_Gate_f = 1; + if (tt[0] == target) { + t1 = "1"; } - } - if (tt[1] == target) - { - if (Intermediate_temp_temp_F == "0") - { - Intermediate_temp_temp.push_back("1"); + if (tt[1] == target) { + t2 = "0"; } - } - if (tt[2] == target) - { - if (Intermediate_temp_temp_F == "1") - { - Intermediate_temp_temp.push_back("0"); + if (tt[2] == target) { + t3 = "1"; } + if (tt[3] == target) { + t4 = "0"; + } + flag = 1; + } else { + int count_sat = 0; + if (tt[0] == target) { + if (Intermediate_temp[j][Gate_judge[Gate_f - 1]] == '1') { + t1 = "11"; + count_sat += 1; + } + } + if (tt[1] == target) { + if (Intermediate_temp[j][Gate_judge[Gate_f - 1]] == '0') { + t2 = "01"; + count_sat += 1; + } + } + if (tt[2] == target) { + if (Intermediate_temp[j][Gate_judge[Gate_f - 1]] == '1') { + t3 = "10"; + count_sat += 1; + } + } + if (tt[3] == target) { + if (Intermediate_temp[j][Gate_judge[Gate_f - 1]] == '0') { + t4 = "00"; + count_sat += 1; + } + } + if (count_sat == 0) { + continue; + } + flag = 2; } - if (tt[3] == target) - { - if (Intermediate_temp_temp_F == "0") - { - Intermediate_temp_temp.push_back("0"); + if (Gate_judge[Gate_b - 1] < 0) { + count_Gate_b = 1; + if (flag == 1) { + if (t1 == "1") { + t1 += "1"; + string result_temporary(Intermediate_temp[j]); + result_temporary += t1; + Intermediate_temp_temp.push_back(result_temporary); + } + if (t2 == "0") { + t2 += "1"; + string result_temporary(Intermediate_temp[j]); + result_temporary += t2; + Intermediate_temp_temp.push_back(result_temporary); + } + if (t3 == "1") { + t3 += "0"; + string result_temporary(Intermediate_temp[j]); + result_temporary += t3; + Intermediate_temp_temp.push_back(result_temporary); + } + if (t4 == "0") { + t4 += "0"; + string result_temporary(Intermediate_temp[j]); + result_temporary += t4; + Intermediate_temp_temp.push_back(result_temporary); + } + } + if (flag == 2) { + if (t1 == "11") { + t1 = "1"; + string result_temporary(Intermediate_temp[j]); + result_temporary += t1; + Intermediate_temp_temp.push_back(result_temporary); + } + if (t2 == "01") { + t2 = "1"; + string result_temporary(Intermediate_temp[j]); + result_temporary += t2; + Intermediate_temp_temp.push_back(result_temporary); + } + if (t3 == "10") { + t3 = "0"; + string result_temporary(Intermediate_temp[j]); + result_temporary += t3; + Intermediate_temp_temp.push_back(result_temporary); + } + if (t4 == "00") { + t4 = "0"; + string result_temporary(Intermediate_temp[j]); + result_temporary += t4; + Intermediate_temp_temp.push_back(result_temporary); + } + } + } else { + if (flag == 1) { + if (tt[0] == target) { + if (Intermediate_temp[j][Gate_judge[Gate_b - 1]] == + '1') { + string result_temporary(Intermediate_temp[j]); + result_temporary += t1; + Intermediate_temp_temp.push_back(result_temporary); + } + } + if (tt[1] == target) { + if (Intermediate_temp[j][Gate_judge[Gate_b - 1]] == + '1') { + string result_temporary(Intermediate_temp[j]); + result_temporary += t2; + Intermediate_temp_temp.push_back(result_temporary); + } + } + if (tt[2] == target) { + if (Intermediate_temp[j][Gate_judge[Gate_b - 1]] == + '0') { + string result_temporary(Intermediate_temp[j]); + result_temporary += t3; + Intermediate_temp_temp.push_back(result_temporary); + } + } + if (tt[3] == target) { + if (Intermediate_temp[j][Gate_judge[Gate_b - 1]] == + '0') { + string result_temporary(Intermediate_temp[j]); + result_temporary += t4; + Intermediate_temp_temp.push_back(result_temporary); + } + } + } + if (flag == 2) { + int count_sat1 = 0; + if (t1 == "11") { + if (Intermediate_temp[j][Gate_judge[Gate_b - 1]] == + '1') { + count_sat1 += 1; + } + } + if (t2 == "01") { + if (Intermediate_temp[j][Gate_judge[Gate_b - 1]] == + '1') { + count_sat1 += 1; + } + } + if (t3 == "10") { + if (Intermediate_temp[j][Gate_judge[Gate_b - 1]] == + '0') { + count_sat1 += 1; + } + } + if (t4 == "00") { + if (Intermediate_temp[j][Gate_judge[Gate_b - 1]] == + '0') { + count_sat1 += 1; + } + } + if (count_sat1 > 0) { + Intermediate_temp_temp.push_back(Intermediate_temp[j]); + } } } } - else if (flag_cdccl == 2) - { + if (count_Gate_f == 1) { Gate_judge[Gate_f - 1] = count_cdccl; count_cdccl += 1; Gate_temp.push_back(Gate_f); - if (tt[0] == target) - { - if (Intermediate_temp_temp_B == "1") - { - Intermediate_temp_temp.push_back("1"); - } - } - if (tt[1] == target) - { - if (Intermediate_temp_temp_B == "1") - { - Intermediate_temp_temp.push_back("0"); - } - } - if (tt[2] == target) - { - if (Intermediate_temp_temp_B == "0") - { - Intermediate_temp_temp.push_back("1"); - } - } - if (tt[3] == target) - { - if (Intermediate_temp_temp_B == "0") - { - Intermediate_temp_temp.push_back("0"); - } - } } - else - { - int t0 = 0, t1 = 0, t2 = 0, t3 = 0; - if (tt[0] == target) - { - if ((Intermediate_temp_temp_F == "1") && (Intermediate_temp_temp_B == "1")) - { - t0 = 1; - } - } - if (tt[1] == target) - { - if ((Intermediate_temp_temp_F == "0") && (Intermediate_temp_temp_B == "1")) - { - t1 = 1; - } - } - if (tt[2] == target) - { - if ((Intermediate_temp_temp_F == "1") && (Intermediate_temp_temp_B == "0")) - { - t2 = 1; - } - } - if (tt[3] == target) - { - if ((Intermediate_temp_temp_F == "0") && (Intermediate_temp_temp_B == "0")) - { - t3 = 1; - } - } - if ((t0 == 1) || (t1 == 1) || (t2 == 1) || (t3 == 1)) - { - Gate_judge[Gate_f - 1] = count_cdccl; - count_cdccl += 1; - Gate_judge[Gate_b - 1] = count_cdccl; - count_cdccl += 1; - Gate_temp.push_back(Gate_f); - Gate_temp.push_back(Gate_b); - if (t0 == 1) - { - Intermediate_temp_temp.push_back("11"); - } - if (t1 == 1) - { - Intermediate_temp_temp.push_back("01"); - } - if (t2 == 1) - { - Intermediate_temp_temp.push_back("10"); - } - if (t3 == 1) - { - Intermediate_temp_temp.push_back("00"); - } - } + if (count_Gate_b == 1) { + Gate_judge[Gate_b - 1] = count_cdccl; + count_cdccl += 1; + Gate_temp.push_back(Gate_b); } - } - else - { - if (flag_cdccl == 0) - { - int count_Gate_f = 0, count_Gate_b = 0; - for (int j = 0; j < Intermediate_temp.size(); j++) - { - int flag; - string t1, t2, t3, t4; - if (Gate_judge[Gate_f - 1] < 0) - { - count_Gate_f = 1; - if (tt[0] == target) - { - t1 = "1"; - } - if (tt[1] == target) - { - t2 = "0"; - } - if (tt[2] == target) - { - t3 = "1"; - } - if (tt[3] == target) - { - t4 = "0"; - } - flag = 1; - } - else - { - int count_sat = 0; - if (tt[0] == target) - { - if (Intermediate_temp[j][Gate_judge[Gate_f - 1]] == '1') - { - t1 = "11"; - count_sat += 1; - } - } - if (tt[1] == target) - { - if (Intermediate_temp[j][Gate_judge[Gate_f - 1]] == '0') - { - t2 = "01"; - count_sat += 1; - } - } - if (tt[2] == target) - { - if (Intermediate_temp[j][Gate_judge[Gate_f - 1]] == '1') - { - t3 = "10"; - count_sat += 1; - } - } - if (tt[3] == target) - { - if (Intermediate_temp[j][Gate_judge[Gate_f - 1]] == '0') - { - t4 = "00"; - count_sat += 1; - } - } - if (count_sat == 0) - { - continue; - } - flag = 2; - } - if (Gate_judge[Gate_b - 1] < 0) - { - count_Gate_b = 1; - if (flag == 1) - { - if (t1 == "1") - { - t1 += "1"; - string result_temporary(Intermediate_temp[j]); - result_temporary += t1; - Intermediate_temp_temp.push_back(result_temporary); - } - if (t2 == "0") - { - t2 += "1"; - string result_temporary(Intermediate_temp[j]); - result_temporary += t2; - Intermediate_temp_temp.push_back(result_temporary); - } - if (t3 == "1") - { - t3 += "0"; - string result_temporary(Intermediate_temp[j]); - result_temporary += t3; - Intermediate_temp_temp.push_back(result_temporary); - } - if (t4 == "0") - { - t4 += "0"; - string result_temporary(Intermediate_temp[j]); - result_temporary += t4; - Intermediate_temp_temp.push_back(result_temporary); - } - } - if (flag == 2) - { - if (t1 == "11") - { - t1 = "1"; - string result_temporary(Intermediate_temp[j]); - result_temporary += t1; - Intermediate_temp_temp.push_back(result_temporary); - } - if (t2 == "01") - { - t2 = "1"; - string result_temporary(Intermediate_temp[j]); - result_temporary += t2; - Intermediate_temp_temp.push_back(result_temporary); - } - if (t3 == "10") - { - t3 = "0"; - string result_temporary(Intermediate_temp[j]); - result_temporary += t3; - Intermediate_temp_temp.push_back(result_temporary); - } - if (t4 == "00") - { - t4 = "0"; - string result_temporary(Intermediate_temp[j]); - result_temporary += t4; - Intermediate_temp_temp.push_back(result_temporary); - } + } else if (flag_cdccl == 1) { + int flag_1 = 0; + for (int j = 0; j < Intermediate_temp.size(); j++) { + if (Gate_judge[Gate_b - 1] < 0) { + flag_1 = 1; + if (tt[0] == target) { + if (Intermediate_temp_temp_F == "1") { + string Intermediate_temp_temp1(Intermediate_temp[j]); + Intermediate_temp_temp1 += "1"; + Intermediate_temp_temp.push_back( + Intermediate_temp_temp1); } } - else - { - if (flag == 1) - { - if (tt[0] == target) - { - if (Intermediate_temp[j][Gate_judge[Gate_b - 1]] == '1') - { - string result_temporary(Intermediate_temp[j]); - result_temporary += t1; - Intermediate_temp_temp.push_back(result_temporary); - } - } - if (tt[1] == target) - { - if (Intermediate_temp[j][Gate_judge[Gate_b - 1]] == '1') - { - string result_temporary(Intermediate_temp[j]); - result_temporary += t2; - Intermediate_temp_temp.push_back(result_temporary); - } - } - if (tt[2] == target) - { - if (Intermediate_temp[j][Gate_judge[Gate_b - 1]] == '0') - { - string result_temporary(Intermediate_temp[j]); - result_temporary += t3; - Intermediate_temp_temp.push_back(result_temporary); - } - } - if (tt[3] == target) - { - if (Intermediate_temp[j][Gate_judge[Gate_b - 1]] == '0') - { - string result_temporary(Intermediate_temp[j]); - result_temporary += t4; - Intermediate_temp_temp.push_back(result_temporary); - } - } - } - if (flag == 2) - { - int count_sat1 = 0; - if (t1 == "11") - { - if (Intermediate_temp[j][Gate_judge[Gate_b - 1]] == '1') - { - count_sat1 += 1; - } - } - if (t2 == "01") - { - if (Intermediate_temp[j][Gate_judge[Gate_b - 1]] == '1') - { - count_sat1 += 1; - } - } - if (t3 == "10") - { - if (Intermediate_temp[j][Gate_judge[Gate_b - 1]] == '0') - { - count_sat1 += 1; - } - } - if (t4 == "00") - { - if (Intermediate_temp[j][Gate_judge[Gate_b - 1]] == '0') - { - count_sat1 += 1; - } - } - if (count_sat1 > 0) - { - Intermediate_temp_temp.push_back(Intermediate_temp[j]); - } + if (tt[1] == target) { + if (Intermediate_temp_temp_F == "0") { + string Intermediate_temp_temp1(Intermediate_temp[j]); + Intermediate_temp_temp1 += "1"; + Intermediate_temp_temp.push_back( + Intermediate_temp_temp1); } } - } - if (count_Gate_f == 1) - { - Gate_judge[Gate_f - 1] = count_cdccl; - count_cdccl += 1; - Gate_temp.push_back(Gate_f); - } - if (count_Gate_b == 1) - { - Gate_judge[Gate_b - 1] = count_cdccl; - count_cdccl += 1; - Gate_temp.push_back(Gate_b); - } - } - else if (flag_cdccl == 1) - { - int flag_1 = 0; - for (int j = 0; j < Intermediate_temp.size(); j++) - { - if (Gate_judge[Gate_b - 1] < 0) - { - flag_1 = 1; - if (tt[0] == target) - { - if (Intermediate_temp_temp_F == "1") - { - string Intermediate_temp_temp1(Intermediate_temp[j]); - Intermediate_temp_temp1 += "1"; - Intermediate_temp_temp.push_back(Intermediate_temp_temp1); - } - } - if (tt[1] == target) - { - if (Intermediate_temp_temp_F == "0") - { - string Intermediate_temp_temp1(Intermediate_temp[j]); - Intermediate_temp_temp1 += "1"; - Intermediate_temp_temp.push_back(Intermediate_temp_temp1); - } - } - if (tt[2] == target) - { - if (Intermediate_temp_temp_F == "1") - { - string Intermediate_temp_temp1(Intermediate_temp[j]); - Intermediate_temp_temp1 += "0"; - Intermediate_temp_temp.push_back(Intermediate_temp_temp1); - } - } - if (tt[3] == target) - { - if (Intermediate_temp_temp_F == "0") - { - string Intermediate_temp_temp1(Intermediate_temp[j]); - Intermediate_temp_temp1 += "0"; - Intermediate_temp_temp.push_back(Intermediate_temp_temp1); - } + if (tt[2] == target) { + if (Intermediate_temp_temp_F == "1") { + string Intermediate_temp_temp1(Intermediate_temp[j]); + Intermediate_temp_temp1 += "0"; + Intermediate_temp_temp.push_back( + Intermediate_temp_temp1); } } - else - { - if (tt[0] == target) - { - if ((Intermediate_temp[j][Gate_judge[Gate_b - 1]] == '1') && (Intermediate_temp_temp_F == "1")) - { - Intermediate_temp_temp.push_back(Intermediate_temp[j]); - } - } - if (tt[1] == target) - { - if ((Intermediate_temp[j][Gate_judge[Gate_b - 1]] == '1') && (Intermediate_temp_temp_F == "0")) - { - Intermediate_temp_temp.push_back(Intermediate_temp[j]); - } - } - if (tt[2] == target) - { - if ((Intermediate_temp[j][Gate_judge[Gate_b - 1]] == '0') && (Intermediate_temp_temp_F == "1")) - { - Intermediate_temp_temp.push_back(Intermediate_temp[j]); - } - } - if (tt[3] == target) - { - if ((Intermediate_temp[j][Gate_judge[Gate_b - 1]] == '0') && (Intermediate_temp_temp_F == "0")) - { - Intermediate_temp_temp.push_back(Intermediate_temp[j]); - } + if (tt[3] == target) { + if (Intermediate_temp_temp_F == "0") { + string Intermediate_temp_temp1(Intermediate_temp[j]); + Intermediate_temp_temp1 += "0"; + Intermediate_temp_temp.push_back( + Intermediate_temp_temp1); } } - } - if (flag_1 == 1) - { - Gate_judge[Gate_b - 1] = count_cdccl; - count_cdccl += 1; - Gate_temp.push_back(Gate_b); - } - } - else if (flag_cdccl == 2) - { - int flag_2 = 0; - for (int j = 0; j < Intermediate_temp.size(); j++) - { - if (Gate_judge[Gate_f - 1] < 0) - { - flag_2 = 1; - if (tt[0] == target) - { - if (Intermediate_temp_temp_B == "1") - { - string Intermediate_temp_temp1(Intermediate_temp[j]); - Intermediate_temp_temp1 += "1"; - Intermediate_temp_temp.push_back(Intermediate_temp_temp1); - } - } - if (tt[1] == target) - { - if (Intermediate_temp_temp_B == "1") - { - string Intermediate_temp_temp1(Intermediate_temp[j]); - Intermediate_temp_temp1 += "0"; - Intermediate_temp_temp.push_back(Intermediate_temp_temp1); - } - } - if (tt[2] == target) - { - if (Intermediate_temp_temp_B == "0") - { - string Intermediate_temp_temp1(Intermediate_temp[j]); - Intermediate_temp_temp1 += "1"; - Intermediate_temp_temp.push_back(Intermediate_temp_temp1); - } - } - if (tt[3] == target) - { - if (Intermediate_temp_temp_B == "0") - { - string Intermediate_temp_temp1(Intermediate_temp[j]); - Intermediate_temp_temp1 += "0"; - Intermediate_temp_temp.push_back(Intermediate_temp_temp1); - } - } - } - else - { - if (tt[0] == target) - { - if ((Intermediate_temp[j][Gate_judge[Gate_f - 1]] == '1') && (Intermediate_temp_temp_B == "1")) - { - Intermediate_temp_temp.push_back(Intermediate_temp[j]); - } - } - if (tt[1] == target) - { - if ((Intermediate_temp[j][Gate_judge[Gate_f - 1]] == '0') && (Intermediate_temp_temp_B == "1")) - { - Intermediate_temp_temp.push_back(Intermediate_temp[j]); - } - } - if (tt[2] == target) - { - if ((Intermediate_temp[j][Gate_judge[Gate_f - 1]] == '1') && (Intermediate_temp_temp_B == "0")) - { - Intermediate_temp_temp.push_back(Intermediate_temp[j]); - } - } - if (tt[3] == target) - { - if ((Intermediate_temp[j][Gate_judge[Gate_f - 1]] == '0') && (Intermediate_temp_temp_B == "0")) - { - Intermediate_temp_temp.push_back(Intermediate_temp[j]); - } - } - } - } - if (flag_2 == 1) - { - Gate_judge[Gate_f - 1] = count_cdccl; - count_cdccl += 1; - Gate_temp.push_back(Gate_f); - } - } - else - { - for (int j = 0; j < Intermediate_temp.size(); j++) - { - if (tt[0] == target) - { - if ((Intermediate_temp_temp_F == "1") && (Intermediate_temp_temp_B == "1")) - { + } else { + if (tt[0] == target) { + if ((Intermediate_temp[j][Gate_judge[Gate_b - 1]] == + '1') && + (Intermediate_temp_temp_F == "1")) { Intermediate_temp_temp.push_back(Intermediate_temp[j]); } } - if (tt[1] == target) - { - if ((Intermediate_temp_temp_F == "0") && (Intermediate_temp_temp_B == "1")) - { + if (tt[1] == target) { + if ((Intermediate_temp[j][Gate_judge[Gate_b - 1]] == + '1') && + (Intermediate_temp_temp_F == "0")) { Intermediate_temp_temp.push_back(Intermediate_temp[j]); } } - if (tt[2] == target) - { - if ((Intermediate_temp_temp_F == "1") && (Intermediate_temp_temp_B == "0")) - { + if (tt[2] == target) { + if ((Intermediate_temp[j][Gate_judge[Gate_b - 1]] == + '0') && + (Intermediate_temp_temp_F == "1")) { Intermediate_temp_temp.push_back(Intermediate_temp[j]); } } - if (tt[3] == target) - { - if ((Intermediate_temp_temp_F == "0") && (Intermediate_temp_temp_B == "0")) - { + if (tt[3] == target) { + if ((Intermediate_temp[j][Gate_judge[Gate_b - 1]] == + '0') && + (Intermediate_temp_temp_F == "0")) { Intermediate_temp_temp.push_back(Intermediate_temp[j]); } } } } - } - Intermediate_temp.assign(Intermediate_temp_temp.begin(), Intermediate_temp_temp.end()); - if (Intermediate_temp_temp.size() == 0) - { - break; + if (flag_1 == 1) { + Gate_judge[Gate_b - 1] = count_cdccl; + count_cdccl += 1; + Gate_temp.push_back(Gate_b); + } + } else if (flag_cdccl == 2) { + int flag_2 = 0; + for (int j = 0; j < Intermediate_temp.size(); j++) { + if (Gate_judge[Gate_f - 1] < 0) { + flag_2 = 1; + if (tt[0] == target) { + if (Intermediate_temp_temp_B == "1") { + string Intermediate_temp_temp1(Intermediate_temp[j]); + Intermediate_temp_temp1 += "1"; + Intermediate_temp_temp.push_back( + Intermediate_temp_temp1); + } + } + if (tt[1] == target) { + if (Intermediate_temp_temp_B == "1") { + string Intermediate_temp_temp1(Intermediate_temp[j]); + Intermediate_temp_temp1 += "0"; + Intermediate_temp_temp.push_back( + Intermediate_temp_temp1); + } + } + if (tt[2] == target) { + if (Intermediate_temp_temp_B == "0") { + string Intermediate_temp_temp1(Intermediate_temp[j]); + Intermediate_temp_temp1 += "1"; + Intermediate_temp_temp.push_back( + Intermediate_temp_temp1); + } + } + if (tt[3] == target) { + if (Intermediate_temp_temp_B == "0") { + string Intermediate_temp_temp1(Intermediate_temp[j]); + Intermediate_temp_temp1 += "0"; + Intermediate_temp_temp.push_back( + Intermediate_temp_temp1); + } + } + } else { + if (tt[0] == target) { + if ((Intermediate_temp[j][Gate_judge[Gate_f - 1]] == + '1') && + (Intermediate_temp_temp_B == "1")) { + Intermediate_temp_temp.push_back(Intermediate_temp[j]); + } + } + if (tt[1] == target) { + if ((Intermediate_temp[j][Gate_judge[Gate_f - 1]] == + '0') && + (Intermediate_temp_temp_B == "1")) { + Intermediate_temp_temp.push_back(Intermediate_temp[j]); + } + } + if (tt[2] == target) { + if ((Intermediate_temp[j][Gate_judge[Gate_f - 1]] == + '1') && + (Intermediate_temp_temp_B == "0")) { + Intermediate_temp_temp.push_back(Intermediate_temp[j]); + } + } + if (tt[3] == target) { + if ((Intermediate_temp[j][Gate_judge[Gate_f - 1]] == + '0') && + (Intermediate_temp_temp_B == "0")) { + Intermediate_temp_temp.push_back(Intermediate_temp[j]); + } + } + } + } + if (flag_2 == 1) { + Gate_judge[Gate_f - 1] = count_cdccl; + count_cdccl += 1; + Gate_temp.push_back(Gate_f); + } + } else { + for (int j = 0; j < Intermediate_temp.size(); j++) { + if (tt[0] == target) { + if ((Intermediate_temp_temp_F == "1") && + (Intermediate_temp_temp_B == "1")) { + Intermediate_temp_temp.push_back(Intermediate_temp[j]); + } + } + if (tt[1] == target) { + if ((Intermediate_temp_temp_F == "0") && + (Intermediate_temp_temp_B == "1")) { + Intermediate_temp_temp.push_back(Intermediate_temp[j]); + } + } + if (tt[2] == target) { + if ((Intermediate_temp_temp_F == "1") && + (Intermediate_temp_temp_B == "0")) { + Intermediate_temp_temp.push_back(Intermediate_temp[j]); + } + } + if (tt[3] == target) { + if ((Intermediate_temp_temp_F == "0") && + (Intermediate_temp_temp_B == "0")) { + Intermediate_temp_temp.push_back(Intermediate_temp[j]); + } + } + } } } - temp1.Intermediate.assign(Intermediate_temp.begin(), Intermediate_temp.end()); - temp1.Gate.assign(Gate_temp.begin(), Gate_temp.end()); - for (int l = 0; l < temp1.Gate.size(); l++) - { - temp1.Level[temp1.Gate[l] - 1] = level_current; + Intermediate_temp.assign(Intermediate_temp_temp.begin(), + Intermediate_temp_temp.end()); + if (Intermediate_temp_temp.size() == 0) { + break; } + } + temp1.Intermediate.assign(Intermediate_temp.begin(), + Intermediate_temp.end()); + temp1.Gate.assign(Gate_temp.begin(), Gate_temp.end()); + for (int l = 0; l < temp1.Gate.size(); l++) { + temp1.Level[temp1.Gate[l] - 1] = level_current; + } - int count = 0; // whether there is a PI assignment - for (int k = 0; k < temp1.Intermediate.size(); k++) // mix the Result and the Intermediate information in one level - { - count = 1; - cdccl_impl temp2; - temp2.Level = temp1.Level; - string Result_temp(temp1.Result); - temp2.Gate.assign(temp1.Gate.begin(), temp1.Gate.end()); - string Intermediate_temp1(temp1.Intermediate[k]); - int count1 = 0, count2 = 0; // whether the assignment made - for (int k11 = 0; k11 < temp1.Gate.size(); k11++) + int count = 0; // whether there is a PI assignment + for (int k = 0; k < temp1.Intermediate.size(); + k++) // mix the Result and the Intermediate information in one + // level + { + count = 1; + cdccl_impl temp2; + temp2.Level = temp1.Level; + string Result_temp(temp1.Result); + temp2.Gate.assign(temp1.Gate.begin(), temp1.Gate.end()); + string Intermediate_temp1(temp1.Intermediate[k]); + int count1 = 0, count2 = 0; // whether the assignment made + for (int k11 = 0; k11 < temp1.Gate.size(); k11++) { + if (temp1.Gate[k11] < + length3) // if the Gate is smaller than length3, it is PI { - if (temp1.Gate[k11] < length3) // if the Gate is smaller than length3, it is PI + temp2.Level[temp1.Gate[k11] - 1].Ordinate = ordinate; + if ((temp1.Result[temp1.Gate[k11] - 1] == '2') || + (temp1.Result[temp1.Gate[k11] - 1] == + temp1.Intermediate[k][k11])) // whether the PI can be + // assigned a value { - temp2.Level[temp1.Gate[k11] - 1].Ordinate = ordinate; - if ((temp1.Result[temp1.Gate[k11] - 1] == '2') || (temp1.Result[temp1.Gate[k11] - 1] == temp1.Intermediate[k][k11])) // whether the PI can be assigned a value - { - Result_temp[temp1.Gate[k11] - 1] = temp1.Intermediate[k][k11]; - } - else - { - count1 = 1; // if one assignment can't make, the count1 = 1 - } - Intermediate_temp1.erase(Intermediate_temp1.begin() + (k11 - count2)); - temp2.Gate.erase(temp2.Gate.begin() + (k11 - count2)); - count++, count2++; - } - } - if (count1 == 0) - { - temp2.Result = Result_temp; - temp2.Intermediate.push_back(Intermediate_temp1); - for (int k12 = 0; k12 < temp2.Gate.size(); k12++) - { - temp2.Level[temp2.Gate[k12] - 1].Ordinate = ordinate; - } - } - if (count == 1) - { - break; - } - else if (temp2.Result.size() > 0) - { - list_temp1.push_back(temp2); - ordinate += 1; - if (temp2.Gate.empty()) - { - flag += 1; + Result_temp[temp1.Gate[k11] - 1] = temp1.Intermediate[k][k11]; + } else { + count1 = 1; // if one assignment can't make, the count1 = 1 } + Intermediate_temp1.erase(Intermediate_temp1.begin() + + (k11 - count2)); + temp2.Gate.erase(temp2.Gate.begin() + (k11 - count2)); + count++, count2++; } } - if (count == 1) - { - list_temp1.push_back(temp1); + if (count1 == 0) { + temp2.Result = Result_temp; + temp2.Intermediate.push_back(Intermediate_temp1); + for (int k12 = 0; k12 < temp2.Gate.size(); k12++) { + temp2.Level[temp2.Gate[k12] - 1].Ordinate = ordinate; + } + } + if (count == 1) { + break; + } else if (temp2.Result.size() > 0) { + list_temp1.push_back(temp2); ordinate += 1; - if (temp1.Gate.empty()) - { + if (temp2.Gate.empty()) { flag += 1; } } - temp1.Intermediate.clear(); } - } - list.push_back(list_temp1); // next level's information - if (flag == list[level + 1].size()) // in one level, if all node's Gate is empty, then break the loop - { - break; + if (count == 1) { + list_temp1.push_back(temp1); + ordinate += 1; + if (temp1.Gate.empty()) { + flag += 1; + } + } + temp1.Intermediate.clear(); } } - - in.clear(); - for (int j = 0; j < list[list.size() - 1].size(); j++) // all result + list.push_back(list_temp1); // next level's information + if (flag == list[level + 1].size()) // in one level, if all node's Gate + // is empty, then break the loop { - in.push_back(list[list.size() - 1][j].Result); + break; } } - private: - vector ∈ - vector> &mtxvec; - }; - - class stp_cdccl_impl2 - { - public: - stp_cdccl_impl2(vector &in, vector> &mtxvec, int &po) - : in(in), mtxvec(mtxvec), po(po) + in.clear(); + for (int j = 0; j < list[list.size() - 1].size(); j++) // all result { + in.push_back(list[list.size() - 1][j].Result); } + } - void run_single_po() - { - parser_from_bench(in, mtxvec); - bench_solve_single_po(in, mtxvec, po); - } + private: + vector ∈ + vector> &mtxvec; +}; - private: - void parser_from_bench(vector &in, vector> &mtxvec) - { - vector tt; - string s1 = "INPUT"; - string s2 = "OUTPUT"; - string s3 = "LUT"; - string s4 = ","; - int count1 = 0, count2 = 0; - for (int i = 0; i < in.size(); i++) - { - if (in[i].find(s1) != string::npos) - { - count1 += 1; - } - else if (in[i].find(s2) != string::npos) - { - count2 += 1; - } - else if (in[i].find(s3) != string::npos) - { - if (in[i].find(s4) != string::npos) - { - vector temp; - string flag0 = "="; - string flag1 = "x"; - string flag2 = "("; - string flag3 = ","; - string flag4 = ")"; - int p0 = in[i].find(flag0); - int p1 = in[i].find(flag1); - int p2 = in[i].find(flag2); - int p3 = in[i].find(flag3); - int p4 = in[i].find(flag4); - string temp0 = in[i].substr(1, p0 - 2); - string temp1 = in[i].substr(p1 + 1, p2 - p1 - 2); - string temp2 = in[i].substr(p2 + 2, p3 - p2 - 2); - string temp3 = in[i].substr(p3 + 3, p4 - p3 - 3); - int intstr0 = atoi(temp0.c_str()); - int intstr1 = atoi(temp2.c_str()); - int intstr2 = atoi(temp3.c_str()); - temp.push_back(intstr1); - temp.push_back(intstr2); - temp.push_back(intstr0); - string temp4; - int len = temp1.length(); - for (int i = 0; i < len; i++) - { - switch (temp1[i]) - { +class stp_cdccl_impl2 { + public: + stp_cdccl_impl2(vector &in, vector> &mtxvec, int &po) + : in(in), mtxvec(mtxvec), po(po) {} + + void run_single_po() { + parser_from_bench(in, mtxvec); + bench_solve_single_po(in, mtxvec, po); + } + + private: + void parser_from_bench(vector &in, vector> &mtxvec) { + vector tt; + string s1 = "INPUT"; + string s2 = "OUTPUT"; + string s3 = "LUT"; + string s4 = ","; + int count1 = 0, count2 = 0; + for (int i = 0; i < in.size(); i++) { + if (in[i].find(s1) != string::npos) { + count1 += 1; + } else if (in[i].find(s2) != string::npos) { + count2 += 1; + } else if (in[i].find(s3) != string::npos) { + if (in[i].find(s4) != string::npos) { + vector temp; + string flag0 = "="; + string flag1 = "x"; + string flag2 = "("; + string flag3 = ","; + string flag4 = ")"; + int p0 = in[i].find(flag0); + int p1 = in[i].find(flag1); + int p2 = in[i].find(flag2); + int p3 = in[i].find(flag3); + int p4 = in[i].find(flag4); + string temp0 = in[i].substr(1, p0 - 2); + string temp1 = in[i].substr(p1 + 1, p2 - p1 - 2); + string temp2 = in[i].substr(p2 + 2, p3 - p2 - 2); + string temp3 = in[i].substr(p3 + 3, p4 - p3 - 3); + int intstr0 = atoi(temp0.c_str()); + int intstr1 = atoi(temp2.c_str()); + int intstr2 = atoi(temp3.c_str()); + temp.push_back(intstr1); + temp.push_back(intstr2); + temp.push_back(intstr0); + string temp4; + int len = temp1.length(); + for (int i = 0; i < len; i++) { + switch (temp1[i]) { case '0': temp4.append("0000"); continue; @@ -1122,30 +974,26 @@ namespace phyLS case 'f': temp4.append("1111"); continue; - } } - tt.push_back(temp4); - mtxvec.push_back(temp); } - else - { - vector temp; - string flag1 = "x"; - string flag2 = "("; - string flag3 = ")"; - int p1 = in[i].find(flag1); - int p2 = in[i].find(flag2); - int p3 = in[i].find(flag3); - string temp1 = in[i].substr(p1 + 1, p2 - p1 - 1); - string temp2 = in[i].substr(p2 + 2, p3 - p2 - 2); - int intstr1 = atoi(temp2.c_str()); - temp.push_back(intstr1); - string temp3; - int len = temp1.length(); - for (int i = 0; i < len; i++) - { - switch (temp1[i]) - { + tt.push_back(temp4); + mtxvec.push_back(temp); + } else { + vector temp; + string flag1 = "x"; + string flag2 = "("; + string flag3 = ")"; + int p1 = in[i].find(flag1); + int p2 = in[i].find(flag2); + int p3 = in[i].find(flag3); + string temp1 = in[i].substr(p1 + 1, p2 - p1 - 1); + string temp2 = in[i].substr(p2 + 2, p3 - p2 - 2); + int intstr1 = atoi(temp2.c_str()); + temp.push_back(intstr1); + string temp3; + int len = temp1.length(); + for (int i = 0; i < len; i++) { + switch (temp1[i]) { case '0': temp3.append("00"); break; @@ -1155,739 +1003,634 @@ namespace phyLS case '2': temp3.append("10"); break; - } } - tt.push_back(temp3); - mtxvec.push_back(temp); } + tt.push_back(temp3); + mtxvec.push_back(temp); } } - vector temp; - temp.push_back(count1); - temp.push_back(count2); - mtxvec.push_back(temp); - in.assign(tt.begin(), tt.end()); } + vector temp; + temp.push_back(count1); + temp.push_back(count2); + mtxvec.push_back(temp); + in.assign(tt.begin(), tt.end()); + } - void bench_solve_single_po(vector &in, vector> &mtxvec, int &po) - { - int length0 = mtxvec.size() - 1; - int length1 = mtxvec[length0][1]; - int length2 = mtxvec[0][2]; - int length3 = mtxvec[length0][0]; - int po_tmp = mtxvec[length0 - length1 + po][0]; - vector temp; - string result_tmp1(length3, '2'); - vector result_tmp; - matrix_propagation(in[length0 - length1 + po], result_tmp, '1'); - if (po_tmp >= length2) - { - int y = po_tmp - length2; - solve(mtxvec, in, result_tmp[0][0], y, result_tmp1, temp); - } - if (temp.size() == 0) - { - in.clear(); - } - in.assign(temp.begin(), temp.end()); + void bench_solve_single_po(vector &in, vector> &mtxvec, + int &po) { + int length0 = mtxvec.size() - 1; + int length1 = mtxvec[length0][1]; + int length2 = mtxvec[0][2]; + int length3 = mtxvec[length0][0]; + int po_tmp = mtxvec[length0 - length1 + po][0]; + vector temp; + string result_tmp1(length3, '2'); + vector result_tmp; + matrix_propagation(in[length0 - length1 + po], result_tmp, '1'); + if (po_tmp >= length2) { + int y = po_tmp - length2; + solve(mtxvec, in, result_tmp[0][0], y, result_tmp1, temp); } + if (temp.size() == 0) { + in.clear(); + } + in.assign(temp.begin(), temp.end()); + } - void solve(vector> &mtxvec, vector &in, char target, int i, string &result1, vector &temp) - { - int length1 = mtxvec[0][2]; - int length2 = mtxvec[mtxvec.size() - 1][0]; - int length3 = length1 - length2; - vector result_tmp; - vector result; - string reset = result1; - matrix_propagation(in[i], result_tmp, target); - if ((mtxvec[i][0] < length1) && (mtxvec[i][1] < length1)) - { - for (int j = 0; j < result_tmp.size(); j++) - { - int count = 0; - result1 = reset; - if ((result1[mtxvec[i][0] - length3] == '2') || (result1[mtxvec[i][0] - length3] == result_tmp[j][0])) - { - result1[mtxvec[i][0] - length3] = result_tmp[j][0]; - count += 1; - } - if ((result1[mtxvec[i][1] - length3] == '2') || (result1[mtxvec[i][1] - length3] == result_tmp[j][1])) - { - result1[mtxvec[i][1] - length3] = result_tmp[j][1]; - count += 1; - } - if (count == 2) - { - result.push_back(result1); - } + void solve(vector> &mtxvec, vector &in, char target, + int i, string &result1, vector &temp) { + int length1 = mtxvec[0][2]; + int length2 = mtxvec[mtxvec.size() - 1][0]; + int length3 = length1 - length2; + vector result_tmp; + vector result; + string reset = result1; + matrix_propagation(in[i], result_tmp, target); + if ((mtxvec[i][0] < length1) && (mtxvec[i][1] < length1)) { + for (int j = 0; j < result_tmp.size(); j++) { + int count = 0; + result1 = reset; + if ((result1[mtxvec[i][0] - length3] == '2') || + (result1[mtxvec[i][0] - length3] == result_tmp[j][0])) { + result1[mtxvec[i][0] - length3] = result_tmp[j][0]; + count += 1; + } + if ((result1[mtxvec[i][1] - length3] == '2') || + (result1[mtxvec[i][1] - length3] == result_tmp[j][1])) { + result1[mtxvec[i][1] - length3] = result_tmp[j][1]; + count += 1; + } + if (count == 2) { + result.push_back(result1); } - temp.assign(result.begin(), result.end()); } - else if ((mtxvec[i][0] < length1) && (mtxvec[i][1] >= length1)) - { - for (int j = 0; j < result_tmp.size(); j++) - { - int count = 0; - result1 = reset; - if ((result1[mtxvec[i][0] - length3] == '2') || (result1[mtxvec[i][0] - length3] == result_tmp[j][0])) - { - result1[mtxvec[i][0] - length3] = result_tmp[j][0]; - count += 1; - } - int i2 = mtxvec[i][1] - length1; - if (count == 1) - { - solve(mtxvec, in, result_tmp[j][1], i2, result1, temp); - } + temp.assign(result.begin(), result.end()); + } else if ((mtxvec[i][0] < length1) && (mtxvec[i][1] >= length1)) { + for (int j = 0; j < result_tmp.size(); j++) { + int count = 0; + result1 = reset; + if ((result1[mtxvec[i][0] - length3] == '2') || + (result1[mtxvec[i][0] - length3] == result_tmp[j][0])) { + result1[mtxvec[i][0] - length3] = result_tmp[j][0]; + count += 1; + } + int i2 = mtxvec[i][1] - length1; + if (count == 1) { + solve(mtxvec, in, result_tmp[j][1], i2, result1, temp); + } + result.insert(result.end(), temp.begin(), temp.end()); + temp.clear(); + } + temp.assign(result.begin(), result.end()); + } else if ((mtxvec[i][0] >= length1) && (mtxvec[i][1] >= length1)) { + for (int j = 0; j < result_tmp.size(); j++) { + result1 = reset; + int i1 = mtxvec[i][0] - length1; + solve(mtxvec, in, result_tmp[j][0], i1, result1, temp); + int i2 = mtxvec[i][1] - length1; + vector temp_temp(temp); + for (int k = 0; k < temp_temp.size(); k++) { + result1 = temp_temp[k]; + solve(mtxvec, in, result_tmp[j][1], i2, result1, temp); result.insert(result.end(), temp.begin(), temp.end()); temp.clear(); } - temp.assign(result.begin(), result.end()); } - else if ((mtxvec[i][0] >= length1) && (mtxvec[i][1] >= length1)) - { - for (int j = 0; j < result_tmp.size(); j++) - { - result1 = reset; - int i1 = mtxvec[i][0] - length1; - solve(mtxvec, in, result_tmp[j][0], i1, result1, temp); - int i2 = mtxvec[i][1] - length1; - vector temp_temp(temp); - for (int k = 0; k < temp_temp.size(); k++) - { - result1 = temp_temp[k]; - solve(mtxvec, in, result_tmp[j][1], i2, result1, temp); - result.insert(result.end(), temp.begin(), temp.end()); - temp.clear(); - } - } - temp.assign(result.begin(), result.end()); + temp.assign(result.begin(), result.end()); + } + } + + void matrix_propagation(string tt, vector &result, char target) { + int n = tt.size(); + if (n == 2) { + if (tt[0] == target) { + string result_tmp1 = "1"; + result.push_back(result_tmp1); + } + if (tt[1] == target) { + string result_tmp2 = "0"; + result.push_back(result_tmp2); + } + } else if (n == 4) { + if (tt[0] == target) { + string result_tmp3 = "11"; + result.push_back(result_tmp3); + } + if (tt[1] == target) { + string result_tmp4 = "01"; // 因为真值表是反的，所以两个变量位置换一下 + result.push_back(result_tmp4); + } + if (tt[2] == target) { + string result_tmp5 = "10"; + result.push_back(result_tmp5); + } + if (tt[3] == target) { + string result_tmp6 = "00"; + result.push_back(result_tmp6); } } + } - void matrix_propagation(string tt, vector &result, char target) - { - int n = tt.size(); - if (n == 2) - { - if (tt[0] == target) - { - string result_tmp1 = "1"; - result.push_back(result_tmp1); - } - if (tt[1] == target) - { - string result_tmp2 = "0"; - result.push_back(result_tmp2); - } - } - else if (n == 4) - { - if (tt[0] == target) - { - string result_tmp3 = "11"; - result.push_back(result_tmp3); - } - if (tt[1] == target) - { - string result_tmp4 = "01"; //因为真值表是反的，所以两个变量位置换一下 - result.push_back(result_tmp4); - } - if (tt[2] == target) - { - string result_tmp5 = "10"; - result.push_back(result_tmp5); - } - if (tt[3] == target) - { - string result_tmp6 = "00"; - result.push_back(result_tmp6); - } - } - } + private: + vector ∈ + vector> &mtxvec; + int &po; +}; - private: - vector ∈ - vector> &mtxvec; - int &po; - }; +class stp_cnf_impl { + public: + stp_cnf_impl(vector &expression, vector &tt, + vector &mtxvec) + : expression(expression), tt(tt), mtxvec(mtxvec) {} - class stp_cnf_impl - { - public: - stp_cnf_impl(vector &expression, vector &tt, vector &mtxvec) - : expression(expression), tt(tt), mtxvec(mtxvec) - { - } + void run_cnf() { + parser_from_expression(tt, expression); + matrix_mapping(tt, mtxvec); + stp_cnf(tt, mtxvec, expression); + stp_result(tt, expression); + } - void run_cnf() - { - parser_from_expression(tt, expression); - matrix_mapping(tt, mtxvec); - stp_cnf(tt, mtxvec, expression); - stp_result(tt, expression); - } - - private: - void parser_from_expression(vector &tt, vector &expression) - { - string tmp0 = "MN"; - string tmp1 = "END"; - string tmp2 = "MP"; - string tmp3 = "MD"; - string tmp4 = "A"; - for (int i = 2; i < expression.size(); i++) - { - if (expression[i] == 0) - { - tt.push_back(tmp1); - } - else - { - if ((expression[i - 1] == 0) && (expression[i + 1] == 0)) - { - if (expression[i] < 0) - { - tt.push_back(tmp0); - tt.push_back(tmp4); - } - else - { - tt.push_back(tmp2); - tt.push_back(tmp4); - } - } - else if (expression[i + 1] == 0) - { - if (expression[i] < 0) - { - tt.push_back(tmp0); - tt.push_back(tmp4); - } - else - { - tt.push_back(tmp4); - } - } - else - { - tt.push_back(tmp3); - if (expression[i] < 0) - { - tt.push_back(tmp0); - } + private: + void parser_from_expression(vector &tt, vector &expression) { + string tmp0 = "MN"; + string tmp1 = "END"; + string tmp2 = "MP"; + string tmp3 = "MD"; + string tmp4 = "A"; + for (int i = 2; i < expression.size(); i++) { + if (expression[i] == 0) { + tt.push_back(tmp1); + } else { + if ((expression[i - 1] == 0) && (expression[i + 1] == 0)) { + if (expression[i] < 0) { + tt.push_back(tmp0); + tt.push_back(tmp4); + } else { + tt.push_back(tmp2); tt.push_back(tmp4); } - } - expression[i] = abs(expression[i]); - } - } - - void matrix_mapping(vector &tt, vector &mtxvec) - { - for (int ix = 0; ix < tt.size(); ix++) - { - if (tt[ix] == "MN") - { - MatrixXi mtxtmp1(2, 2); - mtxtmp1(0, 0) = 0; - mtxtmp1(0, 1) = 1; - mtxtmp1(1, 0) = 1; - mtxtmp1(1, 1) = 0; - mtxvec.push_back(mtxtmp1); - } - else if (tt[ix] == "MP") - { - MatrixXi mtxtmp4(2, 2); - mtxtmp4(0, 0) = 1; - mtxtmp4(0, 1) = 0; - mtxtmp4(1, 0) = 0; - mtxtmp4(1, 1) = 1; - mtxvec.push_back(mtxtmp4); - } - else if (tt[ix] == "MD") - { - MatrixXi mtxtmp2(2, 4); - mtxtmp2(0, 0) = 1; - mtxtmp2(0, 1) = 1; - mtxtmp2(0, 2) = 1; - mtxtmp2(0, 3) = 0; - mtxtmp2(1, 0) = 0; - mtxtmp2(1, 1) = 0; - mtxtmp2(1, 2) = 0; - mtxtmp2(1, 3) = 1; - mtxvec.push_back(mtxtmp2); - } - else - { - MatrixXi mtxtmp3(2, 1); - mtxtmp3(0, 0) = 1; - mtxtmp3(1, 0) = 0; - mtxvec.push_back(mtxtmp3); + } else if (expression[i + 1] == 0) { + if (expression[i] < 0) { + tt.push_back(tmp0); + tt.push_back(tmp4); + } else { + tt.push_back(tmp4); + } + } else { + tt.push_back(tmp3); + if (expression[i] < 0) { + tt.push_back(tmp0); + } + tt.push_back(tmp4); } } + expression[i] = abs(expression[i]); } + } - void stp_cnf(vector &tt, vector &mtxvec, vector expression) - { - vector tt_tmp; - vector mtx_tmp; - vector exp_tmp; - vector result; - string tmp2 = "END"; - expression.erase(expression.begin(), expression.begin() + 2); - for (int i = 0; i < tt.size(); i++) - { - if (tt[i] == "END") - { - stp_cut(tt_tmp, mtx_tmp); - for (int j = 0; j < expression.size(); j++) - { - if (expression[0] == 0) - { - expression.erase(expression.begin()); - break; - } - else - { - exp_tmp.push_back(expression[0]); - expression.erase(expression.begin()); - } - } - for (int m = 0; m < tt_tmp.size(); m++) - { - result.push_back(tt_tmp[m]); - } - result.push_back(tmp2); - tt_tmp.clear(); - mtx_tmp.clear(); - exp_tmp.clear(); - } - else - { - tt_tmp.push_back(tt[i]); - mtx_tmp.push_back(mtxvec[i]); - } + void matrix_mapping(vector &tt, vector &mtxvec) { + for (int ix = 0; ix < tt.size(); ix++) { + if (tt[ix] == "MN") { + MatrixXi mtxtmp1(2, 2); + mtxtmp1(0, 0) = 0; + mtxtmp1(0, 1) = 1; + mtxtmp1(1, 0) = 1; + mtxtmp1(1, 1) = 0; + mtxvec.push_back(mtxtmp1); + } else if (tt[ix] == "MP") { + MatrixXi mtxtmp4(2, 2); + mtxtmp4(0, 0) = 1; + mtxtmp4(0, 1) = 0; + mtxtmp4(1, 0) = 0; + mtxtmp4(1, 1) = 1; + mtxvec.push_back(mtxtmp4); + } else if (tt[ix] == "MD") { + MatrixXi mtxtmp2(2, 4); + mtxtmp2(0, 0) = 1; + mtxtmp2(0, 1) = 1; + mtxtmp2(0, 2) = 1; + mtxtmp2(0, 3) = 0; + mtxtmp2(1, 0) = 0; + mtxtmp2(1, 1) = 0; + mtxtmp2(1, 2) = 0; + mtxtmp2(1, 3) = 1; + mtxvec.push_back(mtxtmp2); + } else { + MatrixXi mtxtmp3(2, 1); + mtxtmp3(0, 0) = 1; + mtxtmp3(1, 0) = 0; + mtxvec.push_back(mtxtmp3); } - tt.clear(); - tt.assign(result.begin(), result.end()); } + } - void stp_result(vector &tt, vector &expression) - { - int v = expression[0]; - string temp(v, '2'); - expression.erase(expression.begin(), (expression.begin() + 2)); - vector result_tmp; - vector result; - result_tmp.push_back(temp); - for (int i = 0; i < tt.size(); i++) - { - if (tt[i] != "END") - { - for (int j = 0; j < result_tmp.size(); j++) - { - string tmp0 = result_tmp[j]; - for (int l = 0; l < expression.size(); l++) - { - if (expression[l] == 0) - { - result.push_back(tmp0); - break; - } - else - { - int temp_count = expression[l] - 1; - if ((tt[i][l] == result_tmp[j][temp_count]) || (result_tmp[j][temp_count] == '2')) - { - tmp0[temp_count] = tt[i][l]; - } - else - { - break; - } - } - } - } - } - else - { - result_tmp.clear(); - result_tmp.assign(result.begin(), result.end()); - result.clear(); - for (int i = 0; i < expression.size(); i++) - { - if (expression[0] == 0) - { - expression.erase(expression.begin()); - break; - } + void stp_cnf(vector &tt, vector &mtxvec, + vector expression) { + vector tt_tmp; + vector mtx_tmp; + vector exp_tmp; + vector result; + string tmp2 = "END"; + expression.erase(expression.begin(), expression.begin() + 2); + for (int i = 0; i < tt.size(); i++) { + if (tt[i] == "END") { + stp_cut(tt_tmp, mtx_tmp); + for (int j = 0; j < expression.size(); j++) { + if (expression[0] == 0) { + expression.erase(expression.begin()); + break; + } else { + exp_tmp.push_back(expression[0]); expression.erase(expression.begin()); } } + for (int m = 0; m < tt_tmp.size(); m++) { + result.push_back(tt_tmp[m]); + } + result.push_back(tmp2); + tt_tmp.clear(); + mtx_tmp.clear(); + exp_tmp.clear(); + } else { + tt_tmp.push_back(tt[i]); + mtx_tmp.push_back(mtxvec[i]); } - tt.clear(); - tt.assign(result_tmp.begin(), result_tmp.end()); } + tt.clear(); + tt.assign(result.begin(), result.end()); + } - void stp_cut(vector &tt, vector &mtxvec) - { - vector mtx_tmp; - vector tt_tmp; - vector result_b; - string stp_result; - vector result; - int count = 0; - int length = tt.size(); - for (int i = 0; i < length; i++) //计算每个子式的变量个数 - { - if (tt[i] == "A") - { - count += 1; - } - } - for (int i = 0; i < length; i++) // CUT计算 - { - tt_tmp.push_back(tt[0]); - mtx_tmp.push_back(mtxvec[0]); - if ((tt[0] != "MN") && (tt[0] != "MD") && (tt[0] != "MP")) - { - tt_tmp.pop_back(); - mtx_tmp.pop_back(); - if (tt_tmp.size() >= 1) - { - stp_exchange_judge(tt_tmp, mtx_tmp); - stp_product_judge(tt_tmp, mtx_tmp); - result_b.push_back(mtx_tmp[0]); - } - tt_tmp.clear(); - mtx_tmp.clear(); - } - tt.erase(tt.begin()); - mtxvec.erase(mtxvec.begin()); - } - mtxvec.clear(); - mtxvec.assign(result_b.begin(), result_b.end()); - int target = 1; - stp_result_enumeration(mtxvec, target, stp_result); - string tmp; - for (int j = 0; j < stp_result.size(); j++) - { - if (stp_result[j] == '\n') - { - if (tmp.size() == count) - { - result.push_back(tmp); - } - if (tmp.size() > count) - { - int tmp0 = tmp.size() - count - 1; - tmp.erase((count - tmp0), tmp0 + 1); - result.push_back(tmp); - } - } - tmp += stp_result[j]; - } - tt.clear(); - tt.assign(result.begin(), result.end()); - } - - bool stp_exchange_judge(vector &tt, vector &mtxvec) - { - for (int i = tt.size(); i > 0; i--) - { - for (int j = tt.size(); j > 1; j--) - { - if (((tt[j - 1] != "MN") && (tt[j - 1] != "MC") && (tt[j - 1] != "MD") && (tt[j - 1] != "ME") && (tt[j - 1] != "MI") && (tt[j - 1] != "MR") && (tt[j - 1] != "MW")) && ((tt[j - 2] != "MN") && (tt[j - 2] != "MC") && (tt[j - 2] != "MD") && (tt[j - 2] != "ME") && (tt[j - 2] != "MI") && (tt[j - 2] != "MR") && (tt[j - 2] != "MW"))) - { - string tmp1_tt; - string tmp2_tt; - tmp1_tt += tt[j - 2]; - tmp2_tt += tt[j - 1]; - if (tmp1_tt[0] > tmp2_tt[0]) - { - MatrixXi matrix_w2(4, 4); - matrix_w2(0, 0) = 1; - matrix_w2(0, 1) = 0; - matrix_w2(0, 2) = 0; - matrix_w2(0, 3) = 0; - matrix_w2(1, 0) = 0; - matrix_w2(1, 1) = 0; - matrix_w2(1, 2) = 1; - matrix_w2(1, 3) = 0; - matrix_w2(2, 0) = 0; - matrix_w2(2, 1) = 1; - matrix_w2(2, 2) = 0; - matrix_w2(2, 3) = 0; - matrix_w2(3, 0) = 0; - matrix_w2(3, 1) = 0; - matrix_w2(3, 2) = 0; - matrix_w2(3, 3) = 1; - string tmp3_tt = "MW"; - string tmp4_tt = tt[j - 2]; - tt.insert(tt.begin() + (j - 2), tt[j - 1]); - tt.erase(tt.begin() + (j - 1)); - tt.insert(tt.begin() + (j - 1), tmp4_tt); - tt.erase(tt.begin() + j); - tt.insert(tt.begin() + (j - 2), tmp3_tt); - MatrixXi tmp_mtx = mtxvec[j - 2]; - mtxvec.insert(mtxvec.begin() + (j - 2), mtxvec[j - 1]); - mtxvec.erase(mtxvec.begin() + (j - 1)); - mtxvec.insert(mtxvec.begin() + (j - 1), tmp_mtx); - mtxvec.erase(mtxvec.begin() + j); - mtxvec.insert(mtxvec.begin() + (j - 2), matrix_w2); + void stp_result(vector &tt, vector &expression) { + int v = expression[0]; + string temp(v, '2'); + expression.erase(expression.begin(), (expression.begin() + 2)); + vector result_tmp; + vector result; + result_tmp.push_back(temp); + for (int i = 0; i < tt.size(); i++) { + if (tt[i] != "END") { + for (int j = 0; j < result_tmp.size(); j++) { + string tmp0 = result_tmp[j]; + for (int l = 0; l < expression.size(); l++) { + if (expression[l] == 0) { + result.push_back(tmp0); + break; + } else { + int temp_count = expression[l] - 1; + if ((tt[i][l] == result_tmp[j][temp_count]) || + (result_tmp[j][temp_count] == '2')) { + tmp0[temp_count] = tt[i][l]; + } else { + break; + } } } - if (((tt[j - 2] != "MN") && (tt[j - 2] != "MC") && (tt[j - 2] != "MD") && (tt[j - 2] != "ME") && (tt[j - 2] != "MI") && (tt[j - 2] != "MR") && (tt[j - 2] != "MW")) && ((tt[j - 1] == "MN") || (tt[j - 1] == "MC") || (tt[j - 1] == "MD") || (tt[j - 1] == "ME") || (tt[j - 1] == "MI") || (tt[j - 1] == "MR") || (tt[j - 1] == "MW"))) - { - MatrixXi tmp1; - tmp1 = mtxvec[j - 2]; - MatrixXi tmp2; - tmp2 = mtxvec[j - 1]; - stpm_exchange(tmp1, tmp2); - string tmp_tt = tt[j - 2]; + } + } else { + result_tmp.clear(); + result_tmp.assign(result.begin(), result.end()); + result.clear(); + for (int i = 0; i < expression.size(); i++) { + if (expression[0] == 0) { + expression.erase(expression.begin()); + break; + } + expression.erase(expression.begin()); + } + } + } + tt.clear(); + tt.assign(result_tmp.begin(), result_tmp.end()); + } + + void stp_cut(vector &tt, vector &mtxvec) { + vector mtx_tmp; + vector tt_tmp; + vector result_b; + string stp_result; + vector result; + int count = 0; + int length = tt.size(); + for (int i = 0; i < length; i++) // 计算每个子式的变量个数 + { + if (tt[i] == "A") { + count += 1; + } + } + for (int i = 0; i < length; i++) // CUT计算 + { + tt_tmp.push_back(tt[0]); + mtx_tmp.push_back(mtxvec[0]); + if ((tt[0] != "MN") && (tt[0] != "MD") && (tt[0] != "MP")) { + tt_tmp.pop_back(); + mtx_tmp.pop_back(); + if (tt_tmp.size() >= 1) { + stp_exchange_judge(tt_tmp, mtx_tmp); + stp_product_judge(tt_tmp, mtx_tmp); + result_b.push_back(mtx_tmp[0]); + } + tt_tmp.clear(); + mtx_tmp.clear(); + } + tt.erase(tt.begin()); + mtxvec.erase(mtxvec.begin()); + } + mtxvec.clear(); + mtxvec.assign(result_b.begin(), result_b.end()); + int target = 1; + stp_result_enumeration(mtxvec, target, stp_result); + string tmp; + for (int j = 0; j < stp_result.size(); j++) { + if (stp_result[j] == '\n') { + if (tmp.size() == count) { + result.push_back(tmp); + } + if (tmp.size() > count) { + int tmp0 = tmp.size() - count - 1; + tmp.erase((count - tmp0), tmp0 + 1); + result.push_back(tmp); + } + } + tmp += stp_result[j]; + } + tt.clear(); + tt.assign(result.begin(), result.end()); + } + + bool stp_exchange_judge(vector &tt, vector &mtxvec) { + for (int i = tt.size(); i > 0; i--) { + for (int j = tt.size(); j > 1; j--) { + if (((tt[j - 1] != "MN") && (tt[j - 1] != "MC") && + (tt[j - 1] != "MD") && (tt[j - 1] != "ME") && + (tt[j - 1] != "MI") && (tt[j - 1] != "MR") && + (tt[j - 1] != "MW")) && + ((tt[j - 2] != "MN") && (tt[j - 2] != "MC") && + (tt[j - 2] != "MD") && (tt[j - 2] != "ME") && + (tt[j - 2] != "MI") && (tt[j - 2] != "MR") && + (tt[j - 2] != "MW"))) { + string tmp1_tt; + string tmp2_tt; + tmp1_tt += tt[j - 2]; + tmp2_tt += tt[j - 1]; + if (tmp1_tt[0] > tmp2_tt[0]) { + MatrixXi matrix_w2(4, 4); + matrix_w2(0, 0) = 1; + matrix_w2(0, 1) = 0; + matrix_w2(0, 2) = 0; + matrix_w2(0, 3) = 0; + matrix_w2(1, 0) = 0; + matrix_w2(1, 1) = 0; + matrix_w2(1, 2) = 1; + matrix_w2(1, 3) = 0; + matrix_w2(2, 0) = 0; + matrix_w2(2, 1) = 1; + matrix_w2(2, 2) = 0; + matrix_w2(2, 3) = 0; + matrix_w2(3, 0) = 0; + matrix_w2(3, 1) = 0; + matrix_w2(3, 2) = 0; + matrix_w2(3, 3) = 1; + string tmp3_tt = "MW"; + string tmp4_tt = tt[j - 2]; tt.insert(tt.begin() + (j - 2), tt[j - 1]); tt.erase(tt.begin() + (j - 1)); - tt.insert(tt.begin() + (j - 1), tmp_tt); + tt.insert(tt.begin() + (j - 1), tmp4_tt); tt.erase(tt.begin() + j); - mtxvec.insert(mtxvec.begin() + (j - 2), tmp1); + tt.insert(tt.begin() + (j - 2), tmp3_tt); + MatrixXi tmp_mtx = mtxvec[j - 2]; + mtxvec.insert(mtxvec.begin() + (j - 2), mtxvec[j - 1]); mtxvec.erase(mtxvec.begin() + (j - 1)); - mtxvec.insert(mtxvec.begin() + (j - 1), tmp2); + mtxvec.insert(mtxvec.begin() + (j - 1), tmp_mtx); mtxvec.erase(mtxvec.begin() + j); - } - if ((tt[j - 2] == tt[j - 1]) && ((tt[j - 2] != "MN") && (tt[j - 2] != "MC") && (tt[j - 2] != "MD") && (tt[j - 2] != "ME") && (tt[j - 2] != "MI") && (tt[j - 2] != "MR") && (tt[j - 2] != "MW"))) - { - MatrixXi temp_mtx(4, 2); - temp_mtx(0, 0) = 1; - temp_mtx(0, 1) = 0; - temp_mtx(1, 0) = 0; - temp_mtx(1, 1) = 0; - temp_mtx(2, 0) = 0; - temp_mtx(2, 1) = 0; - temp_mtx(3, 0) = 0; - temp_mtx(3, 1) = 1; - mtxvec.insert(mtxvec.begin() + (j - 2), temp_mtx); - mtxvec.erase(mtxvec.begin() + (j - 1)); - tt.insert(tt.begin() + (j - 2), "MR"); - tt.erase(tt.begin() + (j - 1)); + mtxvec.insert(mtxvec.begin() + (j - 2), matrix_w2); } } - } - return true; - } - - bool stpm_exchange(MatrixXi &matrix_f, MatrixXi &matrix_b) - { - MatrixXi exchange_matrix; - MatrixXi matrix_i; - exchange_matrix = matrix_b; - MatrixXi matrix_tmp(2, 2); - matrix_tmp(0, 0) = 1; - matrix_tmp(0, 1) = 0; - matrix_tmp(1, 0) = 0; - matrix_tmp(1, 1) = 1; - matrix_i = matrix_tmp; - matrix_b = matrix_f; - matrix_f = stp_kron_product(matrix_i, exchange_matrix); - return true; - } - - bool stp_product_judge(vector &tt, vector &mtxvec) - { - MatrixXi temp0, temp1; - for (int ix = 1; ix < tt.size(); ix++) - { - if ((tt[ix] == "MW") || (tt[ix] == "MN") || (tt[ix] == "MC") || (tt[ix] == "MD") || (tt[ix] == "ME") || (tt[ix] == "MI") || (tt[ix] == "MR") || (tt[ix] == "MM")) - { - temp0 = mtxvec[0]; - temp1 = mtxvec[ix]; - mtxvec[0] = stpm_basic_product(temp0, temp1); + if (((tt[j - 2] != "MN") && (tt[j - 2] != "MC") && + (tt[j - 2] != "MD") && (tt[j - 2] != "ME") && + (tt[j - 2] != "MI") && (tt[j - 2] != "MR") && + (tt[j - 2] != "MW")) && + ((tt[j - 1] == "MN") || (tt[j - 1] == "MC") || + (tt[j - 1] == "MD") || (tt[j - 1] == "ME") || + (tt[j - 1] == "MI") || (tt[j - 1] == "MR") || + (tt[j - 1] == "MW"))) { + MatrixXi tmp1; + tmp1 = mtxvec[j - 2]; + MatrixXi tmp2; + tmp2 = mtxvec[j - 1]; + stpm_exchange(tmp1, tmp2); + string tmp_tt = tt[j - 2]; + tt.insert(tt.begin() + (j - 2), tt[j - 1]); + tt.erase(tt.begin() + (j - 1)); + tt.insert(tt.begin() + (j - 1), tmp_tt); + tt.erase(tt.begin() + j); + mtxvec.insert(mtxvec.begin() + (j - 2), tmp1); + mtxvec.erase(mtxvec.begin() + (j - 1)); + mtxvec.insert(mtxvec.begin() + (j - 1), tmp2); + mtxvec.erase(mtxvec.begin() + j); } - } - return true; - } - - MatrixXi stpm_basic_product(MatrixXi matrix_f, MatrixXi matrix_b) - { - int z; - MatrixXi result_matrix; - int n_col = matrix_f.cols(); - int p_row = matrix_b.rows(); - if (n_col % p_row == 0) - { - z = n_col / p_row; - MatrixXi matrix_i1; - matrix_i1 = MatrixXi::eye(z); - MatrixXi temp = stp_kron_product(matrix_b, matrix_i1); - result_matrix = MatrixXi::product(matrix_f, temp); - } - else if (p_row % n_col == 0) - { - z = p_row / n_col; - MatrixXi matrix_i2; - matrix_i2 = MatrixXi::eye(z); - MatrixXi temp = stp_kron_product(matrix_f, matrix_i2); - result_matrix = MatrixXi::product(temp, matrix_b); - } - return result_matrix; - } - - MatrixXi stp_kron_product(MatrixXi matrix_f, MatrixXi matrix_b) - { - int m = matrix_f.rows(); - int n = matrix_f.cols(); - int p = matrix_b.rows(); - int q = matrix_b.cols(); - MatrixXi dynamic_matrix(m * p, n * q); - for (int i = 0; i < m * p; i++) - { - for (int j = 0; j < n * q; j++) - { - dynamic_matrix(i, j) = matrix_f(i / p, j / q) * matrix_b(i % p, j % q); - } - } - return dynamic_matrix; - } - - void stp_result_enumeration(vector &mtxvec, int &target, string &stp_result) - { - int target_tmp; - int n = mtxvec[0].cols(); - target_tmp = target; - if (n == 4) - { - for (int j = 0; j < n; j++) - { - if (mtxvec[0](0, j) == target_tmp) - { - if (j < 2) - { - string tmp = "1"; - stp_result += tmp; - if (j < 1) - { - target = 1; - if (mtxvec.size() > 1) - { - vector temp; - temp.assign(mtxvec.begin() + 1, mtxvec.end()); - stp_result_enumeration(temp, target, stp_result); - } - if (mtxvec.size() == 1) - { - string tmp = "1"; - stp_result += tmp; - string tmp1 = "\n"; - stp_result += tmp1; - } - } - if (j >= 1) - { - target = 0; - if (mtxvec.size() > 1) - { - vector temp; - temp.assign(mtxvec.begin() + 1, mtxvec.end()); - stp_result_enumeration(temp, target, stp_result); - } - if (mtxvec.size() == 1) - { - string tmp = "0"; - stp_result += tmp; - string tmp1 = "\n"; - stp_result += tmp1; - } - } - } - if (j >= 2) - { - string tmp = "0"; - stp_result += tmp; - if (j < ((3 * n) / 4)) - { - target = 1; - if (mtxvec.size() > 1) - { - vector temp; - temp.assign(mtxvec.begin() + 1, mtxvec.end()); - stp_result_enumeration(temp, target, stp_result); - } - if (mtxvec.size() == 1) - { - string tmp = "1"; - stp_result += tmp; - string tmp1 = "\n"; - stp_result += tmp1; - } - } - if (j >= 3) - { - target = 0; - if (mtxvec.size() > 1) - { - vector temp; - temp.assign(mtxvec.begin() + 1, mtxvec.end()); - stp_result_enumeration(temp, target, stp_result); - } - if (mtxvec.size() == 1) - { - string tmp = "0"; - stp_result += tmp; - string tmp1 = "\n"; - stp_result += tmp1; - } - } - } - } - } - } - else if (n == 2) - { - for (int j = 0; j < n; j++) - { - if (mtxvec[0](0, j) == target_tmp) - { - if (j < 1) - { - string tmp = "1"; - stp_result += tmp; - string tmp1 = "\n"; - stp_result += tmp1; - } - if (j >= 1) - { - string tmp = "0"; - stp_result += tmp; - string tmp1 = "\n"; - stp_result += tmp1; - } - } + if ((tt[j - 2] == tt[j - 1]) && + ((tt[j - 2] != "MN") && (tt[j - 2] != "MC") && + (tt[j - 2] != "MD") && (tt[j - 2] != "ME") && + (tt[j - 2] != "MI") && (tt[j - 2] != "MR") && + (tt[j - 2] != "MW"))) { + MatrixXi temp_mtx(4, 2); + temp_mtx(0, 0) = 1; + temp_mtx(0, 1) = 0; + temp_mtx(1, 0) = 0; + temp_mtx(1, 1) = 0; + temp_mtx(2, 0) = 0; + temp_mtx(2, 1) = 0; + temp_mtx(3, 0) = 0; + temp_mtx(3, 1) = 1; + mtxvec.insert(mtxvec.begin() + (j - 2), temp_mtx); + mtxvec.erase(mtxvec.begin() + (j - 1)); + tt.insert(tt.begin() + (j - 2), "MR"); + tt.erase(tt.begin() + (j - 1)); } } } - - private: - vector &expression; - vector &tt; - vector &mtxvec; - }; - - void cdccl_for_all(vector &in, vector> &mtxvec) - { - stp_cdccl_impl p(in, mtxvec); - p.run_normal(); + return true; } - void cdccl_for_single_po(vector &in, vector> &mtxvec, int &po) - { - stp_cdccl_impl2 p2(in, mtxvec, po); - p2.run_single_po(); + bool stpm_exchange(MatrixXi &matrix_f, MatrixXi &matrix_b) { + MatrixXi exchange_matrix; + MatrixXi matrix_i; + exchange_matrix = matrix_b; + MatrixXi matrix_tmp(2, 2); + matrix_tmp(0, 0) = 1; + matrix_tmp(0, 1) = 0; + matrix_tmp(1, 0) = 0; + matrix_tmp(1, 1) = 1; + matrix_i = matrix_tmp; + matrix_b = matrix_f; + matrix_f = stp_kron_product(matrix_i, exchange_matrix); + return true; } - void stp_cnf(vector &expression, vector &tt, vector &mtxvec) - { - stp_cnf_impl p3(expression, tt, mtxvec); - p3.run_cnf(); + bool stp_product_judge(vector &tt, vector &mtxvec) { + MatrixXi temp0, temp1; + for (int ix = 1; ix < tt.size(); ix++) { + if ((tt[ix] == "MW") || (tt[ix] == "MN") || (tt[ix] == "MC") || + (tt[ix] == "MD") || (tt[ix] == "ME") || (tt[ix] == "MI") || + (tt[ix] == "MR") || (tt[ix] == "MM")) { + temp0 = mtxvec[0]; + temp1 = mtxvec[ix]; + mtxvec[0] = stpm_basic_product(temp0, temp1); + } + } + return true; } + + MatrixXi stpm_basic_product(MatrixXi matrix_f, MatrixXi matrix_b) { + int z; + MatrixXi result_matrix; + int n_col = matrix_f.cols(); + int p_row = matrix_b.rows(); + if (n_col % p_row == 0) { + z = n_col / p_row; + MatrixXi matrix_i1; + matrix_i1 = MatrixXi::eye(z); + MatrixXi temp = stp_kron_product(matrix_b, matrix_i1); + result_matrix = MatrixXi::product(matrix_f, temp); + } else if (p_row % n_col == 0) { + z = p_row / n_col; + MatrixXi matrix_i2; + matrix_i2 = MatrixXi::eye(z); + MatrixXi temp = stp_kron_product(matrix_f, matrix_i2); + result_matrix = MatrixXi::product(temp, matrix_b); + } + return result_matrix; + } + + MatrixXi stp_kron_product(MatrixXi matrix_f, MatrixXi matrix_b) { + int m = matrix_f.rows(); + int n = matrix_f.cols(); + int p = matrix_b.rows(); + int q = matrix_b.cols(); + MatrixXi dynamic_matrix(m * p, n * q); + for (int i = 0; i < m * p; i++) { + for (int j = 0; j < n * q; j++) { + dynamic_matrix(i, j) = matrix_f(i / p, j / q) * matrix_b(i % p, j % q); + } + } + return dynamic_matrix; + } + + void stp_result_enumeration(vector &mtxvec, int &target, + string &stp_result) { + int target_tmp; + int n = mtxvec[0].cols(); + target_tmp = target; + if (n == 4) { + for (int j = 0; j < n; j++) { + if (mtxvec[0](0, j) == target_tmp) { + if (j < 2) { + string tmp = "1"; + stp_result += tmp; + if (j < 1) { + target = 1; + if (mtxvec.size() > 1) { + vector temp; + temp.assign(mtxvec.begin() + 1, mtxvec.end()); + stp_result_enumeration(temp, target, stp_result); + } + if (mtxvec.size() == 1) { + string tmp = "1"; + stp_result += tmp; + string tmp1 = "\n"; + stp_result += tmp1; + } + } + if (j >= 1) { + target = 0; + if (mtxvec.size() > 1) { + vector temp; + temp.assign(mtxvec.begin() + 1, mtxvec.end()); + stp_result_enumeration(temp, target, stp_result); + } + if (mtxvec.size() == 1) { + string tmp = "0"; + stp_result += tmp; + string tmp1 = "\n"; + stp_result += tmp1; + } + } + } + if (j >= 2) { + string tmp = "0"; + stp_result += tmp; + if (j < ((3 * n) / 4)) { + target = 1; + if (mtxvec.size() > 1) { + vector temp; + temp.assign(mtxvec.begin() + 1, mtxvec.end()); + stp_result_enumeration(temp, target, stp_result); + } + if (mtxvec.size() == 1) { + string tmp = "1"; + stp_result += tmp; + string tmp1 = "\n"; + stp_result += tmp1; + } + } + if (j >= 3) { + target = 0; + if (mtxvec.size() > 1) { + vector temp; + temp.assign(mtxvec.begin() + 1, mtxvec.end()); + stp_result_enumeration(temp, target, stp_result); + } + if (mtxvec.size() == 1) { + string tmp = "0"; + stp_result += tmp; + string tmp1 = "\n"; + stp_result += tmp1; + } + } + } + } + } + } else if (n == 2) { + for (int j = 0; j < n; j++) { + if (mtxvec[0](0, j) == target_tmp) { + if (j < 1) { + string tmp = "1"; + stp_result += tmp; + string tmp1 = "\n"; + stp_result += tmp1; + } + if (j >= 1) { + string tmp = "0"; + stp_result += tmp; + string tmp1 = "\n"; + stp_result += tmp1; + } + } + } + } + } + + private: + vector &expression; + vector &tt; + vector &mtxvec; +}; + +void cdccl_for_all(vector &in, vector> &mtxvec) { + stp_cdccl_impl p(in, mtxvec); + p.run_normal(); } + +void cdccl_for_single_po(vector &in, vector> &mtxvec, + int &po) { + stp_cdccl_impl2 p2(in, mtxvec, po); + p2.run_single_po(); +} + +void stp_cnf(vector &expression, vector &tt, + vector &mtxvec) { + stp_cnf_impl p3(expression, tt, mtxvec); + p3.run_cnf(); +} +} // namespace phyLS diff --git a/src/mcnc.genlib b/src/mcnc.genlib new file mode 100644 index 0000000..e5724b6 --- /dev/null +++ b/src/mcnc.genlib @@ -0,0 +1,26 @@ +GATE _const0_ 0.00 z=CONST0; +GATE _const1_ 0.00 z=CONST1; +GATE inv1 1 O=!a; PIN * INV 1 999 0.9 0.3 0.9 0.3 +GATE inv2 2 O=!a; PIN * INV 2 999 1.0 0.1 1.0 0.1 +GATE inv3 3 O=!a; PIN * INV 3 999 1.1 0.09 1.1 0.09 +GATE inv4 4 O=!a; PIN * INV 4 999 1.2 0.07 1.2 0.07 +GATE nand2 2 O=!(a*b); PIN * INV 1 999 1.0 0.2 1.0 0.2 +GATE nand3 3 O=!(a*b*c); PIN * INV 1 999 1.1 0.3 1.1 0.3 +GATE nand4 4 O=!(a*b*c*d); PIN * INV 1 999 1.4 0.4 1.4 0.4 +GATE nor2 2 O=!(a+b); PIN * INV 1 999 1.4 0.5 1.4 0.5 +GATE nor3 3 O=!(a+b+c); PIN * INV 1 999 2.4 0.7 2.4 0.7 +GATE nor4 4 O=!(a+b+c+d); PIN * INV 1 999 3.8 1.0 3.8 1.0 +GATE and2 3 O=a*b; PIN * NONINV 1 999 1.9 0.3 1.9 0.3 +GATE or2 3 O=a+b; PIN * NONINV 1 999 2.4 0.3 2.4 0.3 +GATE xor2a 5 O=a*!b+!a*b; PIN * UNKNOWN 2 999 1.9 0.5 1.9 0.5 +GATE xor2b 5 O=!(a*b+!a*!b); PIN * UNKNOWN 2 999 1.9 0.5 1.9 0.5 +GATE xnor2a 5 O=a*b+!a*!b; PIN * UNKNOWN 2 999 2.1 0.5 2.1 0.5 +GATE xnor2b 5 O=!(!a*b+a*!b); PIN * UNKNOWN 2 999 2.1 0.5 2.1 0.5 +GATE mig3 3 O=(a*b+a*c+b*c); PIN * INV 1 999 2.0 0.2 2.0 0.2 +GATE xor3 6 O=((a*!b+!a*b)*!c+!(a*!b+!a*b)*c); PIN * INV 1 999 2.0 0.2 2.0 0.2 +GATE aoi21 3 O=!(a*b+c); PIN * INV 1 999 1.6 0.4 1.6 0.4 +GATE aoi22 4 O=!(a*b+c*d); PIN * INV 1 999 2.0 0.4 2.0 0.4 +GATE oai21 3 O=!((a+b)*c); PIN * INV 1 999 1.6 0.4 1.6 0.4 +GATE oai22 4 O=!((a+b)*(c+d)); PIN * INV 1 999 2.0 0.4 2.0 0.4 +GATE buf 1 O=a; PIN * NONINV 1 999 1.0 0.0 1.0 0.0 + diff --git a/src/phyLS.cpp b/src/phyLS.cpp index a7ea551..bf5dfcb 100644 --- a/src/phyLS.cpp +++ b/src/phyLS.cpp @@ -1,5 +1,5 @@ /* phyLS: powerful heightened yielded Logic Synthesis - * Copyright (C) 2022 + * Copyright (C) 2022 * * Permission is hereby granted, free of charge, to any person * obtaining a copy of this software and associated documentation @@ -24,13 +24,16 @@ */ #include "store.hpp" -#include "commands/load.hpp" +#include "commands/balance.hpp" #include "commands/exprsim.hpp" -#include "commands/write_dot.hpp" -#include "commands/techmap.hpp" +#include "commands/load.hpp" #include "commands/lut_mapping.hpp" +#include "commands/node_resynthesis.hpp" +#include "commands/resub.hpp" #include "commands/sim.hpp" #include "commands/stpsat.hpp" +#include "commands/techmap.hpp" +#include "commands/write_dot.hpp" +#include "commands/refactor.hpp" - -ALICE_MAIN( phyLS ) +ALICE_MAIN(phyLS) \ No newline at end of file