/***************************************************************************************[Solver.cc]

Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson

Copyright (c) 2007-2010, Niklas Sorensson

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and

associated documentation files (the "Software"), to deal in the Software without restriction,

including without limitation the rights to use, copy, modify, merge, publish, distribute,

sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is

furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or

substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT

NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND

NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,

DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT

OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

**************************************************************************************************/

#include "prop/bvminisat/core/Solver.h"

#include <math.h>

#include <iostream>

#include <vector>

#include "base/check.h"

#include "base/exception.h"

#include "base/output.h"

#include "options/bv_options.h"

#include "options/smt_options.h"

#include "prop/bvminisat/mtl/Sort.h"

#include "theory/interrupted.h"

#include "util/utility.h"

namespace cvc5 {

namespace BVMinisat {

#define OUTPUT_TAG "bvminisat: [a=" << assumptions.size() << ",l=" << decisionLevel() << "] "

}

    }

  }

}

//=================================================================================================

// Options:

static const char* _cat = "CORE";

//=================================================================================================

// Proof declarations

CRef Solver::TCRef_Undef = CRef_Undef;

CRef Solver::TCRef_Lazy = CRef_Undef - 1; // no real lazy ref here

//=================================================================================================

// Constructor/Destructor:

    :

      // Parameters (user settable):

      //

      d_notify(nullptr),

      c(context),

      verbosity(0),

      var_decay(opt_var_decay),

      clause_decay(opt_clause_decay),

      random_var_freq(opt_random_var_freq),

      random_seed(opt_random_seed),

      luby_restart(opt_luby_restart),

      ccmin_mode(opt_ccmin_mode),

      phase_saving(opt_phase_saving),

      rnd_pol(false),

      rnd_init_act(opt_rnd_init_act),

      garbage_frac(opt_garbage_frac),

      restart_first(opt_restart_first),

      restart_inc(opt_restart_inc)

      // Parameters (the rest):

      //

      ,

      learntsize_factor((double)1 / (double)3),

      learntsize_inc(1.5)

      // Parameters (experimental):

      //

      ,

      learntsize_adjust_start_confl(100),

      learntsize_adjust_inc(1.5)

      // Statistics: (formerly in 'SolverStats')

      //

      ,

      solves(0),

      starts(0),

      decisions(0),

      rnd_decisions(0),

      propagations(0),

      conflicts(0),

      dec_vars(0),

      clauses_literals(0),

      learnts_literals(0),

      max_literals(0),

      tot_literals(0)

      ,

      need_to_propagate(false),

      only_bcp(false),

      clause_added(false),

      ok(true),

      cla_inc(1),

      var_inc(1),

      qhead(0),

      simpDB_assigns(-1),

      simpDB_props(0),

      progress_estimate(0),

      remove_satisfied(true)

      ,

      ca()

      // even though these are temporaries and technically should be set

      // before calling, lets initialize them. this will reduces chances of

      // non-determinism in portfolio (parallel) solver if variables are

      // being (incorrectly) used without initialization.

      ,

      seen(),

      analyze_stack(),

      analyze_toclear(),

      add_tmp(),

      max_learnts(0.0),

      learntsize_adjust_confl(0.0),

      learntsize_adjust_cnt(0)

      // Resource constraints:

      //

      ,

      conflict_budget(-1),

      propagation_budget(-1),

{

  // Create the constant variables

  // Assert the constants

{

//=================================================================================================

// Minor methods:

// Creates a new SAT variable in the solver. If 'decision' is cleared, variable will not be

// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).

//

{

    //activity .push(0);

}

{

    }

    }

    // Check if clause is satisfied and remove false/duplicate literals:

    // TODO proof for duplicate literals removal?

    Lit p; int i, j;

      // tautologies are ignored

      }

      // Ignore repeated literals

      }

      }

    }

      }

      } else {

      }

    }

}

  else

  {

    }else{

        // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause)

    }

    else

  // Don't leave pointers to free'd memory!

{

}

// Revert to the state at given level (keeping all assignment at 'level' but not beyond).

//

      {

        {

        }

      }

    }

//=================================================================================================

// Major methods:

{

    // Random decision:

    // Activity based decision:

        }else

}

/*_________________________________________________________________________________________________

|

|  analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&)  ->

[void]

|

|  Description:

|    Analyze conflict and produce a reason clause.

|

|    Pre-conditions:

|      * 'out_learnt' is assumed to be cleared.

|      * Current decision level must be greater than root level.

|

|    Post-conditions:

|      * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.

|      * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision

level of the |        rest of literals. There may be others from the same level

though.

|

|________________________________________________________________________________________________@*/

