Searched refs:operator (Results 1 - 25 of 214) sorted by relevance

123456789

/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/
H A DSolverTypes.h45 friend Lit operator ~ (Lit p);
54 friend bool operator == (Lit p, Lit q);
55 friend bool operator < (Lit p, Lit q);
59 inline Lit operator ~ (Lit p) { Lit q; q.x = p.x ^ 1; return q; }
66 inline bool operator == (Lit p, Lit q) { return index(p) == index(q); }
67 inline bool operator < (Lit p, Lit q) { return index(p) < index(q); } // '<' guarantees that p, ~p are adjacent in the ordering.
100 Lit operator [] (int i) const { return data[i]; }
101 Lit& operator [] (int i) { return data[i]; }
129 bool operator == (GClause c) const { return data == c.data; }
130 bool operator !
[all...]
H A DGlobal.h168 operator T* (void) { return data; } // (unsafe but convenient)
169 operator const T* (void) const { return data; }
187 const T& operator [] (int index) const { return data[index]; }
188 T& operator [] (int index) { return data[index]; }
195 vec<T>& operator = (vec<T>& other) { TEMPLATE_FAIL; }
245 bool operator == (const lbool& other) const { return value == other.value; }
246 bool operator != (const lbool& other) const { return value != other.value; }
247 lbool operator ~ (void) const { return lbool(-value); }
266 template <class T> static inline bool operator != (const T& x, const T& y) { return !(x == y); }
267 template <class T> static inline bool operator > (cons
[all...]
H A DVarOrder.h32 bool operator () (Var x, Var y) { return activity[x] > activity[y]; }
/seL4-l4v-master/HOL4/examples/dev/sw/
H A DpreARMSyntax.sml98 fun from_op operator =
99 if operator = Term `ADD` then Assem.ADD
100 else if operator = Term `SUB:OPERATOR` then Assem.SUB
101 else if operator = Term `RSB:OPERATOR` then Assem.RSB
102 else if operator = Term `MUL:OPERATOR` then Assem.MUL
103 else if operator = Term `MLA:OPERATOR` then Assem.MLA
104 else if operator = Term `AND:OPERATOR` then Assem.AND
105 else if operator = Term `ORR:OPERATOR` then Assem.ORR
106 else if operator = Term `EOR:OPERATOR` then Assem.EOR
107 else if operator
[all...]
H A DIRSyntax.sml13 datatype operator = madd | msub | mrsb | mmul | mmla | mmov | type
28 | SHIFT of operator * int
33 type instr = {oper: operator, dst: exp list, src: exp list}
310 | to_op _ = raise ERR "IL" "No corresponding operator in IL"
473 fun formatInst {oper = operator, src = sList, dst = dList} =
474 if operator = mpush then
475 print_op operator ^ " " ^ format_exp (hd dList) ^ " {" ^
478 else if operator = mpop then
479 print_op operator ^ " " ^ format_exp (hd sList) ^ " {" ^
483 print_op operator
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DpreARMSyntax.sml98 fun from_op operator =
99 if operator = Term `ADD` then Assem.ADD
100 else if operator = Term `SUB:OPERATOR` then Assem.SUB
101 else if operator = Term `RSB:OPERATOR` then Assem.RSB
102 else if operator = Term `MUL:OPERATOR` then Assem.MUL
103 else if operator = Term `MLA:OPERATOR` then Assem.MLA
104 else if operator = Term `AND:OPERATOR` then Assem.AND
105 else if operator = Term `ORR:OPERATOR` then Assem.ORR
106 else if operator = Term `EOR:OPERATOR` then Assem.EOR
107 else if operator
[all...]
H A DIR.sml105 else raise ERR "IR" ("invalid bi-operator : " ^ oper_name)
122 else raise ERR "IR" ("invalid relation operator" ^ oper_name)
210 let val (operator, operands) = dest_comb exp in value
212 if is_relop operator then
215 Tree.RELOP(convert_relop operator, analyzeExp t1, analyzeExp t2)
218 else if is_binop operator then
221 Tree.BINOP (convert_binop operator, analyzeExp t1, analyzeExp t2)
223 else Tree.BINOP (convert_binop operator, analyzeExp operands, analyzeExp operands) (* UNIOP of uniop * exp *)
225 else if same_const operator n2w_tm then (* words *)
228 let val (fun_name, fun_type) = dest_const operator i
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/
H A DpreARMSyntax.sml98 fun from_op operator =
99 if operator = Term `ADD` then Assem.ADD
100 else if operator = Term `SUB:OPERATOR` then Assem.SUB
101 else if operator = Term `RSB:OPERATOR` then Assem.RSB
102 else if operator = Term `MUL:OPERATOR` then Assem.MUL
103 else if operator = Term `MLA:OPERATOR` then Assem.MLA
104 else if operator = Term `AND:OPERATOR` then Assem.AND
105 else if operator = Term `ORR:OPERATOR` then Assem.ORR
106 else if operator = Term `EOR:OPERATOR` then Assem.EOR
107 else if operator
[all...]
H A DIR.sml105 else raise ERR "IR" ("invalid bi-operator : " ^ oper_name)
122 else raise ERR "IR" ("invalid relation operator" ^ oper_name)
210 let val (operator, operands) = dest_comb exp in value
212 if is_relop operator then
215 Tree.RELOP(convert_relop operator, analyzeExp t1, analyzeExp t2)
218 else if is_binop operator then
221 Tree.BINOP (convert_binop operator, analyzeExp t1, analyzeExp t2)
223 else Tree.BINOP (convert_binop operator, analyzeExp operands, analyzeExp operands) (* UNIOP of uniop * exp *)
225 else if same_const operator n2w_tm then (* words *)
228 let val (fun_name, fun_type) = dest_const operator i
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw2/
H A Dbasic.sml38 (* Is the operator a binary arithmetic operator? *)
48 (* Is the operator an arithmetic comparison operator? *)
59 (* Is the operator an arithmetic word operator? *)
69 (* Is the operator a multiplication operator? *)
78 (* Is the operator a word comparison operator
[all...]
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Dpolystring.h61 operator char*() { return m_value; }
62 char* operator = (char* p) { return (m_value = p); }
98 operator TCHAR*() { return m_value; }
99 TCHAR* operator = (TCHAR* p) { return (m_value = p); }
H A Drtsentry.h56 operator PolyWord()
H A Dtiming.h63 operator FILETIME() const { return t; }
78 operator timeval() const { return t; }
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/src/
H A Dbvec.h134 bdd operator[](int i) const { return roots.bitvec[i]; }
137 bvec operator=(const bvec &src);
178 bvec operator&(const bvec &a) const { return bvec_map2(*this, a, bdd_and); }
179 bvec operator^(const bvec &a) const { return bvec_map2(*this, a, bdd_xor); }
180 bvec operator|(const bvec &a) const { return bvec_map2(*this, a, bdd_or); }
181 bvec operator!(void) const { return bvec_map1(*this, bdd_not); }
182 bvec operator<<(int a) const { return bvec_shlfixed(*this,a,bddfalse); }
183 bvec operator<<(const bvec &a) const { return bvec_shl(*this,a,bddfalse); }
184 bvec operator>>(int a) const { return bvec_shrfixed(*this,a,bddfalse); }
185 bvec operator>>(cons
[all...]
H A Dbdd.h178 opHit & entries found in the operator caches \\
179 opMiss & entries not found in the operator caches \\
199 SECTION {* operator *}
397 #define BDD_OP (-12) /* Unknown operator */
433 bdd operator=(const bdd &r);
435 bdd operator&(const bdd &r) const;
436 bdd operator&=(const bdd &r);
437 bdd operator^(const bdd &r) const;
438 bdd operator^=(const bdd &r);
439 bdd operator|(cons
[all...]
/seL4-l4v-master/HOL4/examples/ind_def/
H A DmonosetScript.sml3 (* DESCRIPTION : Creates a new monoset including the EVERY operator, *)
25 We intend to add a new monotonic operator to the standard monoset
27 defined relations. A monotonic operator is a (possibly curried)
28 operator which yields a boolean result, some of whose operands
30 for which the operator yields true only increases
36 operator is to have instances of the new inductive constants appear
68 (* now we have to prove that this operator is monotone *)
/seL4-l4v-master/HOL4/src/1/
H A DMutual.sig6 (* standard INDUCT_THEN operator, which was translated *)
H A DAC_Sort.sig15 sorting terms with respect to an associative and commutative operator.
26 dest: destructor function for operator
28 mk: constructor function for operator
/seL4-l4v-master/HOL4/examples/PSL/regexp/
H A DregexpTools.sig21 (* Evaluating the Prefix operator on set regexps (like in Sugar) *)
24 (* Evaluating the Prefix operator on character regexps *)
27 (* Set this to a SAT solver for evaluating the Prefix operator *)
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/calculator/
H A Dslist.h163 ite &operator=(const ite &start) { next=start.next; return *this; }
164 ite operator++(void)
166 ite operator++(int)
168 T &operator*(void) const { return *((T*)next->data); }
169 int operator==(ite x) { return x.next==next; }
/seL4-l4v-master/HOL4/examples/CCS/
H A DStrongLawsConv.sml19 (* Conversions for the summation operator and strong equivalence *)
119 (* Conversions for the restriction operator and strong equivalence *)
123 (* Conversion for the application of the laws for the restriction operator. *)
168 (* Conversions for the relabelling operator and strong equivalence *)
172 (* Conversion for the application of the laws for the relabelling operator. *)
204 (* Conversions for the parallel operator and strong equivalence *)
236 parallel operator. *)
306 (* Conversion for the application of the law for the parallel operator in the
358 (* Conversion for the application of the laws for the parallel operator in the
382 (* Conversion for the application of the laws for the parallel operator
[all...]
H A DWeakLawsScript.sml16 (* Basic laws of observation equivalence for the binary summation operator *)
42 summation operator on the left:
74 (* operator derived through strong equivalence *)
184 (* operator derived through strong equivalence *)
248 (* operator derived through strong equivalence *)
276 (* operator through strong equivalence *)
/seL4-l4v-master/HOL4/src/num/arith/src/
H A DRJBConv.sml41 (* Applies a conversion to the arguments of a binary operator. *)
/seL4-l4v-master/HOL4/src/simp/
H A Dtest.sml13 (* reduction in operator *)
/seL4-l4v-master/HOL4/examples/hardware/hol88/
H A DITL.ml33 % The ITL next operator for expressions. This is called "O" in Ben's papers
34 but I use that name for the next operator for formulas (see below) %
59 % The ITL next operator for formulas %
65 % The ITL always operator %
71 % ITL chop operator (";" in Ben's notation - HOL won't allow ";" to be
121 % ITL stability operator %

Completed in 217 milliseconds

123456789