summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2016-02-07 21:13:33 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2016-02-07 21:13:33 -0800
commit67f4f1adae4b3d27f19b95fc92ab9213feebf035 (patch)
tree0bb082d1baeb0352665d41b2b1de697dce1ddc0f /src/sat
parent59aea7639f87316ee9efb04a83309b7bb7888a8a (diff)
downloadabc-67f4f1adae4b3d27f19b95fc92ab9213feebf035.tar.gz
abc-67f4f1adae4b3d27f19b95fc92ab9213feebf035.tar.bz2
abc-67f4f1adae4b3d27f19b95fc92ab9213feebf035.zip
Experiments with SAT-based mapping.
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bsat/satSolver.h23
1 files changed, 23 insertions, 0 deletions
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index fc92e557..c7e324cd 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -581,6 +581,29 @@ static inline int sat_solver_add_constraint( sat_solver * pSat, int iVar, int iV
return 2;
}
+static inline int sat_solver_add_half_sorter( sat_solver * pSat, int iVarA, int iVarB, int iVar0, int iVar1 )
+{
+ lit Lits[3];
+ int Cid;
+
+ Lits[0] = toLitCond( iVarA, 0 );
+ Lits[1] = toLitCond( iVar0, 1 );
+ Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
+ assert( Cid );
+
+ Lits[0] = toLitCond( iVarA, 0 );
+ Lits[1] = toLitCond( iVar1, 1 );
+ Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
+ assert( Cid );
+
+ Lits[0] = toLitCond( iVarB, 0 );
+ Lits[1] = toLitCond( iVar0, 1 );
+ Lits[2] = toLitCond( iVar1, 1 );
+ Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
+ assert( Cid );
+ return 3;
+}
+
ABC_NAMESPACE_HEADER_END