[proof] Alethe proof rules (#7180)

Adds header for Alethe proof rules

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

1 files changed, 427 insertions, 0 deletions

diff --git a/src/proof/alethe/alethe_proof_rule.h b/src/proof/alethe/alethe_proof_rule.h
new file mode 100644
index 000000000..127bb8161
--- /dev/null
+++ b/src/proof/alethe/alethe_proof_rule.h
@@ -0,0 +1,427 @@
+/******************************************************************************
+ * 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 */