/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | folTools.sml | 482 val solver = value 483 timed_fn "solver initialization" 499 (mlibStream.map timed_lift (timed_stream (fn () => solver q) ()))
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | loop_bounds.py | 1 import check,search,problem,syntax,solver,logic,rep_graph,re namespace 556 except solver.SolverFailure, e: 572 except solver.SolverFailure, e:
|
H A D | rep_graph.py | 9 from solver import Solver, merge_envs_pcs, smt_expr, mk_smt_expr, to_smt_expr 14 import solver namespace 623 r_x = solver.parse_s_expression (r) 879 mem_sexpr = solver.parse_s_expression (mem_sexpr) 1227 trace ('rep_graph setting up solver', push = 1) 1229 trace ('rep_graph setting up solver', push = -1)
|
H A D | logic.py | 1071 import solver namespace 1072 eval_expr_solver[0] = solver.Solver () 1223 import solver namespace 1237 if solver.typ_representable (lhs.typ)
|
H A D | search.py | 9 import solver namespace 10 from solver import mk_smt_expr, to_smt_expr, smt_expr 434 # mem eqs each time which is important for the solver 467 result = solver.smt_to_val (s) 592 s = solver.smt_expr (v, {}, solv) 593 s_x = solver.parse_s_expression (s)
|
H A D | trace_refute.py | 12 import solver namespace
|
H A D | check.py | 16 from solver import to_smt_expr
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Nitpick/document/ |
H A D | root.tex | 2052 option is useful to determine which scopes are tried or which SAT solver is 2092 value greater than 1, you will need an incremental SAT solver, such as 2101 this option to a value greater than 1, you will need an incremental SAT solver, 2181 Specifies which SAT solver to use. SAT solvers implemented in C or \cpp{} tend 2185 you will need an incremental SAT solver, such as \textit{MiniSat\_JNI} 2193 Lingeling is an efficient solver written in C. The JNI (Java Native Interface) 2213 \item[\labelitemi] \textbf{\textit{MiniSat}:} MiniSat is an efficient solver 2228 \item[\labelitemi] \textbf{\textit{Riss3g}:} Riss3g is an efficient solver written in 2236 \item[\labelitemi] \textbf{\textit{zChaff}:} zChaff is an older solver written 2244 \item[\labelitemi] \textbf{\textit{RSat}:} RSat is an efficient solver writte [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Nitpick/document/ |
H A D | root.tex | 2052 option is useful to determine which scopes are tried or which SAT solver is 2092 value greater than 1, you will need an incremental SAT solver, such as 2101 this option to a value greater than 1, you will need an incremental SAT solver, 2181 Specifies which SAT solver to use. SAT solvers implemented in C or \cpp{} tend 2185 you will need an incremental SAT solver, such as \textit{MiniSat\_JNI} 2193 Lingeling is an efficient solver written in C. The JNI (Java Native Interface) 2213 \item[\labelitemi] \textbf{\textit{MiniSat}:} MiniSat is an efficient solver 2228 \item[\labelitemi] \textbf{\textit{Riss3g}:} Riss3g is an efficient solver written in 2236 \item[\labelitemi] \textbf{\textit{zChaff}:} zChaff is an older solver written 2244 \item[\labelitemi] \textbf{\textit{RSat}:} RSat is an efficient solver writte [all...] |
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | simpLib.sig | 135 * the solver and the depther to be SIMP_CONV itself.
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/poly/ |
H A D | holfoot_command_line.sml | 29 val s = " --yices use the Yices SMT-solver (default off)\n\n";
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Sledgehammer/document/ |
H A D | root.tex | 204 Since Z3's output format is somewhat unstable, other versions of the solver 207 \texttt{Z3\_VERSION} to the solver's version number (e.g., ``4.4.0''). 595 higher-order ATP or an SMT solver. 747 \item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by 832 SMT solver developed by David D\'eharbe, Pascal Fontaine, and their colleagues. 838 \item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Sledgehammer/document/ |
H A D | root.tex | 204 Since Z3's output format is somewhat unstable, other versions of the solver 207 \texttt{Z3\_VERSION} to the solver's version number (e.g., ``4.4.0''). 595 higher-order ATP or an SMT solver. 747 \item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by 832 SMT solver developed by David D\'eharbe, Pascal Fontaine, and their colleagues. 838 \item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
|
/seL4-l4v-10.1.1/HOL4/examples/elliptic/ |
H A D | fieldScript.sml | 1927 fun left_conv solver tm = 1934 field_sub_eq_zero_conv f solver 1937 fun right_conv solver tm = 1945 field_sub_eq_zero_conv f solver
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/ |
H A D | dimacsTools.sml | 223 ** for last invocation of a SAT solver
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | Defn.sml | 494 fun solver (restrf,f,G,nref) _ context tm = function 504 then (nref := true; raise ERR "solver" "nested function") 525 RW.Solver (solver (mk_restr p, f, FV', nested_ref)))
|
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | Yices.sml | 3 (* Functions to invoke the Yices SMT solver *)
|
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
H A D | patternMatchesLib.sml | 33 fun apply {solver,conv,context,stack,relation} tm = (
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics_ZF/document/ |
H A D | ZF.tex | 1434 %approach. Call the simplifier with a new solver expressed using
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics_ZF/document/ |
H A D | ZF.tex | 1434 %approach. Call the simplifier with a new solver expressed using
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
H A D | libraries.tex | 2775 apply : {solver : term list -> term -> thm,
|