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

1234567

/seL4-l4v-10.1.1/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,
H A DTptp.sml1767 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 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,
H A DTptp.sml1767 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 Dselftest.sml7 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 Dgraph_to_graph.py12 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 Dbench.py19 import graph_refine.problem as problem namespace
46 p = fs[f_name].as_problem(problem.Problem)
H A Dconvert_loop_bounds.py13 import graph_refine.problem as problem namespace
69 except problem.Abort, e:
70 print 'failed to analyse %s, problem aborted' % f
H A Delf_file.py11 import graph_refine.problem as problem namespace
H A Dcall_graph_utils.py12 import graph_refine.problem as problem namespace
/seL4-l4v-10.1.1/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-10.1.1/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-10.1.1/HOL4/src/HolSat/
H A DsatConfig.sml18 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 DmergeGrammarsA1Script.sml36 made as the theories load. Instead, the problem is apparent in the
/seL4-l4v-10.1.1/HOL4/src/HolSmt/
H A DHolSmtLib.sml28 "solver reports 'unknown' (solver not installed/problem too hard?)"
/seL4-l4v-10.1.1/HOL4/src/holyhammer/
H A DhhTranslate.sig35 (* problem *)
/seL4-l4v-10.1.1/graph-refine/
H A Dtrace_refute.py13 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 Droot2Script.sml45 (* The proof moves the problem from R to N, then uses lemma *)
/seL4-l4v-10.1.1/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.

Completed in 138 milliseconds

1234567