mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 04:28:17 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source 
:wi
This commit is contained in:
Nikolaj Bjorner 2017-03-08 10:07:40 +01:00
parent 41e6fafc58 b57764800c
commit 202ac0d1ee
10 changed files with 225 additions and 111 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
CMakeLists.txt
View file

@ -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

6
doc/mk_api_doc.py
View file

@ -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,7 +32,7 @@ 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)

2
scripts/mk_unix_dist.py
View file

@ -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():

3
scripts/mk_util.py
View file

@ -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

2
scripts/mk_win_dist.py
View file

@ -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)

3
scripts/update_api.py
View file

@ -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:

146
src/api/java/Optimize.java
View file

@ -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.
**/
@ -70,51 +69,75 @@ public class Optimize extends Z3Object
**/
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;
}
public static class Handle {
/**
* Retrieve a lower bound for the objective handle.
**/
public ArithExpr getLower()
{
return opt.GetLower(handle);
}
private final Optimize opt;
private final int handle;
/**
* Retrieve an upper bound for the objective handle.
**/
public ArithExpr getUpper()
{
return opt.GetUpper(handle);
}
Handle(Optimize opt, int h)
{
this.opt = opt;
this.handle = h;
}
/**
* Retrieve the value of an objective.
**/
public ArithExpr getValue()
{
return getLower();
}
/**
* Retrieve a lower bound for the objective handle.
**/
public ArithExpr getLower()
{
return opt.GetLower(handle);
}
/**
* Print a string representation of the handle.
**/
@Override
public String toString()
/**
* 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();
}
@ -126,7 +149,6 @@ public class Optimize extends Z3Object
* Return an objective which associates with the group of constraints.
*
**/
public Handle AssertSoft(BoolExpr constraint, int weight, String group)
{
getContext().checkContextMatch(constraint);
@ -134,13 +156,11 @@ public class Optimize extends Z3Object
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()));
@ -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());
@ -218,7 +236,6 @@ public class Optimize extends Z3Object
return (ArithExpr)Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
}
/**
* Retrieve an upper bound for the objective handle.
**/
@ -227,6 +244,42 @@ public class Optimize extends Z3Object
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
**/
@ -236,7 +289,6 @@ public class Optimize extends Z3Object
getNativeObject());
}
/**
* Print the context to a String (SMT-LIB parseable benchmark).
**/

2
src/ast/fpa_decl_plugin.cpp
View file

@ -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));
}

55
src/ast/seq_decl_plugin.cpp
View file

@ -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())) {

8
src/ast/seq_decl_plugin.h
View file

@ -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;