/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Problem.sig | 13 type problem = type 17 val size : problem -> {clauses : int, 22 val freeVars : problem -> NameSet.set 24 val toClauses : problem -> Thm.clause list 26 val toFormula : problem -> Formula.formula 28 val toGoal : problem -> Formula.formula 30 val toString : problem -> string 59 val categorize : problem -> category
|
H A D | Tptp.sig | 182 datatype problem = type 188 val hasCnfConjecture : problem -> bool 189 val hasFofConjecture : problem -> bool 190 val hasConjecture : problem -> bool 192 val freeVars : problem -> NameSet.set 199 problem : Problem.problem} -> problem 202 problem -> 204 problem [all...] |
H A D | metis.sml | 93 header = "usage: "^PROGRAM^" [option ...] problem.tptp ...\n" ^ 94 "Proves the input TPTP problem files.\n", 209 fun display_proof_body problem proofs = 217 {problem = problem, 232 {problem = proof, 240 fun display_proof filename problem proofs = 245 val () = display_proof_body problem proofs 259 val problem = 265 problem 367 val problem = Tptp.read {filename = filename, mapping = mapping} value 437 val problem = {axioms = axioms, conjecture = conjecture} value [all...] |
H A D | problems2tptp.sml | 29 fun checkProblems (problems : problem list) = 35 else raise Error ("duplicate problem name: " ^ x) 79 val problem = value 89 {problem = problem,
|
H A D | Tptp.sml | 1767 datatype problem = type 1816 fun mkProblem {comments,includes,names,roles,problem} = 1820 val {axioms,conjecture} = problem 1839 {problem : Problem.problem, 1843 {problem = {axioms = [], conjecture = []}, 1896 raise Error "TPTP problem has both cnf and fof conjecture formulas" 1908 val {problem,sources} : normalization = acc value 1909 val {axioms,conjecture} = problem 1916 val problem value 1957 val {problem,sources} = norm value 1959 val problem = {axioms = List.rev axioms, conjecture = List.rev conjecture} value 2162 val problem = {axioms = axioms, conjecture = conjecture} value 2172 val problem = read filename value [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Problem.sig | 13 type problem = type 17 val size : problem -> {clauses : int, 22 val freeVars : problem -> NameSet.set 24 val toClauses : problem -> Thm.clause list 26 val toFormula : problem -> Formula.formula 28 val toGoal : problem -> Formula.formula 30 val toString : problem -> string 59 val categorize : problem -> category
|
H A D | Tptp.sig | 182 datatype problem = type 188 val hasCnfConjecture : problem -> bool 189 val hasFofConjecture : problem -> bool 190 val hasConjecture : problem -> bool 192 val freeVars : problem -> NameSet.set 199 problem : Problem.problem} -> problem 202 problem -> 204 problem [all...] |
H A D | metis.sml | 93 header = "usage: "^PROGRAM^" [option ...] problem.tptp ...\n" ^ 94 "Proves the input TPTP problem files.\n", 209 fun display_proof_body problem proofs = 217 {problem = problem, 232 {problem = proof, 240 fun display_proof filename problem proofs = 245 val () = display_proof_body problem proofs 259 val problem = 265 problem 367 val problem = Tptp.read {filename = filename, mapping = mapping} value 437 val problem = {axioms = axioms, conjecture = conjecture} value [all...] |
H A D | problems2tptp.sml | 29 fun checkProblems (problems : problem list) = 35 else raise Error ("duplicate problem name: " ^ x) 79 val problem = value 89 {problem = problem,
|
H A D | Tptp.sml | 1767 datatype problem = type 1816 fun mkProblem {comments,includes,names,roles,problem} = 1820 val {axioms,conjecture} = problem 1839 {problem : Problem.problem, 1843 {problem = {axioms = [], conjecture = []}, 1896 raise Error "TPTP problem has both cnf and fof conjecture formulas" 1908 val {problem,sources} : normalization = acc value 1909 val {axioms,conjecture} = problem 1916 val problem value 1957 val {problem,sources} = norm value 1959 val problem = {axioms = List.rev axioms, conjecture = List.rev conjecture} value 2162 val problem = {axioms = axioms, conjecture = conjecture} value 2172 val problem = read filename value [all...] |
/seL4-l4v-10.1.1/HOL4/src/real/ |
H A D | selftest.sml | 7 fun test (problem, result) = let 11 val p_s = padr 30 (t2s problem) 14 val th = QCONV s problem
|
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
H A D | graph_to_graph.py | 12 import graph_refine.problem as problem namespace 29 --L use loop counts at the file dir_name/loop_counts.py to generate ILP problem 71 print "Using automatically determined loopbounds to generate ILP problem" 73 print "Annotating ILP problem with preemption bounds"
|
H A D | bench.py | 19 import graph_refine.problem as problem namespace 46 p = fs[f_name].as_problem(problem.Problem)
|
H A D | convert_loop_bounds.py | 13 import graph_refine.problem as problem namespace 69 except problem.Abort, e: 70 print 'failed to analyse %s, problem aborted' % f
|
H A D | elf_file.py | 11 import graph_refine.problem as problem namespace
|
H A D | call_graph_utils.py | 12 import graph_refine.problem as problem namespace
|
/seL4-l4v-10.1.1/HOL4/src/pred_set/src/ |
H A D | selftest.sml | 15 fun test s (problem, result) = let 17 val p_s = padr 30 (term_to_string problem) 20 val th = QCONV s problem
|
/seL4-l4v-10.1.1/HOL4/examples/CCS/ |
H A D | selftest.sml | 19 fun CCS_TRANS_test (problem, result) = let 22 val p_s = padr 30 (term_to_string problem); 29 problem
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/ |
H A D | satConfig.sml | 18 pterm : term, (* input problem term *) 22 flags : {is_cnf:bool,is_proved:bool} (* problem already in cnf, result is checked in HOL *)
|
/seL4-l4v-10.1.1/HOL4/src/1/theory_tests/ |
H A D | mergeGrammarsA1Script.sml | 36 made as the theories load. Instead, the problem is apparent in the
|
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | HolSmtLib.sml | 28 "solver reports 'unknown' (solver not installed/problem too hard?)"
|
/seL4-l4v-10.1.1/HOL4/src/holyhammer/ |
H A D | hhTranslate.sig | 35 (* problem *)
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | trace_refute.py | 13 import problem namespace 128 printout ('Building compound problem for %s' % fnames) 130 p = problem.Problem (None, name = ', '.join(fnames)) 349 p = functions[f].as_problem (problem.Problem) 374 p = functions[fname].as_problem (problem.Problem) 377 if problem.has_inner_loop (p, h)]) 399 p = functions[fname].as_problem (problem.Problem) 409 elif problem.has_inner_loop (p, l_id): 615 except problem.Abort:
|
/seL4-l4v-10.1.1/HOL4/examples/misc/ |
H A D | root2Script.sml | 45 (* The proof moves the problem from R to N, then uses lemma *)
|
/seL4-l4v-10.1.1/HOL4/developers/discussion/ |
H A D | overloading-extension.tex | 101 To figure out whether the latter is safe or not is the problem of 103 problem that Steven Obua's paper~\cite{Obua-RTA06} solves. If we 105 avoid this problem because we can just check each monomorphic 143 problem.
|