/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/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/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/graph-refine/ |
H A D | trace_refute.py | 12 import solver namespace
|
H A D | stack_logic.py | 10 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 D | solver.py | 14 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 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 | 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 | 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 | 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 | inst_logic.py | 10 import solver namespace
|
H A D | graph-refine.py | 14 import solver namespace 84 except solver.SolverFailure, e: 96 except solver.SolverFailure, e:
|
H A D | debug.py | 15 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 D | check.py | 16 from solver import to_smt_expr
|
/seL4-l4v-10.1.1/graph-refine/seL4-example/ |
H A D | configure_default.sh | 75 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 D | Makefile.common | 53 SOLV=python ${GREF_ROOT}/solver.py
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | RW.sml | 803 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 D | RW.sig | 60 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 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/taut/ |
H A D | tautLib.sml | 3 (* 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 D | simpLib.sml | 46 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 D | simpLib.sig | 135 * the solver and the depther to be SIMP_CONV itself.
|