From 5fbc0cd7f09a382241266404d78c18c5443d2b9d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 10 Jan 2017 16:58:24 +0700 Subject: Updates to arithmetic verification. --- src/proof/acec/acecCl.c | 8 -------- 1 file changed, 8 deletions(-) (limited to 'src/proof/acec/acecCl.c') diff --git a/src/proof/acec/acecCl.c b/src/proof/acec/acecCl.c index 63483d57..145f2e0b 100644 --- a/src/proof/acec/acecCl.c +++ b/src/proof/acec/acecCl.c @@ -306,18 +306,10 @@ Gia_Man_t * Acec_DetectXorBuildNew( Gia_Man_t * p, Vec_Int_t * vRootXorSet ) ***********************************************************************/ Gia_Man_t * Acec_DetectAdditional( Gia_Man_t * p, int fVerbose ) { - extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose ); - extern void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds ); - extern void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds ); - extern int Ree_ManCountFadds( Vec_Int_t * vAdds ); - extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose ); - abctime clk = Abc_Clock(); Gia_Man_t * pNew; Vec_Int_t * vRootXorSet; // Vec_Int_t * vXors, * vAdds = Ree_ManComputeCuts( p, &vXors, 0 ); -// Ree_ManRemoveTrivial( p, vAdds ); -// Ree_ManRemoveContained( p, vAdds ); //Ree_ManPrintAdders( vAdds, 1 ); // printf( "Detected %d full-adders and %d half-adders. Found %d XOR-cuts. ", Ree_ManCountFadds(vAdds), Vec_IntSize(vAdds)/6-Ree_ManCountFadds(vAdds), Vec_IntSize(vXors)/4 ); -- cgit v1.2.3