patrick/madagascar
1
0
Fork 0
Code Issues Pull Requests Releases Activity

Compare commits

base: patrick:master
Branches Tags
patrick:master
patrick:upstream
..
compare: patrick:upstream
Branches Tags
patrick:master
patrick:upstream

No commits in common. "master" and "upstream" have entirely different histories.
master ... upstream

4 changed files with 37 additions and 113 deletions
Show Stats Expand all files Collapse all files

10
Makefile
View File

@ -1,17 +1,17 @@
# 2012 (C) Jussi Rintanen, jrintanen.jr@gmail.com
# Uncomment for Madagascar with the planning heuristic as default (Mp)
VERSION = -DMPDOWNLOAD
EXECUTABLE=Mp
#VERSION = -DMPDOWNLOAD
#EXECUTABLE=Mp
# Uncomment for Madagascar C with the planning heuristic as default (MpC)
#VERSION = -DCMPDOWNLOAD
#EXECUTABLE=MpC
VERSION = -DCMPDOWNLOAD
EXECUTABLE=MpC
# Uncomment for Madagascar with VSIDS as default (M)
#VERSION = -DVSIDS
#EXECUTABLE=M
#ARCH=-m32
INSTRUMENT = -g -ggdb -pg
INSTRUMENT = #-g -ggdb -pg
CONFIGURATION= -DLBD -DREPRTHREE -DWEIGHTS #-DFUIP #-DMULTICORE #-DSPREAD -DCOSTS -DCFMA -DCP3

2
clausesets.c
View File

