| /seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
| H A D | Solver.C | 98 const vec<Lit>& ps = learnt ? ps_ : qs; // 'ps' is now the (possibly) reduced vector of literals. variable
[all...] |
| H A D | SolverTypes.h | 89 Clause(bool learnt, const vec<Lit>& ps, ClauseId id_ = ClauseId_NULL) { argument
106 inline Clause* Clause_new(bool learnt, const vec<Lit>& ps, ClauseId id = ClauseId_NULL) { argument
|
| H A D | Solver.h | 185 void addClause (const vec<Lit>& ps) { newClause(ps); } // (used to be a difference between internal and external method...) argument
|
| /seL4-l4v-10.1.1/HOL4/src/postkernel/ |
| H A D | TheoryGraph.sml | 102 val ps = Theory.parents thy_s value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
| H A D | stack_introLib.sml | 11 val ps = list_dest dest_star p value
|
| H A D | straightlineLib.sml | 31 val ps = list_dest dest_star pre value
|
| H A D | stack_analysisLib.sml | 30 val ps = list_dest dest_star pre value
|
| H A D | graph_specsLib.sml | 107 val ps = list_dest dest_star pre value
122 val ps = list_dest dest_star post value
124 val ps = filter (not o can (match_term pc_pat)) ps value
125 val ps = filter (not o can (match_term emp_pat)) ps value
[all...] |
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
| H A D | polystring.h | 38 inline POLYUNSIGNED PolyStringLength(PolyWord ps) { return ((PolyStringObject*)ps.AsObjPtr())->length; } argument
58 TempCString(PolyWord ps): m_value(Poly_string_to_C_alloc(ps)) {} argument
95 TempString(PolyWord ps): m_value(Poly_string_to_T_alloc(ps)) {} argument
[all...] |
| H A D | polystring.cpp | 84 POLYUNSIGNED Poly_string_to_C(PolyWord ps, char *buff, POLYUNSIGNED bufflen) argument
95 char *Poly_string_to_C_alloc(PolyWord ps, size_t extraChars) argument
160 POLYUNSIGNED Poly_string_to_C(PolyWord ps, WCHAR *buff, POLYUNSIGNED bufflen) argument
184 WCHAR *Poly_string_to_U_alloc(PolyWord ps, size_t extraChars) argument
|
| H A D | pexport.cpp | 139 PolyStringObject* ps = (PolyStringObject*)p; local
679 PolyStringObject * ps = (PolyStringObject *)p; local
|
| H A D | process_env.cpp | 438 PolyStringObject * ps = (PolyStringObject *)path.AsObjPtr(); local
|
| H A D | unix_specific.cpp | 2067 static int findPathVar(TaskData *taskData, PolyWord ps) argument
|
| H A D | windows_specific.cpp | 1259 PolyStringObject *ps = (PolyStringObject*)str.AsObjPtr(); local
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
| H A D | tripleLib.sml | 85 val ps = progSyntax.strip_star (progSyntax.dest_pre (Thm.concl th)) value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
| H A D | codegenLib.sml | 329 val ps = list_dest dest_star p value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/x64_compiler/ |
| H A D | x64_codegenLib.sml | 228 val ps = list_dest dest_star p value
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
| H A D | GdiBase.sml | 215 val (ps, {x=width, ...}, cr) = loadStr v value
|
| /seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/zc2hs/ |
| H A D | zc2hs.cpp | 274 void update(vector<int>& ps, int lit, vector<int>& r1) { argument
311 vector<int> ps; // pivots local
287 get_res(const vector<int>& resolvents, vec<Lit>& res, vector<int>& ps) argument
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/n-bit/ |
| H A D | bitstringLib.sml | 352 val ps = List.tabulate (i - 1, mk_p) value
|
| /seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
| H A D | patternMatchesSyntax.sml | 448 val ps = pairSyntax.strip_pair pt value
491 val ps value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/step/ |
| H A D | arm8_stepLib.sml | 579 val ps = (List.concat o List.map decode_rwt) value
|
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | cacheTools.sml | 84 val ps = fromHOLstring p val qs = fromHOLstring q value
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Pmatch.sml | 799 val (ps,es) = unzip pes value
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | normalForms.sml | 581 val ps = TRY_CONV TSIMP_CONV; value
|