Searched refs:Problem (Results 1 - 25 of 36) sorted by last modified time

12

/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A Dselftest.sml36 (* Problem data. *)
H A Dproblems2tptp.sml15 (* Problem data. *)
80 Tptp.Problem
H A Dmetis.sml164 else TextIO.print ("Problem: " ^ filename ^ "\n\n");
177 else TextIO.print ("Clauses:\n" ^ Problem.toString cls ^ "\n\n");
186 val {clauses,literals,symbols,typedSymbols} = Problem.size cls
200 val cat = Problem.categorize cls
202 TextIO.print ("Category: " ^ Problem.categoryToString cat ^ ".\n\n")
221 Tptp.Problem
355 val Tptp.Problem {includes = i, formulas = f, ...} =
369 val Tptp.Problem {comments,includes,formulas} = problem
380 Tptp.Problem
H A DTptp.sml1768 Problem of
1773 fun hasCnfConjecture (Problem {formulas,...}) =
1776 fun hasFofConjecture (Problem {formulas,...}) =
1779 fun hasConjecture (Problem {formulas,...}) =
1782 fun freeVars (Problem {formulas,...}) = freeVarsListFormula formulas;
1831 Problem
1839 {problem : Problem.problem,
2009 fun goal (Problem {formulas,...}) =
2030 fun normalize (Problem {formulas,...}) =
2110 Problem
2142 val Problem {comments,includes,formulas} = problem value
2540 val Problem {formulas,...} = problem value
[all...]
H A DTptp.sig183 Problem of
199 problem : Problem.problem} -> problem
204 problem : Problem.problem,
H A DProblem.sml6 structure Problem :> Problem = structure
H A DProblem.sig6 signature Problem = signature
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A Dselftest.sml36 (* Problem data. *)
H A Dproblems2tptp.sml15 (* Problem data. *)
80 Tptp.Problem
H A Dmetis.sml164 else TextIO.print ("Problem: " ^ filename ^ "\n\n");
177 else TextIO.print ("Clauses:\n" ^ Problem.toString cls ^ "\n\n");
186 val {clauses,literals,symbols,typedSymbols} = Problem.size cls
200 val cat = Problem.categorize cls
202 TextIO.print ("Category: " ^ Problem.categoryToString cat ^ ".\n\n")
221 Tptp.Problem
355 val Tptp.Problem {includes = i, formulas = f, ...} =
369 val Tptp.Problem {comments,includes,formulas} = problem
380 Tptp.Problem
H A DTptp.sml1768 Problem of
1773 fun hasCnfConjecture (Problem {formulas,...}) =
1776 fun hasFofConjecture (Problem {formulas,...}) =
1779 fun hasConjecture (Problem {formulas,...}) =
1782 fun freeVars (Problem {formulas,...}) = freeVarsListFormula formulas;
1831 Problem
1839 {problem : Problem.problem,
2009 fun goal (Problem {formulas,...}) =
2030 fun normalize (Problem {formulas,...}) =
2110 Problem
2142 val Problem {comments,includes,formulas} = problem value
2540 val Problem {formulas,...} = problem value
[all...]
H A DTptp.sig183 Problem of
199 problem : Problem.problem} -> problem
204 problem : Problem.problem,
H A DProblem.sml6 structure Problem :> Problem = structure
H A DProblem.sig6 signature Problem = signature
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/
H A DMakefile74 src/Problem.sig src/Problem.sml \
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/
H A DMakefile74 src/Problem.sig src/Problem.sml \
/seL4-l4v-10.1.1/isabelle/src/Doc/Sledgehammer/document/
H A Droot.tex1054 \subsection{Problem Encoding}
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Sledgehammer/document/
H A Droot.tex1054 \subsection{Problem Encoding}
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/
H A DLK.tex456 can be solved automatically. Problem~39 concerns set theory, asserting
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics/document/
H A DLK.tex456 can be solved automatically. Problem~39 concerns set theory, asserting
/seL4-l4v-10.1.1/graph-refine/
H A Dtrace_refute.py130 p = problem.Problem (None, name = ', '.join(fnames))
349 p = functions[f].as_problem (problem.Problem)
374 p = functions[fname].as_problem (problem.Problem)
399 p = functions[fname].as_problem (problem.Problem)
H A Dsyntax.py846 def as_problem (self, Problem, name = 'temp'):
847 p = Problem(None, 'Function (%s)' % self.name)
859 def compile_hints (self, Problem):
862 p = self.as_problem (Problem)
H A Dstack_logic.py640 p = fun.as_problem (problem.Problem, name = 'Target')
728 p = fun.as_problem (problem.Problem, name = 'Target')
881 p = problem.Problem (None, name = 'Recursion Test')
H A Dproblem.py23 class Problem: class in inherits:
27 self.name = 'Problem (%s)' % name
371 ss = ['Problem']
486 assert lines[0] == 'Problem', lines[0]
490 p = Problem (pairing = None, name = name)
745 trace ('Problem size now %d' % len(p.nodes))
793 p = f.as_problem (Problem)
H A Dloop_bounds.py655 p = functions[fname].as_problem (problem.Problem)
764 p = functions[fname].as_problem (problem.Problem)
882 p = fun.as_problem (problem.Problem)

Completed in 138 milliseconds

12