31e34f55e7
Drop upstreamed -undefined patch.
144 lines
7.9 KiB
Diff
144 lines
7.9 KiB
Diff
diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
|
|
index 395e737..ff5cc3d 100644
|
|
--- a/src/STPManager/STP.cpp
|
|
+++ b/src/STPManager/STP.cpp
|
|
@@ -576,7 +576,7 @@ namespace BEEV {
|
|
|
|
ToSATAIG toSATAIG(bm, cb, arrayTransformer);
|
|
|
|
- ToSATBase* satBase = bm->UserFlags.isSet("traditional-cnf", "0") ? tosat : ((ToSAT*) &toSATAIG) ;
|
|
+ ToSATBase* satBase = bm->UserFlags.isSet("traditional-cnf", "0") ? tosat : &toSATAIG;
|
|
|
|
if (bm->soft_timeout_expired)
|
|
return SOLVER_TIMEOUT;
|
|
diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp
|
|
index 4cc543d..25102bd 100644
|
|
--- a/src/absrefine_counterexample/AbstractionRefinement.cpp
|
|
+++ b/src/absrefine_counterexample/AbstractionRefinement.cpp
|
|
@@ -119,7 +119,7 @@ namespace BEEV
|
|
}
|
|
return result;
|
|
}
|
|
- else if (v_a.size() == 0 ^ v_b.size() == 0)
|
|
+ else if ((v_a.size() == 0) ^ (v_b.size() == 0))
|
|
{
|
|
ASTNode constant = a.isConstant() ? a : b;
|
|
vector<unsigned> vec = v_a.size() == 0 ? v_b : v_a;
|
|
diff --git a/src/extlib-abc/kit.h b/src/extlib-abc/kit.h
|
|
index af3a1a8..b8db70f 100644
|
|
--- a/src/extlib-abc/kit.h
|
|
+++ b/src/extlib-abc/kit.h
|
|
@@ -53,11 +53,14 @@ struct Kit_Sop_t_
|
|
unsigned * pCubes; // the storage for cubes
|
|
};
|
|
|
|
-typedef struct Kit_Edge_t_ Kit_Edge_t;
|
|
-struct Kit_Edge_t_
|
|
-{
|
|
- unsigned fCompl : 1; // the complemented bit
|
|
- unsigned Node : 30; // the decomposition node pointed by the edge
|
|
+typedef union Kit_Edge_t_ Kit_Edge_t;
|
|
+union Kit_Edge_t_
|
|
+{
|
|
+ struct {
|
|
+ unsigned fCompl : 1; // the complemented bit
|
|
+ unsigned Node : 30; // the decomposition node pointed by the edge
|
|
+ };
|
|
+ unsigned int edgeInt;
|
|
};
|
|
|
|
typedef struct Kit_Node_t_ Kit_Node_t;
|
|
@@ -203,11 +206,11 @@ static inline void Kit_SopShrink( Kit_Sop_t * cSop, int nCubesNew )
|
|
static inline void Kit_SopPushCube( Kit_Sop_t * cSop, unsigned uCube ) { cSop->pCubes[cSop->nCubes++] = uCube; }
|
|
static inline void Kit_SopWriteCube( Kit_Sop_t * cSop, unsigned uCube, int i ) { cSop->pCubes[i] = uCube; }
|
|
|
|
-static inline Kit_Edge_t Kit_EdgeCreate( int Node, int fCompl ) { Kit_Edge_t eEdge = { fCompl, Node }; return eEdge; }
|
|
+static inline Kit_Edge_t Kit_EdgeCreate( int Node, int fCompl ) { Kit_Edge_t eEdge = { { fCompl, Node } }; return eEdge; }
|
|
static inline unsigned Kit_EdgeToInt( Kit_Edge_t eEdge ) { return (eEdge.Node << 1) | eEdge.fCompl; }
|
|
static inline Kit_Edge_t Kit_IntToEdge( unsigned Edge ) { return Kit_EdgeCreate( Edge >> 1, Edge & 1 ); }
|
|
-static inline unsigned Kit_EdgeToInt_( Kit_Edge_t eEdge ) { return *(unsigned *)&eEdge; }
|
|
-static inline Kit_Edge_t Kit_IntToEdge_( unsigned Edge ) { return *(Kit_Edge_t *)&Edge; }
|
|
+static inline unsigned Kit_EdgeToInt_( Kit_Edge_t eEdge ) { return eEdge.edgeInt; }
|
|
+static inline Kit_Edge_t Kit_IntToEdge_( unsigned Edge ) { Kit_Edge_t e; e.edgeInt = Edge; return e; }
|
|
|
|
static inline int Kit_GraphIsConst( Kit_Graph_t * pGraph ) { return pGraph->fConst; }
|
|
static inline int Kit_GraphIsConst0( Kit_Graph_t * pGraph ) { return pGraph->fConst && pGraph->eRoot.fCompl; }
|
|
@@ -228,8 +231,6 @@ static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t
|
|
static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.Node); }
|
|
static inline int Kit_GraphRootLevel( Kit_Graph_t * pGraph ) { return Kit_GraphNode(pGraph, pGraph->eRoot.Node)->Level; }
|
|
|
|
-static inline int Kit_Float2Int( float Val ) { return *((int *)&Val); }
|
|
-static inline float Kit_Int2Float( int Num ) { return *((float *)&Num); }
|
|
static inline int Kit_BitWordNum( int nBits ) { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0); }
|
|
static inline int Kit_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
|
|
static inline unsigned Kit_BitMask( int nBits ) { assert( nBits <= 32 ); return ~((~(unsigned)0) << nBits); }
|
|
@@ -486,6 +487,18 @@ static inline void Kit_TruthIthVar( unsigned * pTruth, int nVars, int iVar )
|
|
/// FUNCTION DECLARATIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
+extern Kit_Graph_t * Kit_GraphCreateConst0( void );
|
|
+extern Kit_Graph_t * Kit_GraphCreateConst1( void );
|
|
+extern void Kit_GraphFree( Kit_Graph_t * );
|
|
+extern Kit_Graph_t * Kit_SopFactor( Vec_Int_t *, int, int, Vec_Int_t * );
|
|
+extern void Kit_TruthCofactor0( unsigned *, int, int );
|
|
+extern void Kit_TruthCofactor1( unsigned *, int, int );
|
|
+extern int Kit_TruthIsop( unsigned *, int, Vec_Int_t *, int );
|
|
+extern void Kit_TruthShrink( unsigned *, unsigned *, int, int, unsigned, int );
|
|
+extern void Kit_TruthStretch( unsigned *, unsigned *, int, int, unsigned, int );
|
|
+extern Kit_Graph_t * Kit_TruthToGraph( unsigned *, int, Vec_Int_t * );
|
|
+extern int Kit_TruthVarInSupport( unsigned *, int, int );
|
|
+
|
|
#if 0
|
|
|
|
/*=== kitBdd.c ==========================================================*/
|
|
diff --git a/src/interface/C/c_interface.cpp b/src/interface/C/c_interface.cpp
|
|
index ee838d1..8179d57 100644
|
|
--- a/src/interface/C/c_interface.cpp
|
|
+++ b/src/interface/C/c_interface.cpp
|
|
@@ -994,7 +994,7 @@ Expr vc_bvConstExprFromInt(VC vc,
|
|
bmstar b = (bmstar)(((stpstar)vc)->bm);
|
|
|
|
unsigned long long int v = (unsigned long long int)value;
|
|
- unsigned long long int max_n_bits = 0xFFFFFFFFFFFFFFFFULL >> 64-n_bits;
|
|
+ unsigned long long int max_n_bits = 0xFFFFFFFFFFFFFFFFULL >> (64-n_bits);
|
|
//printf("%ull", max_n_bits);
|
|
if(v > max_n_bits) {
|
|
printf("CInterface: vc_bvConstExprFromInt: "\
|
|
diff --git a/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp b/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp
|
|
index 7958269..1dded88 100644
|
|
--- a/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp
|
|
+++ b/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp
|
|
@@ -129,6 +129,7 @@ fast_exit(FixedBits& c0, FixedBits& c1)
|
|
}
|
|
return false;
|
|
}
|
|
+ return true;
|
|
}
|
|
|
|
|
|
diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
|
|
index b309a8a..5bd000f 100644
|
|
--- a/src/simplifier/simplifier.cpp
|
|
+++ b/src/simplifier/simplifier.cpp
|
|
@@ -523,6 +523,7 @@ namespace BEEV
|
|
return getConstantBit(n[0], i);
|
|
|
|
assert(false);
|
|
+ return -1;
|
|
}
|
|
|
|
ASTNode
|
|
diff --git a/src/to-sat/ASTNode/ToSAT.cpp b/src/to-sat/ASTNode/ToSAT.cpp
|
|
index 0b01b77..05ba88d 100644
|
|
--- a/src/to-sat/ASTNode/ToSAT.cpp
|
|
+++ b/src/to-sat/ASTNode/ToSAT.cpp
|
|
@@ -53,7 +53,7 @@ namespace BEEV
|
|
|
|
// Copies the symbol into the map that is used to build the counter example.
|
|
// For boolean we create a vector of size 1.
|
|
- if (n.GetKind() == BOOLEXTRACT && n[0].GetKind() == SYMBOL || (n.GetKind() == SYMBOL && !isTseitinVariable(n)))
|
|
+ if ((n.GetKind() == BOOLEXTRACT && n[0].GetKind() == SYMBOL) || (n.GetKind() == SYMBOL && !isTseitinVariable(n)))
|
|
{
|
|
const ASTNode& symbol = n.GetKind() == BOOLEXTRACT ? n[0] : n;
|
|
const unsigned index = n.GetKind() == BOOLEXTRACT ? n[1].GetUnsignedConst() : 0;
|