mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
Nikolaj Bjorner
commit
ec86cd8357
|
|
@ -112,6 +112,13 @@ else()
|
|||
set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${available_build_types})
|
||||
endif()
|
||||
message(STATUS "Build type: ${CMAKE_BUILD_TYPE}")
|
||||
|
||||
# Check the selected build type is valid
|
||||
list(FIND available_build_types "${CMAKE_BUILD_TYPE}" _build_type_index)
|
||||
if ("${_build_type_index}" EQUAL "-1")
|
||||
message(FATAL_ERROR "\"${CMAKE_BUILD_TYPE}\" is an invalid build type.\n"
|
||||
"Use one of the following build types ${available_build_types}")
|
||||
endif()
|
||||
endif()
|
||||
|
||||
# CMAKE_BUILD_TYPE has no meaning for multi-configuration generators
|
||||
|
|
|
|||
|
|
@ -12,10 +12,6 @@ import shutil
|
|||
ML_ENABLED=False
|
||||
BUILD_DIR='../build'
|
||||
|
||||
def norm_path(p):
|
||||
# We use '/' on mk_project for convenience
|
||||
return os.path.join(*(p.split('/')))
|
||||
|
||||
def display_help(exit_code):
|
||||
print("mk_api_doc.py: Z3 documentation generator\n")
|
||||
print("\nOptions:")
|
||||
|
|
@ -36,12 +32,12 @@ def parse_options():
|
|||
|
||||
for opt, arg in options:
|
||||
if opt in ('-b', '--build'):
|
||||
BUILD_DIR = norm_path(arg)
|
||||
BUILD_DIR = mk_util.norm_path(arg)
|
||||
elif opt in ('h', '--help'):
|
||||
display_help()
|
||||
exit(1)
|
||||
elif opt in ('--ml'):
|
||||
ML_ENABLED=True
|
||||
ML_ENABLED=True
|
||||
else:
|
||||
print("ERROR: Invalid command line option: %s" % opt)
|
||||
display_help(1)
|
||||
|
|
@ -59,7 +55,7 @@ def cleanup_API(inf, outf):
|
|||
pat1 = re.compile(".*def_API.*")
|
||||
pat2 = re.compile(".*extra_API.*")
|
||||
_inf = open(inf, 'r')
|
||||
_outf = open(outf, 'w')
|
||||
_outf = open(outf, 'w')
|
||||
for line in _inf:
|
||||
if not pat1.match(line) and not pat2.match(line):
|
||||
_outf.write(line)
|
||||
|
|
@ -90,9 +86,9 @@ try:
|
|||
cleanup_API('../src/api/z3_rcf.h', 'tmp/z3_rcf.h')
|
||||
cleanup_API('../src/api/z3_fixedpoint.h', 'tmp/z3_fixedpoint.h')
|
||||
cleanup_API('../src/api/z3_optimization.h', 'tmp/z3_optimization.h')
|
||||
cleanup_API('../src/api/z3_interp.h', 'tmp/z3_interp.h')
|
||||
cleanup_API('../src/api/z3_interp.h', 'tmp/z3_interp.h')
|
||||
cleanup_API('../src/api/z3_fpa.h', 'tmp/z3_fpa.h')
|
||||
|
||||
|
||||
print("Removed annotations from z3_api.h.")
|
||||
try:
|
||||
if subprocess.call(['doxygen', 'z3api.dox']) != 0:
|
||||
|
|
@ -112,7 +108,7 @@ try:
|
|||
os.remove('tmp/z3_interp.h')
|
||||
os.remove('tmp/z3_fpa.h')
|
||||
print("Removed temporary file header files.")
|
||||
|
||||
|
||||
os.remove('tmp/website.dox')
|
||||
print("Removed temporary file website.dox")
|
||||
os.remove('tmp/z3py.py')
|
||||
|
|
@ -130,7 +126,7 @@ try:
|
|||
print("ERROR: ocamldoc failed.")
|
||||
exit(1)
|
||||
print("Generated ML/OCaml documentation.")
|
||||
|
||||
|
||||
print("Documentation was successfully generated at subdirectory './api/html'.")
|
||||
except:
|
||||
exctype, value = sys.exc_info()[:2]
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
############################################
|
||||
# Copyright (c) 2013 Microsoft Corporation
|
||||
#
|
||||
# Scripts for automatically generating
|
||||
#
|
||||
# Scripts for automatically generating
|
||||
# Linux/OSX/BSD distribution zip files.
|
||||
#
|
||||
# Author: Leonardo de Moura (leonardo)
|
||||
|
|
@ -42,7 +42,7 @@ def mk_dir(d):
|
|||
|
||||
def set_build_dir(path):
|
||||
global BUILD_DIR
|
||||
BUILD_DIR = path
|
||||
BUILD_DIR = mk_util.norm_path(path)
|
||||
mk_dir(BUILD_DIR)
|
||||
|
||||
def display_help():
|
||||
|
|
@ -65,7 +65,7 @@ def display_help():
|
|||
def parse_options():
|
||||
global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_KEY_FILE
|
||||
path = BUILD_DIR
|
||||
options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=',
|
||||
options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=',
|
||||
'help',
|
||||
'silent',
|
||||
'force',
|
||||
|
|
@ -89,7 +89,7 @@ def parse_options():
|
|||
elif opt == '--nodotnet':
|
||||
DOTNET_ENABLED = False
|
||||
elif opt == '--nopython':
|
||||
PYTHON_ENABLED = False
|
||||
PYTHON_ENABLED = False
|
||||
elif opt == '--dotnet-key':
|
||||
DOTNET_KEY_FILE = arg
|
||||
elif opt == '--nojava':
|
||||
|
|
@ -121,7 +121,7 @@ def mk_build_dir(path):
|
|||
opts.append('--python')
|
||||
if subprocess.call(opts) != 0:
|
||||
raise MKException("Failed to generate build directory at '%s'" % path)
|
||||
|
||||
|
||||
# Create build directories
|
||||
def mk_build_dirs():
|
||||
mk_build_dir(BUILD_DIR)
|
||||
|
|
|
|||
|
|
@ -153,8 +153,7 @@ def is_cygwin_mingw():
|
|||
return IS_CYGWIN_MINGW
|
||||
|
||||
def norm_path(p):
|
||||
# We use '/' on mk_project for convenience
|
||||
return os.path.join(*(p.split('/')))
|
||||
return os.path.expanduser(os.path.normpath(p))
|
||||
|
||||
def which(program):
|
||||
import os
|
||||
|
|
@ -1393,7 +1392,7 @@ class DLLComponent(Component):
|
|||
shutil.copy('%s.a' % os.path.join(build_path, self.dll_name),
|
||||
'%s.a' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
|
||||
|
||||
class PythonComponent(Component):
|
||||
class PythonComponent(Component):
|
||||
def __init__(self, name, libz3Component):
|
||||
assert isinstance(libz3Component, DLLComponent)
|
||||
global PYTHON_ENABLED
|
||||
|
|
@ -1418,7 +1417,7 @@ class PythonComponent(Component):
|
|||
|
||||
def mk_makefile(self, out):
|
||||
return
|
||||
|
||||
|
||||
class PythonInstallComponent(Component):
|
||||
def __init__(self, name, libz3Component):
|
||||
assert isinstance(libz3Component, DLLComponent)
|
||||
|
|
@ -1521,7 +1520,7 @@ class PythonInstallComponent(Component):
|
|||
os.path.join('python', 'z3', '*.pyc'),
|
||||
os.path.join(self.pythonPkgDir,'z3'),
|
||||
in_prefix=self.in_prefix_install)
|
||||
|
||||
|
||||
if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib():
|
||||
out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR)
|
||||
|
||||
|
|
@ -1586,7 +1585,7 @@ class DotNetDLLComponent(Component):
|
|||
|
||||
def mk_makefile(self, out):
|
||||
global DOTNET_KEY_FILE
|
||||
|
||||
|
||||
if not is_dotnet_enabled():
|
||||
return
|
||||
cs_fp_files = []
|
||||
|
|
@ -1631,7 +1630,7 @@ class DotNetDLLComponent(Component):
|
|||
else:
|
||||
print("Keyfile '%s' could not be found; %s.dll will be unsigned." % (self.key_file, self.dll_name))
|
||||
self.key_file = None
|
||||
|
||||
|
||||
if not self.key_file is None:
|
||||
print("%s.dll will be signed using key '%s'." % (self.dll_name, self.key_file))
|
||||
cscCmdLine.append('/keyfile:{}'.format(self.key_file))
|
||||
|
|
@ -1658,7 +1657,7 @@ class DotNetDLLComponent(Component):
|
|||
)
|
||||
else:
|
||||
cscCmdLine.extend(['/optimize+'])
|
||||
|
||||
|
||||
if IS_WINDOWS:
|
||||
if VS_X64:
|
||||
cscCmdLine.extend(['/platform:x64'])
|
||||
|
|
@ -1962,7 +1961,7 @@ class MLComponent(Component):
|
|||
|
||||
OCAMLMKLIB = 'ocamlmklib'
|
||||
|
||||
LIBZ3 = '-L. -lz3'
|
||||
LIBZ3 = '-L. -lz3'
|
||||
if is_cygwin() and not(is_cygwin_mingw()):
|
||||
LIBZ3 = 'libz3.dll'
|
||||
|
||||
|
|
@ -2214,7 +2213,7 @@ class PythonExampleComponent(ExampleComponent):
|
|||
def mk_win_dist(self, build_path, dist_path):
|
||||
full = os.path.join(EXAMPLE_DIR, self.path)
|
||||
py = 'example.py'
|
||||
shutil.copyfile(os.path.join(full, py),
|
||||
shutil.copyfile(os.path.join(full, py),
|
||||
os.path.join(dist_path, INSTALL_BIN_DIR, 'python', py))
|
||||
|
||||
def mk_unix_dist(self, build_path, dist_path):
|
||||
|
|
@ -2263,7 +2262,7 @@ def add_java_dll(name, deps=[], path=None, dll_name=None, package_name=None, man
|
|||
def add_python(libz3Component):
|
||||
name = 'python'
|
||||
reg_component(name, PythonComponent(name, libz3Component))
|
||||
|
||||
|
||||
def add_python_install(libz3Component):
|
||||
name = 'python_install'
|
||||
reg_component(name, PythonInstallComponent(name, libz3Component))
|
||||
|
|
@ -2689,7 +2688,7 @@ def get_full_version_string(major, minor, build, revision):
|
|||
branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD', '--long'])
|
||||
res += " master " + check_output(['git', 'describe'])
|
||||
return '"' + res + '"'
|
||||
|
||||
|
||||
# Update files with the version number
|
||||
def mk_version_dot_h(major, minor, build, revision):
|
||||
c = get_component(UTIL_COMPONENT)
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
############################################
|
||||
# Copyright (c) 2012 Microsoft Corporation
|
||||
#
|
||||
# Scripts for automatically generating
|
||||
#
|
||||
# Scripts for automatically generating
|
||||
# Window distribution zip files.
|
||||
#
|
||||
# Author: Leonardo de Moura (leonardo)
|
||||
|
|
@ -46,7 +46,7 @@ def mk_dir(d):
|
|||
|
||||
def set_build_dir(path):
|
||||
global BUILD_DIR, BUILD_X86_DIR, BUILD_X64_DIR
|
||||
BUILD_DIR = path
|
||||
BUILD_DIR = mk_util.norm_path(path)
|
||||
BUILD_X86_DIR = os.path.join(path, 'x86')
|
||||
BUILD_X64_DIR = os.path.join(path, 'x64')
|
||||
mk_dir(BUILD_X86_DIR)
|
||||
|
|
@ -74,7 +74,7 @@ def display_help():
|
|||
def parse_options():
|
||||
global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_KEY_FILE, PYTHON_ENABLED, X86ONLY, X64ONLY
|
||||
path = BUILD_DIR
|
||||
options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=',
|
||||
options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=',
|
||||
'help',
|
||||
'silent',
|
||||
'force',
|
||||
|
|
@ -102,7 +102,7 @@ def parse_options():
|
|||
elif opt == '--nopython':
|
||||
PYTHON_ENABLED = False
|
||||
elif opt == '--dotnet-key':
|
||||
DOTNET_KEY_FILE = arg
|
||||
DOTNET_KEY_FILE = arg
|
||||
elif opt == '--nojava':
|
||||
JAVA_ENABLED = False
|
||||
elif opt == '--githash':
|
||||
|
|
@ -139,7 +139,7 @@ def mk_build_dir(path, x64):
|
|||
opts.append('--python')
|
||||
if subprocess.call(opts) != 0:
|
||||
raise MKException("Failed to generate build directory at '%s'" % path)
|
||||
|
||||
|
||||
# Create build directories
|
||||
def mk_build_dirs():
|
||||
mk_build_dir(BUILD_X86_DIR, False)
|
||||
|
|
@ -176,7 +176,7 @@ def mk_z3(x64):
|
|||
cmds = []
|
||||
if x64:
|
||||
cmds.append('call "%VCINSTALLDIR%vcvarsall.bat" amd64')
|
||||
cmds.append('cd %s' % BUILD_X64_DIR)
|
||||
cmds.append('cd %s' % BUILD_X64_DIR)
|
||||
else:
|
||||
cmds.append('call "%VCINSTALLDIR%vcvarsall.bat" x86')
|
||||
cmds.append('cd %s' % BUILD_X86_DIR)
|
||||
|
|
@ -248,12 +248,12 @@ def mk_zips():
|
|||
VS_RUNTIME_PATS = [re.compile('vcomp.*\.dll'),
|
||||
re.compile('msvcp.*\.dll'),
|
||||
re.compile('msvcr.*\.dll')]
|
||||
|
||||
|
||||
# Copy Visual Studio Runtime libraries
|
||||
def cp_vs_runtime(x64):
|
||||
def cp_vs_runtime(x64):
|
||||
if x64:
|
||||
platform = "x64"
|
||||
|
||||
|
||||
else:
|
||||
platform = "x86"
|
||||
vcdir = os.environ['VCINSTALLDIR']
|
||||
|
|
@ -261,7 +261,7 @@ def cp_vs_runtime(x64):
|
|||
VS_RUNTIME_FILES = []
|
||||
for root, dirs, files in os.walk(path):
|
||||
for filename in files:
|
||||
if fnmatch(filename, '*.dll'):
|
||||
if fnmatch(filename, '*.dll'):
|
||||
for pat in VS_RUNTIME_PATS:
|
||||
if pat.match(filename):
|
||||
fname = os.path.join(root, filename)
|
||||
|
|
|
|||
|
|
@ -710,6 +710,9 @@ def mk_java(java_dir, package_name):
|
|||
java_wrapper.write(' }\n')
|
||||
elif k == OUT_MANAGED_ARRAY:
|
||||
java_wrapper.write(' *(jlong**)a%s = (jlong*)_a%s;\n' % (i, i))
|
||||
|
||||
elif k == IN and param_type(param) == STRING:
|
||||
java_wrapper.write(' jenv->ReleaseStringUTFChars(a%s, _a%s);\n' % (i, i));
|
||||
i = i + 1
|
||||
# return
|
||||
if result == STRING:
|
||||
|
|
|
|||
|
|
@ -14,7 +14,6 @@ Author:
|
|||
Nikolaj Bjorner (nbjorner) 2015-07-16
|
||||
|
||||
Notes:
|
||||
|
||||
**/
|
||||
|
||||
package com.microsoft.z3;
|
||||
|
|
@ -23,10 +22,10 @@ import com.microsoft.z3.enumerations.Z3_lbool;
|
|||
|
||||
|
||||
/**
|
||||
* Object for managing optimizization context
|
||||
* Object for managing optimization context
|
||||
**/
|
||||
public class Optimize extends Z3Object
|
||||
{
|
||||
public class Optimize extends Z3Object {
|
||||
|
||||
/**
|
||||
* A string that describes all available optimize solver parameters.
|
||||
**/
|
||||
|
|
@ -55,7 +54,7 @@ public class Optimize extends Z3Object
|
|||
|
||||
/**
|
||||
* Assert a constraint (or multiple) into the optimize solver.
|
||||
**/
|
||||
**/
|
||||
public void Assert(BoolExpr ... constraints)
|
||||
{
|
||||
getContext().checkContextMatch(constraints);
|
||||
|
|
@ -67,80 +66,101 @@ public class Optimize extends Z3Object
|
|||
|
||||
/**
|
||||
* Alias for Assert.
|
||||
**/
|
||||
**/
|
||||
public void Add(BoolExpr ... constraints)
|
||||
{
|
||||
Assert(constraints);
|
||||
Assert(constraints);
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
* Handle to objectives returned by objective functions.
|
||||
**/
|
||||
public class Handle
|
||||
{
|
||||
Optimize opt;
|
||||
int handle;
|
||||
Handle(Optimize opt, int h)
|
||||
{
|
||||
this.opt = opt;
|
||||
this.handle = h;
|
||||
}
|
||||
|
||||
/**
|
||||
* Retrieve a lower bound for the objective handle.
|
||||
**/
|
||||
public ArithExpr getLower()
|
||||
{
|
||||
return opt.GetLower(handle);
|
||||
}
|
||||
|
||||
/**
|
||||
* Retrieve an upper bound for the objective handle.
|
||||
**/
|
||||
public ArithExpr getUpper()
|
||||
{
|
||||
return opt.GetUpper(handle);
|
||||
}
|
||||
|
||||
/**
|
||||
* Retrieve the value of an objective.
|
||||
**/
|
||||
public ArithExpr getValue()
|
||||
{
|
||||
return getLower();
|
||||
}
|
||||
public static class Handle {
|
||||
|
||||
/**
|
||||
* Print a string representation of the handle.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
private final Optimize opt;
|
||||
private final int handle;
|
||||
|
||||
Handle(Optimize opt, int h)
|
||||
{
|
||||
this.opt = opt;
|
||||
this.handle = h;
|
||||
}
|
||||
|
||||
/**
|
||||
* Retrieve a lower bound for the objective handle.
|
||||
**/
|
||||
public ArithExpr getLower()
|
||||
{
|
||||
return opt.GetLower(handle);
|
||||
}
|
||||
|
||||
/**
|
||||
* Retrieve an upper bound for the objective handle.
|
||||
**/
|
||||
public ArithExpr getUpper()
|
||||
{
|
||||
return opt.GetUpper(handle);
|
||||
}
|
||||
|
||||
/**
|
||||
* @return a triple representing the upper bound of the objective handle.
|
||||
*
|
||||
* The triple contains values {@code inf, value, eps},
|
||||
* where the objective value is unbounded iff {@code inf} is non-zero,
|
||||
* and otherwise is represented by the expression {@code value + eps * EPSILON},
|
||||
* where {@code EPSILON} is an arbitrarily small real number.
|
||||
*/
|
||||
public ArithExpr[] getUpperAsVector()
|
||||
{
|
||||
return opt.GetUpperAsVector(handle);
|
||||
}
|
||||
|
||||
/**
|
||||
* @return a triple representing the upper bound of the objective handle.
|
||||
*
|
||||
* <p>See {@link #getUpperAsVector()} for triple semantics.
|
||||
*/
|
||||
public ArithExpr[] getLowerAsVector()
|
||||
{
|
||||
return opt.GetLowerAsVector(handle);
|
||||
}
|
||||
|
||||
/**
|
||||
* Retrieve the value of an objective.
|
||||
**/
|
||||
public ArithExpr getValue()
|
||||
{
|
||||
return getLower();
|
||||
}
|
||||
|
||||
/**
|
||||
* Print a string representation of the handle.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
return getValue().toString();
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
/**
|
||||
* Assert soft constraint
|
||||
*
|
||||
* Return an objective which associates with the group of constraints.
|
||||
*
|
||||
**/
|
||||
|
||||
**/
|
||||
public Handle AssertSoft(BoolExpr constraint, int weight, String group)
|
||||
{
|
||||
getContext().checkContextMatch(constraint);
|
||||
Symbol s = getContext().mkSymbol(group);
|
||||
return new Handle(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
/**
|
||||
* Check satisfiability of asserted constraints.
|
||||
* Produce a model that (when the objectives are bounded and
|
||||
* don't use strict inequalities) meets the objectives.
|
||||
**/
|
||||
|
||||
public Status Check()
|
||||
{
|
||||
Z3_lbool r = Z3_lbool.fromInt(Native.optimizeCheck(getContext().nCtx(), getNativeObject()));
|
||||
|
|
@ -153,7 +173,7 @@ public class Optimize extends Z3Object
|
|||
return Status.UNKNOWN;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
* Creates a backtracking point.
|
||||
**/
|
||||
|
|
@ -162,13 +182,11 @@ public class Optimize extends Z3Object
|
|||
Native.optimizePush(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
/**
|
||||
* Backtrack one backtracking point.
|
||||
*
|
||||
* Note that an exception is thrown if Pop is called without a corresponding Push.
|
||||
**/
|
||||
|
||||
public void Pop()
|
||||
{
|
||||
Native.optimizePop(getContext().nCtx(), getNativeObject());
|
||||
|
|
@ -191,7 +209,7 @@ public class Optimize extends Z3Object
|
|||
}
|
||||
}
|
||||
|
||||
/**
|
||||
/**
|
||||
* Declare an arithmetical maximization objective.
|
||||
* Return a handle to the objective. The handle is used as
|
||||
* to retrieve the values of objectives after calling Check.
|
||||
|
|
@ -200,11 +218,11 @@ public class Optimize extends Z3Object
|
|||
{
|
||||
return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
* Declare an arithmetical minimization objective.
|
||||
* Similar to MkMaximize.
|
||||
**/
|
||||
**/
|
||||
public Handle MkMinimize(ArithExpr e)
|
||||
{
|
||||
return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
|
||||
|
|
@ -212,21 +230,56 @@ public class Optimize extends Z3Object
|
|||
|
||||
/**
|
||||
* Retrieve a lower bound for the objective handle.
|
||||
**/
|
||||
**/
|
||||
private ArithExpr GetLower(int index)
|
||||
{
|
||||
return (ArithExpr)Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
|
||||
}
|
||||
|
||||
|
||||
|
||||
/**
|
||||
* Retrieve an upper bound for the objective handle.
|
||||
**/
|
||||
**/
|
||||
private ArithExpr GetUpper(int index)
|
||||
{
|
||||
return (ArithExpr)Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
|
||||
}
|
||||
|
||||
/**
|
||||
* @return Triple representing the upper bound for the objective handle.
|
||||
*
|
||||
* <p>See {@link Handle#getUpperAsVector}.
|
||||
*/
|
||||
private ArithExpr[] GetUpperAsVector(int index) {
|
||||
return unpackObjectiveValueVector(
|
||||
Native.optimizeGetUpperAsVector(
|
||||
getContext().nCtx(), getNativeObject(), index
|
||||
)
|
||||
);
|
||||
}
|
||||
|
||||
/**
|
||||
* @return Triple representing the upper bound for the objective handle.
|
||||
*
|
||||
* <p>See {@link Handle#getLowerAsVector}.
|
||||
*/
|
||||
private ArithExpr[] GetLowerAsVector(int index) {
|
||||
return unpackObjectiveValueVector(
|
||||
Native.optimizeGetLowerAsVector(
|
||||
getContext().nCtx(), getNativeObject(), index
|
||||
)
|
||||
);
|
||||
}
|
||||
|
||||
private ArithExpr[] unpackObjectiveValueVector(long nativeVec) {
|
||||
ASTVector vec = new ASTVector(
|
||||
getContext(), nativeVec
|
||||
);
|
||||
return new ArithExpr[] {
|
||||
(ArithExpr) vec.get(0), (ArithExpr) vec.get(1), (ArithExpr) vec.get(2)
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
/**
|
||||
* Return a string the describes why the last to check returned unknown
|
||||
**/
|
||||
|
|
@ -235,8 +288,7 @@ public class Optimize extends Z3Object
|
|||
return Native.optimizeGetReasonUnknown(getContext().nCtx(),
|
||||
getNativeObject());
|
||||
}
|
||||
|
||||
|
||||
|
||||
/**
|
||||
* Print the context to a String (SMT-LIB parseable benchmark).
|
||||
**/
|
||||
|
|
@ -245,7 +297,7 @@ public class Optimize extends Z3Object
|
|||
{
|
||||
return Native.optimizeToString(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
* Optimize statistics.
|
||||
**/
|
||||
|
|
|
|||
|
|
@ -836,7 +836,7 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
|
|||
return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range);
|
||||
|
||||
case OP_FPA_INTERNAL_BVWRAP:
|
||||
return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range);
|
||||
return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range);
|
||||
case OP_FPA_INTERNAL_BV2RM:
|
||||
return mk_internal_bv2rm(k, num_parameters, parameters, arity, domain, range);
|
||||
|
||||
|
|
@ -915,7 +915,7 @@ void fpa_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
|
|||
op_names.push_back(builtin_name("to_fp_unsigned", OP_FPA_TO_FP_UNSIGNED));
|
||||
|
||||
/* Extensions */
|
||||
op_names.push_back(builtin_name("to_ieee_bv", OP_FPA_TO_IEEE_BV));
|
||||
op_names.push_back(builtin_name("to_ieee_bv", OP_FPA_TO_IEEE_BV));
|
||||
op_names.push_back(builtin_name("fp.to_ieee_bv", OP_FPA_TO_IEEE_BV));
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -284,8 +284,54 @@ zstring zstring::operator+(zstring const& other) const {
|
|||
return result;
|
||||
}
|
||||
|
||||
std::ostream& zstring::operator<<(std::ostream& out) const {
|
||||
return out << encode();
|
||||
bool zstring::operator==(const zstring& other) const {
|
||||
// two strings are equal iff they have the same length and characters
|
||||
if (length() != other.length()) {
|
||||
return false;
|
||||
}
|
||||
for (unsigned i = 0; i < length(); ++i) {
|
||||
unsigned Xi = m_buffer[i];
|
||||
unsigned Yi = other[i];
|
||||
if (Xi != Yi) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
bool zstring::operator!=(const zstring& other) const {
|
||||
return !(*this == other);
|
||||
}
|
||||
|
||||
std::ostream& operator<<(std::ostream &os, const zstring &str) {
|
||||
return os << str.encode();
|
||||
}
|
||||
|
||||
bool operator<(const zstring& lhs, const zstring& rhs) {
|
||||
// This has the same semantics as strcmp()
|
||||
unsigned len = lhs.length();
|
||||
if (rhs.length() < len) {
|
||||
len = rhs.length();
|
||||
}
|
||||
for (unsigned i = 0; i < len; ++i) {
|
||||
unsigned Li = lhs[i];
|
||||
unsigned Ri = rhs[i];
|
||||
if (Li < Ri) {
|
||||
return true;
|
||||
} else if (Li > Ri) {
|
||||
return false;
|
||||
} else {
|
||||
continue;
|
||||
}
|
||||
}
|
||||
// at this point, all compared characters are equal,
|
||||
// so decide based on the relative lengths
|
||||
if (lhs.length() < rhs.length()) {
|
||||
return true;
|
||||
} else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -473,6 +519,7 @@ void seq_decl_plugin::init() {
|
|||
sort* str2TintT[3] = { strT, strT, intT };
|
||||
sort* seqAintT[2] = { seqA, intT };
|
||||
sort* seq3A[3] = { seqA, seqA, seqA };
|
||||
sort* reTintT[2] = { reT, intT };
|
||||
m_sigs.resize(LAST_SEQ_OP);
|
||||
// TBD: have (par ..) construct and load parameterized signature from premable.
|
||||
m_sigs[OP_SEQ_UNIT] = alloc(psig, m, "seq.unit", 1, 1, &A, seqA);
|
||||
|
|
@ -516,6 +563,7 @@ void seq_decl_plugin::init() {
|
|||
m_sigs[_OP_REGEXP_EMPTY] = alloc(psig, m, "re.nostr", 0, 0, 0, reT);
|
||||
m_sigs[_OP_REGEXP_FULL] = alloc(psig, m, "re.allchar", 0, 0, 0, reT);
|
||||
m_sigs[_OP_STRING_SUBSTR] = alloc(psig, m, "str.substr", 0, 3, strTint2T, strT);
|
||||
m_sigs[_OP_RE_UNROLL] = alloc(psig, m, "_re.unroll", 0, 2, reTintT, strT);
|
||||
}
|
||||
|
||||
void seq_decl_plugin::set_manager(ast_manager* m, family_id id) {
|
||||
|
|
@ -672,6 +720,9 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
|
|||
m.raise_exception("Incorrect number of arguments passed to loop. Expected 1 regular expression and two integer parameters");
|
||||
}
|
||||
|
||||
case _OP_RE_UNROLL:
|
||||
match(*m_sigs[k], arity, domain, range, rng);
|
||||
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
|
||||
|
||||
case OP_STRING_CONST:
|
||||
if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) {
|
||||
|
|
|
|||
|
|
@ -79,6 +79,7 @@ enum seq_op_kind {
|
|||
_OP_REGEXP_EMPTY,
|
||||
_OP_REGEXP_FULL,
|
||||
_OP_SEQ_SKOLEM,
|
||||
_OP_RE_UNROLL,
|
||||
LAST_SEQ_OP
|
||||
};
|
||||
|
||||
|
|
@ -113,7 +114,11 @@ public:
|
|||
int indexof(zstring const& other, int offset) const;
|
||||
zstring extract(int lo, int hi) const;
|
||||
zstring operator+(zstring const& other) const;
|
||||
std::ostream& operator<<(std::ostream& out) const;
|
||||
bool operator==(const zstring& other) const;
|
||||
bool operator!=(const zstring& other) const;
|
||||
|
||||
friend std::ostream& operator<<(std::ostream &os, const zstring &str);
|
||||
friend bool operator<(const zstring& lhs, const zstring& rhs);
|
||||
};
|
||||
|
||||
class seq_decl_plugin : public decl_plugin {
|
||||
|
|
@ -334,6 +339,7 @@ public:
|
|||
MATCH_UNARY(is_opt);
|
||||
bool is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi);
|
||||
bool is_loop(expr const* n, expr*& body, unsigned& lo);
|
||||
bool is_unroll(expr const* n) const { return is_app_of(n, m_fid, _OP_RE_UNROLL); }
|
||||
};
|
||||
str str;
|
||||
re re;
|
||||
|
|
|
|||
Loading…
Reference in a new issue