diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 6fc59351a..1c0f20233 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2266,7 +2266,7 @@ namespace Microsoft.Z3
}
///
- /// Create a pseudo-Boolean <= constraint.
+ /// Create a pseudo-Boolean less-or-equal constraint.
///
public BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k)
{
diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs
index afd6c11dd..6d75235c6 100644
--- a/src/api/dotnet/Fixedpoint.cs
+++ b/src/api/dotnet/Fixedpoint.cs
@@ -316,6 +316,7 @@ namespace Microsoft.Z3
}
}
+ ///
/// Parse an SMT-LIB2 file with fixedpoint rules.
/// Add the rules to the current fixedpoint context.
/// Return the set of queries in the file.
diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs
index ddbebcfa6..a9499570b 100644
--- a/src/api/dotnet/Optimize.cs
+++ b/src/api/dotnet/Optimize.cs
@@ -97,8 +97,16 @@ namespace Microsoft.Z3
Symbol s = Context.MkSymbol(group);
return Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject);
}
+
- public Status Check() {
+ ///
+ ///
+ /// Check satisfiability of asserted constraints.
+ /// Produce a model that (when the objectives are bounded and
+ /// don't use strict inequalities) meets the objectives.
+ ///
+ ///
+ public Status Check() {
Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject);
switch (r)
{
@@ -149,27 +157,47 @@ namespace Microsoft.Z3
return new Model(Context, x);
}
}
-
+
+ ///
+ /// Declare an arithmetical maximization objective.
+ /// Return a handle to the objective. The handle is used as
+ /// an argument to GetLower and GetUpper.
+ ///
public uint MkMaximize(ArithExpr e)
{
return Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject);
}
+ ///
+ /// Declare an arithmetical minimization objective.
+ /// Similar to MkMaximize.
+ ///
public uint MkMinimize(ArithExpr e)
{
return Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject);
}
+ ///
+ /// Retrieve a lower bound for the objective handle.
+ ///
public ArithExpr GetLower(uint index)
{
return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
}
+
+ ///
+ /// Retrieve an upper bound for the objective handle.
+ ///
public ArithExpr GetUpper(uint index)
{
return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
}
+
+ ///
+ /// Print the context to a string (SMT-LIB parseable benchmark).
+ ///
public override string ToString()
{
return Native.Z3_optimize_to_string(Context.nCtx, NativeObject);
diff --git a/src/opt/inc_sat_solver.cpp b/src/opt/inc_sat_solver.cpp
index a4ec5f380..5eecf42d7 100644
--- a/src/opt/inc_sat_solver.cpp
+++ b/src/opt/inc_sat_solver.cpp
@@ -39,8 +39,9 @@ class inc_sat_solver : public solver {
params_ref m_params;
bool m_optimize_model; // parameter
expr_ref_vector m_fmls;
- expr_ref_vector m_current_fmls;
unsigned_vector m_fmls_lim;
+ unsigned_vector m_fmls_head_lim;
+ unsigned m_fmls_head;
expr_ref_vector m_core;
atom2bool_var m_map;
model_ref m_model;
@@ -61,7 +62,10 @@ public:
inc_sat_solver(ast_manager& m, params_ref const& p):
m(m), m_solver(p,0),
m_params(p), m_optimize_model(false),
- m_fmls(m), m_current_fmls(m), m_core(m), m_map(m),
+ m_fmls(m),
+ m_fmls_head(0),
+ m_core(m),
+ m_map(m),
m_num_scopes(0),
m_dep_core(m),
m_soft(m) {
@@ -127,9 +131,11 @@ public:
if (f) m_preprocess->cancel(); else m_preprocess->reset_cancel();
}
virtual void push() {
+ internalize_formulas();
m_solver.user_push();
++m_num_scopes;
- m_fmls_lim.push_back(m_current_fmls.size());
+ m_fmls_lim.push_back(m_fmls.size());
+ m_fmls_head_lim.push_back(m_fmls_head);
}
virtual void pop(unsigned n) {
if (n < m_num_scopes) { // allow inc_sat_solver to
@@ -139,8 +145,10 @@ public:
m_solver.user_pop(n);
m_num_scopes -= n;
while (n > 0) {
- m_current_fmls.resize(m_fmls_lim.back());
+ m_fmls_head = m_fmls_head_lim.back();
+ m_fmls.resize(m_fmls_lim.back());
m_fmls_lim.pop_back();
+ m_fmls_head_lim.pop_back();
--n;
}
}
@@ -156,8 +164,8 @@ public:
}
}
virtual void assert_expr(expr * t) {
+ TRACE("opt", tout << mk_pp(t, m) << "\n";);
m_fmls.push_back(t);
- m_current_fmls.push_back(t);
}
virtual void set_produce_models(bool f) {}
virtual void collect_param_descrs(param_descrs & r) {
@@ -291,15 +299,14 @@ private:
}
lbool internalize_formulas() {
- if (m_fmls.empty()) {
+ if (m_fmls_head == m_fmls.size()) {
return l_true;
}
dep2asm_t dep2asm;
goal_ref g = alloc(goal, m, true, false); // models, maybe cores are enabled
- for (unsigned i = 0; i < m_fmls.size(); ++i) {
- g->assert_expr(m_fmls[i].get());
+ for (; m_fmls_head < m_fmls.size(); ++m_fmls_head) {
+ g->assert_expr(m_fmls[m_fmls_head].get());
}
- m_fmls.reset();
return internalize_goal(g, dep2asm);
}
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index e032cb80e..79c0ccd72 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -63,7 +63,7 @@ Notes:
#include "opt_context.h"
#include "pb_decl_plugin.h"
#include "opt_params.hpp"
-
+#include "ast_util.h"
using namespace opt;
@@ -101,8 +101,8 @@ public:
strategy_t st):
maxsmt_solver_base(c, ws, soft),
m_B(m), m_asms(m),
- m_mus(m_s, m),
- m_mss(m_s, m),
+ m_mus(c.get_solver(), m),
+ m_mss(c.get_solver(), m),
m_trail(m),
m_st(st),
m_hill_climb(true),
@@ -519,7 +519,7 @@ public:
rational w = split_core(core);
TRACE("opt", display_vec(tout << "minimized core: ", core.size(), core.c_ptr()););
max_resolve(core, w);
- fml = m.mk_not(m.mk_and(m_B.size(), m_B.c_ptr()));
+ fml = mk_not(m, mk_and(m, m_B.size(), m_B.c_ptr()));
s().assert_expr(fml);
m_lower += w;
trace_bounds("maxres");
@@ -811,7 +811,7 @@ public:
expr_ref_vector nsoft(m);
expr_ref fml(m);
for (unsigned i = 0; i < m_soft.size(); ++i) {
- nsoft.push_back(m.mk_not(m_soft[i].get()));
+ nsoft.push_back(mk_not(m, m_soft[i].get()));
}
fml = u.mk_lt(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper);
s().assert_expr(fml);
@@ -880,7 +880,7 @@ public:
for (unsigned i = 0; i < m_soft.size(); ++i) {
n = m_soft[i].get();
if (!m_assignment[i]) {
- n = m.mk_not(n);
+ n = mk_not(m, n);
}
sat_solver->assert_expr(n);
}
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 24c82feb0..d8bc1073f 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -29,13 +29,13 @@ Notes:
#include "uint_set.h"
#include "opt_context.h"
#include "theory_wmaxsat.h"
+#include "ast_util.h"
namespace opt {
maxsmt_solver_base::maxsmt_solver_base(
context& c, vector const& ws, expr_ref_vector const& soft):
- m_s(c.get_solver()),
m(c.get_manager()),
m_c(c),
m_cancel(false), m_soft(m),
@@ -50,6 +50,10 @@ namespace opt {
m_params.copy(p);
}
+ solver& maxsmt_solver_base::s() {
+ return m_c.get_solver();
+ }
+
void maxsmt_solver_base::init_soft(vector const& weights, expr_ref_vector const& soft) {
m_weights.reset();
m_soft.reset();
@@ -78,19 +82,10 @@ namespace opt {
tout << "\n";);
}
- expr* maxsmt_solver_base::mk_not(expr* e) {
- if (m.is_not(e, e)) {
- return e;
- }
- else {
- return m.mk_not(e);
- }
- }
-
void maxsmt_solver_base::set_mus(bool f) {
params_ref p;
p.set_bool("minimize_core", f);
- m_s.updt_params(p);
+ s().updt_params(p);
}
void maxsmt_solver_base::enable_sls(expr_ref_vector const& soft, vector const& ws) {
@@ -149,10 +144,10 @@ namespace opt {
maxsmt::maxsmt(context& c):
- m_s(c.get_solver()), m(c.get_manager()), m_c(c), m_cancel(false),
+ m(c.get_manager()), m_c(c), m_cancel(false),
m_soft_constraints(m), m_answer(m) {}
- lbool maxsmt::operator()(solver* s) {
+ lbool maxsmt::operator()() {
lbool is_sat;
m_msolver = 0;
symbol const& maxsat_engine = m_c.maxsat_engine();
@@ -161,7 +156,7 @@ namespace opt {
if (m_soft_constraints.empty()) {
TRACE("opt", tout << "no constraints\n";);
m_msolver = 0;
- is_sat = m_s.check_sat(0, 0);
+ is_sat = s().check_sat(0, 0);
}
else if (maxsat_engine == symbol("maxres")) {
m_msolver = mk_maxres(m_c, m_weights, m_soft_constraints);
@@ -222,9 +217,9 @@ namespace opt {
// TBD: have to use a different solver
// because we don't push local scope any longer.
return;
- solver::scoped_push _sp(m_s);
+ solver::scoped_push _sp(s());
commit_assignment();
- if (l_true != m_s.check_sat(0,0)) {
+ if (l_true != s().check_sat(0,0)) {
IF_VERBOSE(0, verbose_stream() << "could not verify assignment\n";);
UNREACHABLE();
}
@@ -274,10 +269,10 @@ namespace opt {
expr_ref tmp(m);
tmp = m_soft_constraints[i].get();
if (!get_assignment(i)) {
- tmp = m.mk_not(tmp);
+ tmp = mk_not(m, tmp);
}
TRACE("opt", tout << "committing: " << tmp << "\n";);
- m_s.assert_expr(tmp);
+ s().assert_expr(tmp);
}
}
@@ -327,5 +322,9 @@ namespace opt {
}
}
+ solver& maxsmt::s() {
+ return m_c.get_solver();
+ }
+
};
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index 3bef5bebe..6341d0756 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -58,7 +58,6 @@ namespace opt {
//
class maxsmt_solver_base : public maxsmt_solver {
protected:
- solver& m_s;
ast_manager& m;
context& m_c;
volatile bool m_cancel;
@@ -84,9 +83,8 @@ namespace opt {
void set_model() { s().get_model(m_model); }
virtual void updt_params(params_ref& p);
virtual void init_soft(weights_t& weights, expr_ref_vector const& soft);
- solver& s() { return m_s; }
+ solver& s();
void init();
- expr* mk_not(expr* e);
void set_mus(bool f);
app* mk_fresh_bool(char const* name);
@@ -115,7 +113,6 @@ namespace opt {
class maxsmt {
ast_manager& m;
- solver& m_s;
context& m_c;
scoped_ptr m_msolver;
volatile bool m_cancel;
@@ -129,7 +126,7 @@ namespace opt {
params_ref m_params;
public:
maxsmt(context& c);
- lbool operator()(solver* s);
+ lbool operator()();
void set_cancel(bool f);
void updt_params(params_ref& p);
void add(expr* f, rational const& w);
@@ -150,6 +147,7 @@ namespace opt {
private:
bool is_maxsat_problem(weights_t& ws) const;
void verify_assignment();
+ solver& s();
};
};
diff --git a/src/opt/mus.cpp b/src/opt/mus.cpp
index abb0b326e..0cf9786b2 100644
--- a/src/opt/mus.cpp
+++ b/src/opt/mus.cpp
@@ -22,6 +22,7 @@ Notes:
#include "smt_literal.h"
#include "mus.h"
#include "ast_pp.h"
+#include "ast_util.h"
using namespace opt;
@@ -60,13 +61,6 @@ struct mus::imp {
TRACE("opt", tout << idx << ": " << mk_pp(cls, m) << "\n";);
return idx;
}
-
- expr* mk_not(expr* e) {
- if (m.is_not(e, e)) {
- return e;
- }
- return m.mk_not(e);
- }
lbool get_mus(unsigned_vector& mus) {
// SASSERT: mus does not have duplicates.
@@ -92,7 +86,7 @@ struct mus::imp {
core.pop_back();
expr* cls = m_cls2expr[cls_id].get();
expr_ref not_cls(m);
- not_cls = mk_not(cls);
+ not_cls = mk_not(m, cls);
unsigned sz = assumptions.size();
assumptions.push_back(not_cls);
add_core(core, assumptions);
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 9c720ad97..5004ceb32 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -267,7 +267,7 @@ namespace opt {
model_ref tmp;
maxsmt& ms = *m_maxsmts.find(id);
if (scoped) get_solver().push();
- lbool result = ms(m_solver.get());
+ lbool result = ms();
if (result != l_false && (ms.get_model(tmp), tmp.get())) ms.get_model(m_model);
if (scoped) get_solver().pop(1);
if (result == l_true && committed) ms.commit_assignment();
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 082a4a4b4..b81f07e95 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -911,21 +911,20 @@ namespace sat {
}
m_mc.display(tout);
);
-#define _INSERT_LIT(_l_) \
- SASSERT(is_external((_l_).var())); \
- m_assumption_set.insert(_l_); \
- m_assumptions.push_back(_l_); \
- assign(_l_, justification()); \
-// propagate(false); \
for (unsigned i = 0; !inconsistent() && i < m_user_scope_literals.size(); ++i) {
literal nlit = ~m_user_scope_literals[i];
- _INSERT_LIT(nlit);
+ assign(nlit, justification());
+ // propagate(false);
}
for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) {
literal lit = lits[i];
- _INSERT_LIT(lit);
+ SASSERT(is_external((lit).var()));
+ m_assumption_set.insert(lit);
+ m_assumptions.push_back(lit);
+ assign(lit, justification());
+ // propagate(false);
}
}