mirror of
				https://github.com/Z3Prover/z3
				synced 2025-11-04 05:19:11 +00:00 
			
		
		
		
	merged
This commit is contained in:
		
						commit
						0cf7396707
					
				
					 1 changed files with 38 additions and 7 deletions
				
			
		| 
						 | 
					@ -75,6 +75,8 @@ VER_BUILD=None
 | 
				
			||||||
VER_REVISION=None
 | 
					VER_REVISION=None
 | 
				
			||||||
PREFIX='/usr'
 | 
					PREFIX='/usr'
 | 
				
			||||||
GMP=False
 | 
					GMP=False
 | 
				
			||||||
 | 
					VS_PAR=False
 | 
				
			||||||
 | 
					VS_PAR_NUM=8
 | 
				
			||||||
 | 
					
 | 
				
			||||||
def is_windows():
 | 
					def is_windows():
 | 
				
			||||||
    return IS_WINDOWS
 | 
					    return IS_WINDOWS
 | 
				
			||||||
| 
						 | 
					@ -362,6 +364,8 @@ def display_help(exit_code):
 | 
				
			||||||
    if not IS_WINDOWS:
 | 
					    if not IS_WINDOWS:
 | 
				
			||||||
        print "  -p <dir>, --prefix=<dir>      installation prefix (default: %s)." % PREFIX
 | 
					        print "  -p <dir>, --prefix=<dir>      installation prefix (default: %s)." % PREFIX
 | 
				
			||||||
        print "  -y <dir>, --pydir=<dir>       installation prefix for Z3 python bindings (default: %s)." % PYTHON_PACKAGE_DIR
 | 
					        print "  -y <dir>, --pydir=<dir>       installation prefix for Z3 python bindings (default: %s)." % PYTHON_PACKAGE_DIR
 | 
				
			||||||
 | 
					    else:
 | 
				
			||||||
 | 
					        print "  --parallel=num                use cl option /MP with 'num' parallel processes"
 | 
				
			||||||
    print "  -b <sudir>, --build=<subdir>  subdirectory where Z3 will be built (default: build)."
 | 
					    print "  -b <sudir>, --build=<subdir>  subdirectory where Z3 will be built (default: build)."
 | 
				
			||||||
    print "  -d, --debug                   compile Z3 in debug mode."
 | 
					    print "  -d, --debug                   compile Z3 in debug mode."
 | 
				
			||||||
    print "  -t, --trace                   enable tracing in release mode."
 | 
					    print "  -t, --trace                   enable tracing in release mode."
 | 
				
			||||||
| 
						 | 
					@ -391,13 +395,13 @@ def display_help(exit_code):
 | 
				
			||||||
 | 
					
 | 
				
			||||||
# Parse configuration option for mk_make script
 | 
					# Parse configuration option for mk_make script
 | 
				
			||||||
