Searched refs:solver (Results 1 - 25 of 71) sorted by last modified time

123

/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/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/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/graph-refine/
H A Dtrace_refute.py12 import solver namespace
H A Dstack_logic.py10 import solver namespace
63 val = solver.smt_to_val (expr)
70 (s0, s1) = [solver.smt_num_t (n, typ) for n in [0, 1]]
93 cond_exp = solver.mk_smt_expr (solver.flat_s_expression (cond),
119 addr_x = solver.parse_s_expression (addr_expr)
120 sp_x = solver.parse_s_expression (sp_expr)
190 smt = solver.smt_expr (ptr, env, rep.solv)
200 smt = solver.smt_expr (ptr, pc_env[1], rep.solv)
277 inp_sp = solver
[all...]
H A Dsolver.py14 This tool requires the use of an SMT solver.
20 The .solverlist format is one solver per line, e.g.
22 # SONOLAR is the strongest offline solver in our experiments.
27 # Z3 is a useful online solver. Use of Z3 in offline mode is not recommended,
32 N.B. only ONE online solver is needed, so Z3 is redundant in the above.
37 The name is used to identify the solver. The second token specifies
38 the solver mode. Solvers in "fast" or "online" mode must support all
40 the solver will be executed once per query, and push/pop will not be used.
42 The remainder of each line is a shell command that executes the solver in
44 limit, after which the offline solver wil
235 return '(cannot import psutil, cannot time solver)' namespace
[all...]
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 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 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 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 Dinst_logic.py10 import solver namespace
H A Dgraph-refine.py14 import solver namespace
84 except solver.SolverFailure, e:
96 except solver.SolverFailure, e:
H A Ddebug.py15 import solver namespace
138 print ' %s: %s' % (valid, solver.flat_s_expression (bit))
145 bits = solver.split_hyp_sexpr (cond_def, [])
151 x = solver.smt_expr (x, {}, None)
152 x = solver.parse_s_expression (x)
295 pred = solver.smt_expr (pred, {}, rep.solv)
296 pred = solver.parse_s_expression (pred)
297 bits = solver.split_hyp_sexpr (pred, [])
307 except solver.EnvMiss, e:
323 imp2 = solver
[all...]
H A Dcheck.py16 from solver import to_smt_expr
/seL4-l4v-10.1.1/graph-refine/seL4-example/
H A Dconfigure_default.sh75 if python ../solver.py testq | grep -q 'Solver self-test succ'
81 echo Try python ../solver.py test
89 echo Configured graph-refine to use CVC4 SMT solver.
90 if python ../solver.py testq | grep -q 'Solver self-test succ'
95 echo Try python ../solver.py test
H A DMakefile.common53 SOLV=python ${GREF_ROOT}/solver.py
/seL4-l4v-10.1.1/HOL4/src/tfl/src/
H A DRW.sml803 datatype solver = Solver of simpls -> thm list -> term -> thm; type
813 fun Rewrite Once (Simpls(ss,thl),Context cntxt,Congs congs,Solver solver) =
814 RW_STEPS ONCE_DEPTH (ss,cntxt,congs,solver) thl
816 | Rewrite Fully (Simpls(ss,thl),Context cntxt,Congs congs,Solver solver) =
817 RW_STEPS TOP_DEPTH (ss,cntxt,congs,solver) thl
819 | Rewrite(Special f)(Simpls(ss,thl),Context cntxt,Congs congs,Solver solver) =
820 RW_STEPS f (ss,cntxt,congs,solver) thl
822 | Rewrite Once (Default thl,Context cntxt,Congs congs,Solver solver) =
824 cntxt,congs,solver) thl
826 | Rewrite Once (Pure thl,Context cntxt,Congs congs,Solver solver)
[all...]
H A DRW.sig60 datatype solver = Solver of simpls -> thm list -> term -> thm type
63 val Rewrite :repetitions -> rules*context*congs*solver -> conv
64 val REWRITE_RULE :repetitions -> rules*context*congs*solver -> thm -> thm
65 val ASM_REWRITE_RULE:repetitions -> rules*context*congs*solver -> thm -> thm
66 val REWRITE_TAC :repetitions -> rules*context*congs*solver -> tactic
67 val ASM_REWRITE_TAC :repetitions -> rules*context*congs*solver -> tactic
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/taut/
H A DtautLib.sml3 (* DESCRIPTION : Boolean tautology checking (by SAT solver proof replay) *)
5 (* READS FILES : Temporary files output by SAT solver. Deleted. *)
6 (* WRITES FILES : Temporary input file to solver. Deleted. *)
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DsimpLib.sml46 fun appconv (c,UNBOUNDED) solver stk tm = c false solver stk tm
47 | appconv (c,BOUNDED r) solver stk tm = if !r = 0 then failwith "exceeded rewrite bound"
48 else c true solver stk tm before
206 in fn solver => fn stack => fn tm =>
208 val thm = conv solver stack tm
385 fun applythm solver t (bound, th) = let
402 val scond = solver h
420 fun apply {solver,conv,context,stack,relation = (relation,_)} t = let
431 tryfind (applythm (solver stac
[all...]
H A DsimpLib.sig135 * the solver and the depther to be SIMP_CONV itself.

Completed in 153 milliseconds

123