From 706a037bf4bc20e37f85978b6ae8912cb9f32e67 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 16 Nov 2015 15:16:50 +0100
Subject: [PATCH 01/14] Python 3.x string decoding fix
---
scripts/update_api.py | 2 +-
src/api/python/z3printer.py | 8 +++++++-
2 files changed, 8 insertions(+), 2 deletions(-)
diff --git a/scripts/update_api.py b/scripts/update_api.py
index bb5935a1e..6e7b6d5f7 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -99,7 +99,7 @@ else:
if s != None:
enc = sys.stdout.encoding
if enc != None: return s.decode(enc)
- else: return s
+ else: return s.decode('ascii')
else:
return ""
diff --git a/src/api/python/z3printer.py b/src/api/python/z3printer.py
index 5116046dd..2a242865e 100644
--- a/src/api/python/z3printer.py
+++ b/src/api/python/z3printer.py
@@ -1157,7 +1157,13 @@ def set_pp_option(k, v):
def obj_to_string(a):
out = io.StringIO()
_PP(out, _Formatter(a))
- return out.getvalue()
+ r = out.getvalue()
+ if sys.version < '3':
+ return r
+ else:
+ enc = sys.stdout.encoding
+ if enc != None: return r.decode(enc)
+ return r
_html_out = None
From e8d37dba9cce90574ed5c9ad640968c0362c5c82 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 16 Nov 2015 21:58:17 +0100
Subject: [PATCH 02/14] Added comments for quantifier constructors. Fixes #319.
---
src/api/dotnet/Context.cs | 26 ++++++++++++++++--
src/api/java/Context.java | 58 +++++++++++++++++++++++----------------
2 files changed, 57 insertions(+), 27 deletions(-)
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 25c399d68..d56ba4af1 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2613,8 +2613,13 @@ namespace Microsoft.Z3
/// <paramref name="patterns"/> is an array of patterns, <paramref name="sorts"/> is an array
/// with the sorts of the bound variables, <paramref name="names"/> is an array with the
/// 'names' of the bound variables, and <paramref name="body"/> is the body of the
- /// quantifier. Quantifiers are associated with weights indicating
- /// the importance of using the quantifier during instantiation.
+ /// quantifier. Quantifiers are associated with weights indicating the importance of
+ /// using the quantifier during instantiation.
+ /// Note that the bound variables are de-Bruijn indices created using <see cref="MkBound"/>.
+ /// Z3 applies the convention that the last element in <paramref name="names"/> and
+ /// <paramref name="sorts"/> refers to the variable with index 0, the second to last element
+ /// of <paramref name="names"/> and <paramref name="sorts"/> refers to the variable
+ /// with index 1, etc.
/// </remarks>
/// <param name="sorts">the sorts of the bound variables.</param>
/// <param name="names">names of the bound variables</param>
@@ -2644,6 +2649,11 @@ namespace Microsoft.Z3
/// <summary>
/// Create a universal Quantifier.
/// </summary>
+ /// <remarks>
+ /// Creates a universal quantifier using a list of constants that will
+ /// form the set of bound variables.
+ /// <seealso cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
+ /// </remarks>
public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
{
Contract.Requires(body != null);
@@ -2659,7 +2669,10 @@ namespace Microsoft.Z3
/// <summary>
/// Create an existential Quantifier.
/// </summary>
- /// <seealso cref="MkForall(Sort[],Symbol[],Expr,uint,Pattern[],Expr[],Symbol,Symbol)"/>
+ /// <remarks>
+ /// Creates an existential quantifier using de-Brujin indexed variables.
+ /// (<see cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>).
+ /// </remarks>
public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
{
Contract.Requires(sorts != null);
@@ -2678,6 +2691,11 @@ namespace Microsoft.Z3
/// <summary>
/// Create an existential Quantifier.
/// </summary>
+ /// <remarks>
+ /// Creates an existential quantifier using a list of constants that will
+ /// form the set of bound variables.
+ /// <seealso cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
+ /// </remarks>
public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
{
Contract.Requires(body != null);
@@ -2693,6 +2711,7 @@ namespace Microsoft.Z3
/// <summary>
/// Create a Quantifier.
/// </summary>
+ /// <see cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
public Quantifier MkQuantifier(bool universal, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
{
Contract.Requires(body != null);
@@ -2716,6 +2735,7 @@ namespace Microsoft.Z3
/// <summary>
/// Create a Quantifier.
/// </summary>
+ /// <see cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
{
Contract.Requires(body != null);
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 0f9a85799..4d8484ced 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -433,8 +433,8 @@ public class Context extends IDisposable
/**
* Creates a fresh function declaration with a name prefixed with
* {@code prefix}.
- * @see mkFuncDecl(String,Sort,Sort)
- * @see mkFuncDecl(String,Sort[],Sort)
+ * @see #mkFuncDecl(String,Sort,Sort)
+ * @see #mkFuncDecl(String,Sort[],Sort)
**/
public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
@@ -1722,9 +1722,9 @@ public class Context extends IDisposable
**/
public Expr mkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
{
- checkContextMatch(arg1);
- checkContextMatch(arg2);
- return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
+ checkContextMatch(arg1);
+ checkContextMatch(arg2);
+ return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
}
@@ -2025,6 +2025,7 @@ public class Context extends IDisposable
/**
* Create a universal Quantifier.
+ *
* @param sorts the sorts of the bound variables.
* @param names names of the bound variables
* @param body the body of the quantifier.
@@ -2034,17 +2035,22 @@ public class Context extends IDisposable
* @param quantifierID optional symbol to track quantifier.
* @param skolemID optional symbol to track skolem constants.
*
- * Remarks: Creates a forall formula, where
- * {@code weight"/> is the weight, <paramref name="patterns} is
+ * @return Creates a forall formula, where
+ * {@code weight} is the weight, {@code patterns} is
* an array of patterns, {@code sorts} is an array with the sorts
* of the bound variables, {@code names} is an array with the
* 'names' of the bound variables, and {@code body} is the body
* of the quantifier. Quantifiers are associated with weights indicating the
* importance of using the quantifier during instantiation.
+ * Note that the bound variables are de-Bruijn indices created using {@link mkBound}.
+ * Z3 applies the convention that the last element in {@code names} and
+ * {@code sorts} refers to the variable with index 0, the second to last element
+ * of {@code names} and {@code sorts} refers to the variable
+ * with index 1, etc.
**/
public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body,
- int weight, Pattern[] patterns, Expr[] noPatterns,
- Symbol quantifierID, Symbol skolemID)
+ int weight, Pattern[] patterns, Expr[] noPatterns,
+ Symbol quantifierID, Symbol skolemID)
{
return new Quantifier(this, true, sorts, names, body, weight, patterns,
@@ -2052,11 +2058,12 @@ public class Context extends IDisposable
}
/**
- * Create a universal Quantifier.
+ * Creates a universal quantifier using a list of constants that will form the set of bound variables.
+ * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
**/
public Quantifier mkForall(Expr[] boundConstants, Expr body, int weight,
- Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
- Symbol skolemID)
+ Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
+ Symbol skolemID)
{
return new Quantifier(this, true, boundConstants, body, weight,
@@ -2064,12 +2071,12 @@ public class Context extends IDisposable
}
/**
- * Create an existential Quantifier.
+ * Creates an existential quantifier using de-Brujin indexed variables.
* @see mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
**/
public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body,
- int weight, Pattern[] patterns, Expr[] noPatterns,
- Symbol quantifierID, Symbol skolemID)
+ int weight, Pattern[] patterns, Expr[] noPatterns,
+ Symbol quantifierID, Symbol skolemID)
{
return new Quantifier(this, false, sorts, names, body, weight,
@@ -2077,11 +2084,12 @@ public class Context extends IDisposable
}
/**
- * Create an existential Quantifier.
+ * Creates an existential quantifier using a list of constants that will form the set of bound variables.
+ * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
**/
public Quantifier mkExists(Expr[] boundConstants, Expr body, int weight,
- Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
- Symbol skolemID)
+ Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
+ Symbol skolemID)
{
return new Quantifier(this, false, boundConstants, body, weight,
@@ -2090,11 +2098,12 @@ public class Context extends IDisposable
/**
* Create a Quantifier.
+ * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
**/
public Quantifier mkQuantifier(boolean universal, Sort[] sorts,
- Symbol[] names, Expr body, int weight, Pattern[] patterns,
- Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
-
+ Symbol[] names, Expr body, int weight, Pattern[] patterns,
+ Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
+
{
if (universal)
@@ -2106,11 +2115,12 @@ public class Context extends IDisposable
}
/**
- * Create a Quantifier.
+ * Create a Quantifier
+ * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
**/
public Quantifier mkQuantifier(boolean universal, Expr[] boundConstants,
- Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
- Symbol quantifierID, Symbol skolemID)
+ Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
+ Symbol quantifierID, Symbol skolemID)
{
if (universal)
From 4e9b76365d40882318c32e64682b96e80415b95a Mon Sep 17 00:00:00 2001
From: Yan <yans@yancomm.net>
Date: Mon, 16 Nov 2015 15:41:12 -0800
Subject: [PATCH 03/14] pass the correct context into And() when doing
Tactic.as_expr()
---
src/api/python/z3.py | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 214d8b687..444c025e6 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -4862,7 +4862,7 @@ class Goal(Z3PPObject):
elif sz == 1:
return self.get(0)
else:
- return And([ self.get(i) for i in range(len(self)) ])
+ return And([ self.get(i) for i in range(len(self)) ], self.ctx)
#########################################
#
From c8f09fa955ce4f6bb259eea03697db8944c9cd2f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 16 Nov 2015 22:59:07 -0800
Subject: [PATCH 04/14] fix for unsound results reported in #313
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/ast_util.cpp | 9 ++++++
src/ast/ast_util.h | 7 +++++
src/muz/pdr/pdr_context.cpp | 61 +++++++++++++++++++++++--------------
src/muz/pdr/pdr_context.h | 1 -
4 files changed, 54 insertions(+), 24 deletions(-)
diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp
index 94e7b642c..eba4d526b 100644
--- a/src/ast/ast_util.cpp
+++ b/src/ast/ast_util.cpp
@@ -166,6 +166,11 @@ expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args) {
return m.mk_and(num_args, args);
}
+app* mk_and(ast_manager & m, unsigned num_args, app * const * args) {
+ return to_app(mk_and(m, num_args, (expr* const*) args));
+}
+
+
expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args) {
if (num_args == 0)
return m.mk_false();
@@ -175,6 +180,10 @@ expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args) {
return m.mk_or(num_args, args);
}
+app* mk_or(ast_manager & m, unsigned num_args, app * const * args) {
+ return to_app(mk_or(m, num_args, (expr* const*) args));
+}
+
expr * mk_not(ast_manager & m, expr * arg) {
expr * atom;
if (m.is_not(arg, atom))
diff --git a/src/ast/ast_util.h b/src/ast/ast_util.h
index 87a3a90d9..311001a19 100644
--- a/src/ast/ast_util.h
+++ b/src/ast/ast_util.h
@@ -107,6 +107,9 @@ expr * get_clause_literal(ast_manager & m, expr * cls, unsigned idx);
Return true if num_args == 0
*/
expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args);
+app * mk_and(ast_manager & m, unsigned num_args, app * const * args);
+inline app_ref mk_and(app_ref_vector const& args) { return app_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
+inline expr_ref mk_and(expr_ref_vector const& args) { return expr_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
/**
Return (or args[0] ... args[num_args-1]) if num_args >= 2
@@ -114,6 +117,10 @@ expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args);
Return false if num_args == 0
*/
expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args);
+app * mk_or(ast_manager & m, unsigned num_args, app * const * args);
+inline app_ref mk_or(app_ref_vector const& args) { return app_ref(mk_or(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
+inline expr_ref mk_or(expr_ref_vector const& args) { return expr_ref(mk_or(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
+
/**
Return a if arg = (not a)
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index 4cdc76ede..5140c9eff 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -50,6 +50,7 @@ Notes:
#include "blast_term_ite_tactic.h"
#include "model_implicant.h"
#include "expr_safe_replace.h"
+#include "ast_util.h"
namespace pdr {
@@ -448,6 +449,7 @@ namespace pdr {
else if (is_sat == l_false) {
uses_level = m_solver.assumes_level();
}
+ m_solver.set_model(0);
return is_sat;
}
@@ -481,6 +483,7 @@ namespace pdr {
prop_solver::scoped_level _sl(m_solver, level);
m_solver.set_core(&core);
m_solver.set_subset_based_core(true);
+ m_solver.set_model(0);
lbool res = m_solver.check_assumptions_and_formula(lits, fml);
if (res == l_false) {
lits.reset();
@@ -775,6 +778,13 @@ namespace pdr {
}
// only initial states are not set by the PDR search.
SASSERT(m_model.get());
+ if (!m_model.get()) {
+ std::stringstream msg;
+ msg << "no model for node " << state();
+ IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);
+ throw default_exception(msg.str());
+ }
+
datalog::rule const& rl1 = pt().find_rule(*m_model);
if (is_ini(rl1)) {
set_rule(&rl1);
@@ -793,15 +803,23 @@ namespace pdr {
}
}
SASSERT(!tags.empty());
- ini_tags = m.mk_or(tags.size(), tags.c_ptr());
+ ini_tags = ::mk_or(tags);
ini_state = m.mk_and(ini_tags, pt().initial_state(), state());
model_ref mdl;
pt().get_solver().set_model(&mdl);
- TRACE("pdr", tout << mk_pp(ini_state, m) << "\n";);
- VERIFY(l_true == pt().get_solver().check_conjunction_as_assumptions(ini_state));
+ TRACE("pdr", tout << ini_state << "\n";);
+ if (l_true != pt().get_solver().check_conjunction_as_assumptions(ini_state)) {
+ std::stringstream msg;
+ msg << "Unsatisfiable initial state: " << ini_state << "\n";
+ display(msg, 2);
+ IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);
+ throw default_exception(msg.str());
+ }
+ SASSERT(mdl.get());
datalog::rule const& rl2 = pt().find_rule(*mdl);
SASSERT(is_ini(rl2));
set_rule(&rl2);
+ pt().get_solver().set_model(0);
return const_cast<datalog::rule*>(m_rule);
}
@@ -830,7 +848,7 @@ namespace pdr {
}
r0 = get_rule();
app_ref_vector& inst = pt().get_inst(r0);
- TRACE("pdr", tout << mk_pp(state(), m) << " instance: " << inst.size() << "\n";);
+ TRACE("pdr", tout << state() << " instance: " << inst.size() << "\n";);
for (unsigned i = 0; i < inst.size(); ++i) {
expr* v;
if (model.find(inst[i].get(), v)) {
@@ -852,7 +870,7 @@ namespace pdr {
for (unsigned i = 0; i < indent; ++i) out << " ";
out << m_level << " " << m_pt.head()->get_name() << " " << (m_closed?"closed":"open") << "\n";
for (unsigned i = 0; i < indent; ++i) out << " ";
- out << " " << mk_pp(m_state, m_state.get_manager(), indent) << "\n";
+ out << " " << mk_pp(m_state, m_state.get_manager(), indent) << " " << m_state->get_id() << "\n";
for (unsigned i = 0; i < children().size(); ++i) {
children()[i]->display(out, indent + 1);
}
@@ -925,17 +943,6 @@ namespace pdr {
}
}
- bool model_search::is_repeated(model_node& n) const {
- model_node* p = n.parent();
- while (p) {
- if (p->state() == n.state()) {
- TRACE("pdr", tout << n.state() << "repeated\n";);
- return true;
- }
- p = p->parent();
- }
- return false;
- }
void model_search::add_leaf(model_node& n) {
SASSERT(n.children().empty());
@@ -1012,11 +1019,11 @@ namespace pdr {
nodes.erase(&n);
bool is_goal = n.is_goal();
remove_goal(n);
- if (!nodes.empty() && is_goal && backtrack) {
+ // TBD: siblings would also fail if n is not a goal.
+ if (!nodes.empty() && backtrack && nodes[0]->children().empty() && nodes[0]->is_closed()) {
TRACE("pdr_verbose", for (unsigned i = 0; i < nodes.size(); ++i) n.display(tout << &n << "\n", 2););
model_node* n1 = nodes[0];
- n1->set_open();
- SASSERT(n1->children().empty());
+ n1->set_open();
enqueue_leaf(n1);
}
@@ -1702,7 +1709,15 @@ namespace pdr {
void context::validate_search() {
expr_ref tr = m_search.get_trace(*this);
- // TBD: tr << "\n";
+ smt::kernel solver(m, get_fparams());
+ solver.assert_expr(tr);
+ lbool res = solver.check();
+ if (res != l_true) {
+ std::stringstream msg;
+ msg << "rule validation failed when checking: " << tr;
+ IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);
+ throw default_exception(msg.str());
+ }
}
void context::validate_model() {
@@ -1938,11 +1953,11 @@ namespace pdr {
proof_ref proof(m);
SASSERT(m_last_result == l_true);
proof = m_search.get_proof_trace(*this);
- TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
+ TRACE("pdr", tout << "PDR trace: " << proof << "\n";);
apply(m, m_pc.get(), proof);
- TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
+ TRACE("pdr", tout << "PDR trace: " << proof << "\n";);
// proof_utils::push_instantiations_up(proof);
- // TRACE("pdr", tout << "PDR up: " << mk_pp(proof, m) << "\n";);
+ // TRACE("pdr", tout << "PDR up: " << proof << "\n";);
return proof;
}
diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h
index 35b9067b2..ad4b44d90 100644
--- a/src/muz/pdr/pdr_context.h
+++ b/src/muz/pdr/pdr_context.h
@@ -268,7 +268,6 @@ namespace pdr {
void enqueue_leaf(model_node* n); // add leaf to priority queue.
void update_models();
void set_leaf(model_node& n); // Set node as leaf, remove children.
- bool is_repeated(model_node& n) const;
unsigned num_goals() const;
public:
From 6e1c246454930377bb14f249e3827db29878050b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 16 Nov 2015 23:06:04 -0800
Subject: [PATCH 05/14] avoid exception in Ratul's environment
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
scripts/mk_util.py | 2 ++
1 file changed, 2 insertions(+)
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 0b924c21f..407c78e13 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2653,6 +2653,8 @@ def mk_z3consts_py(api_files):
z3consts.write('%s = %s\n' % (k, i))
z3consts.write('\n')
mode = SEARCHING
+ elif len(words) <= 2:
+ pass
else:
if words[2] != '':
if len(words[2]) > 1 and words[2][1] == 'x':
From 70069e0ae1042ade02fa0a69b3400fc905d58b67 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 17 Nov 2015 13:50:11 +0000
Subject: [PATCH 06/14] Fixed regular expressions in to expect cross-platform
newlines.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
scripts/mk_util.py | 8 +++++---
1 file changed, 5 insertions(+), 3 deletions(-)
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 407c78e13..67b60cbaf 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2592,7 +2592,7 @@ def mk_z3consts_py(api_files):
if Z3PY_SRC_DIR is None:
raise MKException("You must invoke set_z3py_dir(path):")
- blank_pat = re.compile("^ *$")
+ blank_pat = re.compile("^ *\r?$")
comment_pat = re.compile("^ *//.*$")
typedef_pat = re.compile("typedef enum *")
typedef2_pat = re.compile("typedef enum { *")
@@ -2654,7 +2654,7 @@ def mk_z3consts_py(api_files):
z3consts.write('\n')
mode = SEARCHING
elif len(words) <= 2:
- pass
+ assert False, "Invalid %s, line: %s" % (api_file, linenum)
else:
if words[2] != '':
if len(words[2]) > 1 and words[2][1] == 'x':
@@ -2672,7 +2672,7 @@ def mk_z3consts_py(api_files):
# Extract enumeration types from z3_api.h, and add .Net definitions
def mk_z3consts_dotnet(api_files):
- blank_pat = re.compile("^ *$")
+ blank_pat = re.compile("^ *\r?$")
comment_pat = re.compile("^ *//.*$")
typedef_pat = re.compile("typedef enum *")
typedef2_pat = re.compile("typedef enum { *")
@@ -2742,6 +2742,8 @@ def mk_z3consts_dotnet(api_files):
z3consts.write(' %s = %s,\n' % (k, i))
z3consts.write(' }\n\n')
mode = SEARCHING
+ elif len(words) <= 2:
+ assert False, "Invalid %s, line: %s" % (api_file, linenum)
else:
if words[2] != '':
if len(words[2]) > 1 and words[2][1] == 'x':
From fc05eb65bd7195e5baef7af0b3645c63e3dbd997 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 17 Nov 2015 13:50:11 +0000
Subject: [PATCH 07/14] Fixed regular expressions in build scripts to expect
cross-platform newlines.
---
scripts/mk_util.py | 8 +++++---
1 file changed, 5 insertions(+), 3 deletions(-)
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 407c78e13..67b60cbaf 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2592,7 +2592,7 @@ def mk_z3consts_py(api_files):
if Z3PY_SRC_DIR is None:
raise MKException("You must invoke set_z3py_dir(path):")
- blank_pat = re.compile("^ *$")
+ blank_pat = re.compile("^ *\r?$")
comment_pat = re.compile("^ *//.*$")
typedef_pat = re.compile("typedef enum *")
typedef2_pat = re.compile("typedef enum { *")
@@ -2654,7 +2654,7 @@ def mk_z3consts_py(api_files):
z3consts.write('\n')
mode = SEARCHING
elif len(words) <= 2:
- pass
+ assert False, "Invalid %s, line: %s" % (api_file, linenum)
else:
if words[2] != '':
if len(words[2]) > 1 and words[2][1] == 'x':
@@ -2672,7 +2672,7 @@ def mk_z3consts_py(api_files):
# Extract enumeration types from z3_api.h, and add .Net definitions
def mk_z3consts_dotnet(api_files):
- blank_pat = re.compile("^ *$")
+ blank_pat = re.compile("^ *\r?$")
comment_pat = re.compile("^ *//.*$")
typedef_pat = re.compile("typedef enum *")
typedef2_pat = re.compile("typedef enum { *")
@@ -2742,6 +2742,8 @@ def mk_z3consts_dotnet(api_files):
z3consts.write(' %s = %s,\n' % (k, i))
z3consts.write(' }\n\n')
mode = SEARCHING
+ elif len(words) <= 2:
+ assert False, "Invalid %s, line: %s" % (api_file, linenum)
else:
if words[2] != '':
if len(words[2]) > 1 and words[2][1] == 'x':
From 66fc873613a80c5f2935fbeb29ced4ae8ec2b405 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 17 Nov 2015 09:00:16 -0800
Subject: [PATCH 08/14] Fix for #322: PDR engine cannot falls back on fixed
size arithmetic for difference logic. It would eventually overflow and cause
incorrect model construction. Enable only fixed-size arithmetic when
configuration allows it
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/smt_setup.cpp | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 524dbeab6..edb4f1e55 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -721,8 +721,8 @@ namespace smt {
IF_VERBOSE(100, verbose_stream() << "(smt.collecting-features)\n";);
st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas());
IF_VERBOSE(1000, st.display_primitive(verbose_stream()););
- bool fixnum = st.arith_k_sum_is_small();
- bool int_only = !st.m_has_rational && !st.m_has_real;
+ bool fixnum = st.arith_k_sum_is_small() && m_params.m_arith_fixnum;
+ bool int_only = !st.m_has_rational && !st.m_has_real && m_params.m_arith_int_only;
switch(m_params.m_arith_mode) {
case AS_NO_ARITH:
m_context.register_plugin(alloc(smt::theory_dummy, m_manager.mk_family_id("arith"), "no arithmetic"));
From d6d301c5ebe10c584798ddfd5f54128d4d83526f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 17 Nov 2015 18:38:37 -0800
Subject: [PATCH 09/14] fix for mising handling of quantifiers in tactic. Bug
#324
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/tactic/arith/eq2bv_tactic.cpp | 14 ++++++++------
1 file changed, 8 insertions(+), 6 deletions(-)
diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp
index b84d5567c..7cba66a5a 100644
--- a/src/tactic/arith/eq2bv_tactic.cpp
+++ b/src/tactic/arith/eq2bv_tactic.cpp
@@ -305,14 +305,16 @@ public:
m_nonfd.mark(f, true);
expr* e1, *e2;
if (m.is_eq(f, e1, e2)) {
- if (is_fd(e1, e2)) {
+ if (is_fd(e1, e2) || is_fd(e2, e1)) {
continue;
- }
- if (is_fd(e2, e1)) {
- continue;
- }
+ }
}
- m_todo.append(to_app(f)->get_num_args(), to_app(f)->get_args());
+ if (is_app(f)) {
+ m_todo.append(to_app(f)->get_num_args(), to_app(f)->get_args());
+ }
+ else if (is_quantifier(f)) {
+ m_todo.push_back(to_quantifier(f)->get_expr());
+ }
}
}
From 04b0e3c2f74c318d52de5fa7fb3324d95b89bf56 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 17 Nov 2015 18:48:52 -0800
Subject: [PATCH 10/14] add checks for cancellation inside mam to agilely not
ignore Rustan's soft requests for a timeout #326
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/mam.cpp | 9 +++++++++
1 file changed, 9 insertions(+)
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index d92eef5b8..d22ca88db 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -3646,6 +3646,9 @@ namespace smt {
approx_set::iterator it1 = plbls1.begin();
approx_set::iterator end1 = plbls1.end();
for (; it1 != end1; ++it1) {
+ if (m_context.get_cancel_flag()) {
+ break;
+ }
unsigned plbl1 = *it1;
SASSERT(plbls1.may_contain(plbl1));
approx_set::iterator it2 = plbls2.begin();
@@ -3687,6 +3690,9 @@ namespace smt {
approx_set::iterator it1 = plbls.begin();
approx_set::iterator end1 = plbls.end();
for (; it1 != end1; ++it1) {
+ if (m_context.get_cancel_flag()) {
+ break;
+ }
unsigned plbl1 = *it1;
SASSERT(plbls.may_contain(plbl1));
approx_set::iterator it2 = clbls.begin();
@@ -3706,6 +3712,9 @@ namespace smt {
svector<qp_pair>::iterator it1 = m_new_patterns.begin();
svector<qp_pair>::iterator end1 = m_new_patterns.end();
for (; it1 != end1; ++it1) {
+ if (m_context.get_cancel_flag()) {
+ break;
+ }
quantifier * qa = it1->first;
app * mp = it1->second;
SASSERT(m_ast_manager.is_pattern(mp));
From d7c3e77b66414d1d10f1df73b6b1a792496710e6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 17 Nov 2015 18:59:43 -0800
Subject: [PATCH 11/14] port test_capi.c to use mostly essentially
non-deprecated APIs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
examples/c/test_capi.c | 489 ++++++++++++++++++++++++-----------------
1 file changed, 291 insertions(+), 198 deletions(-)
diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c
index 11306a98b..385035361 100644
--- a/examples/c/test_capi.c
+++ b/examples/c/test_capi.c
@@ -83,6 +83,18 @@ Z3_context mk_context_custom(Z3_config cfg, Z3_error_handler err)
return ctx;
}
+Z3_solver mk_solver(Z3_context ctx)
+{
+ Z3_solver s = Z3_mk_solver(ctx);
+ Z3_solver_inc_ref(ctx, s);
+ return s;
+}
+
+void del_solver(Z3_context ctx, Z3_solver s)
+{
+ Z3_solver_dec_ref(ctx, s);
+}
+
/**
\brief Create a logical context.
@@ -184,28 +196,30 @@ Z3_ast mk_binary_app(Z3_context ctx, Z3_func_decl f, Z3_ast x, Z3_ast y)
\brief Check whether the logical context is satisfiable, and compare the result with the expected result.
If the context is satisfiable, then display the model.
*/
-void check(Z3_context ctx, Z3_lbool expected_result)
+void check(Z3_context ctx, Z3_solver s, Z3_lbool expected_result)
{
Z3_model m = 0;
- Z3_lbool result = Z3_check_and_get_model(ctx, &m);
+ Z3_lbool result = Z3_solver_check(ctx, s);
switch (result) {
case Z3_L_FALSE:
printf("unsat\n");
break;
case Z3_L_UNDEF:
- printf("unknown\n");
+ printf("unknown\n");
+ m = Z3_solver_get_model(ctx, s);
+ if (m) Z3_model_inc_ref(ctx, m);
printf("potential model:\n%s\n", Z3_model_to_string(ctx, m));
break;
case Z3_L_TRUE:
+ m = Z3_solver_get_model(ctx, s);
+ if (m) Z3_model_inc_ref(ctx, m);
printf("sat\n%s\n", Z3_model_to_string(ctx, m));
break;
}
- if (m) {
- Z3_del_model(ctx, m);
- }
if (result != expected_result) {
exitf("unexpected result");
}
+ if (m) Z3_model_dec_ref(ctx, m);
}
/**
@@ -218,20 +232,18 @@ void check(Z3_context ctx, Z3_lbool expected_result)
The context \c ctx is not modified by this function.
*/
-void prove(Z3_context ctx, Z3_ast f, Z3_bool is_valid)
+void prove(Z3_context ctx, Z3_solver s, Z3_ast f, Z3_bool is_valid)
{
- Z3_model m;
+ Z3_model m = 0;
Z3_ast not_f;
/* save the current state of the context */
- Z3_push(ctx);
+ Z3_solver_push(ctx, s);
not_f = Z3_mk_not(ctx, f);
- Z3_assert_cnstr(ctx, not_f);
-
- m = 0;
-
- switch (Z3_check_and_get_model(ctx, &m)) {
+ Z3_solver_assert(ctx, s, not_f);
+
+ switch (Z3_solver_check(ctx, s)) {
case Z3_L_FALSE:
/* proved */
printf("valid\n");
@@ -242,9 +254,11 @@ void prove(Z3_context ctx, Z3_ast f, Z3_bool is_valid)
case Z3_L_UNDEF:
/* Z3 failed to prove/disprove f. */
printf("unknown\n");
+ m = Z3_solver_get_model(ctx, s);
if (m != 0) {
+ Z3_model_inc_ref(ctx, m);
/* m should be viewed as a potential counterexample. */
- printf("potential counterexample:\n%s\n", Z3_model_to_string(ctx, m));
+ printf("potential counterexample:\n%s\n", Z3_model_to_string(ctx, m));
}
if (is_valid) {
exitf("unexpected result");
@@ -253,7 +267,9 @@ void prove(Z3_context ctx, Z3_ast f, Z3_bool is_valid)
case Z3_L_TRUE:
/* disproved */
printf("invalid\n");
+ m = Z3_solver_get_model(ctx, s);
if (m) {
+ Z3_model_inc_ref(ctx, m);
/* the model returned by Z3 is a counterexample */
printf("counterexample:\n%s\n", Z3_model_to_string(ctx, m));
}
@@ -262,13 +278,10 @@ void prove(Z3_context ctx, Z3_ast f, Z3_bool is_valid)
}
break;
}
+ if (m) Z3_model_dec_ref(ctx, m);
- if (m) {
- Z3_del_model(ctx, m);
- }
-
- /* restore context */
- Z3_pop(ctx, 1);
+ /* restore scope */
+ Z3_solver_pop(ctx, s, 1);
}
/**
@@ -281,7 +294,7 @@ void prove(Z3_context ctx, Z3_ast f, Z3_bool is_valid)
Where, \c finv is a fresh function declaration.
*/
-void assert_inj_axiom(Z3_context ctx, Z3_func_decl f, unsigned i)
+void assert_inj_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f, unsigned i)
{
unsigned sz, j;
Z3_sort finv_domain, finv_range;
@@ -339,7 +352,7 @@ void assert_inj_axiom(Z3_context ctx, Z3_func_decl f, unsigned i)
names,
eq);
printf("assert axiom:\n%s\n", Z3_ast_to_string(ctx, q));
- Z3_assert_cnstr(ctx, q);
+ Z3_solver_assert(ctx, s, q);
/* free temporary arrays */
free(types);
@@ -352,7 +365,7 @@ void assert_inj_axiom(Z3_context ctx, Z3_func_decl f, unsigned i)
This example uses the SMT-LIB parser to simplify the axiom construction.
*/
-void assert_comm_axiom(Z3_context ctx, Z3_func_decl f)
+void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f)
{
Z3_sort t;
Z3_symbol f_name, t_name;
@@ -379,7 +392,7 @@ void assert_comm_axiom(Z3_context ctx, Z3_func_decl f)
1, &f_name, &f);
q = Z3_get_smtlib_formula(ctx, 0);
printf("assert axiom:\n%s\n", Z3_ast_to_string(ctx, q));
- Z3_assert_cnstr(ctx, q);
+ Z3_solver_assert(ctx, s, q);
}
/**
@@ -554,42 +567,50 @@ void display_function_interpretations(Z3_context c, FILE * out, Z3_model m)
fprintf(out, "function interpretations:\n");
- num_functions = Z3_get_model_num_funcs(c, m);
+ num_functions = Z3_model_get_num_funcs(c, m);
for (i = 0; i < num_functions; i++) {
Z3_func_decl fdecl;
Z3_symbol name;
Z3_ast func_else;
- unsigned num_entries, j;
+ unsigned num_entries = 0, j;
+ Z3_func_interp_opt finterp;
- fdecl = Z3_get_model_func_decl(c, m, i);
+ fdecl = Z3_model_get_func_decl(c, m, i);
+ finterp = Z3_model_get_func_interp(c, m, fdecl);
+ Z3_func_interp_inc_ref(c, finterp);
name = Z3_get_decl_name(c, fdecl);
display_symbol(c, out, name);
fprintf(out, " = {");
- num_entries = Z3_get_model_func_num_entries(c, m, i);
+ if (finterp)
+ num_entries = Z3_func_interp_get_num_entries(c, finterp);
for (j = 0; j < num_entries; j++) {
unsigned num_args, k;
+ Z3_func_entry fentry = Z3_func_interp_get_entry(c, finterp, j);
+ Z3_func_entry_inc_ref(c, fentry);
if (j > 0) {
fprintf(out, ", ");
}
- num_args = Z3_get_model_func_entry_num_args(c, m, i, j);
+ num_args = Z3_func_entry_get_num_args(c, fentry);
fprintf(out, "(");
for (k = 0; k < num_args; k++) {
if (k > 0) {
fprintf(out, ", ");
}
- display_ast(c, out, Z3_get_model_func_entry_arg(c, m, i, j, k));
+ display_ast(c, out, Z3_func_entry_get_arg(c, fentry, k));
}
fprintf(out, "|->");
- display_ast(c, out, Z3_get_model_func_entry_value(c, m, i, j));
+ display_ast(c, out, Z3_func_entry_get_value(c, fentry));
fprintf(out, ")");
+ Z3_func_entry_dec_ref(c, fentry);
}
if (num_entries > 0) {
fprintf(out, ", ");
}
fprintf(out, "(else|->");
- func_else = Z3_get_model_func_else(c, m, i);
+ func_else = Z3_func_interp_get_else(c, finterp);
display_ast(c, out, func_else);
fprintf(out, ")}\n");
+ Z3_func_interp_dec_ref(c, finterp);
}
}
@@ -601,10 +622,12 @@ void display_model(Z3_context c, FILE * out, Z3_model m)
unsigned num_constants;
unsigned i;
- num_constants = Z3_get_model_num_constants(c, m);
+ if (!m) return;
+
+ num_constants = Z3_model_get_num_consts(c, m);
for (i = 0; i < num_constants; i++) {
Z3_symbol name;
- Z3_func_decl cnst = Z3_get_model_constant(c, m, i);
+ Z3_func_decl cnst = Z3_model_get_const_decl(c, m, i);
Z3_ast a, v;
Z3_bool ok;
name = Z3_get_decl_name(c, cnst);
@@ -612,7 +635,7 @@ void display_model(Z3_context c, FILE * out, Z3_model m)
fprintf(out, " = ");
a = Z3_mk_app(c, cnst, 0, 0);
v = a;
- ok = Z3_eval(c, m, a, &v);
+ ok = Z3_model_eval(c, m, a, 1, &v);
display_ast(c, out, v);
fprintf(out, "\n");
}
@@ -622,10 +645,10 @@ void display_model(Z3_context c, FILE * out, Z3_model m)
/**
\brief Similar to #check, but uses #display_model instead of #Z3_model_to_string.
*/
-void check2(Z3_context ctx, Z3_lbool expected_result)
+void check2(Z3_context ctx, Z3_solver s, Z3_lbool expected_result)
{
Z3_model m = 0;
- Z3_lbool result = Z3_check_and_get_model(ctx, &m);
+ Z3_lbool result = Z3_solver_check(ctx, s);
switch (result) {
case Z3_L_FALSE:
printf("unsat\n");
@@ -633,19 +656,22 @@ void check2(Z3_context ctx, Z3_lbool expected_result)
case Z3_L_UNDEF:
printf("unknown\n");
printf("potential model:\n");
+ m = Z3_solver_get_model(ctx, s);
+ if (m) Z3_model_inc_ref(ctx, m);
display_model(ctx, stdout, m);
break;
case Z3_L_TRUE:
printf("sat\n");
+ m = Z3_solver_get_model(ctx, s);
+ if (m) Z3_model_inc_ref(ctx, m);
display_model(ctx, stdout, m);
break;
}
- if (m) {
- Z3_del_model(ctx, m);
- }
if (result != expected_result) {
exitf("unexpected result");
}
+ if (m) Z3_model_dec_ref(ctx, m);
+
}
/**
@@ -674,9 +700,6 @@ void simple_example()
ctx = mk_context();
- /* do something with the context */
- printf("CONTEXT:\n%sEND OF CONTEXT\n", Z3_context_to_string(ctx));
-
/* delete logical context */
Z3_del_context(ctx);
}
@@ -689,6 +712,7 @@ void demorgan()
{
Z3_config cfg;
Z3_context ctx;
+ Z3_solver s;
Z3_sort bool_sort;
Z3_symbol symbol_x, symbol_y;
Z3_ast x, y, not_x, not_y, x_and_y, ls, rs, conjecture, negated_conjecture;
@@ -719,9 +743,10 @@ void demorgan()
rs = Z3_mk_or(ctx, 2, args);
conjecture = Z3_mk_iff(ctx, ls, rs);
negated_conjecture = Z3_mk_not(ctx, conjecture);
-
- Z3_assert_cnstr(ctx, negated_conjecture);
- switch (Z3_check(ctx)) {
+
+ s = mk_solver(ctx);
+ Z3_solver_assert(ctx, s, negated_conjecture);
+ switch (Z3_solver_check(ctx, s)) {
case Z3_L_FALSE:
/* The negated conjecture was unsatisfiable, hence the conjecture is valid */
printf("DeMorgan is valid\n");
@@ -735,6 +760,7 @@ void demorgan()
printf("DeMorgan is not valid\n");
break;
}
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -745,21 +771,24 @@ void find_model_example1()
{
Z3_context ctx;
Z3_ast x, y, x_xor_y;
+ Z3_solver s;
printf("\nfind_model_example1\n");
LOG_MSG("find_model_example1");
ctx = mk_context();
+ s = mk_solver(ctx);
x = mk_bool_var(ctx, "x");
y = mk_bool_var(ctx, "y");
x_xor_y = Z3_mk_xor(ctx, x, y);
- Z3_assert_cnstr(ctx, x_xor_y);
+ Z3_solver_assert(ctx, s, x_xor_y);
printf("model for: x xor y\n");
- check(ctx, Z3_L_TRUE);
+ check(ctx, s, Z3_L_TRUE);
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -774,11 +803,13 @@ void find_model_example2()
Z3_ast x_eq_y;
Z3_ast args[2];
Z3_ast c1, c2, c3;
+ Z3_solver s;
printf("\nfind_model_example2\n");
LOG_MSG("find_model_example2");
ctx = mk_context();
+ s = mk_solver(ctx);
x = mk_int_var(ctx, "x");
y = mk_int_var(ctx, "y");
one = mk_int(ctx, 1);
@@ -791,20 +822,21 @@ void find_model_example2()
c1 = Z3_mk_lt(ctx, x, y_plus_one);
c2 = Z3_mk_gt(ctx, x, two);
- Z3_assert_cnstr(ctx, c1);
- Z3_assert_cnstr(ctx, c2);
+ Z3_solver_assert(ctx, s, c1);
+ Z3_solver_assert(ctx, s, c2);
printf("model for: x < y + 1, x > 2\n");
- check(ctx, Z3_L_TRUE);
+ check(ctx, s, Z3_L_TRUE);
/* assert not(x = y) */
x_eq_y = Z3_mk_eq(ctx, x, y);
c3 = Z3_mk_not(ctx, x_eq_y);
- Z3_assert_cnstr(ctx, c3);
+ Z3_solver_assert(ctx, s,c3);
printf("model for: x < y + 1, x > 2, not(x = y)\n");
- check(ctx, Z3_L_TRUE);
+ check(ctx, s, Z3_L_TRUE);
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -818,6 +850,7 @@ void find_model_example2()
void prove_example1()
{
Z3_context ctx;
+ Z3_solver s;
Z3_symbol U_name, g_name, x_name, y_name;
Z3_sort U;
Z3_sort g_domain[1];
@@ -829,7 +862,8 @@ void prove_example1()
LOG_MSG("prove_example1");
ctx = mk_context();
-
+ s = mk_solver(ctx);
+
/* create uninterpreted type. */
U_name = Z3_mk_string_symbol(ctx, "U");
U = Z3_mk_uninterpreted_sort(ctx, U_name);
@@ -850,12 +884,12 @@ void prove_example1()
/* assert x = y */
eq = Z3_mk_eq(ctx, x, y);
- Z3_assert_cnstr(ctx, eq);
+ Z3_solver_assert(ctx, s, eq);
/* prove g(x) = g(y) */
f = Z3_mk_eq(ctx, gx, gy);
printf("prove: x = y implies g(x) = g(y)\n");
- prove(ctx, f, Z3_TRUE);
+ prove(ctx, s, f, Z3_TRUE);
/* create g(g(x)) */
ggx = mk_unary_app(ctx, g, gx);
@@ -863,8 +897,9 @@ void prove_example1()
/* disprove g(g(x)) = g(y) */
f = Z3_mk_eq(ctx, ggx, gy);
printf("disprove: x = y implies g(g(x)) = g(y)\n");
- prove(ctx, f, Z3_FALSE);
+ prove(ctx, s, f, Z3_FALSE);
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -877,6 +912,7 @@ void prove_example1()
void prove_example2()
{
Z3_context ctx;
+ Z3_solver s;
Z3_sort int_sort;
Z3_symbol g_name;
Z3_sort g_domain[1];
@@ -889,6 +925,7 @@ void prove_example2()
LOG_MSG("prove_example2");
ctx = mk_context();
+ s = mk_solver(ctx);
/* declare function g */
int_sort = Z3_mk_int_sort(ctx);
@@ -916,30 +953,31 @@ void prove_example2()
ggx_gy = mk_unary_app(ctx, g, gx_gy);
eq = Z3_mk_eq(ctx, ggx_gy, gz);
c1 = Z3_mk_not(ctx, eq);
- Z3_assert_cnstr(ctx, c1);
+ Z3_solver_assert(ctx, s, c1);
/* assert x + z <= y */
args[0] = x;
args[1] = z;
x_plus_z = Z3_mk_add(ctx, 2, args);
c2 = Z3_mk_le(ctx, x_plus_z, y);
- Z3_assert_cnstr(ctx, c2);
+ Z3_solver_assert(ctx, s, c2);
/* assert y <= x */
c3 = Z3_mk_le(ctx, y, x);
- Z3_assert_cnstr(ctx, c3);
+ Z3_solver_assert(ctx, s, c3);
/* prove z < 0 */
f = Z3_mk_lt(ctx, z, zero);
printf("prove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0\n");
- prove(ctx, f, Z3_TRUE);
+ prove(ctx, s, f, Z3_TRUE);
/* disprove z < -1 */
minus_one = mk_int(ctx, -1);
f = Z3_mk_lt(ctx, z, minus_one);
printf("disprove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < -1\n");
- prove(ctx, f, Z3_FALSE);
+ prove(ctx, s, f, Z3_FALSE);
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -952,6 +990,7 @@ void prove_example2()
void push_pop_example1()
{
Z3_context ctx;
+ Z3_solver s;
Z3_sort int_sort;
Z3_symbol x_sym, y_sym;
Z3_ast x, y, big_number, three;
@@ -961,6 +1000,7 @@ void push_pop_example1()
LOG_MSG("push_pop_example1");
ctx = mk_context();
+ s = mk_solver(ctx);
/* create a big number */
int_sort = Z3_mk_int_sort(ctx);
@@ -976,32 +1016,32 @@ void push_pop_example1()
/* assert x >= "big number" */
c1 = Z3_mk_ge(ctx, x, big_number);
printf("assert: x >= 'big number'\n");
- Z3_assert_cnstr(ctx, c1);
+ Z3_solver_assert(ctx, s, c1);
/* create a backtracking point */
printf("push\n");
- Z3_push(ctx);
+ Z3_solver_push(ctx, s);
- printf("number of scopes: %d\n", Z3_get_num_scopes(ctx));
+ printf("number of scopes: %d\n", Z3_solver_get_num_scopes(ctx, s));
/* assert x <= 3 */
c2 = Z3_mk_le(ctx, x, three);
printf("assert: x <= 3\n");
- Z3_assert_cnstr(ctx, c2);
+ Z3_solver_assert(ctx, s, c2);
/* context is inconsistent at this point */
- check2(ctx, Z3_L_FALSE);
+ check2(ctx, s, Z3_L_FALSE);
/* backtrack: the constraint x <= 3 will be removed, since it was
- asserted after the last Z3_push. */
+ asserted after the last Z3_solver_push. */
printf("pop\n");
- Z3_pop(ctx, 1);
+ Z3_solver_pop(ctx, s, 1);
- printf("number of scopes: %d\n", Z3_get_num_scopes(ctx));
+ printf("number of scopes: %d\n", Z3_solver_get_num_scopes(ctx, s));
/* the context is consistent again. */
- check2(ctx, Z3_L_TRUE);
+ check2(ctx, s, Z3_L_TRUE);
/* new constraints can be asserted... */
@@ -1012,11 +1052,12 @@ void push_pop_example1()
/* assert y > x */
c3 = Z3_mk_gt(ctx, y, x);
printf("assert: y > x\n");
- Z3_assert_cnstr(ctx, c3);
+ Z3_solver_assert(ctx, s, c3);
/* the context is still consistent. */
- check2(ctx, Z3_L_TRUE);
+ check2(ctx, s, Z3_L_TRUE);
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -1030,6 +1071,7 @@ void quantifier_example1()
{
Z3_config cfg;
Z3_context ctx;
+ Z3_solver s;
Z3_sort int_sort;
Z3_symbol f_name;
Z3_sort f_domain[2];
@@ -1052,6 +1094,7 @@ void quantifier_example1()
Z3_global_param_set("smt.mbqi.max_iterations", "10");
ctx = mk_context_custom(cfg, error_handler);
Z3_del_config(cfg);
+ s = mk_solver(ctx);
/* declare function f */
int_sort = Z3_mk_int_sort(ctx);
@@ -1061,7 +1104,7 @@ void quantifier_example1()
f = Z3_mk_func_decl(ctx, f_name, 2, f_domain, int_sort);
/* assert that f is injective in the second argument. */
- assert_inj_axiom(ctx, f, 1);
+ assert_inj_axiom(ctx, s, f, 1);
/* create x, y, v, w, fxy, fwv */
x = mk_int_var(ctx, "x");
@@ -1073,26 +1116,23 @@ void quantifier_example1()
/* assert f(x, y) = f(w, v) */
p1 = Z3_mk_eq(ctx, fxy, fwv);
- Z3_assert_cnstr(ctx, p1);
+ Z3_solver_assert(ctx, s, p1);
/* prove f(x, y) = f(w, v) implies y = v */
p2 = Z3_mk_eq(ctx, y, v);
printf("prove: f(x, y) = f(w, v) implies y = v\n");
- prove(ctx, p2, Z3_TRUE);
+ prove(ctx, s, p2, Z3_TRUE);
/* disprove f(x, y) = f(w, v) implies x = w */
/* using check2 instead of prove */
p3 = Z3_mk_eq(ctx, x, w);
not_p3 = Z3_mk_not(ctx, p3);
- Z3_assert_cnstr(ctx, not_p3);
+ Z3_solver_assert(ctx, s, not_p3);
printf("disprove: f(x, y) = f(w, v) implies x = w\n");
printf("that is: not(f(x, y) = f(w, v) implies x = w) is satisfiable\n");
- check2(ctx, Z3_L_UNDEF);
- printf("reason for last failure: %d (7 = quantifiers)\n",
- Z3_get_search_failure(ctx));
- if (Z3_get_search_failure(ctx) != Z3_QUANTIFIERS) {
- exitf("unexpected result");
- }
+ check2(ctx, s, Z3_L_UNDEF);
+ printf("reason for last failure: %s\n", Z3_solver_get_reason_unknown(ctx, s));
+ del_solver(ctx, s);
Z3_del_context(ctx);
/* reset global parameters set by this function */
Z3_global_param_reset_all();
@@ -1105,7 +1145,8 @@ void quantifier_example1()
*/
void array_example1()
{
- Z3_context ctx;
+ Z3_context ctx = mk_context();
+ Z3_solver s = mk_solver(ctx);
Z3_sort int_sort, array_sort;
Z3_ast a1, a2, i1, v1, i2, v2, i3;
Z3_ast st1, st2, sel1, sel2;
@@ -1116,7 +1157,6 @@ void array_example1()
printf("\narray_example1\n");
LOG_MSG("array_example1");
- ctx = mk_context();
int_sort = Z3_mk_int_sort(ctx);
array_sort = Z3_mk_array_sort(ctx, int_sort, int_sort);
@@ -1148,8 +1188,9 @@ void array_example1()
thm = Z3_mk_implies(ctx, antecedent, consequent);
printf("prove: store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3))\n");
printf("%s\n", Z3_ast_to_string(ctx, thm));
- prove(ctx, thm, Z3_TRUE);
+ prove(ctx, s, thm, Z3_TRUE);
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -1163,6 +1204,7 @@ void array_example1()
void array_example2()
{
Z3_context ctx;
+ Z3_solver s;
Z3_sort bool_sort, array_sort;
Z3_ast a[5];
Z3_ast d;
@@ -1174,6 +1216,7 @@ void array_example2()
for (n = 2; n <= 5; n++) {
printf("n = %d\n", n);
ctx = mk_context();
+ s = mk_solver(ctx);
bool_sort = Z3_mk_bool_sort(ctx);
array_sort = Z3_mk_array_sort(ctx, bool_sort, bool_sort);
@@ -1187,11 +1230,12 @@ void array_example2()
/* assert distinct(a[0], ..., a[n]) */
d = Z3_mk_distinct(ctx, n, a);
printf("%s\n", Z3_ast_to_string(ctx, d));
- Z3_assert_cnstr(ctx, d);
+ Z3_solver_assert(ctx, s, d);
/* context is satisfiable if n < 5 */
- check2(ctx, n < 5 ? Z3_L_TRUE : Z3_L_FALSE);
+ check2(ctx, s, n < 5 ? Z3_L_TRUE : Z3_L_FALSE);
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
}
@@ -1201,13 +1245,13 @@ void array_example2()
*/
void array_example3()
{
- Z3_context ctx;
+ Z3_context ctx = mk_context();
+ Z3_solver s = mk_solver(ctx);
Z3_sort bool_sort, int_sort, array_sort;
Z3_sort domain, range;
printf("\narray_example3\n");
LOG_MSG("array_example3");
- ctx = mk_context();
bool_sort = Z3_mk_bool_sort(ctx);
int_sort = Z3_mk_int_sort(ctx);
@@ -1231,6 +1275,7 @@ void array_example3()
exitf("invalid array type");
}
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -1239,7 +1284,8 @@ void array_example3()
*/
void tuple_example1()
{
- Z3_context ctx;
+ Z3_context ctx = mk_context();
+ Z3_solver s = mk_solver(ctx);
Z3_sort real_sort, pair_sort;
Z3_symbol mk_tuple_name;
Z3_func_decl mk_tuple_decl;
@@ -1251,7 +1297,6 @@ void tuple_example1()
printf("\ntuple_example1\n");
LOG_MSG("tuple_example1");
- ctx = mk_context();
real_sort = Z3_mk_real_sort(ctx);
@@ -1284,13 +1329,13 @@ void tuple_example1()
eq2 = Z3_mk_eq(ctx, x, one);
thm = Z3_mk_implies(ctx, eq1, eq2);
printf("prove: get_x(mk_pair(x, y)) = 1 implies x = 1\n");
- prove(ctx, thm, Z3_TRUE);
+ prove(ctx, s, thm, Z3_TRUE);
/* disprove that get_x(mk_pair(x,y)) == 1 implies y = 1*/
eq3 = Z3_mk_eq(ctx, y, one);
thm = Z3_mk_implies(ctx, eq1, eq3);
printf("disprove: get_x(mk_pair(x, y)) = 1 implies y = 1\n");
- prove(ctx, thm, Z3_FALSE);
+ prove(ctx, s, thm, Z3_FALSE);
}
{
@@ -1311,12 +1356,12 @@ void tuple_example1()
consequent = Z3_mk_eq(ctx, p1, p2);
thm = Z3_mk_implies(ctx, antecedent, consequent);
printf("prove: get_x(p1) = get_x(p2) and get_y(p1) = get_y(p2) implies p1 = p2\n");
- prove(ctx, thm, Z3_TRUE);
+ prove(ctx, s, thm, Z3_TRUE);
/* disprove that get_x(p1) = get_x(p2) implies p1 = p2 */
thm = Z3_mk_implies(ctx, antecedents[0], consequent);
printf("disprove: get_x(p1) = get_x(p2) implies p1 = p2\n");
- prove(ctx, thm, Z3_FALSE);
+ prove(ctx, s, thm, Z3_FALSE);
}
{
@@ -1335,16 +1380,17 @@ void tuple_example1()
consequent = Z3_mk_eq(ctx, x, ten);
thm = Z3_mk_implies(ctx, antecedent, consequent);
printf("prove: p2 = update(p1, 0, 10) implies get_x(p2) = 10\n");
- prove(ctx, thm, Z3_TRUE);
+ prove(ctx, s, thm, Z3_TRUE);
/* disprove that p2 = update(p1, 0, 10) implies get_y(p2) = 10 */
y = mk_unary_app(ctx, get_y_decl, p2);
consequent = Z3_mk_eq(ctx, y, ten);
thm = Z3_mk_implies(ctx, antecedent, consequent);
printf("disprove: p2 = update(p1, 0, 10) implies get_y(p2) = 10\n");
- prove(ctx, thm, Z3_FALSE);
+ prove(ctx, s, thm, Z3_FALSE);
}
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -1353,14 +1399,14 @@ void tuple_example1()
*/
void bitvector_example1()
{
- Z3_context ctx;
+ Z3_context ctx = mk_context();
+ Z3_solver s = mk_solver(ctx);
Z3_sort bv_sort;
Z3_ast x, zero, ten, x_minus_ten, c1, c2, thm;
printf("\nbitvector_example1\n");
LOG_MSG("bitvector_example1");
- ctx = mk_context();
bv_sort = Z3_mk_bv_sort(ctx, 32);
@@ -1373,8 +1419,9 @@ void bitvector_example1()
c2 = Z3_mk_bvsle(ctx, x_minus_ten, zero);
thm = Z3_mk_iff(ctx, c1, c2);
printf("disprove: x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers\n");
- prove(ctx, thm, Z3_FALSE);
+ prove(ctx, s, thm, Z3_FALSE);
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -1384,6 +1431,7 @@ void bitvector_example1()
void bitvector_example2()
{
Z3_context ctx = mk_context();
+ Z3_solver s = mk_solver(ctx);
/* construct x ^ y - 103 == x * y */
Z3_sort bv_sort = Z3_mk_bv_sort(ctx, 32);
@@ -1400,11 +1448,12 @@ void bitvector_example2()
printf("find values of x and y, such that x ^ y - 103 == x * y\n");
/* add the constraint <tt>x ^ y - 103 == x * y<\tt> to the logical context */
- Z3_assert_cnstr(ctx, ctr);
+ Z3_solver_assert(ctx, s, ctr);
/* find a model (i.e., values for x an y that satisfy the constraint */
- check(ctx, Z3_L_TRUE);
+ check(ctx, s, Z3_L_TRUE);
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -1413,36 +1462,38 @@ void bitvector_example2()
*/
void eval_example1()
{
- Z3_context ctx;
+ Z3_context ctx = mk_context();
+ Z3_solver s = mk_solver(ctx);
Z3_ast x, y, two;
Z3_ast c1, c2;
- Z3_model m;
+ Z3_model m = 0;
printf("\neval_example1\n");
LOG_MSG("eval_example1");
- ctx = mk_context();
x = mk_int_var(ctx, "x");
y = mk_int_var(ctx, "y");
two = mk_int(ctx, 2);
/* assert x < y */
c1 = Z3_mk_lt(ctx, x, y);
- Z3_assert_cnstr(ctx, c1);
+ Z3_solver_assert(ctx, s, c1);
/* assert x > 2 */
c2 = Z3_mk_gt(ctx, x, two);
- Z3_assert_cnstr(ctx, c2);
+ Z3_solver_assert(ctx, s, c2);
/* find model for the constraints above */
- if (Z3_check_and_get_model(ctx, &m) == Z3_L_TRUE) {
+ if (Z3_solver_check(ctx, s) == Z3_L_TRUE) {
Z3_ast x_plus_y;
Z3_ast args[2] = {x, y};
Z3_ast v;
+ m = Z3_solver_get_model(ctx, s);
+ if (m) Z3_model_inc_ref(ctx, m);
printf("MODEL:\n%s", Z3_model_to_string(ctx, m));
x_plus_y = Z3_mk_add(ctx, 2, args);
printf("\nevaluating x+y\n");
- if (Z3_eval(ctx, m, x_plus_y, &v)) {
+ if (Z3_model_eval(ctx, m, x_plus_y, 1, &v)) {
printf("result = ");
display_ast(ctx, stdout, v);
printf("\n");
@@ -1450,12 +1501,13 @@ void eval_example1()
else {
exitf("failed to evaluate: x+y");
}
- Z3_del_model(ctx, m);
}
else {
exitf("the constraints are satisfiable");
}
+ if (m) Z3_model_dec_ref(ctx, m);
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -1492,6 +1544,7 @@ void error_code_example1()
{
Z3_config cfg;
Z3_context ctx;
+ Z3_solver s;
Z3_ast x;
Z3_model m;
Z3_ast v;
@@ -1505,16 +1558,19 @@ void error_code_example1()
cfg = Z3_mk_config();
ctx = mk_context_custom(cfg, NULL);
Z3_del_config(cfg);
+ s = mk_solver(ctx);
x = mk_bool_var(ctx, "x");
x_decl = Z3_get_app_decl(ctx, Z3_to_app(ctx, x));
- Z3_assert_cnstr(ctx, x);
+ Z3_solver_assert(ctx, s, x);
- if (Z3_check_and_get_model(ctx, &m) != Z3_L_TRUE) {
+ if (Z3_solver_check(ctx, s) != Z3_L_TRUE) {
exitf("unexpected result");
}
- if (!Z3_eval_func_decl(ctx, m, x_decl, &v)) {
+ m = Z3_solver_get_model(ctx, s);
+ if (m) Z3_model_inc_ref(ctx, m);
+ if (!Z3_model_eval(ctx, m, x, 1, &v)) {
exitf("did not obtain value for declaration.\n");
}
if (Z3_get_error_code(ctx) == Z3_OK) {
@@ -1525,7 +1581,8 @@ void error_code_example1()
if (Z3_get_error_code(ctx) != Z3_OK) {
printf("last call failed.\n");
}
- Z3_del_model(ctx, m);
+ if (m) Z3_model_dec_ref(ctx, m);
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -1558,7 +1615,7 @@ void error_code_example2() {
Z3_del_context(ctx);
}
else {
- printf("Z3 error: %s.\n", Z3_get_error_msg((Z3_error_code)r));
+ printf("Z3 error: %s.\n", Z3_get_error_msg_ex(ctx, (Z3_error_code)r));
if (ctx != NULL) {
Z3_del_context(ctx);
}
@@ -1570,13 +1627,13 @@ void error_code_example2() {
*/
void parser_example1()
{
- Z3_context ctx;
+ Z3_context ctx = mk_context();
+ Z3_solver s = mk_solver(ctx);
unsigned i, num_formulas;
printf("\nparser_example1\n");
LOG_MSG("parser_example1");
- ctx = mk_context();
Z3_parse_smtlib_string(ctx,
"(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))",
@@ -1586,11 +1643,12 @@ void parser_example1()
for (i = 0; i < num_formulas; i++) {
Z3_ast f = Z3_get_smtlib_formula(ctx, i);
printf("formula %d: %s\n", i, Z3_ast_to_string(ctx, f));
- Z3_assert_cnstr(ctx, f);
+ Z3_solver_assert(ctx, s, f);
}
- check(ctx, Z3_L_TRUE);
+ check(ctx, s, Z3_L_TRUE);
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -1599,7 +1657,8 @@ void parser_example1()
*/
void parser_example2()
{
- Z3_context ctx;
+ Z3_context ctx = mk_context();
+ Z3_solver s = mk_solver(ctx);
Z3_ast x, y;
Z3_symbol names[2];
Z3_func_decl decls[2];
@@ -1608,7 +1667,6 @@ void parser_example2()
printf("\nparser_example2\n");
LOG_MSG("parser_example2");
- ctx = mk_context();
/* Z3_enable_arithmetic doesn't need to be invoked in this example
because it will be implicitly invoked by mk_int_var.
@@ -1629,9 +1687,10 @@ void parser_example2()
2, names, decls);
f = Z3_get_smtlib_formula(ctx, 0);
printf("formula: %s\n", Z3_ast_to_string(ctx, f));
- Z3_assert_cnstr(ctx, f);
- check(ctx, Z3_L_TRUE);
+ Z3_solver_assert(ctx, s, f);
+ check(ctx, s, Z3_L_TRUE);
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -1642,6 +1701,7 @@ void parser_example3()
{
Z3_config cfg;
Z3_context ctx;
+ Z3_solver s;
Z3_sort int_sort;
Z3_symbol g_name;
Z3_sort g_domain[2];
@@ -1656,6 +1716,7 @@ void parser_example3()
Z3_set_param_value(cfg, "model", "true");
ctx = mk_context_custom(cfg, error_handler);
Z3_del_config(cfg);
+ s = mk_solver(ctx);
/* declare function g */
int_sort = Z3_mk_int_sort(ctx);
@@ -1664,7 +1725,7 @@ void parser_example3()
g_domain[1] = int_sort;
g = Z3_mk_func_decl(ctx, g_name, 2, g_domain, int_sort);
- assert_comm_axiom(ctx, g);
+ assert_comm_axiom(ctx, s, g);
Z3_parse_smtlib_string(ctx,
"(benchmark tst :formula (forall (x Int) (y Int) (implies (= x y) (= (g x 0) (g 0 y)))))",
@@ -1672,8 +1733,9 @@ void parser_example3()
1, &g_name, &g);
thm = Z3_get_smtlib_formula(ctx, 0);
printf("formula: %s\n", Z3_ast_to_string(ctx, thm));
- prove(ctx, thm, Z3_TRUE);
+ prove(ctx, s, thm, Z3_TRUE);
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -1718,6 +1780,7 @@ void parser_example4()
void parser_example5() {
Z3_config cfg;
Z3_context ctx = NULL;
+ Z3_solver s = NULL;
int r;
printf("\nparser_example5\n");
@@ -1727,6 +1790,7 @@ void parser_example5() {
if (r == 0) {
cfg = Z3_mk_config();
ctx = mk_context_custom(cfg, throw_z3_error);
+ s = mk_solver(ctx);
Z3_del_config(cfg);
Z3_parse_smtlib_string(ctx,
@@ -1735,12 +1799,14 @@ void parser_example5() {
0, 0, 0,
0, 0, 0);
unreachable();
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
else {
- printf("Z3 error: %s.\n", Z3_get_error_msg((Z3_error_code)r));
+ printf("Z3 error: %s.\n", Z3_get_error_msg_ex(ctx, (Z3_error_code)r));
if (ctx != NULL) {
printf("Error message: '%s'.\n",Z3_get_smtlib_error(ctx));
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
}
@@ -1751,24 +1817,28 @@ void parser_example5() {
*/
void numeral_example() {
Z3_context ctx;
+ Z3_solver s;
Z3_ast n1, n2;
Z3_sort real_ty;
printf("\nnumeral_example\n");
LOG_MSG("numeral_example");
ctx = mk_context();
+ s = mk_solver(ctx);
+
real_ty = Z3_mk_real_sort(ctx);
n1 = Z3_mk_numeral(ctx, "1/2", real_ty);
n2 = Z3_mk_numeral(ctx, "0.5", real_ty);
printf("Numerals n1:%s", Z3_ast_to_string(ctx, n1));
printf(" n2:%s\n", Z3_ast_to_string(ctx, n2));
- prove(ctx, Z3_mk_eq(ctx, n1, n2), Z3_TRUE);
+ prove(ctx, s, Z3_mk_eq(ctx, n1, n2), Z3_TRUE);
n1 = Z3_mk_numeral(ctx, "-1/3", real_ty);
n2 = Z3_mk_numeral(ctx, "-0.33333333333333333333333333333333333333333333333333", real_ty);
printf("Numerals n1:%s", Z3_ast_to_string(ctx, n1));
printf(" n2:%s\n", Z3_ast_to_string(ctx, n2));
- prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, n1, n2)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, n1, n2)), Z3_TRUE);
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -1801,6 +1871,7 @@ void ite_example()
*/
void enum_example() {
Z3_context ctx = mk_context();
+ Z3_solver s = mk_solver(ctx);
Z3_sort fruit;
Z3_symbol name = Z3_mk_string_symbol(ctx, "fruit");
Z3_symbol enum_names[3];
@@ -1831,14 +1902,14 @@ void enum_example() {
orange = Z3_mk_app(ctx, enum_consts[2], 0, 0);
/* Apples are different from oranges */
- prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, apple, orange)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, apple, orange)), Z3_TRUE);
/* Apples pass the apple test */
- prove(ctx, Z3_mk_app(ctx, enum_testers[0], 1, &apple), Z3_TRUE);
+ prove(ctx, s, Z3_mk_app(ctx, enum_testers[0], 1, &apple), Z3_TRUE);
/* Oranges fail the apple test */
- prove(ctx, Z3_mk_app(ctx, enum_testers[0], 1, &orange), Z3_FALSE);
- prove(ctx, Z3_mk_not(ctx, Z3_mk_app(ctx, enum_testers[0], 1, &orange)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_app(ctx, enum_testers[0], 1, &orange), Z3_FALSE);
+ prove(ctx, s, Z3_mk_not(ctx, Z3_mk_app(ctx, enum_testers[0], 1, &orange)), Z3_TRUE);
fruity = mk_var(ctx, "fruity", fruit);
@@ -1847,9 +1918,10 @@ void enum_example() {
ors[1] = Z3_mk_eq(ctx, fruity, banana);
ors[2] = Z3_mk_eq(ctx, fruity, orange);
- prove(ctx, Z3_mk_or(ctx, 3, ors), Z3_TRUE);
+ prove(ctx, s, Z3_mk_or(ctx, 3, ors), Z3_TRUE);
/* delete logical context */
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -1858,6 +1930,7 @@ void enum_example() {
*/
void list_example() {
Z3_context ctx = mk_context();
+ Z3_solver s = mk_solver(ctx);
Z3_sort int_ty, int_list;
Z3_func_decl nil_decl, is_nil_decl, cons_decl, is_cons_decl, head_decl, tail_decl;
Z3_ast nil, l1, l2, x, y, u, v, fml, fml1;
@@ -1877,43 +1950,44 @@ void list_example() {
l2 = mk_binary_app(ctx, cons_decl, mk_int(ctx, 2), nil);
/* nil != cons(1, nil) */
- prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, l1)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, l1)), Z3_TRUE);
/* cons(2,nil) != cons(1, nil) */
- prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, l1, l2)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, l1, l2)), Z3_TRUE);
/* cons(x,nil) = cons(y, nil) => x = y */
x = mk_var(ctx, "x", int_ty);
y = mk_var(ctx, "y", int_ty);
l1 = mk_binary_app(ctx, cons_decl, x, nil);
l2 = mk_binary_app(ctx, cons_decl, y, nil);
- prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE);
/* cons(x,u) = cons(x, v) => u = v */
u = mk_var(ctx, "u", int_list);
v = mk_var(ctx, "v", int_list);
l1 = mk_binary_app(ctx, cons_decl, x, u);
l2 = mk_binary_app(ctx, cons_decl, y, v);
- prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE);
- prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE);
/* is_nil(u) or is_cons(u) */
ors[0] = Z3_mk_app(ctx, is_nil_decl, 1, &u);
ors[1] = Z3_mk_app(ctx, is_cons_decl, 1, &u);
- prove(ctx, Z3_mk_or(ctx, 2, ors), Z3_TRUE);
+ prove(ctx, s, Z3_mk_or(ctx, 2, ors), Z3_TRUE);
/* occurs check u != cons(x,u) */
- prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE);
/* destructors: is_cons(u) => u = cons(head(u),tail(u)) */
fml1 = Z3_mk_eq(ctx, u, mk_binary_app(ctx, cons_decl, mk_unary_app(ctx, head_decl, u), mk_unary_app(ctx, tail_decl, u)));
fml = Z3_mk_implies(ctx, Z3_mk_app(ctx, is_cons_decl, 1, &u), fml1);
printf("Formula %s\n", Z3_ast_to_string(ctx, fml));
- prove(ctx, fml, Z3_TRUE);
+ prove(ctx, s, fml, Z3_TRUE);
- prove(ctx, fml1, Z3_FALSE);
+ prove(ctx, s, fml1, Z3_FALSE);
/* delete logical context */
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -1922,6 +1996,7 @@ void list_example() {
*/
void tree_example() {
Z3_context ctx = mk_context();
+ Z3_solver s = mk_solver(ctx);
Z3_sort cell;
Z3_func_decl nil_decl, is_nil_decl, cons_decl, is_cons_decl, car_decl, cdr_decl;
Z3_ast nil, l1, l2, x, y, u, v, fml, fml1;
@@ -1957,7 +2032,7 @@ void tree_example() {
l2 = mk_binary_app(ctx, cons_decl, l1, nil);
/* nil != cons(nil, nil) */
- prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, l1)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, l1)), Z3_TRUE);
/* cons(x,u) = cons(x, v) => u = v */
u = mk_var(ctx, "u", cell);
@@ -1966,26 +2041,27 @@ void tree_example() {
y = mk_var(ctx, "y", cell);
l1 = mk_binary_app(ctx, cons_decl, x, u);
l2 = mk_binary_app(ctx, cons_decl, y, v);
- prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE);
- prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE);
/* is_nil(u) or is_cons(u) */
ors[0] = Z3_mk_app(ctx, is_nil_decl, 1, &u);
ors[1] = Z3_mk_app(ctx, is_cons_decl, 1, &u);
- prove(ctx, Z3_mk_or(ctx, 2, ors), Z3_TRUE);
+ prove(ctx, s, Z3_mk_or(ctx, 2, ors), Z3_TRUE);
/* occurs check u != cons(x,u) */
- prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE);
/* destructors: is_cons(u) => u = cons(car(u),cdr(u)) */
fml1 = Z3_mk_eq(ctx, u, mk_binary_app(ctx, cons_decl, mk_unary_app(ctx, car_decl, u), mk_unary_app(ctx, cdr_decl, u)));
fml = Z3_mk_implies(ctx, Z3_mk_app(ctx, is_cons_decl, 1, &u), fml1);
printf("Formula %s\n", Z3_ast_to_string(ctx, fml));
- prove(ctx, fml, Z3_TRUE);
+ prove(ctx, s, fml, Z3_TRUE);
- prove(ctx, fml1, Z3_FALSE);
+ prove(ctx, s, fml1, Z3_FALSE);
/* delete logical context */
+ del_solver(ctx, s);
Z3_del_context(ctx);
@@ -2000,6 +2076,7 @@ void tree_example() {
void forest_example() {
Z3_context ctx = mk_context();
+ Z3_solver s = mk_solver(ctx);
Z3_sort tree, forest;
Z3_func_decl nil1_decl, is_nil1_decl, cons1_decl, is_cons1_decl, car1_decl, cdr1_decl;
Z3_func_decl nil2_decl, is_nil2_decl, cons2_decl, is_cons2_decl, car2_decl, cdr2_decl;
@@ -2073,8 +2150,8 @@ void forest_example() {
/* nil != cons(nil,nil) */
- prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil1, f1)), Z3_TRUE);
- prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil2, t1)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil1, f1)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil2, t1)), Z3_TRUE);
/* cons(x,u) = cons(x, v) => u = v */
@@ -2084,18 +2161,19 @@ void forest_example() {
y = mk_var(ctx, "y", tree);
l1 = mk_binary_app(ctx, cons1_decl, x, u);
l2 = mk_binary_app(ctx, cons1_decl, y, v);
- prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE);
- prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE);
/* is_nil(u) or is_cons(u) */
ors[0] = Z3_mk_app(ctx, is_nil1_decl, 1, &u);
ors[1] = Z3_mk_app(ctx, is_cons1_decl, 1, &u);
- prove(ctx, Z3_mk_or(ctx, 2, ors), Z3_TRUE);
+ prove(ctx, s, Z3_mk_or(ctx, 2, ors), Z3_TRUE);
/* occurs check u != cons(x,u) */
- prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE);
/* delete logical context */
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -2108,6 +2186,7 @@ void forest_example() {
*/
void binary_tree_example() {
Z3_context ctx = mk_context();
+ Z3_solver s = mk_solver(ctx);
Z3_sort cell;
Z3_func_decl
nil_decl, /* nil : BinTree (constructor) */
@@ -2164,22 +2243,23 @@ void binary_tree_example() {
Z3_ast node3 = Z3_mk_app(ctx, node_decl, 3, args3);
/* prove that nil != node1 */
- prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, node1)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, node1)), Z3_TRUE);
/* prove that nil = left(node1) */
- prove(ctx, Z3_mk_eq(ctx, nil, mk_unary_app(ctx, left_decl, node1)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_eq(ctx, nil, mk_unary_app(ctx, left_decl, node1)), Z3_TRUE);
/* prove that node1 = right(node3) */
- prove(ctx, Z3_mk_eq(ctx, node1, mk_unary_app(ctx, right_decl, node3)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_eq(ctx, node1, mk_unary_app(ctx, right_decl, node3)), Z3_TRUE);
/* prove that !is-nil(node2) */
- prove(ctx, Z3_mk_not(ctx, mk_unary_app(ctx, is_nil_decl, node2)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_not(ctx, mk_unary_app(ctx, is_nil_decl, node2)), Z3_TRUE);
/* prove that value(node2) >= 0 */
- prove(ctx, Z3_mk_ge(ctx, mk_unary_app(ctx, value_decl, node2), mk_int(ctx, 0)), Z3_TRUE);
+ prove(ctx, s, Z3_mk_ge(ctx, mk_unary_app(ctx, value_decl, node2), mk_int(ctx, 0)), Z3_TRUE);
}
/* delete logical context */
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -2190,6 +2270,7 @@ void binary_tree_example() {
*/
void unsat_core_and_proof_example() {
Z3_context ctx = mk_proof_context();
+ Z3_solver s = mk_solver(ctx);
Z3_ast pa = mk_bool_var(ctx, "PredA");
Z3_ast pb = mk_bool_var(ctx, "PredB");
Z3_ast pc = mk_bool_var(ctx, "PredC");
@@ -2210,49 +2291,53 @@ void unsat_core_and_proof_example() {
Z3_ast g2[2] = { f2, p2 };
Z3_ast g3[2] = { f3, p3 };
Z3_ast g4[2] = { f4, p4 };
- Z3_ast core[4] = { 0, 0, 0, 0 };
- unsigned core_size = 4;
- Z3_ast proof;
- Z3_model m = 0;
Z3_lbool result;
+ Z3_ast proof;
+ Z3_model m = 0;
unsigned i;
+ Z3_ast_vector core;
printf("\nunsat_core_and_proof_example\n");
LOG_MSG("unsat_core_and_proof_example");
- Z3_assert_cnstr(ctx, Z3_mk_or(ctx, 2, g1));
- Z3_assert_cnstr(ctx, Z3_mk_or(ctx, 2, g2));
- Z3_assert_cnstr(ctx, Z3_mk_or(ctx, 2, g3));
- Z3_assert_cnstr(ctx, Z3_mk_or(ctx, 2, g4));
+ Z3_solver_assert(ctx, s, Z3_mk_or(ctx, 2, g1));
+ Z3_solver_assert(ctx, s, Z3_mk_or(ctx, 2, g2));
+ Z3_solver_assert(ctx, s, Z3_mk_or(ctx, 2, g3));
+ Z3_solver_assert(ctx, s, Z3_mk_or(ctx, 2, g4));
- result = Z3_check_assumptions(ctx, 4, assumptions, &m, &proof, &core_size, core);
+ result = Z3_solver_check_assumptions(ctx, s, 4, assumptions);
switch (result) {
case Z3_L_FALSE:
+ core = Z3_solver_get_unsat_core(ctx, s);
+ proof = Z3_solver_get_proof(ctx, s);
printf("unsat\n");
printf("proof: %s\n", Z3_ast_to_string(ctx, proof));
printf("\ncore:\n");
- for (i = 0; i < core_size; ++i) {
- printf("%s\n", Z3_ast_to_string(ctx, core[i]));
+ for (i = 0; i < Z3_ast_vector_size(ctx, core); ++i) {
+ printf("%s\n", Z3_ast_to_string(ctx, Z3_ast_vector_get(ctx, core, i)));
}
printf("\n");
break;
case Z3_L_UNDEF:
printf("unknown\n");
printf("potential model:\n");
+ m = Z3_solver_get_model(ctx, s);
+ if (m) Z3_model_inc_ref(ctx, m);
display_model(ctx, stdout, m);
break;
case Z3_L_TRUE:
printf("sat\n");
+ m = Z3_solver_get_model(ctx, s);
+ if (m) Z3_model_inc_ref(ctx, m);
display_model(ctx, stdout, m);
break;
}
- if (m) {
- Z3_del_model(ctx, m);
- }
/* delete logical context */
+ if (m) Z3_model_dec_ref(ctx, m);
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -2264,6 +2349,7 @@ void unsat_core_and_proof_example() {
*/
typedef struct {
Z3_context m_context;
+ Z3_solver m_solver;
// IMPORTANT: the fields m_answer_literals, m_retracted and m_num_answer_literals must be saved/restored
// if push/pop operations are performed on m_context.
Z3_ast m_answer_literals[MAX_RETRACTABLE_ASSERTIONS];
@@ -2279,6 +2365,7 @@ typedef Z3_ext_context_struct * Z3_ext_context;
Z3_ext_context mk_ext_context() {
Z3_ext_context ctx = (Z3_ext_context) malloc(sizeof(Z3_ext_context_struct));
ctx->m_context = mk_context();
+ ctx->m_solver = mk_solver(ctx->m_context);
ctx->m_num_answer_literals = 0;
return ctx;
}
@@ -2287,6 +2374,7 @@ Z3_ext_context mk_ext_context() {
\brief Delete the given logical context wrapper.
*/
void del_ext_context(Z3_ext_context ctx) {
+ del_solver(ctx->m_context, ctx->m_solver);
Z3_del_context(ctx->m_context);
free(ctx);
}
@@ -2313,7 +2401,7 @@ unsigned assert_retractable_cnstr(Z3_ext_context ctx, Z3_ast c) {
// assert: c OR (not ans_lit)
args[0] = c;
args[1] = Z3_mk_not(ctx->m_context, ans_lit);
- Z3_assert_cnstr(ctx->m_context, Z3_mk_or(ctx->m_context, 2, args));
+ Z3_solver_assert(ctx->m_context, ctx->m_solver, Z3_mk_or(ctx->m_context, 2, args));
return result;
}
@@ -2344,10 +2432,8 @@ Z3_lbool ext_check(Z3_ext_context ctx) {
Z3_lbool result;
unsigned num_assumptions = 0;
Z3_ast assumptions[MAX_RETRACTABLE_ASSERTIONS];
- Z3_ast core[MAX_RETRACTABLE_ASSERTIONS];
+ Z3_ast_vector core;
unsigned core_size;
- Z3_ast dummy_proof = 0; // we don't care about the proof in this example.
- Z3_model dummy_model = 0; // we don't care about the model in this example.
unsigned i;
for (i = 0; i < ctx->m_num_answer_literals; i++) {
if (ctx->m_retracted[i] == Z3_FALSE) {
@@ -2358,15 +2444,18 @@ Z3_lbool ext_check(Z3_ext_context ctx) {
num_assumptions ++;
}
}
- result = Z3_check_assumptions(ctx->m_context, num_assumptions, assumptions, &dummy_model, &dummy_proof, &core_size, core);
+ result = Z3_solver_check_assumptions(ctx->m_context, ctx->m_solver, num_assumptions, assumptions);
if (result == Z3_L_FALSE) {
// Display the UNSAT core
printf("unsat core: ");
+ core = Z3_solver_get_unsat_core(ctx->m_context, ctx->m_solver);
+ core_size = Z3_ast_vector_size(ctx->m_context, core);
for (i = 0; i < core_size; i++) {
+
// In this example, we display the core based on the assertion ids.
unsigned j;
for (j = 0; j < ctx->m_num_answer_literals; j++) {
- if (core[i] == ctx->m_answer_literals[j]) {
+ if (Z3_ast_vector_get(ctx->m_context, core, i) == ctx->m_answer_literals[j]) {
printf("%d ", j);
break;
}
@@ -2378,10 +2467,6 @@ Z3_lbool ext_check(Z3_ext_context ctx) {
printf("\n");
}
- if (dummy_model) {
- Z3_del_model(ctx->m_context, dummy_model);
- }
-
return result;
}
@@ -2452,6 +2537,7 @@ void incremental_example1() {
void reference_counter_example() {
Z3_config cfg;
Z3_context ctx;
+ Z3_solver s;
Z3_sort ty;
Z3_ast x, y, x_xor_y;
Z3_symbol sx, sy;
@@ -2465,6 +2551,8 @@ void reference_counter_example() {
// Z3_ast reference counters.
ctx = Z3_mk_context_rc(cfg);
Z3_del_config(cfg);
+ s = mk_solver(ctx);
+ Z3_solver_inc_ref(ctx, s);
ty = Z3_mk_bool_sort(ctx);
Z3_inc_ref(ctx, Z3_sort_to_ast(ctx, ty)); // Z3_sort_to_ast(ty) is just syntax sugar for ((Z3_ast) ty)
@@ -2482,17 +2570,19 @@ void reference_counter_example() {
// x and y are not needed anymore.
Z3_dec_ref(ctx, x);
Z3_dec_ref(ctx, y);
- Z3_assert_cnstr(ctx, x_xor_y);
+ Z3_solver_assert(ctx, s, x_xor_y);
// x_or_y is not needed anymore.
Z3_dec_ref(ctx, x_xor_y);
printf("model for: x xor y\n");
- check(ctx, Z3_L_TRUE);
+ check(ctx, s, Z3_L_TRUE);
// Test push & pop
- Z3_push(ctx);
- Z3_pop(ctx, 1);
+ Z3_solver_push(ctx, s);
+ Z3_solver_pop(ctx, s, 1);
+ Z3_solver_dec_ref(ctx, s);
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
@@ -2608,6 +2698,7 @@ void substitute_vars_example() {
void fpa_example() {
Z3_config cfg;
Z3_context ctx;
+ Z3_solver s;
Z3_sort double_sort, rm_sort;
Z3_symbol s_rm, s_x, s_y, s_x_plus_y;
Z3_ast rm, x, y, n, x_plus_y, c1, c2, c3, c4, c5;
@@ -2618,6 +2709,7 @@ void fpa_example() {
cfg = Z3_mk_config();
ctx = Z3_mk_context(cfg);
+ s = mk_solver(ctx);
Z3_del_config(cfg);
double_sort = Z3_mk_fpa_sort(ctx, 11, 53);
@@ -2652,10 +2744,10 @@ void fpa_example() {
c4 = Z3_mk_and(ctx, 2, (Z3_ast*)&args3);
printf("c4: %s\n", Z3_ast_to_string(ctx, c4));
- Z3_push(ctx);
- Z3_assert_cnstr(ctx, c4);
- check(ctx, Z3_L_TRUE);
- Z3_pop(ctx, 1);
+ Z3_solver_push(ctx, s);
+ Z3_solver_assert(ctx, s, c4);
+ check(ctx, s, Z3_L_TRUE);
+ Z3_solver_pop(ctx, s, 1);
// Show that the following are equal:
// (fp #b0 #b10000000001 #xc000000000000)
@@ -2663,7 +2755,7 @@ void fpa_example() {
// ((_ to_fp 11 53) RTZ 1.75 2)))
// ((_ to_fp 11 53) RTZ 7.0)))
- Z3_push(ctx);
+ Z3_solver_push(ctx, s);
c1 = Z3_mk_fpa_fp(ctx,
Z3_mk_numeral(ctx, "0", Z3_mk_bv_sort(ctx, 1)),
Z3_mk_numeral(ctx, "3377699720527872", Z3_mk_bv_sort(ctx, 52)),
@@ -2686,10 +2778,11 @@ void fpa_example() {
c5 = Z3_mk_and(ctx, 3, args3);
printf("c5: %s\n", Z3_ast_to_string(ctx, c5));
- Z3_assert_cnstr(ctx, c5);
- check(ctx, Z3_L_TRUE);
- Z3_pop(ctx, 1);
+ Z3_solver_assert(ctx, s, c5);
+ check(ctx, s, Z3_L_TRUE);
+ Z3_solver_pop(ctx, s, 1);
+ del_solver(ctx, s);
Z3_del_context(ctx);
}
From 1575dd06a73e5dcdcdec57f41713d38126f49ab2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 18 Nov 2015 09:42:12 -0800
Subject: [PATCH 12/14] expose labels from optimization. Move printing of
objectives to after sat/unsat. Cahnge format to something that is somewhat
related to how other output is created. Issue #325.
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/cmd_context/cmd_context.cpp | 10 ++++++----
src/opt/opt_context.cpp | 14 ++++++++++++--
src/opt/opt_context.h | 2 +-
3 files changed, 19 insertions(+), 7 deletions(-)
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index b018d62c5..6e443d476 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1401,9 +1401,10 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
unsigned rlimit = m_params.m_rlimit;
scoped_watch sw(*this);
lbool r;
+ bool was_pareto = false, was_opt = false;
if (m_opt && !m_opt->empty()) {
- bool was_pareto = false;
+ was_opt = true;
m_check_sat_result = get_opt();
cancel_eh<opt_wrapper> eh(*get_opt());
scoped_ctrl_c ctrlc(eh);
@@ -1436,9 +1437,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
r = l_true;
}
get_opt()->set_status(r);
- if (r != l_false && !was_pareto) {
- get_opt()->display_assignment(regular_stream());
- }
}
else if (m_solver) {
m_check_sat_result = m_solver.get(); // solver itself stores the result.
@@ -1465,6 +1463,10 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
}
display_sat_result(r);
validate_check_sat_result(r);
+ if (was_opt && r != l_false && !was_pareto) {
+ get_opt()->display_assignment(regular_stream());
+ }
+
if (r == l_true) {
validate_model();
if (m_params.m_dump_models) {
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 1b4b1e7bc..265e3b7c8 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -167,6 +167,12 @@ namespace opt {
m_hard_constraints.reset();
}
+ void context::get_labels(svector<symbol> & r) {
+ if (m_solver) {
+ m_solver->get_labels(r);
+ }
+ }
+
void context::set_hard_constraints(ptr_vector<expr>& fmls) {
if (m_scoped_state.set(fmls)) {
clear_state();
@@ -1121,16 +1127,20 @@ namespace opt {
}
void context::display_assignment(std::ostream& out) {
+ out << "(objectives\n";
for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) {
objective const& obj = m_scoped_state.m_objectives[i];
+ out << " (";
display_objective(out, obj);
if (get_lower_as_num(i) != get_upper_as_num(i)) {
- out << " |-> [" << get_lower(i) << ":" << get_upper(i) << "]\n";
+ out << " (" << get_lower(i) << " " << get_upper(i) << ")";
}
else {
- out << " |-> " << get_lower(i) << "\n";
+ out << " " << get_lower(i);
}
+ out << ")\n";
}
+ out << ")\n";
}
void context::display_objective(std::ostream& out, objective const& obj) const {
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 735dc6905..b364fe63e 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -184,7 +184,7 @@ namespace opt {
virtual void fix_model(model_ref& _m);
virtual void collect_statistics(statistics& stats) const;
virtual proof* get_proof() { return 0; }
- virtual void get_labels(svector<symbol> & r) {}
+ virtual void get_labels(svector<symbol> & r);
virtual void get_unsat_core(ptr_vector<expr> & r) {}
virtual std::string reason_unknown() const;
From 9cba63c31f6f1466dd4ef442bb840d1ab84539c7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 18 Nov 2015 12:32:15 -0800
Subject: [PATCH 13/14] remove deprecated iz3 example. Remove deprecated
process control
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
examples/interp/iz3.cpp | 458 ----------------------------------------
scripts/mk_project.py | 1 -
src/api/api_context.cpp | 4 +-
src/util/util.cpp | 21 --
src/util/util.h | 1 -
5 files changed, 1 insertion(+), 484 deletions(-)
delete mode 100755 examples/interp/iz3.cpp
diff --git a/examples/interp/iz3.cpp b/examples/interp/iz3.cpp
deleted file mode 100755
index 21ea518a6..000000000
--- a/examples/interp/iz3.cpp
+++ /dev/null
@@ -1,458 +0,0 @@
-
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
---*/
-
-#include <stdio.h>
-#include <stdlib.h>
-#include <iostream>
-#include <string>
-#include <vector>
-#include "z3.h"
-
-
-
-int usage(const char **argv){
- std::cerr << "usage: " << argv[0] << " [options] file.smt" << std::endl;
- std::cerr << std::endl;
- std::cerr << "options:" << std::endl;
- std::cerr << " -t,--tree tree interpolation" << std::endl;
- std::cerr << " -c,--check check result" << std::endl;
- std::cerr << " -p,--profile profile execution" << std::endl;
- std::cerr << " -w,--weak weak interpolants" << std::endl;
- std::cerr << " -f,--flat ouput flat formulas" << std::endl;
- std::cerr << " -o <file> ouput to SMT-LIB file" << std::endl;
- std::cerr << " -a,--anon anonymize" << std::endl;
- std::cerr << " -s,--simple simple proof mode" << std::endl;
- std::cerr << std::endl;
- return 1;
-}
-
-int main(int argc, const char **argv) {
-
- bool tree_mode = false;
- bool check_mode = false;
- bool profile_mode = false;
- bool incremental_mode = false;
- std::string output_file;
- bool flat_mode = false;
- bool anonymize = false;
- bool write = false;
-
- Z3_config cfg = Z3_mk_config();
- // Z3_interpolation_options options = Z3_mk_interpolation_options();
- // Z3_params options = 0;
-
- /* Parse the command line */
- int argn = 1;
- while(argn < argc-1){
- std::string flag = argv[argn];
- if(flag[0] == '-'){
- if(flag == "-t" || flag == "--tree")
- tree_mode = true;
- else if(flag == "-c" || flag == "--check")
- check_mode = true;
- else if(flag == "-p" || flag == "--profile")
- profile_mode = true;
-#if 0
- else if(flag == "-w" || flag == "--weak")
- Z3_set_interpolation_option(options,"weak","1");
- else if(flag == "--secondary")
- Z3_set_interpolation_option(options,"secondary","1");
-#endif
- else if(flag == "-i" || flag == "--incremental")
- incremental_mode = true;
- else if(flag == "-o"){
- argn++;
- if(argn >= argc) return usage(argv);
- output_file = argv[argn];
- }
- else if(flag == "-f" || flag == "--flat")
- flat_mode = true;
- else if(flag == "-a" || flag == "--anon")
- anonymize = true;
- else if(flag == "-w" || flag == "--write")
- write = true;
- else if(flag == "-s" || flag == "--simple")
- Z3_set_param_value(cfg,"PREPROCESS","false");
- else
- return usage(argv);
- }
- argn++;
- }
- if(argn != argc-1)
- return usage(argv);
- const char *filename = argv[argn];
-
-
- /* Create a Z3 context to contain formulas */
- Z3_context ctx = Z3_mk_interpolation_context(cfg);
-
- if(write || anonymize)
- Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB2_COMPLIANT);
- else if(!flat_mode)
- Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB_COMPLIANT);
-
- /* Read an interpolation problem */
-
- unsigned num;
- Z3_ast *constraints;
- unsigned *parents = 0;
- const char *error;
- bool ok;
- unsigned num_theory;
- Z3_ast *theory;
-
- ok = Z3_read_interpolation_problem(ctx, &num, &constraints, tree_mode ? &parents : 0, filename, &error, &num_theory, &theory) != 0;
-
- /* If parse failed, print the error message */
-
- if(!ok){
- std::cerr << error << "\n";
- return 1;
- }
-
- /* if we get only one formula, and it is a conjunction, split it into conjuncts. */
- if(!tree_mode && num == 1){
- Z3_app app = Z3_to_app(ctx,constraints[0]);
- Z3_func_decl func = Z3_get_app_decl(ctx,app);
- Z3_decl_kind dk = Z3_get_decl_kind(ctx,func);
- if(dk == Z3_OP_AND){
- int nconjs = Z3_get_app_num_args(ctx,app);
- if(nconjs > 1){
- std::cout << "Splitting formula into " << nconjs << " conjuncts...\n";
- num = nconjs;
- constraints = new Z3_ast[num];
- for(unsigned k = 0; k < num; k++)
- constraints[k] = Z3_get_app_arg(ctx,app,k);
- }
- }
- }
-
- /* Write out anonymized version. */
-
- if(write || anonymize){
-#if 0
- Z3_anonymize_ast_vector(ctx,num,constraints);
-#endif
- std::string ofn = output_file.empty() ? "iz3out.smt2" : output_file;
- Z3_write_interpolation_problem(ctx, num, constraints, parents, ofn.c_str(), num_theory, theory);
- std::cout << "anonymized problem written to " << ofn << "\n";
- exit(0);
- }
-
- /* Compute an interpolant, or get a model. */
-
- Z3_ast *interpolants = (Z3_ast *)malloc((num-1) * sizeof(Z3_ast));
- Z3_model model = 0;
- Z3_lbool result;
-
- if(!incremental_mode){
- /* In non-incremental mode, we just pass the constraints. */
- result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, constraints, parents, options, interpolants, &model, 0, false, num_theory, theory);
- }
- else {
-
- /* This is a somewhat useless demonstration of incremental mode.
- Here, we assert the constraints in the context, then pass them to
- iZ3 in an array, so iZ3 knows the sequence. Note it's safe to pass
- "true", even though we haven't techically asserted if. */
-
- Z3_push(ctx);
- std::vector<Z3_ast> asserted(num);
-
- /* We start with nothing asserted. */
- for(unsigned i = 0; i < num; i++)
- asserted[i] = Z3_mk_true(ctx);
-
- /* Now we assert the constrints one at a time until UNSAT. */
-
- for(unsigned i = 0; i < num; i++){
- asserted[i] = constraints[i];
- Z3_assert_cnstr(ctx,constraints[i]); // assert one constraint
- result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, &asserted[0], parents, options, interpolants, &model, 0, true, 0, 0);
- if(result == Z3_L_FALSE){
- for(unsigned j = 0; j < num-1; j++)
- /* Since we want the interpolant formulas to survive a "pop", we
- "persist" them here. */
- Z3_persist_ast(ctx,interpolants[j],1);
- break;
- }
- }
- Z3_pop(ctx,1);
- }
-
- switch (result) {
-
- /* If UNSAT, print the interpolants */
- case Z3_L_FALSE:
- printf("unsat\n");
- if(output_file.empty()){
- printf("interpolant:\n");
- for(unsigned i = 0; i < num-1; i++)
- printf("%s\n", Z3_ast_to_string(ctx, interpolants[i]));
- }
- else {
-#if 0
- Z3_write_interpolation_problem(ctx,num-1,interpolants,0,output_file.c_str());
- printf("interpolant written to %s\n",output_file.c_str());
-#endif
- }
-#if 1
- if(check_mode){
- std::cout << "Checking interpolant...\n";
- bool chk;
- chk = Z3_check_interpolant(ctx,num,constraints,parents,interpolants,&error,num_theory,theory) != 0;
- if(chk)
- std::cout << "Interpolant is correct\n";
- else {
- std::cout << "Interpolant is incorrect\n";
- std::cout << error;
- return 1;
- }
- }
-#endif
- break;
- case Z3_L_UNDEF:
- printf("fail\n");
- break;
- case Z3_L_TRUE:
- printf("sat\n");
- printf("model:\n%s\n", Z3_model_to_string(ctx, model));
- break;
- }
-
- if(profile_mode)
- std::cout << Z3_interpolation_profile(ctx);
-
- /* Delete the model if there is one */
-
- if (model)
- Z3_del_model(ctx, model);
-
- /* Delete logical context. */
-
- Z3_del_context(ctx);
- free(interpolants);
-
- return 0;
-}
-
-
-#if 0
-
-
-
-int test(){
- int i;
-
- /* Create a Z3 context to contain formulas */
-
- Z3_config cfg = Z3_mk_config();
- Z3_context ctx = iz3_mk_context(cfg);
-
- int num = 2;
-
- Z3_ast *constraints = (Z3_ast *)malloc(num * sizeof(Z3_ast));
-
-#if 1
- Z3_sort arr = Z3_mk_array_sort(ctx,Z3_mk_int_sort(ctx),Z3_mk_bool_sort(ctx));
- Z3_symbol as = Z3_mk_string_symbol(ctx, "a");
- Z3_symbol bs = Z3_mk_string_symbol(ctx, "b");
- Z3_symbol xs = Z3_mk_string_symbol(ctx, "x");
-
- Z3_ast a = Z3_mk_const(ctx,as,arr);
- Z3_ast b = Z3_mk_const(ctx,bs,arr);
- Z3_ast x = Z3_mk_const(ctx,xs,Z3_mk_int_sort(ctx));
-
- Z3_ast c1 = Z3_mk_eq(ctx,a,Z3_mk_store(ctx,b,x,Z3_mk_true(ctx)));
- Z3_ast c2 = Z3_mk_not(ctx,Z3_mk_select(ctx,a,x));
-#else
- Z3_symbol xs = Z3_mk_string_symbol(ctx, "x");
- Z3_ast x = Z3_mk_const(ctx,xs,Z3_mk_bool_sort(ctx));
- Z3_ast c1 = Z3_mk_eq(ctx,x,Z3_mk_true(ctx));
- Z3_ast c2 = Z3_mk_eq(ctx,x,Z3_mk_false(ctx));
-
-#endif
-
- constraints[0] = c1;
- constraints[1] = c2;
-
- /* print out the result for grins. */
-
- // Z3_string smtout = Z3_benchmark_to_smtlib_string (ctx, "foo", "QFLIA", "sat", "", num, constraints, Z3_mk_true(ctx));
-
- // Z3_string smtout = Z3_ast_to_string(ctx,constraints[0]);
- // Z3_string smtout = Z3_context_to_string(ctx);
- // puts(smtout);
-
- iz3_print(ctx,num,constraints,"iZ3temp.smt");
-
- /* Make room for interpolants. */
-
- Z3_ast *interpolants = (Z3_ast *)malloc((num-1) * sizeof(Z3_ast));
-
- /* Make room for the model. */
-
- Z3_model model = 0;
-
- /* Call the prover */
-
- Z3_lbool result = iz3_interpolate(ctx, num, constraints, interpolants, &model);
-
- switch (result) {
-
- /* If UNSAT, print the interpolants */
- case Z3_L_FALSE:
- printf("unsat, interpolants:\n");
- for(i = 0; i < num-1; i++)
- printf("%s\n", Z3_ast_to_string(ctx, interpolants[i]));
- break;
- case Z3_L_UNDEF:
- printf("fail\n");
- break;
- case Z3_L_TRUE:
- printf("sat\n");
- printf("model:\n%s\n", Z3_model_to_string(ctx, model));
- break;
- }
-
- /* Delete the model if there is one */
-
- if (model)
- Z3_del_model(ctx, model);
-
- /* Delete logical context (note, we call iz3_del_context, not
- Z3_del_context */
-
- iz3_del_context(ctx);
-
- return 1;
-}
-
-struct z3_error {
- Z3_error_code c;
- z3_error(Z3_error_code _c) : c(_c) {}
-};
-
-extern "C" {
- static void throw_z3_error(Z3_error_code c){
- throw z3_error(c);
- }
-}
-
-int main(int argc, const char **argv) {
-
- /* Create a Z3 context to contain formulas */
-
- Z3_config cfg = Z3_mk_config();
- Z3_context ctx = iz3_mk_context(cfg);
- Z3_set_error_handler(ctx, throw_z3_error);
-
- /* Make some constraints, by parsing an smtlib formatted file given as arg 1 */
-
- try {
- Z3_parse_smtlib_file(ctx, argv[1], 0, 0, 0, 0, 0, 0);
- }
- catch(const z3_error &err){
- std::cerr << "Z3 error: " << Z3_get_error_msg(err.c) << "\n";
- std::cerr << Z3_get_smtlib_error(ctx) << "\n";
- return(1);
- }
-
- /* Get the constraints from the parser. */
-
- int num = Z3_get_smtlib_num_formulas(ctx);
-
- if(num == 0){
- std::cerr << "iZ3 error: File contains no formulas.\n";
- return 1;
- }
-
-
- Z3_ast *constraints = (Z3_ast *)malloc(num * sizeof(Z3_ast));
-
- int i;
- for (i = 0; i < num; i++)
- constraints[i] = Z3_get_smtlib_formula(ctx, i);
-
- /* if we get only one formula, and it is a conjunction, split it into conjuncts. */
- if(num == 1){
- Z3_app app = Z3_to_app(ctx,constraints[0]);
- Z3_func_decl func = Z3_get_app_decl(ctx,app);
- Z3_decl_kind dk = Z3_get_decl_kind(ctx,func);
- if(dk == Z3_OP_AND){
- int nconjs = Z3_get_app_num_args(ctx,app);
- if(nconjs > 1){
- std::cout << "Splitting formula into " << nconjs << " conjuncts...\n";
- num = nconjs;
- constraints = new Z3_ast[num];
- for(int k = 0; k < num; k++)
- constraints[k] = Z3_get_app_arg(ctx,app,k);
- }
- }
- }
-
-
- /* print out the result for grins. */
-
- // Z3_string smtout = Z3_benchmark_to_smtlib_string (ctx, "foo", "QFLIA", "sat", "", num, constraints, Z3_mk_true(ctx));
-
- // Z3_string smtout = Z3_ast_to_string(ctx,constraints[0]);
- // Z3_string smtout = Z3_context_to_string(ctx);
- // puts(smtout);
-
- // iz3_print(ctx,num,constraints,"iZ3temp.smt");
-
- /* Make room for interpolants. */
-
- Z3_ast *interpolants = (Z3_ast *)malloc((num-1) * sizeof(Z3_ast));
-
- /* Make room for the model. */
-
- Z3_model model = 0;
-
- /* Call the prover */
-
- Z3_lbool result = iz3_interpolate(ctx, num, constraints, interpolants, &model);
-
- switch (result) {
-
- /* If UNSAT, print the interpolants */
- case Z3_L_FALSE:
- printf("unsat, interpolants:\n");
- for(i = 0; i < num-1; i++)
- printf("%s\n", Z3_ast_to_string(ctx, interpolants[i]));
- std::cout << "Checking interpolants...\n";
- const char *error;
- if(iZ3_check_interpolant(ctx, num, constraints, 0, interpolants, &error))
- std::cout << "Interpolant is correct\n";
- else {
- std::cout << "Interpolant is incorrect\n";
- std::cout << error << "\n";
- }
- break;
- case Z3_L_UNDEF:
- printf("fail\n");
- break;
- case Z3_L_TRUE:
- printf("sat\n");
- printf("model:\n%s\n", Z3_model_to_string(ctx, model));
- break;
- }
-
- /* Delete the model if there is one */
-
- if (model)
- Z3_del_model(ctx, model);
-
- /* Delete logical context (note, we call iz3_del_context, not
- Z3_del_context */
-
- iz3_del_context(ctx);
-
- return 0;
-}
-
-#endif
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 2863de628..dfe801bdd 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -94,7 +94,6 @@ def init_project_def():
set_z3py_dir('api/python')
# Examples
add_cpp_example('cpp_example', 'c++')
- add_cpp_example('iz3', 'interp')
add_cpp_example('z3_tptp', 'tptp')
add_c_example('c_example', 'c')
add_c_example('maxsat')
diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index f17a296fa..6749f1525 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -103,9 +103,7 @@ namespace api {
m_smtlib_parser = 0;
m_smtlib_parser_has_decls = false;
-
- z3_bound_num_procs();
-
+
m_error_handler = &default_error_handler;
m_basic_fid = m().get_basic_family_id();
diff --git a/src/util/util.cpp b/src/util/util.cpp
index c4b729adb..bfd4923a8 100644
--- a/src/util/util.cpp
+++ b/src/util/util.cpp
@@ -151,24 +151,3 @@ void escaped::display(std::ostream & out) const {
}
}
-#ifdef _WINDOWS
-#ifdef ARRAYSIZE
-#undef ARRAYSIZE
-#endif
-#include <windows.h>
-#endif
-
-void z3_bound_num_procs() {
-
-#ifdef _Z3_COMMERCIAL
-#define Z3_COMMERCIAL_MAX_CORES 4
-#ifdef _WINDOWS
- DWORD_PTR numProcs = (1 << Z3_COMMERCIAL_MAX_CORES) - 1;
- SetProcessAffinityMask(GetCurrentProcess(), numProcs);
-#endif
-#else
- // Not bounded: Research evaluations are
- // not reasonable if run with artificial
- // or hidden throttles.
-#endif
-}
diff --git a/src/util/util.h b/src/util/util.h
index f97f5c1f9..1e15b526c 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -400,7 +400,6 @@ inline size_t megabytes_to_bytes(unsigned mb) {
return r;
}
-void z3_bound_num_procs();
#endif /* UTIL_H_ */
From c58e640563424747ecf086339aeb2f6437b46567 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 18 Nov 2015 14:53:08 -0800
Subject: [PATCH 14/14] extract labels for optimal model. Fix to #325
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/opt/maxsmt.cpp | 5 +++--
src/opt/maxsmt.h | 10 ++++++----
src/opt/opt_context.cpp | 16 +++++-----------
src/opt/opt_context.h | 2 +-
src/opt/opt_pareto.cpp | 2 ++
src/opt/opt_pareto.h | 5 +++--
src/opt/optsmt.cpp | 9 +++++++--
src/opt/optsmt.h | 3 ++-
src/sat/sat_solver/inc_sat_solver.cpp | 1 -
9 files changed, 29 insertions(+), 24 deletions(-)
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 1bb521923..cb598617c 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -191,7 +191,7 @@ namespace opt {
m_msolver->set_adjust_value(m_adjust_value);
is_sat = (*m_msolver)();
if (is_sat != l_false) {
- m_msolver->get_model(m_model);
+ m_msolver->get_model(m_model, m_labels);
}
}
@@ -247,8 +247,9 @@ namespace opt {
m_upper = r;
}
- void maxsmt::get_model(model_ref& mdl) {
+ void maxsmt::get_model(model_ref& mdl, svector<symbol>& labels) {
mdl = m_model.get();
+ labels = m_labels;
}
void maxsmt::commit_assignment() {
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index 8d290a640..7dbf763e2 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -46,7 +46,7 @@ namespace opt {
virtual bool get_assignment(unsigned index) const = 0;
virtual void set_cancel(bool f) = 0;
virtual void collect_statistics(statistics& st) const = 0;
- virtual void get_model(model_ref& mdl) = 0;
+ virtual void get_model(model_ref& mdl, svector<symbol>& labels) = 0;
virtual void updt_params(params_ref& p) = 0;
void set_adjust_value(adjust_value& adj) { m_adjust_value = adj; }
@@ -67,6 +67,7 @@ namespace opt {
rational m_lower;
rational m_upper;
model_ref m_model;
+ svector<symbol> m_labels;
svector<bool> m_assignment; // truth assignment to soft constraints
params_ref m_params; // config
@@ -79,9 +80,9 @@ namespace opt {
virtual bool get_assignment(unsigned index) const { return m_assignment[index]; }
virtual void set_cancel(bool f) { m_cancel = f; if (f) s().cancel(); else s().reset_cancel(); }
virtual void collect_statistics(statistics& st) const { }
- virtual void get_model(model_ref& mdl) { mdl = m_model.get(); }
+ virtual void get_model(model_ref& mdl, svector<symbol>& labels) { mdl = m_model.get(); labels = m_labels;}
virtual void commit_assignment();
- void set_model() { s().get_model(m_model); }
+ void set_model() { s().get_model(m_model); s().get_labels(m_labels); }
virtual void updt_params(params_ref& p);
solver& s();
void init();
@@ -122,6 +123,7 @@ namespace opt {
rational m_upper;
adjust_value m_adjust_value;
model_ref m_model;
+ svector<symbol> m_labels;
params_ref m_params;
public:
maxsmt(maxsat_context& c);
@@ -139,7 +141,7 @@ namespace opt {
rational get_upper() const;
void update_lower(rational const& r);
void update_upper(rational const& r);
- void get_model(model_ref& mdl);
+ void get_model(model_ref& mdl, svector<symbol>& labels);
bool get_assignment(unsigned index) const;
void display_answer(std::ostream& out) const;
void collect_statistics(statistics& st) const;
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 265e3b7c8..1b33c2cf1 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -168,9 +168,7 @@ namespace opt {
}
void context::get_labels(svector<symbol> & r) {
- if (m_solver) {
- m_solver->get_labels(r);
- }
+ r.append(m_labels);
}
void context::set_hard_constraints(ptr_vector<expr>& fmls) {
@@ -234,6 +232,7 @@ namespace opt {
TRACE("opt", tout << "initial search result: " << is_sat << "\n";);
if (is_sat != l_false) {
s.get_model(m_model);
+ s.get_labels(m_labels);
}
if (is_sat != l_true) {
return is_sat;
@@ -282,11 +281,6 @@ namespace opt {
}
}
- void context::set_model(model_ref& mdl) {
- m_model = mdl;
- fix_model(mdl);
- }
-
void context::get_model(model_ref& mdl) {
mdl = m_model;
fix_model(mdl);
@@ -295,7 +289,7 @@ namespace opt {
lbool context::execute_min_max(unsigned index, bool committed, bool scoped, bool is_max) {
if (scoped) get_solver().push();
lbool result = m_optsmt.lex(index, is_max);
- if (result == l_true) m_optsmt.get_model(m_model);
+ if (result == l_true) m_optsmt.get_model(m_model, m_labels);
if (scoped) get_solver().pop(1);
if (result == l_true && committed) m_optsmt.commit_assignment(index);
return result;
@@ -306,7 +300,7 @@ namespace opt {
maxsmt& ms = *m_maxsmts.find(id);
if (scoped) get_solver().push();
lbool result = ms();
- if (result != l_false && (ms.get_model(tmp), tmp.get())) ms.get_model(m_model);
+ if (result != l_false && (ms.get_model(tmp, m_labels), tmp.get())) ms.get_model(m_model, m_labels);
if (scoped) get_solver().pop(1);
if (result == l_true && committed) ms.commit_assignment();
return result;
@@ -459,7 +453,7 @@ namespace opt {
}
void context::yield() {
- m_pareto->get_model(m_model);
+ m_pareto->get_model(m_model, m_labels);
update_bound(true);
update_bound(false);
}
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index b364fe63e..dc180e8e6 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -162,6 +162,7 @@ namespace opt {
bool m_pp_neat;
symbol m_maxsat_engine;
symbol m_logic;
+ svector<symbol> m_labels;
public:
context(ast_manager& m);
virtual ~context();
@@ -180,7 +181,6 @@ namespace opt {
virtual lbool optimize();
virtual bool print_model() const;
virtual void get_model(model_ref& _m);
- virtual void set_model(model_ref& _m);
virtual void fix_model(model_ref& _m);
virtual void collect_statistics(statistics& stats) const;
virtual proof* get_proof() { return 0; }
diff --git a/src/opt/opt_pareto.cpp b/src/opt/opt_pareto.cpp
index 5e1d4b269..dea744a72 100644
--- a/src/opt/opt_pareto.cpp
+++ b/src/opt/opt_pareto.cpp
@@ -38,6 +38,7 @@ namespace opt {
return l_undef;
}
m_solver->get_model(m_model);
+ m_solver->get_labels(m_labels);
IF_VERBOSE(1,
model_ref mdl(m_model);
cb.fix_model(mdl);
@@ -96,6 +97,7 @@ namespace opt {
}
if (is_sat == l_true) {
m_solver->get_model(m_model);
+ m_solver->get_labels(m_labels);
mk_not_dominated_by();
}
return is_sat;
diff --git a/src/opt/opt_pareto.h b/src/opt/opt_pareto.h
index 88a3ce9c1..122f29c55 100644
--- a/src/opt/opt_pareto.h
+++ b/src/opt/opt_pareto.h
@@ -31,7 +31,6 @@ namespace opt {
virtual expr_ref mk_gt(unsigned i, model_ref& model) = 0;
virtual expr_ref mk_ge(unsigned i, model_ref& model) = 0;
virtual expr_ref mk_le(unsigned i, model_ref& model) = 0;
- virtual void set_model(model_ref& m) = 0;
virtual void fix_model(model_ref& m) = 0;
};
class pareto_base {
@@ -42,6 +41,7 @@ namespace opt {
ref<solver> m_solver;
params_ref m_params;
model_ref m_model;
+ svector<symbol> m_labels;
public:
pareto_base(
ast_manager & m,
@@ -77,8 +77,9 @@ namespace opt {
}
virtual lbool operator()() = 0;
- virtual void get_model(model_ref& mdl) {
+ virtual void get_model(model_ref& mdl, svector<symbol>& labels) {
mdl = m_model;
+ labels = m_labels;
}
protected:
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index 02effa337..c9ee61ebc 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -51,6 +51,7 @@ namespace opt {
if (src[i] >= dst[i]) {
dst[i] = src[i];
m_models.set(i, m_s->get_model(i));
+ m_s->get_labels(m_labels);
m_lower_fmls[i] = fmls[i].get();
if (dst[i].is_pos() && !dst[i].is_finite()) { // review: likely done already.
m_lower_fmls[i] = m.mk_false();
@@ -156,7 +157,8 @@ namespace opt {
if (is_sat == l_true) {
disj.reset();
m_s->maximize_objectives(disj);
- m_s->get_model(m_model);
+ m_s->get_model(m_model);
+ m_s->get_labels(m_labels);
for (unsigned i = 0; i < ors.size(); ++i) {
expr_ref tmp(m);
m_model->eval(ors[i].get(), tmp);
@@ -203,6 +205,7 @@ namespace opt {
expr_ref optsmt::update_lower() {
expr_ref_vector disj(m);
m_s->get_model(m_model);
+ m_s->get_labels(m_labels);
m_s->maximize_objectives(disj);
set_max(m_lower, m_s->get_objective_values(), disj);
TRACE("opt",
@@ -331,6 +334,7 @@ namespace opt {
m_s->maximize_objective(obj_index, block);
m_s->get_model(m_model);
+ m_s->get_labels(m_labels);
inf_eps obj = m_s->saved_objective_value(obj_index);
if (obj > m_lower[obj_index]) {
m_lower[obj_index] = obj;
@@ -405,8 +409,9 @@ namespace opt {
return m_upper[i];
}
- void optsmt::get_model(model_ref& mdl) {
+ void optsmt::get_model(model_ref& mdl, svector<symbol> & labels) {
mdl = m_model.get();
+ labels = m_labels;
}
// force lower_bound(i) <= objective_value(i)
diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h
index 10ea9f11c..f4efa25f9 100644
--- a/src/opt/optsmt.h
+++ b/src/opt/optsmt.h
@@ -38,6 +38,7 @@ namespace opt {
svector<smt::theory_var> m_vars;
symbol m_optsmt_engine;
model_ref m_model;
+ svector<symbol> m_labels;
sref_vector<model> m_models;
public:
optsmt(ast_manager& m):
@@ -60,7 +61,7 @@ namespace opt {
inf_eps get_lower(unsigned index) const;
inf_eps get_upper(unsigned index) const;
bool objective_is_model_valid(unsigned index) const;
- void get_model(model_ref& mdl);
+ void get_model(model_ref& mdl, svector<symbol>& labels);
model* get_model(unsigned index) const { return m_models[index]; }
void update_lower(unsigned idx, inf_eps const& r);
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index b0d771ba8..43b2c2e3f 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -250,7 +250,6 @@ public:
return "no reason given";
}
virtual void get_labels(svector<symbol> & r) {
- UNREACHABLE();
}
virtual unsigned get_num_assertions() const {
return m_fmls.size();