Lines Matching refs:clause
68 id_counter = 1; //HA: to save sign info on-the-fly, unit_id uses -ve clause id's to indicate
69 // that the clause literal is negated, so can't use 0
72 c2fp.push(0); // dummy argument (placeholder for clause ID 0 which does not exist)
85 cl.copyTo(clause);
87 sortUnique(clause);
90 trav->root(clause);
100 putUInt(fp, index(clause[0]));
101 for (int i = 1; i < clause.size(); i++)
102 putUInt(fp, index(clause[i]) - index(clause[i-1]));
176 //HA: fill up "clause" as a root clause
178 ClauseId Proof::parseRoot(vec<Lit>& clause, File& fp, uint64 tmp, std::ofstream* fout) {
180 ClauseId Proof::parseRoot(vec<Lit>& clause, File& fp, uint64 tmp) {
189 clause.clear();
197 clause.push(toLit(idx));
207 clause.push(toLit(idx));
262 vec<ClauseId> c2c(goal+2,-1); // c2c[old_id] is new id in compressed proof of clause old_id
308 ClauseId orig_root_id = parseRoot(clause,fp,tmp);
309 c2c[id] = dst.addRoot(clause,orig_root_id);
386 // Root clause:
388 parseRoot(clause,fp,tmp,&fout);
390 parseRoot(clause,fp,tmp);
392 trav.root(clause);
402 id--, // (no new clause introduced)