path: root/src/theory/strings/inference_manager.h

/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Andres Noetzli, Gereon Kremer
 *
 * 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.
 * ****************************************************************************
 *
 * Customized inference manager for the theory of strings.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__STRINGS__INFERENCE_MANAGER_H
#define CVC5__THEORY__STRINGS__INFERENCE_MANAGER_H

#include <map>
#include <vector>

#include "context/cdhashset.h"
#include "context/context.h"
#include "expr/node.h"
#include "proof/proof_node_manager.h"
#include "theory/ext_theory.h"
#include "theory/inference_manager_buffered.h"
#include "theory/output_channel.h"
#include "theory/strings/infer_info.h"
#include "theory/strings/infer_proof_cons.h"
#include "theory/strings/sequences_stats.h"
#include "theory/strings/solver_state.h"
#include "theory/strings/term_registry.h"
#include "theory/theory_inference_manager.h"
#include "theory/uf/equality_engine.h"

namespace cvc5 {
namespace theory {
namespace strings {

/** Inference Manager
 *
 * The purpose of this class is to process inference steps for strategies
 * in the theory of strings.
 *
 * In particular, inferences are given to this class via calls to functions:
 *
 * sendInternalInference, sendInference, sendSplit
 *
 * This class decides how the conclusion of these calls will be processed.
 * It primarily has to decide whether the conclusions will be processed:
 *
 * (1) Internally in the strings solver, via calls to equality engine's
 * assertLiteral and assertPredicate commands. We refer to these literals as
 * "facts",
 * (2) Externally on the output channel of theory of strings as "lemmas",
 * (3) External on the output channel as "conflicts" (when a conclusion of an
 * inference is false).
 *
 * It buffers facts and lemmas in vectors d_pending and d_pending_lem
 * respectively.
 *
 * When applicable, facts can be flushed to the equality engine via a call to
 * doPendingFacts, and lemmas can be flushed to the output channel via a call
 * to doPendingLemmas.
 *
 * It also manages other kinds of interaction with the output channel of the
 * theory of strings, e.g. sendPhaseRequirement, setIncomplete, and
 * with the extended theory object e.g. markCongruent.
 */
class InferenceManager : public InferenceManagerBuffered
{
  typedef context::CDHashSet<Node> NodeSet;
  typedef context::CDHashMap<Node, Node> NodeNodeMap;
  friend class InferInfo;

 public:
  InferenceManager(Theory& t,
                   SolverState& s,
                   TermRegistry& tr,
                   ExtTheory& e,
                   SequencesStatistics& statistics,
                   ProofNodeManager* pnm);
  ~InferenceManager() {}

  /**
   * Do pending method. This processes all pending facts, lemmas and pending
   * phase requests based on the policy of this manager. This means that
   * we process the pending facts first and abort if in conflict. Otherwise, we
   * process the pending lemmas and then the pending phase requirements.
   * Notice that we process the pending lemmas even if there were facts.
   */
  void doPending();

  /** send internal inferences
   *
   * This is called when we have inferred exp => conc, where exp is a set
   * of equalities and disequalities that hold in the current equality engine.
   * This method adds equalities and disequalities ~( s = t ) via
   * sendInference such that both s and t are either constants or terms
   * that already occur in the equality engine, and ~( s = t ) is a consequence
   * of conc. This function can be seen as a "conservative" version of
   * sendInference below in that it does not introduce any new non-constant
   * terms to the state.
   *
   * The argument infer identifies the reason for the inference.
   * This is used for debugging and statistics purposes.
   *
   * Return true if the inference is complete, in the sense that we infer
   * inferences that are equivalent to conc. This returns false e.g. if conc
   * (or one of its conjuncts if it is a conjunction) was not inferred due
   * to the criteria mentioned above.
   */
  bool sendInternalInference(std::vector<Node>& exp,
                             Node conc,
                             InferenceId infer);

