Searched refs:solver (Results 51 - 71 of 71) sorted by relevance

123

/seL4-l4v-10.1.1/HOL4/src/metis/
H A DfolTools.sml482 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 Dloop_bounds.py1 import check,search,problem,syntax,solver,logic,rep_graph,re namespace
556 except solver.SolverFailure, e:
572 except solver.SolverFailure, e:
H A Drep_graph.py9 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 Dlogic.py1071 import solver namespace
1072 eval_expr_solver[0] = solver.Solver ()
1223 import solver namespace
1237 if solver.typ_representable (lhs.typ)
H A Dsearch.py9 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 Dtrace_refute.py12 import solver namespace
H A Dcheck.py16 from solver import to_smt_expr
/seL4-l4v-10.1.1/isabelle/src/Doc/Nitpick/document/
H A Droot.tex2052 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 Droot.tex2052 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 DsimpLib.sig135 * the solver and the depther to be SIMP_CONV itself.
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/poly/
H A Dholfoot_command_line.sml29 val s = " --yices use the Yices SMT-solver (default off)\n\n";
/seL4-l4v-10.1.1/isabelle/src/Doc/Sledgehammer/document/
H A Droot.tex204 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 Droot.tex204 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 DfieldScript.sml1927 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 DdimacsTools.sml223 ** for last invocation of a SAT solver
/seL4-l4v-10.1.1/HOL4/src/tfl/src/
H A DDefn.sml494 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 DYices.sml3 (* Functions to invoke the Yices SMT solver *)
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/
H A DpatternMatchesLib.sml33 fun apply {solver,conv,context,stack,relation} tm = (
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics_ZF/document/
H A DZF.tex1434 %approach. Call the simplifier with a new solver expressed using
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics_ZF/document/
H A DZF.tex1434 %approach. Call the simplifier with a new solver expressed using
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/
H A Dlibraries.tex2775 apply : {solver : term list -> term -> thm,

Completed in 218 milliseconds

123