diff -dur picosat-913.ORIG/picosat.c picosat-913/picosat.c --- picosat-913.ORIG/picosat.c 2009-07-13 07:04:44.000000000 -0600 +++ picosat-913/picosat.c 2009-09-02 12:24:48.428654095 -0600 @@ -6112,6 +6112,160 @@ #endif } +/** + * method to access the zhains without printing to a file + */ + +static int* proof = NULL; +static int cursor = 0; +#define PROOF_BLOCK 10000 +static int current_size; +static void add_int_to_proof(int i) +{ + if(cursor >= current_size){ + current_size += PROOF_BLOCK; + proof = realloc(proof, current_size); + } + proof[cursor] = i; + cursor++; +} + +static int +my_write_idx (unsigned idx) +{ + return EXPORTIDX (idx); +} +static void +my_trace_lits (Cls * cls) +{ + Lit **p, **eol = end_of_lits (cls); + + assert (cls); + assert (cls->core); + + for (p = cls->lits; p < eol; p++) + { + int lit = LIT2INT (*p); + add_int_to_proof(lit); + } + + add_int_to_proof(0); +} +static void +my_trace_zhain (unsigned idx, Zhn * zhain) +{ + unsigned prev, this, delta, i; + Znt *p, byte; + Cls * cls; + + assert (zhain); + assert (zhain->core); + + int id = my_write_idx (idx); + add_int_to_proof(id); + + cls = IDX2CLS (idx); + assert (cls); + my_trace_lits (cls); + + i = 0; + delta = 0; + prev = 0; + + for (p = zhain->znt; (byte = *p); p++, i += 7) + { + delta |= (byte & 0x7f) << i; + if (byte & 0x80) + continue; + + this = prev + delta; + + int id = my_write_idx (this); + add_int_to_proof(id); + + prev = this; + delta = 0; + i = -7; + } + + add_int_to_proof(0); + +} +static void +my_trace_clause (unsigned idx, Cls * cls) +{ + assert (cls); + assert (cls->core); + assert (!cls->learned); + assert (CLS2IDX (cls) == idx); + + int id = my_write_idx (idx); + add_int_to_proof(id); + + my_trace_lits (cls); + + add_int_to_proof(0); + +} +static int* +get_proof() +{ +#ifdef TRACE + if (proof != NULL){ + free(proof); + } + proof = malloc(PROOF_BLOCK * (sizeof(int))); + current_size = PROOF_BLOCK; + cursor = 0; + + + Cls *cls, ** p; + Zhn *zhain; + unsigned i; + + core (); + + for (p = SOC; p != EOC; p = NXC (p)) + { + cls = *p; + + if (oclauses <= p && p < eoo) + { + i = OIDX2IDX (p - oclauses); + assert (!cls || CLS2IDX (cls) == i); + } + else + { + assert (lclauses <= p && p < eol); + i = LIDX2IDX (p - lclauses); + } + + zhain = IDX2ZHN (i); + + if (zhain) + { + if (zhain->core) + { + my_trace_zhain (i, zhain); + } + } + else if (cls) + { + if (cls->core) + my_trace_clause (i, cls); + } + } + add_int_to_proof(EOP); + return proof; +#endif +} +int * +picosat_get_proof(){ + return get_proof(); +} +//// + + static void write_core_wrapper (FILE * file, int fmt) { diff -dur picosat-913.ORIG/picosat.h picosat-913/picosat.h --- picosat-913.ORIG/picosat.h 2009-07-13 07:04:44.000000000 -0600 +++ picosat-913/picosat.h 2009-09-02 12:24:27.959725988 -0600 @@ -178,6 +178,12 @@ */ void picosat_adjust (int max_idx); +/* Return an array of int where every cell is the next value of the proof in + * EXTENDED_TRACECHECK_TRACE_FMT format. + * The proof finishes by EOP. + */ +#define EOP ((int)(1 << 31)) /* 2^31 -1, max caml int32*/ +int* picosat_get_proof(); /*------------------------------------------------------------------------*/ /* Statistics. */