def parse_options():
 | 
					def parse_options():
 | 
				
			||||||
    global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE
 | 
					    global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
 | 
				
			||||||
    global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP, PYTHON_PACKAGE_DIR
 | 
					    global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP, PYTHON_PACKAGE_DIR
 | 
				
			||||||
    try:
 | 
					    try:
 | 
				
			||||||
        options, remainder = getopt.gnu_getopt(sys.argv[1:], 
 | 
					        options, remainder = getopt.gnu_getopt(sys.argv[1:], 
 | 
				
			||||||
                                               'b:dsxhmcvtnp:gjy:', 
 | 
					                                               'b:dsxhmcvtnp:gjy:', 
 | 
				
			||||||
                                               ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
 | 
					                                               ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
 | 
				
			||||||
                                                'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'java', 'pydir='])
 | 
					                                                'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'java', 'pydir=', 'parallel='])
 | 
				
			||||||
    except:
 | 
					    except:
 | 
				
			||||||
        print "ERROR: Invalid command line option"
 | 
					        print "ERROR: Invalid command line option"
 | 
				
			||||||
        display_help(1)
 | 
					        display_help(1)
 | 
				
			||||||
| 
						 | 
					@ -429,8 +433,11 @@ def parse_options():
 | 
				
			||||||
            DOTNET_ENABLED = False
 | 
					            DOTNET_ENABLED = False
 | 
				
			||||||
        elif opt in ('--staticlib'):
 | 
					        elif opt in ('--staticlib'):
 | 
				
			||||||
            STATIC_LIB = True
 | 
					            STATIC_LIB = True
 | 
				
			||||||
        elif opt in ('-p', '--prefix'):
 | 
					        elif not IS_WINDOWS and opt in ('-p', '--prefix'):
 | 
				
			||||||
            PREFIX = arg
 | 
					            PREFIX = arg
 | 
				
			||||||
 | 
					        elif IS_WINDOWS and opt == '--parallel':
 | 
				
			||||||
 | 
					            VS_PAR = True
 | 
				
			||||||
 | 
					            VS_PAR_NUM = int(arg)
 | 
				
			||||||
        elif opt in ('-y', '--pydir'):
 | 
					        elif opt in ('-y', '--pydir'):
 | 
				
			||||||
            PYTHON_PACKAGE_DIR = arg
 | 
					            PYTHON_PACKAGE_DIR = arg
 | 
				
			||||||
            mk_dir(PYTHON_PACKAGE_DIR)
 | 
					            mk_dir(PYTHON_PACKAGE_DIR)
 | 
				
			||||||
| 
						 | 
					@ -656,6 +663,30 @@ class Component:
 | 
				
			||||||
            out.write(' -I%s' % get_component(dep).to_src_dir)
 | 
					            out.write(' -I%s' % get_component(dep).to_src_dir)
 | 
				
			||||||
        out.write('\n')
 | 
					        out.write('\n')
 | 
				
			||||||
        mk_dir(os.path.join(BUILD_DIR, self.build_dir))
 | 
					        mk_dir(os.path.join(BUILD_DIR, self.build_dir))
 | 
				
			||||||
 | 
					        if VS_PAR and IS_WINDOWS:
 | 
				
			||||||
 | 
					            cppfiles = get_cpp_files(self.src_dir)
 | 
				
			||||||
 | 
					            dependencies = set()
 | 
				
			||||||
 | 
					            for cppfile in cppfiles:
 | 
				
			||||||
 | 
					                dependencies.add(os.path.join(self.to_src_dir, cppfile))
 | 
				
			||||||
 | 
					                self.add_rule_for_each_include(out, cppfile)
 | 
				
			||||||
 | 
					                includes = extract_c_includes(os.path.join(self.src_dir, cppfile))
 | 
				
			||||||
 | 
					                for include in includes:
 | 
				
			||||||
 | 
					                    owner = self.find_file(include, cppfile)
 | 
				
			||||||
 | 
					                    dependencies.add('%s.node' % os.path.join(owner.build_dir, include))
 | 
				
			||||||
 | 
					            for cppfile in cppfiles:
 | 
				
			||||||
 | 
					                out.write('%s$(OBJ_EXT) ' % os.path.join(self.build_dir, os.path.splitext(cppfile)[0]))
 | 
				
			||||||
 | 
					            out.write(': ')
 | 
				
			||||||
 | 
					            for dep in dependencies:
 | 
				
			||||||
 | 
					                out.write(dep)
 | 
				
			||||||
 | 
					                out.write(' ')
 | 
				
			||||||
 | 
					            out.write('\n')
 | 
				
			||||||
 | 
					            out.write('\t@$(CXX) $(CXXFLAGS) /MP%s $(%s)' % (VS_PAR_NUM, include_defs))
 | 
				
			||||||
 | 
					            for cppfile in cppfiles:
 | 
				
			||||||
 | 
					                out.write(' ')
 | 
				
			||||||
 | 
					                out.write(os.path.join(self.to_src_dir, cppfile))
 | 
				
			||||||
 | 
					            out.write('\n')
 | 
				
			||||||
 | 
					            out.write('\tmove *.obj %s\n' % self.build_dir)
 | 
				
			||||||
 | 
					        else:
 | 
				
			||||||
            for cppfile in get_cpp_files(self.src_dir):
 | 
					            for cppfile in get_cpp_files(self.src_dir):
 | 
				
			||||||
                self.add_cpp_rules(out, include_defs, cppfile)
 | 
					                self.add_cpp_rules(out, include_defs, cppfile)
 | 
				
			||||||
 | 
					
 | 
				
			||||||
| 
						 | 
					@ -1253,12 +1284,12 @@ def mk_config():
 | 
				
			||||||
                'SLINK_FLAGS=/nologo /LDd\n')
 | 
					                'SLINK_FLAGS=/nologo /LDd\n')
 | 
				
			||||||
            if not VS_X64:
 | 
					            if not VS_X64:
 | 
				
			||||||
                config.write(
 | 
					                config.write(
 | 
				
			||||||
                    'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n'
 | 
					                    'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n'
 | 
				
			||||||
                    'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
 | 
					                    'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
 | 
				
			||||||
                    'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
 | 
					                    'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
 | 
				
			||||||
            else:
 | 
					            else:
 | 
				
			||||||
                config.write(
 | 
					                config.write(
 | 
				
			||||||
                    'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n'
 | 
					                    'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n'
 | 
				
			||||||
                    'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
 | 
					                    'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
 | 
				
			||||||
                    'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
 | 
					                    'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
 | 
				
			||||||
        else:
 | 
					        else:
 | 
				
			||||||
| 
						 | 
					
 | 
				
			||||||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue