summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
authorMathias Soeken <mathias.soeken@epfl.ch>2016-11-02 19:27:12 +0100
committerMathias Soeken <mathias.soeken@epfl.ch>2016-11-02 19:27:12 +0100
commitf9b7e929045f348ef6ccff9024de3be0c35c2eec (patch)
tree0a03dd2e4363cdf9ada92676cb2cd1131affb585 /src/base
parent16109b11f6eaed93359ba9c806d2924fc6404eb4 (diff)
downloadabc-f9b7e929045f348ef6ccff9024de3be0c35c2eec.tar.gz
abc-f9b7e929045f348ef6ccff9024de3be0c35c2eec.tar.bz2
abc-f9b7e929045f348ef6ccff9024de3be0c35c2eec.zip
Exact synthesis.
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abci/abcExact.c17
1 files changed, 16 insertions, 1 deletions
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c
index 757034cd..9ab1c3ac 100644
--- a/src/base/abci/abcExact.c
+++ b/src/base/abci/abcExact.c
@@ -1195,7 +1195,7 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
{
extern int Extra_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 );
- int h, i, j, k, t, ii, jj, kk, p, q;
+ int h, i, j, k, t, ii, jj, kk, iii, p, q;
int pLits[3];
Vec_Int_t * vLits = NULL;
@@ -1419,6 +1419,18 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, k, pSes->nSpecVars + i ), 1 );
sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
}
+ if ( pSes->nGates > 2 )
+ for ( i = 0; i < pSes->nGates - 2; ++i )
+ for ( ii = i + 1; ii < pSes->nGates - 1; ++ii )
+ for ( iii = ii + 1; iii < pSes->nGates; ++iii )
+ for ( k = 1; k < pSes->nSpecVars + i; ++k )
+ for ( j = 0; j < k; ++j )
+ {
+ pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
+ pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, j, k ), 1 );
+ pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, iii, i, ii ), 1 );
+ sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
+ }
/* EXTRA clauses: co-lexicographic order */
for ( i = 0; i < pSes->nGates - 1; ++i )
@@ -1595,6 +1607,9 @@ static inline int Ses_ManSolve( Ses_Man_t * pSes )
pSes->timeSatUndef += timeDelta;
if ( pSes->fSatVerbose )
{
+ //Sat_SolverWriteDimacs( pSes->pSat, "/tmp/test.cnf", Vec_IntArray( pSes->vAssump ), Vec_IntLimit( pSes->vAssump ), 1 );
+ //exit( 42 );
+
printf( "resource limit reached\n" );
}
return 2;