Lines Matching refs:vec
30 void removeWatch(vec<Clause*>& ws, Clause* elem)
45 | newClause : (ps : const vec<Lit>&) (learnt : bool) (id : ClauseId) -> [void]
62 void Solver::newClause(const vec<Lit>& ps_, bool learnt, ClauseId id)
67 vec<Lit> qs;
98 const vec<Lit>& ps = learnt ? ps_ : qs; // 'ps' is now the (possibly) reduced vector of literals.
232 | analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&) -> [void]
248 const vec<int>& trail_pos;
250 lastToFirst_lt(const vec<int>& t) : trail_pos(t) {}
254 void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel)
256 vec<char>& seen = analyze_seen;
421 vec<char>& seen = analyze_seen;
509 vec<Clause*>& ws = watches[index(p)];
634 vec<Clause*>& cs = type ? learnts : clauses;
681 vec<Lit> learnt_clause;
764 | solve : (assumps : const vec<Lit>&) -> [bool]
775 bool Solver::solve(const vec<Lit>& assumps)