Searched refs:addClause (Results 1 - 8 of 8) sorted by relevance
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Solver.h | 182 void addUnit (Lit p) { addUnit_tmp [0] = p; addClause(addUnit_tmp); } 183 void addBinary (Lit p, Lit q) { addBinary_tmp [0] = p; addBinary_tmp [1] = q; addClause(addBinary_tmp); } 184 void addTernary(Lit p, Lit q, Lit r) { addTernary_tmp[0] = p; addTernary_tmp[1] = q; addTernary_tmp[2] = r; addClause(addTernary_tmp); } 185 void addClause (const vec<Lit>& ps) { newClause(ps); } // (used to be a difference between internal and external method...) function in class:Solver
|
H A D | Main.C | 38 void addClause(Solver& S, vec<Lit>& lits) { function 42 S.addClause(lits); 61 if (lits.size()>0) addClause(S,lits); // in case last clause had no trailing 0 64 if (itok==0) addClause(S,lits);
|
/seL4-l4v-master/HOL4/src/HolSat/ |
H A D | minisatParse.sml | 127 fun addClause lfn cl sva vc clauseth fin lit1 id = function 136 ("addClause:Failed parsing clause "^Int.toString id^"\n") 151 let val _ = addClause lfn cl sva vc clauseth fin tmp id
|
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/zc2hs/ |
H A D | zc2hs.cpp | 40 void addClause(vector<int>& lits, vec<vec<Lit> >& roots, parsed_clauses* pclauses, function 79 if (lits.size()>0) addClause(lits,roots,pclauses,units,numclauses); // in case last clause had no trailing 0 82 if (itok==0) addClause(lits,roots,pclauses,units,numclauses);
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Active.sml | 496 fun addClause active cl = function 900 val active = addClause active cl
|
H A D | Tptp.sml | 1905 fun addClause (cl_src,sources) = function 1917 and sources = List.foldl addClause sources clauses
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Active.sml | 496 fun addClause active cl = function 900 val active = addClause active cl
|
H A D | Tptp.sml | 1905 fun addClause (cl_src,sources) = function 1917 and sources = List.foldl addClause sources clauses
|
Completed in 162 milliseconds