Skip to content

Commit

Permalink
edit bash scripts to receive env vars
Browse files Browse the repository at this point in the history
  • Loading branch information
bsubercaseaux committed Jun 9, 2024
1 parent 8b93998 commit d74e35b
Show file tree
Hide file tree
Showing 2 changed files with 7 additions and 6 deletions.
7 changes: 3 additions & 4 deletions cube_checking/solve_cube.sh
Original file line number Diff line number Diff line change
@@ -1,10 +1,9 @@
#!/usr/bin/env sh
#!/bin/sh
# Receives the desired cube number as $1

gcc 6hole-cube.c -o cube_gen
./cube_gen $1 vars.out > .tmp_cube_$1
python3 cube_join.py -f 6-30.cnf -c .tmp_cube_$1 -o with_cube_$1.cnf
cadical with_cube_$1.cnf proof_cube_$1.lrat --lrat
cake_lpr with_cube_$1.cnf proof_cube_$1.lrat
${CADICAL:-cadical} with_cube_$1.cnf proof_cube_$1.lrat --lrat
${CAKELPR:-cake_lpr} with_cube_$1.cnf proof_cube_$1.lrat

rm with_cube_$1.cnf proof_cube_$1.lrat .tmp_cube_$1
6 changes: 4 additions & 2 deletions cube_checking/verify_tautology.sh
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
#!/bin/sh

gcc 6hole-cube.c -o cube_gen
./cube_gen 0 vars.out > cubes.icnf
python3 cube_join.py -f 6-30.cnf -c cubes.icnf --tautcheck -o taut_if_unsat.cnf
cadical taut_if_unsat.cnf tautology_proof.lrat --lrat
cake_lpr taut_if_unsat.cnf tautology_proof.lrat
${CADICAL:-cadical} taut_if_unsat.cnf tautology_proof.lrat --lrat
${CAKELPR:-cake_lpr} taut_if_unsat.cnf tautology_proof.lrat

0 comments on commit d74e35b

Please sign in to comment.