/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Proof.h | 37 virtual void root (const vec<Lit>& c) {} 38 virtual void chain (const vec<ClauseId>& cs, const vec<Var>& xs) {} 52 vec<Lit> clause; 53 vec<ClauseId> chain_id; 54 vec<Var> chain_var; 55 vec<int64> c2fp; // c2fp[id] gives position in proof trace of clause with id 'id' 63 ClauseId addRoot (vec<Lit>& clause, ClauseId orig_root_id = -1); 72 ClauseId parseRoot (vec<Lit>& clause, File& fp, uint64 tmp, std::ofstream* fout = NULL); 73 void parseChain(vec<ClauseI [all...] |
H A D | Solver.h | 54 vec<Clause*> clauses; // List of problem clauses. 55 vec<Clause*> learnts; // List of learnt clauses. 56 vec<ClauseId> unit_id; // 'unit_id[var]' is the clause ID for the unit literal 'var' or '~var' (if set at toplevel). 60 vec<double> activity; // A heuristic measurement of the activity of a variable. 65 vec<vec<Clause*> > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). 66 vec<char> assigns; // The current assignments (lbool:s stored as char:s). 67 vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made. 68 vec<int> trail_lim; // Separator indices for different decision levels in 'trail[]'. 69 vec<Claus [all...] |
H A D | VarOrder.h | 31 const vec<double>& activity; 33 VarOrder_lt(const vec<double>& act) : activity(act) { } 37 const vec<char>& assigns; // var->val. Pointer to external assignment table. 38 const vec<double>& activity; // var->act. Pointer to external activity table. 43 VarOrder(const vec<char>& ass, const vec<double>& act) :
|
H A D | Global.h | 140 // 'vec' -- automatically resizable arrays (via 'push()' method): 146 class vec { class 160 vec(void) : data(NULL) , sz(0) , cap(0) { } function in class:vec 161 vec(int size) : data(NULL) , sz(0) , cap(0) { growTo(size); } function in class:vec 162 vec(int size, const T& pad) : data(NULL) , sz(0) , cap(0) { growTo(size, pad); } function in class:vec 163 vec(T* array, int size) : data(array), sz(size), cap(size) { } // (takes ownership of array -- will be deallocated with 'xfree()') function in class:vec 164 ~vec(void) { clear(true); } 195 vec<T>& operator = (vec<T>& other) { TEMPLATE_FAIL; } 196 vec (ve function in class:vec [all...] |
H A D | Sort.h | 111 // For 'vec's: 114 template <class T, class LessThan> void sort(vec<T>& v, LessThan lt) { 116 template <class T> void sort(vec<T>& v) { 120 template <class T, class LessThan> void sortUnique(vec<T>& v, LessThan lt) { 124 v.~vec<T>(); 125 new (&v) vec<T>(data, size); } 126 template <class T> void sortUnique(vec<T>& v) {
|
H A D | Main.C | 32 void addLit(int parsed_lit,Solver& S, vec<Lit>& lits) { 38 void addClause(Solver& S, vec<Lit>& lits) { 51 vec<Lit> lits; 108 static void resolve(vec<Lit>& main, vec<Lit>& other, Var x) 139 vec<vec<Lit> > clauses; 141 void root (const vec<Lit>& c) { 149 void chain (const vec<ClauseId>& cs, const vec<Va [all...] |
H A D | Proof.C | 29 vec<cchar*> files; // For clean-up purposed on abnormal exit. 83 ClauseId Proof::addRoot(vec<Lit>& cl, ClauseId orig_root_id) 178 ClauseId Proof::parseRoot(vec<Lit>& clause, File& fp, uint64 tmp, std::ofstream* fout) { 180 ClauseId Proof::parseRoot(vec<Lit>& clause, File& fp, uint64 tmp) { 219 void Proof::parseChain(vec<ClauseId>& chain_id, vec<Var>& chain_var, 222 void Proof::parseChain(vec<ClauseId>& chain_id, vec<Var>& chain_var, 259 vec<ClauseId> dfs_stack; // stack for simulating "backwards" DFS 260 vec<ve [all...] |
H A D | SolverTypes.h | 89 Clause(bool learnt, const vec<Lit>& ps, ClauseId id_ = ClauseId_NULL) { 96 friend Clause* Clause_new(bool, const vec<Lit>&, ClauseId); 106 inline Clause* Clause_new(bool learnt, const vec<Lit>& ps, ClauseId id = ClauseId_NULL) {
|
H A D | Heap.h | 35 vec<int> heap; // heap of ints 36 vec<int> indices; // int -> index in heap
|
H A D | Solver.C | 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<cha [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | PolyVectorOperations.sml | 48 fun appi f vec = 50 val len = length vec 53 else (f(wordAsInt j, unsafeSub(vec, j)); doapp(j+0w1)) 58 fun app f vec = 60 val len = length vec 63 else (f(unsafeSub(vec, j)); doapp(j+0w1)) 70 fun foldl f init vec = 72 val len = length vec 75 else dofold (j+0w1) (f (unsafeSub(vec, j), acc)) 80 fun foldli f init vec [all...] |
H A D | VectorOperations.sml | 52 fun appi f vec = 54 val len = length vec 57 else (f(wordAsInt j, unsafeSub(vec, j)); doapp(j+0w1)) 62 fun app f vec = 64 val len = length vec 67 else (f(unsafeSub(vec, j)); doapp(j+0w1)) 74 fun foldl f init vec = 76 val len = length vec 79 else dofold (j+0w1) (f (unsafeSub(vec, j), acc)) 84 fun foldli f init vec [all...] |
H A D | Array.sml | 63 val vec = RunCall.allocateWordMemory(Word.fromInt len, 0wx40, 0w0) value 65 RunCall.unsafeCast vec 71 val vec = RunCall.allocateWordMemory(Word.fromInt len, 0wx40, RunCall.unsafeCast a) value 73 RunCall.unsafeCast vec 77 fun length (vec: 'a array): int = wordAsInt(RunCall.memoryCellLength(arrayAsWord vec)) 79 fun op sub (vec: 'a array, i: int): 'a = 80 if not (LibrarySupport.isShortInt i) orelse intAsWord i >= RunCall.memoryCellLength vec 82 else unsafeSub(vec, i) 84 fun update (vec 95 val vec = alloc length value 112 val vec = value [all...] |
H A D | Vector.sml | 63 fun op sub (vec:'a vector, i: int): 'a = 65 val v = vecAsWord vec 69 else unsafeSub(vec, i) 81 val vec = alloc length; value 92 init(vec, 0, l); 93 RunCall.clearMutableBit vec; 94 wordAsVec vec 100 val vec = value 105 else (RunCall.storeWord(vec, intAsWord i, RunCall.unsafeCast(f i)); init(i+1)) 108 RunCall.clearMutableBit vec; [all...] |
H A D | BoolArray.sml | 49 val vec = RunCall.allocateByteMemory(words, F_mutable_bytes) value 54 else (RunCall.storeByte(vec, n, 0w0); fill(n+0w1)) 59 vec 78 val vec = alloc length value 83 if bit = 0w1 then () else RunCall.storeByte(vec, byteno, acc) 91 RunCall.storeByte(vec, byteno, byte); 98 (length, vec) 103 val vec = value 114 then ( RunCall.storeByte(vec, byteNo, byte) ; init (i+1) (byteNo+0w1) 0w1 0w0 ) 120 RunCall.storeByte(vec, byteN 381 val vec = alloc len value [all...] |
H A D | BasicStreamIO.sml | 68 { vec: vector, offset: int, rest: instream, startPos: pos option } 76 {vec: vector, rest: streamState ref, startPos: pos option } 102 else Committed { vec = v, offset = 0, rest = readRest, startPos = NONE } 106 fun input' (ref (HaveRead {vec, rest, ...}), locker) = 111 (vec, Uncommitted{ state = rest, locker = locker }) 130 HaveRead {vec = data, rest = nextLink, startPos = startPos} 142 fun inputNList' (ref (HaveRead {vec, rest, startPos}), locker, n) = 144 val vecLength = Vector.length vec 147 then ([vec], Uncommitted{ state = rest, locker = locker }) 151 ([VectorSlice.vector(VectorSlice.slice(vec, 171 val (vec, f') = input' (f, locker) value [all...] |
H A D | Word8Array.sml | 144 val vec = LibrarySupport.allocBytes len value 148 else (RunCall.storeByte(vec, i, ini); init(i+0w1)) 151 Array(len, vec) 169 val vec = LibrarySupport.allocBytes length; value 176 init(vec, 0w0, l); 177 Array(length, vec) 183 val vec = LibrarySupport.allocBytes len value 187 else (RunCall.storeByte(vec, i, f(wordAsInt i)); init(i+0w1)) 190 Array(len, vec) 194 fun vector(Array(len, vec)) [all...] |
H A D | VectorSliceOperations.sml | 94 fun slice(vec: vector, i: int, NONE) = 97 val len = vecLength vec 100 then Slice{vector=vec, start=iW, length=len-iW} (* Length is rest of vector. *) 103 | slice(vec: vector, i: int, SOME l) = 105 val len = vecLength vec 110 then Slice{vector=vec, start=iW, length=lW} (* Length is as given. *)
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/mos-count/ |
H A D | types.ml | 12 let vec = ":^posn->^val";; 14 let bus = ":^time->^vec";;
|
H A D | dataabs.ml | 37 "(Defn 0 (v:^vec) = Def (v 0)) /\ 38 (Defn (SUC n) (v:^vec) = Def (v (SUC n)) /\ Defn n v)");; 47 "WordAbs (v:^vec) = \p. BoolAbs (v p)");;
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
H A D | Color.sml | 114 fun doStore (pe: PALETTEENTRY, vec) = 116 ignore(storePE(vec, toPE pe)); (* Ignore result - nothing to free *) 117 vec ++ peSize 123 val vec = allocPEVec count value 124 val _ = List.foldl doStore vec pl 126 (vec, count) 133 val vec = malloc(Word.fromInt count * peSize + lpSize) value 134 val _ = storeLP(vec, (0x300, count)) 135 val _ = List.foldl doStore (vec ++ lpSize) pl 137 vec 166 val (vec, count) = palListToC pl value 181 val vec = logPaletteToC pl value 197 val vec = allocPEVec no value 214 val vec = allocPEVec no value 231 val (vec, count) = palListToC pl value [all...] |
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/zc2hs/ |
H A D | zc2hs.cpp | 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<Li [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | polystring.cpp | 268 char **vec = (char**)calloc(len+1, sizeof(char*)); local 275 vec[len++] = Poly_string_to_C_alloc(cell->h); 278 return vec; 282 void freeStringVector(char **vec) argument 285 if (vec == 0) return; 286 for (p = vec; *p != 0; p++) free(*p); 287 free(vec);
|
H A D | polystring.h | 111 extern void freeStringVector(char **vec);
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/vector_def_CNF/ |
H A D | defCNF.sml | 64 fun def_step (defs as (vec, n, ds), tm) = 67 val g = mk_comb (vec, n) 70 ((vec, n, (g, tm) :: ds), g) 148 val (vec, n, ds) = defs value 156 val th2 = GEN vec (foldl DISCH_CONJ (DISCH eq th1) rest)
|