Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add <lit_type> to std::vector #4

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Add <lit_type> to std::vector #4

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
2787c49
Modify files to make it compile on W10
Nick-Liou May 11, 2024
677ced8
Update README.md to triger workflows
Nick-Liou May 12, 2024
018efcd
Merge branch 'hriener:master' into master
Nick-Liou May 18, 2024
b5a6100
Update actions/checkout@v1 to v4, to use Node.js 20
Nick-Liou May 18, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/coveralls.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ jobs:
name: GNU GCC 9 and run coveralls

steps:
- uses: actions/checkout@v1
- uses: actions/checkout@v4
with:
submodules: true
- name: Build easy
Expand Down
10 changes: 5 additions & 5 deletions .github/workflows/linux.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ jobs:
name: GNU GCC 9

steps:
- uses: actions/checkout@v1
- uses: actions/checkout@v4
with:
submodules: true
- name: Build mockturtle
Expand All @@ -32,7 +32,7 @@ jobs:
name: GNU GCC 10

steps:
- uses: actions/checkout@v1
- uses: actions/checkout@v4
with:
submodules: true
- name: Build mockturtle
Expand All @@ -50,7 +50,7 @@ jobs:
name: GNU GCC 12

steps:
- uses: actions/checkout@v1
- uses: actions/checkout@v4
with:
submodules: true
- name: Build mockturtle
Expand All @@ -68,7 +68,7 @@ jobs:
name: Clang 11

steps:
- uses: actions/checkout@v1
- uses: actions/checkout@v4
with:
submodules: true
- name: Build mockturtle
Expand All @@ -86,7 +86,7 @@ jobs:
name: Clang 13

steps:
- uses: actions/checkout@v1
- uses: actions/checkout@v4
with:
submodules: true
- name: Build mockturtle
Expand Down
10 changes: 5 additions & 5 deletions .github/workflows/macos.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ jobs:
runs-on: macOS-11

steps:
- uses: actions/checkout@v1
- uses: actions/checkout@v4
with:
submodules: true
- name: Build
Expand All @@ -32,7 +32,7 @@ jobs:
runs-on: macOS-latest

steps:
- uses: actions/checkout@v1
- uses: actions/checkout@v4
with:
submodules: true
- name: Build easy
Expand All @@ -50,7 +50,7 @@ jobs:
runs-on: macOS-latest

steps:
- uses: actions/checkout@v1
- uses: actions/checkout@v4
with:
submodules: true
- name: Build easy
Expand All @@ -68,7 +68,7 @@ jobs:
runs-on: macOS-latest

steps:
- uses: actions/checkout@v1
- uses: actions/checkout@v4
with:
submodules: true
- name: Build easy
Expand All @@ -86,7 +86,7 @@ jobs:
runs-on: macOS-latest

steps:
- uses: actions/checkout@v1
- uses: actions/checkout@v4
with:
submodules: true
- name: Build easy
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/windows.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ jobs:
runs-on: ${{matrix.os}}

