/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Proof.h | 65 void resolve (ClauseId next, Var x); 66 void resolve (ClauseId next, Lit p);
|
H A D | Solver.C | 94 if (proof != NULL) proof->resolve(unit_id[var(qs[i])], var(qs[i])); 287 if (proof != NULL) proof->resolve(unit_id[var(q)], var(q)); 301 proof->resolve(sconfl ? (confl->id())*(-1) : confl->id(), var(p)); 351 proof->resolve(sreason[v] ? -1*(c.id()) : c.id(), v); //HA: -id if v&1 in c 354 proof->resolve(unit_id[var(c[k])], var(c[k])); 428 if (proof != NULL) proof->resolve(unit_id[x], x); 442 proof->resolve(sreason[x] ? -1*(c.id()) : c.id(), x); 447 if (proof != NULL) proof->resolve(unit_id[var(c[j])], var(c[j])); 541 proof->resolve(unit_id[var(c[k])], var(c[k])); 549 proof->resolve((unit_i [all...] |
H A D | Proof.C | 118 void Proof::resolve(ClauseId next, Var x) function in class:Proof 126 void Proof::resolve(ClauseId next, Lit p) function in class:Proof 286 dst.resolve(chain_var[i-1] & 1 ? -1*chain_id[i] : chain_id[i],chain_var[i-1] >> 1);
|
H A D | Main.C | 108 static void resolve(vec<Lit>& main, vec<Lit>& other, Var x) function 159 resolve(c, clauses[cs[i+1]-1], xs[i] >> 1);
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Clause.sml | 278 fun resolve (cl1,lit1) (cl2,lit2) = function 281 val () = Print.trace pp "Clause.resolve: cl1" cl1 282 val () = Print.trace Literal.pp "Clause.resolve: lit1" lit1 283 val () = Print.trace pp "Clause.resolve: cl2" cl2 284 val () = Print.trace Literal.pp "Clause.resolve: lit2" lit2 290 val () = Print.trace Subst.pp "Clause.resolve: sub" sub 298 (trace "Clause.resolve: th1 violates ordering\n"; false) orelse 300 raise Error "resolve: clause1: ordering constraints" 303 (trace "Clause.resolve: th2 violates ordering\n"; false) orelse 305 raise Error "resolve [all...] |
H A D | Thm.sig | 120 (* --------------------- resolve L *) 127 val resolve : Literal.literal -> thm -> thm -> thm value
|
H A D | Thm.sml | 160 (* --------------------- resolve L *) 167 fun resolve lit (th1 as Thm (cl1,_)) (th2 as Thm (cl2,_)) = function 176 val resolve = fn lit => fn pos => fn neg => 177 resolve lit pos neg 179 raise Error ("Thm.resolve:\nlit = " ^ Literal.toString lit ^
|
H A D | Units.sml | 77 val th = Thm.resolve lit th (Thm.refl tm) 91 val th = Thm.resolve lit th rth
|
H A D | Rule.sml | 52 Thm.resolve reflLit reflTh eqTh 67 Thm.resolve (Literal.mkEq (yVar,xVar)) symmetry eqTh 87 Thm.resolve lit th symTh 134 val th = Thm.resolve x_y th1 th 135 val th = Thm.resolve y_z th2 th 220 val th = Thm.resolve reflLit reflTh th 224 | SOME x_y => Thm.resolve x_y eqTh th 304 else Thm.resolve lit' th1 th2) 340 | SOME x_y => Thm.resolve x_y eqTh th 410 else Thm.resolve li [all...] |
H A D | Clause.sig | 91 val resolve : clause * Literal.literal -> clause * Literal.literal -> clause value
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Clause.sml | 278 fun resolve (cl1,lit1) (cl2,lit2) = function 281 val () = Print.trace pp "Clause.resolve: cl1" cl1 282 val () = Print.trace Literal.pp "Clause.resolve: lit1" lit1 283 val () = Print.trace pp "Clause.resolve: cl2" cl2 284 val () = Print.trace Literal.pp "Clause.resolve: lit2" lit2 290 val () = Print.trace Subst.pp "Clause.resolve: sub" sub 298 (trace "Clause.resolve: th1 violates ordering\n"; false) orelse 300 raise Error "resolve: clause1: ordering constraints" 303 (trace "Clause.resolve: th2 violates ordering\n"; false) orelse 305 raise Error "resolve [all...] |
H A D | Thm.sig | 120 (* --------------------- resolve L *) 127 val resolve : Literal.literal -> thm -> thm -> thm value
|
H A D | Thm.sml | 160 (* --------------------- resolve L *) 167 fun resolve lit (th1 as Thm (cl1,_)) (th2 as Thm (cl2,_)) = function 176 val resolve = fn lit => fn pos => fn neg => 177 resolve lit pos neg 179 raise Error ("Thm.resolve:\nlit = " ^ Literal.toString lit ^
|
H A D | Units.sml | 77 val th = Thm.resolve lit th (Thm.refl tm) 91 val th = Thm.resolve lit th rth
|
H A D | Rule.sml | 52 Thm.resolve reflLit reflTh eqTh 67 Thm.resolve (Literal.mkEq (yVar,xVar)) symmetry eqTh 87 Thm.resolve lit th symTh 134 val th = Thm.resolve x_y th1 th 135 val th = Thm.resolve y_z th2 th 220 val th = Thm.resolve reflLit reflTh th 224 | SOME x_y => Thm.resolve x_y eqTh th 304 else Thm.resolve lit' th1 th2) 340 | SOME x_y => Thm.resolve x_y eqTh th 410 else Thm.resolve li [all...] |
H A D | Clause.sig | 91 val resolve : clause * Literal.literal -> clause * Literal.literal -> clause value
|
/seL4-l4v-master/isabelle/src/Pure/PIDE/ |
H A D | query_operation.scala | 95 /* resolve sendback: static command id */ 102 def resolve(body: XML.Body): XML.Body = 104 case XML.Wrapped_Elem(m, b1, b2) => XML.Wrapped_Elem(m, resolve(b1), resolve(b2)) 112 XML.Elem(Markup(Markup.SENDBACK, props1), resolve(b)) 113 case XML.Elem(m, b) => XML.Elem(m, resolve(b)) 116 resolve(body)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/PIDE/ |
H A D | query_operation.scala | 95 /* resolve sendback: static command id */ 102 def resolve(body: XML.Body): XML.Body = 104 case XML.Wrapped_Elem(m, b1, b2) => XML.Wrapped_Elem(m, resolve(b1), resolve(b2)) 112 XML.Elem(Markup(Markup.SENDBACK, props1), resolve(b)) 113 case XML.Elem(m, b) => XML.Elem(m, resolve(b)) 116 resolve(body)
|
/seL4-l4v-master/HOL4/src/HolSat/ |
H A D | minisatResolve.sml | 87 (* ground resolve clauses c0 and c1 on v, 91 fun resolve v n0 rth0 rth1 = function 99 (* resolve c0 against c1 wrt v *) 107 val rth = resolve v n0 rth0 rth1
|
H A D | minisatParse.sml | 94 (* parse and resolve a chain : assumes all dependencies already calculated *) 105 resolveChain lfn sva cl (br,brl) id; true) (* resolve *)
|
/seL4-l4v-master/HOL4/src/new-datatype/ |
H A D | Witness.sml | 44 fun resolve q [] thm = [] function 45 | resolve q (rule::rules) thm = let 56 in res :: (resolve q rules thm) 57 end handle _ => resolve q rules thm; 92 val res = resolve h1 rules thm
|
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/zc2hs/ |
H A D | zc2hs.cpp | 110 static void resolve(vec<Lit>& main, vec<Lit>& other, Var x) function 161 resolve(c, clauses[cs[i+1]-1], xs[i]>>1); 316 P.resolve(c2c[resolvents[ii]]+1, ~Lit(ps[ii-1]>>1,ps[ii-1]&1)); 341 P.resolve(c2c[iter->second]+1, ~lits[i]); 361 P.resolve(c2c[iter->second]+1, ~lits[i]);
|
/seL4-l4v-master/isabelle/src/Pure/General/ |
H A D | file_watcher.scala | 110 case (set, event) => set + dir.toPath.resolve(event.context).toFile
|
/seL4-l4v-master/l4v/isabelle/src/Pure/General/ |
H A D | file_watcher.scala | 110 case (set, event) => set + dir.toPath.resolve(event.context).toFile
|
/seL4-l4v-master/isabelle/src/Pure/Admin/ |
H A D | build_jdk.scala | 197 val path2 = dir2.resolve(main_dir.relativize(path1))
|