diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2010-11-01 01:35:04 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2010-11-01 01:35:04 -0700 |
commit | 6130e39b18b5f53902e4eab14f6d5cdde5219563 (patch) | |
tree | 0db0628479a1b750e9af1f66cb8379ebd0913d31 /src/sat/msat/msatSolverSearch.c | |
parent | f0e77f6797c0504b0da25a56152b707d3357f386 (diff) | |
download | abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.tar.gz abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.tar.bz2 abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.zip |
initial commit of public abc
Diffstat (limited to 'src/sat/msat/msatSolverSearch.c')
-rw-r--r-- | src/sat/msat/msatSolverSearch.c | 11 |
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 + |