@ -1524,7 +1524,7 @@ int solve0(satinstance sati,int conflictstogo,int restart) {
sati->value = 0;
return 0;
SAT:
printf("SAT (%i ID %i decisions %i conflicts %i variables)\n",sati->id,sati->decisions,sati->conflicts,sati->nOfVars);
printf("SAT (%i decisions %i conflicts)\n",sati->decisions,sati->conflicts);
#ifdef COSTS
printf("FINAL COST %i.\n",sati->currentcost);
sati->costbound = sati->currentcost;

2
invariants.c
View File

@ -304,7 +304,7 @@ inline int ctruep(cfma f) {
}
#endif
int truep(fma *f) {
inline int truep(fma *f) {
fmalist *fs;
switch(f->t) {
case natom: return (onelits[f->a] != 1);

136
main.c
View File

@ -35,14 +35,6 @@
#include <omp.h>
#endif
int numberOfGroundActionsAfterParsing = -1;
int numberOfStateVariablesAfterParsing = -1;
int numberOfGroundActionsAfterSimplification = -1;
int numberOfStateVariablesAfterSimplification = -1;
int maxSizeOfStronglyConnectedComponents = -1;
char state_for_random[256];
char dump_for_random[256];
@ -81,10 +73,22 @@ void givememorystatistics() {
unsigned text;// text (code)
unsigned lib;// library
unsigned data;// data/stack
int MB;
fscanf(pf, "%u %u %u %u %u %u", &size, &resident, &share, &text, &lib, &data);
printf("memoryConsumption:\n total: %.1f # [MB]\n", ((double)size)/256.0);
MB = ((double)size)/256.0;
printf("total size %.3f %s\n",
/*
resident size: %u\n
shared pages : %u\n
text (code) : %u\n
library : %u\n
data/stack : %u\n",
*/
(MB < 700.0) ? MB : MB / 1024.0,
(MB < 700.0) ? "MB" : "GB");
}
fclose(pf);
}
@ -207,96 +211,7 @@ void processheuristic(char *decls) {
}
void printStatistics()
{
printf("\n\n# statistics in YAML format\n---\n");
printf("runtime:\n total: %.2f # [s]\n preprocessing: %.2f # [s]\n",
time2real(time10ms() - TIMEstart),
time2real(TIMEpreprocess - TIMEstart));
printf("maxLearnedClauseLength: %i\n",stats_longest_learned);
if (numberOfGroundActionsAfterParsing > -1)
printf("groundActions:\n afterParsing: %i\n",numberOfGroundActionsAfterParsing);
if (numberOfGroundActionsAfterSimplification > -1)
printf(" afterPreprocessing: %i\n",numberOfGroundActionsAfterSimplification);
if (numberOfStateVariablesAfterParsing > -1)
printf("stateVariables:\n afterParsing: %i\n",numberOfStateVariablesAfterParsing);
if (numberOfStateVariablesAfterSimplification > -1)
printf(" afterPreprocessing: %i\n",numberOfStateVariablesAfterSimplification);
if (maxSizeOfStronglyConnectedComponents > -1)
printf("stronglyConnectedComponents:\n maxSize: %i\n",maxSizeOfStronglyConnectedComponents);
int solutionIndex = -1;
for (int i = 0; seqs[i].sati; i++)
{
if (seqs[i].sati->value != 1)
continue;
solutionIndex = i;
break;
}
printf("plan:\n found: ");
if (solutionIndex < 0)
printf("false\n");
else
{
printf("true\n");
const auto planLength = seqs[solutionIndex].sati->nOfTPoints - 1;
int numberOfActions = 0;
const satinstance sati = seqs[solutionIndex].sati;
for (int t = 0; t < sati->nOfTPoints - 1; t++)
for (int i = 0; i < sati->nOfActions; i++)
if (vartruep(sati,TACT(i,t)))
numberOfActions++;
printf(" length: %i\n actions: %i\n", planLength, numberOfActions);
}
if(flagOutputDIMACS == 0) {
if (seqs[0].sati)
printf("iterations:\n");
int i = 0;
while(i*outputTimeStep+firstTimePoint < lastTimePoint && seqs[i].sati) {
printf(" - horizon: %i\n",seqs[i].sati->nOfTPoints-1);
printf(" result: ");
if (seqs[i].sati->value == 0)
printf("unsatisfiable");
else if (seqs[i].sati->value == 1)
printf("satisfiable");
else
printf("unknown");
printf("\n");
printf(" conflicts: %i\n",seqs[i].sati->conflicts);
printf(" decisions: %i\n",seqs[i].sati->decisions);
printf(" variables: %i\n",seqs[i].sati->nOfVars);
i += 1;
}// && seqs[i-1].sati->value != 1);
// } while(i*outputTimeStep+firstTimePoint < lastTimePoint);
}
printf("...\n");
}
void handleSignal()
{
printStatistics();
exit(0);
}
int main(int argc,char **argv) {
signal(SIGINT, handleSignal);
signal(SIGTERM, handleSignal);
int i,j;
syntacticclass sclass;
@ -737,9 +652,6 @@ int main(int argc,char **argv) {
NEWgroundoperators();
numberOfGroundActionsAfterParsing = nOfActions;
numberOfStateVariablesAfterParsing = nOfAtoms;
printf("Parser: %i ground actions and %i state variables\n",nOfActions,nOfAtoms);
if(flagShowInput) {
@ -776,9 +688,6 @@ int main(int argc,char **argv) {
if(flagEliminateConverses) mergecontras();
numberOfGroundActionsAfterSimplification = nOfActions;
numberOfStateVariablesAfterSimplification = nOfAtoms;
printf("Simplified: %i ground actions and %i state variables\n",nOfActions,nOfAtoms);
sortactions();
@ -811,7 +720,6 @@ int main(int argc,char **argv) {
int maxsize;
TIMEdisabling = time10ms();
maxsize = scc(nOfActions);
maxSizeOfStronglyConnectedComponents = maxsize;
printf(" %.2f secs (max SCC size %i)\n",time2real(time10ms() - TIMEdisabling),maxsize);
}
@ -819,7 +727,23 @@ int main(int argc,char **argv) {
encoding();
printStatistics();
printf("total time %.2f preprocess %.2f \n",
time2real(time10ms() - TIMEstart),
time2real(TIMEpreprocess - TIMEstart));
givememorystatistics();
printf("max. learned clause length %i\n",stats_longest_learned);
if(flagOutputDIMACS == 0) {
printf("t val conflicts decisions\n");
i = 0;
do {
printf("%i %i %i %i\n",seqs[i].sati->nOfTPoints-1,seqs[i].sati->value,seqs[i].sati->conflicts,seqs[i].sati->decisions);
i += 1;
} while(i*outputTimeStep+firstTimePoint <= lastTimePoint && seqs[i].sati && seqs[i-1].sati->value != 1);
// } while(i*outputTimeStep+firstTimePoint < lastTimePoint);
}
}