APIs to represent simple gates in CNF.

1 files changed, 112 insertions, 0 deletions

diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index ebd999b1..f3d70deb 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -264,6 +264,118 @@ static inline int sat_solver2_bookmark(sat_solver2* s)
     s->iVarPivot    = s->size;
 }
 
+static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark )
+{
+    lit Lits[1];
+    int Cid;
+    assert( iVar >= 0 );
+
+    Lits[0] = toLitCond( iVar, fCompl );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 1 );
+    if ( fMark )
+        clause_set_partA( pSat, Cid, 1 );
+    return 1;
+}
+static inline int sat_solver2_add_buffer( sat_solver2 * pSat, int iVarA, int iVarB, int fCompl, int fMark )
+{
+    lit Lits[2];
+    int Cid;
+    assert( iVarA >= 0 && iVarB >= 0 );
+
+    Lits[0] = toLitCond( iVarA, 0 );
+    Lits[1] = toLitCond( iVarB, !fCompl );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
+    if ( fMark )
+        clause_set_partA( pSat, Cid, 1 );
+
+    Lits[0] = toLitCond( iVarA, 1 );
+    Lits[1] = toLitCond( iVarB, fCompl );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
+    if ( fMark )
+        clause_set_partA( pSat, Cid, 1 );
+    return 2;
+}
+static inline int sat_solver2_add_and( sat_solver2 * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fMark )
+{
+    lit Lits[3];
+    int Cid;
+
+    Lits[0] = toLitCond( iVar, 1 );
+    Lits[1] = toLitCond( iVar0, fCompl0 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
+    if ( fMark )
+        clause_set_partA( pSat, Cid, 1 );
+
+    Lits[0] = toLitCond( iVar, 1 );
+    Lits[1] = toLitCond( iVar1, fCompl1 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
+    if ( fMark )
+        clause_set_partA( pSat, Cid, 1 );
+
+    Lits[0] = toLitCond( iVar, 0 );
+    Lits[1] = toLitCond( iVar0, !fCompl0 );
+    Lits[2] = toLitCond( iVar1, !fCompl1 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
+    if ( fMark )
+        clause_set_partA( pSat, Cid, 1 );
+    return 3;
+}
+static inline int sat_solver2_add_xor( sat_solver2 * pSat, int iVarA, int iVarB, int iVarC, int fCompl, int fMark )
+{
+    lit Lits[3];
+    int Cid;
+    assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
+
+    Lits[0] = toLitCond( iVarA, !fCompl );
+    Lits[1] = toLitCond( iVarB, 1 );
+    Lits[2] = toLitCond( iVarC, 1 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
+    if ( fMark )
+        clause_set_partA( pSat, Cid, 1 );
+
+    Lits[0] = toLitCond( iVarA, !fCompl );
+    Lits[1] = toLitCond( iVarB, 0 );
+    Lits[2] = toLitCond( iVarC, 0 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
+    if ( fMark )
+        clause_set_partA( pSat, Cid, 1 );
+
+    Lits[0] = toLitCond( iVarA, fCompl );
+    Lits[1] = toLitCond( iVarB, 1 );
+    Lits[2] = toLitCond( iVarC, 0 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
+    if ( fMark )
+        clause_set_partA( pSat, Cid, 1 );
+
+    Lits[0] = toLitCond( iVarA, fCompl );
+    Lits[1] = toLitCond( iVarB, 0 );
+    Lits[2] = toLitCond( iVarC, 1 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
+    if ( fMark )
+        clause_set_partA( pSat, Cid, 1 );
+    return 4;
+}
+static inline int sat_solver2_add_constraint( sat_solver2 * pSat, int iVar, int fCompl, int fMark )
+{
+    lit Lits[2];
+    int Cid;
+    assert( iVar >= 0 );
+
+    Lits[0] = toLitCond( iVar, fCompl );
+    Lits[1] = toLitCond( iVar+1, 0 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
+    if ( fMark )
+        clause_set_partA( pSat, Cid, 1 );
+
+    Lits[0] = toLitCond( iVar, fCompl );
+    Lits[1] = toLitCond( iVar+1, 1 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
+    if ( fMark )
+        clause_set_partA( pSat, Cid, 1 );
+    return 2;
+}
+
+
 ABC_NAMESPACE_HEADER_END
 
 #endif