| /**CFile**************************************************************** |
| |
| FileName [msatSolverSearch.c] |
| |
| PackageName [A C version of SAT solver MINISAT, originally developed |
| in C++ by Niklas Een and Niklas Sorensson, Chalmers University of |
| Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] |
| |
| Synopsis [The search part of the solver.] |
| |
| Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - January 1, 2004.] |
| |
| Revision [$Id: msatSolverSearch.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "msatInt.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| static void Msat_SolverUndoOne( Msat_Solver_t * p ); |
| static void Msat_SolverCancel( Msat_Solver_t * p ); |
| static Msat_Clause_t * Msat_SolverRecord( Msat_Solver_t * p, Msat_IntVec_t * vLits ); |
| static void Msat_SolverAnalyze( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_IntVec_t * vLits_out, int * pLevel_out ); |
| static void Msat_SolverReduceDB( Msat_Solver_t * p ); |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Makes the next assumption (Lit).] |
| |
| Description [Returns FALSE if immediate conflict.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit ) |
| { |
| assert( Msat_QueueReadSize(p->pQueue) == 0 ); |
| if ( p->fVerbose ) |
| printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(Lit)); |
| Msat_IntVecPush( p->vTrailLim, Msat_IntVecReadSize(p->vTrail) ); |
| // assert( Msat_IntVecReadSize(p->vTrailLim) <= Msat_IntVecReadSize(p->vTrail) + 1 ); |
| // assert( Msat_IntVecReadSize( p->vTrailLim ) < p->nVars ); |
| return Msat_SolverEnqueue( p, Lit, NULL ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Reverts one variable binding on the trail.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_SolverUndoOne( Msat_Solver_t * p ) |
| { |
| Msat_Lit_t Lit; |
| Msat_Var_t Var; |
| Lit = Msat_IntVecPop( p->vTrail ); |
| Var = MSAT_LIT2VAR(Lit); |
| p->pAssigns[Var] = MSAT_VAR_UNASSIGNED; |
| p->pReasons[Var] = NULL; |
| p->pLevel[Var] = -1; |
| // Msat_OrderUndo( p->pOrder, Var ); |
| Msat_OrderVarUnassigned( p->pOrder, Var ); |
| |
| if ( p->fVerbose ) |
| printf(L_IND"unbind("L_LIT")\n", L_ind, L_lit(Lit)); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Reverts to the state before last Msat_SolverAssume().] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_SolverCancel( Msat_Solver_t * p ) |
| { |
| int c; |
| assert( Msat_QueueReadSize(p->pQueue) == 0 ); |
| if ( p->fVerbose ) |
| { |
| if ( Msat_IntVecReadSize(p->vTrail) != Msat_IntVecReadEntryLast(p->vTrailLim) ) |
| { |
| Msat_Lit_t Lit; |
| Lit = Msat_IntVecReadEntry( p->vTrail, Msat_IntVecReadEntryLast(p->vTrailLim) ); |
| printf(L_IND"cancel("L_LIT")\n", L_ind, L_lit(Lit)); |
| } |
| } |
| for ( c = Msat_IntVecReadSize(p->vTrail) - Msat_IntVecPop( p->vTrailLim ); c != 0; c-- ) |
| Msat_SolverUndoOne( p ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Reverts to the state at given level.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_SolverCancelUntil( Msat_Solver_t * p, int Level ) |
| { |
| while ( Msat_IntVecReadSize(p->vTrailLim) > Level ) |
| Msat_SolverCancel(p); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Record a clause and drive backtracking.] |
| |
| Description [vLits[0] must contain the asserting literal.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Msat_Clause_t * Msat_SolverRecord( Msat_Solver_t * p, Msat_IntVec_t * vLits ) |
| { |
| Msat_Clause_t * pC; |
| int Value; |
| assert( Msat_IntVecReadSize(vLits) != 0 ); |
| Value = Msat_ClauseCreate( p, vLits, 1, &pC ); |
| assert( Value ); |
| Value = Msat_SolverEnqueue( p, Msat_IntVecReadEntry(vLits,0), pC ); |
| assert( Value ); |
| if ( pC ) |
| Msat_ClauseVecPush( p->vLearned, pC ); |
| return pC; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Enqueues one variable assignment.] |
| |
| Description [Puts a new fact on the propagation queue and immediately |
| updates the variable value. Should a conflict arise, FALSE is returned. |
| Otherwise returns TRUE.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC ) |
| { |
| Msat_Var_t Var = MSAT_LIT2VAR(Lit); |
| |
| // skip literals that are not in the current cone |
| if ( !Msat_IntVecReadEntry( p->vVarsUsed, Var ) ) |
| return 1; |
| |
| // assert( Msat_QueueReadSize(p->pQueue) == Msat_IntVecReadSize(p->vTrail) ); |
| // if the literal is assigned |
| // return 1 if the assignment is consistent |
| // return 0 if the assignment is inconsistent (conflict) |
| if ( p->pAssigns[Var] != MSAT_VAR_UNASSIGNED ) |
| return p->pAssigns[Var] == Lit; |
| // new fact - store it |
| if ( p->fVerbose ) |
| { |
| // printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(Lit)); |
| printf(L_IND"bind("L_LIT") ", L_ind, L_lit(Lit)); |
| Msat_ClausePrintSymbols( pC ); |
| } |
| p->pAssigns[Var] = Lit; |
| p->pLevel[Var] = Msat_IntVecReadSize(p->vTrailLim); |
| // p->pReasons[Var] = p->pLevel[Var]? pC: NULL; |
| p->pReasons[Var] = pC; |
| Msat_IntVecPush( p->vTrail, Lit ); |
| Msat_QueueInsert( p->pQueue, Lit ); |
| |
| Msat_OrderVarAssigned( p->pOrder, Var ); |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Propagates the assignments in the queue.] |
| |
| Description [Propagates all enqueued facts. If a conflict arises, |
| the conflicting clause is returned, otherwise NULL.] |
| |
| SideEffects [The propagation queue is empty, even if there was a conflict.] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Msat_Clause_t * Msat_SolverPropagate( Msat_Solver_t * p ) |
| { |
| Msat_ClauseVec_t ** pvWatched = p->pvWatched; |
| Msat_Clause_t ** pClauses; |
| Msat_Clause_t * pConflict; |
| Msat_Lit_t Lit, Lit_out; |
| int i, j, nClauses; |
| |
| // propagate all the literals in the queue |
| while ( (Lit = Msat_QueueExtract( p->pQueue )) >= 0 ) |
| { |
| p->Stats.nPropagations++; |
| // get the clauses watched by this literal |
| nClauses = Msat_ClauseVecReadSize( pvWatched[Lit] ); |
| pClauses = Msat_ClauseVecReadArray( pvWatched[Lit] ); |
| // go through the watched clauses and decide what to do with them |
| for ( i = j = 0; i < nClauses; i++ ) |
| { |
| p->Stats.nInspects++; |
| // clear the returned literal |
| Lit_out = -1; |
| // propagate the clause |
| if ( !Msat_ClausePropagate( pClauses[i], Lit, p->pAssigns, &Lit_out ) ) |
| { // the clause is unit |
| // "Lit_out" contains the new assignment to be enqueued |
| if ( Msat_SolverEnqueue( p, Lit_out, pClauses[i] ) ) |
| { // consistent assignment |
| // no changes to the implication queue; the watch is the same too |
| pClauses[j++] = pClauses[i]; |
| continue; |
| } |
| // remember the reason of conflict (will be returned) |
| pConflict = pClauses[i]; |
| // leave the remaning clauses in the same watched list |
| for ( ; i < nClauses; i++ ) |
| pClauses[j++] = pClauses[i]; |
| Msat_ClauseVecShrink( pvWatched[Lit], j ); |
| // clear the propagation queue |
| Msat_QueueClear( p->pQueue ); |
| return pConflict; |
| } |
| // the clause is not unit |
| // in this case "Lit_out" contains the new watch if it has changed |
| if ( Lit_out >= 0 ) |
| Msat_ClauseVecPush( pvWatched[Lit_out], pClauses[i] ); |
| else // the watch did not change |
| pClauses[j++] = pClauses[i]; |
| } |
| Msat_ClauseVecShrink( pvWatched[Lit], j ); |
| } |
| return NULL; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Simplifies the data base.] |
| |
| Description [Simplify all constraints according to the current top-level |
| assigment (redundant constraints may be removed altogether).] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Msat_SolverSimplifyDB( Msat_Solver_t * p ) |
| { |
| Msat_ClauseVec_t * vClauses; |
| Msat_Clause_t ** pClauses; |
| int nClauses, Type, i, j; |
| int * pAssigns; |
| int Counter; |
| |
| assert( Msat_SolverReadDecisionLevel(p) == 0 ); |
| if ( Msat_SolverPropagate(p) != NULL ) |
| return 0; |
| //Msat_SolverPrintClauses( p ); |
| //Msat_SolverPrintAssignment( p ); |
| //printf( "Simplification\n" ); |
| |
| // simplify and reassign clause numbers |
| Counter = 0; |
| pAssigns = Msat_SolverReadAssignsArray( p ); |
| for ( Type = 0; Type < 2; Type++ ) |
| { |
| vClauses = Type? p->vLearned : p->vClauses; |
| nClauses = Msat_ClauseVecReadSize( vClauses ); |
| pClauses = Msat_ClauseVecReadArray( vClauses ); |
| for ( i = j = 0; i < nClauses; i++ ) |
| if ( Msat_ClauseSimplify( pClauses[i], pAssigns ) ) |
| Msat_ClauseFree( p, pClauses[i], 1 ); |
| else |
| { |
| pClauses[j++] = pClauses[i]; |
| Msat_ClauseSetNum( pClauses[i], Counter++ ); |
| } |
| Msat_ClauseVecShrink( vClauses, j ); |
| } |
| p->nClauses = Counter; |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Cleans the clause databased from the useless learnt clauses.] |
| |
| Description [Removes half of the learnt clauses, minus the clauses locked |
| by the current assignment. Locked clauses are clauses that are reason |
| to a some assignment.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_SolverReduceDB( Msat_Solver_t * p ) |
| { |
| Msat_Clause_t ** pLearned; |
| int nLearned, i, j; |
| double dExtraLim = p->dClaInc / Msat_ClauseVecReadSize(p->vLearned); |
| // Remove any clause below this activity |
| |
| // sort the learned clauses in the increasing order of activity |
| Msat_SolverSortDB( p ); |
| |
| // discard the first half the clauses (the less active ones) |
| nLearned = Msat_ClauseVecReadSize( p->vLearned ); |
| pLearned = Msat_ClauseVecReadArray( p->vLearned ); |
| for ( i = j = 0; i < nLearned / 2; i++ ) |
| if ( !Msat_ClauseIsLocked( p, pLearned[i]) ) |
| Msat_ClauseFree( p, pLearned[i], 1 ); |
| else |
| pLearned[j++] = pLearned[i]; |
| // filter the more active clauses and leave those above the limit |
| for ( ; i < nLearned; i++ ) |
| if ( !Msat_ClauseIsLocked( p, pLearned[i] ) && |
| Msat_ClauseReadActivity(pLearned[i]) < dExtraLim ) |
| Msat_ClauseFree( p, pLearned[i], 1 ); |
| else |
| pLearned[j++] = pLearned[i]; |
| Msat_ClauseVecShrink( p->vLearned, j ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Removes the learned clauses.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_SolverRemoveLearned( Msat_Solver_t * p ) |
| { |
| Msat_Clause_t ** pLearned; |
| int nLearned, i; |
| |
| // discard the learned clauses |
| nLearned = Msat_ClauseVecReadSize( p->vLearned ); |
| pLearned = Msat_ClauseVecReadArray( p->vLearned ); |
| for ( i = 0; i < nLearned; i++ ) |
| { |
| assert( !Msat_ClauseIsLocked( p, pLearned[i]) ); |
| |
| Msat_ClauseFree( p, pLearned[i], 1 ); |
| } |
| Msat_ClauseVecShrink( p->vLearned, 0 ); |
| p->nClauses = Msat_ClauseVecReadSize(p->vClauses); |
| |
| for ( i = 0; i < p->nVarsAlloc; i++ ) |
| p->pReasons[i] = NULL; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Removes the recently added clauses.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_SolverRemoveMarked( Msat_Solver_t * p ) |
| { |
| Msat_Clause_t ** pLearned, ** pClauses; |
| int nLearned, nClauses, i; |
| |
| // discard the learned clauses |
| nClauses = Msat_ClauseVecReadSize( p->vClauses ); |
| pClauses = Msat_ClauseVecReadArray( p->vClauses ); |
| for ( i = p->nClausesStart; i < nClauses; i++ ) |
| { |
| // assert( !Msat_ClauseIsLocked( p, pClauses[i]) ); |
| Msat_ClauseFree( p, pClauses[i], 1 ); |
| } |
| Msat_ClauseVecShrink( p->vClauses, p->nClausesStart ); |
| |
| // discard the learned clauses |
| nLearned = Msat_ClauseVecReadSize( p->vLearned ); |
| pLearned = Msat_ClauseVecReadArray( p->vLearned ); |
| for ( i = 0; i < nLearned; i++ ) |
| { |
| // assert( !Msat_ClauseIsLocked( p, pLearned[i]) ); |
| Msat_ClauseFree( p, pLearned[i], 1 ); |
| } |
| Msat_ClauseVecShrink( p->vLearned, 0 ); |
| p->nClauses = Msat_ClauseVecReadSize(p->vClauses); |
| /* |
| // undo the previous data |
| for ( i = 0; i < p->nVarsAlloc; i++ ) |
| { |
| p->pAssigns[i] = MSAT_VAR_UNASSIGNED; |
| p->pReasons[i] = NULL; |
| p->pLevel[i] = -1; |
| p->pdActivity[i] = 0.0; |
| } |
| Msat_OrderClean( p->pOrder, p->nVars, NULL ); |
| Msat_QueueClear( p->pQueue ); |
| */ |
| } |
| |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Analyze conflict and produce a reason clause.] |
| |
| Description [Current decision level must be greater than root level.] |
| |
| SideEffects [vLits_out[0] is the asserting literal at level pLevel_out.] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Msat_SolverAnalyze( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_IntVec_t * vLits_out, int * pLevel_out ) |
| { |
| Msat_Lit_t LitQ, Lit = MSAT_LIT_UNASSIGNED; |
| Msat_Var_t VarQ, Var; |
| int * pReasonArray, nReasonSize; |
| int j, pathC = 0, nLevelCur = Msat_IntVecReadSize(p->vTrailLim); |
| int iStep = Msat_IntVecReadSize(p->vTrail) - 1; |
| |
| // increment the seen counter |
| p->nSeenId++; |
| // empty the vector array |
| Msat_IntVecClear( vLits_out ); |
| Msat_IntVecPush( vLits_out, -1 ); // (leave room for the asserting literal) |
| *pLevel_out = 0; |
| do { |
| assert( pC != NULL ); // (otherwise should be UIP) |
| // get the reason of conflict |
| Msat_ClauseCalcReason( p, pC, Lit, p->vReason ); |
| nReasonSize = Msat_IntVecReadSize( p->vReason ); |
| pReasonArray = Msat_IntVecReadArray( p->vReason ); |
| for ( j = 0; j < nReasonSize; j++ ) { |
| LitQ = pReasonArray[j]; |
| VarQ = MSAT_LIT2VAR(LitQ); |
| if ( p->pSeen[VarQ] != p->nSeenId ) { |
| p->pSeen[VarQ] = p->nSeenId; |
| |
| // added to better fine-tune the search |
| Msat_SolverVarBumpActivity( p, LitQ ); |
| |
| // skip all the literals on this decision level |
| if ( p->pLevel[VarQ] == nLevelCur ) |
| pathC++; |
| else if ( p->pLevel[VarQ] > 0 ) { |
| // add the literals on other decision levels but |
| // exclude variables from decision level 0 |
| Msat_IntVecPush( vLits_out, MSAT_LITNOT(LitQ) ); |
| if ( *pLevel_out < p->pLevel[VarQ] ) |
| *pLevel_out = p->pLevel[VarQ]; |
| } |
| } |
| } |
| // Select next clause to look at: |
| do { |
| // Lit = Msat_IntVecReadEntryLast(p->vTrail); |
| Lit = Msat_IntVecReadEntry( p->vTrail, iStep-- ); |
| Var = MSAT_LIT2VAR(Lit); |
| pC = p->pReasons[Var]; |
| // Msat_SolverUndoOne( p ); |
| } while ( p->pSeen[Var] != p->nSeenId ); |
| pathC--; |
| } while ( pathC > 0 ); |
| // we do not unbind the variables above |
| // this will be done after conflict analysis |
| |
| Msat_IntVecWriteEntry( vLits_out, 0, MSAT_LITNOT(Lit) ); |
| if ( p->fVerbose ) |
| { |
| printf( L_IND"Learnt {", L_ind ); |
| nReasonSize = Msat_IntVecReadSize( vLits_out ); |
| pReasonArray = Msat_IntVecReadArray( vLits_out ); |
| for ( j = 0; j < nReasonSize; j++ ) |
| printf(" "L_LIT, L_lit(pReasonArray[j])); |
| printf(" } at level %d\n", *pLevel_out); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [The search procedure called between the restarts.] |
| |
| Description [Search for a satisfying solution as long as the number of |
| conflicts does not exceed the limit (nConfLimit) while keeping the number |
| of learnt clauses below the provided limit (nLearnedLimit). NOTE! Use |
| negative value for nConfLimit or nLearnedLimit to indicate infinity.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t * pPars ) |
| { |
| Msat_Clause_t * pConf; |
| Msat_Var_t Var; |
| int nLevelBack, nConfs, nAssigns, Value; |
| int i; |
| |
| assert( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot ); |
| p->Stats.nStarts++; |
| p->dVarDecay = 1 / pPars->dVarDecay; |
| p->dClaDecay = 1 / pPars->dClaDecay; |
| |
| // reset the activities |
| for ( i = 0; i < p->nVars; i++ ) |
| p->pdActivity[i] = (double)p->pFactors[i]; |
| // p->pdActivity[i] = 0.0; |
| |
| nConfs = 0; |
| while ( 1 ) |
| { |
| pConf = Msat_SolverPropagate( p ); |
| if ( pConf != NULL ){ |
| // CONFLICT |
| if ( p->fVerbose ) |
| { |
| // printf(L_IND"**CONFLICT**\n", L_ind); |
| printf(L_IND"**CONFLICT** ", L_ind); |
| Msat_ClausePrintSymbols( pConf ); |
| } |
| // count conflicts |
| p->Stats.nConflicts++; |
| nConfs++; |
| |
| // if top level, return UNSAT |
| if ( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot ) |
| return MSAT_FALSE; |
| |
| // perform conflict analysis |
| Msat_SolverAnalyze( p, pConf, p->vTemp, &nLevelBack ); |
| Msat_SolverCancelUntil( p, (p->nLevelRoot > nLevelBack)? p->nLevelRoot : nLevelBack ); |
| Msat_SolverRecord( p, p->vTemp ); |
| |
| // it is important that recording is done after cancelling |
| // because canceling cleans the queue while recording adds to it |
| Msat_SolverVarDecayActivity( p ); |
| Msat_SolverClaDecayActivity( p ); |
| |
| } |
| else{ |
| // NO CONFLICT |
| if ( Msat_IntVecReadSize(p->vTrailLim) == 0 ) { |
| // Simplify the set of problem clauses: |
| // Value = Msat_SolverSimplifyDB(p); |
| // assert( Value ); |
| } |
| nAssigns = Msat_IntVecReadSize( p->vTrail ); |
| if ( nLearnedLimit >= 0 && Msat_ClauseVecReadSize(p->vLearned) >= nLearnedLimit + nAssigns ) { |
| // Reduce the set of learnt clauses: |
| Msat_SolverReduceDB(p); |
| } |
| |
| Var = Msat_OrderVarSelect( p->pOrder ); |
| if ( Var == MSAT_ORDER_UNKNOWN ) { |
| // Model found and stored in p->pAssigns |
| memcpy( p->pModel, p->pAssigns, sizeof(int) * p->nVars ); |
| Msat_QueueClear( p->pQueue ); |
| Msat_SolverCancelUntil( p, p->nLevelRoot ); |
| return MSAT_TRUE; |
| } |
| if ( nConfLimit > 0 && nConfs > nConfLimit ) { |
| // Reached bound on number of conflicts: |
| p->dProgress = Msat_SolverProgressEstimate( p ); |
| Msat_QueueClear( p->pQueue ); |
| Msat_SolverCancelUntil( p, p->nLevelRoot ); |
| return MSAT_UNKNOWN; |
| } |
| else if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit ) { |
| // Reached bound on number of conflicts: |
| Msat_QueueClear( p->pQueue ); |
| Msat_SolverCancelUntil( p, p->nLevelRoot ); |
| return MSAT_UNKNOWN; |
| } |
| else{ |
| // New variable decision: |
| p->Stats.nDecisions++; |
| assert( Var != MSAT_ORDER_UNKNOWN && Var >= 0 && Var < p->nVars ); |
| Value = Msat_SolverAssume(p, MSAT_VAR2LIT(Var,0) ); |
| assert( Value ); |
| } |
| } |
| } |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
