void Solver::uncheckedEnqueue(Lit p, Clause* from)
{
#ifdef __PRINT  
  if (from) {
    printClause(*from);
  }
  
  printf("--> ");
  printLit(p);
  printf("\n");

  if (decisionLevel() == 0) {
    printf("Zl: ");
    printLit(p);
    printf("\n");

  }
#endif
    

  assigns [var(p)] = toInt(lbool(!sign(p)));  // <<== abstract but not uttermost effecient
  level   [var(p)] = decisionLevel();
  reason  [var(p)] = from;
  trail.push(p);
}

void Engine::btToLevel(int level) {
	if (decisionLevel() == 0 && level == 0) return;
	assert(decisionLevel() > level);

	btToPos(trail_lim[level]);
  trail_lim.resize(level);
	dec_info.resize(level);
}

double Solver::progressEstimate() const
{
    double  progress = 0;
    double  F = 1.0 / nVars();

    for (int i = 0; i <= decisionLevel(); i++){
        int beg = i == 0 ? 0 : trail_lim[i - 1];
        int end = i == decisionLevel() ? trail.size() : trail_lim[i];
        progress += pow(F, i) * (end - beg);
    }

    return progress / nVars();
}

int MIP::doSimplex() {
//	printf("start simplex\n");
	int r = SIMPLEX_IN_PROGRESS;
	int steps = 0;
	int limit = getLimit();
	for ( ; steps < limit; steps++) {
		if ((r = simplex.simplex()) != SIMPLEX_IN_PROGRESS) break;
//		if (i == limit-1) printf("limit exceeded\n");
//		if (i%10 == 0) printf("Optimum = %.3f, ", optimum());
	}
	simplex.calcObjBound();

//	if (MIP_DEBUG) {
		int bound = (int) ceil((double) simplex.optimum());
		if (engine.opt_type == OPT_MAX) bound = -bound;
		if (steps) fprintf(stderr, "level = %d, %d simplex steps, status = %d, bound = %d\n", decisionLevel(), steps, r, bound);
//		fprintf(stderr, "%d simplex steps, status = %d, bound = %d\n", steps, r, bound);
//		fprintf(stderr, "%d %d\n", bound, engine.opt_type == OPT_MIN ? vars[0]->getMin() : -vars[0]->getMax());
//	}
		exit(0);


	if (decisionLevel() == 0) simplex.saveState(simplex.root);

	return r;
}

bool Solver::addClause(vec<Lit>& ps)
{
    assert(decisionLevel() == 0);

    if (!ok)
        return false;
    else{
        // Check if clause is satisfied and remove false/duplicate literals:
        sort(ps);
        Lit p; int i, j;
        for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
            if (value(ps[i]) == l_True || ps[i] == ~p)
                return true;
            else if (value(ps[i]) != l_False && ps[i] != p)
                ps[j++] = p = ps[i];
        ps.shrink(i - j);
    }

    if (ps.size() == 0)
        return ok = false;
    else if (ps.size() == 1){
        assert(value(ps[0]) == l_Undef);
        uncheckedEnqueue(ps[0]);
        return ok = (propagate() == NULL);
    }else{
        Clause* c = Clause_new(ps, false);
        clauses.push(c);
        attachClause(*c);
    }

    return true;
}

bool SimpSMTSolver::asymm(Var v, Clause& c)
{
  assert(decisionLevel() == 0);

  if (c.mark() || satisfied(c)) return true;

  trail_lim.push(trail.size());
  Lit l = lit_Undef;
  for (int i = 0; i < c.size(); i++)
    if (var(c[i]) != v && value(c[i]) != l_False)
    {
      uncheckedEnqueue(~c[i]);
    }
    else
      l = c[i];

  if (propagate() != NULL){
    cancelUntil(0);
    asymm_lits++;
    if (!strengthenClause(c, l))
      return false;
  }else
    cancelUntil(0);

  return true;
}

/*_________________________________________________________________________________________________
|
|  analyzeFinal : (p : Lit)  ->  [void]
|  
|  Description:
|    Specialized analysis procedure to express the final conflict in terms of assumptions.
|    Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
|    stores the result in 'out_conflict'.
|_________________________________[email protected]*/
void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
{
    out_conflict.clear();
    out_conflict.push(p);

    if (decisionLevel() == 0)
        return;

    seen[var(p)] = 1;

    for (int i = trail.size()-1; i >= trail_lim[0]; i--){
        Var x = var(trail[i]);
        if (seen[x]){
            if (reason[x] == NULL){
                assert(level[x] > 0);
                out_conflict.push(~trail[i]);
            }else{
                Clause& c = *reason[x];
                for (int j = 1; j < c.size(); j++)
                    if (level[var(c[j])] > 0)
                        seen[var(c[j])] = 1;
            }
            seen[x] = 0;
        }
    }

    seen[var(p)] = 0;
}

