/*********************                                                        */
/*! \file nonlinear_extension.h
 ** \verbatim
 ** Top contributors (to current version):
 **   Tim King
 ** This file is part of the CVC4 project.
 ** Copyright (c) 2009-2017 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.\endverbatim
 **
 ** \brief Extensions for incomplete handling of nonlinear multiplication.
 **
 ** Extensions to the theory of arithmetic incomplete handling of nonlinear
 ** multiplication via axiom instantiations.
 **/

#ifndef __CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H
#define __CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H

#include <stdint.h>

#include <map>
#include <queue>
#include <set>
#include <utility>
#include <vector>

#include "context/cdhashset.h"
#include "context/cdinsert_hashmap.h"
#include "context/cdlist.h"
#include "context/cdqueue.h"
#include "context/context.h"
#include "expr/kind.h"
#include "expr/node.h"
#include "theory/arith/theory_arith.h"
#include "theory/uf/equality_engine.h"

namespace CVC4 {
namespace theory {
namespace arith {

typedef std::map<Node, unsigned> NodeMultiset;

class NonlinearExtension {
 public:
  NonlinearExtension(TheoryArith& containing, eq::EqualityEngine* ee);
  ~NonlinearExtension();
  bool getCurrentSubstitution(int effort, const std::vector<Node>& vars,
                              std::vector<Node>& subs,
                              std::map<Node, std::vector<Node> >& exp);

  std::pair<bool, Node> isExtfReduced(int effort, Node n, Node on,
                                      const std::vector<Node>& exp) const;
  void check(Theory::Effort e);
  bool needsCheckLastEffort() const { return d_needsLastCall; }
  int compare(Node i, Node j, unsigned orderType) const;
  int compare_value(Node i, Node j, unsigned orderType) const;

  bool isMonomialSubset(Node a, Node b) const;
  void registerMonomialSubset(Node a, Node b);

 private:
  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;

  // monomial information (context-independent)
  class MonomialIndex {
   public:
    // status 0 : n equal, -1 : n superset, 1 : n subset
    void addTerm(Node n, const std::vector<Node>& reps, NonlinearExtension* nla,
                 int status = 0, unsigned argIndex = 0);

   private:
    std::map<Node, MonomialIndex> d_data;
    std::vector<Node> d_monos;
  }; /* class MonomialIndex */

  // constraint information (context-independent)
  struct ConstraintInfo {
   public:
    Node d_rhs;
    Node d_coeff;
    Kind d_type;
  }; /* struct ConstraintInfo */

  // Check assertions for consistency in the effort LAST_CALL with a subset of
  // the assertions, false_asserts, evaluate to false in the current model.
  void checkLastCall(const std::vector<Node>& assertions,
                     const std::set<Node>& false_asserts,
                     const std::vector<Node>& xts);

  static bool isArithKind(Kind k);
  static Node mkLit(Node a, Node b, int status, int orderType = 0);
  static Node mkAbs(Node a);
  static Node mkValidPhase(Node a, Node pi);
  static Node mkBounded( Node l, Node a, Node u );
  static Kind joinKinds(Kind k1, Kind k2);
  static Kind transKinds(Kind k1, Kind k2);
  static bool isTranscendentalKind(Kind k);
  Node mkMonomialRemFactor(Node n, const NodeMultiset& n_exp_rem) const;

  // register monomial
  void registerMonomial(Node n);
  void setMonomialFactor(Node a, Node b, const NodeMultiset& common);

  void registerConstraint(Node atom);
  // index = 0 : concrete, 1 : abstract
  Node computeModelValue(Node n, unsigned index = 0);

  Node get_compare_value(Node i, unsigned orderType) const;
  void assignOrderIds(std::vector<Node>& vars, NodeMultiset& d_order,
                      unsigned orderType);

  // Returns the subset of assertions that evaluate to false in the model.
  std::set<Node> getFalseInModel(const std::vector<Node>& assertions);

  // status
  // 0 : equal
  // 1 : greater than or equal
  // 2 : greater than
  // -X : (less)
  // in these functions we are iterating over variables of monomials
  // initially : exp => ( oa = a ^ ob = b )
  int compareSign(Node oa, Node a, unsigned a_index, int status,
                  std::vector<Node>& exp, std::vector<Node>& lem);
  bool compareMonomial(
      Node oa, Node a, NodeMultiset& a_exp_proc, Node ob, Node b,
      NodeMultiset& b_exp_proc, std::vector<Node>& exp, std::vector<Node>& lem,
      std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers);
  bool compareMonomial(
      Node oa, Node a, unsigned a_index, NodeMultiset& a_exp_proc, Node ob,
      Node b, unsigned b_index, NodeMultiset& b_exp_proc, int status,
      std::vector<Node>& exp, std::vector<Node>& lem,
      std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers);
  bool cmp_holds(Node x, Node y,
                 std::map<Node, std::map<Node, Node> >& cmp_infers,
                 std::vector<Node>& exp, std::map<Node, bool>& visited);

  bool isEntailed(Node n, bool pol);

