From a9e6d83c6e746480811b80467a33281a2e554e21 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Nov 2018 10:40:08 -0800 Subject: [PATCH 1/4] std::cout -> out Signed-off-by: Nikolaj Bjorner --- src/solver/solver.h | 2 ++ src/util/gparams.cpp | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/solver/solver.h b/src/solver/solver.h index 5329161cd..7437a5a08 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -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. diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 4ba3b3b5c..9ab3123a2 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -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(); From ddf6d48b3e731cd3a7bd79cab7ef73985c8824f1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Nov 2018 10:48:45 -0800 Subject: [PATCH 2/4] update unix-dist Signed-off-by: Nikolaj Bjorner --- scripts/mk_unix_dist.py | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index 3e4456676..5b019f17b 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -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 From 5188f4d82e9c1a71eae1332470c2f11e3e4d9c18 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Nov 2018 10:55:59 -0800 Subject: [PATCH 3/4] update dist scripts Signed-off-by: Nikolaj Bjorner --- scripts/mk_unix_dist.py | 2 +- scripts/mk_win_dist.py | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index 5b019f17b..bad51528f 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -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', diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index e61a7714c..bd3cad18a 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -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': From 93835eab05da592efaffd6f3ddd82cee135f8c4d Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Mon, 19 Nov 2018 13:04:07 +0700 Subject: [PATCH 4/4] Correct Z3_(fixedpoint|optimize)_from_file param doc. --- src/api/z3_fixedpoint.h | 2 +- src/api/z3_optimization.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/z3_fixedpoint.h b/src/api/z3_fixedpoint.h index b4c3eee49..df1f1461f 100644 --- a/src/api/z3_fixedpoint.h +++ b/src/api/z3_fixedpoint.h @@ -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))) */ diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h index f15d8ff9c..b1c01a386 100644 --- a/src/api/z3_optimization.h +++ b/src/api/z3_optimization.h @@ -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))) */