void SAT::addClause(Clause& c, bool one_watch) {
	assert(c.size() > 0);
	if (c.size() == 1) {
		assert(decisionLevel() == 0);
		if (DEBUG) fprintf(stderr, "warning: adding length 1 clause!\n");
		if (value(c[0]) == l_False) TL_FAIL();
		if (value(c[0]) == l_Undef) enqueue(c[0]);
		free(&c);
		return;
	}
	if (!c.learnt) {
		if (c.size() == 2) bin_clauses++;
		else if (c.size() == 3) tern_clauses++;
		else long_clauses++;
	}

	// Mark lazy lits which are used
	if (c.learnt) for (int i = 0; i < c.size(); i++) incVarUse(var(c[i]));

	if (c.size() == 2) {
		if (!one_watch) watches[toInt(~c[0])].push(c[1]);
		watches[toInt(~c[1])].push(c[0]);
		if (!c.learnt) free(&c);
		return;
	}
	if (!one_watch) watches[toInt(~c[0])].push(&c);
	watches[toInt(~c[1])].push(&c);
	if (c.learnt) learnts_literals += c.size();
	else            clauses_literals += c.size();
        
	if (c.received) receiveds.push(&c);
        else if (c.learnt) learnts.push(&c);
	else            clauses.push(&c);
}

/*_________________________________________________________________________________________________
|
|  simplify : [void]  ->  [bool]
|  
|  Description:
|    Simplify the clause database according to the current top-level assigment. Currently, the only
|    thing done here is the removal of satisfied clauses, but more things can be put here.
|_________________________________[email protected]*/
bool MiniSATP::simplify()
{
    remove_satisfied = false;
    assert(decisionLevel() == 0);

    // Modified Lines
    // if (!ok || propagate() != NULL)
        // return ok = false;
    if (!ok) return false;
    Clause * confl = propagate( );
    if ( confl != NULL )
    {
      fillExplanation( confl );
      return ok = false;
    }

    if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
        return true;

    // Remove satisfied clauses:
    removeSatisfied(learnts);
    if (remove_satisfied)        // Can be turned off.
        removeSatisfied(clauses);

    // Remove fixed variables from the variable heap:
    order_heap.filter(VarFilter(*this));

    simpDB_assigns = nAssigns();
    simpDB_props   = clauses_literals + learnts_literals;   // (shouldn't depend on stats really, but it will do for now)

    return true;
}

void SimpSolver::remember(Var v)
{
    assert(decisionLevel() == 0);
    assert(isEliminated(v));

    vec<Lit> clause;

    // Re-activate variable:
    elimtable[v].order = 0;
    setDecisionVar(v, true); // Not good if the variable wasn't a decision variable before. Not sure how to fix this right now.

    if (use_simplification)
        updateElimHeap(v);

    // Reintroduce all old clauses which may implicitly remember other clauses:
    for (int i = 0; i < elimtable[v].eliminated.size(); i++){
        Clause& c = *elimtable[v].eliminated[i];
        clause.clear();
        for (int j = 0; j < c.size(); j++)
            clause.push(c[j]);

        remembered_clauses++;
        check(addClause(clause));
        free(&c);
    }

    elimtable[v].eliminated.clear();
}

// Can assume everything has been propagated! (esp. the first two literals are != l_False, unless
// the clause is binary and satisfied, in which case the first literal is true)
// Returns True if clause is satisfied (will be removed), False otherwise.
//
bool Solver::simplify(Clause* c) const
{
    assert(decisionLevel() == 0);
    for (int i = 0; i < c->size(); i++){
        if (value((*c)[i]) == l_True)
            return true;
    }
    return false;
}

// Revert to the state at given level (keeping all assignment at 'level' but not beyond).
//
void Solver::cancelUntil(int level) {
    if (decisionLevel() > level){
        for (int c = trail.size()-1; c >= trail_lim[level]; c--){
            Var     x  = var(trail[c]);
            assigns[x] = toInt(l_Undef);
            insertVarOrder(x); }
        qhead = trail_lim[level];
        trail.shrink(trail.size() - trail_lim[level]);
        trail_lim.shrink(trail_lim.size() - level);
    } }

// Revert to the state at given level.
void Solver::cancelUntil(int level) {
    if (decisionLevel() > level){
        for (int c = trail.size()-1; c >= trail_lim[level]; c--){
            Var     x  = var(trail[c]);
            assigns[x] = toInt(l_Undef);
            reason [x] = GClause_NULL;
            order.undo(x); }
        trail.shrink(trail.size() - trail_lim[level]);
        trail_lim.shrink(trail_lim.size() - level);
        qhead = trail.size(); } }