  // Potentially sends lem on the output channel if lem has not been sent on the
  // output channel in this context. Returns the number of lemmas sent on the
  // output channel.
  int flushLemma(Node lem);

  // Potentially sends lemmas to the output channel and clears lemmas. Returns
  // the number of lemmas sent to the output channel.
  int flushLemmas(std::vector<Node>& lemmas);

  // Returns the NodeMultiset for an existing monomial.
  const NodeMultiset& getMonomialExponentMap(Node monomial) const;

  // Map from monomials to var^index.
  typedef std::map<Node, NodeMultiset> MonomialExponentMap;
  MonomialExponentMap d_m_exp;

  std::map<Node, std::vector<Node> > d_m_vlist;
  NodeMultiset d_m_degree;
  // monomial index, by sorted variables
  MonomialIndex d_m_index;
  // list of all monomials
  std::vector<Node> d_monomials;
  // containment ordering
  std::map<Node, std::vector<Node> > d_m_contain_children;
  std::map<Node, std::vector<Node> > d_m_contain_parent;
  std::map<Node, std::map<Node, Node> > d_m_contain_mult;
  std::map<Node, std::map<Node, Node> > d_m_contain_umult;
  // ( x*y, x*z, y ) for each pair of monomials ( x*y, x*z ) with common factors
  std::map<Node, std::map<Node, Node> > d_mono_diff;

  // cache of all lemmas sent
  NodeSet d_lemmas;
  NodeSet d_zero_split;
  
  // literals with Skolems (need not be satisfied by model)
  NodeSet d_skolem_atoms;

  // utilities
  Node d_zero;
  Node d_one;
  Node d_neg_one;
  Node d_true;
  Node d_false;

  // The theory of arithmetic containing this extension.
  TheoryArith& d_containing;

  // pointer to used equality engine
  eq::EqualityEngine* d_ee;
  // needs last call effort
  bool d_needsLastCall;

  // if d_c_info[lit][x] = ( r, coeff, k ), then ( lit <=>  (coeff * x) <k> r )
  std::map<Node, std::map<Node, ConstraintInfo> > d_c_info;
  std::map<Node, std::map<Node, bool> > d_c_info_maxm;
  std::vector<Node> d_constraints;

  // model values/orderings
  // model values
  std::map<Node, Node> d_mv[2];

  // ordering, stores variables and 0,1,-1
  std::map<Node, unsigned> d_order_vars;
  std::vector<Node> d_order_points;
  
  //transcendent functions
  std::map<Node, Node> d_trig_base;
  std::map<Node, bool> d_trig_is_base;
  std::map< Node, bool > d_tf_initial_refine;
  Node d_pi;
  Node d_pi_2;
  Node d_pi_neg_2;
  Node d_pi_neg;
  Node d_pi_bound[2];
  
  void mkPi();
  void getCurrentPiBounds( std::vector< Node >& lemmas );
private:
  //per last-call effort check
  
  //information about monomials
  std::vector< Node > d_ms;
  std::vector< Node > d_ms_vars;
  std::map<Node, bool> d_ms_proc;
  std::vector<Node> d_mterms;  
  //list of monomials with factors whose model value is non-constant in model 
  //  e.g. y*cos( x )
  std::map<Node, bool> d_m_nconst_factor;
  // If ( m, p1, true ), then it would help satisfiability if m were ( >
  // if p1=true, < if p1=false )
  std::map<Node, std::map<bool, bool> > d_tplane_refine_dir;
  // term -> coeff -> rhs -> ( status, exp, b ),
  //   where we have that : exp =>  ( coeff * term <status> rhs )
  //   b is true if degree( term ) >= degree( rhs )
  std::map<Node, std::map<Node, std::map<Node, Kind> > > d_ci;
  std::map<Node, std::map<Node, std::map<Node, Node> > > d_ci_exp;
  std::map<Node, std::map<Node, std::map<Node, bool> > > d_ci_max;
  
  //information about transcendental functions
  std::map< Kind, std::map< Node, Node > > d_tf_rep_map;  
  
  // factor skolems
  std::map< Node, Node > d_factor_skolem;
  Node getFactorSkolem( Node n, std::vector< Node >& lemmas );
  
  Node getTaylor( Node tf, Node x, unsigned n, std::vector< Node >& lemmas );
private:
  // Returns a vector containing a split on whether each term is 0 or not for
  // those terms that have not been split on in the current context.
  std::vector<Node> checkSplitZero();
  
  std::vector<Node> checkMonomialSign();
  
  std::vector<Node> checkMonomialMagnitude( unsigned c );
  
  std::vector<Node> checkMonomialInferBounds( std::vector<Node>& nt_lemmas,
                                              const std::set<Node>& false_asserts );
  
  std::vector<Node> checkFactoring( const std::set<Node>& false_asserts );
  
  std::vector<Node> checkMonomialInferResBounds();
  
  std::vector<Node> checkTangentPlanes();
  
  std::vector<Node> checkTranscendentalInitialRefine();

  std::vector<Node> checkTranscendentalMonotonic();
}; /* class NonlinearExtension */

}  // namespace arith
}  // namespace theory
}  // namespace CVC4

#endif /* __CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */