Searched refs:chain_var (Results 1 - 2 of 2) sorted by relevance
| /seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
| H A D | Proof.C | 113 chain_var.clear();
122 if (next>=0) chain_var.push(x << 1);
123 else chain_var.push((x << 1) | 1); // HA: adding sign info to pivots
130 chain_var.push(index(p));
136 assert(chain_id.size() == chain_var.size() + 1);
142 trav->chain(chain_id, chain_var);
152 for (int i = 0; i < chain_var.size(); i++)
153 putUInt(fp, chain_var[i] + 1),
217 //HA: fill up chain_id and chain_var
219 void Proof::parseChain(vec<ClauseId>& chain_id, vec<Var>& chain_var, argument
293 fout << " " << chain_var[i] << " "; local
[all...] |
| H A D | Proof.h | 54 vec<Var> chain_var; member in class:Proof
73 void parseChain(vec<ClauseId>& chain_id, vec<Var>& chain_var, File& fp, uint64 tmp, ClauseId id, std::ofstream* fout = NULL);
76 void parseChain(vec<ClauseId>& chain_id, vec<Var>& chain_var, File& fp, uint64 tmp, ClauseId id);
|
Completed in 99 milliseconds