summaryrefslogtreecommitdiffstats
path: root/src/aig/ssw_old/sswSat.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ssw_old/sswSat.c')
-rw-r--r--src/aig/ssw_old/sswSat.c264
1 files changed, 0 insertions, 264 deletions
diff --git a/src/aig/ssw_old/sswSat.c b/src/aig/ssw_old/sswSat.c
deleted file mode 100644
index 85d3b8c1..00000000
--- a/src/aig/ssw_old/sswSat.c
+++ /dev/null
@@ -1,264 +0,0 @@
-/**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 [Both nodes should be regular and different from each other.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
-{
- int nBTLimit = p->pPars->nBTLimit;
- int pLits[3], nLits, RetValue, RetValue1, clk;//, status;
- p->nSatCalls++;
-
- // sanity checks
- assert( !Aig_IsComplement(pOld) );
- assert( !Aig_IsComplement(pNew) );
- assert( pOld != pNew );
-
- 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 ( p->pSat->qtail != p->pSat->qhead )
- {
- RetValue = sat_solver_simplify(p->pSat);
- assert( RetValue != 0 );
- }
-
- // solve under assumptions
- // A = 1; B = 0 OR A = 1; B = 1
- nLits = 2;
- pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 );
- pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
- if ( p->iOutputLit > -1 )
- pLits[nLits++] = p->iOutputLit;
- 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 + nLits,
- (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
-p->timeSat += clock() - clk;
- if ( RetValue1 == l_False )
- {
-p->timeSatUnsat += clock() - clk;
- if ( nLits == 2 )
- {
- 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
- nLits = 2;
- pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 );
- pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
- if ( p->iOutputLit > -1 )
- pLits[nLits++] = p->iOutputLit;
- if ( p->pPars->fPolarFlip )
- {
- if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
- if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
- }
-/*
- if ( p->pSat->qtail != p->pSat->qhead )
- {
- RetValue = sat_solver_simplify(p->pSat);
- assert( RetValue != 0 );
- }
-*/
-clk = clock();
- RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + nLits,
- (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
-p->timeSat += clock() - clk;
- if ( RetValue1 == l_False )
- {
-p->timeSatUnsat += clock() - clk;
- if ( nLits == 2 )
- {
- 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, fComplNew;
- Aig_Obj_t * pTemp;
-
- // sanity checks
- assert( Aig_Regular(pOld) != Aig_Regular(pNew) );
-
- // move constant to the old node
- if ( Aig_Regular(pNew) == Aig_ManConst1(p->pFrames) )
- {
- assert( Aig_Regular(pOld) != Aig_ManConst1(p->pFrames) );
- pTemp = pOld;
- pOld = pNew;
- pNew = pTemp;
- }
-
- // move complement to the new node
- if ( Aig_IsComplement(pOld) )
- {
- pOld = Aig_Regular(pOld);
- pNew = Aig_Not(pNew);
- }
-
- // start the solver
- if ( p->pSat == NULL )
- Ssw_ManStartSolver( p );
-
- // if the nodes do not have SAT variables, allocate them
- Ssw_CnfNodeAddToSolver( p, pOld );
- Ssw_CnfNodeAddToSolver( p, Aig_Regular(pNew) );
-
- // transform the new node
- fComplNew = Aig_IsComplement( pNew );
- pNew = Aig_Regular( pNew );
-
- // consider the constant 1 case
- if ( pOld == Aig_ManConst1(p->pFrames) )
- {
- // add constaint A = 1 ----> A
- pLits[0] = toLitCond( Ssw_ObjSatNum(p,pNew), fComplNew );
- 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
- {
- // add constaint A = B ----> (A v !B)(!A v B)
-
- // (A v !B)
- pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 );
- pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), !fComplNew );
- 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 );
-
- // (!A v B)
- pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 );
- pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), fComplNew);
- 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 );
- }
- return 1;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-20 05:50:12 +0000