  /** send inference
   *
   * This function should be called when exp => eq. The set exp
   * contains literals that are explainable, i.e. those that hold in the
   * equality engine of the theory of strings. On the other hand, the set
   * noExplain contains nodes that are not explainable by the theory of strings.
   * This method may call sendLemma or otherwise add a InferInfo to d_pending,
   * indicating a fact should be asserted to the equality engine. Overall, the
   * result of this method is one of the following:
   *
   * [1] (No-op) Do nothing if eq is equivalent to true,
   *
   * [2] (Infer) Indicate that eq should be added to the equality engine of this
   * class with explanation exp, where exp is a set of literals that currently
   * hold in the equality engine. We add this to the pending vector d_pending.
   *
   * [3] (Lemma) Indicate that the lemma
   *   ( EXPLAIN(exp \ noExplain) ^ noExplain ) => eq
   * should be sent on the output channel of the theory of strings, where
   * EXPLAIN returns the explanation of the node in exp in terms of the literals
   * asserted to the theory of strings, as computed by the equality engine.
   * This is also added to a pending vector, d_pendingLem.
   *
   * [4] (Conflict) Immediately report a conflict EXPLAIN(exp) on the output
   * channel of the theory of strings.
   *
   * Determining which case to apply depends on the form of eq and whether
   * noExplain is empty. In particular, lemmas must be used whenever noExplain
   * is non-empty, conflicts are used when noExplain is empty and eq is false.
   *
   * @param exp The explanation of eq.
   * @param noExplain The subset of exp that cannot be explained by the
   * equality engine. This may impact whether we are processing this call as a
   * fact or as a lemma.
   * @param eq The conclusion.
   * @param infer Identifies the reason for inference, used for
   * debugging. This updates the statistics about the number of inferences made
   * of each type.
   * @param isRev Whether this is the "reverse variant" of the inference, which
   * is used as a hint for proof reconstruction.
   * @param asLemma If true, then this method will send a lemma instead
   * of a fact whenever applicable.
   * @return true if the inference was not trivial (e.g. its conclusion did
   * not rewrite to true).
   */
  bool sendInference(const std::vector<Node>& exp,
                     const std::vector<Node>& noExplain,
                     Node eq,
                     InferenceId infer,
                     bool isRev = false,
                     bool asLemma = false);
  /** same as above, but where noExplain is empty */
  bool sendInference(const std::vector<Node>& exp,
                     Node eq,
                     InferenceId infer,
                     bool isRev = false,
                     bool asLemma = false);

  /** Send inference
   *
   * This implements the above methods for the InferInfo object. It is called
   * by the methods above.
   *
   * The inference info ii should have a rewritten conclusion and should not be
   * trivial (InferInfo::isTrivial). It is the responsibility of the caller to
   * ensure this.
   *
   * If the flag asLemma is true, then this method will send a lemma instead
   * of a fact whenever applicable.
   */
  void sendInference(InferInfo& ii, bool asLemma = false);
  /** Send split
   *
   * This requests that ( a = b V a != b ) is sent on the output channel as a
   * lemma. We additionally request a phase requirement for the equality a=b
   * with polarity preq.
   *
   * The argument infer identifies the reason for inference, used for
   * debugging. This updates the statistics about the number of
   * inferences made of each type.
   *
   * This method returns true if the split was non-trivial, and false
   * otherwise. A split is trivial if a=b rewrites to a constant.
   */
  bool sendSplit(Node a, Node b, InferenceId infer, bool preq = true);

  //----------------------------constructing antecedants
  /**
   * Adds equality a = b to the vector exp if a and b are distinct terms. It
   * must be the case that areEqual( a, b ) holds in this context.
   */
  void addToExplanation(Node a, Node b, std::vector<Node>& exp) const;
  /** Adds lit to the vector exp if it is non-null */
  void addToExplanation(Node lit, std::vector<Node>& exp) const;
  //----------------------------end constructing antecedants
  /**
   * Have we processed an inference during this call to check? In particular,
   * this returns true if we have a pending fact or lemma, or have encountered
   * a conflict.
   */
  bool hasProcessed() const;

  // ------------------------------------------------- extended theory
  /**
   * Mark that extended function is reduced. If contextDepend is true,
   * then this mark is SAT-context dependent, otherwise it is user-context
   * dependent (see ExtTheory::markReduced).
   */
  void markReduced(Node n, ExtReducedId id, bool contextDepend = true);
  // ------------------------------------------------- end extended theory

  /**
   * Called when ii is ready to be processed as a conflict. This makes a
   * trusted node whose generator is the underlying proof equality engine
   * (if it exists), and sends it on the output channel.
   */
  void processConflict(const InferInfo& ii);

 private:
  /** Called when ii is ready to be processed as a fact */
  void processFact(InferInfo& ii, ProofGenerator*& pg);
  /** Called when ii is ready to be processed as a lemma */
  TrustNode processLemma(InferInfo& ii, LemmaProperty& p);
  /** Reference to the solver state of the theory of strings. */
  SolverState& d_state;
  /** Reference to the term registry of theory of strings */
  TermRegistry& d_termReg;
  /** the extended theory object for the theory of strings */
  ExtTheory& d_extt;
  /** Reference to the statistics for the theory of strings/sequences. */
  SequencesStatistics& d_statistics;
  /** Conversion from inferences to proofs */
  std::unique_ptr<InferProofCons> d_ipc;
  /** Common constants */
  Node d_true;
  Node d_false;
  Node d_zero;
  Node d_one;
};

}  // namespace strings
}  // namespace theory
}  // namespace cvc5

#endif