/******************************************************************************
 * Top contributors (to current version):
 *   Hanna Lachnitt
 *
 * 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.
 * ****************************************************************************
 *
 * Enumeration of Alethe proof rules
 */

#include "cvc5_private.h"

#ifndef CVC4__PROOF__ALETHE_PROOF_RULE_H
#define CVC4__PROOF__ALETHE_PROOF_RULE_H

#include <memory>

namespace cvc5 {

namespace proof {

enum class AletheRule : uint32_t
{
  // This enumeration lists all Alethe proof rules. For each rule a list of
  // steps is given. The last step is the conclusion obtained by applying the
  // rule in question. There might be zero or more steps occuring before the
  // conclusion in the proof. A step has the form:
  //
  //   G > i. F
  // where G is a context, i is an id and F is a formula. A context may include
  // substitutions x->y and fixed variables x. For more details see
  // https://verit.loria.fr/documentation/alethe-spec.pdf
  //
  //================================================= Special Rules: Commands
  // These rules should be printed as commands
  //
  // ======== subproof
  // > i1. F1
  // ...
  // > in. Fn
  // ...
  // > j. F
  // ---------------------------------
  // > k. (cl (not F1) ... (not Fn) F)
  //
  // Each subproof in Alethe begins with an anchor command. The outermost
  // application of ANCHOR_SUBPROOF will not be printed.
  ANCHOR_SUBPROOF,
  // ======== bind
  // G,y1,...,yn,x1->y1,...,xn->yn > j.  (= F1 F2)
  // ------------------------------------------------------
  // G > k. (= (forall (x1 ... xn) F1) (forall (y1 ... yn) F2))
  //
  // where y1,...,yn are not free in (forall (x1,...,xn) F2)
  ANCHOR_BIND,
  // ======== input
  // > i. F
  ASSUME,
  //================================================= Rules of the Alethe
  // calculus
  //
  // ======== true
  // > i. true
  TRUE,
  // ======== false
  // > i. (not true)
  FALSE,
  // ======== not_not
  // > i.  (cl (not(not(not F)))  F)
  NOT_NOT,
  // ======== and_pos
  // > i.  (cl (not(and F1 ... Fn))  Fi)
  // , with 1 <= i <= n
  AND_POS,
  // ======== and_neg
  // > i.  (cl (and F1 ... Fn) (not F1) ... (not Fn))
  AND_NEG,
  // ======== or_pos
  // > i.  (cl (not (or F1 ... Fn)) (not F1) ... (not Fn))
  OR_POS,
  // ======== or_neg
  // > i.  (cl (or F1 ... Fn) (not Fi))
  // , with 1 <= i <= n
  OR_NEG,
  // ======== xor_pos1
  // > i.  (cl (not (xor F1 F2)) F1 F2)
  XOR_POS1,
  // ======== xor_pos2
  // > i.  (cl (not (xor F1 F2)) (not F1) (not F2))
  XOR_POS2,
  // ======== xor_neg1
  // > i.  (cl (xor F1 F2) F1 (not F2))
  XOR_NEG1,
  // ======== xor_neg2
  // > i.  (cl (xor F1 F2) (not F1) F2)
  XOR_NEG2,
  // ======== implies_pos
  // > i.  (cl (not (implies F1 F2)) (not F1) F2)
  IMPLIES_POS,
  // ======== implies_neg1
  // > i.  (cl (implies F1 F2) F1)
  IMPLIES_NEG1,
  // ======== implies_neg2
  // > i.  (cl (implies F1 F2) (not F2))
  IMPLIES_NEG2,
  // ======== equiv_pos1
  // > i.  (cl (not (= F1 F2)) F1 (not F2))
  EQUIV_POS1,
  // ======== equiv_pos2
  // > i.  (cl (not (= F1 F2)) (not F1) F2)
  EQUIV_POS2,
  // ======== equiv_neg1
  // > i.  (cl (= F1 F2) (not F1) (not F2))
  EQUIV_NEG1,
  // ======== equiv_neg2
  // > i.  (cl (= F1 F2) F1 F2)
  EQUIV_NEG2,
  // ======== ite_pos1
  // > i.  (cl (not (ite F1 F2 F3)) F1 F3)
  ITE_POS1,
  // ======== ite_pos2
  // > i.  (cl (not (ite F1 F2 F3)) (not F1) F2)
  ITE_POS2,
  // ======== ite_neg1
  // > i.  (cl (ite F1 F2 F3) F1 (not F3))
  ITE_NEG1,
  // ======== ite_neg2
  // > i.  (cl (ite F1 F2 F3) (not F1) (not F2))
  ITE_NEG2,
  // ======== eq_reflexive
  // > i.  (= F F)
  EQ_REFLEXIVE,
  // ======== eq_transitive
  // > i.  (cl (not (= F1 F2)) ... (not (= F_{n-1} Fn)) (= F1 Fn))
  EQ_TRANSITIVE,
  // ======== eq_congruent
  // > i.  (cl (not (= F1 G1)) ... (not (= Fn Gn)) (= f(F1,...,Fn)
  // f(G1,...,Gn)))
  EQ_CONGRUENT,
  // ======== eq_congruent_pred
  // > i.  (cl (not (= F1 G1)) ... (not (= Fn Gn)) (= P(F1,...,Fn)
  // P(G1,...,Gn)))
  EQ_CONGRUENT_PRED,
  // ======== distinct_elim
  // If called with one argument:
  //  > i. (= (distinct F) true)
  // If applied to terms of type Bool more than two terms can never be distinct.
  // Two cases can be possible:
  //  > i. (= (distinct F G) (not (= F G)))
  // and
  //  > i. (= (distinct F1 F2 F3 ...) false)
  // In general:
  //  > i. (= (distinct F1 ... Fn) (AND^n_i=1 (AND^n_j=i+1 (!= Fi Fj))))
  DISTINCT_ELIM,
  // ======== la_rw_eq
  // > i. (= (= F G) (and (<= F G) (<= G F)))
  LA_RW_EQ,
  // Tautology of linear disequalities.
  // > i. (cl F1 ... Fn)
  LA_GENERIC,
  // Tautology of linear integer arithmetic
  // > i. (cl F1 ... Fn)
  LIA_GENERIC,
  // ======== la_disequality
  // > i. (= (= F G) (not (<= F G)) (not (<= G F)))
  LA_DISEQUALITY,
  // ======== la_totality
  // > i. (or (<= t1 t2) (<= t2 t1))
  LA_TOTALITY,
  // ======== la_tautology
  // Tautology of linear arithmetic that can be checked without sophisticated
  // reasoning.
  LA_TAUTOLOGY,
  // ======== forall_inst
  // > i. (or (not (forall (x1 ... xn) P)) P[t1/x1]...[tn/xn])
  // args = ((:= x_k1 tk1) ... (:= xkn tkn))
  // where k1,...,kn is a permutation of 1,...,n and xi and ki have the same
  // sort.
  FORALL_INST,
  // ======== qnt_join
  // G > i. (= (Q (x1 ... xn) (Q (xn+1 ... xm) F)) (Q (xk1 ... xko) F))
  // where m>n, Q in {forall,exist}, k1...ko is a monotonic map 1,...,m s.t.
  // xk1,...,xko are pairwise distinct and {x1,...,xm} = {xk1,...,xko}.
  QNT_JOIN,
  // ======== qnt_tm_unused
  // G > i. (= (Q (x1 ... xn) F) (Q (xk1 ... xkm) F))
  // where m <= n, Q in {forall,exists}, k1,...,km is monotonic map to 1,...,n
  // and if x in {xj | j in {1,...,n} and j not in {k1,...,km}} then x is not
  // free in P
  QNT_RM_UNUSED,
  // ======== th_resolution
  // > i1. (cl F^1_1 ... F^1_k1)
  // ...
  // > in. (cl F^n_1 ... F^n_kn)
  // ...
  // > i1,...,in. (cl F^r1_s1 ... F^rm_sm)
  // where (cl F^r1_s1 ... F^rm_sm) are from F^i_j and are the result of a chain
  // of predicate resolution steps on the clauses i1 to in. This rule is used
  // when the resolution step is not emitted by the SAT solver.
  TH_RESOLUTION,
  // ======== resolution
  // This rule is equivalent to the th_resolution rule but is emitted by the SAT
  // solver.
  RESOLUTION,
  // ======== refl
  // G > i. (= F1 F2)
  REFL,
  // ======== trans
  // G > i. (= F1 F2)
  // ...
  // G > j. (= F2 F3)
  // ...
  // G > k. (= F1 F3)
  TRANS,
  // ======== cong
  // G > i1. (= F1 G1)
  // ...
  // G > in. (= Fn Gn)
  // ...
  // G > j. (= (f F1 ... Fn) (f G1 ... Gn))
  // where f is an n-ary function symbol.
  CONG,
  // ======== and
  // > i. (and F1 ... Fn)
  // ...
  // > j. Fi
  AND,
  // ======== tautologic_clause
  // > i. (cl F1 ... Fi ... Fj ... Fn)
  // ...
  // > j. true
  // where Fi != Fj
  TAUTOLOGIC_CLAUSE,
  // ======== not_or
  // > i. (not (or F1 ... Fn))
  // ...
  // > j. (not Fi)
  NOT_OR,
  // ======== or
  // > i. (or F1 ... Fn)
  // ...
  // > j. (cl F1 ... Fn)
  OR,
  // ======== not_and
  // > i. (not (and F1 ... Fn))
  // ...
  // > j. (cl (not F1) ... (not Fn))
  NOT_AND,
  // ======== xor1
  // > i. (xor F1 F2)
  // ...
  // > j. (cl F1 F2)
  XOR1,
  // ======== xor2
  // > i. (xor F1 F2)
  // ...
  // > j. (cl (not F1) (not F2))
  XOR2,
  // ======== not_xor1
  // > i. (not (xor F1 F2))
  // ...
  // > j. (cl F1 (not F2))
  NOT_XOR1,
  // ======== not_xor2
  // > i. (not (xor F1 F2))
  // ...
  // > j. (cl (not F1) F2)
  NOT_XOR2,
  // ======== implies
  // > i. (=> F1 F2)
  // ...
  // > j. (cl (not F1) F2)
  IMPLIES,
  // ======== not_implies1
  // > i. (not (=> F1 F2))
  // ...
  // > j. (not F2)
  NOT_IMPLIES1,
  // ======== not_implies2
  // > i. (not (=> F1 F2))
  // ...
  // > j. (not F2)
  NOT_IMPLIES2,
  // ======== equiv1
  // > i. (= F1 F2)
  // ...
  // > j. (cl (not F1) F2)
  EQUIV1,
  // ======== equiv2
  // > i. (= F1 F2)
  // ...
  // > j. (cl F1 (not F2))
  EQUIV2,
  // ======== not_equiv1
  // > i. (not (= F1 F2))
  // ...
  // > j. (cl F1 F2)
  NOT_EQUIV1,
  // ======== not_equiv2
  // > i. (not (= F1 F2))
  // ...
  // > j. (cl (not F1) (not F2))
  NOT_EQUIV2,
  // ======== ite1
  // > i. (ite F1 F2 F3)
  // ...
  // > j. (cl F1 F3)
  ITE1,
  // ======== ite2
  // > i. (ite F1 F2 F3)
  // ...
  // > j. (cl (not F1) F2)
  ITE2,
  // ======== not_ite1
  // > i. (not (ite F1 F2 F3))
  // ...
  // > j. (cl F1 (not F3))
  NOT_ITE1,
  // ======== not_ite2
  // > i. (not (ite F1 F2 F3))
  // ...
  // > j. (cl (not F1) (not F3))
  NOT_ITE2,
  // ======== ite_intro
  // > i. (= F (and F F1 ... Fn))
  // where F contains the ite operator. Let G1,...,Gn be the terms starting with
  // ite, i.e. Gi := (ite Fi Hi Hi'), then Fi = (ite Fi (= Gi Hi) (= Gi Hi')) if
  // Hi is of sort Bool
  ITE_INTRO,
  // ======== duplicated_literals
  // > i. (cl F1 ... Fn)
  // ...
  // > j. (cl Fk1 ... Fkm)
  // where m <= n and k1,...,km is a monotonic map to 1,...,n such that Fk1 ...
  // Fkm are pairwise distinct and {F1,...,Fn} = {Fk1 ... Fkm}
  DUPLICATED_LITERALS,
  // ======== connective_def
  //  G > i. (= (xor F1 F2) (or (and (not F1) F2) (and F1 (not F2))))
  // or
  //  G > i. (= (= F1 F2) (and (=> F1 F2) (=> F2 F1)))
  // or
  //  G > i. (= (ite F1 F2 F3) (and (=> F1 F2) (=> (not F1) (not F3))))
  CONNECTIVE_DEF,
  // ======== Simplify rules
  // The following rules are simplifying rules introduced as tautologies that can be
  // verified by a number of simple transformations
  ITE_SIMPLIFY,
  EQ_SIMPLIFY,
  AND_SIMPLIFY,
  OR_SIMPLIFY,
  NOT_SIMPLIFY,
  IMPLIES_SIMPLIFY,
  EQUIV_SIMPLIFY,
  BOOL_SIMPLIFY,
  QUANTIFIER_SIMPLIFY,
  DIV_SIMPLIFY,
  PROD_SIMPLIFY,
  UNARY_MINUS_SIMPLIFY,
  MINUS_SIMPLIFY,
  SUM_SIMPLIFY,
  COMP_SIMPLIFY,
  NARY_ELIM,
  QNT_SIMPLIFY,
  // ======== let
  // G,x1->F1,...,xn->Fn > j. (= G G')
  // ---------------------------------
  // G > k. (= (let (x1 := F1,...,xn := Fn.G) G')
  LET,
  // ======== sko_ex
  // G,x1->(e x1.F),...,xn->(e xn.F) > j. (= F G)
  // --------------------------------------------
  // G > k. (exists (x1 ... xn) (= F G))
  SKO_EX,
  // ======== sko_forall
  // G,x1->(e x1.(not F)),...,xn->(e xn.(not F)) > j. (= F G)
  // --------------------------------------------------------
  // G > k. (forall (x1 ... xn) (= F G))
  SKO_FORALL,
  // ======== symm
  // > i. (= F G)
  // ...
  // > j. (= G F)
  SYMM,
  // ======== not_symm
  // > i. (not (= F G))
  // ...
  // > j. (not (= G F))
  NOT_SYMM,
  // ======== reorder
  // > i1. F1
  // ...
  // > j. F2
  // where set representation of F1 and F2 are the same and the number of
  // literals in C2 is the same of that of C1.
  REORDER,
  // ======== undefined
  // Used in case that a step in the proof rule could not be translated.
  UNDEFINED
};

/**
 * Converts an Alethe proof rule to a string.
 *
 * @param id The Alethe proof rule
 * @return The name of the Alethe proof rule
 */
const char* aletheRuleToString(AletheRule id);

/**
 * Writes an Alethe proof rule name to a stream.
 *
 * @param out The stream to write to
 * @param id The Alethe proof rule to write to the stream
 * @return The stream
 */
std::ostream& operator<<(std::ostream& out, AletheRule id);

}  // namespace proof

}  // namespace cvc5

#endif /* CVC4__PROOF__ALETHE_PROOF_RULE_H */