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

 * Top contributors (to current version):

 *   Liana Hadarean, Mathias Preiner, Tim King

 *

 * This file is part of the cvc5 project.

 *

 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS

 * in the top-level source directory and their institutional affiliations.

 * All rights reserved.  See the file COPYING in the top-level source

 * directory for licensing information.

 * ****************************************************************************

 *

 * Algebraic solver.

 */

#include "cvc5_private.h"

#pragma once

#include <unordered_map>

#include <unordered_set>

#include "theory/bv/bv_subtheory.h"

#include "theory/bv/slicer.h"

#include "theory/substitutions.h"

namespace cvc5 {

namespace theory {

namespace bv {

class AlgebraicSolver;

Node mergeExplanations(TNode expl1, TNode expl2);

Node mergeExplanations(const std::vector<Node>& expls);

/**

 * Non-context dependent substitution with explanations.

 *

 */

{

  {

    Node to;

    Node reason;

  };

  {

    TNode node;

    bool childrenAdded;

    {

  };

  typedef std::unordered_map<Node, SubstitutionElement> Substitutions;

  typedef std::unordered_map<Node, SubstitutionElement> SubstitutionsCache;

  Substitutions d_substitutions;

  SubstitutionsCache d_cache;

  bool d_cacheInvalid;

  theory::SubstitutionMap* d_modelMap;

  Node getReason(TNode node) const;

  bool hasCache(TNode node) const;

  Node getCache(TNode node) const;

  void storeCache(TNode from, TNode to, Node rason);

  Node internalApply(TNode node);

 public:

  SubstitutionEx(theory::SubstitutionMap* modelMap);

  /**

   * Returnst true if the substitution map did not contain from.

   *

   * @param from

   * @param to

   * @param reason

   *

   * @return

   */

  bool addSubstitution(TNode from, TNode to, TNode reason);

  Node apply(TNode node);

  Node explain(TNode node) const;

};

/**

 * In-processing worklist element, id keeps track of

 * original assertion.

 *

 */

{

  Node node;

  unsigned id;

};

typedef std::unordered_map<Node, Node> NodeNodeMap;

typedef std::unordered_map<Node, unsigned> NodeIdMap;

typedef std::unordered_set<TNode> TNodeSet;

class ExtractSkolemizer

{

  struct Extract

  {

    unsigned high;

    unsigned low;

  };

  {

    Base base;

    std::vector<Extract> extracts;

    void addExtract(Extract& e);

  };

  typedef std::unordered_map<Node, ExtractList> VarExtractMap;

  context::Context d_emptyContext;

  VarExtractMap d_varToExtract;

  theory::SubstitutionMap* d_modelMap;

  theory::SubstitutionMap d_skolemSubst;

  theory::SubstitutionMap d_skolemSubstRev;

  void storeSkolem(TNode node, TNode skolem);

  void storeExtract(TNode var, unsigned high, unsigned low);

  void collectExtracts(TNode node, TNodeSet& seen);

  Node skolemize(TNode);

  Node unSkolemize(TNode);

  Node mkSkolem(Node node);

 public:

  ExtractSkolemizer(theory::SubstitutionMap* modelMap);

  void skolemize(std::vector<WorklistElement>&);

  void unSkolemize(std::vector<WorklistElement>&);

  ~ExtractSkolemizer();

};

class BVQuickCheck;

class QuickXPlain;

/**

 * AlgebraicSolver

 */

class AlgebraicSolver : public SubtheorySolver

{

  struct Statistics

  {

    IntStat d_numCallstoCheck;

    IntStat d_numSimplifiesToTrue;

    IntStat d_numSimplifiesToFalse;

    IntStat d_numUnsat;

    IntStat d_numSat;

    IntStat d_numUnknown;

    TimerStat d_solveTime;

    ValueStat<double> d_useHeuristic;

    Statistics();

  };

  std::unique_ptr<SubstitutionMap> d_modelMap;

  std::unique_ptr<BVQuickCheck> d_quickSolver;

  context::CDO<bool> d_isComplete;

  context::CDO<bool>

      d_isDifficult; /**< flag to indicate whether the current assertions

                        contain expensive BV operators */

  unsigned long d_budget;

  std::vector<Node> d_explanations; /**< explanations for assertions indexed by

                                       assertion id */

  TNodeSet d_inputAssertions; /**< assertions in current context (for debugging

                                 purposes only) */

  NodeIdMap d_ids;            /**< map from assertions to ids */

  uint64_t d_numSolved;

  uint64_t d_numCalls;

  /** separate quickXplain module as it can reuse the current SAT solver */

  std::unique_ptr<QuickXPlain> d_quickXplain;

  Statistics d_statistics;

  bool useHeuristic();

  void setConflict(TNode conflict);

  bool isSubstitutableIn(TNode node, TNode in);

  bool checkExplanation(TNode expl);

  void storeExplanation(TNode expl);

  void storeExplanation(unsigned id, TNode expl);

  /**

   * Apply substitutions and rewriting to the worklist assertions to a fixpoint.

   * Subsitutions learned store in subst.

   *

   * @param worklist

   * @param subst

   */

  void processAssertions(std::vector<WorklistElement>& worklist,

                         SubstitutionEx& subst);

  /**

   * Attempt to solve the equation in fact, and if successful

   * add a substitution to subst.

   *

   * @param fact equation we are trying to solve

   * @param reason the reason in terms of original assertions

   * @param subst substitution map

   *

   * @return true if added a substitution to subst

   */

  bool solve(TNode fact, TNode reason, SubstitutionEx& subst);

  /**

   * Run a SAT solver on the given facts with the given budget.

   * Sets the isComplete flag and conflict accordingly.

   *

   * @param facts

   *

   * @return true if no conflict was detected.

   */

  bool quickCheck(std::vector<Node>& facts);

 public:

  AlgebraicSolver(context::Context* c, BVSolverLazy* bv);

  ~AlgebraicSolver();

  bool check(Theory::Effort e) override;

  {

  }

  EqualityStatus getEqualityStatus(TNode a, TNode b) override;

  bool collectModelValues(TheoryModel* m,

                          const std::set<Node>& termSet) override;

  Node getModelValue(TNode node) override;

  bool isComplete() override;

  void assertFact(TNode fact) override;

};

}  // namespace bv

}  // namespace theory

}  // namespace cvc5