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

 * Top contributors (to current version):

 *   Andrew Reynolds, Tim King, Haniel Barbosa

 *

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

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

 *

 * Theory of separation logic.

 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__SEP__THEORY_SEP_H

#define CVC5__THEORY__SEP__THEORY_SEP_H

#include "context/cdhashmap.h"

#include "context/cdhashset.h"

#include "context/cdlist.h"

#include "context/cdqueue.h"

#include "theory/decision_strategy.h"

#include "theory/inference_manager_buffered.h"

#include "theory/sep/theory_sep_rewriter.h"

#include "theory/theory.h"

#include "theory/theory_state.h"

#include "theory/uf/equality_engine.h"

#include "util/statistics_stats.h"

namespace cvc5 {

namespace theory {

class TheoryModel;

namespace sep {

class TheorySep : public Theory {

  typedef context::CDList<Node> NodeList;

  typedef context::CDHashSet<Node> NodeSet;

  typedef context::CDHashMap<Node, Node> NodeNodeMap;

  /////////////////////////////////////////////////////////////////////////////

  // MISC

  /////////////////////////////////////////////////////////////////////////////

 private:

  /** all lemmas sent */

  NodeSet d_lemmas_produced_c;

  /** True node for predicates = true */

  Node d_true;

  /** True node for predicates = false */

  Node d_false;

  //whether bounds have been initialized

  bool d_bounds_init;

  TheorySepRewriter d_rewriter;

  /** A (default) theory state object */

  TheoryState d_state;

  /** A buffered inference manager */

  InferenceManagerBuffered d_im;

  Node mkAnd( std::vector< TNode >& assumptions );

  int processAssertion(

      Node n,

      std::map<int, std::map<Node, int> >& visited,

      std::map<int, std::map<Node, std::vector<Node> > >& references,

      std::map<int, std::map<Node, bool> >& references_strict,

      bool pol,

      bool hasPol,

      bool underSpatial);

 public:

  TheorySep(Env& env, OutputChannel& out, Valuation valuation);

  ~TheorySep();

  /**

   * Declare heap. For smt2 inputs, this is called when the command

   * (declare-heap (locT datat)) is invoked by the user. This sets locT as the

   * location type and dataT is the data type for the heap. This command can be

   * executed once only, and must be invoked before solving separation logic

   * inputs.

   */

  void declareSepHeap(TypeNode locT, TypeNode dataT) override;

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

  /** get the official theory rewriter of this theory */

  TheoryRewriter* getTheoryRewriter() override;

  /** get the proof checker of this theory */

  ProofRuleChecker* getProofChecker() override;

  /**

   * 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

  /** preregister term */

  void preRegisterTerm(TNode n) override;

  /////////////////////////////////////////////////////////////////////////////

  // PREPROCESSING

  /////////////////////////////////////////////////////////////////////////////

 public:

  void ppNotifyAssertions(const std::vector<Node>& assertions) override;

  /////////////////////////////////////////////////////////////////////////////

  // T-PROPAGATION / REGISTRATION

  /////////////////////////////////////////////////////////////////////////////

 private:

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

  bool propagateLit(TNode literal);

  /** Conflict when merging constants */

  void conflict(TNode a, TNode b);

 public:

  TrustNode explain(TNode n) override;

 public:

  void computeCareGraph() override;

  /////////////////////////////////////////////////////////////////////////////

  // MODEL GENERATION

  /////////////////////////////////////////////////////////////////////////////

 public:

  void postProcessModel(TheoryModel* m) override;

  /////////////////////////////////////////////////////////////////////////////

  // NOTIFICATIONS

  /////////////////////////////////////////////////////////////////////////////

 public:

  void presolve() override;

  /////////////////////////////////////////////////////////////////////////////

  // MAIN SOLVER

  /////////////////////////////////////////////////////////////////////////////

  //--------------------------------- standard check

  /** Do we need a check call at last call effort? */

  bool needsCheckLastEffort() override;

  /** Post-check, called after the fact queue of the theory is processed. */

  void postCheck(Effort level) override;

  /** Pre-notify fact, return true if processed. */

  bool preNotifyFact(TNode atom,

                     bool pol,

                     TNode fact,

                     bool isPrereg,

                     bool isInternal) override;

  /** Notify fact */

  void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;

  //--------------------------------- end standard check

 private:

  /** Ensures that the reduction has been added for the given fact */

  void reduceFact(TNode atom, bool polarity, TNode fact);

  /** Is spatial kind? */

  bool isSpatialKind(Kind k) const;

  // NotifyClass: template helper class for d_equalityEngine - handles

  // call-back from congruence closure module

  {

    TheorySep& d_sep;

   public:

    {

      // Just forward to sep

      {

      }

    }

                                     TNode t1,

                                     TNode t2,

                                     bool value) override

    {

      {

        // Propagate equality between shared terms

      }

    }

