diff --git a/examples/c/README b/examples/c/README new file mode 100644 index 000000000..5ea885519 --- /dev/null +++ b/examples/c/README @@ -0,0 +1,11 @@ +Small example using the c++ bindings. +To build the example execute + make examples +in the build directory. + +This command will create the executable c_example. +On Windows, you can just execute it. +On OSX and Linux, you must install z3 first using + sudo make install +OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX) with the build directory. You need that to be able to find the Z3 shared library. + diff --git a/examples/c/README.txt b/examples/c/README.txt deleted file mode 100644 index c23e632c4..000000000 --- a/examples/c/README.txt +++ /dev/null @@ -1,25 +0,0 @@ -WARNING: this example still uses the old Z3 (version 3.x) C API. -The current version is backward compatible. - -1) Using Visual Studio (with Z3 source code release) - -The test_capi application is automatically built when the z3-prover.sln is processed. The following command should be used to compile z3-prover.sln in the Z3 root directory - - msbuild /p:configuration=external - -The maxsat executable is located at - - ..\external\test_capi - -2) Using gcc (on Linux or OSX) - -Use 'build.sh' to build the test application using gcc. - -You must install Z3 before running this example. -To install Z3, execute the following command in the Z3 root directory. - - sudo make install - -Use 'build.sh' to build the test application using gcc. -It generates the executable 'test_capi'. - diff --git a/examples/c/build.sh b/examples/c/build.sh deleted file mode 100755 index 0caa7fff5..000000000 --- a/examples/c/build.sh +++ /dev/null @@ -1,9 +0,0 @@ -if gcc -fopenmp -o test_capi test_capi.c -lz3; then - echo "test_capi applicatio was successfully compiled." - echo "To try it, execute:" - echo " ./test_capi" -else - echo "You must install Z3 before compiling this example." - echo "To install Z3, execute the following command in the Z3 root directory." - echo " sudo make install" -fi diff --git a/examples/c/test_capi.vcxproj b/examples/c/test_capi.vcxproj deleted file mode 100644 index 91121ab1e..000000000 --- a/examples/c/test_capi.vcxproj +++ /dev/null @@ -1,430 +0,0 @@ - - - - - commercial - Win32 - - - commercial - x64 - - - Debug - Win32 - - - Debug - x64 - - - external - Win32 - - - external - x64 - - - release_mt - Win32 - - - release_mt - x64 - - - Release - Win32 - - - Release - x64 - - - - {9E76526D-EDA2-4B88-9616-A8FC08F31071} - test_capi - Win32Proj - - - - Application - Unicode - true - - - Application - Unicode - true - - - Application - Unicode - true - - - Application - Unicode - true - - - Application - Unicode - - - Application - Unicode - true - - - Application - Unicode - true - - - Application - Unicode - true - - - Application - Unicode - true - - - Application - Unicode - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - <_ProjectFileVersion>10.0.30319.1 - $(SolutionDir)$(Configuration)\ - $(Configuration)\ - true - $(SolutionDir)$(Platform)\$(Configuration)\ - $(Platform)\$(Configuration)\ - true - $(SolutionDir)$(Configuration)\ - $(Configuration)\ - false - $(SolutionDir)$(Platform)\$(Configuration)\ - $(Platform)\$(Configuration)\ - false - $(SolutionDir)$(Configuration)\ - $(SolutionDir)$(Configuration)\ - $(SolutionDir)$(Configuration)\ - $(Configuration)\ - $(Configuration)\ - $(Configuration)\ - false - false - false - $(SolutionDir)$(Platform)\$(Configuration)\ - $(SolutionDir)$(Platform)\$(Configuration)\ - $(SolutionDir)$(Platform)\$(Configuration)\ - $(Platform)\$(Configuration)\ - $(Platform)\$(Configuration)\ - $(Platform)\$(Configuration)\ - false - false - false - AllRules.ruleset - - - AllRules.ruleset - - - AllRules.ruleset - - - AllRules.ruleset - - - AllRules.ruleset - AllRules.ruleset - AllRules.ruleset - - - - - - - AllRules.ruleset - AllRules.ruleset - AllRules.ruleset - - - - - - - - - - Disabled - ..\lib;%(AdditionalIncludeDirectories) - WIN32;_CONSOLE;Z3DEBUG;_WINDOWS;%(PreprocessorDefinitions) - true - EnableFastChecks - MultiThreadedDebugDLL - - - Level3 - EditAndContinue - - - true - Console - false - - - MachineX86 - - - - - X64 - - - Disabled - ..\lib;%(AdditionalIncludeDirectories) - WIN32;_CONSOLE;Z3DEBUG;_WINDOWS;%(PreprocessorDefinitions) - true - EnableFastChecks - MultiThreadedDebugDLL - - - Level3 - ProgramDatabase - - - true - Console - MachineX64 - - - - - false - ..\lib;%(AdditionalIncludeDirectories) - WIN32;NDEBUG;_CONSOLE;_WINDOWS;%(PreprocessorDefinitions) - MultiThreaded - - - Level3 - ProgramDatabase - - - psapi.lib;%(AdditionalDependencies) - true - Console - 8388608 - true - true - false - - - MachineX86 - - - - - X64 - - - false - ..\lib;%(AdditionalIncludeDirectories) - WIN32;NDEBUG;_CONSOLE;_WINDOWS;%(PreprocessorDefinitions) - MultiThreaded - - - Level3 - ProgramDatabase - - - psapi.lib;%(AdditionalDependencies) - true - Console - 8388608 - true - true - MachineX64 - - - - - ..\lib;%(AdditionalIncludeDirectories) - WIN32;_CONSOLE;_WINDOWS;%(PreprocessorDefinitions) - MultiThreadedDLL - - - Level3 - ProgramDatabase - - - true - Console - true - true - false - - - MachineX86 - - - - - ..\lib;%(AdditionalIncludeDirectories) - WIN32;_CONSOLE;_WINDOWS;%(PreprocessorDefinitions) - MultiThreadedDLL - - - Level3 - ProgramDatabase - - - true - Console - true - true - false - - - MachineX86 - - - - - ..\lib;%(AdditionalIncludeDirectories) - WIN32;_CONSOLE;_WINDOWS;%(PreprocessorDefinitions) - MultiThreadedDLL - - - Level3 - ProgramDatabase - - - true - Console - true - true - false - - - MachineX86 - - - - - X64 - - - ..\lib;%(AdditionalIncludeDirectories) - WIN32;_CONSOLE;_WINDOWS;%(PreprocessorDefinitions) - MultiThreadedDLL - - - Level3 - ProgramDatabase - - - true - Console - true - true - MachineX64 - - - - - X64 - - - ..\lib;%(AdditionalIncludeDirectories) - WIN32;_CONSOLE;_WINDOWS;%(PreprocessorDefinitions) - MultiThreadedDLL - - - Level3 - ProgramDatabase - - - true - Console - true - true - MachineX64 - - - - - X64 - - - ..\lib;%(AdditionalIncludeDirectories) - WIN32;_CONSOLE;_WINDOWS;%(PreprocessorDefinitions) - MultiThreadedDLL - - - Level3 - ProgramDatabase - - - true - Console - true - true - MachineX64 - - - - - - - - {0bf8cb94-61c7-4545-ae55-c58d858aa8b6} - false - - - {4a7e5a93-19d8-4382-8950-fb2edec7a76e} - false - - - - - - \ No newline at end of file diff --git a/examples/maxsat/README b/examples/maxsat/README new file mode 100644 index 000000000..cf022d847 --- /dev/null +++ b/examples/maxsat/README @@ -0,0 +1,12 @@ +Small example using the c++ bindings. +To build the example execute + make examples +in the build directory. + +This command will create the executable maxsat. +On Windows, you can just execute it. +On OSX and Linux, you must install z3 first using + sudo make install +OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX) with the build directory. You need that to be able to find the Z3 shared library. + +This directory contains a test file (ex.smt) that can be use as input for the maxsat test application. diff --git a/examples/maxsat/README-external.txt b/examples/maxsat/README-external.txt deleted file mode 100644 index bfef1acaa..000000000 --- a/examples/maxsat/README-external.txt +++ /dev/null @@ -1,16 +0,0 @@ -WARNING: this example still uses the old Z3 (version 3.x) C API. -The current version is backward compatible. - -This directory contains scripts to build the MaxSAT application using -Microsoft C compiler, or gcc. - -1) Using Microsoft C compiler (with binary release) - -Use 'build.cmd' to build the MaxSAT application using Microsoft C compiler. - -Remark: The Microsoft C compiler (cl) must be in your path, -or you can use the Visual Studio Command Prompt. - -The script 'exec.cmd' adds the bin directory to the path. So, -maxsat.exe can find z3.dll. - diff --git a/examples/maxsat/README.txt b/examples/maxsat/README.txt deleted file mode 100644 index 82eb6bc2a..000000000 --- a/examples/maxsat/README.txt +++ /dev/null @@ -1,28 +0,0 @@ -WARNING: this example still uses the old Z3 (version 3.x) C API. -The current version is backward compatible. - -1) Using Visual Studio (with Z3 source code release) - -The maxsat example application is automatically built when the z3-prover.sln is processed. The following command should be used to compile z3-prover.sln in the Z3 root directory - - msbuild /p:configuration=external - -The maxsat executable is located at - - ..\external\maxsat - -To process ex.smt, use - - ..\external\maxsat ex.smt - -2) Using gcc (on Linux or OSX) - -Use 'build.sh' to build the MaxSAT application using gcc. - -You must install Z3 before running this example. -To install Z3, execute the following command in the Z3 root directory. - - sudo make install - -Use 'build.sh' to build the test application using gcc. -It generates the executable 'maxsat'. diff --git a/examples/maxsat/build-external.cmd b/examples/maxsat/build-external.cmd deleted file mode 100644 index d71fb0e9b..000000000 --- a/examples/maxsat/build-external.cmd +++ /dev/null @@ -1 +0,0 @@ -cl /I ..\..\include ..\..\bin\z3.lib maxsat.c diff --git a/examples/maxsat/build.sh b/examples/maxsat/build.sh deleted file mode 100755 index 22770c134..000000000 --- a/examples/maxsat/build.sh +++ /dev/null @@ -1,9 +0,0 @@ -if gcc -fopenmp -o maxsat maxsat.c -lz3; then - echo "maxsat example was successfully compiled." - echo "To run example, execute:" - echo " ./maxsat ex.smt" -else - echo "You must install Z3 before compiling this example." - echo "To install Z3, execute the following command in the Z3 root directory." - echo " sudo make install" -fi diff --git a/examples/maxsat/exec-external.cmd b/examples/maxsat/exec-external.cmd deleted file mode 100644 index 9610dec88..000000000 --- a/examples/maxsat/exec-external.cmd +++ /dev/null @@ -1,5 +0,0 @@ -@echo off -SETLOCAL -set PATH=..\..\bin;%PATH% -maxsat.exe %1 -ENDLOCAL diff --git a/examples/maxsat/maxsat.vcxproj b/examples/maxsat/maxsat.vcxproj deleted file mode 100644 index 4858316d4..000000000 --- a/examples/maxsat/maxsat.vcxproj +++ /dev/null @@ -1,295 +0,0 @@ - - - - - commercial - Win32 - - - commercial - x64 - - - Debug - Win32 - - - Debug - x64 - - - external - Win32 - - - external - x64 - - - Release - Win32 - - - Release - x64 - - - - {7C154132-AAAB-4F60-B652-F8C51A63D244} - Win32Proj - maxsat - - - - Application - true - Unicode - - - Application - true - Unicode - - - Application - false - true - Unicode - - - Application - false - true - Unicode - - - Application - false - true - Unicode - - - Application - false - true - Unicode - - - Application - false - true - Unicode - - - Application - false - true - Unicode - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - true - - - true - - - false - - - false - - - false - - - false - - - false - - - false - - - - - - Level3 - Disabled - WIN32;_DEBUG;_CONSOLE;%(PreprocessorDefinitions) - ..\lib - - - Console - true - false - - - - - - - Level3 - Disabled - WIN32;_DEBUG;_CONSOLE;%(PreprocessorDefinitions) - ..\lib - - - Console - true - false - - - - - Level3 - - - MaxSpeed - true - true - WIN32;NDEBUG;_CONSOLE;%(PreprocessorDefinitions) - ..\lib - - - Console - true - true - true - - - - - Level3 - - - MaxSpeed - true - true - WIN32;NDEBUG;_CONSOLE;%(PreprocessorDefinitions) - ..\lib - - - Console - true - true - true - - - - - Level3 - - - MaxSpeed - true - true - WIN32;NDEBUG;_CONSOLE;%(PreprocessorDefinitions) - ..\lib - - - Console - true - true - true - - - - - Level3 - - - MaxSpeed - true - true - _AMD64_;WIN32;NDEBUG;_CONSOLE;%(PreprocessorDefinitions) - ..\lib - - - Console - true - true - true - - - - - Level3 - - - MaxSpeed - true - true - WIN32;NDEBUG;_CONSOLE;%(PreprocessorDefinitions) - ..\lib - - - Console - true - true - true - - - - - Level3 - - - MaxSpeed - true - true - WIN32;NDEBUG;_CONSOLE;%(PreprocessorDefinitions) - ..\lib - - - Console - true - true - true - - - - - - - - {4a7e5a93-19d8-4382-8950-fb2edec7a76e} - true - false - false - true - false - - - - - - \ No newline at end of file diff --git a/scripts/mk_make.py b/scripts/mk_make.py index 238197b17..2bf58a6b6 100644 --- a/scripts/mk_make.py +++ b/scripts/mk_make.py @@ -75,6 +75,8 @@ add_hlib('cpp', 'bindings/c++', includes2install=['z3++.h']) set_z3py_dir('bindings/python') # Examples add_cpp_example('cpp_example', 'c++') +add_c_example('c_example', 'c') +add_c_example('maxsat') add_dotnet_example('dotnet_example', 'dotnet') update_version(4, 2, 0, 0) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 8c1f995e6..eb63ea5f5 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -229,6 +229,9 @@ def is_verbose(): def get_cpp_files(path): return filter(lambda f: f.endswith('.cpp'), os.listdir(path)) +def get_c_files(path): + return filter(lambda f: f.endswith('.c'), os.listdir(path)) + def get_cs_files(path): return filter(lambda f: f.endswith('.cs'), os.listdir(path)) @@ -584,7 +587,7 @@ class DotNetDLLComponent(Component): class ExampleComponent(Component): def __init__(self, name, path): Component.__init__(self, name, path, []) - self.ex_dir = '%s/%s' % (EXAMPLE_DIR, path) + self.ex_dir = '%s/%s' % (EXAMPLE_DIR, self.path) self.to_ex_dir = '%s/%s' % (REV_BUILD_DIR, self.ex_dir) def is_example(self): @@ -594,20 +597,26 @@ class CppExampleComponent(ExampleComponent): def __init__(self, name, path): ExampleComponent.__init__(self, name, path) + def compiler(self): + return "$(CXX)" + + def src_files(self): + return get_cpp_files(self.ex_dir) + def mk_makefile(self, out): dll_name = get_component(Z3_DLL_COMPONENT).dll_name dll = '%s$(SO_EXT)' % dll_name exefile = '%s$(EXE_EXT)' % self.name out.write('%s: %s' % (exefile, dll)) - for cppfile in get_cpp_files(self.ex_dir): + for cppfile in self.src_files(): out.write(' ') out.write('%s/%s' % (self.to_ex_dir, cppfile)) out.write('\n') - out.write('\t$(LINK) $(LINK_OUT_FLAG)%s $(LINK_FLAGS)' % exefile) + out.write('\t%s $(LINK_OUT_FLAG)%s $(LINK_FLAGS)' % (self.compiler(), exefile)) # Add include dir components out.write(' -I%s' % get_component(API_COMPONENT).to_src_dir) out.write(' -I%s' % get_component(CPP_COMPONENT).to_src_dir) - for cppfile in get_cpp_files(self.ex_dir): + for cppfile in self.src_files(): out.write(' ') out.write('%s/%s' % (self.to_ex_dir, cppfile)) out.write(' ') @@ -618,6 +627,16 @@ class CppExampleComponent(ExampleComponent): out.write(' $(LINK_EXTRA_FLAGS)\n') out.write('_ex_%s: %s\n\n' % (self.name, exefile)) +class CExampleComponent(CppExampleComponent): + def __init__(self, name, path): + CppExampleComponent.__init__(self, name, path) + + def compiler(self): + return "$(CC)" + + def src_files(self): + return get_c_files(self.ex_dir) + class DotNetExampleComponent(ExampleComponent): def __init__(self, name, path): ExampleComponent.__init__(self, name, path) @@ -682,6 +701,10 @@ def add_cpp_example(name, path=None): c = CppExampleComponent(name, path) reg_component(name, c) +def add_c_example(name, path=None): + c = CExampleComponent(name, path) + reg_component(name, c) + def add_dotnet_example(name, path=None): c = DotNetExampleComponent(name, path) reg_component(name, c)