Merge pull request #1443 from GaloisInc/at-external-aig-slash

Allow slashes in `write_aig_external` filenames Closes #1438
GaloisInc · Sep 1, 2021 · 91c5148 · 91c5148
2 parents 354cda0 + 6b51c13
commit 91c5148
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 6 deletions.
diff --git a/intTests/test_external_abc/test.saw b/intTests/test_external_abc/test.saw
@@ -16,16 +16,16 @@ let q_unsat = {{ \(x:[8]) -> x != 0 /\ x+x == x }};
 
 write_verilog "write_verilog_unsat.v" q_unsat;
 write_smtlib2_w4 "write_smtlib2_w4_unsat.smt2" q_unsat;
-write_aig_external "write_aig_external_unsat.aig" q_unsat;
-write_cnf_external "write_aig_external_unsat.cnf" q_unsat;
+write_aig_external "./write_aig_external_unsat.aig" q_unsat;
+write_cnf_external "./write_aig_external_unsat.cnf" q_unsat;
 
 // A formula that is satisfiable.
 let q_sat = {{ \(x:[8]) -> x+x == x }};
 
 write_verilog "write_verilog_sat.v" q_sat;
 write_smtlib2_w4 "write_smtlib2_w4_sat.smt2" q_sat;
-write_aig_external "write_aig_external_sat.aig" q_sat;
-write_cnf_external "write_aig_external_sat.cnf" q_sat;
+write_aig_external "./write_aig_external_sat.aig" q_sat;
+write_cnf_external "./write_aig_external_sat.cnf" q_sat;
 
 fails (prove_print sbv_abc q_sat);
 fails (prove_print w4_abc_smtlib2 q_sat);

diff --git a/src/SAWScript/Prover/Exporter.hs b/src/SAWScript/Prover/Exporter.hs
@@ -56,6 +56,7 @@ import qualified Data.Map as Map
 import Data.Set (Set)
 import qualified Data.SBV.Dynamic as SBV
 import System.Directory (removeFile)
+import System.FilePath (takeBaseName)
 import System.IO
 import System.IO.Temp(emptySystemTempFile)
 import Data.Text (pack)
@@ -148,8 +149,8 @@ writeAIG f t = do
      io $ AIG.writeAiger f aig
 
 withABCVerilog :: FilePath -> Term -> (FilePath -> String) -> TopLevel ()
-withABCVerilog baseName t buildCmd =
-  do verilogFile <- io $ emptySystemTempFile (baseName ++ ".v")
+withABCVerilog fileName t buildCmd =
+  do verilogFile <- io $ emptySystemTempFile (takeBaseName fileName ++ ".v")
      sc <- getSharedContext
      write_verilog sc verilogFile t
      io $