X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Ftheory%2Farith%2Fnl%2Fext_theory_callback.h;h=a810d9d537b32af18623079728040a2b75b13678;hb=4a8d2407468eee50c91fc6cbe19f5edd8feeb688;hp=0d95db16637fa596fd837a6a89febcc3143c8f1f;hpb=8b4444dad1647c89b313deedd22129252078fe1b;p=cvc5.git

diff --git a/src/theory/arith/nl/ext_theory_callback.h b/src/theory/arith/nl/ext_theory_callback.h
index 0d95db166..a810d9d53 100644
--- a/src/theory/arith/nl/ext_theory_callback.h
+++ b/src/theory/arith/nl/ext_theory_callback.h
@@ -1,25 +1,29 @@
-/*********************                                                        */
-/*! \file ext_theory_callback.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 The extended theory callback for non-linear arithmetic
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Tim King, 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.
+ * ****************************************************************************
+ *
+ * The extended theory callback for non-linear arithmetic.
+ */
 
-#ifndef CVC4__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H
-#define CVC4__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H
+#define CVC5__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H
 
 #include "expr/node.h"
 #include "theory/ext_theory.h"
 
-namespace CVC4 {
+namespace cvc5 {
 namespace theory {
+namespace eq {
+class EqualityEngine;
+}
 namespace arith {
 namespace nl {
 
@@ -69,7 +73,8 @@ class NlExtTheoryCallback : public ExtTheoryCallback
   bool isExtfReduced(int effort,
                      Node n,
                      Node on,
-                     std::vector<Node>& exp) override;
+                     std::vector<Node>& exp,
+                     ExtReducedId& id) override;
 
  private:
   /** The underlying equality engine. */
@@ -81,6 +86,6 @@ class NlExtTheoryCallback : public ExtTheoryCallback
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H */
+#endif /* CVC5__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H */