From 0b7a2b5764f845cff0b81ec16ebac20cb5cc138c Mon Sep 17 00:00:00 2001 From: Armin Biere Date: Thu, 11 Jun 2020 11:43:16 +0200 Subject: [PATCH] ports & fixed two issues 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 --- VERSION | 2 +- configure | 4 +- scripts/build-and-test-all-configurations.sh | 4 + scripts/colors.sh | 23 ++- src/profile.cpp | 11 +- src/profile.hpp | 144 ++++++++++--------- src/random.hpp | 5 + src/solver.cpp | 7 +- src/version.cpp | 2 +- src/vivify.cpp | 6 +- test/api/run.sh | 20 +-- test/cnf/run.sh | 72 +++++----- test/icnf/run.sh | 24 ++-- test/mbt/run.sh | 16 +-- test/trace/run.sh | 22 +-- test/usage/run.sh | 22 +-- 16 files changed, 208 insertions(+), 176 deletions(-) mode change 100755 => 100644 scripts/colors.sh diff --git a/VERSION b/VERSION index 6582e891..f0bb29e7 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -sc2020 +1.3.0 diff --git a/configure b/configure index c45a7b87..a4f8421e 100755 --- a/configure +++ b/configure @@ -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 diff --git a/scripts/build-and-test-all-configurations.sh b/scripts/build-and-test-all-configurations.sh index 6dc0e594..d1e0596f 100755 --- a/scripts/build-and-test-all-configurations.sh +++ b/scripts/build-and-test-all-configurations.sh @@ -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 diff --git a/scripts/colors.sh b/scripts/colors.sh old mode 100755 new mode 100644 index 15f1817f..d65b919e --- a/scripts/colors.sh +++ b/scripts/colors.sh @@ -1,13 +1,20 @@ # Use colors if '' 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="" @@ -16,3 +23,7 @@ else BOLD="" NORMAL="" fi + +cecho () { + echo$color_echo_options $* +} diff --git a/src/profile.cpp b/src/profile.cpp index bbb9a193..9346b0da 100644 --- a/src/profile.cpp +++ b/src/profile.cpp @@ -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 diff --git a/src/profile.hpp b/src/profile.hpp index c1afe27b..720fee24 100644 --- a/src/profile.hpp +++ b/src/profile.hpp @@ -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) @@ -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) @@ -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) @@ -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) /*------------------------------------------------------------------------*/ @@ -209,7 +235,9 @@ do { \ do { \ require_mode (SEARCH); \ assert (!preprocessing); \ - START (walk); \ + NON_QUIET_PROFILE_CODE ( \ + START (walk); \ + ) \ set_mode (WALK); \ } while (0) @@ -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 diff --git a/src/random.hpp b/src/random.hpp index a371347f..594c9836 100644 --- a/src/random.hpp +++ b/src/random.hpp @@ -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; } diff --git a/src/solver.cpp b/src/solver.cpp index 49bfa695..d53cdb72 100644 --- a/src/solver.cpp +++ b/src/solver.cpp @@ -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) { diff --git a/src/version.cpp b/src/version.cpp index 7db0994f..a6a5b9d6 100644 --- a/src/version.cpp +++ b/src/version.cpp @@ -20,7 +20,7 @@ #ifndef NBUILD #ifndef VERSION -# define VERSION "sc2020" +# define VERSION "1.3.0" #endif // NBUILD #endif // VERSION diff --git a/src/vivify.cpp b/src/vivify.cpp index 351b88b7..2af78402 100644 --- a/src/vivify.cpp +++ b/src/vivify.cpp @@ -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; } }; diff --git a/test/api/run.sh b/test/api/run.sh index 406a54b9..b270184a 100755 --- a/test/api/run.sh +++ b/test/api/run.sh @@ -3,12 +3,12 @@ #--------------------------------------------------------------------------# die () { - echo "${HIDE}test/api/run.sh:${NORMAL} ${BAD}error:${NORMAL} $*" + cecho "${HIDE}test/api/run.sh:${NORMAL} ${BAD}error:${NORMAL} $*" exit 1 } msg () { - echo "${HIDE}test/api/run.sh:${NORMAL} $*" + cecho "${HIDE}test/api/run.sh:${NORMAL} $*" } for dir in . .. ../.. @@ -31,11 +31,11 @@ die "needs to be called from a top-level sub-directory of CaDiCaL" [ -f "$CADICALBUILD/libcadical.a" ] || \ die "can not find '$CADICALBUILD/libcadical.a' (run 'make' first)" -echo -n "$HILITE" -echo "---------------------------------------------------------" -echo "API testing in '$CADICALBUILD'" -echo "---------------------------------------------------------" -echo -n "$NORMAL" +cecho -n "$HILITE" +cecho "---------------------------------------------------------" +cecho "API testing in '$CADICALBUILD'" +cecho "---------------------------------------------------------" +cecho -n "$NORMAL" make -C $CADICALBUILD res=$? @@ -62,7 +62,7 @@ failed=0 cmd () { test $status = 1 && return - echo $* + cecho $* $* >> $name.log status=$? } @@ -90,10 +90,10 @@ run () { cmd $name if test $status = 0 then - echo "# 0 ... ${GOOD}ok${NORMAL} (zero exit code)" + cecho "# 0 ... ${GOOD}ok${NORMAL} (zero exit code)" ok=`expr $ok + 1` else - echo "# 0 ... ${BAD}failed${NORMAL} (non-zero exit code)" + cecho "# 0 ... ${BAD}failed${NORMAL} (non-zero exit code)" failed=`expr $failed + 1` fi } diff --git a/test/cnf/run.sh b/test/cnf/run.sh index 7ccf6cc4..289bb4d0 100755 --- a/test/cnf/run.sh +++ b/test/cnf/run.sh @@ -3,12 +3,12 @@ #--------------------------------------------------------------------------# die () { - echo "${HIDE}test/cnf/run.sh:${NORMAL} ${BAD}error:${NORMAL} $*" + cecho "${HIDE}test/cnf/run.sh:${NORMAL} ${BAD}error:${NORMAL} $*" exit 1 } msg () { - echo "${HIDE}test/cnf/run.sh:${NORMAL} $*" + cecho "${HIDE}test/cnf/run.sh:${NORMAL} $*" } for dir in . .. ../.. @@ -28,11 +28,11 @@ die "needs to be called from a top-level sub-directory of CaDiCaL" [ -x "$CADICALBUILD/cadical" ] || \ die "can not find '$CADICALBUILD/cadical' (run 'make' first)" -echo -n "$HILITE" -echo "---------------------------------------------------------" -echo "CNF testing in '$CADICALBUILD'" -echo "---------------------------------------------------------" -echo -n "$NORMAL" +cecho -n "$HILITE" +cecho "---------------------------------------------------------" +cecho "CNF testing in '$CADICALBUILD'" +cecho "---------------------------------------------------------" +cecho -n "$NORMAL" make -C $CADICALBUILD res=$? @@ -52,7 +52,7 @@ then if [ ! -f $solutionchecker -o ../test/cnf/precochk.c -nt $solutionchecker ] then cmd="cc -O -o $solutionchecker ../test/cnf/precochk.c -lz" - echo "$cmd" + cecho "$cmd" if $cmd 2>/dev/null then msg "external solution checking with '$solutionchecker'" @@ -107,58 +107,58 @@ core () { proofopts=" $prf" fi opts="$cnf --check$solopts$proofopts" - echo "$coresolver \\" - echo "$opts" - echo -n "# $2 ..." + cecho "$coresolver \\" + cecho "$opts" + cecho -n "# $2 ..." "$coresolver" $opts 1>$log 2>$err res=$? if [ ! $res = $2 ] then - echo " ${BAD}FAILED${NORMAL} (actual exit code $res)" + cecho " ${BAD}FAILED${NORMAL} (actual exit code $res)" failed=`expr $failed + 1` elif [ $res = 10 ] then if [ "$solopts" = "" ] then - echo " ${GOOD}ok${NORMAL} (without solution file)" + cecho " ${GOOD}ok${NORMAL} (without solution file)" else - echo " ${GOOD}ok${NORMAL} (solution file checked after parsing)" + cecho " ${GOOD}ok${NORMAL} (solution file checked after parsing)" fi if [ x"$solutionchecker" = xnone ] then ok=`expr $ok + 1` else - echo "$solutionchecker \\" - echo "$cnf $log" - echo -n "# 0 ..." + cecho "$solutionchecker \\" + cecho "$cnf $log" + cecho -n "# 0 ..." if $solutionchecker $cnf $log 1>&2 >$chk then - echo " ${GOOD}ok${NORMAL} (solution checked externally too)" + cecho " ${GOOD}ok${NORMAL} (solution checked externally too)" ok=`expr $ok + 1` else - echo " ${BAD}FAILED${NORMAL} (incorrect solution)" + cecho " ${BAD}FAILED${NORMAL} (incorrect solution)" failed=`expr $failed + 1` fi fi elif [ $res = 20 ] then - echo " ${GOOD}ok${NORMAL} (exit code as expected)" + cecho " ${GOOD}ok${NORMAL} (exit code as expected)" if [ ! x"$proofchecker" = xnone ] then - echo "$proofchecker \\" - echo "$cnf $prf" - echo -n "# 0 ..." + cecho "$proofchecker \\" + cecho "$cnf $prf" + cecho -n "# 0 ..." if $proofchecker $cnf $prf 1>&2 >$chk then - echo " ${GOOD}ok${NORMAL} (proof checked)" + cecho " ${GOOD}ok${NORMAL} (proof checked)" ok=`expr $ok + 1` else - echo " ${BAD}FAILED${NORMAL} (proof check '$proofchecker $cnf $prf' failed)" + cecho " ${BAD}FAILED${NORMAL} (proof check '$proofchecker $cnf $prf' failed)" failed=`expr $failed + 1` fi fi else - echo " ${BAD}FAILED${NORMAL} (unsupported exit code $res)" + cecho " ${BAD}FAILED${NORMAL} (unsupported exit code $res)" failed=`expr $failed + 1` fi } @@ -171,31 +171,31 @@ simp () { err=$prefix-$1.err chk=$prefix-$1.chk opts="$cnf" - echo "$simpsolver \\" - echo "$opts" - echo -n "# $2 ..." + cecho "$simpsolver \\" + cecho "$opts" + cecho -n "# $2 ..." "$simpsolver" $opts 1>$log 2>$err res=$? if [ ! $res = $2 ] then - echo " ${BAD}FAILED${NORMAL} (actual exit code $res)" + cecho " ${BAD}FAILED${NORMAL} (actual exit code $res)" failed=`expr $failed + 1` elif [ $res = 10 ] then - echo " ${GOOD}ok${NORMAL}" + cecho " ${GOOD}ok${NORMAL}" if [ x"$solutionchecker" = xnone ] then ok=`expr $ok + 1` else - echo "$solutionchecker \\" - echo "$cnf $log" - echo -n "# 0 ..." + cecho "$solutionchecker \\" + cecho "$cnf $log" + cecho -n "# 0 ..." if $solutionchecker $cnf $log 1>&2 >$chk then - echo " ${GOOD}ok${NORMAL} (solution checked externally)" + cecho " ${GOOD}ok${NORMAL} (solution checked externally)" ok=`expr $ok + 1` else - echo " ${BAD}FAILED${NORMAL} (incorrect solution)" + cecho " ${BAD}FAILED${NORMAL} (incorrect solution)" failed=`expr $failed + 1` fi fi diff --git a/test/icnf/run.sh b/test/icnf/run.sh index be0ce170..082ef203 100755 --- a/test/icnf/run.sh +++ b/test/icnf/run.sh @@ -3,12 +3,12 @@ #--------------------------------------------------------------------------# die () { - echo "${HIDE}test/icnf/run.sh:${NORMAL} ${BAD}error:${NORMAL} $*" + cecho "${HIDE}test/icnf/run.sh:${NORMAL} ${BAD}error:${NORMAL} $*" exit 1 } msg () { - echo "${HIDE}test/icnf/run.sh:${NORMAL} $*" + cecho "${HIDE}test/icnf/run.sh:${NORMAL} $*" } for dir in . .. ../.. @@ -28,11 +28,11 @@ die "needs to be called from a top-level sub-directory of CaDiCaL" [ -x "$CADICALBUILD/cadical" ] || \ die "can not find '$CADICALBUILD/cadical' (run 'make' first)" -echo -n "$HILITE" -echo "---------------------------------------------------------" -echo "ICNF testing in '$CADICALBUILD'" -echo "---------------------------------------------------------" -echo -n "$NORMAL" +cecho -n "$HILITE" +cecho "---------------------------------------------------------" +cecho "ICNF testing in '$CADICALBUILD'" +cecho "---------------------------------------------------------" +cecho -n "$NORMAL" make -C $CADICALBUILD res=$? @@ -55,17 +55,17 @@ run () { err=$prefix-$1.err opts="$icnf --check" opts="$icnf" - echo "$solver \\" - echo "$opts" - echo -n "# $2 ..." + cecho "$solver \\" + cecho "$opts" + cecho -n "# $2 ..." "$solver" $opts 1>$log 2>$err res=$? if [ ! $res = $2 ] then - echo " ${BAD}FAILED${NORMAL} (actual exit code $res)" + cecho " ${BAD}FAILED${NORMAL} (actual exit code $res)" failed=`expr $failed + 1` else - echo " ${GOOD}ok${NORMAL} (exit code '$res' as expected)" + cecho " ${GOOD}ok${NORMAL} (exit code '$res' as expected)" ok=`expr $ok + 1` fi } diff --git a/test/mbt/run.sh b/test/mbt/run.sh index 05fdb3da..33354c5f 100755 --- a/test/mbt/run.sh +++ b/test/mbt/run.sh @@ -3,12 +3,12 @@ #--------------------------------------------------------------------------# die () { - echo "${HIDE}test/mbt/run.sh:${NORMAL} ${BAD}error:${NORMAL} $*" + cecho "${HIDE}test/mbt/run.sh:${NORMAL} ${BAD}error:${NORMAL} $*" exit 1 } msg () { - echo "${HIDE}test/mbt/run.sh:${NORMAL} $*" + cecho "${HIDE}test/mbt/run.sh:${NORMAL} $*" } for dir in . .. ../.. @@ -28,11 +28,11 @@ die "needs to be called from a top-level sub-directory of CaDiCaL" [ -x "$CADICALBUILD/cadical" ] || \ die "can not find '$CADICALBUILD/cadical' (run 'make' first)" -echo -n "$HILITE" -echo "---------------------------------------------------------" -echo "Model-Based Testing in '$CADICALBUILD'" -echo "---------------------------------------------------------" -echo -n "$NORMAL" +cecho -n "$HILITE" +cecho "---------------------------------------------------------" +cecho "Model-Based Testing in '$CADICALBUILD'" +cecho "---------------------------------------------------------" +cecho -n "$NORMAL" make -C $CADICALBUILD res=$? @@ -47,7 +47,7 @@ msg "changing to build directory '$CADICALBUILD' and running" cd $CADICALBUILD cmd="./mobical 42 --medium -L $tests --do-not-fork" -echo "${HILITE}$cmd${NORMAL}" +cecho "${HILITE}$cmd${NORMAL}" $cmd res=$? diff --git a/test/trace/run.sh b/test/trace/run.sh index cc1269c1..de15ef8d 100755 --- a/test/trace/run.sh +++ b/test/trace/run.sh @@ -1,12 +1,12 @@ #!/bin/sh die () { - echo "${HIDE}test/trace/run.sh:${NORMAL} ${BAD}error:${NORMAL} $*" + cecho "${HIDE}test/trace/run.sh:${NORMAL} ${BAD}error:${NORMAL} $*" exit 1 } msg () { - echo "${HIDE}test/trace/run.sh:${NORMAL} $*" + cecho "${HIDE}test/trace/run.sh:${NORMAL} $*" } for dir in . .. ../.. @@ -26,11 +26,11 @@ die "needs to be called from a top-level sub-directory of CaDiCaL" [ -x "$CADICALBUILD/cadical" ] || \ die "can not find '$CADICALBUILD/cadical' (run 'make' first)" -echo -n "$HILITE" -echo "---------------------------------------------------------" -echo "Regression Testing API traces in '$CADICALBUILD'" -echo "---------------------------------------------------------" -echo -n "$NORMAL" +cecho -n "$HILITE" +cecho "---------------------------------------------------------" +cecho "Regression Testing API traces in '$CADICALBUILD'" +cecho "---------------------------------------------------------" +cecho -n "$NORMAL" cd $CADICALBUILD || exit 1 make @@ -48,16 +48,16 @@ run () { msg "running ${HILITE}'$1'${NORMAL}" trace=../test/trace/$1.trace executed=`expr $executed + 1` - echo "$CADICALBUILD/mobical $trace" + cecho "$CADICALBUILD/mobical $trace" $CADICALBUILD/mobical $trace 2>/dev/null 1>/dev/null res=$? - echo $res + cecho $res if [ $res = 0 ] then - echo "# ... ${GOOD}ok${NORMAL}" + cecho "# ... ${GOOD}ok${NORMAL}" ok=`expr $ok + 1` else - echo "# ... ${BAD}failed${NORMAL}" + cecho "# ... ${BAD}failed${NORMAL}" failed=`expr $failed + 1` fi } diff --git a/test/usage/run.sh b/test/usage/run.sh index 32535873..03b1f1d9 100755 --- a/test/usage/run.sh +++ b/test/usage/run.sh @@ -3,12 +3,12 @@ #--------------------------------------------------------------------------# die () { - echo "${HIDE}test/usage/run.sh:${NORMAL} ${BAD}error:${NORMAL} $*" + cecho "${HIDE}test/usage/run.sh:${NORMAL} ${BAD}error:${NORMAL} $*" exit 1 } msg () { - echo "${HIDE}test/usage/run.sh:${NORMAL} $*" + cecho "${HIDE}test/usage/run.sh:${NORMAL} $*" } for dir in . .. ../.. @@ -28,11 +28,11 @@ die "needs to be called from a top-level sub-directory of CaDiCaL" [ -x "$CADICALBUILD/cadical" ] || \ die "can not find '$CADICALBUILD/cadical' (run 'make' first)" -echo -n "$HILITE" -echo "---------------------------------------------------------" -echo "usage testing in '$CADICALBUILD'" -echo "---------------------------------------------------------" -echo -n "$NORMAL" +cecho -n "$HILITE" +cecho "---------------------------------------------------------" +cecho "usage testing in '$CADICALBUILD'" +cecho "---------------------------------------------------------" +cecho -n "$NORMAL" make -C $CADICALBUILD res=$? @@ -44,7 +44,7 @@ solver="$CADICALBUILD/cadical" #--------------------------------------------------------------------------# -echo "starting test run `pwd`" +cecho "starting test run `pwd`" ok=0 failed=0 @@ -58,15 +58,15 @@ run () { log="$buildprefix.log" err="$buildprefix.err" cmd="$solver $options" - echo -n "$cmd" + cecho -n "$cmd" $cmd 1>$log 2>$err res=$? if [ $res = $expected ] then - echo " # ${GOOD}ok${NORMAL} (expected exit code '$res')" + cecho " # ${GOOD}ok${NORMAL} (expected exit code '$res')" ok=`expr $ok + 1` else - echo " # ${BAD}FAILED${NORMAL} (unexpected exit code '$res')" + cecho " # ${BAD}FAILED${NORMAL} (unexpected exit code '$res')" failed=`expr $failed + 1` fi }