/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | SolverTypes.h | 45 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 D | Global.h | 168 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 D | VarOrder.h | 32 bool operator () (Var x, Var y) { return activity[x] > activity[y]; }
|
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | preARMSyntax.sml | 98 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 D | IRSyntax.sml | 13 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 D | preARMSyntax.sml | 98 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 D | IR.sml | 105 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 D | preARMSyntax.sml | 98 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 D | IR.sml | 105 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 D | basic.sml | 38 (* 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 D | polystring.h | 61 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 D | rtsentry.h | 56 operator PolyWord()
|
H A D | timing.h | 63 operator FILETIME() const { return t; } 78 operator timeval() const { return t; }
|
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | bvec.h | 134 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 D | bdd.h | 178 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 D | monosetScript.sml | 3 (* 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 D | Mutual.sig | 6 (* standard INDUCT_THEN operator, which was translated *)
|
H A D | AC_Sort.sig | 15 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 D | regexpTools.sig | 21 (* 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 D | slist.h | 163 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 D | StrongLawsConv.sml | 19 (* 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 D | WeakLawsScript.sml | 16 (* 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 D | RJBConv.sml | 41 (* Applies a conversion to the arguments of a binary operator. *)
|
/seL4-l4v-master/HOL4/src/simp/ |
H A D | test.sml | 13 (* reduction in operator *)
|
/seL4-l4v-master/HOL4/examples/hardware/hol88/ |
H A D | ITL.ml | 33 % 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 %
|