Skip to content

Commit

Permalink
ports & fixed two issues
Browse files Browse the repository at this point in the history
fixed gcc9, vc++2019, and cygwin issues (also colored script output)
./configure --check --quiet fix (was not tested by ./scripts/build-...)
fixed write_dimacs to call restore_clauses
  • Loading branch information
Armin Biere committed Jun 11, 2020
1 parent 45029f8 commit 0b7a2b5
Show file tree
Hide file tree
Showing 16 changed files with 208 additions and 176 deletions.
2 changes: 1 addition & 1 deletion VERSION
Original file line number Diff line number Diff line change
@@ -1 +1 @@
sc2020
1.3.0
4 changes: 2 additions & 2 deletions configure
Original file line number Diff line number Diff line change
Expand Up @@ -51,12 +51,12 @@ die () {
else
checklog=""
fi
echo "${BOLD}configure:${NORMAL} ${BAD}error:${NORMAL} $*${checklog}"
cecho "${BOLD}configure:${NORMAL} ${BAD}error:${NORMAL} $*${checklog}"
exit 1
}

msg () {
echo "${BOLD}configure:${NORMAL} $*"
cecho "${BOLD}configure:${NORMAL} $*"
}

# if we can find the 'color.sh' script source it and overwrite color codes
Expand Down
4 changes: 4 additions & 0 deletions scripts/build-and-test-all-configurations.sh
Original file line number Diff line number Diff line change
Expand Up @@ -92,12 +92,16 @@ run -l -p
# ('-g' can not be combined '-c')

run -c -l
run -c -q
run -g -l
run -g -q

# the same pairs but now with pedantic compilation

run -c -l -p
run -c -q -p
run -g -l -p
run -g -q -p

# finally check that these also work to some extend

Expand Down
23 changes: 17 additions & 6 deletions scripts/colors.sh
100755 → 100644
Original file line number Diff line number Diff line change
@@ -1,13 +1,20 @@
# Use colors if '<stdin>' is connected to a terminal.

color_echo_options=""

if [ -t 1 ]
then
BAD="\033[1;31m" # bright red
HILITE="\033[32m" # normal green
GOOD="\033[1;32m" # bright green
HIDE="\033[34m" # cyan
BOLD="\033[1m" # bold color
NORMAL="\033[0m" # normal color
BAD="\033[1;31m" # bright red
HILITE="\033[32m" # normal green
GOOD="\033[1;32m" # bright green
HIDE="\033[34m" # cyan
BOLD="\033[1m" # bold color
NORMAL="\033[0m" # normal color

if [ x"`echo -e 2>/dev/null`" = x ]
then
color_echo_options=" -e"
fi
else
BAD=""
HILITE=""
Expand All @@ -16,3 +23,7 @@ else
BOLD=""
NORMAL=""
fi

cecho () {
echo$color_echo_options $*
}
11 changes: 6 additions & 5 deletions src/profile.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -67,12 +67,13 @@ void Internal::print_profile () {
#define PROFILE(NAME,LEVEL) \
do { \
if (LEVEL > opts.profile) break; \
if (&profiles.NAME == &profiles.solve) break; \
Profile * p = &profiles.NAME; \
if (p == &profiles.solve) break; \
if (!profiles.NAME.value && \
&profiles.NAME != &profiles.parse && \
&profiles.NAME != &profiles.search && \
&profiles.NAME != &profiles.simplify) break; \
profs[n++] = &profiles.NAME; \
p != &profiles.parse && \
p != &profiles.search && \
p != &profiles.simplify) break; \
profs[n++] = p; \
} while (0);
PROFILES
#undef PROFILE
Expand Down
144 changes: 77 additions & 67 deletions src/profile.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -104,41 +104,59 @@ struct Profiles {

}

#define NON_QUIET_PROFILE_CODE(CODE) CODE

#else // !defined(QUIET)

#define NON_QUIET_PROFILE_CODE(CODE) /**/

#endif

/*------------------------------------------------------------------------*/

// Macros for Profiling support.
// Macros for Profiling support and checking and changing the mode.

#define START(P) \
do { \
if (internal->profiles.P.level > internal->opts.profile) break; \
internal->start_profiling (internal->profiles.P, internal->time ()); \
NON_QUIET_PROFILE_CODE ( \
if (internal->profiles.P.level <= internal->opts.profile) \
internal->start_profiling (internal->profiles.P, internal->time ()); \
) \
} while (0)

