Searched refs:addClause (Results 1 - 8 of 8) sorted by relevance

/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/
H A DSolver.h182 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 DMain.C38 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 DminisatParse.sml127 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 Dzc2hs.cpp40 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 DActive.sml496 fun addClause active cl = function
900 val active = addClause active cl
H A DTptp.sml1905 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 DActive.sml496 fun addClause active cl = function
900 val active = addClause active cl
H A DTptp.sml1905 fun addClause (cl_src,sources) = function
1917 and sources = List.foldl addClause sources clauses

Completed in 162 milliseconds