Searched refs:vec (Results 1 - 25 of 50) sorted by relevance

12

/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/
H A DProof.h37 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 DSolver.h54 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 DVarOrder.h31 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 DGlobal.h140 // '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 DSort.h111 // 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 DMain.C32 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 DProof.C29 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 DSolverTypes.h89 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 DHeap.h35 vec<int> heap; // heap of ints
36 vec<int> indices; // int -> index in heap
H A DSolver.C30 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 DPolyVectorOperations.sml48 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 DVectorOperations.sml52 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 DArray.sml63 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 DVector.sml63 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 DBoolArray.sml49 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 DBasicStreamIO.sml68 { 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 DWord8Array.sml144 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 DVectorSliceOperations.sml94 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 Dtypes.ml12 let vec = ":^posn->^val";;
14 let bus = ":^time->^vec";;
H A Ddataabs.ml37 "(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 DColor.sml114 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 Dzc2hs.cpp28 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 Dpolystring.cpp268 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 Dpolystring.h111 extern void freeStringVector(char **vec);
/seL4-l4v-10.1.1/HOL4/src/HolSat/vector_def_CNF/
H A DdefCNF.sml64 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)

Completed in 124 milliseconds

12