Searched refs:Solver (Results 1 - 13 of 13) sorted by path
| /seL4-l4v-10.1.1/HOL4/examples/elliptic/ |
| H A D | subtypeTools.sig | 9 (* Solver conversions. *)
|
| H A D | subtypeTools.sml | 112 (* Solver conversions. *)
|
| /seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
| H A D | Main.C | 20 #include "Solver.h"
32 void addLit(int parsed_lit,Solver& S, vec<Lit>& lits) {
38 void addClause(Solver& S, vec<Lit>& lits) {
46 static void parse_DIMACS(char* filename, Solver& S) {
92 Solver* solver;
242 Solver S;
301 // (faster than "return", which will invoke the destructor for 'Solver')
|
| H A D | Solver.C | 0 /****************************************************************************************[Solver.C]
20 #include "Solver.h"
62 void Solver::newClause(const vec<Lit>& ps_, bool learnt, ClauseId id)
151 void Solver::remove(Clause* c, bool just_dealloc)
171 bool Solver::simplify(Clause* c) const
189 Var Solver::newVar() {
207 bool Solver::assume(Lit p) {
213 void Solver::cancelUntil(int level) {
254 void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel)
372 bool Solver
[all...] |
| H A D | Solver.h | 0 /****************************************************************************************[Solver.h]
32 // Solver -- the main class:
49 class Solver { class
51 // Solver state:
127 Solver() : ok (true) function in class:Solver
151 ~Solver() {
175 Proof* proof; // Set this directly after constructing 'Solver' to enable proof logging. Initialized to NULL.
|
| /seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
| H A D | Defn.sml | 525 RW.Solver (solver (mk_restr p, f, FV', nested_ref)))
|
| H A D | RW.sig | 60 datatype solver = Solver of simpls -> thm list -> term -> thm
|
| H A D | RW.sml | 803 datatype solver = Solver of simpls -> thm list -> term -> thm;
813 fun Rewrite Once (Simpls(ss,thl),Context cntxt,Congs congs,Solver solver) =
816 | Rewrite Fully (Simpls(ss,thl),Context cntxt,Congs congs,Solver solver) =
819 | Rewrite(Special f)(Simpls(ss,thl),Context cntxt,Congs congs,Solver solver) =
822 | Rewrite Once (Default thl,Context cntxt,Congs congs,Solver solver) =
826 | Rewrite Once (Pure thl,Context cntxt,Congs congs,Solver solver) =
829 | Rewrite Fully (Default thl,Context cntxt,Congs congs,Solver solver) =
833 | Rewrite Fully (Pure thl,Context cntxt,Congs congs,Solver solver) =
836 | Rewrite (Special f) (Default thl,Context cntxt,Congs congs,Solver solver) =
839 | Rewrite (Special f) (Pure thl,Context cntxt,Congs congs,Solver solve
[all...] |
| H A D | Rules.sml | 18 Solver always_fails)
|
| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | logic.py | 1072 eval_expr_solver[0] = solver.Solver ()
|
| H A D | rep_graph.py | 9 from solver import Solver, merge_envs_pcs, smt_expr, mk_smt_expr, to_smt_expr namespace
781 solv = Solver (produce_unsat_cores
1226 def mk_graph_slice (p, inliner = None, fast = False, mk_solver = Solver):
|
| H A D | solver.py | 704 class Solver: class in inherits:
2165 solv = Solver ()
2186 solv = Solver ()
2204 print 'Solver self-test successful'
|
| /seL4-l4v-10.1.1/graph-refine/seL4-example/ |
| H A D | Makefile.common | 55 SOLV_TEST_SUCC='Solver self-test succ'
58 $(if ${SOLV_TEST},,$(error Solver self-test failed (${SOLV} test)))
|
Completed in 139 milliseconds