(proof-new) Add the term conversion sequence generator (#5097)

This class will be used in the theory preprocessor and is planned to be used in other preprocessing passes that can be understood as sequences of rewrite systems.

1 files changed, 9 insertions, 0 deletions

diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h
index 47fdf3ebd..7d7993146 100644
--- a/src/expr/proof_node_manager.h
+++ b/src/expr/proof_node_manager.h
@@ -81,6 +81,15 @@ class ProofNodeManager
    */
   std::shared_ptr<ProofNode> mkAssume(Node fact);
   /**
+   * Make transitivity proof, where children contains one or more proofs of
+   * equalities that form an ordered chain. In other words, the vector children
+   * is a legal set of children for an application of TRANS.
+   */
+  std::shared_ptr<ProofNode> mkTrans(
+      const std::vector<std::shared_ptr<ProofNode>>& children,
+      Node expected = Node::null());
+
+  /**
    * Make scope having body pf and arguments (assumptions-to-close) assumps.
    * If ensureClosed is true, then this method throws an assertion failure if
    * the returned proof is not closed. This is the case if a free assumption