    {

    {

  };

  /** The notify class for d_equalityEngine */

  NotifyClass d_notify;

  /** list of all refinement lemms */

  std::map< Node, std::map< Node, std::vector< Node > > > d_refinement_lem;

  //cache for positive polarity start reduction

  NodeSet d_reduce;

  std::map< Node, std::map< Node, Node > > d_red_conc;

  std::map< Node, std::map< Node, Node > > d_neg_guard;

  std::vector< Node > d_neg_guards;

  /** a (singleton) decision strategy for each negative guard. */

  std::map<Node, std::unique_ptr<DecisionStrategySingleton> >

      d_neg_guard_strategy;

  std::map< Node, Node > d_guard_to_assertion;

  NodeList d_spatial_assertions;

  //data,ref type (globally fixed)

  TypeNode d_type_ref;

  TypeNode d_type_data;

  //currently fix one data type for each location type, throw error if using more than one

  std::map< TypeNode, TypeNode > d_loc_to_data_type;

  //information about types

  std::map< TypeNode, Node > d_base_label;

  std::map< TypeNode, Node > d_nil_ref;

  //reference bound

  std::map< TypeNode, Node > d_reference_bound;

  std::map< TypeNode, Node > d_reference_bound_max;

  std::map< TypeNode, std::vector< Node > > d_type_references;

  //kind of bound for reference types

  enum {

    bound_strict,

    bound_default,

    bound_invalid,

  };

  std::map< TypeNode, unsigned > d_bound_kind;

  std::map< TypeNode, std::vector< Node > > d_type_references_card;

  std::map< Node, unsigned > d_type_ref_card_id;

  std::map< TypeNode, std::vector< Node > > d_type_references_all;

  std::map< TypeNode, unsigned > d_card_max;

  //for empty argument

  std::map< TypeNode, Node > d_emp_arg;

  //map from ( atom, label, child index ) -> label

  std::map< Node, std::map< Node, std::map< int, Node > > > d_label_map;

  std::map< Node, Node > d_label_map_parent;

  //term model

  std::map< Node, Node > d_tmodel;

  std::map< Node, Node > d_pto_model;

  class HeapAssertInfo {

  public:

    HeapAssertInfo( context::Context* c );

    context::CDO< Node > d_pto;

    context::CDO< bool > d_has_neg_pto;

  };

  std::map< Node, HeapAssertInfo * > d_eqc_info;

  HeapAssertInfo * getOrMakeEqcInfo( Node n, bool doMake = false );

  //get global reference/data type

  TypeNode getReferenceType( Node n );

  TypeNode getDataType( Node n );

  /**

   * Register reference data types for atom. Calls the method below for

   * the appropriate types.

   */

  void registerRefDataTypesAtom(Node atom);

  /**

   * This is called either when:

   * (A) a declare-heap command is issued with tn1/tn2, and atom is null, or

   * (B) an atom specifying the heap type tn1/tn2 is registered to this theory.

   * We set the heap type if we are are case (A), and check whether the

   * heap type is consistent in the case of (B).

   */

  void registerRefDataTypes(TypeNode tn1, TypeNode tn2, Node atom);

  //get location/data type

  //get the base label for the spatial assertion

  Node getBaseLabel( TypeNode tn );

  Node getNilRef( TypeNode tn );

  void setNilRef( TypeNode tn, Node n );

  Node getLabel( Node atom, int child, Node lbl );

  Node applyLabel( Node n, Node lbl, std::map< Node, Node >& visited );

  void getLabelChildren( Node atom, Node lbl, std::vector< Node >& children, std::vector< Node >& labels );

  public:

    //information about the model

    bool d_computed;

    std::vector< Node > d_heap_locs;

    std::vector< Node > d_heap_locs_model;

    //get value

    Node getValue( TypeNode tn );

  };

  //heap info ( label -> HeapInfo )

  std::map< Node, HeapInfo > d_label_model;

  // loc -> { data_1, ..., data_n } where (not (pto loc data_1))...(not (pto loc data_n))).

  std::map< Node, std::vector< Node > > d_heap_locs_nptos;

  void debugPrintHeap( HeapInfo& heap, const char * c );

  void validatePto( HeapAssertInfo * ei, Node ei_n );

  void addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity );

  void mergePto( Node p1, Node p2 );

  void computeLabelModel( Node lbl );

  Node instantiateLabel(Node n,

                        Node o_lbl,

                        Node lbl,

                        Node lbl_v,

                        std::map<Node, Node>& visited,

                        std::map<Node, Node>& pto_model,

                        TypeNode rtn,

                        std::map<Node, bool>& active_lbl,

                        unsigned ind = 0);

  void setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active );

  Node mkUnion( TypeNode tn, std::vector< Node >& locs );

 private:

  Node getRepresentative( Node t );

  bool hasTerm( Node a );

  bool areEqual( Node a, Node b );

  bool areDisequal( Node a, Node b );

  void eqNotifyMerge(TNode t1, TNode t2);

  void sendLemma( std::vector< Node >& ant, Node conc, InferenceId id, bool infer = false );

  void doPending();

 public:

  void initializeBounds();

};/* class TheorySep */

}  // namespace sep

}  // namespace theory

}  // namespace cvc5

#endif /* CVC5__THEORY__SEP__THEORY_SEP_H */