Searched refs:resolve (Results 1 - 25 of 74) sorted by relevance

123

/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/
H A DProof.h65 void resolve (ClauseId next, Var x);
66 void resolve (ClauseId next, Lit p);
H A DSolver.C94 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 DProof.C118 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 DMain.C108 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 DClause.sml278 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 DThm.sig120 (* --------------------- resolve L *)
127 val resolve : Literal.literal -> thm -> thm -> thm value
H A DThm.sml160 (* --------------------- 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 DUnits.sml77 val th = Thm.resolve lit th (Thm.refl tm)
91 val th = Thm.resolve lit th rth
H A DRule.sml52 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 DClause.sig91 val resolve : clause * Literal.literal -> clause * Literal.literal -> clause value
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DClause.sml278 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 DThm.sig120 (* --------------------- resolve L *)
127 val resolve : Literal.literal -> thm -> thm -> thm value
H A DThm.sml160 (* --------------------- 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 DUnits.sml77 val th = Thm.resolve lit th (Thm.refl tm)
91 val th = Thm.resolve lit th rth
H A DRule.sml52 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 DClause.sig91 val resolve : clause * Literal.literal -> clause * Literal.literal -> clause value
/seL4-l4v-master/isabelle/src/Pure/PIDE/
H A Dquery_operation.scala95 /* 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 Dquery_operation.scala95 /* 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 DminisatResolve.sml87 (* 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 DminisatParse.sml94 (* 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 DWitness.sml44 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 Dzc2hs.cpp110 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 Dfile_watcher.scala110 case (set, event) => set + dir.toPath.resolve(event.context).toFile
/seL4-l4v-master/l4v/isabelle/src/Pure/General/
H A Dfile_watcher.scala110 case (set, event) => set + dir.toPath.resolve(event.context).toFile
/seL4-l4v-master/isabelle/src/Pure/Admin/
H A Dbuild_jdk.scala197 val path2 = dir2.resolve(main_dir.relativize(path1))

Completed in 85 milliseconds

123