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

 * Top contributors (to current version):

 *   Mathias Preiner, Liana Hadarean, Andrew Reynolds

 *

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

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

 *

 * Lazy bit-vector solver.

 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__BV__BV_SOLVER_LAZY_H

#define CVC5__THEORY__BV__BV_SOLVER_LAZY_H

#include <unordered_map>

#include <unordered_set>

#include "context/cdhashset.h"

#include "context/cdlist.h"

#include "context/context.h"

#include "theory/bv/bv_solver.h"

#include "theory/bv/bv_subtheory.h"

#include "theory/bv/theory_bv.h"

#include "util/hash.h"

namespace cvc5 {

namespace theory {

namespace bv {

class CoreSolver;

class InequalitySolver;

class AlgebraicSolver;

class BitblastSolver;

class EagerBitblastSolver;

class AbstractionModule;

class BVSolverLazy : public BVSolver

{

  /** Back reference to TheoryBV */

  TheoryBV& d_bv;

  /** The context we are using */

  context::Context* d_context;

  /** Context dependent set of atoms we already propagated */

  context::CDHashSet<Node> d_alreadyPropagatedSet;

  context::CDHashSet<Node> d_sharedTermsSet;

  std::vector<std::unique_ptr<SubtheorySolver>> d_subtheories;

  std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int>>

      d_subtheoryMap;

 public:

  BVSolverLazy(TheoryBV& bv,

               context::Context* c,

               context::UserContext* u,

               ProofNodeManager* pnm = nullptr,

               std::string name = "");

  ~BVSolverLazy();

  //--------------------------------- initialization

  /**

   * Returns true if we need an equality engine. If so, we initialize the

   * information regarding how it should be setup. For details, see the

   * documentation in Theory::needsEqualityEngine.

   */

  bool needsEqualityEngine(EeSetupInfo& esi) override;

  /** finish initialization */

  void finishInit() override;

  //--------------------------------- end initialization

  void preRegisterTerm(TNode n) override;

  bool preCheck(Theory::Effort e) override;

  bool needsCheckLastEffort() override;

  void propagate(Theory::Effort e) override;

  TrustNode explain(TNode n) override;

  bool collectModelValues(TheoryModel* m,

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

  TrustNode ppRewrite(TNode t) override;

  void ppStaticLearn(TNode in, NodeBuilder& learned) override;

  void presolve() override;

  bool applyAbstraction(const std::vector<Node>& assertions,

                        std::vector<Node>& new_assertions) override;

 private:

  class Statistics

  {

   public:

    AverageStat d_avgConflictSize;

    TimerStat d_solveTimer;

    IntStat d_numCallsToCheckFullEffort;

    IntStat d_numCallsToCheckStandardEffort;

    TimerStat d_weightComputationTimer;

    IntStat d_numMultSlice;

    Statistics();

  };

  Statistics d_statistics;

  void check(Theory::Effort e);

  void spendResource(Resource r);

  typedef std::unordered_set<TNode> TNodeSet;

  typedef std::unordered_set<Node> NodeSet;

  NodeSet d_staticLearnCache;

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

  context::CDO<bool> d_lemmasAdded;

  // Are we in conflict?

  context::CDO<bool> d_conflict;

  // Invalidate the model cache if check was called

  context::CDO<bool> d_invalidateModelCache;

  /** The conflict node */

  Node d_conflictNode;

  /** Literals to propagate */

  context::CDList<Node> d_literalsToPropagate;

  /** Index of the next literal to propagate */

  context::CDO<unsigned> d_literalsToPropagateIndex;

  /**

   * Keeps a map from nodes to the subtheory that propagated it so that we can

   * explain it properly.

   */

  typedef context::CDHashMap<Node, SubTheory> PropagatedMap;

  PropagatedMap d_propagatedBy;

  std::unique_ptr<EagerBitblastSolver> d_eagerSolver;

  std::unique_ptr<AbstractionModule> d_abstractionModule;

  bool d_calledPreregister;

  {

  }

  {

  }

  /** Should be called to propagate the literal.  */

  bool storePropagation(TNode literal, SubTheory subtheory);

  /**

   * Explains why this literal (propagated by subtheory) is true by adding

   * assumptions.

   */

  void explain(TNode literal, std::vector<TNode>& assumptions);

  void notifySharedTerm(TNode t) override;

  EqualityStatus getEqualityStatus(TNode a, TNode b) override;

  Node getModelValue(TNode var);

  {

  }

  void setConflict(Node conflict = Node::null());

  void sendConflict();

  {

  void checkForLemma(TNode node);

  friend class LazyBitblaster;

  friend class TLazyBitblaster;

  friend class EagerBitblaster;

  friend class BitblastSolver;

  friend class EqualitySolver;

  friend class CoreSolver;

  friend class InequalitySolver;

  friend class AlgebraicSolver;

  friend class EagerBitblastSolver;

}; /* class BVSolverLazy */

}  // namespace bv

}  // namespace theory

}  // namespace cvc5

#endif /* CVC5__THEORY__BV__BV_SOLVER_LAZY_H */