#define STOP(P) \
do { \
if (internal->profiles.P.level > internal->opts.profile) break; \
internal->stop_profiling (internal->profiles.P, internal->time ()); \
NON_QUIET_PROFILE_CODE ( \
if (internal->profiles.P.level <= internal->opts.profile) \
internal->stop_profiling (internal->profiles.P, internal->time ()); \
) \
} while (0)

/*------------------------------------------------------------------------*/

#define START_SIMPLIFIER(S,M) \
do { \
const double N = time (); \
const int L = internal->opts.profile; \
NON_QUIET_PROFILE_CODE ( \
const double N = time (); \
const int L = internal->opts.profile; \
) \
if (!preprocessing && !lookingahead) { \
if (stable && internal->profiles.stable.level <= L) \
internal->stop_profiling (internal->profiles.stable, N); \
if (!stable && internal->profiles.unstable.level <= L) \
internal->stop_profiling (internal->profiles.unstable, N); \
if (internal->profiles.search.level <= L) \
internal->stop_profiling (internal->profiles.search, N); \
NON_QUIET_PROFILE_CODE ( \
if (stable && internal->profiles.stable.level <= L) \
internal->stop_profiling (internal->profiles.stable, N); \
if (!stable && internal->profiles.unstable.level <= L) \
internal->stop_profiling (internal->profiles.unstable, N); \
if (internal->profiles.search.level <= L) \
internal->stop_profiling (internal->profiles.search, N); \
) \
reset_mode (SEARCH); \
} \
if (internal->profiles.simplify.level <= L) \
internal->start_profiling (internal->profiles.simplify, N); \
if (internal->profiles.S.level <= L) \
internal->start_profiling (internal->profiles.S, N); \
NON_QUIET_PROFILE_CODE ( \
if (internal->profiles.simplify.level <= L) \
internal->start_profiling (internal->profiles.simplify, N); \
if (internal->profiles.S.level <= L) \
internal->start_profiling (internal->profiles.S, N); \
) \
set_mode (SIMPLIFY); \
set_mode (M); \
} while (0)
Expand All @@ -147,21 +165,25 @@ do { \

#define STOP_SIMPLIFIER(S,M) \
do { \
const double N = time (); \
const int L = internal->opts.profile; \
if (internal->profiles.S.level <= L) \
internal->stop_profiling (internal->profiles.S, N); \
if (internal->profiles.simplify.level <= L) \
internal->stop_profiling (internal->profiles.simplify, N); \
NON_QUIET_PROFILE_CODE ( \
const double N = time (); \
const int L = internal->opts.profile; \
if (internal->profiles.S.level <= L) \
internal->stop_profiling (internal->profiles.S, N); \
if (internal->profiles.simplify.level <= L) \
internal->stop_profiling (internal->profiles.simplify, N); \
) \
reset_mode (M); \
reset_mode (SIMPLIFY); \
if (!preprocessing && !lookingahead) { \
if (internal->profiles.search.level <= L) \
internal->start_profiling (internal->profiles.search, N); \
if (stable && internal->profiles.stable.level <= L) \
internal->start_profiling (internal->profiles.stable, N); \
if (!stable && internal->profiles.unstable.level <= L) \
internal->start_profiling (internal->profiles.unstable, N); \
NON_QUIET_PROFILE_CODE ( \
if (internal->profiles.search.level <= L) \
internal->start_profiling (internal->profiles.search, N); \
if (stable && internal->profiles.stable.level <= L) \
internal->start_profiling (internal->profiles.stable, N); \
if (!stable && internal->profiles.unstable.level <= L) \
internal->start_profiling (internal->profiles.unstable, N); \
) \
set_mode (SEARCH); \
} \
} while (0)
Expand All @@ -173,14 +195,16 @@ do { \
do { \
require_mode (SEARCH); \
assert (!preprocessing); \
const double N = time (); \
const int L = internal->opts.profile; \
if (stable && internal->profiles.stable.level <= L) \
internal->stop_profiling (internal->profiles.stable, N); \
if (!stable && internal->profiles.unstable.level <= L) \
internal->stop_profiling (internal->profiles.unstable, N); \
if (internal->profiles.walk.level <= L) \
internal->start_profiling (internal->profiles.walk, N); \
NON_QUIET_PROFILE_CODE ( \
const double N = time (); \
const int L = internal->opts.profile; \
if (stable && internal->profiles.stable.level <= L) \
internal->stop_profiling (internal->profiles.stable, N); \
if (!stable && internal->profiles.unstable.level <= L) \
internal->stop_profiling (internal->profiles.unstable, N); \
if (internal->profiles.walk.level <= L) \
internal->start_profiling (internal->profiles.walk, N); \
) \
set_mode (WALK); \
} while (0)

Expand All @@ -192,14 +216,16 @@ do { \
require_mode (SEARCH); \
assert (!preprocessing); \
reset_mode (WALK); \
const double N = time (); \
const int L = internal->opts.profile; \
if (internal->profiles.walk.level <= L) \
internal->stop_profiling (internal->profiles.walk, N); \
if (stable && internal->profiles.stable.level <= L) \
internal->start_profiling (internal->profiles.stable, N); \
if (!stable && internal->profiles.unstable.level <= L) \
internal->start_profiling (internal->profiles.unstable, N); \
NON_QUIET_PROFILE_CODE ( \
const double N = time (); \
const int L = internal->opts.profile; \
if (internal->profiles.walk.level <= L) \
internal->stop_profiling (internal->profiles.walk, N); \
if (stable && internal->profiles.stable.level <= L) \
internal->start_profiling (internal->profiles.stable, N); \
if (!stable && internal->profiles.unstable.level <= L) \
internal->start_profiling (internal->profiles.unstable, N); \
) \
} while (0)

/*------------------------------------------------------------------------*/
Expand All @@ -209,7 +235,9 @@ do { \
do { \
require_mode (SEARCH); \
assert (!preprocessing); \
START (walk); \
NON_QUIET_PROFILE_CODE ( \
START (walk); \
) \
set_mode (WALK); \
} while (0)

Expand All @@ -221,27 +249,9 @@ do { \
require_mode (SEARCH); \
assert (!preprocessing); \
reset_mode (WALK); \
STOP (walk); \
NON_QUIET_PROFILE_CODE ( \
STOP (walk); \
) \
} while (0)

/*------------------------------------------------------------------------*/
#else // ifndef QUIET
/*------------------------------------------------------------------------*/

#define START(...) do { } while (0)
#define STOP(...) do { } while (0)

#define START_SIMPLIFIER(...) do { } while (0)
#define STOP_SIMPLIFIER(...) do { } while (0)

#define START_OUTER_WALK(...) do { } while (0)
#define STOP_OUTER_WALK(...) do { } while (0)

#define START_INNER_WALK(...) do { } while (0)
#define STOP_INNER_WALK(...) do { } while (0)

/*------------------------------------------------------------------------*/
#endif // ifndef QUIET
/*------------------------------------------------------------------------*/

#endif // ifndef _profiles_h_INCLUDED
5 changes: 5 additions & 0 deletions src/random.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,11 @@ class Random {
Random (uint64_t seed) : state (seed) { }
Random (const Random & other) : state (other.seed ()) { }

// Without this explicit default copy assignment operator declaration GCC
// 9.3.0 issues a warning (C++11 semantics but not checked before GCC 9).
//
Random & operator = (const Random &) = default;

void operator += (uint64_t a) { add (a); }
uint64_t seed () const { return state; }

Expand Down
7 changes: 4 additions & 3 deletions src/solver.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1089,13 +1089,14 @@ class ClauseWriter : public ClauseIterator {
const char * Solver::write_dimacs (const char * path, int min_max_var) {
LOG_API_CALL_BEGIN ("write_dimacs", path, min_max_var);
REQUIRE_VALID_STATE ();
#ifndef QUIET
const double start = internal->time ();
#endif
internal->restore_clauses ();
ClauseCounter counter;
(void) traverse_clauses (counter);
LOG ("found maximal variable %d and %" PRId64 " clauses",
counter.vars, counter.clauses);
#ifndef QUIET
const double start = internal->time ();
#endif
File * file = File::write (internal, path);
const char * res = 0;
if (file) {
Expand Down
2 changes: 1 addition & 1 deletion src/version.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@

#ifndef NBUILD
#ifndef VERSION
# define VERSION "sc2020"
# define VERSION "1.3.0"
#endif // NBUILD
#endif // VERSION

Expand Down
6 changes: 3 additions & 3 deletions src/vivify.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -286,11 +286,11 @@ struct vivify_flush_smaller {
bool operator () (Clause * a, Clause * b) const {

const auto eoa = a->end (), eob = b->end ();
auto j = b->begin ();
for (auto i = a->begin (); i != eoa && j != eob; i++, j++)
auto i = a->begin (), j = b->begin ();
for (; i != eoa && j != eob; i++, j++)
if (*i != *j) return *i < *j;

return j == eob;
return j == eob && i != eoa;
}
};

Expand Down
Loading

0 comments on commit 0b7a2b5

Please sign in to comment.