steps:
- uses: actions/checkout@v1
- uses: actions/checkout@v4
with:
submodules: true
- name: Create build directory
Expand Down
2 changes: 1 addition & 1 deletion README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
[![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT)

# easy

<img src="https://cdn.rawgit.com/hriener/easy/master/easy.svg" width="64" height="64" align="left" style="margin-right: 12pt" />
easy is a C++ library for verification and synthesis of exclusive-or sum-of-product (ESOP) forms.

Expand Down
2 changes: 1 addition & 1 deletion include/easy/esop/helliwell.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ namespace detail

inline int32_t get_lowest_set_bit( int32_t num )
{
#if WIN32
#if defined(WIN32)
uint32_t mask = 1;
for ( int32_t counter = 1; counter <= 32; counter++, mask <<= 1 )
{
Expand Down
12 changes: 6 additions & 6 deletions lib/bill/bill/include/bill/sat/incremental_totalizer_cardinality.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,20 +34,20 @@ inline void create_totalizer_internal(Solver& solver, std::vector<std::vector<li
/* i = 0 */
uint32_t kmin = std::min(rhs, uint32_t(bv.size()));
for (auto j = 0u; j < kmin; ++j) {
dest.emplace_back(std::vector{~bv[j], ov[j]});
dest.emplace_back(std::vector<lit_type>{~bv[j], ov[j]});
}

/* j = 0 */
kmin = std::min(rhs, uint32_t(av.size()));
for (auto i = 0u; i < kmin; ++i) {
dest.emplace_back(std::vector{~av[i], ov[i]});
dest.emplace_back(std::vector<lit_type>{~av[i], ov[i]});
}

/* i, j > 0 */
for (auto i = 1u; i <= kmin; ++i) {
auto const min_j = std::min(rhs - i, uint32_t(bv.size()));
for (auto j = 1u; j <= min_j; ++j) {
dest.emplace_back(std::vector{~av[i - 1], ~bv[j - 1], ov[i + j - 1]});
dest.emplace_back(std::vector<lit_type>{~av[i - 1], ~bv[j - 1], ov[i + j - 1]});
}
}
}
Expand All @@ -66,21 +66,21 @@ inline void increase_totalizer_internal(Solver& solver, std::vector<std::vector<
/* i = 0 */
uint32_t const max_j = std::min(rhs, uint32_t(bv.size()));
for (auto j = last; j < max_j; ++j) {
dest.emplace_back(std::vector{~bv[j], ov[j]});
dest.emplace_back(std::vector<lit_type>{~bv[j], ov[j]});
}

/* j = 0 */
uint32_t const max_i = std::min(rhs, uint32_t(av.size()));
for (auto i = last; i < max_i; ++i) {
dest.emplace_back(std::vector{~av[i], ov[i]});
dest.emplace_back(std::vector<lit_type>{~av[i], ov[i]});
}

/* i, j > 0 */
for (auto i = 1u; i <= max_i; ++i) {
auto const max_j = std::min(rhs - i, uint32_t(bv.size()));
auto const min_j = uint32_t(std::max(int(last) - int(i) + 1, 1));
for (auto j = min_j; j <= max_j; ++j) {
dest.emplace_back(std::vector{~av[i - 1], ~bv[j - 1], ov[i + j - 1]});
dest.emplace_back(std::vector<lit_type>{~av[i - 1], ~bv[j - 1], ov[i + j - 1]});
}
}
}
Expand Down
32 changes: 16 additions & 16 deletions lib/bill/bill/include/bill/sat/tseytin.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,9 +20,9 @@ template<typename Solver>
lit_type add_tseytin_and(Solver& solver, lit_type const& a, lit_type const& b)
{
auto const r = solver.add_variable();
solver.add_clause(std::vector{~a, ~b, lit_type(r, lit_type::polarities::positive)});
solver.add_clause(std::vector{a, lit_type(r, lit_type::polarities::negative)});
solver.add_clause(std::vector{b, lit_type(r, lit_type::polarities::negative)});
solver.add_clause(std::vector<lit_type>{~a, ~b, lit_type(r, lit_type::polarities::positive)});
solver.add_clause(std::vector<lit_type>{a, lit_type(r, lit_type::polarities::negative)});
solver.add_clause(std::vector<lit_type>{b, lit_type(r, lit_type::polarities::negative)});
return lit_type(r, lit_type::polarities::positive);
}

Expand All @@ -42,7 +42,7 @@ lit_type add_tseytin_and(Solver& solver, std::vector<lit_type> const& ls)
cls.emplace_back(lit_type(r, lit_type::polarities::positive));
solver.add_clause(cls);
for (const auto& l : ls)
solver.add_clause(std::vector{l, lit_type(r, lit_type::polarities::negative)});
solver.add_clause(std::vector<lit_type>{l, lit_type(r, lit_type::polarities::negative)});
return lit_type(r, lit_type::polarities::positive);
}

Expand All @@ -57,9 +57,9 @@ template<typename Solver>
lit_type add_tseytin_or(Solver& solver, lit_type const& a, lit_type const& b)
{
auto const r = solver.add_variable();
solver.add_clause(std::vector{a, b, lit_type(r, lit_type::polarities::negative)});
solver.add_clause(std::vector{~a, lit_type(r, lit_type::polarities::positive)});
solver.add_clause(std::vector{~b, lit_type(r, lit_type::polarities::positive)});
solver.add_clause(std::vector<lit_type>{a, b, lit_type(r, lit_type::polarities::negative)});
solver.add_clause(std::vector<lit_type>{~a, lit_type(r, lit_type::polarities::positive)});
solver.add_clause(std::vector<lit_type>{~b, lit_type(r, lit_type::polarities::positive)});
return lit_type(r, lit_type::polarities::positive);
}

Expand All @@ -77,7 +77,7 @@ lit_type add_tseytin_or(Solver& solver, std::vector<lit_type> const& ls)
cls.emplace_back(lit_type(r, lit_type::polarities::negative));
solver.add_clause(cls);
for (const auto& l : ls)
solver.add_clause(std::vector{~l, lit_type(r, lit_type::polarities::positive)});
solver.add_clause(std::vector<lit_type>{~l, lit_type(r, lit_type::polarities::positive)});
return lit_type(r, lit_type::polarities::positive);
}

Expand All @@ -92,10 +92,10 @@ template<typename Solver>
lit_type add_tseytin_xor(Solver& solver, lit_type const& a, lit_type const& b)
{
auto const r = solver.add_variable();
solver.add_clause(std::vector{~a, ~b, lit_type(r, lit_type::polarities::negative)});
solver.add_clause(std::vector{~a, b, lit_type(r, lit_type::polarities::positive)});
solver.add_clause(std::vector{a, ~b, lit_type(r, lit_type::polarities::positive)});
solver.add_clause(std::vector{a, b, lit_type(r, lit_type::polarities::negative)});
solver.add_clause(std::vector<lit_type>{~a, ~b, lit_type(r, lit_type::polarities::negative)});
solver.add_clause(std::vector<lit_type>{~a, b, lit_type(r, lit_type::polarities::positive)});
solver.add_clause(std::vector<lit_type>{a, ~b, lit_type(r, lit_type::polarities::positive)});
solver.add_clause(std::vector<lit_type>{a, b, lit_type(r, lit_type::polarities::negative)});
return lit_type(r, lit_type::polarities::positive);
}

Expand All @@ -110,10 +110,10 @@ template<typename Solver>
lit_type add_tseytin_equals(Solver& solver, lit_type const& a, lit_type const& b)
{
auto const r = solver.add_variable();
solver.add_clause(std::vector{~a, ~b, lit_type(r, lit_type::polarities::positive)});
solver.add_clause(std::vector{~a, b, lit_type(r, lit_type::polarities::negative)});
solver.add_clause(std::vector{a, ~b, lit_type(r, lit_type::polarities::negative)});
solver.add_clause(std::vector{a, b, lit_type(r, lit_type::polarities::positive)});
solver.add_clause(std::vector<lit_type>{~a, ~b, lit_type(r, lit_type::polarities::positive)});
solver.add_clause(std::vector<lit_type>{~a, b, lit_type(r, lit_type::polarities::negative)});
solver.add_clause(std::vector<lit_type>{a, ~b, lit_type(r, lit_type::polarities::negative)});
solver.add_clause(std::vector<lit_type>{a, b, lit_type(r, lit_type::polarities::positive)});
return lit_type(r, lit_type::polarities::positive);
}

Expand Down
Loading