mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 05:18:44 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
This commit is contained in:
Nikolaj Bjorner
commit
6a18015622
51
.gitignore
vendored
Normal file
51
.gitignore
vendored
Normal file
|
|
@ -0,0 +1,51 @@
|
|||
*~
|
||||
*.pyc
|
||||
.z3-trace
|
||||
# OCaml generated files
|
||||
*.a
|
||||
*.cma
|
||||
*.cmi
|
||||
*.cmxa
|
||||
ocamlz3
|
||||
# Emacs temp files
|
||||
\#*\#
|
||||
# Directories with generated code and documentation
|
||||
build/*
|
||||
build-dist/*
|
||||
dist/*
|
||||
doc/html/*
|
||||
# GTAGS generated files
|
||||
src/GPATH
|
||||
src/GRTAGS
|
||||
src/GSYMS
|
||||
src/GTAGS
|
||||
src/HTML/*
|
||||
# CSCOPE files
|
||||
src/cscope.in.out
|
||||
src/cscope.out
|
||||
src/cscope.po.out
|
||||
ncscope.out
|
||||
# CEDET files
|
||||
.cproject
|
||||
.project
|
||||
# Commonly used directories for code
|
||||
bld_dbg/*
|
||||
bld_rel/*
|
||||
# Auto generated files.
|
||||
config.log
|
||||
config.status
|
||||
configure
|
||||
install_tactic.cpp
|
||||
mem_initializer.cpp
|
||||
scripts/config-debug.mk
|
||||
scripts/config-release.mk
|
||||
src/api/api_commands.cpp
|
||||
src/api/api_log_macros.h
|
||||
src/api/api_log_macros.cpp
|
||||
src/api/dll/api_dll.def
|
||||
src/api/dotnet/Enumerations.cs
|
||||
src/api/dotnet/Native.cs
|
||||
src/api/python/z3consts.py
|
||||
src/api/python/z3core.py
|
||||
src/ast/pattern/database.h
|
||||
src/util/version.h
|
||||
2
README
2
README
|
|
@ -12,7 +12,7 @@ Z3 can be built using Visual Studio Command Prompt and make/g++.
|
|||
2) Building Z3 using make/g++ and Python
|
||||
Execute:
|
||||
|
||||
autconf
|
||||
autoconf
|
||||
./configure
|
||||
python scripts/mk_make.py
|
||||
cd build
|
||||
|
|
|
|||
|
|
@ -7,6 +7,11 @@ Version 4.3.2
|
|||
|
||||
- Added support for FreeBSD. Z3 can be compiled on FreeBSD using g++.
|
||||
|
||||
- Reverted to `(set-option :global-decls false)` as the default. In Z3 4.3.0 and Z3 4.3.1, this option was set to true.
|
||||
Thanks to Julien Henry for reporting this problem.
|
||||
|
||||
- Added `doc` directory and scripts for automatically generating the API documentation.
|
||||
|
||||
Version 4.3.1
|
||||
=============
|
||||
|
||||
|
|
|
|||
11
doc/README
Normal file
11
doc/README
Normal file
|
|
@ -0,0 +1,11 @@
|
|||
API documentation
|
||||
-----------------
|
||||
|
||||
To generate the API documentation for the C, .NET and Python APIs, we must execute
|
||||
|
||||
python mk_doc.py
|
||||
|
||||
We must have doxygen installed in our system.
|
||||
|
||||
The documentation will be stored in the subdirectory './html'.
|
||||
The main file is './html/index.html'
|
||||
4
doc/footer.html
Normal file
4
doc/footer.html
Normal file
|
|
@ -0,0 +1,4 @@
|
|||
<div id="nav">
|
||||
</div>
|
||||
</body>
|
||||
</html>
|
||||
23
doc/header.html
Normal file
23
doc/header.html
Normal file
|
|
@ -0,0 +1,23 @@
|
|||
<HTML>
|
||||
<HEAD>
|
||||
<meta name="author" content="Leonardo de Moura" />
|
||||
<meta name="author" content="Nikolaj Bjorner" />
|
||||
<meta name="author" content="Christoph Wintersteiger" />
|
||||
<meta name="description" content="Z3: theorem prover" />
|
||||
<meta name="keywords" content="decision procedure, theorem prover, SMT-LIB, SMTLIB, SMT LIB, SMT Solver, SMTCOMP, SMT-COMP, SAT solver, formal methods, constraint solver, software verification, hardware verification" />
|
||||
<TITLE>Z3: Theorem Prover</TITLE>
|
||||
<LINK HREF="z3.css" REL="stylesheet" TYPE="text/css">
|
||||
<LINK href="tabs.css" rel="stylesheet" type="text/css">
|
||||
</HEAD>
|
||||
<BODY BGCOLOR="#FFFFFF">
|
||||
|
||||
<table>
|
||||
<tr>
|
||||
<th style="width:120px"><a style="border=0px" class="el" href="http://z3.codeplex.com"><img border="0" src="z3.png" alt="Z3" /></a></th>
|
||||
<th style="width:100%">
|
||||
<div id="nav">
|
||||
</div>
|
||||
</th>
|
||||
</tr>
|
||||
</table>
|
||||
|
||||
47
doc/mk_doc.py
Normal file
47
doc/mk_doc.py
Normal file
|
|
@ -0,0 +1,47 @@
|
|||
import os
|
||||
import shutil
|
||||
import re
|
||||
import pydoc
|
||||
import sys
|
||||
import subprocess
|
||||
|
||||
def mk_dir(d):
|
||||
if not os.path.exists(d):
|
||||
os.makedirs(d)
|
||||
|
||||
# Eliminate def_API and extra_API directives from file 'inf'.
|
||||
# The result is stored in 'outf'.
|
||||
def cleanup_API(inf, outf):
|
||||
pat1 = re.compile(".*def_API.*")
|
||||
pat2 = re.compile(".*extra_API.*")
|
||||
_inf = open(inf, 'r')
|
||||
_outf = open(outf, 'w')
|
||||
for line in _inf:
|
||||
if not pat1.match(line) and not pat2.match(line):
|
||||
_outf.write(line)
|
||||
|
||||
try:
|
||||
mk_dir('html')
|
||||
cleanup_API('../src/api/z3_api.h', 'z3_api.h')
|
||||
print "Removed annotations from z3_api.h."
|
||||
DEVNULL = open(os.devnull, 'wb')
|
||||
try:
|
||||
subprocess.call(['doxygen', 'z3.dox'], stdout=DEVNULL, stderr=DEVNULL)
|
||||
except:
|
||||
print "ERROR: failed to execute 'doxygen', make sure doxygen (http://www.doxygen.org) is available in your system."
|
||||
exit(1)
|
||||
print "Generated C and .NET API documentation."
|
||||
os.remove('z3_api.h')
|
||||
print "Removed temporary file z3_api.h."
|
||||
shutil.copy('z3.css', 'html/z3.css')
|
||||
print "Copied z3.css."
|
||||
shutil.copy('z3.png', 'html/z3.png')
|
||||
print "Copied z3.png."
|
||||
sys.path.append('../src/api/python')
|
||||
pydoc.writedoc('z3')
|
||||
shutil.move('z3.html', 'html/z3.html')
|
||||
print "Generated Python documentation."
|
||||
print "Documentation was successfully generated at subdirectory './html'."
|
||||
except:
|
||||
print "ERROR: failed to generate documentation"
|
||||
exit(1)
|
||||
4
doc/update_website.cmd
Normal file
4
doc/update_website.cmd
Normal file
|
|
@ -0,0 +1,4 @@
|
|||
REM Script for updating the website containing the Z3 API documentation.
|
||||
REM You must be inside the Microsoft network to execute this script, and
|
||||
REM robocopy must be in your PATH.
|
||||
robocopy /S html \\research\root\web\external\en-us\UM\redmond\projects\z3
|
||||
17
doc/website.dox
Normal file
17
doc/website.dox
Normal file
|
|
@ -0,0 +1,17 @@
|
|||
/**
|
||||
\mainpage An Efficient Theorem Prover
|
||||
|
||||
Z3 is a high-performance theorem prover being developed at <a class="el"
|
||||
href="http://research.microsoft.com">Microsoft Research</a>.
|
||||
|
||||
<b>The Z3 website moved to <a class="el" href="http://z3.codeplex.com">z3.codeplex.com</a>.</b>
|
||||
|
||||
The old Z3 website can be found <a class="el" href="http://research.microsoft.com/en-us/um/redmond/projects/z3/old/index.html">here</a>.
|
||||
|
||||
This website hosts the automatically generated documentation for the Z3 APIs.
|
||||
|
||||
- \ref capi
|
||||
- <a class="el" href="class_microsoft_1_1_z3_1_1_context.html">.NET API</a>
|
||||
- <a class="el" href="z3.html">Python API</a>
|
||||
- Try Z3 online at <a href="http://rise4fun.com/z3py">RiSE4Fun</a> using <a href="http://rise4fun.com/z3py">Python</a> or <a href="http://rise4fun.com/z3">SMT 2.0</a>.
|
||||
*/
|
||||
934
doc/z3.css
Normal file
934
doc/z3.css
Normal file
|
|
@ -0,0 +1,934 @@
|
|||
|
||||
/* Section Start for new text handling */
|
||||
.PSubText
|
||||
{
|
||||
FONT-SIZE: 8pt;
|
||||
COLOR: #555555;
|
||||
}
|
||||
.LeftJustifyBullet
|
||||
{
|
||||
FONT-SIZE: 10pt;
|
||||
margin-left:-24px;
|
||||
}
|
||||
/* Section End for new text handling */
|
||||
|
||||
/* Section Start for text handling based on Rob Gruen's layout for the Download Details page */
|
||||
A:hover
|
||||
{
|
||||
TEXT-DECORATION: underline
|
||||
}
|
||||
A
|
||||
{
|
||||
TEXT-DECORATION: none;
|
||||
COLOR: #333399;
|
||||
}
|
||||
LI
|
||||
{
|
||||
FONT-SIZE: 10pt;
|
||||
COLOR: #555555;
|
||||
margin-bottom:10px;
|
||||
margin-left: -3px;
|
||||
}
|
||||
LI LI
|
||||
{
|
||||
FONT-SIZE: 10pt;
|
||||
COLOR: #555555;
|
||||
margin-bottom:10px;
|
||||
margin-left: -3px;
|
||||
}
|
||||
BODY
|
||||
{
|
||||
margin-right: 20px;
|
||||
margin-left: 20px;
|
||||
COLOR: #555555;
|
||||
FONT-FAMILY: Verdana, Arial, Helvetica, sans-serif;
|
||||
FONT-SIZE: 10pt;
|
||||
}
|
||||
P
|
||||
{
|
||||
FONT-SIZE: 10pt;
|
||||
COLOR: #555555;
|
||||
}
|
||||
.Z3Title
|
||||
{
|
||||
FONT-SIZE: 18pt;
|
||||
COLOR: #1A41A8;
|
||||
margin-bottom:-10px;
|
||||
}
|
||||
.PageTitle
|
||||
{
|
||||
FONT-SIZE: 12pt;
|
||||
COLOR: #333333;
|
||||
margin-bottom:-10px;
|
||||
}
|
||||
.BlobTitle
|
||||
{
|
||||
FONT-SIZE: 12pt;
|
||||
COLOR: #333333;
|
||||
LINE-HEIGHT: 100%;
|
||||
margin-bottom:-10px;
|
||||
}
|
||||
.Heading1
|
||||
{
|
||||
FONT-SIZE: 10pt;
|
||||
COLOR: #2A51B8;
|
||||
margin-bottom:-10px;
|
||||
|
||||
}
|
||||
.Heading2
|
||||
{
|
||||
FONT-WEIGHT: bold;
|
||||
FONT-SIZE: 10pt;
|
||||
COLOR: #555555;
|
||||
margin-bottom:-10px;
|
||||
}
|
||||
.Heading3
|
||||
{
|
||||
FONT-SIZE: 10pt;
|
||||
COLOR: #2A51B8;
|
||||
margin-bottom:-10px;
|
||||
}
|
||||
.title
|
||||
{
|
||||
font-size: 18pt;
|
||||
color: #1A41A8;
|
||||
margin-bottom:-10px;
|
||||
line-height: 35pt
|
||||
}
|
||||
.quote
|
||||
{
|
||||
FONT-FAMILY: Georgia, Times, Times New Roman, serif;
|
||||
FONT-STYLE: italic;
|
||||
FONT-SIZE: 20pt;
|
||||
COLOR: #2A51B8;
|
||||
}
|
||||
.attribution
|
||||
{
|
||||
FONT-SIZE: 8pt;
|
||||
COLOR: #555555;
|
||||
}
|
||||
.quickinfo
|
||||
{
|
||||
FONT-WEIGHT: bold;
|
||||
FONT-SIZE: 13pt;
|
||||
MARGIN-LEFT: 12px;
|
||||
COLOR: #2A51B8;
|
||||
}
|
||||
.quickinfo_header
|
||||
{
|
||||
font-weight: bold;
|
||||
color: #555555;
|
||||
margin-left: 25px;
|
||||
}
|
||||
hr
|
||||
{
|
||||
width: 100%;
|
||||
margin-top: 10px;
|
||||
margin-bottom: 10px;
|
||||
color: #cccccc;
|
||||
}
|
||||
|
||||
.RHPSectionHeader
|
||||
{
|
||||
font-size: 10pt;
|
||||
margin-left: 20px;
|
||||
color: #2A51B8;
|
||||
display: block;
|
||||
}
|
||||
.RHPNav
|
||||
{
|
||||
FONT-SIZE: 10pt;
|
||||
MARGIN-TOP: 6px;
|
||||
COLOR: #333333;
|
||||
}
|
||||
.author
|
||||
{
|
||||
FONT-SIZE: 8pt;
|
||||
COLOR: #555555;
|
||||
}
|
||||
.lastupdated
|
||||
{
|
||||
FONT-SIZE: 8pt;
|
||||
COLOR: #555555;
|
||||
}
|
||||
/* Section End for text handling based on Rob Gruen's layout for the Download Details page */
|
||||
|
||||
/* Section Start for text handling based on rmcstyle.css */
|
||||
.title_2ndLvl
|
||||
{
|
||||
font-family: tahoma;
|
||||
font-size: 120%;
|
||||
color: #FFFFFF;
|
||||
padding-left: 5px;
|
||||
}
|
||||
.VR
|
||||
{
|
||||
background-color: #cccccc;
|
||||
width: 1px;
|
||||
margin-top: -24;
|
||||
}
|
||||
.link1
|
||||
{
|
||||
font-size:70%;
|
||||
font-family: verdana;
|
||||
}
|
||||
.link2
|
||||
{
|
||||
font-size: 70%;
|
||||
font-family:Verdana;
|
||||
font-style:italic;
|
||||
}
|
||||
.link3
|
||||
{
|
||||
font-style: italic;
|
||||
font-family: Verdana;
|
||||
color: #000000;
|
||||
font-weight: bold;
|
||||
}
|
||||
.link4
|
||||
{
|
||||
font: italic 70% Verdana;
|
||||
color: #000000;
|
||||
text-decoration: none;
|
||||
}
|
||||
.link5
|
||||
{
|
||||
font: 70% Verdana;
|
||||
color: #003399;
|
||||
text-decoration: none;
|
||||
}
|
||||
.link6
|
||||
{
|
||||
font: 70% verdana;
|
||||
color: #003399;
|
||||
}
|
||||
.ReadMore
|
||||
{
|
||||
text-decoration:none;
|
||||
}
|
||||
/* .text1
|
||||
{
|
||||
font: 70% Verdana;
|
||||
} */
|
||||
.text2
|
||||
{
|
||||
padding-bottom: 10px;
|
||||
font: 70% Verdana;
|
||||
}
|
||||
.text3
|
||||
{
|
||||
font-size: 120%;
|
||||
font-family:Verdana;
|
||||
color: #000000;
|
||||
}
|
||||
.text3_w_padding
|
||||
{
|
||||
font: 120% Verdana;
|
||||
color: #000000;
|
||||
padding-left:20px;
|
||||
}
|
||||
.text4
|
||||
{
|
||||
font-weight: bold;
|
||||
font-size: 70%;
|
||||
font-family: Verdana;
|
||||
color: #000000;
|
||||
}
|
||||
.text5
|
||||
{
|
||||
padding-left: 5px;
|
||||
font-weight: bold;
|
||||
font-size: 70%;
|
||||
font-family: Verdana;
|
||||
color: #ffffff;
|
||||
}
|
||||
.text6
|
||||
{
|
||||
font: 70%;
|
||||
font-family: verdana;
|
||||
}
|
||||
.newsTitle
|
||||
{
|
||||
font-family: tahoma;
|
||||
font-size: 120%;
|
||||
color: #CCCCCC;
|
||||
}
|
||||
.areaTitle
|
||||
{
|
||||
font-family: tahoma;
|
||||
font-size: 120%;
|
||||
color: #FFFFFF;
|
||||
}
|
||||
.newsContentTitle
|
||||
{
|
||||
font-family: tahoma;
|
||||
font-size: 120%;
|
||||
color: #FFFFFF;
|
||||
}
|
||||
.areaContentTitle
|
||||
{
|
||||
font-family: verdana;
|
||||
font-size: 140%;
|
||||
color: #000000;
|
||||
}
|
||||
.areaContentTitle_w_pad
|
||||
{
|
||||
font-family: verdana;
|
||||
font-size: 140%;
|
||||
color: #000000;
|
||||
padding-left: 20px;
|
||||
padding-top: 20px;
|
||||
}
|
||||
.newsArchiveTitle
|
||||
{
|
||||
font-family: verdana;
|
||||
font-size: 150%;
|
||||
color: #000000;
|
||||
}
|
||||
.FeatureStoryTitle
|
||||
{
|
||||
font-family: verdana;
|
||||
font-size: 18 pt;
|
||||
COLOR: #2A51B8;
|
||||
margin-bottom:-15px;
|
||||
}
|
||||
.FeatureStoryDate
|
||||
{
|
||||
font-family: Verdana;
|
||||
font-size: 8 pt;
|
||||
color: #555555;
|
||||
|
||||
}
|
||||
.FeatureStoryByLine
|
||||
{
|
||||
font-family: verdana;
|
||||
font-size: 10 pt;
|
||||
color: #555555;
|
||||
margin-bottom:-15px;
|
||||
font-weight: bold;
|
||||
}
|
||||
.SideBarLink
|
||||
{
|
||||
font-family: verdana;
|
||||
font-size: 80%;
|
||||
color: #000000;
|
||||
}
|
||||
.newsArchiveSubTitle
|
||||
{
|
||||
font-family: verdana;
|
||||
font-size: 118%;
|
||||
color: #666666;
|
||||
}
|
||||
.newsArchiveYear
|
||||
{
|
||||
font: bold 80% Verdana;
|
||||
color: #000000;
|
||||
border-bottom: #cccccc 1px solid;
|
||||
border-top: #cccccc 1px solid;
|
||||
}
|
||||
.newsHeadlineTitle
|
||||
{
|
||||
font-family: verdana;
|
||||
font-size: 140%;
|
||||
color: #000000;
|
||||
}
|
||||
.newsPublicationDate
|
||||
{
|
||||
font-family: Verdana;
|
||||
font-size: 60%;
|
||||
color: #000000;
|
||||
font-weight: bold;
|
||||
}
|
||||
.newsPublicationSource
|
||||
{
|
||||
font-family: Verdana;
|
||||
font-size: 60%;
|
||||
color: #000000;
|
||||
font-weight: bold;
|
||||
}
|
||||
|
||||
|
||||
h1 {font-size: 16pt; color: #2A51B8; margin: 30px 0px; font-weight: normal;}
|
||||
|
||||
.anchor { color: #2A51B8; }
|
||||
|
||||
h2 {font-size: 14pt; color: #2A51B8; margin: 10px 0px; font-weight: normal;}
|
||||
|
||||
h3 {font-size: 12pt; color: #2A51B8; margin: 10px 0px; font-weight: normal;}
|
||||
|
||||
h4
|
||||
{
|
||||
color: #808080;
|
||||
font-family: Tahoma;
|
||||
font-size: 90%;
|
||||
margin-bottom: -10px
|
||||
}
|
||||
|
||||
.TitleHeader {font-family: tahoma; font-weight: bold; font-size: 110%; color: #000000;}
|
||||
|
||||
P P
|
||||
{
|
||||
font-size: 100%;
|
||||
}
|
||||
.groupheading
|
||||
{
|
||||
padding-left: 20px;
|
||||
padding-top: 40px;
|
||||
padding-bottom: 10px;
|
||||
font-size: 1.4em;
|
||||
color: #0065CF;
|
||||
font-family:verdana;
|
||||
}
|
||||
.GroupTitle
|
||||
{
|
||||
padding-left: 20px;
|
||||
padding-top: 20px;
|
||||
padding-bottom: 10px;
|
||||
font-size: 1.4em;
|
||||
color: #0065CF;
|
||||
}
|
||||
LI LI
|
||||
{
|
||||
font-size: 100%;
|
||||
}
|
||||
LI A
|
||||
{
|
||||
font-size: 100%;
|
||||
}
|
||||
/* Section End for text handling based on rmcstyle.css */
|
||||
|
||||
/* Section Start for text handling based on new_style.css */
|
||||
.O
|
||||
{
|
||||
color:white;
|
||||
font-size:149%;
|
||||
}
|
||||
ul
|
||||
{
|
||||
color: #808080;
|
||||
list-style-type:square
|
||||
}
|
||||
|
||||
|
||||
/* Section End for text handling based on new_style.css */
|
||||
|
||||
/* Section Start for page layout based on Rob Gruen's downloads Page */
|
||||
.bodymargin
|
||||
{
|
||||
margin-left: 20px;
|
||||
position: relative;
|
||||
}
|
||||
/* Section Start for page layout based on Rob Gruen's downloads Page */
|
||||
|
||||
/* Section Start for page layout based on Rob Gruen's downloads Page */
|
||||
.quickinfo_tbl
|
||||
{
|
||||
color: #555555;
|
||||
BORDER-RIGHT: black 1px solid;
|
||||
BORDER-TOP: black 1px solid;
|
||||
BORDER-LEFT: black 1px solid;
|
||||
WIDTH: 560px;
|
||||
BORDER-BOTTOM: black 1px solid;
|
||||
HEIGHT: 164px;
|
||||
}
|
||||
/* Section Start for page layout based on Rob Gruen's downloads Page */
|
||||
|
||||
/* Section Start for page layout based on rmcstyle.css */
|
||||
.linkbox
|
||||
{
|
||||
margin-left: 20px;
|
||||
margin-right: 30px;
|
||||
margin-bottom: 20px;
|
||||
padding-bottom: 10px;
|
||||
width: 175px;
|
||||
float: right;
|
||||
background: #ffffff;
|
||||
border-bottom: #CCCCCC 1px solid;
|
||||
}
|
||||
.outlineDivTitle
|
||||
{
|
||||
border-top: #CCCCCC 1px solid;
|
||||
background-color: #FFFFFF;
|
||||
color: #CCCCCC;
|
||||
padding-left: 15px;
|
||||
padding-bottom: 12px;
|
||||
padding-top: 12px;
|
||||
font: bold 70% Verdana;
|
||||
color: #2A51B8;
|
||||
}
|
||||
.outlineDiv
|
||||
{
|
||||
padding-left: 20px;
|
||||
background-image: URL(/images/orangesquare.gif);
|
||||
background-repeat: no-repeat;
|
||||
background-position: 6 8;
|
||||
font: 70% verdana;
|
||||
color: #555555;
|
||||
line-height: 200%;
|
||||
}
|
||||
/* Section End for page layout based on rmcstyle.css */
|
||||
|
||||
/* Section Start for page layout based on new_style.css */
|
||||
.QL_border
|
||||
{
|
||||
border-right: #555555 1px solid;
|
||||
background: #ffffff;
|
||||
border-left: #555555 1px solid;
|
||||
border-bottom: #555555 1px solid;
|
||||
}
|
||||
|
||||
/* Section End for page layout based on new_style.css */
|
||||
|
||||
|
||||
/* Begin Versal-specific styles */
|
||||
|
||||
|
||||
.imageAlignLeft
|
||||
{
|
||||
background-color: #ffffff;
|
||||
margin: 0px 10px 10px 10px;
|
||||
color: #666666;
|
||||
font-family: Verdana, Arial, Helvetica, sans-serif;
|
||||
font-size: 70%;
|
||||
font-weight:normal;
|
||||
text-align: left;
|
||||
}
|
||||
.imageAlignRight
|
||||
{
|
||||
background-color: #ffffff;
|
||||
margin: 0px 10px 10px 10px;
|
||||
color: #666666;
|
||||
font-family: Verdana, Arial, Helvetica, sans-serif;
|
||||
font-size: 70%;
|
||||
font-weight:normal;
|
||||
text-align: left;
|
||||
}
|
||||
.imageFloatLeft
|
||||
{
|
||||
float: left;
|
||||
background-color: #ffffff;
|
||||
margin: 0px 10px 10px 0px;
|
||||
color: #666666;
|
||||
font-family: Verdana, Arial, Helvetica, sans-serif;
|
||||
font-size: 70%;
|
||||
font-weight:normal;
|
||||
text-align: left;
|
||||
}
|
||||
.imageFloatRight
|
||||
{
|
||||
float: right;
|
||||
background-color: #ffffff;
|
||||
margin: 0px 10px 10px 10px;
|
||||
color: #666666;
|
||||
font-family: Verdana, Arial, Helvetica, sans-serif;
|
||||
font-size: 70%;
|
||||
font-weight:normal;
|
||||
text-align: left;
|
||||
}
|
||||
.imageCaptionText
|
||||
{
|
||||
color:#666666;
|
||||
font-family:Verdana, Arial, Helvetica, sans-serif;
|
||||
font-size:xx-small;
|
||||
font-weight:normal;
|
||||
}
|
||||
.tableBorder
|
||||
{
|
||||
border-top: solid 1px #C0C0C0;
|
||||
border-left: solid 1px #C0C0C0;
|
||||
font-family: Verdana, Arial, Helvetica, sans-serif;
|
||||
font-size: 100%;
|
||||
margin-top: 1em;
|
||||
}
|
||||
.tableNoBorder
|
||||
{
|
||||
font-family: Verdana, Arial, Helvetica, sans-serif;
|
||||
font-size: 100%;
|
||||
margin-top: 1em;
|
||||
}
|
||||
.tableBorderLabel
|
||||
{
|
||||
border-top: solid 1px #C0C0C0;
|
||||
border-left: solid 1px #C0C0C0;
|
||||
font-family: Verdana, Arial, Helvetica, sans-serif;
|
||||
font-size: 100%;
|
||||
font-weight: bold;
|
||||
background: #999999;
|
||||
color: #FFFFFF;
|
||||
}
|
||||
.tableNoBorderLabel
|
||||
{
|
||||
font-family: Verdana, Arial, Helvetica, sans-serif;
|
||||
font-size: 100%;
|
||||
font-weight: bold;
|
||||
background: #999999;
|
||||
color: #FFFFFF;
|
||||
}
|
||||
.tableBorderHeader
|
||||
{
|
||||
background: #CCCCCC;
|
||||
color: #000000;
|
||||
}
|
||||
.tableBorderHeader td
|
||||
{
|
||||
font-family: Verdana, Arial, Helvetica, sans-serif;
|
||||
font-size: 100%;
|
||||
font-weight: bold;
|
||||
border-top: solid 1px #CCCCCC;
|
||||
border-left: solid 1px #CCCCCC;
|
||||
}
|
||||
.tableNoBorderHeader
|
||||
{
|
||||
background: #CCCCCC;
|
||||
color: #000000;
|
||||
}
|
||||
.tableNoBorderHeader td
|
||||
{
|
||||
font-family: Verdana, Arial, Helvetica, sans-serif;
|
||||
font-size: 100%;
|
||||
font-weight: bold;
|
||||
}
|
||||
.tableBorderSection
|
||||
{
|
||||
background: #DDDDDD;
|
||||
}
|
||||
.tableBorderSection td
|
||||
{
|
||||
border-top: solid 1px #CCCCCC;
|
||||
border-left: solid 1px #CCCCCC;
|
||||
font-family: Verdana, Arial, Helvetica, sans-serif;
|
||||
font-size: 100%;
|
||||
font-weight: bold;
|
||||
}
|
||||
.tableNoBorderSection
|
||||
{
|
||||
background: #DDDDDD;
|
||||
}
|
||||
.tableNoBorderSection td
|
||||
{
|
||||
font-family: Verdana, Arial, Helvetica, sans-serif;
|
||||
font-size: 100%;
|
||||
font-weight: bold;
|
||||
}
|
||||
.tableBorderRecord td
|
||||
{
|
||||
border-bottom: solid 1px #CCCCCC;
|
||||
border-right: solid 1px #CCCCCC;
|
||||
}
|
||||
.tableBorderRecord td td
|
||||
{
|
||||
border-width: 0px;
|
||||
}
|
||||
.tableNoBorderRecord td
|
||||
{
|
||||
}
|
||||
.tableNoBorderRecord td td
|
||||
{
|
||||
}
|
||||
.tableFootnotes
|
||||
{
|
||||
margin-top: 7px;
|
||||
margin-left: 5px;
|
||||
}
|
||||
.dataTableBottomMargin
|
||||
{
|
||||
height: 1px;
|
||||
overflow: hidden;
|
||||
margin-bottom: 18px;
|
||||
}
|
||||
|
||||
.footnote
|
||||
{
|
||||
font: 70% Arial;
|
||||
position: relative;
|
||||
top: -0.2em;
|
||||
}
|
||||
|
||||
.footnoteText
|
||||
{
|
||||
font-family: Verdana, Arial, Helvetica, sans-serif;
|
||||
font-size: 65%;
|
||||
}
|
||||
|
||||
.footnotes
|
||||
{
|
||||
margin-top: 11px;
|
||||
margin-bottom: 36px;
|
||||
}
|
||||
|
||||
pre.codeSample
|
||||
{
|
||||
background: #DDDDDD;
|
||||
font-family: Lucida Console, Courier New;
|
||||
font-size: 70%;
|
||||
padding: 10px 15px 10px 25px;
|
||||
margin-bottom: 1em;
|
||||
}
|
||||
|
||||
span.codeSample
|
||||
{
|
||||
font-family: Lucida Console, Courier New;
|
||||
}
|
||||
|
||||
/* End Versal-specific styles */
|
||||
|
||||
/* Section Start for MNP styles */
|
||||
|
||||
.mnpSearchButton {width:22px;}
|
||||
|
||||
|
||||
table.centered-small {
|
||||
background-color: #eef3f5;
|
||||
border: 1px solid;
|
||||
border-color: #dedeee;
|
||||
width: 100%;
|
||||
border-style: solid; border-width: thin;
|
||||
font-size: 10pt; text-decoration: none;
|
||||
}
|
||||
table.centered-small a:link { text-decoration: none; }
|
||||
table.centered-small a:visited { text-decoration: none; }
|
||||
table.centered-small a:active { text-decoration: none; }
|
||||
|
||||
address { font-size: 10pt; font-family: Verdana, Arial, Helvetica, sans-serif; }
|
||||
|
||||
.fragment {
|
||||
font-family: monospace, fixed;
|
||||
font-size: 10ptr;
|
||||
}
|
||||
PRE.fragment {
|
||||
border: 1px solid #CCCCCC;
|
||||
background-color: #f5f5f5;
|
||||
margin-top: 4px;
|
||||
margin-bottom: 4px;
|
||||
margin-left: 2px;
|
||||
margin-right: 8px;
|
||||
padding-left: 6px;
|
||||
padding-right: 6px;
|
||||
padding-top: 4px;
|
||||
padding-bottom: 4px;
|
||||
}
|
||||
|
||||
|
||||
/* Style for detailed member documentation */
|
||||
.memtemplate {
|
||||
font-size: 80%;
|
||||
color: #606060;
|
||||
font-weight: normal;
|
||||
}
|
||||
.memnav {
|
||||
background-color: #e8eef2;
|
||||
border: 1px solid #84b0c7;
|
||||
text-align: center;
|
||||
margin: 2px;
|
||||
margin-right: 15px;
|
||||
padding: 2px;
|
||||
}
|
||||
.memitem {
|
||||
padding: 4px;
|
||||
background-color: #eef3f5;
|
||||
border-width: 1px;
|
||||
border-style: solid;
|
||||
border-color: #dedeee;
|
||||
-moz-border-radius: 8px 8px 8px 8px;
|
||||
}
|
||||
.memname {
|
||||
white-space: nowrap;
|
||||
font-weight: normal;
|
||||
font-size: 10pt;
|
||||
}
|
||||
.memdoc{
|
||||
padding-left: 10px;
|
||||
}
|
||||
.memproto {
|
||||
background-color: #d5e1e8;
|
||||
width: 100%;
|
||||
border-width: 1px;
|
||||
border-style: solid;
|
||||
border-color: #84b0c7;
|
||||
font-weight: bold;
|
||||
-moz-border-radius: 8px 8px 8px 8px;
|
||||
}
|
||||
.paramkey {
|
||||
text-align: right;
|
||||
}
|
||||
.paramtype {
|
||||
white-space: nowrap;
|
||||
}
|
||||
.paramname {
|
||||
color: #602020;
|
||||
font-style: italic;
|
||||
white-space: nowrap;
|
||||
}
|
||||
DIV.ah { background-color: black; font-weight: bold; color: #ffffff; margin-bottom: 3px; margin-top: 3px }
|
||||
|
||||
DIV.groupHeader {
|
||||
margin-left: 16px;
|
||||
margin-top: 12px;
|
||||
margin-bottom: 6px;
|
||||
font-weight: bold;
|
||||
}
|
||||
DIV.groupText { margin-left: 16px; font-style: italic; font-size: 90% }
|
||||
TD.indexkey {
|
||||
background-color: #e8eef2;
|
||||
font-weight: bold;
|
||||
padding-right : 10px;
|
||||
padding-top : 2px;
|
||||
padding-left : 10px;
|
||||
padding-bottom : 2px;
|
||||
margin-left : 0px;
|
||||
margin-right : 0px;
|
||||
margin-top : 2px;
|
||||
margin-bottom : 2px;
|
||||
border: 1px solid #CCCCCC;
|
||||
}
|
||||
TD.indexvalue {
|
||||
background-color: #e8eef2;
|
||||
font-style: italic;
|
||||
padding-right : 10px;
|
||||
padding-top : 2px;
|
||||
padding-left : 10px;
|
||||
padding-bottom : 2px;
|
||||
margin-left : 0px;
|
||||
margin-right : 0px;
|
||||
margin-top : 2px;
|
||||
margin-bottom : 2px;
|
||||
border: 1px solid #CCCCCC;
|
||||
}
|
||||
TR.memlist {
|
||||
background-color: #f0f0f0;
|
||||
}
|
||||
P.formulaDsp { text-align: center; }
|
||||
IMG.formulaDsp { }
|
||||
IMG.formulaInl { vertical-align: middle; }
|
||||
SPAN.keyword { color: #008000 }
|
||||
SPAN.keywordtype { color: #604020 }
|
||||
SPAN.keywordflow { color: #e08000 }
|
||||
SPAN.comment { color: #800000 }
|
||||
SPAN.preprocessor { color: #806020 }
|
||||
SPAN.stringliteral { color: #002080 }
|
||||
SPAN.charliteral { color: #008080 }
|
||||
|
||||
|
||||
.mdescLeft {
|
||||
padding: 0px 8px 4px 8px;
|
||||
font-size: 80%;
|
||||
font-style: italic;
|
||||
background-color: #FAFAFA;
|
||||
border-top: 1px none #E0E0E0;
|
||||
border-right: 1px none #E0E0E0;
|
||||
border-bottom: 1px none #E0E0E0;
|
||||
border-left: 1px none #E0E0E0;
|
||||
margin: 0px;
|
||||
}
|
||||
.mdescRight {
|
||||
padding: 0px 8px 4px 8px;
|
||||
font-size: 80%;
|
||||
font-style: italic;
|
||||
background-color: #FAFAFA;
|
||||
border-top: 1px none #E0E0E0;
|
||||
border-right: 1px none #E0E0E0;
|
||||
border-bottom: 1px none #E0E0E0;
|
||||
border-left: 1px none #E0E0E0;
|
||||
margin: 0px;
|
||||
}
|
||||
.memItemLeft {
|
||||
padding: 1px 0px 0px 8px;
|
||||
margin: 4px;
|
||||
border-top-width: 1px;
|
||||
border-right-width: 1px;
|
||||
border-bottom-width: 1px;
|
||||
border-left-width: 1px;
|
||||
border-top-color: #E0E0E0;
|
||||
border-right-color: #E0E0E0;
|
||||
border-bottom-color: #E0E0E0;
|
||||
border-left-color: #E0E0E0;
|
||||
border-top-style: solid;
|
||||
border-right-style: none;
|
||||
border-bottom-style: none;
|
||||
border-left-style: none;
|
||||
background-color: #FAFAFA;
|
||||
font-size: 80%;
|
||||
}
|
||||
.memItemRight {
|
||||
padding: 1px 8px 0px 8px;
|
||||
margin: 4px;
|
||||
border-top-width: 1px;
|
||||
border-right-width: 1px;
|
||||
border-bottom-width: 1px;
|
||||
border-left-width: 1px;
|
||||
border-top-color: #E0E0E0;
|
||||
border-right-color: #E0E0E0;
|
||||
border-bottom-color: #E0E0E0;
|
||||
border-left-color: #E0E0E0;
|
||||
border-top-style: solid;
|
||||
border-right-style: none;
|
||||
border-bottom-style: none;
|
||||
border-left-style: none;
|
||||
background-color: #FAFAFA;
|
||||
font-size: 80%;
|
||||
}
|
||||
.memTemplItemLeft {
|
||||
padding: 1px 0px 0px 8px;
|
||||
margin: 4px;
|
||||
border-top-width: 1px;
|
||||
border-right-width: 1px;
|
||||
border-bottom-width: 1px;
|
||||
border-left-width: 1px;
|
||||
border-top-color: #E0E0E0;
|
||||
border-right-color: #E0E0E0;
|
||||
border-bottom-color: #E0E0E0;
|
||||
border-left-color: #E0E0E0;
|
||||
border-top-style: none;
|
||||
border-right-style: none;
|
||||
border-bottom-style: none;
|
||||
border-left-style: none;
|
||||
background-color: #FAFAFA;
|
||||
font-size: 80%;
|
||||
}
|
||||
.memTemplItemRight {
|
||||
padding: 1px 8px 0px 8px;
|
||||
margin: 4px;
|
||||
border-top-width: 1px;
|
||||
border-right-width: 1px;
|
||||
border-bottom-width: 1px;
|
||||
border-left-width: 1px;
|
||||
border-top-color: #E0E0E0;
|
||||
border-right-color: #E0E0E0;
|
||||
border-bottom-color: #E0E0E0;
|
||||
border-left-color: #E0E0E0;
|
||||
border-top-style: none;
|
||||
border-right-style: none;
|
||||
border-bottom-style: none;
|
||||
border-left-style: none;
|
||||
background-color: #FAFAFA;
|
||||
font-size: 80%;
|
||||
}
|
||||
.memTemplParams {
|
||||
padding: 1px 0px 0px 8px;
|
||||
margin: 4px;
|
||||
border-top-width: 1px;
|
||||
border-right-width: 1px;
|
||||
border-bottom-width: 1px;
|
||||
border-left-width: 1px;
|
||||
border-top-color: #E0E0E0;
|
||||
border-right-color: #E0E0E0;
|
||||
border-bottom-color: #E0E0E0;
|
||||
border-left-color: #E0E0E0;
|
||||
border-top-style: solid;
|
||||
border-right-style: none;
|
||||
border-bottom-style: none;
|
||||
border-left-style: none;
|
||||
color: #606060;
|
||||
background-color: #FAFAFA;
|
||||
font-size: 80%;
|
||||
}
|
||||
|
||||
dl { font-size: 10pt; }
|
||||
td { font-size: 10pt; }
|
||||
th { font-weight: normal; }
|
||||
|
||||
#nav {font-family: Verdana, Arial, sans-serif; margin:0 0 0 10px;border-bottom:3px solid #DDE4EC; height:35px; min-width:500px;}
|
||||
#nav ul { list-style: none; margin-top:15px; padding: 0; font-size:150%; float:left; }
|
||||
#nav ul li, div.sitemenu ul li a, div.sitemenu ul li a:visited {color: #4E688E;display: block;padding: 0 5px;text-decoration: none;white-space: nowrap;float:left;}
|
||||
#nav ul li a:hover {color: #000;text-decoration: none;}
|
||||
#nav ul li a:active {color: #cfdbe6;text-decoration: none;}
|
||||
1610
doc/z3.dox
Normal file
1610
doc/z3.dox
Normal file
File diff suppressed because it is too large
Load diff
BIN
doc/z3.png
Normal file
BIN
doc/z3.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 7.9 KiB |
|
|
@ -5535,7 +5535,7 @@ END_MLAPI_EXCLUDE
|
|||
of sorts in the domain of \c r. Each sort in the domain should be an integral
|
||||
(bit-vector, Boolean or or finite domain sort).
|
||||
|
||||
The call has the same effect as adding a rule where \r is applied to the arguments.
|
||||
The call has the same effect as adding a rule where \c r is applied to the arguments.
|
||||
|
||||
def_API('Z3_fixedpoint_add_fact', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(FUNC_DECL), _in(UINT), _in_array(3, UINT)))
|
||||
*/
|
||||
|
|
|
|||
|
|
@ -306,7 +306,7 @@ cmd_context::cmd_context(front_end_params * params, bool main_ctx, ast_manager *
|
|||
m_params_owner(params == 0),
|
||||
m_logic(l),
|
||||
m_interactive_mode(false),
|
||||
m_global_decls(!this->params().m_smtlib2_compliant), // SMTLIB 2.0 uses scoped decls.
|
||||
m_global_decls(false), // :global-decls is false by default.
|
||||
m_print_success(false), // params.m_smtlib2_compliant),
|
||||
m_random_seed(0),
|
||||
m_produce_unsat_cores(false),
|
||||
|
|
|
|||
Loading…
Reference in a new issue