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:
commit
b8ac3e6ce4
|
@ -65,7 +65,7 @@ def display_help():
|
|||
|
||||
# Parse configuration option for mk_make script
|
||||
def parse_options():
|
||||
global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_KEY_FILE
|
||||
global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_CORE_ENABLED, DOTNET_KEY_FILE
|
||||
path = BUILD_DIR
|
||||
options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=',
|
||||
'help',
|
||||
|
@ -93,6 +93,7 @@ def parse_options():
|
|||
DOTNET_ENABLED = False
|
||||
elif opt == '--dotnetcore':
|
||||
DOTNET_CORE_ENABLED = True
|
||||
DOTNET_ENABLED = False
|
||||
elif opt == '--nopython':
|
||||
PYTHON_ENABLED = False
|
||||
elif opt == '--dotnet-key':
|
||||
|
@ -195,10 +196,8 @@ def mk_dist_dir():
|
|||
build_path = BUILD_DIR
|
||||
dist_path = os.path.join(DIST_DIR, get_z3_name())
|
||||
mk_dir(dist_path)
|
||||
if DOTNET_CORE_ENABLED:
|
||||
mk_util.DOTNET_CORE_ENABLED = True
|
||||
else:
|
||||
mk_util.DOTNET_ENABLED = DOTNET_ENABLED
|
||||
mk_util.DOTNET_CORE_ENABLED = DOTNET_CORE_ENABLED
|
||||
mk_util.DOTNET_ENABLED = DOTNET_ENABLED
|
||||
mk_util.DOTNET_KEY_FILE = DOTNET_KEY_FILE
|
||||
mk_util.JAVA_ENABLED = JAVA_ENABLED
|
||||
mk_util.PYTHON_ENABLED = PYTHON_ENABLED
|
||||
|
|
|
@ -104,6 +104,7 @@ def parse_options():
|
|||
DOTNET_ENABLED = False
|
||||
elif opt == '--dotnetcore':
|
||||
DOTNET_CORE_ENABLED = True
|
||||
DOTNET_ENABLED = False
|
||||
elif opt == '--nopython':
|
||||
PYTHON_ENABLED = False
|
||||
elif opt == '--dotnet-key':
|
||||
|
|
|
@ -308,7 +308,7 @@ extern "C" {
|
|||
|
||||
\param c - context.
|
||||
\param f - fixedpoint context.
|
||||
\param s - string containing SMT2 specification.
|
||||
\param s - path to file containing SMT2 specification.
|
||||
|
||||
def_API('Z3_fixedpoint_from_file', AST_VECTOR, (_in(CONTEXT), _in(FIXEDPOINT), _in(STRING)))
|
||||
*/
|
||||
|
|
|
@ -252,7 +252,7 @@ extern "C" {
|
|||
|
||||
\param c - context.
|
||||
\param o - optimize context.
|
||||
\param s - string containing SMT2 specification.
|
||||
\param s - path to file containing SMT2 specification.
|
||||
|
||||
def_API('Z3_optimize_from_file', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(STRING)))
|
||||
*/
|
||||
|
|
|
@ -146,6 +146,8 @@ public:
|
|||
|
||||
lbool check_sat(app_ref_vector const& asms) { return check_sat(asms.size(), (expr* const*)asms.c_ptr()); }
|
||||
|
||||
lbool check_sat() { return check_sat(0, nullptr); }
|
||||
|
||||
/**
|
||||
\brief Check satisfiability modulo a cube and a clause.
|
||||
|
||||
|
|
|
@ -520,7 +520,7 @@ public:
|
|||
try {
|
||||
symbol m, p;
|
||||
normalize(name, m, p);
|
||||
std::cout << name << " " << m << " " << p << "\n";
|
||||
out << name << " " << m << " " << p << "\n";
|
||||
param_descrs * d;
|
||||
if (m == symbol::null) {
|
||||
d = &get_param_descrs();
|
||||
|
|
Loading…
Reference in a new issue