@@ -414,20 +414,34 @@ impl ProverBackend for AbcBackend {
414414 . context ( "Failed to read ABC input file" ) ?;
415415
416416 let extension = path. extension ( ) . and_then ( |e| e. to_str ( ) ) ;
417- self . parse_design ( & content, extension)
417+ let mut state = self . parse_design ( & content, extension) ?;
418+ state. metadata . insert (
419+ "abc_source" . to_string ( ) ,
420+ serde_json:: Value :: String ( content. clone ( ) ) ,
421+ ) ;
422+ state. metadata . insert (
423+ "source_path" . to_string ( ) ,
424+ serde_json:: Value :: String ( path. to_string_lossy ( ) . into_owned ( ) ) ,
425+ ) ;
426+ Ok ( state)
418427 }
419428
420429 async fn parse_string ( & self , content : & str ) -> Result < ProofState > {
421430 // Without file extension context, try ABC command script first,
422431 // then fall back to AIGER ASCII if header starts with "aag"/"aig"
423432 let trimmed = content. trim ( ) ;
424- if trimmed. starts_with ( "aag" ) || trimmed. starts_with ( "aig" ) {
425- self . parse_design ( content, Some ( "aig" ) )
433+ let mut state = if trimmed. starts_with ( "aag" ) || trimmed. starts_with ( "aig" ) {
434+ self . parse_design ( content, Some ( "aig" ) ) ?
426435 } else if trimmed. starts_with ( ".model" ) || trimmed. starts_with ( ".inputs" ) {
427- self . parse_design ( content, Some ( "blif" ) )
436+ self . parse_design ( content, Some ( "blif" ) ) ?
428437 } else {
429- self . parse_design ( content, None )
430- }
438+ self . parse_design ( content, None ) ?
439+ } ;
440+ state. metadata . insert (
441+ "abc_source" . to_string ( ) ,
442+ serde_json:: Value :: String ( content. to_string ( ) ) ,
443+ ) ;
444+ Ok ( state)
431445 }
432446
433447 async fn apply_tactic ( & self , state : & ProofState , tactic : & Tactic ) -> Result < TacticResult > {
@@ -567,6 +581,131 @@ impl ProverBackend for AbcBackend {
567581 }
568582
569583 async fn verify_proof ( & self , state : & ProofState ) -> Result < bool > {
584+ // Prefer the original source — parsing ABC/BLIF/AIGER into the
585+ // generic Term IR and reconstructing via `to_abc_script` loses
586+ // structure for anything beyond a one-command script.
587+ let method = state
588+ . metadata
589+ . get ( "abc_method" )
590+ . and_then ( |v| v. as_str ( ) )
591+ . unwrap_or ( "pdr" ) ;
592+ let bmc_bound = state
593+ . metadata
594+ . get ( "bmc_bound" )
595+ . and_then ( |v| v. as_str ( ) )
596+ . unwrap_or ( "100" ) ;
597+ let verify_cmd = match method {
598+ "bmc" | "bmc3" => format ! ( "bmc3 -F {}" , bmc_bound) ,
599+ "int" => "int" . to_string ( ) ,
600+ "dprove" => "dprove" . to_string ( ) ,
601+ "dsec" => "dsec" . to_string ( ) ,
602+ "cec" => "cec" . to_string ( ) ,
603+ _ => "pdr" . to_string ( ) ,
604+ } ;
605+
606+ if let Some ( path) = state. metadata . get ( "source_path" ) . and_then ( |v| v. as_str ( ) ) {
607+ let p = std:: path:: Path :: new ( path) ;
608+ let read_cmd = match p. extension ( ) . and_then ( |e| e. to_str ( ) ) {
609+ Some ( "aig" ) => format ! ( "read_aiger {}" , path) ,
610+ Some ( "blif" ) => format ! ( "read_blif {}" , path) ,
611+ Some ( "v" ) => format ! ( "read_verilog {}" , path) ,
612+ _ => format ! ( "read {}" , path) ,
613+ } ;
614+ let script = format ! ( "{}\n {}\n print_status\n quit\n " , read_cmd, verify_cmd) ;
615+ let tmp_dir =
616+ tempfile:: tempdir ( ) . context ( "Failed to create temporary directory for ABC" ) ?;
617+ let tmp_file = tmp_dir. path ( ) . join ( "verify.abc" ) ;
618+ tokio:: fs:: write ( & tmp_file, & script)
619+ . await
620+ . context ( "Failed to write temporary ABC script file" ) ?;
621+ let output = tokio:: time:: timeout (
622+ tokio:: time:: Duration :: from_secs ( self . config . timeout ) ,
623+ Command :: new ( & self . config . executable )
624+ . arg ( "-f" )
625+ . arg ( & tmp_file)
626+ . stdout ( Stdio :: piped ( ) )
627+ . stderr ( Stdio :: piped ( ) )
628+ . output ( ) ,
629+ )
630+ . await
631+ . map_err ( |_| anyhow ! ( "ABC timed out after {} seconds" , self . config. timeout) ) ?
632+ . context ( "Failed to execute ABC" ) ?;
633+ let stdout = String :: from_utf8_lossy ( & output. stdout ) ;
634+ let stderr = String :: from_utf8_lossy ( & output. stderr ) ;
635+ let combined = format ! ( "{}\n {}" , stdout, stderr) ;
636+ return self . parse_result ( & combined) ;
637+ }
638+
639+ if let Some ( source) = state. metadata . get ( "abc_source" ) . and_then ( |v| v. as_str ( ) ) {
640+ let trimmed = source. trim ( ) ;
641+ let ( ext, read_cmd_base) =
642+ if trimmed. starts_with ( "aag" ) || trimmed. starts_with ( "aig" ) {
643+ ( ".aig" , "read_aiger" )
644+ } else if trimmed. starts_with ( ".model" ) || trimmed. starts_with ( ".inputs" ) {
645+ ( ".blif" , "read_blif" )
646+ } else {
647+ // Inline script — just execute it directly.
648+ ( "" , "" )
649+ } ;
650+ let tmp_dir =
651+ tempfile:: tempdir ( ) . context ( "Failed to create temporary directory for ABC" ) ?;
652+ if ext. is_empty ( ) {
653+ let tmp_file = tmp_dir. path ( ) . join ( "verify.abc" ) ;
654+ let script = format ! ( "{}\n {}\n print_status\n quit\n " , source, verify_cmd) ;
655+ tokio:: fs:: write ( & tmp_file, & script)
656+ . await
657+ . context ( "Failed to write temporary ABC script file" ) ?;
658+ let output = tokio:: time:: timeout (
659+ tokio:: time:: Duration :: from_secs ( self . config . timeout ) ,
660+ Command :: new ( & self . config . executable )
661+ . arg ( "-f" )
662+ . arg ( & tmp_file)
663+ . stdout ( Stdio :: piped ( ) )
664+ . stderr ( Stdio :: piped ( ) )
665+ . output ( ) ,
666+ )
667+ . await
668+ . map_err ( |_| anyhow ! ( "ABC timed out after {} seconds" , self . config. timeout) ) ?
669+ . context ( "Failed to execute ABC" ) ?;
670+ let stdout = String :: from_utf8_lossy ( & output. stdout ) ;
671+ let stderr = String :: from_utf8_lossy ( & output. stderr ) ;
672+ let combined = format ! ( "{}\n {}" , stdout, stderr) ;
673+ return self . parse_result ( & combined) ;
674+ } else {
675+ let design_file = tmp_dir. path ( ) . join ( format ! ( "design{}" , ext) ) ;
676+ tokio:: fs:: write ( & design_file, source)
677+ . await
678+ . context ( "Failed to write temporary ABC design file" ) ?;
679+ let script_file = tmp_dir. path ( ) . join ( "verify.abc" ) ;
680+ let script = format ! (
681+ "{} {}\n {}\n print_status\n quit\n " ,
682+ read_cmd_base,
683+ design_file. display( ) ,
684+ verify_cmd
685+ ) ;
686+ tokio:: fs:: write ( & script_file, & script)
687+ . await
688+ . context ( "Failed to write temporary ABC script file" ) ?;
689+ let output = tokio:: time:: timeout (
690+ tokio:: time:: Duration :: from_secs ( self . config . timeout ) ,
691+ Command :: new ( & self . config . executable )
692+ . arg ( "-f" )
693+ . arg ( & script_file)
694+ . stdout ( Stdio :: piped ( ) )
695+ . stderr ( Stdio :: piped ( ) )
696+ . output ( ) ,
697+ )
698+ . await
699+ . map_err ( |_| anyhow ! ( "ABC timed out after {} seconds" , self . config. timeout) ) ?
700+ . context ( "Failed to execute ABC" ) ?;
701+ let stdout = String :: from_utf8_lossy ( & output. stdout ) ;
702+ let stderr = String :: from_utf8_lossy ( & output. stderr ) ;
703+ let combined = format ! ( "{}\n {}" , stdout, stderr) ;
704+ return self . parse_result ( & combined) ;
705+ }
706+ }
707+
708+ // Fallback: reconstruct an ABC script from the parsed IR.
570709 let abc_script = self . to_abc_script ( state) ?;
571710
572711 // ABC can execute commands via -c flag or from a script file.
0 commit comments