Code: Select all
pltlf@GAMING ~/metasat
$ python ikpx.py -v 2,1c/7
****************************************************************
Incremental Knightship Partial Extend (ikpx)
****************************************************************
Please enter fully-qualified target directory [/tmp/ikpx] : 21c7
Parsing velocity...
Parameters: {'dudy': 3, 'dudx': 1, 'dvdx': 0, 'dvdy': 7, 'a': 1, 'p': 7, 'b': 2, 'dudt': 1, 'dvdt': 2}
Neither head nor tail specified; defaulting to head.
Please enter lookahead for the search [30] : 15
Please enter number of CPU cores for the search [40] : 7
Directory 21c7 created.
Ensuring iglucose is installed and operational:
****************************************************************
Installing iglucose...
Archive: iGlucose.zip
creating: tom-iGlucose/
creating: tom-iGlucose/mtl/
inflating: tom-iGlucose/mtl/XAlloc.h
inflating: tom-iGlucose/mtl/IntTypes.h
inflating: tom-iGlucose/mtl/Vec.h
inflating: tom-iGlucose/mtl/config.mk
inflating: tom-iGlucose/mtl/Sort.h
inflating: tom-iGlucose/mtl/Queue.h
inflating: tom-iGlucose/mtl/Alg.h
inflating: tom-iGlucose/mtl/Map.h
inflating: tom-iGlucose/mtl/Alloc.h
inflating: tom-iGlucose/mtl/template.mk
inflating: tom-iGlucose/mtl/Heap.h
creating: tom-iGlucose/core/
inflating: tom-iGlucose/core/depend.mk
inflating: tom-iGlucose/core/Main.cc
inflating: tom-iGlucose/core/Solver.cc
inflating: tom-iGlucose/core/Constants.h
inflating: tom-iGlucose/core/SolverTypes.h
inflating: tom-iGlucose/core/Dimacs.h
inflating: tom-iGlucose/core/Solver.h
inflating: tom-iGlucose/core/BoundedQueue.h
inflating: tom-iGlucose/core/Makefile
creating: tom-iGlucose/simp/
inflating: tom-iGlucose/simp/Makefile
inflating: tom-iGlucose/simp/SimpSolver.cc
inflating: tom-iGlucose/simp/SimpSolver.h
inflating: tom-iGlucose/simp/Main.cc
creating: tom-iGlucose/utils/
inflating: tom-iGlucose/utils/ParseUtils.h
inflating: tom-iGlucose/utils/System.cc
inflating: tom-iGlucose/utils/Makefile
inflating: tom-iGlucose/utils/System.h
inflating: tom-iGlucose/utils/Options.h
inflating: tom-iGlucose/utils/Options.cc
make: Warning: File '/home/pltlf/metasat/iGlucose/core/../mtl/template.mk' has modification time 19010 s in the future
Making dependencies
make: Warning: File '/home/pltlf/metasat/iGlucose/core/../mtl/template.mk' has modification time 18983 s in the future
Compiling: /home/pltlf/metasat/iGlucose/core/Main.o
In file included from /home/pltlf/metasat/iGlucose/core/Main.cc:36:0:
/home/pltlf/metasat/iGlucose/utils/Options.h:285:29: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
fprintf(stderr, "%4"PRIi64, range.begin);
^
/home/pltlf/metasat/iGlucose/utils/Options.h:291:29: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
fprintf(stderr, "%4"PRIi64, range.end);
^
/home/pltlf/metasat/iGlucose/utils/Options.h:293:25: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
fprintf(stderr, "] (default: %"PRIi64")\n", value);
^
/home/pltlf/metasat/iGlucose/core/Main.cc:49:12: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
printf("c restarts : %"PRIu64" (%"PRIu64" conflicts in avg)\n", solver.starts,(solver.starts>0 ?solver.conflicts/solver.starts : 0));
^
/home/pltlf/metasat/iGlucose/core/Main.cc:49:47: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
printf("c restarts : %"PRIu64" (%"PRIu64" conflicts in avg)\n", solver.starts,(solver.starts>0 ?solver.conflicts/solver.starts : 0));
^
/home/pltlf/metasat/iGlucose/core/Main.cc:50:12: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
printf("c blocked restarts : %"PRIu64" (multiple: %"PRIu64") \n", solver.nbstopsrestarts,solver.nbstopsrestartssame);
^
/home/pltlf/metasat/iGlucose/core/Main.cc:50:47: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
printf("c blocked restarts : %"PRIu64" (multiple: %"PRIu64") \n", solver.nbstopsrestarts,solver.nbstopsrestartssame);
^
/home/pltlf/metasat/iGlucose/core/Main.cc:51:12: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
printf("c last block at restart : %"PRIu64"\n",solver.lastblockatrestart);
^
/home/pltlf/metasat/iGlucose/core/Main.cc:58:12: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
printf("c conflicts : %-12"PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time);
^
/home/pltlf/metasat/iGlucose/core/Main.cc:59:12: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
printf("c decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time);
^
/home/pltlf/metasat/iGlucose/core/Main.cc:60:12: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
printf("c propagations : %-12"PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
^
/home/pltlf/metasat/iGlucose/core/Main.cc:61:12: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
printf("c conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
^
In file included from /home/pltlf/metasat/iGlucose/core/Main.cc:35:0:
/home/pltlf/metasat/iGlucose/utils/ParseUtils.h: In function ‘double Glucose::parseDouble(B&)’:
/home/pltlf/metasat/iGlucose/utils/ParseUtils.h:103:5: warning: this ‘while’ clause does not guard... [-Wmisleading-indentation]
while (*in >= '0' && *in <= '9')
^~~~~
/home/pltlf/metasat/iGlucose/utils/ParseUtils.h:107:2: note: ...this statement, but the latter is misleadingly indented as if it is guarded by the ‘while’
if (*in != 'e') printf("PARSE ERROR! Unexpected char: %c\n", *in),exit(3);
^~
/home/pltlf/metasat/iGlucose/core/Main.cc: At global scope:
/home/pltlf/metasat/iGlucose/core/Main.cc:76:13: warning: ‘void SIGINT_exit(int ’ defined but not used [-Wunused-function]
static void SIGINT_exit(int signum) {
^~~~~~~~~~~
Compiling: /home/pltlf/metasat/iGlucose/core/Solver.o
In file included from /home/pltlf/metasat/iGlucose/core/Solver.h:35:0,
from /home/pltlf/metasat/iGlucose/core/Solver.cc:33:
/home/pltlf/metasat/iGlucose/utils/Options.h:285:29: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
fprintf(stderr, "%4"PRIi64, range.begin);
^
/home/pltlf/metasat/iGlucose/utils/Options.h:291:29: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
fprintf(stderr, "%4"PRIi64, range.end);
^
/home/pltlf/metasat/iGlucose/utils/Options.h:293:25: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
fprintf(stderr, "] (default: %"PRIi64")\n", value);
^
In file included from /home/pltlf/metasat/iGlucose/utils/Options.h:30:0,
from /home/pltlf/metasat/iGlucose/core/Solver.h:35,
from /home/pltlf/metasat/iGlucose/core/Solver.cc:33:
/home/pltlf/metasat/iGlucose/utils/ParseUtils.h: In function ‘double Glucose::parseDouble(B&)’:
/home/pltlf/metasat/iGlucose/utils/ParseUtils.h:103:5: warning: this ‘while’ clause does not guard... [-Wmisleading-indentation]
while (*in >= '0' && *in <= '9')
^~~~~
/home/pltlf/metasat/iGlucose/utils/ParseUtils.h:107:2: note: ...this statement, but the latter is misleadingly indented as if it is guarded by the ‘while’
if (*in != 'e') printf("PARSE ERROR! Unexpected char: %c\n", *in),exit(3);
^~
/home/pltlf/metasat/iGlucose/core/Solver.cc: In member function ‘unsigned int Glucose::Solver::computeLBD(const Glucose::vec<Glucose::Lit>&, int)’:
/home/pltlf/metasat/iGlucose/core/Solver.cc:379:16: warning: comparison between signed and unsigned integer expressions [-Wsign-compare]
if(nbDone>=end) break;
~~~~~~^~~~~
/home/pltlf/metasat/iGlucose/core/Solver.cc: In member function ‘unsigned int Glucose::Solver::computeLBD(const Glucose::Clause&)’:
/home/pltlf/metasat/iGlucose/core/Solver.cc:408:16: warning: comparison between signed and unsigned integer expressions [-Wsign-compare]
if(nbDone>=c.sizeWithoutSelectors()) break;
~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~
/home/pltlf/metasat/iGlucose/core/Solver.cc: In member function ‘Glucose::lbool Glucose::Solver::search(int)’:
/home/pltlf/metasat/iGlucose/core/Solver.cc:1147:19: warning: comparison between signed and unsigned integer expressions [-Wsign-compare]
if(conflicts >= curRestart * nbclausesbeforereduce )
~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Compiling: utils/Options.o
In file included from /home/pltlf/metasat/iGlucose/core/../utils/Options.cc:21: :
/home/pltlf/metasat/iGlucose/utils/Options.h:285:29: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
fprintf(stderr, "%4"PRIi64, range.begin);
^
/home/pltlf/metasat/iGlucose/utils/Options.h:291:29: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
fprintf(stderr, "%4"PRIi64, range.end);
^
/home/pltlf/metasat/iGlucose/utils/Options.h:293:25: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
fprintf(stderr, "] (default: %"PRIi64")\n", value);
^
In file included from /home/pltlf/metasat/iGlucose/utils/Options.h:30:0,
from /home/pltlf/metasat/iGlucose/core/../utils/Options.cc:21:
/home/pltlf/metasat/iGlucose/utils/ParseUtils.h: In function ‘double Glucose::parseDouble(B&)’:
/home/pltlf/metasat/iGlucose/utils/ParseUtils.h:103:5: warning: this ‘while’ clause does not guard... [-Wmisleading-indentation]
while (*in >= '0' && *in <= '9')
^~~~~
/home/pltlf/metasat/iGlucose/utils/ParseUtils.h:107:2: note: ...this statement, but the latter is misleadingly indented as if it is guarded by the ‘while’
if (*in != 'e') printf("PARSE ERROR! Unexpected char: %c\n", *in),exit(3);
^~
/home/pltlf/metasat/iGlucose/core/../utils/Options.cc: In function ‘void Glucose::printUsageAndExit(int, char**, bool)’:
/home/pltlf/metasat/iGlucose/core/../utils/Options.cc:62:5: warning: this ‘if’ clause does not guard... [-Wmisleading-indentation]
if (usage != NULL)
^~
/home/pltlf/metasat/iGlucose/core/../utils/Options.cc:65:9: note: ...this statement, but the latter is misleadingly indented as if it is guarded by the ‘if’
sort(Option::getOptionList(), Option::OptionLt());
^~~~
Compiling: utils/System.o
Linking: iGlucose ( /home/pltlf/metasat/iGlucose/core/Main.o /home/pltlf/metasat/iGlucose/core/Solver.o utils/Options.o utils/System.o )
make: warning: Clock skew detected. Your build may be incomplete.
/home/pltlf/metasat
Installed iglucose
c
c This is glucose 3.0 -- based on MiniSAT (Many thanks to MiniSAT team)
c
c USAGE: compiled/iglucose [options] <input-file> <result-output-file>
where input may be either in plain or gzipped DIMACS.
CORE OPTIONS:
-incremental, -no-incremental (default: off)
-rnd-init, -no-rnd-init (default: off)
-gc-frac = <double> ( 0 .. inf) (default: 0.2)
-rnd-seed = <double> ( 0 .. inf) (default: 9.16483e+07)
-rnd-freq = <double> [ 0 .. 1] (default: 0)
-cla-decay = <double> ( 0 .. 1) (default: 0.999)
-var-decay = <double> ( 0 .. 1) (default: 0.8)
-phase-saving = <int32> [ 0 .. 2] (default: 2)
-ccmin-mode = <int32> [ 0 .. 2] (default: 2)
CORE -- CERTIFIED UNSAT OPTIONS:
-vbyte, -no-vbyte (default: off)
-certified, -no-certified (default: off)
-certified-output = <string>
CORE -- MINIMIZE OPTIONS:
-minLBDMinimizingClause = <int32> [ 3 .. imax] (default: 6)
-minSizeMinimizingClause = <int32> [ 3 .. imax] (default: 30)
CORE -- REDUCE OPTIONS:
-firstReduceDB = <int32> [ 0 .. imax] (default: 2000)
-minLBDFrozenClause = <int32> [ 0 .. imax] (default: 30)
-specialIncReduceDB = <int32> [ 0 .. imax] (default: 1000)
-incReduceDB = <int32> [ 0 .. imax] (default: 300)
CORE -- RESTART OPTIONS:
-K = <double> ( 0 .. 1) (default: 0.8)
-R = <double> ( 1 .. 5) (default: 1.4)
-szLBDQueue = <int32> [ 10 .. imax] (default: 50)
-szTrailQueue = <int32> [ 10 .. imax] (default: 5000)
MAIN OPTIONS:
-stop-at-unsat, -no-stop-at-unsat (default: off)
-model, -no-model (default: off)
-stop-at-sat, -no-stop-at-sat (default: off)
-inc-bound = <int32> [ 1 .. imax] (default: 1)
-to-bound = <int32> [ 0 .. imax] (default: 2147483647)
-from-bound = <int32> [ 0 .. imax] (default: 0)
-mem-lim = <int32> [ 0 .. imax] (default: 2147483647)
-cpu-lim = <int32> [ 0 .. imax] (default: 2147483647)
-vv = <int32> [ 1 .. imax] (default: 10000)
-verb = <int32> [ 0 .. 2] (default: 1)
HELP OPTIONS:
--help Print help message.
--help-verb Print verbose help message.
Exit status: 0
****************************************************************
Commencing search with the following parameters:
head search: {'a': 999999, 'd': 0.9, 'i': (0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1), 'k': 15, 'j': 7, 'p': 7, 't': 600, 'w': 5}
Directory 21c7/backup created.
Backup file 21c7/backup/backup_head_location.txt not found
To quit the program, either Ctrl+C or run the command:
kill -SIGINT -17956
Increasing head search width to 6...
...adaptive widening completed.