Searched refs:problem (Results 1 - 25 of 162) sorted by relevance

1234567

/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DProblem.sig13 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 DTptp.sig182 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 Dmetis.sml93 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 Dproblems2tptp.sml29 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 DProblem.sig13 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 DTptp.sig182 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 Dmetis.sml93 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 Dproblems2tptp.sml29 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 Dgraph_to_graph.py9 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 Dbench.py17 import graph_refine.problem as problem namespace
44 p = fs[f_name].as_problem(problem.Problem)
H A Dconvert_loop_bounds.py11 import graph_refine.problem as problem namespace
67 except problem.Abort, e:
68 print 'failed to analyse %s, problem aborted' % f
H A Delf_file.py9 import graph_refine.problem as problem namespace
H A Dcall_graph_utils.py9 import graph_refine.problem as problem namespace
/seL4-l4v-master/HOL4/src/metis/
H A Dselftest.sml23 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 Dselftest.sml15 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 Dselftest.sml19 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 DmleCombinLib.sig33 (* problem generation *)
/seL4-l4v-master/HOL4/src/HolSat/
H A DsatConfig.sml24 pterm : term, (* input problem term *)
30 (* problem already in cnf, result is checked in HOL *)
/seL4-l4v-master/HOL4/src/real/
H A Dselftest.sml8 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 Dltl2omega.sml166 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 DmergeGrammarsA1Script.sml36 made as the theories load. Instead, the problem is apparent in the
/seL4-l4v-master/HOL4/src/HolSmt/
H A DHolSmtLib.sml28 "solver reports 'unknown' (solver not installed/problem too hard?)"
/seL4-l4v-master/HOL4/developers/discussion/
H A Doverloading-extension.tex101 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 Droot2Script.sml45 (* The proof moves the problem from R to N, then uses lemma *)
/seL4-l4v-master/graph-refine/
H A Dtrace_refute.py11 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:

Completed in 135 milliseconds

1234567