{

    // Generate conflict clause:

    //

      {

        {

          else

        }

      }

        // Select next clause to look at:

          break;

        }

    // Simplify conflict clause:

    //

    int i1, j;

                                     // involved in conflict)

        {

          {

          }

          else

          {

            // Check if the literal is redundant

            {

              // Literal is not redundant

            }

          }

        }

        for (i1 = j = 1; i1 < out_learnt.size(); i1++)

        {

          Var x = var(out_learnt[i1]);

          if (reason(x) == CRef_Undef)

            out_learnt[j++] = out_learnt[i1];

          else

          {

            Clause& clause = ca[reason(var(out_learnt[i1]))];

            for (int k = 1; k < clause.size(); k++)

              if (!seen[var(clause[k])] && level(var(clause[k])) > 0)

              {

                out_learnt[j++] = out_learnt[i1];

                break;

              }

          }

        }

    }else

    {

      {

      }

    }

    // Find correct backtrack level:

    //

    }

    else{

        // Find the first literal assigned at the next-highest level:

        // Swap-in this literal at i1 1:

    }

// Check if 'p' can be removed. 'abstract_levels' is used to abort early if the algorithm is

// visiting literals at levels that cannot be removed later.

{

          {

            {

            }

            else

            {

            }

          }

        }

    }

}

/**

 * Specialized analyzeFinal procedure where we test the consistency

 * of the assumptions before backtracking bellow the assumption level.

 *

 * @param p the original uip (may be unit)

 * @param confl_clause the conflict clause

 * @param out_conflict the conflict in terms of assumptions we are building

 */

  }

        // we skip p if was a learnt unit

          }

        }

      } else {

        {

        }

      }

    }

  }

/*_________________________________________________________________________________________________

|

|  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'.

|________________________________________________________________________________________________@*/

{

    }

    {

    }

              {

              }

            } else {

              {

                {

                }

              }

            }

        }

    }

}

{

  {

    {

    }

  }

}

  // TODO need to somehow mark the assumption as unit in the current context?

  // it's not always unit though, but this would be useful for debugging

  // Assert(marker[var(p)] == 1);

  }

  // add to the assumptions

  } else {

    ClauseId id;

    }

  }

  // run the propagation

  } else {

  }

}

  // make sure it wasn't already marked

/*_________________________________________________________________________________________________

|

|  propagate : [void]  ->  [Clause*]

|

|  Description:

|    Propagates all enqueued facts. If a conflict arises, the conflicting clause

is returned, |    otherwise CRef_Undef.

|

|    Post-conditions:

|      * the propagation queue is empty, even if there was a conflict.

|________________________________________________________________________________________________@*/

{

        Watcher        *i, *j, *end;

            // Try to avoid inspecting the clause:

            // Make sure the false literal is data[1]:

            // If 0th watch is true, then clause is already satisfied.

            // Look for new watch:

              {

              }

            // Did not find watch -- clause is unit under assignment:

                // Copy the remaining watches:

            }else

        }

    }

}

/*_________________________________________________________________________________________________

|

|  reduceDB : ()  ->  [void]

|

|  Description:

|    Remove half of the learnt clauses, minus the clauses locked by the current

assignment. Locked |    clauses are clauses that are reason to some assignment.

Binary clauses are never removed.

|________________________________________________________________________________________________@*/

struct reduceDB_lt

{

  ClauseAllocator& ca;

  {

  }

};

{

    int     i, j;

    // Don't delete binary or locked clauses. From the rest, delete clauses from the first half

    // and clauses with activity smaller than 'extra_lim':

      else

    }

{

    int i, j;

      {

      }

        else

    }

{

/*_________________________________________________________________________________________________

|

|  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.

|________________________________________________________________________________________________@*/

{

  // Remove satisfied clauses:

                                            // really, but it will do for now)

}

/*_________________________________________________________________________________________________

|

|  search : (nof_conflicts : int) (params : const SearchParams&)  ->  [lbool]

|

|  Description:

|    Search for a model the specified number of conflicts.

|    NOTE! Use negative value for 'nof_conflicts' indicate infinity.

|

|  Output:

|    'l_True' if a partial assigment that is consistent with respect to the

clauseset is found. If |    all variables are decision variables, this means

that the clause set is satisfiable. 'l_False' |    if the clause set is

unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.

|________________________________________________________________________________________________@*/

{

  int backtrack_level;

  for (;;)

  {

    {

      // CONFLICT

      {

        // can this happen for bv?

      }

      // bool assumption = marker[var(p)] == 2;

      {

      }

      {

        // learning a unit clause

      }

      //  if the uip was an assumption we are unsat

      {

        {

        }

      }

      {

        // check if uip leads to a conflict

        {

          {

            // we have a conflict we now need to explain it

          }

        }

      }

      {

                 nClauses(),

                 nLearnts(),

      }

    }

    else

    {

      // NO CONFLICT

      bool isWithinBudget;

      try

      {

            withinBudget(Resource::BvSatConflictsStep);

      }

      catch (const cvc5::theory::Interrupted& e)

      {

        // do some clean-up and rethrow

        cancelUntil(assumptions.size());

        throw e;

      }

      {

        // Reached bound on number of conflicts:

      }

      // Simplify the set of problem clauses:

      {

      }

      // We can't erase clauses if there is unprocessed assumptions, there might

      // be some propagationg we need to redu

      {

        // Reduce the set of learnt clauses:

      }

      {

        // Perform user provided assumption:

        {

          // Dummy decision level:

        }

        {

        }

        else

        {

        }

      }

      {

        {

        }

        // New variable decision:

        {

          // Model found:

        }

      }

      // Increase decision level and enqueue 'next'

    }

}

{

    }