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

123

/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/
H A DHolSat.tex51 {\tt{HolSatLib}} provides a function {\tt SAT\_PROVE} \index{HolSatLib!SAT\_PROVE@\ml{SAT\_PROVE}} for propositional satisfiability testing and for proving propositional tautologies. It uses an external SAT solver (currently MiniSat 1.14p) to find an unsatisfiability proof or satisfying assignment, and then reconstructs the proof or checks the assignment deductively in \HOL.
53 Alternatively, the function {\tt SAT\_ORACLE} \index{HolSatLib!SAT\_ORACLE@\ml{SAT\_ORACLE}} has the same behaviour as {\tt SAT\_PROVE} but asserts the result of the solver without proof. The theorem thus asserted is tagged with ``{\tt{HolSatLib}}'' to indicate that it is unchecked. Since proof reconstruction can be expensive, the oracle facility can be useful during prototyping, or if proof is not required.
106 {\tt{HolSatLib}} will delete temporary files generated by the SAT solver, such as the proof file and any statistics. This is to avoid accumulating thousands of possibly large files. Currently {\tt HolSatLib} has only been tested on Linux, and on Windows XP using MinGW.
121 The ZChaff SAT solver has a proof production mode and is supported by {\tt{HolSatLib}}. However, the ZChaff end user license is not compatible with the \HOL{} license, so we are unable to distribute it with \HOL{}. If you wish to use ZChaff, download and unpack it in the directory {\tt src/HolSat/sat\_solvers/} under the main \HOL{} directory, and compile it with proof production mode enabled (which is not the default). This should create a binary {\tt zchaff} in the directory {\tt src/HolSat/sat\_solvers/zchaff/}. ZChaff can now be used as the external proof engine instead of MiniSat, by using the HolSatLib functions described above, prefixed with a ``{\tt Z}'', e.g., {\tt ZSAT\_PROVE}.
125 Other SAT solvers are currently not supported. If you would like such support to be added for your favourite solver, please send a feature request via \url{http://github.com/mn200/HOL}.
135 \item{\texttt{solver : SatSolvers.sat\_solver}}
137 The external SAT solver to use. The default is \texttt{SatSolvers.minisatp}. If ZChaff is installed (see \S\ref{subsec:hs_zchaff}), then \texttt{SatSolvers.zchaff} may also be used.
143 The name of a proof trace file. Overrides \texttt{solver} if set. The file must be in the native format of {\tt{HolSatLib}}, and must correspond to a proof for \texttt{infile}, which must also be set. The included version of MiniSat has been modified to produce proofs in the native format, and ZChaff proofs are translated to this format using the included proof translator \texttt{src/HolSat/sat\_solvers/zc2hs} (type \texttt{zc2hs -h} for usage help). \texttt{zc2hs} is used internally by \texttt{ZSAT\_PROVE} etc.
149 If true then \HOL{} will prove the SAT solver's results.
152 A special value \texttt{base\_config~:~sat\_config} is provided for which the term is \texttt{T}, the solver i
[all...]
H A DHolQbf.tex28 \ml{HolQbfLib} uses an external QBF solver, Squolem, to decide
141 solver) to be installed.
181 So far, Squolem is the only QBF solver that has been integrated with
188 The need to install a QBF solver locally poses an entry barrier. It
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DOpening.sml10 solver : term -> thm,
124 Side conditions must be passed to the solver, sub-congruences
145 in fn {relation,solver,depther,freevars} =>
212 val side_condition_thm = solver condition
236 fun EQ_CONGPROC {relation,depther,solver,freevars} tm =
H A DTravrules.sig45 * {solver, depther} -> conv
63 * by the solver provided to the congruence procedure. If they
H A DcongLib.sml155 fun apply {solver,conv,context,stack,relation} tm =
177 fun apply {solver,conv,context,stack,relation as (_, refl)} tm = let
179 {solver=solver,conv=conv,
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 DTraverse.sml40 apply: {solver:term list -> term -> thm,
253 (#apply rdata) {solver=ctxt_solver,
269 solver=(fn tm => ctxt_solver stack tm), (* do not eta-convert! *)
H A DCond_rewr.sml146 fn solver => fn stack => fn tm =>
171 fun solver' condition =
173 val res = solver new_stack condition
179 val condition_thms = map solver' conditions
/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...]
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/
H A DMain.C28 // DIMACS Parser: // Inserts problem into solver.
92 Solver* solver; variable
97 printStats(solver->stats,cpu_time,mem_used);
259 solver = &S;
/seL4-l4v-10.1.1/HOL4/src/HolSat/
H A DminisatParse.sml149 fun parseTrace cl sva nr fname solver vc clauseth lfn proof =
152 else fname^"."^(getSolverName solver)^".proof")
164 fun replayProof sva nr fname solver vc clauseth lfn proof =
167 in case parseTrace cl sva nr fname solver vc clauseth lfn proof of
H A DsatTools.sml59 ** invokeSat solver t
60 ** invokes solver on t and returns SOME s (where s is the satisfying instance
/seL4-l4v-10.1.1/HOL4/examples/PSL/regexp/
H A DregexpTools.sig27 (* Set this to a SAT solver for evaluating the Prefix operator *)
/seL4-l4v-10.1.1/graph-refine/
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 Dgraph-refine.py14 import solver namespace
84 except solver.SolverFailure, e:
96 except solver.SolverFailure, e:
H A Dinst_logic.py10 import solver namespace
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DfolTools.sig52 (* A pure interface to the first-order solver: no normalization *)
/seL4-l4v-10.1.1/HOL4/Manual/Description/
H A DHolQbf.tex28 \ml{HolQbfLib} uses an external QBF solver, Squolem, to decide
144 solver) to be installed.
184 So far, Squolem is the only QBF solver that has been integrated with
191 The need to install a QBF solver locally poses an entry barrier. It
/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/HolSmt/
H A DLibrary.sml18 4 - moreover, temporary files (for communication with the SMT solver) are
19 not removed after solver invocation *)
H A DZ3.sml3 (* Functions to invoke the Z3 SMT solver *)
H A Dselftest.sml52 die ("Test of solver '" ^ name ^ "' failed on term '" ^
59 die ("Test of solver '" ^ name ^ "' failed on term '" ^
69 die ("Test of solver '" ^ name ^ "' failed on term '" ^
74 (message = "solver reports negated term to be 'satisfiable'" orelse
75 message = "solver reports negated term to be 'satisfiable' (model returned)")
79 die ("Test of solver '" ^ name ^ "' failed on term '" ^
/seL4-l4v-10.1.1/HOL4/examples/elliptic/
H A DellipticScript.sml121 fun flexible_solver solver cond =
123 val cond_th = solver cond
128 else raise Bug "flexible_solver: solver didn't prove condition"
141 fn solver => fn tm =>
147 else MP th (flexible_solver solver (rand (rator (concl th))))
154 fun mk_conv solver solver_conv = solver_conv solver
156 fn solver => FIRST_CONV (map (mk_conv solver) solver_convs)
/seL4-l4v-10.1.1/graph-refine/seL4-example/
H A DMakefile.common53 SOLV=python ${GREF_ROOT}/solver.py
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/
H A Dtemporal_deep_simplificationsLib.sml99 fun apply {solver,conv, context,stack,relation} tm = conv' tm;

Completed in 144 milliseconds

123