Skip to content

Commit

Permalink
fix warnings and trim whitespace
Browse files Browse the repository at this point in the history
  • Loading branch information
tklip committed Nov 30, 2023
1 parent 1a5157a commit 29feec1
Show file tree
Hide file tree
Showing 25 changed files with 326 additions and 394 deletions.
4 changes: 1 addition & 3 deletions cmake/tau-common.cmake
Original file line number Diff line number Diff line change
Expand Up @@ -26,14 +26,12 @@ function(target_setup target)
target_compile_options(${target} PRIVATE
-W -Wall -Wextra -Wpedantic
-Wformat=2
-Wno-variadic-macros
-Wcast-align
-Wstrict-aliasing=2
-Wstrict-overflow=5
-Wfloat-equal
-Wwrite-strings
-Wno-missing-braces
-Wno-parentheses-equality)
)
endif()
target_compile_features(${target} PRIVATE cxx_std_20)
target_git_definitions(${target})
Expand Down
14 changes: 7 additions & 7 deletions src/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -56,9 +56,9 @@ target_link_options(TAUo PRIVATE ${TAU_LINK_OPTIONS})
target_sources(TAUo PRIVATE ${TAU_SOURCES} ${TAU_HEADERS})
target_link_libraries(TAUo ${CMAKE_THREAD_LIBS_INIT})
target_link_libraries(TAUo ${OBJECT_LIB_NAME} idni_parser)
target_include_directories(TAUo PUBLIC
$<BUILD_INTERFACE:${CMAKE_SOURCE_DIR}/parser>
$<BUILD_INTERFACE:${CMAKE_SOURCE_DIR}/external/parser/src>)
target_include_directories(TAUo PUBLIC
$<BUILD_INTERFACE:${CMAKE_SOURCE_DIR}/parser>
$<BUILD_INTERFACE:${CMAKE_SOURCE_DIR}/external/parser/src>)
target_include_directories(TAUo PUBLIC
$<BUILD_INTERFACE:${CMAKE_SOURCE_DIR}>
)
Expand All @@ -73,9 +73,9 @@ target_compile_options(TAUso PRIVATE ${TAU_COMPILE_OPTIONS})
target_link_options(TAUso PRIVATE ${TAU_LINK_OPTIONS})
target_link_libraries(TAUso TAUo)
target_link_libraries(TAUso ${OBJECT_LIB_NAME} idni_parser)
target_include_directories(TAUso PUBLIC
$<BUILD_INTERFACE:${CMAKE_SOURCE_DIR}/parser>
$<BUILD_INTERFACE:${CMAKE_SOURCE_DIR}/external/parser/src>)
target_include_directories(TAUso PUBLIC
$<BUILD_INTERFACE:${CMAKE_SOURCE_DIR}/parser>
$<BUILD_INTERFACE:${CMAKE_SOURCE_DIR}/external/parser/src>)
target_include_directories(TAUso PUBLIC
$<BUILD_INTERFACE:${CMAKE_SOURCE_DIR}>
$<INSTALL_INTERFACE:.>
Expand All @@ -94,7 +94,7 @@ target_setup(TAUs)
target_compile_options(TAUs PRIVATE ${TAU_COMPILE_OPTIONS})
target_link_options(TAUs PRIVATE ${TAU_LINK_OPTIONS})
target_link_libraries(TAUs TAUo)
target_include_directories(TAUs
target_include_directories(TAUs
PUBLIC $<BUILD_INTERFACE:${CMAKE_SOURCE_DIR}>
)
set_target_properties(TAUs PROPERTIES OUTPUT_NAME "TAU")
Expand Down
2 changes: 1 addition & 1 deletion src/anf.h
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ struct anf : set<set<int_t>> {
r.neg = !(neg == x.neg);
return r;
}

anf operator|(const anf& x) const { return x + *this + (*this * x); }

static set<int_t> union_(const set<int_t>& x, const set<int_t>& y) {
Expand Down
14 changes: 9 additions & 5 deletions src/babdd.h
Original file line number Diff line number Diff line change
Expand Up @@ -431,8 +431,10 @@ struct bdd : variant<bdd_node<bdd_reference<o.has_varshift(), o.has_inv_order(),
static bdd_ref add(const bdd_node_t& n) { return add(n.v, n.h, n.l); }

static bdd_ref add(uint_t v, bdd_ref h, bdd_ref l) {
DBG(assert(V.size() < pow(2, o.idW)));
if constexpr (o.has_varshift()) DBG(assert(v < pow(2, o.shiftW)));
#ifdef DEBUG
assert(V.size() < pow(2, o.idW));
if constexpr (o.has_varshift()) assert(v < pow(2, o.shiftW));
#endif
if (h == l) return h;
#ifdef DEBUG
auto p = get(l), q = get(h);
Expand Down Expand Up @@ -678,7 +680,7 @@ struct bdd : variant<bdd_node<bdd_reference<o.has_varshift(), o.has_inv_order(),
if (var_cmp(nx.v, v)) return add(nx.v, sub0(nx.h, v), sub0(nx.l, v));
if (var_cmp(v, nx.v)) return x;
return nx.l;

}

static bdd_ref sub1(bdd_ref x, uint_t v) {
Expand Down Expand Up @@ -954,8 +956,10 @@ struct bdd<Bool, o> : bdd_node<bdd_reference<o.has_varshift(), o.has_inv_order()
static bdd_ref add(bdd_node_t b) { return add(b.v, b.h, b.l); }

static bdd_ref add(uint_t v, bdd_ref h, bdd_ref l) {
DBG(assert(V.size() < pow(2, o.idW)));
if constexpr (o.has_varshift()) DBG(assert(v < pow(2, o.shiftW)));
#ifdef DEBUG
assert(V.size() < pow(2, o.idW));
if constexpr (o.has_varshift()) assert(v < pow(2, o.shiftW));
#endif
if (h == l) return h;
#ifdef DEBUG
if(!leaf(l) && !leaf(h))
Expand Down
4 changes: 2 additions & 2 deletions src/bdd_handle.h
Original file line number Diff line number Diff line change
Expand Up @@ -213,7 +213,7 @@ struct bdd_handle {
return f(v);
});
}

set<pair<B, vector<int_t>>> dnf() const {
set<pair<B, vector<int_t>>> r;
dnf([&r](auto& x) { r.insert(x); return true; });
Expand Down Expand Up @@ -491,7 +491,7 @@ template<typename B, bdd_options o> void create_universe(B a) {
}
}

template<typename B, bdd_options o> void create_universe(Bool a) {
template<typename B, bdd_options o> void create_universe(Bool /*a*/) {
const auto &T = bdd<Bool, o>::T;
const auto &F = bdd<Bool, o>::F;
auto &V = bdd<Bool, o>::V;
Expand Down
16 changes: 8 additions & 8 deletions src/bool.h
Original file line number Diff line number Diff line change
Expand Up @@ -18,19 +18,19 @@ struct Bool {

static const Bool& zero() { static Bool b(false); return b; }
static const Bool& one() { static Bool b(true); return b; }

Bool operator&(const Bool& x) const;
Bool operator|(const Bool& x) const;
Bool operator^(const Bool& x) const;
Bool operator+(const Bool& x) const;
Bool operator~() const;
auto operator<=>(const Bool& x) const = default;
bool is_zero() const {
return !b;

bool is_zero() const {
return !b;
}
bool is_one() const {
return b;
bool is_one() const {
return b;
}

bool b;
Expand All @@ -52,8 +52,8 @@ Bool Bool::operator+(const Bool& x) const {
return (this->b == true) ? ~x : x;
}

Bool Bool::operator~() const {
return (this->b == true) ? zero() : one();
Bool Bool::operator~() const {
return (this->b == true) ? zero() : one();
}

#endif
3 changes: 2 additions & 1 deletion src/defs.h
Original file line number Diff line number Diff line change
Expand Up @@ -16,10 +16,11 @@

typedef int sym_t;

// toggles for debugging, comment properly to enable/disable each feature/debug helper.
// toggles for debugging, comment properly to enable/disable each feature/debug helper.

// TODO (LOW) final features should be cotrolled by a command line flag

#undef OUTPUT_APPLY_RULES
#define OUTPUT_APPLY_RULES
#define OUTPUT_PARSED_TREES

Expand Down
7 changes: 3 additions & 4 deletions src/formula.h
Original file line number Diff line number Diff line change
Expand Up @@ -580,8 +580,8 @@ struct stringify {
return n;
}

const extractor_t& extractor;
std::basic_stringstream<char>& stream;
const extractor_t& extractor;
};

// converts a sp_tau_node<...> to a string skipping the nodes that satisfy the
Expand Down Expand Up @@ -795,7 +795,7 @@ tau_rule<BAs...> make_rule(sp_tau_node<BAs...>& rule) {
switch (type) {
case tau_parser::bf_rule: return make_rule<tau_parser::bf_rule, tau_parser::bf_matcher, tau_parser::bf_body, BAs...>(rule);
case tau_parser::wff_rule: return make_rule<tau_parser::wff_rule, tau_parser::wff_matcher, tau_parser::wff_body, BAs...>(rule);
default: assert(false);
default: assert(false); return {};
};
}

Expand Down Expand Up @@ -924,7 +924,7 @@ template<typename... BAs>
sp_tau_node<BAs...> tau_apply_builder(const builder<BAs...>& b, std::vector<sp_tau_node<BAs...>>& n) {
std::map<sp_tau_node<BAs...>, sp_tau_node<BAs...>> changes;
std::vector<sp_tau_node<BAs...>> vars = b.first || tau_parser::capture;
for (int i = 0; i < vars.size(); ++i) changes[vars[i]] = n[i];
for (size_t i = 0; i < vars.size(); ++i) changes[vars[i]] = n[i];
return replace<sp_tau_node<BAs...>>(b.second, changes);
}

Expand Down Expand Up @@ -1435,7 +1435,6 @@ sp_tau_node<BAs...> tau_apply(const rules<BAs...>& rs, const sp_tau_node<BAs...>

// TODO (HIGH) << for tau_source_sym
// TODO (HIGH) << for tau_source_node
// TODO (HIGH) << for tau_source_node
// TODO (HIGH) << for sp_tau_source_node
// TODO (HIGH) << for tau_sym
// TODO (HIGH) << for sp_tau_node
Expand Down
6 changes: 3 additions & 3 deletions src/main.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -23,15 +23,15 @@ using namespace idni::tau;

// We could use TODO (HIGH|MEDIUM|LOW|nothing), DOING, IDEA, FIXME, REVIEW and MARK.

// TODO (IMPORTANT) deal with runtime errors in the code.
// TODO (IMPORTANT) deal with runtime errors in the code.
// For example, if the user provides a formula with errors, we should not continue
// and print garbage. Instead, we should print an error message and exit.

// TODO (MEDIUM) declare a static const lambda instead of a predicates if possible
//
// This could be done in all the code.
// This could be done in all the code.

int main(int argc, char** argv) {
int main(int /*argc*/, char** /*argv*/) {
// TODO (LOW) tau main method, parse command line arguments, read input file,...
// normalize, print output, etc.
return 0;
Expand Down
2 changes: 1 addition & 1 deletion src/normalizer.h
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ struct normalizer<tuple<BDDs...>, aux...> {
for (const auto& x : pos) p = (p | x);
msba_t r(true, p);
hbdd<B, o> np = ~p;
if (!(p->get_uelim() == false)) return msba_t(false);
if (!(p->get_uelim() == false)) return msba_t(false);
auto t = p->lgrs();
for (const hbdd<B, o>& x : neg) {
hbdd<B, o> z = x->compose(t) & np;
Expand Down
Loading

0 comments on commit 29feec1

Please sign in to comment.