Searched refs:solver (Results 1 - 25 of 73) sorted by relevance

123

/seL4-l4v-master/HOL4/src/HolSat/
H A DsatConfig.sml3 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 DminisatProve.sml30 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 DSatSolvers.sml6 ** {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 DmlibSolver.sig18 (* 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 DmlibMeson.sig33 (* The meson solver *)
37 (* The delta preprocessor as a solver *)
41 (* The prolog solver *)
H A DmetisTools.sml167 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 DmlibMetis.sig21 type solver = mlibSolver.solver type
47 val query : formula -> solver (* Axiomatizes, then runs prolog *)
H A DmlibSolver.sml62 (* 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 DmetisTools.sig28 type parameters = {interface : Fparm, solver : Mparm, limit : limit}
35 (* Prolog solver *)
38 (* Metis solver *)
/seL4-l4v-master/HOL4/src/HolQbf/
H A DQbfTrace.sml12 4 - moreover, temporary files (for communication with the QBF solver) are
13 not removed after solver invocation *)
H A DHolQbfLib.sig9 (* Default sat solver is HolSatLib.SAT_PROVE *)
H A DHolQbfLib.sml37 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 DHolSmtLib.sml10 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 DSolverSpec.sml12 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 Dconfigure_default.sh73 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 DsubtypeTools.sml51 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 DfieldTools.sml470 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 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
/seL4-l4v-master/graph-refine/
H A Ddebug.py13 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 Dsolver.py12 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 DTraverse.sig37 * 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 DCond_rewr.sig11 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 DOpening.sig19 * - Use the provided solver to solve side conditions (solver
74 solver : term -> thm,
/seL4-l4v-master/HOL4/examples/lambda/barendregt/
H A DreductionEval.sml149 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 DwardScript.sml196 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

Completed in 91 milliseconds

123