1 files changed, 44 insertions, 43 deletions
diff --git a/examples/api/sygus-grammar.cpp b/examples/api/sygus-grammar.cpp
index 441cfa30c..095f15889 100644
--- a/examples/api/sygus-grammar.cpp
+++ b/examples/api/sygus-grammar.cpp
@@ -1,46 +1,47 @@
-/*********************                                                        */
-/*! \file sygus-grammar.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Abdalrhman Mohamed, Mudathir Mohamed
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief A simple demonstration of the Sygus API.
- **
- ** A simple demonstration of how to use Grammar to add syntax constraints to
- ** the Sygus solution for the identity function. Here is the same problem
- ** written in Sygus V2 format:
- **
- ** (set-logic LIA)
- **
- ** (synth-fun id1 ((x Int)) Int
- **   ((Start Int)) ((Start Int ((- x) (+ x Start)))))
- **
- ** (synth-fun id2 ((x Int)) Int
- **   ((Start Int)) ((Start Int ((Variable Int) (- x) (+ x Start)))))
- **
- ** (synth-fun id3 ((x Int)) Int
- **   ((Start Int)) ((Start Int (0 (- x) (+ x Start)))))
- **
- ** (synth-fun id4 ((x Int)) Int
- **   ((Start Int)) ((Start Int ((- x) (+ x Start)))))
- **
- ** (declare-var x Int)
- **
- ** (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x))
- **
- ** (check-synth)
- **
- ** The printed output to this example should look like:
- ** (define-fun id1 ((x Int)) Int (+ x (+ x (- x))))
- ** (define-fun id2 ((x Int)) Int x)
- ** (define-fun id3 ((x Int)) Int (+ x 0))
- ** (define-fun id4 ((x Int)) Int (+ x (+ x (- x))))
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * A simple demonstration of the Sygus API.
+ *
+ * A simple demonstration of how to use Grammar to add syntax constraints to
+ * the Sygus solution for the identity function. Here is the same problem
+ * written in Sygus V2 format:
+ *
+ * (set-logic LIA)
+ *
+ * (synth-fun id1 ((x Int)) Int
+ *   ((Start Int)) ((Start Int ((- x) (+ x Start)))))
+ *
+ * (synth-fun id2 ((x Int)) Int
+ *   ((Start Int)) ((Start Int ((Variable Int) (- x) (+ x Start)))))
+ *
+ * (synth-fun id3 ((x Int)) Int
+ *   ((Start Int)) ((Start Int (0 (- x) (+ x Start)))))
+ *
+ * (synth-fun id4 ((x Int)) Int
+ *   ((Start Int)) ((Start Int ((- x) (+ x Start)))))
+ *
+ * (declare-var x Int)
+ *
+ * (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x))
+ *
+ * (check-synth)
+ *
+ * The printed output to this example should look like:
+ * (define-fun id1 ((x Int)) Int (+ x (+ x (- x))))
+ * (define-fun id2 ((x Int)) Int x)
+ * (define-fun id3 ((x Int)) Int (+ x 0))
+ * (define-fun id4 ((x Int)) Int (+ x (+ x (- x))))
+ */
 
 #include <cvc5/cvc5.h>