Updated header settings, moved files to folder, added samples

Author: leventeBajczi

.gitignore

@@ -1,3 +1,2 @@
-*.c
 .idea
 __pycache__

README.md

@@ -1,26 +1,37 @@
 # CHC2C Converter
 
-This project is a Python-based tool that converts Constrained Horn Clauses (CHC) in SMT-LIB format into C code for verification. 
-The CHC2C tool is designed to handle both linear and non-linear CHC problems, producing equivalent C code which can then be used in verification processes.
+This project is a Python-based tool that converts Constrained Horn Clauses (CHC) in SMT-LIB format into C code for
+verification.
+The CHC2C tool is designed to handle both linear and non-linear CHC problems, producing equivalent C code which can then
+be used in verification processes.
 
 ## Features
+
 - Converts CHC files (in SMT-LIB format) into C code.
 - Supports both linear and non-linear CHC transformations.
 - Automatically retries with a recursive mapping if necessary.
 - Command-line interface for specifying input and output files.
 
 ## Prerequisites
+
 - Python 3.12
 - [z3-solver](https://pypi.org/project/z3-solver/)
 
+For exact versions, see [requirements.txt](requirements.txt).
+
+Run `pip install -r requirements.txt` to install all python dependencies.
+
 ## Installation
+
 Clone the repository and navigate to the directory:
+
 ```bash
 git clone https://github.com/your-repo/CHC2C.git
 cd CHC2C
 ```
 
 ## Usage
+
 To use the tool, run the script with a CHC file as input. The following arguments are supported:
 
 ```bash
@@ -31,22 +42,25 @@ To use the tool, run the script with a CHC file as input. The following argument
 - `-o`, `--out`: (Optional) Specifies the name of the output C file. Defaults to `chc.c`.
 - `--recursive`: (Optional) Enables recursive conversion for non-linear CHC problems.
 
-If the tool encounters a recursive CHC problem while using the linear conversion, it will automatically retry using a recursive mapping.
+If the tool encounters a recursive CHC problem while using the linear conversion, it will automatically retry using a
+recursive mapping.
 
 ### Example
+
 ```bash
 ./chc2c.py example.chc -o output.c
 ```
 
 This command converts the `example.chc` file to C code and writes the output to `output.c`.
 
 ## Further Information
+
 For more information on the CHC format, visit [CHC Competition Documentation](https://chc-comp.github.io/format.html).
 
 ## Contributors
 
- * [Levente Bajczi](https://github.com/leventebajczi/)
- * [Mihály Dobos-Kovács](https://github.com/as3810t/)
+* [Levente Bajczi](https://github.com/leventebajczi/)
+* [Mihály Dobos-Kovács](https://github.com/as3810t/)
 
 ## Publications
 

chc2c.py

@@ -1,25 +1,23 @@
 #!/usr/bin/python3
 
-
-#  Copyright 2025 Budapest University of Technology and Economics
-#
-#  Licensed under the Apache License, Version 2.0 (the "License");
-#  you may not use this file except in compliance with the License.
-#  You may obtain a copy of the License at
+#   Copyright 2025 Budapest University of Technology and Economics
 #
-#      http://www.apache.org/licenses/LICENSE-2.0
+#   Licensed under the Apache License, Version 2.0 (the "License");
+#   you may not use this file except in compliance with the License.
+#   You may obtain a copy of the License at
 #
-#  Unless required by applicable law or agreed to in writing, software
-#  distributed under the License is distributed on an "AS IS" BASIS,
-#  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-#  See the License for the specific language governing permissions and
-#  limitations under the License.
+#       http://www.apache.org/licenses/LICENSE-2.0
 #
+#   Unless required by applicable law or agreed to in writing, software
+#   distributed under the License is distributed on an "AS IS" BASIS,
+#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+#   See the License for the specific language governing permissions and
+#   limitations under the License.
 
 import argparse
 
-from LinearCHC2C import LinearCHC2C, RecursiveException
-from NonLinearCHC2C import NonLinearCHC2C
+from src.LinearCHC2C import LinearCHC2C, RecursiveException
+from src.NonLinearCHC2C import NonLinearCHC2C
 
 
 def main():

sample/linear.c

@@ -1,21 +1,21 @@
-#  Copyright 2025 Budapest University of Technology and Economics
+#   Copyright 2025 Budapest University of Technology and Economics
 #
-#  Licensed under the Apache License, Version 2.0 (the "License");
-#  you may not use this file except in compliance with the License.
-#  You may obtain a copy of the License at
+#   Licensed under the Apache License, Version 2.0 (the "License");
+#   you may not use this file except in compliance with the License.
+#   You may obtain a copy of the License at
 #
-#      http://www.apache.org/licenses/LICENSE-2.0
-#
-#  Unless required by applicable law or agreed to in writing, software
-#  distributed under the License is distributed on an "AS IS" BASIS,
-#  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-#  See the License for the specific language governing permissions and
-#  limitations under the License.
+#       http://www.apache.org/licenses/LICENSE-2.0
 #
+#   Unless required by applicable law or agreed to in writing, software
+#   distributed under the License is distributed on an "AS IS" BASIS,
+#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+#   See the License for the specific language governing permissions and
+#   limitations under the License.
 
-import z3
 import re
 
+import z3
+
 
 # As long as the CHC is nonrecursive, this can be used
 class BaseCHC2C:

sample/recursive.c

@@ -1,22 +1,22 @@
-#  Copyright 2025 Budapest University of Technology and Economics
+#   Copyright 2025 Budapest University of Technology and Economics
 #
-#  Licensed under the Apache License, Version 2.0 (the "License");
-#  you may not use this file except in compliance with the License.
-#  You may obtain a copy of the License at
+#   Licensed under the Apache License, Version 2.0 (the "License");
+#   you may not use this file except in compliance with the License.
+#   You may obtain a copy of the License at
 #
-#      http://www.apache.org/licenses/LICENSE-2.0
-#
-#  Unless required by applicable law or agreed to in writing, software
-#  distributed under the License is distributed on an "AS IS" BASIS,
-#  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-#  See the License for the specific language governing permissions and
-#  limitations under the License.
+#       http://www.apache.org/licenses/LICENSE-2.0
 #
+#   Unless required by applicable law or agreed to in writing, software
+#   distributed under the License is distributed on an "AS IS" BASIS,
+#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+#   See the License for the specific language governing permissions and
+#   limitations under the License.
 
-import z3
 import textwrap
 
-from BaseCHC2C import BaseCHC2C
+import z3
+
+from src.BaseCHC2C import BaseCHC2C
 
 
 class RecursiveException(Exception):

sample.smt2 renamed to sample/sample.smt2

@@ -11,25 +11,12 @@
 #   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 #   See the License for the specific language governing permissions and
 #   limitations under the License.
-#
-#  Licensed under the Apache License, Version 2.0 (the "License");
-#  you may not use this file except in compliance with the License.
-#  You may obtain a copy of the License at
-#
-#      http://www.apache.org/licenses/LICENSE-2.0
-#
-#  Unless required by applicable law or agreed to in writing, software
-#  distributed under the License is distributed on an "AS IS" BASIS,
-#  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-#  See the License for the specific language governing permissions and
-#  limitations under the License.
-#
 
 import textwrap
 
 import z3
 
-from BaseCHC2C import BaseCHC2C
+from src.BaseCHC2C import BaseCHC2C
 
 
 # This works for all CHCs, linear, nonlinear, recursive, etc.