summaryrefslogtreecommitdiffstats
path: root/src/aig/ssw/sswSat.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ssw/sswSat.c')
-rw-r--r--src/aig/ssw/sswSat.c234
1 files changed, 234 insertions, 0 deletions
diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c
new file mode 100644
index 00000000..06abd2c9
--- /dev/null
+++ b/src/aig/ssw/sswSat.c
@@ -0,0 +1,234 @@
+/**CFile****************************************************************
+
+ FileName [sswSat.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Inductive prover with constraints.]
+
+ Synopsis [Calls to the SAT solver.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - September 1, 2008.]
+
+ Revision [$Id: sswSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Runs equivalence test for the two nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
+{
+ int nBTLimit = p->pPars->nBTLimit;
+ int pLits[2], RetValue, RetValue1, status, clk;
+ p->nSatCalls++;
+
+ // sanity checks
+ assert( !Aig_IsComplement(pNew) );
+ assert( !Aig_IsComplement(pOld) );
+ assert( pNew != pOld );
+
+ if ( p->pSat == NULL )
+ Ssw_ManStartSolver( p );
+
+ // if the nodes do not have SAT variables, allocate them
+ Ssw_CnfNodeAddToSolver( p, pOld );
+ Ssw_CnfNodeAddToSolver( p, pNew );
+
+ // propagate unit clauses
+ if ( p->pSat->qtail != p->pSat->qhead )
+ {
+ status = sat_solver_simplify(p->pSat);
+ assert( status != 0 );
+ assert( p->pSat->qtail == p->pSat->qhead );
+ }
+
+ // solve under assumptions
+ // A = 1; B = 0 OR A = 1; B = 1
+ pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 );
+ pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
+ }
+//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
+clk = clock();
+ RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
+ (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+p->timeSat += clock() - clk;
+ if ( RetValue1 == l_False )
+ {
+p->timeSatUnsat += clock() - clk;
+ pLits[0] = lit_neg( pLits[0] );
+ pLits[1] = lit_neg( pLits[1] );
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+ assert( RetValue );
+ p->nSatCallsUnsat++;
+ }
+ else if ( RetValue1 == l_True )
+ {
+p->timeSatSat += clock() - clk;
+ p->nSatCallsSat++;
+ return 0;
+ }
+ else // if ( RetValue1 == l_Undef )
+ {
+p->timeSatUndec += clock() - clk;
+ p->nSatFailsReal++;
+ return -1;
+ }
+
+ // if the old node was constant 0, we already know the answer
+ if ( pOld == Aig_ManConst1(p->pFrames) )
+ {
+ p->nSatProof++;
+ return 1;
+ }
+
+ // solve under assumptions
+ // A = 0; B = 1 OR A = 0; B = 0
+ pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 );
+ pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
+ }
+clk = clock();
+ RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
+ (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+p->timeSat += clock() - clk;
+ if ( RetValue1 == l_False )
+ {
+p->timeSatUnsat += clock() - clk;
+ pLits[0] = lit_neg( pLits[0] );
+ pLits[1] = lit_neg( pLits[1] );
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+ assert( RetValue );
+ p->nSatCallsUnsat++;
+ }
+ else if ( RetValue1 == l_True )
+ {
+p->timeSatSat += clock() - clk;
+ p->nSatCallsSat++;
+ return 0;
+ }
+ else // if ( RetValue1 == l_Undef )
+ {
+p->timeSatUndec += clock() - clk;
+ p->nSatFailsReal++;
+ return -1;
+ }
+ // return SAT proof
+ p->nSatProof++;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Constrains two nodes to be equivalent in the SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
+{
+ int pLits[2], RetValue;
+
+ // sanity checks
+ assert( !Aig_IsComplement(pNew) );
+ assert( !Aig_IsComplement(pOld) );
+ assert( pNew != pOld );
+
+ if ( p->pSat == NULL )
+ Ssw_ManStartSolver( p );
+
+ // if the nodes do not have SAT variables, allocate them
+ Ssw_CnfNodeAddToSolver( p, pOld );
+ Ssw_CnfNodeAddToSolver( p, pNew );
+
+ if ( pOld == Aig_ManConst1(p->pFrames) )
+ {
+ pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), !pNew->fPhase );
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( pNew->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ }
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
+ assert( RetValue );
+ }
+ else
+ {
+ // solve under assumptions
+ // A = 1; B = 0 OR A = 1; B = 1
+ pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 );
+ pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
+ }
+ pLits[0] = lit_neg( pLits[0] );
+ pLits[1] = lit_neg( pLits[1] );
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+ assert( RetValue );
+
+ // solve under assumptions
+ // A = 0; B = 1 OR A = 0; B = 0
+ pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 );
+ pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
+ }
+ pLits[0] = lit_neg( pLits[0] );
+ pLits[1] = lit_neg( pLits[1] );
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+ assert( RetValue );
+ }
+/*
+ // propagate unit clauses
+ if ( p->pSat->qtail != p->pSat->qhead )
+ {
+ int status;
+ status = sat_solver_simplify(p->pSat);
+ assert( status != 0 );
+ assert( p->pSat->qtail == p->pSat->qhead );
+ }
+*/
+ return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 12:24:23 +0000