summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bmc/bmc.h4
-rw-r--r--src/sat/bmc/bmcCexCare.c38
-rw-r--r--src/sat/bmc/bmcCexTools.c47
-rw-r--r--src/sat/bsat2/Alloc.h8
-rw-r--r--src/sat/bsat2/Vec.h4
-rw-r--r--src/sat/bsat2/XAlloc.h4
-rw-r--r--src/sat/glucose/Alloc.h8
-rw-r--r--src/sat/glucose/IntTypes.h14
-rw-r--r--src/sat/glucose/Vec.h4
-rw-r--r--src/sat/glucose/XAlloc.h4
-rw-r--r--src/sat/glucose2/Alloc.h8
-rw-r--r--src/sat/glucose2/IntTypes.h14
-rw-r--r--src/sat/glucose2/Vec.h8
-rw-r--r--src/sat/glucose2/XAlloc.h4
14 files changed, 150 insertions, 19 deletions
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 844497ad..34356359 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -227,7 +227,8 @@ extern int Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars
extern Abc_Cex_t * Bmc_CexCareExtendToObjects( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
extern Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose );
extern Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose );
-extern void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose );
+extern int Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose );
+extern int Bmc_CexCareVerifyAnyPo( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose );
extern Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int fHighEffort, int fCheck, int fVerbose );
extern Abc_Cex_t * Bmc_CexCareSatBasedMinimizeAig( Gia_Man_t * p, Abc_Cex_t * pCex, int fHighEffort, int fVerbose );
/*=== bmcCexCut.c ==========================================================*/
@@ -238,6 +239,7 @@ extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pC
/*=== bmcCexTool.c ==========================================================*/
extern void Bmc_CexPrint( Abc_Cex_t * pCex, int nRealPis, int fVerbose );
extern int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
+extern int Bmc_CexVerifyAnyPo( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
/*=== bmcICheck.c ==========================================================*/
extern void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose );
extern Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fDump, int fVerbose );
diff --git a/src/sat/bmc/bmcCexCare.c b/src/sat/bmc/bmcCexCare.c
index c274b04c..d9a677c3 100644
--- a/src/sat/bmc/bmcCexCare.c
+++ b/src/sat/bmc/bmcCexCare.c
@@ -455,8 +455,9 @@ Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t
SeeAlso []
***********************************************************************/
-void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose )
+int Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose )
{
+ int result;
Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
if ( fVerbose )
{
@@ -465,11 +466,13 @@ void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, in
printf( "Minimized: " );
Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 );
}
- if ( !Bmc_CexVerify( pGia, pCex, pCexMin ) )
+ result = Bmc_CexVerify( pGia, pCex, pCexMin );
+ if ( !result )
printf( "Counter-example verification has failed.\n" );
else
printf( "Counter-example verification succeeded.\n" );
Gia_ManStop( pGia );
+ return result;
}
/*
{
@@ -480,6 +483,37 @@ void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, in
}
*/
+/**Function*************************************************************
+
+ Synopsis [Verifies the care set of the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Bmc_CexCareVerifyAnyPo( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose )
+{
+ int iPo;
+ Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
+ if ( fVerbose )
+ {
+ printf( "Original : " );
+ Bmc_CexPrint( pCex, Gia_ManPiNum(pGia), 0 );
+ printf( "Minimized: " );
+ Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 );
+ }
+ iPo = Bmc_CexVerifyAnyPo( pGia, pCex, pCexMin );
+ if ( iPo < 0 )
+ printf( "Counter-example verification has failed.\n" );
+ else
+ printf( "Counter-example verification succeeded.\n" );
+ Gia_ManStop( pGia );
+ return iPo;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/bmc/bmcCexTools.c b/src/sat/bmc/bmcCexTools.c
index 6cc29857..6bea6fc5 100644
--- a/src/sat/bmc/bmcCexTools.c
+++ b/src/sat/bmc/bmcCexTools.c
@@ -376,6 +376,53 @@ int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )
/**Function*************************************************************
+ Synopsis [Verifies the care set of the counter-example for an arbitrary PO.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Bmc_CexVerifyAnyPo( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )
+{
+ Gia_Obj_t * pObj;
+ int i, k;
+// assert( pCex->nRegs > 0 );
+// assert( pCexCare->nRegs == 0 );
+ Gia_ObjTerSimSet0( Gia_ManConst0(p) );
+ Gia_ManForEachRi( p, pObj, k )
+ Gia_ObjTerSimSet0( pObj );
+ for ( i = 0; i <= pCex->iFrame; i++ )
+ {
+ Gia_ManForEachPi( p, pObj, k )
+ {
+ if ( !Abc_InfoHasBit( pCexCare->pData, pCexCare->nRegs + i * pCexCare->nPis + k ) )
+ Gia_ObjTerSimSetX( pObj );
+ else if ( Abc_InfoHasBit( pCex->pData, pCex->nRegs + i * pCex->nPis + k ) )
+ Gia_ObjTerSimSet1( pObj );
+ else
+ Gia_ObjTerSimSet0( pObj );
+ }
+ Gia_ManForEachRo( p, pObj, k )
+ Gia_ObjTerSimRo( p, pObj );
+ Gia_ManForEachAnd( p, pObj, k )
+ Gia_ObjTerSimAnd( pObj );
+ Gia_ManForEachCo( p, pObj, k )
+ Gia_ObjTerSimCo( pObj );
+ }
+ for (i = 0; i < Gia_ManPoNum(p) - Gia_ManConstrNum(p); i++)
+ {
+ pObj = Gia_ManPo( p, i );
+ if (Gia_ObjTerSimGet1(pObj))
+ return i;
+ }
+ return -1;
+}
+
+/**Function*************************************************************
+
Synopsis [Computes internal states of the CEX.]
Description []
diff --git a/src/sat/bsat2/Alloc.h b/src/sat/bsat2/Alloc.h
index 7f506cb5..9a65cf0c 100644
--- a/src/sat/bsat2/Alloc.h
+++ b/src/sat/bsat2/Alloc.h
@@ -97,7 +97,11 @@ void RegionAllocator<T>::capacity(uint32_t min_cap)
cap += delta;
if (cap <= prev_cap)
+#ifdef __wasm
+ abort();
+#else
throw OutOfMemoryException();
+#endif
}
// printf(" .. (%p) cap = %u\n", this, cap);
@@ -119,7 +123,11 @@ RegionAllocator<T>::alloc(int size)
// Handle overflow:
if (sz < prev_sz)
+#ifdef __wasm
+ abort();
+#else
throw OutOfMemoryException();
+#endif
return prev_sz;
}
diff --git a/src/sat/bsat2/Vec.h b/src/sat/bsat2/Vec.h
index f0e07d01..5eea6174 100644
--- a/src/sat/bsat2/Vec.h
+++ b/src/sat/bsat2/Vec.h
@@ -97,7 +97,11 @@ void vec<T>::capacity(int min_cap) {
if (cap >= min_cap) return;
int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM))
+#ifdef __wasm
+ abort();
+#else
throw OutOfMemoryException();
+#endif
}
diff --git a/src/sat/bsat2/XAlloc.h b/src/sat/bsat2/XAlloc.h
index 1da17602..33741e33 100644
--- a/src/sat/bsat2/XAlloc.h
+++ b/src/sat/bsat2/XAlloc.h
@@ -34,7 +34,11 @@ static inline void* xrealloc(void *ptr, size_t size)
{
void* mem = realloc(ptr, size);
if (mem == NULL && errno == ENOMEM){
+#ifdef __wasm
+ abort();
+#else
throw OutOfMemoryException();
+#endif
}else
return mem;
}
diff --git a/src/sat/glucose/Alloc.h b/src/sat/glucose/Alloc.h
index e56b5441..a63de032 100644
--- a/src/sat/glucose/Alloc.h
+++ b/src/sat/glucose/Alloc.h
@@ -100,7 +100,11 @@ void RegionAllocator<T>::capacity(uint32_t min_cap)
cap += delta;
if (cap <= prev_cap)
+#ifdef __wasm
+ abort();
+#else
throw OutOfMemoryException();
+#endif
}
//printf(" .. (%p) cap = %u\n", this, cap);
@@ -122,7 +126,11 @@ RegionAllocator<T>::alloc(int size)
// Handle overflow:
if (sz < prev_sz)
+#ifdef __wasm
+ abort();
+#else
throw OutOfMemoryException();
+#endif
return prev_sz;
}
diff --git a/src/sat/glucose/IntTypes.h b/src/sat/glucose/IntTypes.h
index 3f75862b..5c4176b2 100644
--- a/src/sat/glucose/IntTypes.h
+++ b/src/sat/glucose/IntTypes.h
@@ -28,20 +28,18 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
# include <sys/int_fmtio.h>
# include <sys/int_limits.h>
-#else
+#elif _WIN32
-#define __STDC_LIMIT_MACROS
# include "pstdint.h"
-//# include <inttypes.h>
-#endif
+#else
-#include <limits.h>
+# define __STDC_LIMIT_MACROS
+# include <limits.h>
+# include <inttypes.h>
-#ifndef PRIu64
-#define PRIu64 "lu"
-#define PRIi64 "ld"
#endif
+
//=================================================================================================
#include <misc/util/abc_namespaces.h>
diff --git a/src/sat/glucose/Vec.h b/src/sat/glucose/Vec.h
index dd1bc20a..d2781635 100644
--- a/src/sat/glucose/Vec.h
+++ b/src/sat/glucose/Vec.h
@@ -100,7 +100,11 @@ void vec<T>::capacity(int min_cap) {
if (cap >= min_cap) return;
int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM))
+#ifdef __wasm
+ abort();
+#else
throw OutOfMemoryException();
+#endif
}
diff --git a/src/sat/glucose/XAlloc.h b/src/sat/glucose/XAlloc.h
index 233f834e..d1f1062a 100644
--- a/src/sat/glucose/XAlloc.h
+++ b/src/sat/glucose/XAlloc.h
@@ -39,7 +39,11 @@ static inline void* xrealloc(void *ptr, size_t size)
{
void* mem = realloc(ptr, size);
if (mem == NULL && errno == ENOMEM){
+#ifdef __wasm
+ abort();
+#else
throw OutOfMemoryException();
+#endif
}else {
return mem;
}
diff --git a/src/sat/glucose2/Alloc.h b/src/sat/glucose2/Alloc.h
index b7bebaca..427cd323 100644
--- a/src/sat/glucose2/Alloc.h
+++ b/src/sat/glucose2/Alloc.h
@@ -100,7 +100,11 @@ void RegionAllocator<T>::capacity(uint32_t min_cap)
cap += delta;
if (cap <= prev_cap)
+#ifdef __wasm
+ abort();
+#else
throw OutOfMemoryException();
+#endif
}
//printf(" .. (%p) cap = %u\n", this, cap);
@@ -122,7 +126,11 @@ RegionAllocator<T>::alloc(int size)
// Handle overflow:
if (sz < prev_sz)
+#ifdef __wasm
+ abort();
+#else
throw OutOfMemoryException();
+#endif
return prev_sz;
}
diff --git a/src/sat/glucose2/IntTypes.h b/src/sat/glucose2/IntTypes.h
index 3f75862b..5c4176b2 100644
--- a/src/sat/glucose2/IntTypes.h
+++ b/src/sat/glucose2/IntTypes.h
@@ -28,20 +28,18 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
# include <sys/int_fmtio.h>
# include <sys/int_limits.h>
-#else
+#elif _WIN32
-#define __STDC_LIMIT_MACROS
# include "pstdint.h"
-//# include <inttypes.h>
-#endif
+#else
-#include <limits.h>
+# define __STDC_LIMIT_MACROS
+# include <limits.h>
+# include <inttypes.h>
-#ifndef PRIu64
-#define PRIu64 "lu"
-#define PRIi64 "ld"
#endif
+
//=================================================================================================
#include <misc/util/abc_namespaces.h>
diff --git a/src/sat/glucose2/Vec.h b/src/sat/glucose2/Vec.h
index eaeed207..bc989217 100644
--- a/src/sat/glucose2/Vec.h
+++ b/src/sat/glucose2/Vec.h
@@ -102,14 +102,22 @@ void vec<T>::capacity(int min_cap) {
if (cap >= min_cap) return;
int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM))
+#ifdef __wasm
+ abort();
+#else
throw OutOfMemoryException();
+#endif
}
template<class T>
void vec<T>::prelocate(int ext_cap) {
if (cap >= ext_cap) return;
if (ext_cap > INT_MAX || (((data = (T*)::realloc(data, ext_cap * sizeof(T))) == NULL) && errno == ENOMEM))
+#ifdef __wasm
+ abort();
+#else
throw OutOfMemoryException();
+#endif
cap = ext_cap;
}
diff --git a/src/sat/glucose2/XAlloc.h b/src/sat/glucose2/XAlloc.h
index 716643ef..86e65a49 100644
--- a/src/sat/glucose2/XAlloc.h
+++ b/src/sat/glucose2/XAlloc.h
@@ -39,7 +39,11 @@ static inline void* xrealloc(void *ptr, size_t size)
{
void* mem = realloc(ptr, size);
if (mem == NULL && errno == ENOMEM){
+#ifdef __wasm
+ abort();
+#else
throw OutOfMemoryException();
+#endif
}else {
return mem;
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-08-06 19:14:02 +0000