summaryrefslogtreecommitdiffstats
path: root/src/sat/msat/msatSolverSearch.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/msat/msatSolverSearch.c')
-rw-r--r--src/sat/msat/msatSolverSearch.c11
1 files changed, 8 insertions, 3 deletions
diff --git a/src/sat/msat/msatSolverSearch.c b/src/sat/msat/msatSolverSearch.c
index 11a6540c..b3190e39 100644
--- a/src/sat/msat/msatSolverSearch.c
+++ b/src/sat/msat/msatSolverSearch.c
@@ -20,6 +20,9 @@
#include "msatInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -45,7 +48,7 @@ static void Msat_SolverReduceDB( Msat_Solver_t * p );
SeeAlso []
***********************************************************************/
-bool Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit )
+int Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit )
{
assert( Msat_QueueReadSize(p->pQueue) == 0 );
if ( p->fVerbose )
@@ -167,7 +170,7 @@ Msat_Clause_t * Msat_SolverRecord( Msat_Solver_t * p, Msat_IntVec_t * vLits )
SeeAlso []
***********************************************************************/
-bool Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC )
+int Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC )
{
Msat_Var_t Var = MSAT_LIT2VAR(Lit);
@@ -276,7 +279,7 @@ Msat_Clause_t * Msat_SolverPropagate( Msat_Solver_t * p )
SeeAlso []
***********************************************************************/
-bool Msat_SolverSimplifyDB( Msat_Solver_t * p )
+int Msat_SolverSimplifyDB( Msat_Solver_t * p )
{
Msat_ClauseVec_t * vClauses;
Msat_Clause_t ** pClauses;
@@ -627,3 +630,5 @@ Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLi
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+