From b556c2591e8dc6e35d523971aa467bce4ad6200e Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 27 Feb 2014 21:11:05 -0800
Subject: Changes to LUT mappers.

---
 src/sat/bsat/satSolver.h | 46 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)

(limited to 'src/sat/bsat/satSolver.h')

diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 0d46b86b..345bbd28 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -368,6 +368,52 @@ static inline int sat_solver_add_xor( sat_solver * pSat, int iVarA, int iVarB, i
     assert( Cid );
     return 4;
 }
+static inline int sat_solver_add_mux( sat_solver * pSat, int iVarC, int iVarT, int iVarE, int iVarZ )
+{
+    lit Lits[3];
+    int Cid;
+    assert( iVarC >= 0 && iVarT >= 0 && iVarE >= 0 && iVarZ >= 0 );
+
+    Lits[0] = toLitCond( iVarC, 1 );
+    Lits[1] = toLitCond( iVarT, 1 );
+    Lits[2] = toLitCond( iVarZ, 0 );
+    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarC, 1 );
+    Lits[1] = toLitCond( iVarT, 0 );
+    Lits[2] = toLitCond( iVarZ, 1 );
+    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarC, 0 );
+    Lits[1] = toLitCond( iVarE, 1 );
+    Lits[2] = toLitCond( iVarZ, 0 );
+    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarC, 0 );
+    Lits[1] = toLitCond( iVarE, 0 );
+    Lits[2] = toLitCond( iVarZ, 1 );
+    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    if ( iVarT == iVarE )
+        return 4;
+
+    Lits[0] = toLitCond( iVarT, 0 );
+    Lits[1] = toLitCond( iVarE, 0 );
+    Lits[2] = toLitCond( iVarZ, 1 );
+    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarT, 1 );
+    Lits[1] = toLitCond( iVarE, 1 );
+    Lits[2] = toLitCond( iVarZ, 0 );
+    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+    return 6;
+}
 static inline int sat_solver_add_xor_and( sat_solver * pSat, int iVarF, int iVarA, int iVarB, int iVarC )
 {
     // F = (a (+) b) * c
-- 
cgit v1.2.3