3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00

checkpoint

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-23 14:41:26 -07:00
parent c4898a67e3
commit 236a32c3d4
10 changed files with 256 additions and 965 deletions

View file

@ -0,0 +1,14 @@
CXX=@CXX@
CXXFLAGS=@CPPFLAGS@ @CXXFLAGS@ -c -g -Wall -fopenmp -msse -msse2 -mfpmath=sse -fPIC
CXX_OUT_FLAG=-o
OBJ_EXT=.o
LIB_EXT=.a
AR=@AR@
AR_FLAGS=rcs
AR_OUTFLAG=
EXE_EXT=
LINK=@CXX@
LINK_FLAGS=-lpthread -fopenmp
LINK_OUT_FLAG=-o

View file

@ -0,0 +1,14 @@
CXX=@CXX@
CXXFLAGS=@CPPFLAGS@ @CXXFLAGS@ -c -O3 -fomit-frame-pointer -Wall -fopenmp -msse -msse2 -mfpmath=sse -fPIC
CXX_OUT_FLAG=-o
OBJ_EXT=.o
LIB_EXT=.a
AR=@AR@
AR_FLAGS=rcs
AR_OUTFLAG=
EXE_EXT=
LINK=@CXX@
LINK_FLAGS=-lpthread -fopenmp
LINK_OUT_FLAG=-o

View file

@ -11,26 +11,6 @@ import os
import sets
from mk_exception import *
# Return a list containing a file names included using '#include' in
# the given C/C++ file named fname.
def extract_c_includes(fname):
result = []
# We look for well behaved #include directives
std_inc_pat = re.compile("[ \t]*#include[ \t]*\"(.*)\"[ \t]*")
system_inc_pat = re.compile("[ \t]*#include[ \t]*\<.*\>[ \t]*")
# We should generate and error for any occurrence of #include that does not match the previous pattern.
non_std_inc_pat = re.compile(".*#include.*")
f = open(fname, 'r')
linenum = 1
for line in f:
m1 = std_inc_pat.match(line)
if m1:
result.append(m1.group(1))
elif not system_inc_pat.match(line) and non_std_inc_pat.match(line):
raise MKException("Invalid #include directive at '%s':%s" % (fname, line))
linenum = linenum + 1
return result
# Return src_dir/path/fname
def mk_full_fname(src_dir, path, fname):

View file

@ -9,7 +9,7 @@
import os
import glob
import sets
from dependencies import *
import re
from mk_exception import *
BUILD_DIR='build'
@ -27,6 +27,28 @@ SHOW_CPPS = True
LIB_KIND = 0
EXE_KIND = 1
# Return a list containing a file names included using '#include' in
# the given C/C++ file named fname.
def extract_c_includes(fname):
result = []
# We look for well behaved #include directives
std_inc_pat = re.compile("[ \t]*#include[ \t]*\"(.*)\"[ \t]*")
system_inc_pat = re.compile("[ \t]*#include[ \t]*\<.*\>[ \t]*")
# We should generate and error for any occurrence of #include that does not match the previous pattern.
non_std_inc_pat = re.compile(".*#include.*")
f = open(fname, 'r')
linenum = 1
for line in f:
m1 = std_inc_pat.match(line)
if m1:
result.append(m1.group(1))
elif not system_inc_pat.match(line) and non_std_inc_pat.match(line):
raise MKException("Invalid #include directive at '%s':%s" % (fname, line))
linenum = linenum + 1
return result
# Given a path dir1/subdir2/subdir3 returns ../../..
def reverse_path(p):
l = p.split('/')

20
scripts/update-version.sh Normal file
View file

@ -0,0 +1,20 @@
#!/bin/sh
#
# Update Z3 version
#
if [ $# -ne 1 ]; then
echo "Usage: update-version.sh MAJOR.MINOR.BUILD.REVISION"
fi
sd edit lib/version.h
sd edit release.cmd
sd edit shell/shell.rc
sd edit dll/dll.rc
sd edit shell/main.cpp
sd edit Z3Inspector/Properties/AssemblyInfo.cs
sd edit Microsoft.Z3/Properties/AssemblyInfo.cs
sd edit Microsoft.Z3V3/AssemblyInfo.cpp
scripts/perl scripts/update-version.pl "$1"

11
scripts/update_api.txt Normal file
View file

@ -0,0 +1,11 @@
Instructions for updating external Z3 API
-----------------------------------------
The python "macros": def_Type() and def_API() are used to add new types and function definitions to the Z3 API.
The .h files listed at update_api.py contain these definitions.
See lib\z3_api.py for many examples.
To generate bindings and the API logging infrastructure, the following command must be used:
python update_api.py