void SAT::addClause(Lit p, Lit q) {
	if (value(p) == l_True || value(q) == l_True) return;
	if (value(p) == l_False && value(q) == l_False) {
		assert(false);
		TL_FAIL();
	}
	if (value(p) == l_False) {
		assert(decisionLevel() == 0);
		enqueue(q);
		return;
	}
	if (value(q) == l_False) {
		assert(decisionLevel() == 0);
		enqueue(p);
		return;
	}
	bin_clauses++;
	watches[toInt(~p)].push(q);
	watches[toInt(~q)].push(p);
}

/*_________________________________________________________________________________________________
|
|  enqueue : (p : Lit) (from : Clause*)  ->  [bool]
|  
|  Description:
|    Puts a new fact on the propagation queue as well as immediately updating the variable's value.
|    Should a conflict arise, FALSE is returned.
|  
|  Input:
|    p    - The fact to enqueue
|    from - [Optional] Fact propagated from this (currently) unit clause. Stored in 'reason[]'.
|           Default value is NULL (no reason).
|  
|  Output:
|    TRUE if fact was enqueued without conflict, FALSE otherwise.
|_________________________________[email protected]*/
bool Solver::enqueue(Lit p, GClause from)
{
    if (value(p) != l_Undef)
        return value(p) != l_False;
    else{
        assigns[var(p)] = toInt(lbool(!sign(p)));
        level  [var(p)] = decisionLevel();
        reason [var(p)] = from;
        trail.push(p);
        return true;
    }
}

inline void SAT::untrailToPos(vec<Lit>& t, int p) {
	int dl = decisionLevel();

	for (int i = t.size(); i-- > p; ) {
		int x = var(t[i]);
		assigns[x] = toInt(l_Undef);
#if PHASE_SAVING
		if (so.phase_saving >= 1 || (so.phase_saving == 1 && dl >= l0))
			polarity[x] = sign(t[i]);
#endif
		insertVarOrder(x);
	}
	t.resize(p);
}

void Solver::saveState()
{
    for (int i = 0; i < watchBackup.changed.size(); i++) {
        const int which = watchBackup.changed[i];

        assert(watchBackup.flags[which] == true);
        watchBackup.flags[which] = false;
    }
    watchBackup.changed.clear();

    backup.touchedClauses.clear();
    backup.sublevel = trail.size();
    backup.level = decisionLevel();
}

void Solver::uncheckedEnqueue(Lit p, Clause* from)
{
    #ifdef RESTORE
    if (backup.stage == 0) {
        printf("setting lit "); printLit(p); printf(" decLevel: %d flag: %d detachedClause: %p\n", decisionLevel(), backup.stage, backup.detachedClause);
    }
    #endif

    assert(value(p) == l_Undef);
    assigns [var(p)] = toInt(lbool(!sign(p)));  // <<== abstract but not uttermost effecient
    level   [var(p)] = decisionLevel();
    reason  [var(p)] = from;
    polarity[var(p)] = sign(p);
    trail.push(p);
}

void SAT::btToLevel(int level) {
  if (decisionLevel() <= level) return;

	for (int l = trail.size(); l-- > level+1; ) {
		untrailToPos(trail[l], 0);
		for (int i = rtrail[l].size(); i--; ) {
			free(rtrail[l][i]);
		}
	}
  trail.resize(level+1);
	qhead.resize(level+1);
	rtrail.resize(level+1);

	engine.btToLevel(level);
	if (so.mip) mip->btToLevel(level);

}

lbool SimpSolver::solve(const vec<Lit>& assumps, bool do_simp, bool turn_off_simp) {
    vec<Var> extra_frozen;
    lbool     result = l_True;

    do_simp &= use_simplification;
    do_simp &= (decisionLevel() == 0);

    if (do_simp){

        // Assumptions must be temporarily frozen to run variable elimination:
        for (int i = 0; i < assumps.size(); i++){
            Var v = var(assumps[i]);

            // If an assumption has been eliminated, remember it.
            if (isEliminated(v))
                remember(v);

            if (!frozen[v]){
                // Freeze and store.
                setFrozen(v, true);
                extra_frozen.push(v);
            } }

	if(eliminate(turn_off_simp))
	  result = l_True;
	else
	  result = l_False;
    }

    if (result == l_True) 
      result = Solver::solve(assumps);

    if (result == l_True) {
        extendModel();
#ifndef NDEBUG
        verifyModel();
#endif
    }

    if (do_simp)
        // Unfreeze the assumptions that were frozen:
        for (int i = 0; i < extra_frozen.size(); i++)
            setFrozen(extra_frozen[i], false);

    return result;
}