/dports/lang/yorick/yorick-y_2_2_04/drat/ |
H A D | Makefile | 10 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 D | sat_unsat.sh | 28 ./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 D | ballofcrystal.sh | 136 …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 D | sat_unsat.sh | 28 ./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 D | ballofcrystal.sh | 136 …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 D | sat_drat.cpp | 27 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 D | sat_drat.cpp | 27 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 D | test_colcheck.R | 7 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 D | tbl-format.md | 38 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 D | completedetachreattacher.cpp | 41 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 D | intree.cpp | 89 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 D | varreplacer.cpp | 384 (*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 D | completedetachreattacher.cpp | 41 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 D | intree.cpp | 89 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 D | varreplacer.cpp | 384 (*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 D | instally.sh | 112 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 | .gitignore | 28 # 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 D | drat_frontend.cpp | 21 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 D | build_drat-trim2.sh | 22 git clone https://github.com/msoos/drat-trim.git 23 cd drat-trim
|
/dports/math/cryptominisat/cryptominisat-5.8.0/scripts/aws/ |
H A D | build_drat-trim2.sh | 22 git clone https://github.com/msoos/drat-trim.git 23 cd drat-trim
|
/dports/math/py-cryptominisat/cryptominisat-5.8.0/ |
H A D | .gitmodules | 23 [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 | .gitmodules | 23 [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 D | Discretize.cpp | 34 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 D | drat_frontend.cpp | 21 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 D | t007 | 79 (define (drat! s . args) 93 (drat! "no error output")) 96 (drat! "unexpected error output:~%-| ~A" line))) 99 (drat! "missing file: ~A" fn)))
|