From b992f59aad9fe4a574a8af43fe79deccbc74bc3b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 30 Aug 2020 10:32:17 -0700 Subject: [PATCH] expose name inclusion as optional Signed-off-by: Nikolaj Bjorner --- src/api/api_goal.cpp | 6 +++--- src/api/c++/z3++.h | 2 +- src/api/dotnet/Goal.cs | 4 ++-- src/api/python/z3/z3.py | 4 ++-- src/api/z3_api.h | 4 ++-- 5 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/api/api_goal.cpp b/src/api/api_goal.cpp index f8225e0d4..a9dddd6f2 100644 --- a/src/api/api_goal.cpp +++ b/src/api/api_goal.cpp @@ -193,16 +193,16 @@ extern "C" { Z3_CATCH_RETURN(""); } - Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g) { + Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g, bool include_names) { Z3_TRY; - LOG_Z3_goal_to_dimacs_string(c, g); + LOG_Z3_goal_to_dimacs_string(c, g, include_names); RESET_ERROR_CODE(); std::ostringstream buffer; if (!to_goal_ref(g)->is_cnf()) { SET_ERROR_CODE(Z3_INVALID_ARG, "If this is not what you want, then preprocess by optional bit-blasting and applying tseitin-cnf"); RETURN_Z3(nullptr); } - to_goal_ref(g)->display_dimacs(buffer, true); + to_goal_ref(g)->display_dimacs(buffer, include_names); // Hack for removing the trailing '\n' std::string result = buffer.str(); SASSERT(result.size() > 0); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 1e297cf05..425e2e314 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2630,7 +2630,7 @@ namespace z3 { return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr())); } } - std::string dimacs() const { return std::string(Z3_goal_to_dimacs_string(ctx(), m_goal)); } + std::string dimacs(bool include_names = true) const { return std::string(Z3_goal_to_dimacs_string(ctx(), m_goal, include_names)); } friend std::ostream & operator<<(std::ostream & out, goal const & g); }; inline std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; } diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs index 883b91f35..05edb36b1 100644 --- a/src/api/dotnet/Goal.cs +++ b/src/api/dotnet/Goal.cs @@ -225,9 +225,9 @@ namespace Microsoft.Z3 /// Goal to DIMACS formatted string conversion. /// /// A string representation of the Goal. - public string ToDimacs() + public string ToDimacs(bool include_names = true) { - return Native.Z3_goal_to_dimacs_string(Context.nCtx, NativeObject); + return Native.Z3_goal_to_dimacs_string(Context.nCtx, NativeObject, include_names); } /// diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index b5d33ff6c..2e2de4e23 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -5413,9 +5413,9 @@ class Goal(Z3PPObject): """Return a textual representation of the s-expression representing the goal.""" return Z3_goal_to_string(self.ctx.ref(), self.goal) - def dimacs(self): + def dimacs(self, include_names = True): """Return a textual representation of the goal in DIMACS format.""" - return Z3_goal_to_dimacs_string(self.ctx.ref(), self.goal) + return Z3_goal_to_dimacs_string(self.ctx.ref(), self.goal, include_names) def translate(self, target): """Copy goal `self` to context `target`. diff --git a/src/api/z3_api.h b/src/api/z3_api.h index fbe7eb40f..4311a0bdb 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5840,9 +5840,9 @@ extern "C" { preserve satisfiability, it should apply bit-blasting tactics. Quantifiers and theory atoms will not be encoded. - def_API('Z3_goal_to_dimacs_string', STRING, (_in(CONTEXT), _in(GOAL))) + def_API('Z3_goal_to_dimacs_string', STRING, (_in(CONTEXT), _in(GOAL), _in(BOOL))) */ - Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g); + Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g, bool include_names); /*@}*/