/seL4-l4v-master/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,
|
/seL4-l4v-master/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,
|
/seL4-l4v-master/graph-refine/graph-to-graph/ |
H A D | graph_to_graph.py | 9 import graph_refine.problem as problem namespace 26 --L use loop counts at the file dir_name/loop_counts.py to generate ILP problem 68 print "Using automatically determined loopbounds to generate ILP problem" 70 print "Annotating ILP problem with preemption bounds"
|
H A D | bench.py | 17 import graph_refine.problem as problem namespace 44 p = fs[f_name].as_problem(problem.Problem)
|
H A D | convert_loop_bounds.py | 11 import graph_refine.problem as problem namespace 67 except problem.Abort, e: 68 print 'failed to analyse %s, problem aborted' % f
|
H A D | elf_file.py | 9 import graph_refine.problem as problem namespace
|
H A D | call_graph_utils.py | 9 import graph_refine.problem as problem namespace
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | selftest.sml | 23 fun normalForms_test (fname, function :conv, problem, result) = let 27 val p_s = padr 25 (term_to_string problem); 34 problem (* 'b *)
|
/seL4-l4v-master/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-master/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-master/HOL4/examples/AI_tasks/ |
H A D | mleCombinLib.sig | 33 (* problem generation *)
|
/seL4-l4v-master/HOL4/src/HolSat/ |
H A D | satConfig.sml | 24 pterm : term, (* input problem term *) 30 (* problem already in cnf, result is checked in HOL *)
|
/seL4-l4v-master/HOL4/src/real/ |
H A D | selftest.sml | 8 fun test (problem, result) = let 12 val p_s = padr 30 (t2s problem) 15 val th = QCONV s problem
|
/seL4-l4v-master/HOL4/examples/temporal_deep/src/examples/ |
H A D | ltl2omega.sml | 166 fun ltl2omega_test (test_fn, problem, result) = let 167 val _ = tprint (term_to_string problem); 169 require (check_result (aconv result o concl)) test_fn problem 297 fun ltl2omega_test_simple (test_fn, problem) = let 298 val _ = tprint (term_to_string problem); 300 require (check_result (fn th => true)) test_fn problem
|
/seL4-l4v-master/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-master/HOL4/src/HolSmt/ |
H A D | HolSmtLib.sml | 28 "solver reports 'unknown' (solver not installed/problem too hard?)"
|
/seL4-l4v-master/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.
|
/seL4-l4v-master/HOL4/examples/misc/ |
H A D | root2Script.sml | 45 (* The proof moves the problem from R to N, then uses lemma *)
|
/seL4-l4v-master/graph-refine/ |
H A D | trace_refute.py | 11 import problem namespace 126 printout ('Building compound problem for %s' % fnames) 128 p = problem.Problem (None, name = ', '.join(fnames)) 347 p = functions[f].as_problem (problem.Problem) 372 p = functions[fname].as_problem (problem.Problem) 375 if problem.has_inner_loop (p, h)]) 397 p = functions[fname].as_problem (problem.Problem) 407 elif problem.has_inner_loop (p, l_id): 613 except problem.Abort:
|