/seL4-l4v-master/HOL4/src/HolSat/ |
H A D | satConfig.sml | 3 SAT solver 5 SAT solver specific config is in SatSolver.sml 25 solver: sat_solver, (* solver to use *) 28 (* proof trace file in HolSatLib format; overrides solver if SOME*) 34 {pterm = boolSyntax.T, solver = minisatp, infile = NONE, proof = NONE, 41 fun get_solver (c:sat_config) = (#solver c) 58 {pterm = tm, solver = #solver c, infile = #infile c, proof = #proof c, 62 {pterm = #pterm c, solver [all...] |
H A D | minisatProve.sml | 30 fun replay_proof is_proved sva nr in_name solver vc clauseth lfn ntm proof = 32 ((case getSolverPostExe solver of (* post-process proof, if required *) 34 val (fin,fout) = (in_name,in_name^"."^(getSolverName solver)) 37 (getSolverPostRun solver post_exe (fin,fout))) 40 (case replayProof sva nr in_name solver vc clauseth lfn proof of 57 fun invoke_solver solver lfn ntm clauseth cnfv vc is_proved svm sva in_name = 60 if access(getSolverExe solver,[A_EXEC]) then 62 val answer = invokeSat solver T (SOME vc) (SOME nr) svm sva in_name 69 replay_proof is_proved sva nr in_name solver vc clauseth 72 else (* do not have execute access to solver binar [all...] |
H A D | SatSolvers.sml | 6 ** {name (* solver name *) 10 ** notime_run, (* command to invoke solver on a file *) 12 ** post_run, (* transform SAT solver output before reading into HOL *)
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibSolver.sig | 18 (* The type of a generic solver *) 20 type solver = formula list -> thm list option stream type 22 val contradiction_solver : thm -> solver 26 val solved_filter : solver -> solver 27 val subsumed_filter : solver -> solver 31 val solve : solver -> int -> formula list -> thm list list 32 val find : solver -> formula list -> thm list option 33 val refute : solver [all...] |
H A D | mlibMeson.sig | 33 (* The meson solver *) 37 (* The delta preprocessor as a solver *) 41 (* The prolog solver *)
|
H A D | metisTools.sml | 167 type parameters = {interface : Fparm, solver : Mparm, limit : limit}; 172 solver = fo_solver}; 174 fun update_interface f {interface, solver, limit} = 175 {interface = f interface, solver = solver, limit = limit}; 177 fun update_solver f {interface, solver, limit} = 178 {interface = interface, solver = f solver, limit = limit}; 180 fun update_limit f {interface, solver, limit} = 181 {interface = interface, solver [all...] |
H A D | mlibMetis.sig | 21 type solver = mlibSolver.solver type 47 val query : formula -> solver (* Axiomatizes, then runs prolog *)
|
H A D | mlibSolver.sml | 62 (* The type of a generic solver. *) 65 type solver = formula list -> thm list option stream; type 85 fun solved_filter solver goals = 91 drop_after final (solver goals) 145 type node_data = {name : string, solver_con : form -> solver}; 154 (* At each step we schedule a time slice to the least cost solver node. *) 169 (* This allows us to hierarchically arrange solver nodes. *) 186 fun init_subnode (cost, (name, solver : solver)) goal = 191 solns = SOME (fn () => solver goa 333 val solver = value [all...] |
H A D | metisTools.sig | 28 type parameters = {interface : Fparm, solver : Mparm, limit : limit} 35 (* Prolog solver *) 38 (* Metis solver *)
|
/seL4-l4v-master/HOL4/src/HolQbf/ |
H A D | QbfTrace.sml | 12 4 - moreover, temporary files (for communication with the QBF solver) are 13 not removed after solver invocation *)
|
H A D | HolQbfLib.sig | 9 (* Default sat solver is HolSatLib.SAT_PROVE *)
|
H A D | HolQbfLib.sml | 37 certificate of validity generated by the QBF solver Squolem. 51 a certificate of invalidity generated by the QBF solver Squolem. 67 invalidity, respectively) generated by the QBF solver
|
/seL4-l4v-master/HOL4/src/HolSmt/ |
H A D | HolSmtLib.sml | 10 fun GENERIC_SMT_TAC solver goal = 14 case solver goal of 16 raise ERR "solver reports negated term to be 'satisfiable'" 19 "solver reports negated term to be 'satisfiable' (model returned)" 28 "solver reports 'unknown' (solver not installed/problem too hard?)" 30 raise ERR ("solver reports 'unknown' (" ^ message ^ ")") 48 Feedback.HOL_MESG ("HolSmtLib: solver " ^ name ^ " is available.")
|
H A D | SolverSpec.sml | 12 strings that the SMT solver will understand); writes these strings into a 15 the output file generated by the SMT solver); deletes input and output 22 (* call 'pre goal' to generate SMT solver input *) 29 (* the actual system call to the SMT solver *) 40 "HolSmtLib: solver reports negated term to be '" ^ 53 (* if the SMT solver returned a theorem 'thm', then this should be of the 87 the respective SMT solver; simp_tac must produce at most one subgoal *) 92 (* apply the SMT solver anyway, but to the trivial goal ``T`` *)
|
/seL4-l4v-master/graph-refine/seL4-example/ |
H A D | configure_default.sh | 73 if python ../solver.py testq | grep -q 'Solver self-test succ' 79 echo Try python ../solver.py test 87 echo Configured graph-refine to use CVC4 SMT solver. 88 if python ../solver.py testq | grep -q 'Solver self-test succ' 93 echo Try python ../solver.py test
|
/seL4-l4v-master/HOL4/examples/elliptic/ |
H A D | subtypeTools.sml | 51 fun flexible_solver solver cond = 53 val cond_th = solver cond 58 else raise Bug "flexible_solver: solver didn't prove condition" 71 fn solver => fn tm => 77 else MP th (flexible_solver solver (rand (rator (concl th)))) 84 fun mk_conv solver solver_conv = solver_conv solver 86 fn solver => FIRST_CONV (map (mk_conv solver) solver_convs) 182 fn solver [all...] |
H A D | fieldTools.sml | 470 fun left_conv solver tm = 477 field_sub_eq_zero_conv f solver 480 fun right_conv solver tm = 485 field_sub_eq_zero_conv f solver 717 fun field_mult_presimp_conv solver = 721 (QCONV (TRY_CONV (#conv field_mult_ac_conv solver) THENC 724 fun field_mult_postsimp_conv solver = 725 BINOP_CONV (field_mult_presimp_conv solver); 772 fun push_conv solver a_th = 773 RAND_CONV (K a_th) THENC field_mult_comm_conv' solver; [all...] |
/seL4-l4v-master/HOL4/src/tfl/src/ |
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
|
/seL4-l4v-master/graph-refine/ |
H A D | debug.py | 13 import solver namespace 136 print ' %s: %s' % (valid, solver.flat_s_expression (bit)) 143 bits = solver.split_hyp_sexpr (cond_def, []) 149 x = solver.smt_expr (x, {}, None) 150 x = solver.parse_s_expression (x) 293 pred = solver.smt_expr (pred, {}, rep.solv) 294 pred = solver.parse_s_expression (pred) 295 bits = solver.split_hyp_sexpr (pred, []) 305 except solver.EnvMiss, e: 321 imp2 = solver [all...] |
H A D | solver.py | 12 This tool requires the use of an SMT solver. 18 The .solverlist format is one solver per line, e.g. 20 # SONOLAR is the strongest offline solver in our experiments. 25 # Z3 is a useful online solver. Use of Z3 in offline mode is not recommended, 30 N.B. only ONE online solver is needed, so Z3 is redundant in the above. 35 The name is used to identify the solver. The second token specifies 36 the solver mode. Solvers in "fast" or "online" mode must support all 38 the solver will be executed once per query, and push/pop will not be used. 40 The remainder of each line is a shell command that executes the solver in 42 limit, after which the offline solver wil 233 return '(cannot import psutil, cannot time solver)' namespace [all...] |
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | Traverse.sig | 37 * solver: 47 * the congruence side condition solver. 54 * to the solver are made. 59 * under equality. Similar to solver, but does not call EQT_ELIM. 71 apply: {solver:term list -> term -> thm, 82 apply: {solver:term list -> term -> thm,
|
H A D | Cond_rewr.sig | 11 conversion then solves with the solver provided. If any of the 30 Fails if any of the assumptions cannot be solved by the solver,
|
H A D | Opening.sig | 19 * - Use the provided solver to solve side conditions (solver 74 solver : term -> thm,
|
/seL4-l4v-master/HOL4/examples/lambda/barendregt/ |
H A D | reductionEval.sml | 149 fun normorder_step solver t = let 159 val subth = normorder_step solver bdy 168 val isnt_ABS_th = solver (mk_neg(mk_comb(is_abs_t,M1))) 170 case total (normorder_step solver) M1 of 172 val bnf_th = solver (mk_comb(bnf_t,M1)) 173 val subth = normorder_step solver M2 195 fun noreduct_CONV solver t = let 219 val isnt_ABS = solver (mk_neg(mk_comb(is_abs_t, M1))) 246 fun nopath_CONV solver t = let 249 val subth = noreduct_CONV solver (mk_com [all...] |
/seL4-l4v-master/HOL4/examples/misc/ |
H A D | wardScript.sml | 196 fun solver (asl, t) = let function 241 solver, 252 end (asl,t) handle Empty => raise mk_HOL_ERR "wardScript" "solver" "Empty list" 267 solver) 270 srw_tac [][] >> fsrw_tac [][] >> TRY solver >> 272 fsrw_tac [][APPEND_EQ_CONS] >> TRY solver 277 solver
|