Lines Matching refs:vec
28 void vi2vl(const vector<int>& vi, vec<Lit>& vl) {
40 void addClause(vector<int>& lits, vec<vec<Lit> >& roots, parsed_clauses* pclauses,
54 vec<Lit> Lits;
63 void parse_DIMACS(Proof& P, vec<vec<Lit> >& roots, char* filename, parsed_clauses* pclauses,
110 static void resolve(vec<Lit>& main, vec<Lit>& other, Var x)
141 vec<vec<Lit> > clauses;
145 void root (const vec<Lit>& c) {
152 void chain (const vec<ClauseId>& cs, const vec<Var>& xs) {
157 vec<Lit>& c = clauses.last();
176 vec<Lit>& c = trav.clauses.last();
266 vec<vec<Lit> >& clauses;
267 vec<vec<Lit> >& roots;
288 vec<Lit>& res, vector<int>& ps) {
292 const vec<Lit>& cc = clauses[c2c[resolvents[ii]]];
310 vec<Lit> res;
333 vec<Lit>& lits = clauses[c2c[ante]];
355 vec<Lit>& lits = clauses[c2c[conf_id]];
392 vec<Lit> cc;
420 Z2M(Proof& P_,vec<vec<Lit> >& clauses_,vec<vec<Lit> >& roots_,
436 vec<Lit> cc;
487 vec<vec<Lit> > clauses; // proof clause database
488 vec<vec<Lit> > roots; // root clauses