mirror of
				https://github.com/Z3Prover/z3
				synced 2025-11-04 13:29:11 +00:00 
			
		
		
		
	Cleaned maxsat example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
		
							parent
							
								
									659fe1e361
								
							
						
					
					
						commit
						dfaa03b018
					
				
					 13 changed files with 34 additions and 46 deletions
				
			
		| 
						 | 
				
			
			@ -1,12 +1,12 @@
 | 
			
		|||
WARNING: this example still uses the old Z3 (version 3.x) C API. The current version is backward compatible. 
 | 
			
		||||
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
 | 
			
		||||
1) Using Microsoft C compiler (with binary release)
 | 
			
		||||
 | 
			
		||||
Use 'build.cmd' to build the MaxSAT application using Microsoft C
 | 
			
		||||
compiler.
 | 
			
		||||
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.
 | 
			
		||||
| 
						 | 
				
			
			@ -14,12 +14,3 @@ 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.
 | 
			
		||||
 | 
			
		||||
 | 
			
		||||
2) Using gcc
 | 
			
		||||
 | 
			
		||||
Use 'build.sh' to build the MaxSAT application using gcc. 
 | 
			
		||||
The script 'exec.sh' adds the bin directory to the path. So, 
 | 
			
		||||
maxsat.exe can find z3.dll.
 | 
			
		||||
 | 
			
		||||
Remark: the scripts 'build.sh' and 'exec.sh' assumes you are in a
 | 
			
		||||
Cygwin or Mingw shell.
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -1,8 +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 gcc.
 | 
			
		||||
 | 
			
		||||
Use 'build.sh' to build the MaxSAT application using gcc. 
 | 
			
		||||
The script 'exec.sh' adds the lib directory to the path. So, 
 | 
			
		||||
maxsat can find libz3.so.
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			@ -1,8 +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 gcc.
 | 
			
		||||
 | 
			
		||||
Use 'build.sh' to build the MaxSAT application using gcc. 
 | 
			
		||||
The script 'exec.sh' adds the lib directory to the path. So, 
 | 
			
		||||
maxsat can find libz3.dylib.
 | 
			
		||||
 | 
			
		||||
							
								
								
									
										21
									
								
								maxsat/README.txt
									
										
									
									
									
										Normal file
									
								
							
							
						
						
									
										21
									
								
								maxsat/README.txt
									
										
									
									
									
										Normal file
									
								
							| 
						 | 
				
			
			@ -0,0 +1,21 @@
 | 
			
		|||
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 Visual Studio (with Z3 source code release)
 | 
			
		||||
 | 
			
		||||
Use the maxsat.vcxproj project file.
 | 
			
		||||
 | 
			
		||||
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'.
 | 
			
		||||
| 
						 | 
				
			
			@ -1 +0,0 @@
 | 
			
		|||
gcc -fopenmp -o maxsat maxsat.c -I ../../include -L ../../lib -lz3
 | 
			
		||||
| 
						 | 
				
			
			@ -1 +0,0 @@
 | 
			
		|||
gcc -fopenmp -o maxsat maxsat.c -I ../../include -L ../../lib -lz3 
 | 
			
		||||
| 
						 | 
				
			
			@ -1 +0,0 @@
 | 
			
		|||
gcc -o maxsat.exe -I ../../include ../../bin/z3.dll maxsat.c
 | 
			
		||||
| 
						 | 
				
			
			@ -1,4 +0,0 @@
 | 
			
		|||
# Note: Z3 was built using C++, so libz3.a has C++ dependencies. 
 | 
			
		||||
#       You can use gcc to link the program, but you need tell it 
 | 
			
		||||
#       to link the C++ libraries
 | 
			
		||||
g++ -fopenmp -static -I../../include -L../../lib maxsat.c -lz3 -o maxsat
 | 
			
		||||
| 
						 | 
				
			
			@ -1,4 +0,0 @@
 | 
			
		|||
# Note: Z3 was built using C++, so libz3.a has C++ dependencies. 
 | 
			
		||||
#       You can use gcc to link the program, but you need tell it 
 | 
			
		||||
#       to link the C++ libraries
 | 
			
		||||
g++ -fopenmp  -I../../include maxsat.c ../../lib/libz3.a -o maxsat
 | 
			
		||||
							
								
								
									
										9
									
								
								maxsat/build.sh
									
										
									
									
									
										Executable file
									
								
							
							
						
						
									
										9
									
								
								maxsat/build.sh
									
										
									
									
									
										Executable file
									
								
							| 
						 | 
				
			
			@ -0,0 +1,9 @@
 | 
			
		|||
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
 | 
			
		||||
| 
						 | 
				
			
			@ -1,2 +0,0 @@
 | 
			
		|||
export LD_LIBRARY_PATH=../../lib:$LD_LIBRARY_PATH
 | 
			
		||||
./maxsat $1
 | 
			
		||||
| 
						 | 
				
			
			@ -1,2 +0,0 @@
 | 
			
		|||
export DYLD_LIBRARY_PATH=../../lib:$DYLD_LIBRARY_PATH
 | 
			
		||||
./maxsat $1
 | 
			
		||||
| 
						 | 
				
			
			@ -1,2 +0,0 @@
 | 
			
		|||
export PATH=../../bin:$PATH
 | 
			
		||||
./maxsat.exe $1
 | 
			
		||||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue