/*********************                                                        */
/*! \file inference_manager.cpp
 ** \verbatim
 ** Top contributors (to current version):
 **   Andrew Reynolds
 ** This file is part of the CVC4 project.
 ** Copyright (c) 2009-2019 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 Implementation of the inference manager for the theory of strings.
 **/

#include "theory/strings/inference_manager.h"

#include "expr/kind.h"
#include "options/strings_options.h"
#include "theory/rewriter.h"
#include "theory/strings/theory_strings.h"
#include "theory/strings/theory_strings_rewriter.h"
#include "theory/strings/theory_strings_utils.h"

using namespace std;
using namespace CVC4::context;
using namespace CVC4::kind;

namespace CVC4 {
namespace theory {
namespace strings {

InferenceManager::InferenceManager(TheoryStrings& p,
                                   context::Context* c,
                                   context::UserContext* u,
                                   SolverState& s,
                                   OutputChannel& out)
    : d_parent(p), d_state(s), d_out(out), d_keep(c), d_lengthLemmaTermsCache(u)
{
  NodeManager* nm = NodeManager::currentNM();
  d_zero = nm->mkConst(Rational(0));
  d_one = nm->mkConst(Rational(1));
  d_emptyString = nm->mkConst(::CVC4::String(""));
  d_true = nm->mkConst(true);
  d_false = nm->mkConst(false);
}

bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
                                             Node conc,
                                             const char* c)
{
  if (conc.getKind() == AND
      || (conc.getKind() == NOT && conc[0].getKind() == OR))
  {
    Node conj = conc.getKind() == AND ? conc : conc[0];
    bool pol = conc.getKind() == AND;
    bool ret = true;
    for (const Node& cc : conj)
    {
      bool retc = sendInternalInference(exp, pol ? cc : cc.negate(), c);
      ret = ret && retc;
    }
    return ret;
  }
  bool pol = conc.getKind() != NOT;
  Node lit = pol ? conc : conc[0];
  if (lit.getKind() == EQUAL)
  {
    for (unsigned i = 0; i < 2; i++)
    {
      if (!lit[i].isConst() && !d_state.hasTerm(lit[i]))
      {
        // introduces a new non-constant term, do not infer
        return false;
      }
    }
    // does it already hold?
    if (pol ? d_state.areEqual(lit[0], lit[1])
            : d_state.areDisequal(lit[0], lit[1]))
    {
      return true;
    }
  }
  else if (lit.isConst())
  {
    if (lit.getConst<bool>())
    {
      Assert(pol);
      // trivially holds
      return true;
    }
  }
  else if (!d_state.hasTerm(lit))
  {
    // introduces a new non-constant term, do not infer
    return false;
  }
  else if (d_state.areEqual(lit, pol ? d_true : d_false))
  {
    // already holds
    return true;
  }
  sendInference(exp, conc, c);
  return true;
}

void InferenceManager::sendInference(const std::vector<Node>& exp,
                                     const std::vector<Node>& exp_n,
                                     Node eq,
                                     const char* c,
                                     bool asLemma)
{
  eq = eq.isNull() ? d_false : Rewriter::rewrite(eq);
  if (Trace.isOn("strings-infer-debug"))
  {
    Trace("strings-infer-debug")
        << "By " << c << ", infer : " << eq << " from: " << std::endl;
    for (unsigned i = 0; i < exp.size(); i++)
    {
      Trace("strings-infer-debug") << "  " << exp[i] << std::endl;
    }
    for (unsigned i = 0; i < exp_n.size(); i++)
    {
      Trace("strings-infer-debug") << "  N:" << exp_n[i] << std::endl;
    }
  }
  if (eq == d_true)
  {
    return;
  }
  Node atom = eq.getKind() == NOT ? eq[0] : eq;
  // check if we should send a lemma or an inference
  if (asLemma || atom == d_false || atom.getKind() == OR || !exp_n.empty()
      || options::stringInferAsLemmas())
  {
    Node eq_exp;
    if (options::stringRExplainLemmas())
    {
      eq_exp = mkExplain(exp, exp_n);
    }
    else
    {
      if (exp.empty())
      {
        eq_exp = utils::mkAnd(exp_n);
      }
      else if (exp_n.empty())
      {
        eq_exp = utils::mkAnd(exp);
      }
      else
      {
        std::vector<Node> ev;
        ev.insert(ev.end(), exp.begin(), exp.end());
        ev.insert(ev.end(), exp_n.begin(), exp_n.end());
        eq_exp = NodeManager::currentNM()->mkNode(AND, ev);
      }
    }
    // if we have unexplained literals, this lemma is not a conflict
    if (eq == d_false && !exp_n.empty())
    {
      eq = eq_exp.negate();
      eq_exp = d_true;
    }
    sendLemma(eq_exp, eq, c);
  }
  else
  {
    sendInfer(utils::mkAnd(exp), eq, c);
  }
}

void InferenceManager::sendInference(const std::vector<Node>& exp,
                                     Node eq,
                                     const char* c,
                                     bool asLemma)
{
  std::vector<Node> exp_n;
  sendInference(exp, exp_n, eq, c, asLemma);
}

void InferenceManager::sendInference(const InferInfo& i)
{
  std::stringstream ssi;
  ssi << i.d_id;
  sendInference(i.d_ant, i.d_antn, i.d_conc, ssi.str().c_str(), true);
}

void InferenceManager::sendLemma(Node ant, Node conc, const char* c)
{
  if (conc.isNull() || conc == d_false)
  {
    Trace("strings-conflict")
        << "Strings::Conflict : " << c << " : " << ant << std::endl;
    Trace("strings-lemma") << "Strings::Conflict : " << c << " : " << ant
                           << std::endl;
    Trace("strings-assert")
        << "(assert (not " << ant << ")) ; conflict " << c << std::endl;
    d_out.conflict(ant);
    d_state.setConflict();
    return;
  }
  Node lem;
  if (ant == d_true)
  {
    lem = conc;
  }
  else
  {
    lem = NodeManager::currentNM()->mkNode(IMPLIES, ant, conc);
  }
  Trace("strings-lemma") << "Strings::Lemma " << c << " : " << lem << std::endl;
  Trace("strings-assert") << "(assert " << lem << ") ; lemma " << c
                          << std::endl;
  d_pendingLem.push_back(lem);
}

void InferenceManager::sendInfer(Node eq_exp, Node eq, const char* c)
{
  if (options::stringInferSym())
  {
    std::vector<Node> vars;
    std::vector<Node> subs;
    std::vector<Node> unproc;
    inferSubstitutionProxyVars(eq_exp, vars, subs, unproc);
    if (unproc.empty())
    {
      Node eqs =
          eq.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
      if (Trace.isOn("strings-lemma-debug"))
      {
        Trace("strings-lemma-debug") << "Strings::Infer " << eq << " from "
                                     << eq_exp << " by " << c << std::endl;
        Trace("strings-lemma-debug")
            << "Strings::Infer Alternate : " << eqs << std::endl;
        for (unsigned i = 0, nvars = vars.size(); i < nvars; i++)
        {
          Trace("strings-lemma-debug")
              << "  " << vars[i] << " -> " << subs[i] << std::endl;
        }
      }
      sendLemma(d_true, eqs, c);
      return;
    }
    if (Trace.isOn("strings-lemma-debug"))
    {
      for (const Node& u : unproc)
      {
        Trace("strings-lemma-debug")
            << "  non-trivial exp : " << u << std::endl;
      }
    }
  }
  Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eq_exp
                         << " by " << c << std::endl;
  Trace("strings-assert") << "(assert (=> " << eq_exp << " " << eq
                          << ")) ; infer " << c << std::endl;
  d_pending.push_back(eq);
  d_pendingExp[eq] = eq_exp;
  d_keep.insert(eq);
  d_keep.insert(eq_exp);
}

bool InferenceManager::sendSplit(Node a, Node b, const char* c, bool preq)
{
  Node eq = a.eqNode(b);
  eq = Rewriter::rewrite(eq);
  if (eq.isConst())
  {
    return false;
  }
  NodeManager* nm = NodeManager::currentNM();
  Node lemma_or = nm->mkNode(OR, eq, nm->mkNode(NOT, eq));
  Trace("strings-lemma") << "Strings::Lemma " << c << " SPLIT : " << lemma_or
                         << std::endl;
  d_pendingLem.push_back(lemma_or);
  sendPhaseRequirement(eq, preq);
  return true;
}

void InferenceManager::sendPhaseRequirement(Node lit, bool pol)
{
  lit = Rewriter::rewrite(lit);
  d_pendingReqPhase[lit] = pol;
}

void InferenceManager::registerLength(Node n, LengthStatus s)
{
  if (d_lengthLemmaTermsCache.find(n) != d_lengthLemmaTermsCache.end())
  {
    return;
  }
  d_lengthLemmaTermsCache.insert(n);

  if (s == LENGTH_IGNORE)
  {
    // ignore it
    return;
  }

  NodeManager* nm = NodeManager::currentNM();
  Node n_len = nm->mkNode(kind::STRING_LENGTH, n);

  if (s == LENGTH_GEQ_ONE)
  {
    Node neq_empty = n.eqNode(d_emptyString).negate();
    Node len_n_gt_z = nm->mkNode(GT, n_len, d_zero);
    Node len_geq_one = nm->mkNode(AND, neq_empty, len_n_gt_z);
    Trace("strings-lemma") << "Strings::Lemma SK-GEQ-ONE : " << len_geq_one
                           << std::endl;
    Trace("strings-assert") << "(assert " << len_geq_one << ")" << std::endl;
    d_out.lemma(len_geq_one);
    return;
  }

  if (s == LENGTH_ONE)
  {
    Node len_one = n_len.eqNode(d_one);
    Trace("strings-lemma") << "Strings::Lemma SK-ONE : " << len_one
                           << std::endl;
    Trace("strings-assert") << "(assert " << len_one << ")" << std::endl;
    d_out.lemma(len_one);
    return;
  }
  Assert(s == LENGTH_SPLIT);

  if (options::stringSplitEmp() || !options::stringLenGeqZ())
  {
    Node n_len_eq_z = n_len.eqNode(d_zero);
    Node n_len_eq_z_2 = n.eqNode(d_emptyString);
    Node case_empty = nm->mkNode(AND, n_len_eq_z, n_len_eq_z_2);
    case_empty = Rewriter::rewrite(case_empty);
    Node case_nempty = nm->mkNode(GT, n_len, d_zero);
    if (!case_empty.isConst())
    {
      Node lem = nm->mkNode(OR, case_empty, case_nempty);
      d_out.lemma(lem);
      Trace("strings-lemma")
          << "Strings::Lemma LENGTH >= 0 : " << lem << std::endl;
      // prefer trying the empty case first
      // notice that requirePhase must only be called on rewritten literals that
      // occur in the CNF stream.
      n_len_eq_z = Rewriter::rewrite(n_len_eq_z);
      Assert(!n_len_eq_z.isConst());
      d_out.requirePhase(n_len_eq_z, true);
      n_len_eq_z_2 = Rewriter::rewrite(n_len_eq_z_2);
      Assert(!n_len_eq_z_2.isConst());
      d_out.requirePhase(n_len_eq_z_2, true);
    }
    else if (!case_empty.getConst<bool>())
    {
      // the rewriter knows that n is non-empty
      Trace("strings-lemma")
          << "Strings::Lemma LENGTH > 0 (non-empty): " << case_nempty
          << std::endl;
      d_out.lemma(case_nempty);
    }
    else
    {
      // If n = "" ---> true or len( n ) = 0 ----> true, then we expect that
      // n ---> "". Since this method is only called on non-constants n, it must
      // be that n = "" ^ len( n ) = 0 does not rewrite to true.
      Assert(false);
    }
  }

  // additionally add len( x ) >= 0 ?
  if (options::stringLenGeqZ())
  {
    Node n_len_geq = nm->mkNode(kind::GEQ, n_len, d_zero);
    n_len_geq = Rewriter::rewrite(n_len_geq);
    d_out.lemma(n_len_geq);
  }
}

void InferenceManager::addToExplanation(Node a,
                                        Node b,
                                        std::vector<Node>& exp) const
{
  if (a != b)
  {
    Debug("strings-explain")
        << "Add to explanation : " << a << " == " << b << std::endl;
    Assert(d_state.areEqual(a, b));
    exp.push_back(a.eqNode(b));
  }
}

void InferenceManager::addToExplanation(Node lit, std::vector<Node>& exp) const
{
  if (!lit.isNull())
  {
    exp.push_back(lit);
  }
}

void InferenceManager::doPendingFacts()
{
  size_t i = 0;
  while (!d_state.isInConflict() && i < d_pending.size())
  {
    Node fact = d_pending[i];
    Node exp = d_pendingExp[fact];
    if (fact.getKind() == AND)
    {
      for (const Node& lit : fact)
      {
        bool polarity = lit.getKind() != NOT;
        TNode atom = polarity ? lit : lit[0];
        d_parent.assertPendingFact(atom, polarity, exp);
      }
    }
    else
    {
      bool polarity = fact.getKind() != NOT;
      TNode atom = polarity ? fact : fact[0];
      d_parent.assertPendingFact(atom, polarity, exp);
    }
    i++;
  }
  d_pending.clear();
  d_pendingExp.clear();
}

void InferenceManager::doPendingLemmas()
{
  if (!d_state.isInConflict())
  {
    for (const Node& lc : d_pendingLem)
    {
      Trace("strings-pending") << "Process pending lemma : " << lc << std::endl;
      d_out.lemma(lc);
    }
    for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)
    {
      Trace("strings-pending") << "Require phase : " << prp.first
                               << ", polarity = " << prp.second << std::endl;
      d_out.requirePhase(prp.first, prp.second);
    }
  }
  d_pendingLem.clear();
  d_pendingReqPhase.clear();
}

bool InferenceManager::hasProcessed() const
{
  return d_state.isInConflict() || !d_pendingLem.empty() || !d_pending.empty();
}

void InferenceManager::inferSubstitutionProxyVars(
    Node n,
    std::vector<Node>& vars,
    std::vector<Node>& subs,
    std::vector<Node>& unproc) const
{
  if (n.getKind() == AND)
  {
    for (const Node& nc : n)
    {
      inferSubstitutionProxyVars(nc, vars, subs, unproc);
    }
    return;
  }
  if (n.getKind() == EQUAL)
  {
    Node ns = n.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
    ns = Rewriter::rewrite(ns);
    if (ns.getKind() == EQUAL)
    {
      Node s;
      Node v;
      for (unsigned i = 0; i < 2; i++)
      {
        Node ss;
        // determine whether this side has a proxy variable
        if (ns[i].getAttribute(StringsProxyVarAttribute()))
        {
          // it is a proxy variable
          ss = ns[i];
        }
        else if (ns[i].isConst())
        {
          ss = d_parent.getProxyVariableFor(ns[i]);
        }
        if (!ss.isNull())
        {
          v = ns[1 - i];
          // if the other side is a constant or variable
          if (v.getNumChildren() == 0)
          {
            if (s.isNull())
            {
              s = ss;
            }
            else
            {
              // both sides of the equality correspond to a proxy variable
              if (ss == s)
              {
                // it is a trivial equality, e.g. between a proxy variable
                // and its definition
                return;
              }
              else
              {
                // equality between proxy variables, non-trivial
                s = Node::null();
              }
            }
          }
        }
      }
      if (!s.isNull())
      {
        // the equality can be turned into a substitution
        subs.push_back(s);
        vars.push_back(v);
        return;
      }
    }
    else
    {
      n = ns;
    }
  }
  if (n != d_true)
  {
    unproc.push_back(n);
  }
}

Node InferenceManager::mkExplain(const std::vector<Node>& a) const
{
  std::vector<Node> an;
  return mkExplain(a, an);
}

Node InferenceManager::mkExplain(const std::vector<Node>& a,
                                 const std::vector<Node>& an) const
{
  std::vector<TNode> antec_exp;
  // copy to processing vector
  std::vector<Node> aconj;
  for (const Node& ac : a)
  {
    utils::flattenOp(AND, ac, aconj);
  }
  eq::EqualityEngine* ee = d_state.getEqualityEngine();
  for (const Node& apc : aconj)
  {
    Assert(apc.getKind() != AND);
    Debug("strings-explain") << "Add to explanation " << apc << std::endl;
    if (apc.getKind() == NOT && apc[0].getKind() == EQUAL)
    {
      Assert(ee->hasTerm(apc[0][0]));
      Assert(ee->hasTerm(apc[0][1]));
      // ensure that we are ready to explain the disequality
      AlwaysAssert(ee->areDisequal(apc[0][0], apc[0][1], true));
    }
    Assert(apc.getKind() != EQUAL || ee->areEqual(apc[0], apc[1]));
    // now, explain
    explain(apc, antec_exp);
  }
  for (const Node& anc : an)
  {
    if (std::find(antec_exp.begin(), antec_exp.end(), anc) == antec_exp.end())
    {
      Debug("strings-explain")
          << "Add to explanation (new literal) " << anc << std::endl;
      antec_exp.push_back(anc);
    }
  }
  Node ant;
  if (antec_exp.empty())
  {
    ant = d_true;
  }
  else if (antec_exp.size() == 1)
  {
    ant = antec_exp[0];
  }
  else
  {
    ant = NodeManager::currentNM()->mkNode(kind::AND, antec_exp);
  }
  return ant;
}

void InferenceManager::explain(TNode literal,
                               std::vector<TNode>& assumptions) const
{
  Debug("strings-explain") << "Explain " << literal << " "
                           << d_state.isInConflict() << std::endl;
  eq::EqualityEngine* ee = d_state.getEqualityEngine();
  bool polarity = literal.getKind() != NOT;
  TNode atom = polarity ? literal : literal[0];
  std::vector<TNode> tassumptions;
  if (atom.getKind() == EQUAL)
  {
    if (atom[0] != atom[1])
    {
      Assert(ee->hasTerm(atom[0]));
      Assert(ee->hasTerm(atom[1]));
      ee->explainEquality(atom[0], atom[1], polarity, tassumptions);
    }
  }
  else
  {
    ee->explainPredicate(atom, polarity, tassumptions);
  }
  for (const TNode a : tassumptions)
  {
    if (std::find(assumptions.begin(), assumptions.end(), a)
        == assumptions.end())
    {
      assumptions.push_back(a);
    }
  }
  if (Debug.isOn("strings-explain-debug"))
  {
    Debug("strings-explain-debug")
        << "Explanation for " << literal << " was " << std::endl;
    for (const TNode a : tassumptions)
    {
      Debug("strings-explain-debug") << "   " << a << std::endl;
    }
  }
}

}  // namespace strings
}  // namespace theory
}  // namespace CVC4