From 461e88e34cfd6819343297e1ee87543a1ea3817e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 25 Oct 2016 20:32:13 -0700
Subject: [PATCH] additional robustness check for incremental sat solver core
when it recieves interpreted constants, added PB equality to interface and
special handling of equalities to adddress performance gap documented in #755
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
contrib/cmake/src/solver/CMakeLists.txt | 1 +
src/api/api_pb.cpp | 18 ++
src/api/dotnet/Context.cs | 15 ++
src/api/dotnet/Optimize.cs | 9 +-
src/api/python/z3/z3.py | 20 ++
src/api/z3_api.h | 16 ++
src/sat/sat_solver/inc_sat_solver.cpp | 10 +
src/sat/tactic/goal2sat.cpp | 17 +-
src/sat/tactic/goal2sat.h | 6 +-
src/smt/tactic/smt_tactic.cpp | 55 +-----
src/smt/tactic/smt_tactic.h | 2 -
src/solver/combined_solver.cpp | 1 +
src/solver/solver2tactic.cpp | 179 ++++++++++++++++++
src/solver/solver2tactic.h | 30 +++
src/solver/tactic2solver.cpp | 1 +
src/tactic/arith/bound_manager.cpp | 39 +++-
src/tactic/arith/bound_manager.h | 2 +
src/tactic/nlsat_smt/nl_purify_tactic.cpp | 1 +
.../portfolio/bounded_int2bv_solver.cpp | 10 +
src/tactic/portfolio/smt_strategic_solver.cpp | 3 +
src/util/sorting_network.h | 79 ++++++--
21 files changed, 430 insertions(+), 84 deletions(-)
create mode 100644 src/solver/solver2tactic.cpp
create mode 100644 src/solver/solver2tactic.h
diff --git a/contrib/cmake/src/solver/CMakeLists.txt b/contrib/cmake/src/solver/CMakeLists.txt
index 8142ca872..7f54e7745 100644
--- a/contrib/cmake/src/solver/CMakeLists.txt
+++ b/contrib/cmake/src/solver/CMakeLists.txt
@@ -5,6 +5,7 @@ z3_add_component(solver
mus.cpp
solver.cpp
solver_na2as.cpp
+ solver2tactic.cpp
tactic2solver.cpp
COMPONENT_DEPENDENCIES
model
diff --git a/src/api/api_pb.cpp b/src/api/api_pb.cpp
index 6d5a56d2c..b7c28c34f 100644
--- a/src/api/api_pb.cpp
+++ b/src/api/api_pb.cpp
@@ -57,5 +57,23 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
+ Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args,
+ Z3_ast const args[], int _coeffs[],
+ int k) {
+ Z3_TRY;
+ LOG_Z3_mk_pble(c, num_args, args, _coeffs, k);
+ RESET_ERROR_CODE();
+ pb_util util(mk_c(c)->m());
+ vector<rational> coeffs;
+ for (unsigned i = 0; i < num_args; ++i) {
+ coeffs.push_back(rational(_coeffs[i]));
+ }
+ ast* a = util.mk_eq(num_args, coeffs.c_ptr(), to_exprs(args), rational(k));
+ mk_c(c)->save_ast_trail(a);
+ check_sorts(c, a);
+ RETURN_Z3(of_ast(a));
+ Z3_CATCH_RETURN(0);
+ }
+
};
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 6ca48fcb0..c3c33a41e 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2640,6 +2640,21 @@ namespace Microsoft.Z3
AST.ArrayToNative(args),
coeffs, k));
}
+
+ /// <summary>
+ /// Create a pseudo-Boolean equal constraint.
+ /// </summary>
+ public BoolExpr MkPBEq(int[] coeffs, BoolExpr[] args, int k)
+ {
+ Contract.Requires(args != null);
+ Contract.Requires(coeffs != null);
+ Contract.Requires(args.Length == coeffs.Length);
+ Contract.Requires(Contract.Result<BoolExpr[]>() != null);
+ CheckContextMatch<BoolExpr>(args);
+ return new BoolExpr(this, Native.Z3_mk_pbeq(nCtx, (uint) args.Length,
+ AST.ArrayToNative(args),
+ coeffs, k));
+ }
#endregion
#region Numerals
diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs
index 036aaf2f2..c8954a473 100644
--- a/src/api/dotnet/Optimize.cs
+++ b/src/api/dotnet/Optimize.cs
@@ -258,10 +258,13 @@ namespace Microsoft.Z3
/// <summary>
/// Return a string the describes why the last to check returned unknown
/// </summary>
- public String getReasonUnknown()
+ public String ReasonUnknown
{
- Contract.Ensures(Contract.Result<string>() != null);
- return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
+ get
+ {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
+ }
}
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index a037bbc5d..514a45fc6 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -7654,6 +7654,26 @@ def PbLe(args, k):
_coeffs[i] = coeffs[i]
return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)
+def PbEq(args, k):
+ """Create a Pseudo-Boolean inequality k constraint.
+
+ >>> a, b, c = Bools('a b c')
+ >>> f = PbEq(((a,1),(b,3),(c,2)), 3)
+ """
+ args = _get_args(args)
+ args, coeffs = zip(*args)
+ if __debug__:
+ _z3_assert(len(args) > 0, "Non empty list of arguments expected")
+ ctx = _ctx_from_ast_arg_list(args)
+ if __debug__:
+ _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
+ args = _coerce_expr_list(args, ctx)
+ _args, sz = _to_ast_array(args)
+ _coeffs = (ctypes.c_int * len(coeffs))()
+ for i in range(len(coeffs)):
+ _coeffs[i] = coeffs[i]
+ return BoolRef(Z3_mk_pbeq(ctx.ref(), sz, _args, _coeffs, k), ctx)
+
def solve(*args, **keywords):
"""Solve the constraints `*args`.
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 9e9771884..069f83340 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -861,6 +861,9 @@ typedef enum
- Z3_OP_PB_GE: Generalized Pseudo-Boolean cardinality constraint.
Example 2*x + 3*y + 2*z >= 4
+ - Z3_OP_PB_EQ: Generalized Pseudo-Boolean equality constraint.
+ Example 2*x + 1*y + 2*z + 1*u = 4
+
- Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN: Floating-point rounding mode RNE
- Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY: Floating-point rounding mode RNA
@@ -1166,6 +1169,7 @@ typedef enum {
Z3_OP_PB_AT_MOST=0x900,
Z3_OP_PB_LE,
Z3_OP_PB_GE,
+ Z3_OP_PB_EQ,
// Floating-Point Arithmetic
Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN,
@@ -3913,6 +3917,18 @@ extern "C" {
Z3_ast const args[], int coeffs[],
int k);
+ /**
+ \brief Pseudo-Boolean relations.
+
+ Encode k1*p1 + k2*p2 + ... + kn*pn = k
+
+ def_API('Z3_mk_pbeq', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in_array(1,INT), _in(INT)))
+ */
+
+ Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args,
+ Z3_ast const args[], int coeffs[],
+ int k);
+
/**
\brief Convert a \c Z3_func_decl into \c Z3_ast. This is just type casting.
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 349b60f55..d091339bd 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -371,8 +371,18 @@ private:
return l_undef;
}
g = m_subgoals[0];
+ expr_ref_vector atoms(m);
TRACE("sat", g->display_with_dependencies(tout););
m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true);
+ m_goal2sat.get_interpreted_atoms(atoms);
+ if (!atoms.empty()) {
+ std::stringstream strm;
+ strm << "interpreted atoms sent to SAT solver " << atoms;
+ TRACE("sat", std::cout << strm.str() << "\n";);
+ IF_VERBOSE(1, verbose_stream() << strm.str() << "\n";);
+ set_reason_unknown(strm.str().c_str());
+ return l_undef;
+ }
return l_true;
}
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 4d5542866..136921914 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -59,6 +59,7 @@ struct goal2sat::imp {
bool m_ite_extra;
unsigned long long m_max_memory;
expr_ref_vector m_trail;
+ expr_ref_vector m_interpreted_atoms;
bool m_default_external;
imp(ast_manager & _m, params_ref const & p, sat::solver & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external):
@@ -67,6 +68,7 @@ struct goal2sat::imp {
m_map(map),
m_dep2asm(dep2asm),
m_trail(m),
+ m_interpreted_atoms(m),
m_default_external(default_external) {
updt_params(p);
m_true = sat::null_bool_var;
@@ -128,6 +130,9 @@ struct goal2sat::imp {
m_map.insert(t, v);
l = sat::literal(v, sign);
TRACE("goal2sat", tout << "new_var: " << v << "\n" << mk_ismt2_pp(t, m) << "\n";);
+ if (ext && !is_uninterp_const(t)) {
+ m_interpreted_atoms.push_back(t);
+ }
}
}
else {
@@ -474,7 +479,7 @@ bool goal2sat::has_unsupported_bool(goal const & g) {
return test<unsupported_bool_proc>(g);
}
-goal2sat::goal2sat():m_imp(0) {
+goal2sat::goal2sat():m_imp(0), m_interpreted_atoms(0) {
}
void goal2sat::collect_param_descrs(param_descrs & r) {
@@ -492,10 +497,20 @@ struct goal2sat::scoped_set_imp {
}
};
+
void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external) {
imp proc(g.m(), p, t, m, dep2asm, default_external);
scoped_set_imp set(this, &proc);
proc(g);
+ dealloc(m_interpreted_atoms);
+ m_interpreted_atoms = alloc(expr_ref_vector, g.m());
+ m_interpreted_atoms->append(proc.m_interpreted_atoms);
+}
+
+void goal2sat::get_interpreted_atoms(expr_ref_vector& atoms) {
+ if (m_interpreted_atoms) {
+ atoms.append(*m_interpreted_atoms);
+ }
}
diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h
index c6776f2f7..cd63cd497 100644
--- a/src/sat/tactic/goal2sat.h
+++ b/src/sat/tactic/goal2sat.h
@@ -38,8 +38,11 @@ class goal2sat {
struct imp;
imp * m_imp;
struct scoped_set_imp;
+ expr_ref_vector* m_interpreted_atoms;
+
public:
goal2sat();
+ ~goal2sat() { dealloc(m_interpreted_atoms); }
typedef obj_map<expr, sat::literal> dep2asm_map;
@@ -53,12 +56,13 @@ public:
\remark m doesn't need to be empty. the definitions there are
reused.
-
+
\warning conversion throws a tactic_exception, if it is interrupted (by set_cancel),
an unsupported operator is found, or memory consumption limit is reached (set with param :max-memory).
*/
void operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false);
+ void get_interpreted_atoms(expr_ref_vector& atoms);
};
diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index f2fbcf6d9..2909d8848 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -24,63 +24,10 @@ Notes:
#include"rewriter_types.h"
#include"filter_model_converter.h"
#include"ast_util.h"
+#include"solver2tactic.h"
typedef obj_map<expr, expr *> expr2expr_map;
-void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector<expr>& assumptions, expr2expr_map& bool2dep, ref<filter_model_converter>& fmc) {
- expr2expr_map dep2bool;
- ptr_vector<expr> deps;
- ast_manager& m = g->m();
- expr_ref_vector clause(m);
- unsigned sz = g->size();
- for (unsigned i = 0; i < sz; i++) {
- expr * f = g->form(i);
- expr_dependency * d = g->dep(i);
- if (d == 0 || !g->unsat_core_enabled()) {
- clauses.push_back(f);
- }
- else {
- // create clause (not d1 \/ ... \/ not dn \/ f) when the d's are the assumptions/dependencies of f.
- clause.reset();
- clause.push_back(f);
- deps.reset();
- m.linearize(d, deps);
- SASSERT(!deps.empty()); // d != 0, then deps must not be empty
- ptr_vector<expr>::iterator it = deps.begin();
- ptr_vector<expr>::iterator end = deps.end();
- for (; it != end; ++it) {
- expr * d = *it;
- if (is_uninterp_const(d) && m.is_bool(d)) {
- // no need to create a fresh boolean variable for d
- if (!bool2dep.contains(d)) {
- assumptions.push_back(d);
- bool2dep.insert(d, d);
- }
- clause.push_back(m.mk_not(d));
- }
- else {
- // must normalize assumption
- expr * b = 0;
- if (!dep2bool.find(d, b)) {
- b = m.mk_fresh_const(0, m.mk_bool_sort());
- dep2bool.insert(d, b);
- bool2dep.insert(b, d);
- assumptions.push_back(b);
- if (!fmc) {
- fmc = alloc(filter_model_converter, m);
- }
- fmc->insert(to_app(b)->get_decl());
- }
- clause.push_back(m.mk_not(b));
- }
- }
- SASSERT(clause.size() > 1);
- expr_ref cls(m);
- cls = mk_or(m, clause.size(), clause.c_ptr());
- clauses.push_back(cls);
- }
- }
-}
class smt_tactic : public tactic {
smt_params m_params;
diff --git a/src/smt/tactic/smt_tactic.h b/src/smt/tactic/smt_tactic.h
index dd113634b..a23695fd1 100644
--- a/src/smt/tactic/smt_tactic.h
+++ b/src/smt/tactic/smt_tactic.h
@@ -32,8 +32,6 @@ tactic * mk_smt_tactic(params_ref const & p = params_ref());
tactic * mk_smt_tactic_using(bool auto_config = true, params_ref const & p = params_ref());
-void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector<expr>& assumptions, obj_map<expr, expr*>& bool2dep, ref<filter_model_converter>& fmc);
-
/*
ADD_TACTIC("smt", "apply a SAT based SMT solver.", "mk_smt_tactic(p)")
*/
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index fc76f85c1..2856315bd 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -196,6 +196,7 @@ public:
virtual lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
switch_inc_mode();
+ m_use_solver1_results = false;
return m_solver2->get_consequences(asms, vars, consequences);
}
diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp
new file mode 100644
index 000000000..53b120fea
--- /dev/null
+++ b/src/solver/solver2tactic.cpp
@@ -0,0 +1,179 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+ solver2tactic.cpp
+
+Abstract:
+
+ Convert solver to a tactic.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2016-10-17
+
+Notes:
+
+--*/
+
+#include "solver.h"
+#include "tactic.h"
+#include"filter_model_converter.h"
+#include "solver2tactic.h"
+#include "ast_util.h"
+
+typedef obj_map<expr, expr *> expr2expr_map;
+
+void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector<expr>& assumptions, expr2expr_map& bool2dep, ref<filter_model_converter>& fmc) {
+ expr2expr_map dep2bool;
+ ptr_vector<expr> deps;
+ ast_manager& m = g->m();
+ expr_ref_vector clause(m);
+ unsigned sz = g->size();
+ for (unsigned i = 0; i < sz; i++) {
+ expr * f = g->form(i);
+ expr_dependency * d = g->dep(i);
+ if (d == 0 || !g->unsat_core_enabled()) {
+ clauses.push_back(f);
+ }
+ else {
+ // create clause (not d1 \/ ... \/ not dn \/ f) when the d's are the assumptions/dependencies of f.
+ clause.reset();
+ clause.push_back(f);
+ deps.reset();
+ m.linearize(d, deps);
+ SASSERT(!deps.empty()); // d != 0, then deps must not be empty
+ ptr_vector<expr>::iterator it = deps.begin();
+ ptr_vector<expr>::iterator end = deps.end();
+ for (; it != end; ++it) {
+ expr * d = *it;
+ if (is_uninterp_const(d) && m.is_bool(d)) {
+ // no need to create a fresh boolean variable for d
+ if (!bool2dep.contains(d)) {
+ assumptions.push_back(d);
+ bool2dep.insert(d, d);
+ }
+ clause.push_back(m.mk_not(d));
+ }
+ else {
+ // must normalize assumption
+ expr * b = 0;
+ if (!dep2bool.find(d, b)) {
+ b = m.mk_fresh_const(0, m.mk_bool_sort());
+ dep2bool.insert(d, b);
+ bool2dep.insert(b, d);
+ assumptions.push_back(b);
+ if (!fmc) {
+ fmc = alloc(filter_model_converter, m);
+ }
+ fmc->insert(to_app(b)->get_decl());
+ }
+ clause.push_back(m.mk_not(b));
+ }
+ }
+ SASSERT(clause.size() > 1);
+ expr_ref cls(m);
+ cls = mk_or(m, clause.size(), clause.c_ptr());
+ clauses.push_back(cls);
+ }
+ }
+}
+
+class solver2tactic : public tactic {
+ ast_manager& m;
+ ref<solver> m_solver;
+ params_ref m_params;
+
+public:
+ solver2tactic(solver* s):
+ m(s->get_manager()),
+ m_solver(s)
+ {}
+
+ virtual void updt_params(params_ref const & p) {
+ m_solver->updt_params(p);
+ }
+
+ virtual void collect_param_descrs(param_descrs & r) {
+ m_solver->collect_param_descrs(r);
+ }
+
+ virtual void operator()(/* in */ goal_ref const & in,
+ /* out */ goal_ref_buffer & result,
+ /* out */ model_converter_ref & mc,
+ /* out */ proof_converter_ref & pc,
+ /* out */ expr_dependency_ref & core) {
+ expr_ref_vector clauses(m);
+ expr2expr_map bool2dep;
+ ptr_vector<expr> assumptions;
+ ref<filter_model_converter> fmc;
+ extract_clauses_and_dependencies(in, clauses, assumptions, bool2dep, fmc);
+ m_solver->push();
+ m_solver->assert_expr(clauses);
+ lbool r = m_solver->check_sat(assumptions.size(), assumptions.c_ptr());
+ switch (r) {
+ case l_true:
+ if (in->models_enabled()) {
+ model_ref mdl;
+ m_solver->get_model(mdl);
+ mc = model2model_converter(mdl.get());
+ mc = concat(fmc.get(), mc.get());
+ }
+ in->reset();
+ result.push_back(in.get());
+ pc = 0;
+ core = 0;
+ break;
+ case l_false: {
+ in->reset();
+ proof* pr = 0;
+ expr_dependency* lcore = 0;
+ if (in->proofs_enabled()) {
+ pr = m_solver->get_proof();
+ }
+ if (in->unsat_core_enabled()) {
+ ptr_vector<expr> core;
+ m_solver->get_unsat_core(core);
+ for (unsigned i = 0; i < core.size(); ++i) {
+ lcore = m.mk_join(lcore, m.mk_leaf(bool2dep.find(core[i])));
+ }
+ }
+ in->assert_expr(m.mk_false(), pr, lcore);
+ result.push_back(in.get());
+ mc = 0;
+ pc = 0;
+ core = 0;
+ break;
+ }
+ case l_undef:
+ if (m.canceled()) {
+ throw tactic_exception(Z3_CANCELED_MSG);
+ }
+ throw tactic_exception(m_solver->reason_unknown().c_str());
+ }
+ m_solver->pop(1);
+ }
+
+ virtual void collect_statistics(statistics & st) const {
+ m_solver->collect_statistics(st);
+ }
+ virtual void reset_statistics() {}
+
+ virtual void cleanup() {
+ m_solver = m_solver->translate(m, m_params);
+ }
+ virtual void reset() { cleanup(); }
+
+ virtual void set_logic(symbol const & l) {}
+
+ virtual void set_progress_callback(progress_callback * callback) {
+ m_solver->set_progress_callback(callback);
+ }
+
+ virtual tactic * translate(ast_manager & m) {
+ return alloc(solver2tactic, m_solver->translate(m, m_params));
+ }
+};
+
+tactic* mk_solver2tactic(solver* s) { return alloc(solver2tactic, s); }
diff --git a/src/solver/solver2tactic.h b/src/solver/solver2tactic.h
new file mode 100644
index 000000000..65fbd37b1
--- /dev/null
+++ b/src/solver/solver2tactic.h
@@ -0,0 +1,30 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+ solver2tactic.h
+
+Abstract:
+
+ Convert solver to a tactic.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2016-10-17
+
+Notes:
+
+--*/
+#ifndef SOLVER2TACTIC_H_
+#define SOLVER2TACTIC_H_
+
+#include "tactic.h"
+#include "filter_model_converter.h"
+class solver;
+
+tactic * mk_solver2tactic(solver* s);
+
+void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector<expr>& assumptions, obj_map<expr, expr*>& bool2dep, ref<filter_model_converter>& fmc);
+
+#endif
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index f53301948..213ba5c1c 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -160,6 +160,7 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
}
}
catch (z3_error & ex) {
+ TRACE("tactic2solver", tout << "exception: " << ex.msg() << "\n";);
throw ex;
}
catch (z3_exception & ex) {
diff --git a/src/tactic/arith/bound_manager.cpp b/src/tactic/arith/bound_manager.cpp
index ed77467c3..97d93658c 100644
--- a/src/tactic/arith/bound_manager.cpp
+++ b/src/tactic/arith/bound_manager.cpp
@@ -79,12 +79,23 @@ static bool is_strict(decl_kind k) {
return k == OP_LT || k == OP_GT;
}
+bool bound_manager::is_numeral(expr* v, numeral& n, bool& is_int) {
+ expr* w;
+ if (m_util.is_uminus(v, w) && is_numeral(w, n, is_int)) {
+ n.neg();
+ return true;
+ }
+ return m_util.is_numeral(v, n, is_int);
+}
+
void bound_manager::operator()(expr * f, expr_dependency * d) {
TRACE("bound_manager", tout << "processing:\n" << mk_ismt2_pp(f, m()) << "\n";);
expr * v;
numeral n;
if (is_disjunctive_bound(f, d))
return;
+ if (is_equality_bound(f, d))
+ return;
bool pos = true;
while (m().is_not(f, f))
pos = !pos;
@@ -99,10 +110,10 @@ void bound_manager::operator()(expr * f, expr_dependency * d) {
expr * lhs = t->get_arg(0);
expr * rhs = t->get_arg(1);
bool is_int;
- if (is_uninterp_const(lhs) && m_util.is_numeral(rhs, n, is_int)) {
+ if (is_uninterp_const(lhs) && is_numeral(rhs, n, is_int)) {
v = lhs;
}
- else if (is_uninterp_const(rhs) && m_util.is_numeral(lhs, n, is_int)) {
+ else if (is_uninterp_const(rhs) && is_numeral(lhs, n, is_int)) {
v = rhs;
k = swap_decl(k);
}
@@ -165,6 +176,26 @@ void bound_manager::insert_lower(expr * v, bool strict, numeral const & n, expr_
}
}
+bool bound_manager::is_equality_bound(expr * f, expr_dependency * d) {
+ expr* x, *y;
+ if (!m().is_eq(f, x, y)) {
+ return false;
+ }
+ if (!is_uninterp_const(x)) {
+ std::swap(x, y);
+ }
+ numeral n;
+ bool is_int;
+ if (is_uninterp_const(x) && is_numeral(y, n, is_int)) {
+ insert_lower(x, false, n, d);
+ insert_upper(x, false, n, d);
+ return true;
+ }
+ else {
+ return false;
+ }
+}
+
bool bound_manager::is_disjunctive_bound(expr * f, expr_dependency * d) {
numeral lo, hi, n;
if (!m().is_or(f)) return false;
@@ -176,14 +207,14 @@ bool bound_manager::is_disjunctive_bound(expr * f, expr_dependency * d) {
expr * e = to_app(f)->get_arg(i);
if (!m().is_eq(e, x, y)) return false;
if (is_uninterp_const(x) &&
- m_util.is_numeral(y, n, is_int) && is_int &&
+ is_numeral(y, n, is_int) && is_int &&
(x == v || v == 0)) {
if (v == 0) { v = x; lo = hi = n; }
if (n < lo) lo = n;
if (n > hi) hi = n;
}
else if (is_uninterp_const(y) &&
- m_util.is_numeral(x, n, is_int) && is_int &&
+ is_numeral(x, n, is_int) && is_int &&
(y == v || v == 0)) {
if (v == 0) { v = y; lo = hi = n; }
if (n < lo) lo = n;
diff --git a/src/tactic/arith/bound_manager.h b/src/tactic/arith/bound_manager.h
index cc0d693e9..6a4dc2c96 100644
--- a/src/tactic/arith/bound_manager.h
+++ b/src/tactic/arith/bound_manager.h
@@ -36,6 +36,8 @@ private:
obj_map<expr, expr_dependency*> m_upper_deps;
ptr_vector<expr> m_bounded_vars;
bool is_disjunctive_bound(expr * f, expr_dependency * d);
+ bool is_equality_bound(expr * f, expr_dependency * d);
+ bool is_numeral(expr* v, rational& n, bool& is_int);
void insert_lower(expr * v, bool strict, numeral const & n, expr_dependency * d);
void insert_upper(expr * v, bool strict, numeral const & n, expr_dependency * d);
public:
diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.cpp b/src/tactic/nlsat_smt/nl_purify_tactic.cpp
index d8b016d7b..46b5a51b0 100644
--- a/src/tactic/nlsat_smt/nl_purify_tactic.cpp
+++ b/src/tactic/nlsat_smt/nl_purify_tactic.cpp
@@ -59,6 +59,7 @@ Revision History:
#include "model_smt2_pp.h"
#include "expr_safe_replace.h"
#include "ast_util.h"
+#include "solver2tactic.h"
class nl_purify_tactic : public tactic {
diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp
index f7236351c..688d9403a 100644
--- a/src/tactic/portfolio/bounded_int2bv_solver.cpp
+++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp
@@ -251,6 +251,16 @@ private:
}
sub.insert(e, t);
}
+ else {
+ IF_VERBOSE(1,
+ verbose_stream() << "unprocessed entry: " << mk_pp(e, m) << "\n";
+ if (bm.has_lower(e, lo, s1)) {
+ verbose_stream() << "lower: " << lo << " " << s1 << "\n";
+ }
+ if (bm.has_upper(e, hi, s2)) {
+ verbose_stream() << "upper: " << hi << " " << s2 << "\n";
+ });
+ }
}
}
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index 81825221e..d2414ec72 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -40,6 +40,7 @@ Notes:
#include"inc_sat_solver.h"
#include"fd_solver.h"
#include"bv_rewriter.h"
+#include"solver2tactic.h"
tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const & logic) {
@@ -89,6 +90,8 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
return mk_qffpbv_tactic(m, p);
else if (logic=="HORN")
return mk_horn_tactic(m, p);
+ else if (logic == "QF_FD")
+ return mk_solver2tactic(mk_fd_solver(m, p));
//else if (logic=="QF_UFNRA")
// return mk_qfufnra_tactic(m, p);
else
diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h
index 0f5d2838e..9e35d6e8b 100644
--- a/src/util/sorting_network.h
+++ b/src/util/sorting_network.h
@@ -202,7 +202,8 @@ Notes:
return ge(full, k, n, in.c_ptr());
}
else if (k == 1) {
- return mk_at_most_1(full, n, xs);
+ literal_vector ors;
+ return mk_at_most_1(full, n, xs, ors);
}
else {
SASSERT(2*k <= n);
@@ -221,6 +222,9 @@ Notes:
if (dualize(k, n, xs, in)) {
return eq(k, n, in.c_ptr());
}
+ else if (k == 1) {
+ return mk_exactly_1(true, n, xs);
+ }
else {
SASSERT(2*k <= n);
m_t = EQ;
@@ -238,12 +242,56 @@ Notes:
private:
- literal mk_at_most_1(bool full, unsigned n, literal const* xs) {
+
+ literal mk_and(literal l1, literal l2) {
+ literal result = fresh();
+ add_clause(ctx.mk_not(result), l1);
+ add_clause(ctx.mk_not(result), l2);
+ add_clause(ctx.mk_not(l1), ctx.mk_not(l2), result);
+ return result;
+ }
+
+ void mk_implies_or(literal l, unsigned n, literal const* xs) {
+ literal_vector lits(n, xs);
+ lits.push_back(ctx.mk_not(l));
+ add_clause(lits);
+ }
+
+ void mk_or_implies(literal l, unsigned n, literal const* xs) {
+ for (unsigned j = 0; j < n; ++j) {
+ add_clause(ctx.mk_not(xs[j]), l);
+ }
+ }
+
+ literal mk_or(literal_vector const& ors) {
+ if (ors.size() == 1) {
+ return ors[0];
+ }
+ literal result = fresh();
+ mk_implies_or(result, ors.size(), ors.c_ptr());
+ mk_or_implies(result, ors.size(), ors.c_ptr());
+ return result;
+ }
+
+ literal mk_exactly_1(bool full, unsigned n, literal const* xs) {
+ literal_vector ors;
+ literal r1 = mk_at_most_1(full, n, xs, ors);
+
+ if (full) {
+ r1 = mk_and(r1, mk_or(ors));
+ }
+ else {
+ mk_implies_or(r1, ors.size(), ors.c_ptr());
+ }
+ return r1;
+ }
+
+ literal mk_at_most_1(bool full, unsigned n, literal const* xs, literal_vector& ors) {
TRACE("pb", tout << (full?"full":"partial") << " ";
for (unsigned i = 0; i < n; ++i) tout << xs[i] << " ";
tout << "\n";);
- if (!full && n >= 4) {
+ if (false && !full && n >= 4) {
return mk_at_most_1_bimander(n, xs);
}
literal_vector in(n, xs);
@@ -252,9 +300,10 @@ Notes:
literal_vector ands;
ands.push_back(result);
while (!in.empty()) {
- literal_vector ors;
+ ors.reset();
unsigned i = 0;
unsigned n = in.size();
+ if (n + 1 == inc_size) ++inc_size;
bool last = n <= inc_size;
for (; i + inc_size < n; i += inc_size) {
mk_at_most_1_small(full, last, inc_size, in.c_ptr() + i, result, ands, ors);
@@ -267,7 +316,6 @@ Notes:
}
in.reset();
in.append(ors);
- ors.reset();
}
if (full) {
add_clause(ands);
@@ -278,23 +326,16 @@ Notes:
void mk_at_most_1_small(bool full, bool last, unsigned n, literal const* xs, literal result, literal_vector& ands, literal_vector& ors) {
SASSERT(n > 0);
if (n == 1) {
- if (!last) {
- ors.push_back(xs[0]);
- }
+ ors.push_back(xs[0]);
return;
}
- if (!last) {
- literal ex = fresh();
- for (unsigned j = 0; j < n; ++j) {
- add_clause(ctx.mk_not(xs[j]), ex);
- }
- if (full) {
- literal_vector lits(n, xs);
- lits.push_back(ctx.mk_not(ex));
- add_clause(lits.size(), lits.c_ptr());
- }
- ors.push_back(ex);
+ literal ex = fresh();
+ mk_or_implies(ex, n, xs);
+ if (full) {
+ mk_implies_or(ex, n, xs);
}
+ ors.push_back(ex);
+
// result => xs[0] + ... + xs[n-1] <= 1
for (unsigned i = 0; i < n; ++i) {
for (unsigned j = i + 1; j < n; ++j) {