Home
last modified time | relevance | path

Searched refs:drat (Results 1 – 25 of 309) sorted by relevance

12345678910>>...13

/dports/lang/yorick/yorick-y_2_2_04/drat/
H A DMakefile10 PKG_NAME=drat
12 PKG_I=drat.i
14 OBJS=bound.o track.o trans.o drat.o ydrat.o
16 PKG_CLEAN=../i0/drat.i
44 drat.o: drat.h trans.h track.h bound.h
45 ydrat.o: drat.h trans.h track.h bound.h $(H_YDRAT)
47 ../i0/drat.i: drat.i
48 cp -f drat.i ../i0/drat.i
52 preexe: $(PKG_LIB) ../i0/drat.i
58 postdll: $(PKG_DLL) ../i0/drat.i
/dports/math/py-cryptominisat/cryptominisat-5.8.0/scripts/crystal/
H A Dsat_unsat.sh28 ./cryptominisat5 --zero-exit-status --dumpdecformodel b tmp drat.out > out.sat
37 ./tests/drat-trim/drat-trim final.cnf drat.out |tee out.drat
38 grep "VERIFIED" out.drat
39 grep "resol.*steps" out.drat
65 ./tests/drat-trim/drat-trim final.cnf drat.out |tee out.drat
66 grep "VERIFIED" out.drat || exit -1
67 grep "resol.*steps" out.drat
H A Dballofcrystal.sh136 …RATIO" --cllockdatagen 0.5 --clid --sql 2 --sqlitedb "$FNAMEOUT.db-raw" --drat "$FNAMEOUT.drat" --…
147 ../utils/drat-trim/drat-trim "../$FNAME" "$FNAMEOUT.drat" -o "$FNAMEOUT.usedCls" -i
155 ../tests/drat-trim/drat-trim final_good.cnf "$FNAMEOUT.drat" -o "$FNAMEOUT.usedCls" -i
/dports/math/cryptominisat/cryptominisat-5.8.0/scripts/crystal/
H A Dsat_unsat.sh28 ./cryptominisat5 --zero-exit-status --dumpdecformodel b tmp drat.out > out.sat
37 ./tests/drat-trim/drat-trim final.cnf drat.out |tee out.drat
38 grep "VERIFIED" out.drat
39 grep "resol.*steps" out.drat
65 ./tests/drat-trim/drat-trim final.cnf drat.out |tee out.drat
66 grep "VERIFIED" out.drat || exit -1
67 grep "resol.*steps" out.drat
H A Dballofcrystal.sh136 …RATIO" --cllockdatagen 0.5 --clid --sql 2 --sqlitedb "$FNAMEOUT.db-raw" --drat "$FNAMEOUT.drat" --…
147 ../utils/drat-trim/drat-trim "../$FNAME" "$FNAMEOUT.drat" -o "$FNAMEOUT.usedCls" -i
155 ../tests/drat-trim/drat-trim final_good.cnf "$FNAMEOUT.drat" -o "$FNAMEOUT.usedCls" -i
/dports/math/z3/z3-z3-4.8.13/src/sat/
H A Dsat_drat.cpp27 drat::drat(solver& s) : in drat() function in sat::drat
45 drat::~drat() { in ~drat()
60 void drat::updt_config() { in updt_config()
145 void drat::dump_activity() { in dump_activity()
269 void drat::def_end() { in def_end()
282 …bool drat::is_clause(clause& c, literal l1, literal l2, literal l3, drat::status st1, drat::status…
362 void drat::declare(literal l) { in declare()
663 void drat::assign(literal l) { in assign()
744 void drat::add() { in add()
825 void drat::del(literal l) { in del()
[all …]
/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/
H A Dsat_drat.cpp27 drat::drat(solver& s) : in drat() function in sat::drat
46 drat::~drat() { in ~drat()
62 void drat::updt_config() { in updt_config()
147 void drat::dump_activity() { in dump_activity()
275 void drat::def_end() { in def_end()
288 …bool drat::is_clause(clause& c, literal l1, literal l2, literal l3, drat::status st1, drat::status…
368 void drat::declare(literal l) { in declare()
671 void drat::assign(literal l) { in assign()
752 void drat::add() { in add()
833 void drat::del(literal l) { in del()
[all …]
/dports/math/R-cran-recipes/recipes/tests/testthat/
H A Dtest_colcheck.R7 rp2 <- recipe(mtcars, cyl ~ mpg + drat)
12 expect_error(rp2 %>% check_cols(cyl, mpg, drat) %>% prep(), NA)
22 expect_error(rp2 %>% check_cols(cyl, mpg, drat) %>% prep %>% bake(mtcars), NA)
23 expect_equal(rp2 %>% check_cols(cyl, mpg, drat) %>% prep %>% bake(mtcars),
27 expect_error(rp2 %>% check_cols(cyl, mpg, drat) %>% prep %>%
/dports/devel/R-cran-pillar/pillar/tests/testthat/_snaps/
H A Dtbl-format.md38 mpg cyl disp hp drat wt qsec vs am gear carb
67 # drat <dbl>, wt <dbl>,
75 mpg cyl disp hp drat wt qsec vs am gear carb
112 mpg cyl disp hp drat wt qsec vs am gear carb
153 mpg cyl disp hp drat wt
171 mpg cyl disp hp drat wt
203 # drat <dbl>, wt <dbl>, ...
208 mpg cyl disp hp drat wt qsec vs am gear carb
225 mpg cyl disp hp drat wt qsec vs am gear carb
242 mpg cyl disp hp drat wt qsec vs am gear carb
/dports/math/py-cryptominisat/cryptominisat-5.8.0/src/
H A Dcompletedetachreattacher.cpp41 assert(!solver->drat->something_delayed());
98 assert(!solver->drat->something_delayed());
138 assert(!solver->drat->something_delayed());
166 (*solver->drat) << deldelay << ps << fin;
179 (*solver->drat) << findelay;
190 (*solver->drat) << add << *cl
196 solver->drat->forget_delay();
H A Dintree.cpp89 assert(!(solver->timedOutPropagateFull && solver->drat->enabled())); in check_timeout_due_to_hyperbin()
93 && !(solver->drat->enabled() || solver->conf.simulate_drat) in check_timeout_due_to_hyperbin()
339 if (!solver->drat->enabled() && in handle_lit_popped_from_queue()
386 *(solver->drat) << add << lit in empty_failed_list()
397 *(solver->drat) << add << ~lit in empty_failed_list()
404 *(solver->drat) << add in empty_failed_list()
H A Dvarreplacer.cpp384 (*solver->drat) << add << lit2 in updateBin()
415 (*solver->drat) in updateBin()
525 assert(!solver->drat->something_delayed()); in replace_set()
557 solver->drat->forget_delay(); in replace_set()
616 (*solver->drat) << findelay; in handleUpdatedClause()
623 (*solver->drat) << add << c in handleUpdatedClause()
781 (*solver->drat) in handleAlreadyReplaced()
825 (*solver->drat) in replace_vars_already_set()
861 (*solver->drat) << add << toEnqueue in handleOneSet()
896 (*solver->drat) in replace()
[all …]
/dports/math/cryptominisat/cryptominisat-5.8.0/src/
H A Dcompletedetachreattacher.cpp41 assert(!solver->drat->something_delayed()); in detach_nonbins_nontris()
98 assert(!solver->drat->something_delayed()); in reattachLongs()
138 assert(!solver->drat->something_delayed()); in cleanAndAttachClauses()
166 (*solver->drat) << deldelay << ps << fin; in clean_clause()
179 (*solver->drat) << findelay; in clean_clause()
190 (*solver->drat) << add << *cl in clean_clause()
196 solver->drat->forget_delay(); in clean_clause()
H A Dintree.cpp89 assert(!(solver->timedOutPropagateFull && solver->drat->enabled())); in check_timeout_due_to_hyperbin()
93 && !(solver->drat->enabled() || solver->conf.simulate_drat) in check_timeout_due_to_hyperbin()
339 if (!solver->drat->enabled() && in handle_lit_popped_from_queue()
386 *(solver->drat) << add << lit in empty_failed_list()
397 *(solver->drat) << add << ~lit in empty_failed_list()
404 *(solver->drat) << add in empty_failed_list()
H A Dvarreplacer.cpp384 (*solver->drat) << add << lit2 in updateBin()
415 (*solver->drat) in updateBin()
525 assert(!solver->drat->something_delayed()); in replace_set()
557 solver->drat->forget_delay(); in replace_set()
616 (*solver->drat) << findelay; in handleUpdatedClause()
623 (*solver->drat) << add << c in handleUpdatedClause()
781 (*solver->drat) in handleAlreadyReplaced()
825 (*solver->drat) in replace_vars_already_set()
861 (*solver->drat) << add << toEnqueue in handleOneSet()
896 (*solver->drat) in replace()
[all …]
/dports/lang/yorick/yorick-y_2_2_04/
H A Dinstally.sh112 if test -r drat/libdrat.a; then
113 cp -f drat/libdrat.a "$Y_HOME/lib"
121 if test -r drat/drat$PLUG_SFX; then
122 $YNSTALL $YGP drat/drat$PLUG_SFX "$Y_HOME/lib"
H A D.gitignore28 # files copied from drat/ and hex/ during build
29 i0/drat.i
/dports/math/py-z3-solver/z3-z3-4.8.10/src/shell/
H A Ddrat_frontend.cpp21 sat::drat& m_drat;
139 smt_checker(sat::drat& drat, expr_ref_vector const& b2e): in smt_checker() argument
140 m(b2e.m()), m_drat(drat), m_b2e(b2e), m_fresh_exprs(m), m_core(m), m_inputs(m) { in smt_checker()
268 dimacs::drat_parser drat(ins, std::cerr); in verify_smt() local
276 drat.set_read_theory(read_theory); in verify_smt()
281 sat::drat drat_checker(solver); in verify_smt()
294 for (auto const& r : drat) { in verify_smt()
/dports/math/py-cryptominisat/cryptominisat-5.8.0/scripts/aws/
H A Dbuild_drat-trim2.sh22 git clone https://github.com/msoos/drat-trim.git
23 cd drat-trim
/dports/math/cryptominisat/cryptominisat-5.8.0/scripts/aws/
H A Dbuild_drat-trim2.sh22 git clone https://github.com/msoos/drat-trim.git
23 cd drat-trim
/dports/math/py-cryptominisat/cryptominisat-5.8.0/
H A D.gitmodules23 [submodule "utils/drat-trim"]
24 path = utils/drat-trim
25 url = https://github.com/msoos/drat-trim
/dports/math/cryptominisat/cryptominisat-5.8.0/
H A D.gitmodules23 [submodule "utils/drat-trim"]
24 path = utils/drat-trim
25 url = https://github.com/msoos/drat-trim
/dports/science/axom/axom-0.6.1/src/axom/quest/
H A DDiscretize.cpp34 double drat = sphere.getRadius() * dist / (dist2 + PTINY); in project_to_shape() local
35 double dratc = drat - 1.0; in project_to_shape()
36 return Point3D::make_point(drat * p[0] - dratc * ctr[0], in project_to_shape()
37 drat * p[1] - dratc * ctr[1], in project_to_shape()
38 drat * p[2] - dratc * ctr[2]); in project_to_shape()
/dports/math/z3/z3-z3-4.8.13/src/shell/
H A Ddrat_frontend.cpp21 sat::drat& m_drat;
144 smt_checker(sat::drat& drat, expr_ref_vector const& b2e): in smt_checker() argument
145 m(b2e.m()), m_drat(drat), m_b2e(b2e), m_fresh_exprs(m), m_core(m), m_inputs(m) { in smt_checker()
316 dimacs::drat_parser drat(ins, std::cerr); in verify_smt() local
324 drat.set_read_theory(read_theory); in verify_smt()
329 sat::drat drat_checker(solver); in verify_smt()
342 for (auto const& r : drat) { in verify_smt()
/dports/net/serveez/serveez-0.2.2/test/
H A Dt00779 (define (drat! s . args)
93 (drat! "no error output"))
96 (drat! "unexpected error output:~%-| ~A" line)))
99 (drat! "missing file: ~A" fn)))

12345678910>>...13