diff --git a/src/trans-netlist/aig.h b/src/trans-netlist/aig.h index 51f1048a5..1a2593b1e 100644 --- a/src/trans-netlist/aig.h +++ b/src/trans-netlist/aig.h @@ -22,18 +22,30 @@ class aig_nodet { public: literalt a, b; - aig_nodet() {} + explicit aig_nodet(literalt::var_not var_no) + : a{literalt::unused_var_no(), false}, b{var_no, false} + { + } - bool is_and() const { return a.var_no() != literalt::unused_var_no(); } + aig_nodet(literalt _a, literalt _b) : a(_a), b(_b) + { + } - bool is_var() const { return a.var_no() == literalt::unused_var_no(); } + bool is_and() const + { + return a.var_no() != literalt::unused_var_no(); + } - void make_and(literalt _a, literalt _b) { - a = _a; - b = _b; + bool is_var() const + { + return a.var_no() == literalt::unused_var_no(); } - void make_var() { a.set(literalt::unused_var_no(), false); } + literalt::var_not var_no() const + { + PRECONDITION(is_var()); + return b.var_no(); + } }; class aigt { @@ -56,23 +68,15 @@ class aigt { void swap(aigt &g) { nodes.swap(g.nodes); } - literalt new_node() { - nodes.push_back(aig_nodet()); - literalt l; - l.set(nodes.size() - 1, false); - return l; - } - - literalt new_var_node() { - literalt l = new_node(); - nodes.back().make_var(); - return l; + literalt new_var_node(literalt::var_not var_no = literalt::unused_var_no()) + { + nodes.emplace_back(var_no); + return {narrow_cast(nodes.size() - 1), false}; } literalt new_and_node(literalt a, literalt b) { - literalt l = new_node(); - nodes.back().make_and(a, b); - return l; + nodes.emplace_back(a, b); + return {narrow_cast(nodes.size() - 1), false}; } bool empty() const { return nodes.empty(); } diff --git a/src/trans-netlist/aig_prop.h b/src/trans-netlist/aig_prop.h index 1d18be4d3..cc2aa4949 100644 --- a/src/trans-netlist/aig_prop.h +++ b/src/trans-netlist/aig_prop.h @@ -46,7 +46,10 @@ class aig_prop_baset : public propt { PRECONDITION(false); } - literalt new_variable() override { return dest.new_node(); } + literalt new_variable() override + { + return dest.new_var_node(); + } size_t no_variables() const override { return dest.number_of_nodes(); }