mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

Merge remote-tracking branch 'origin/master' into polysat

Browse source
This commit is contained in:
Jakob Rath 2023-02-06 10:50:05 +01:00
commit 8774952aeb
40 changed files with 708 additions and 189 deletions
Download patch file Download diff file Expand all files Collapse all files

4
scripts/mk_nuget_task.py
View file

@ -25,9 +25,11 @@ os_info = { 'ubuntu-latest' : ('so', 'linux-x64'),
'ubuntu-18' : ('so', 'linux-x64'),
'ubuntu-20' : ('so', 'linux-x64'),
'glibc-2.31' : ('so', 'linux-x64'),
'glibc' : ('so', 'linux-x64'),
'x64-win' : ('dll', 'win-x64'),
'x86-win' : ('dll', 'win-x86'),
'osx' : ('dylib', 'osx-x64'),
'x64-osx' : ('dylib', 'osx-x64'),
'arm64-osx' : ('dylib', 'osx-arm64'),
'debian' : ('so', 'linux-x64') }

34
src/api/api_solver.cpp
View file

@ -233,16 +233,38 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
/**
* attach a simplifier to solver.
* This is legal when the solver is fresh, does not already have assertions (and scopes).
* To allow recycling the argument solver, we create a fresh copy of it and pass it to
* mk_simplifier_solver.
*/
Z3_solver Z3_API Z3_solver_add_simplifier(Z3_context c, Z3_solver solver, Z3_simplifier simplifier) {
Z3_TRY;
LOG_Z3_solver_add_simplifier(c, solver, simplifier);
init_solver(c, solver);
solver_ref s_fresh;
if (to_solver(solver)->m_solver) {
s_fresh = to_solver_ref(solver)->translate(mk_c(c)->m(), to_solver(solver)->m_params);
}
else {
// create the solver, but hijack it for internal uses.
init_solver(c, solver);
s_fresh = to_solver(solver)->m_solver;
to_solver(solver)->m_solver = nullptr;
}
if (!s_fresh) {
SET_ERROR_CODE(Z3_INVALID_ARG, "unexpected empty solver state");
RETURN_Z3(nullptr);
}
if (s_fresh->get_num_assertions() > 0) {
SET_ERROR_CODE(Z3_INVALID_ARG, "adding a simplifier to a solver with assertions is not allowed.");
RETURN_Z3(nullptr);
}
auto simp = to_simplifier_ref(simplifier);
auto* slv = mk_simplifier_solver(to_solver_ref(solver), simp);
Z3_solver_ref* sr = alloc(Z3_solver_ref, *mk_c(c), slv);
mk_c(c)->save_object(sr);
// ?? init_solver_log(c, sr)
RETURN_Z3(of_solver(sr));
auto* simplifier_solver = mk_simplifier_solver(s_fresh.get(), simp);
Z3_solver_ref* result = alloc(Z3_solver_ref, *mk_c(c), simplifier_solver);
mk_c(c)->save_object(result);
RETURN_Z3(of_solver(result));
Z3_CATCH_RETURN(nullptr);
}

1
src/api/dotnet/CMakeLists.txt
View file

@ -103,6 +103,7 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
SeqExpr.cs
SeqSort.cs
SetSort.cs
Simplifiers.cs
Solver.cs
Sort.cs
Statistics.cs

116
src/api/dotnet/Context.cs
View file

@ -3726,6 +3726,110 @@ namespace Microsoft.Z3
}
#endregion
#region Simplifiers
/// <summary>
/// The number of supported simplifiers.
/// </summary>
public uint NumSimplifiers
{
get { return Native.Z3_get_num_simplifiers(nCtx); }
}
/// <summary>
/// The names of all supported tactics.
/// </summary>
public string[] SimplifierNames
{
get
{
uint n = NumSimplifiers;
string[] res = new string[n];
for (uint i = 0; i < n; i++)
res[i] = Native.Z3_get_simplifier_name(nCtx, i);
return res;
}
}
/// <summary>
/// Returns a string containing a description of the simplifier with the given name.
/// </summary>
public string SimplifierDescription(string name)
{
return Native.Z3_simplifier_get_descr(nCtx, name);
}
/// <summary>
/// Creates a new Tactic.
/// </summary>
public Simplifier MkSimplifier(string name)
{
return new Simplifier(this, name);
}
/// <summary>
/// Create a simplifie that applies <paramref name="t1"/> and
/// then <paramref name="t2"/>.
/// </summary>
public Simplifier AndThen(Simplifier t1, Simplifier t2, params Simplifier[] ts)
{
Debug.Assert(t1 != null);
Debug.Assert(t2 != null);
// Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
CheckContextMatch(t1);
CheckContextMatch(t2);
CheckContextMatch<Simplifier>(ts);
IntPtr last = IntPtr.Zero;
if (ts != null && ts.Length > 0)
{
last = ts[ts.Length - 1].NativeObject;
for (int i = ts.Length - 2; i >= 0; i--)
last = Native.Z3_simplifier_and_then(nCtx, ts[i].NativeObject, last);
}
if (last != IntPtr.Zero)
{
last = Native.Z3_simplifier_and_then(nCtx, t2.NativeObject, last);
return new Simplifier(this, Native.Z3_simplifier_and_then(nCtx, t1.NativeObject, last));
}
else
return new Simplifier(this, Native.Z3_simplifier_and_then(nCtx, t1.NativeObject, t2.NativeObject));
}
/// <summary>
/// Create a simplifier that applies <paramref name="t1"/> and then
/// then <paramref name="t2"/>.
/// </summary>
/// <remarks>
/// Shorthand for <c>AndThen</c>.
/// </remarks>
public Simplifier Then(Simplifier t1, Simplifier t2, params Simplifier[] ts)
{
Debug.Assert(t1 != null);
Debug.Assert(t2 != null);
// Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
return AndThen(t1, t2, ts);
}
/// <summary>
/// Create a tactic that applies <paramref name="t"/> using the given set of parameters <paramref name="p"/>.
/// </summary>
public Simplifier UsingParams(Simplifier t, Params p)
{
Debug.Assert(t != null);
Debug.Assert(p != null);
CheckContextMatch(t);
CheckContextMatch(p);
return new Simplifier(this, Native.Z3_simplifier_using_params(nCtx, t.NativeObject, p.NativeObject));
}
#endregion
#region Probes
/// <summary>
/// The number of supported Probes.
@ -3926,6 +4030,16 @@ namespace Microsoft.Z3
return new Solver(this, Native.Z3_mk_simple_solver(nCtx));
}
/// <summary>
/// Creates a solver that uses an incremental simplifier.
/// </summary>
public Solver MkSolver(Solver s, Simplifier t)
{
Debug.Assert(t != null);
Debug.Assert(s != null);
return new Solver(this, Native.Z3_solver_add_simplifier(nCtx, s.NativeObject, t.NativeObject));
}
/// <summary>
/// Creates a solver that is implemented using the given tactic.
/// </summary>
@ -3939,6 +4053,8 @@ namespace Microsoft.Z3
return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject));
}
#endregion
#region Fixedpoints

78
src/api/dotnet/Simplifiers.cs Normal file
View file

@ -0,0 +1,78 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
Simplifiers.cs
Abstract:
Z3 Managed API: Simplifiers
Author:
Christoph Wintersteiger (cwinter) 2012-03-21
--*/
using System;
using System.Diagnostics;
namespace Microsoft.Z3
{
/// <summary>
/// Simplifiers are the basic building block for creating custom solvers with incremental pre-processing.
/// The complete list of simplifiers may be obtained using <c>Context.NumSimplifiers</c>
/// and <c>Context.SimplifierNames</c>.
/// It may also be obtained using the command <c>(help-simplifier)</c> in the SMT 2.0 front-end.
/// </summary>
public class Simplifier : Z3Object
{
/// <summary>
/// A string containing a description of parameters accepted by the tactic.
/// </summary>
public string Help
{
get
{
return Native.Z3_simplifier_get_help(Context.nCtx, NativeObject);
}
}
/// <summary>
/// Retrieves parameter descriptions for Simplifiers.
/// </summary>
public ParamDescrs ParameterDescriptions
{
get { return new ParamDescrs(Context, Native.Z3_simplifier_get_param_descrs(Context.nCtx, NativeObject)); }
}
#region Internal
internal Simplifier(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Debug.Assert(ctx != null);
}
internal Simplifier(Context ctx, string name)
: base(ctx, Native.Z3_mk_simplifier(ctx.nCtx, name))
{
Debug.Assert(ctx != null);
}
internal override void IncRef(IntPtr o)
{
Native.Z3_simplifier_inc_ref(Context.nCtx, o);
}
internal override void DecRef(IntPtr o)
{
lock (Context)
{
if (Context.nCtx != IntPtr.Zero)
Native.Z3_simplifier_dec_ref(Context.nCtx, o);
}
}
#endregion
}
}

2
src/api/java/CMakeLists.txt
View file

@ -165,6 +165,8 @@ set(Z3_JAVA_JAR_SOURCE_FILES
SeqExpr.java
SeqSort.java
SetSort.java
Simplifier.java
SimplifierDecRefQueue.java
SolverDecRefQueue.java
Solver.java
Sort.java

115
src/api/java/Context.java
View file

@ -3081,6 +3081,106 @@ public class Context implements AutoCloseable {
Native.interrupt(nCtx());
}
/**
* The number of supported simplifiers.
**/
public int getNumSimplifiers()
{
return Native.getNumSimplifiers(nCtx());
}
/**
* The names of all supported simplifiers.
**/
public String[] getSimplifierNames()
{
int n = getNumSimplifiers();
String[] res = new String[n];
for (int i = 0; i < n; i++)
res[i] = Native.getSimplifierName(nCtx(), i);
return res;
}
/**
* Returns a string containing a description of the simplifier with the given
* name.
**/
public String getSimplifierDescription(String name)
{
return Native.simplifierGetDescr(nCtx(), name);
}
/**
* Creates a new Simplifier.
**/
public Simplifier mkSimplifier(String name)
{
return new Simplifier(this, name);
}
/**
* Create a simplifier that applies {@code t1} and then {@code t1}
**/
public Simplifier andThen(Simplifier t1, Simplifier t2, Simplifier... ts)
{
checkContextMatch(t1);
checkContextMatch(t2);
checkContextMatch(ts);
long last = 0;
if (ts != null && ts.length > 0)
{
last = ts[ts.length - 1].getNativeObject();
for (int i = ts.length - 2; i >= 0; i--) {
last = Native.simplifierAndThen(nCtx(), ts[i].getNativeObject(),
last);
}
}
if (last != 0)
{
last = Native.simplifierAndThen(nCtx(), t2.getNativeObject(), last);
return new Simplifier(this, Native.simplifierAndThen(nCtx(),
t1.getNativeObject(), last));
} else
return new Simplifier(this, Native.simplifierAndThen(nCtx(),
t1.getNativeObject(), t2.getNativeObject()));
}
/**
* Create a simplifier that applies {@code t1} and then {@code t2}
*
* Remarks: Shorthand for {@code AndThen}.
**/
public Simplifier then(Simplifier t1, Simplifier t2, Simplifier... ts)
{
return andThen(t1, t2, ts);
}
/**
* Create a simplifier that applies {@code t} using the given set of
* parameters {@code p}.
**/
public Simplifier usingParams(Simplifier t, Params p)
{
checkContextMatch(t);
checkContextMatch(p);
return new Simplifier(this, Native.simplifierUsingParams(nCtx(),
t.getNativeObject(), p.getNativeObject()));
}
/**
* Create a simplifier that applies {@code t} using the given set of
* parameters {@code p}.
* Remarks: Alias for
* {@code UsingParams}
**/
public Simplifier with(Simplifier t, Params p)
{
return usingParams(t, p);
}
/**
* The number of supported Probes.
**/
@ -3279,6 +3379,14 @@ public class Context implements AutoCloseable {
t.getNativeObject()));
}
/**
* Creates a solver that is uses the simplifier pre-processing.
**/
public Solver mkSolver(Solver s, Simplifier simp)
{
return new Solver(this, Native.solverAddSimplifier(nCtx(), s.getNativeObject(), simp.getNativeObject()));
}
/**
* Create a Fixedpoint context.
**/
@ -4209,6 +4317,7 @@ public class Context implements AutoCloseable {
private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue();
private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue();
private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue();
private SimplifierDecRefQueue m_Simplifier_DRQ = new SimplifierDecRefQueue();
private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue();
private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue();
private ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue();
@ -4293,6 +4402,11 @@ public class Context implements AutoCloseable {
return m_Tactic_DRQ;
}
public IDecRefQueue<Simplifier> getSimplifierDRQ()
{
return m_Simplifier_DRQ;
}
public IDecRefQueue<Fixedpoint> getFixedpointDRQ()
{
return m_Fixedpoint_DRQ;
@ -4323,6 +4437,7 @@ public class Context implements AutoCloseable {
m_Optimize_DRQ.forceClear(this);
m_Statistics_DRQ.forceClear(this);
m_Tactic_DRQ.forceClear(this);
m_Simplifier_DRQ.forceClear(this);
m_Fixedpoint_DRQ.forceClear(this);
m_boolSort = null;

58
src/api/java/Simplifier.java Normal file
View file

@ -0,0 +1,58 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
Simplifiers.cs
Abstract:
Z3 Managed API: Simplifiers
Author:
Christoph Wintersteiger (cwinter) 2012-03-21
--*/
package com.microsoft.z3;
public class Simplifier extends Z3Object {
/*
* A string containing a description of parameters accepted by the simplifier.
*/
public String getHelp()
{
return Native.simplifierGetHelp(getContext().nCtx(), getNativeObject());
}
/*
* Retrieves parameter descriptions for Simplifiers.
*/
public ParamDescrs getParameterDescriptions() {
return new ParamDescrs(getContext(), Native.simplifierGetParamDescrs(getContext().nCtx(), getNativeObject()));
}
Simplifier(Context ctx, long obj)
{
super(ctx, obj);
}
Simplifier(Context ctx, String name)
{
super(ctx, Native.mkSimplifier(ctx.nCtx(), name));
}
@Override
void incRef()
{
Native.simplifierIncRef(getContext().nCtx(), getNativeObject());
}
@Override
void addToReferenceQueue() {
getContext().getSimplifierDRQ().storeReference(getContext(), this);
}
}

31
src/api/java/SimplifierDecRefQueue.java Normal file
View file

@ -0,0 +1,31 @@
/**
Copyright (c) 2012-2014 Microsoft Corporation
Module Name:
SimplifierDecRefQueue.java
Abstract:
Author:
@author Christoph Wintersteiger (cwinter) 2012-03-15
Notes:
**/
package com.microsoft.z3;
class SimplifierDecRefQueue extends IDecRefQueue<Simplifier> {
public SimplifierDecRefQueue()
{
super();
}
@Override
protected void decRef(Context ctx, long obj)
{
Native.simplifierDecRef(ctx.nCtx(), obj);
}
}

4
src/api/python/z3/z3.py
View file

@ -8214,8 +8214,6 @@ class Simplifier:
def add(self, solver):
"""Return a solver that applies the simplification pre-processing specified by the simplifier"""
print(solver.solver)
print(self.simplifier)
return Solver(Z3_solver_add_simplifier(self.ctx.ref(), solver.solver, self.simplifier), self.ctx)
def help(self):
@ -9074,7 +9072,7 @@ def PbGe(args, k):
def PbEq(args, k, ctx=None):
"""Create a Pseudo-Boolean inequality k constraint.
"""Create a Pseudo-Boolean equality k constraint.
>>> a, b, c = Bools('a b c')
>>> f = PbEq(((a,1),(b,3),(c,2)), 3)

2
src/ast/recfun_decl_plugin.h
View file

@ -60,7 +60,7 @@ namespace recfun {
func_decl_ref m_pred; //<! predicate used for this case
expr_ref_vector m_guards; //<! conjunction that is equivalent to this case
expr_ref m_rhs; //<! if guard is true, `f(t1...tn) = rhs` holds
def * m_def; //<! definition this is a part of
def * m_def = nullptr;; //<! definition this is a part of
bool m_immediate = false; //<! does `rhs` contain no defined_fun/case_pred?
case_def(ast_manager& m):

3
src/ast/simplifiers/dependent_expr_state.h
View file

@ -90,7 +90,8 @@ public:
* Freeze internal functions
*/
void freeze(expr* term);
bool frozen(func_decl* f) const { return m_frozen.is_marked(f); }
void freeze(expr_ref_vector const& terms) { for (expr* t : terms) freeze(t); }
bool frozen(func_decl* f) const { return m_frozen.is_marked(f); }
bool frozen(expr* f) const { return is_app(f) && m_frozen.is_marked(to_app(f)->get_decl()); }
void freeze_suffix();

14
src/ast/simplifiers/dominator_simplifier.cpp
View file

@ -41,7 +41,7 @@ expr_ref dominator_simplifier::simplify_ite(app * ite) {
if (is_subexpr(child, t) && !is_subexpr(child, e))
simplify_rec(child);
pop(scope_level() - old_lvl);
local_pop(scope_level() - old_lvl);
expr_ref new_t = simplify_arg(t);
reset_cache();
if (!assert_expr(new_c, true)) {
@ -50,7 +50,7 @@ expr_ref dominator_simplifier::simplify_ite(app * ite) {
for (expr * child : tree(ite))
if (is_subexpr(child, e) && !is_subexpr(child, t))
simplify_rec(child);
pop(scope_level() - old_lvl);
local_pop(scope_level() - old_lvl);
expr_ref new_e = simplify_arg(e);
if (c == new_c && t == new_t && e == new_e) {
@ -159,7 +159,7 @@ expr_ref dominator_simplifier::simplify_and_or(bool is_and, app * e) {
r = simplify_arg(arg);
args.push_back(r);
if (!assert_expr(r, !is_and)) {
pop(scope_level() - old_lvl);
local_pop(scope_level() - old_lvl);
r = is_and ? m.mk_false() : m.mk_true();
reset_cache();
return true;
@ -181,7 +181,7 @@ expr_ref dominator_simplifier::simplify_and_or(bool is_and, app * e) {
args.reverse();
}
pop(scope_level() - old_lvl);
local_pop(scope_level() - old_lvl);
reset_cache();
return { is_and ? mk_and(args) : mk_or(args), m };
}
@ -191,7 +191,7 @@ expr_ref dominator_simplifier::simplify_not(app * e) {
ENSURE(m.is_not(e, ee));
unsigned old_lvl = scope_level();
expr_ref t = simplify_rec(ee);
pop(scope_level() - old_lvl);
local_pop(scope_level() - old_lvl);
reset_cache();
return mk_not(t);
}
@ -245,7 +245,7 @@ void dominator_simplifier::reduce() {
}
m_fmls.update(i, dependent_expr(m, r, new_pr, d));
}
pop(scope_level());
local_pop(scope_level());
// go backwards
m_forward = false;
@ -268,7 +268,7 @@ void dominator_simplifier::reduce() {
}
m_fmls.update(i, dependent_expr(m, r, new_pr, d));
}
pop(scope_level());
local_pop(scope_level());
}
SASSERT(scope_level() == 0);
}

2
src/ast/simplifiers/dominator_simplifier.h
View file

@ -48,7 +48,7 @@ class dominator_simplifier : public dependent_expr_simplifier {
expr* idom(expr *e) const { return m_dominators.idom(e); }
unsigned scope_level() { return m_simplifier->scope_level(); }
void pop(unsigned n) { SASSERT(n <= m_simplifier->scope_level()); m_simplifier->pop(n); }
void local_pop(unsigned n) { SASSERT(n <= m_simplifier->scope_level()); m_simplifier->pop(n); }
bool assert_expr(expr* f, bool sign) { return m_simplifier->assert_expr(f, sign); }

9
src/ast/simplifiers/eliminate_predicates.cpp
View file

@ -567,9 +567,9 @@ void eliminate_predicates::try_find_macro(clause& cl) {
return false;
app* x = to_app(_x);
return
can_be_quasi_macro_head(x, cl.m_bound.size()) &&
is_macro_safe(y) &&
!occurs(x->get_decl(), y);
can_be_quasi_macro_head(x, cl.m_bound.size()) &&
is_macro_safe(y) &&
!occurs(x->get_decl(), y);
};
if (cl.is_unit() && m.is_eq(cl.atom(0), x, y)) {
@ -592,7 +592,8 @@ void eliminate_predicates::try_find_macro(clause& cl) {
}
if (cl.is_unit()) {
expr* body = cl.sign(0) ? m.mk_false() : m.mk_true();
if (can_be_qdef(cl.atom(0), body)) {
expr* x = cl.atom(0);
if (can_be_qdef(x, body)) {
insert_quasi_macro(to_app(x), body, cl);
return;
}

1
src/ast/substitution/demodulator_rewriter.cpp
View file

@ -780,7 +780,6 @@ void demodulator_rewriter::operator()(expr_ref_vector const& exprs,
demodulator_match_subst::demodulator_match_subst(ast_manager & m):
m(m),
m_subst(m) {
}

1
src/ast/substitution/demodulator_rewriter.h
View file

@ -111,7 +111,6 @@ class demodulator_match_subst {
typedef std::pair<expr *, expr *> expr_pair;
typedef obj_pair_hashtable<expr, expr> cache;
ast_manager & m;
substitution m_subst;
cache m_cache;
svector<expr_pair> m_todo;

5
src/cmd_context/tactic_cmds.cpp
View file

@ -296,9 +296,10 @@ public:
}
void execute(cmd_context & ctx) override {
if (!m_tactic) {
if (!m_tactic)
throw cmd_exception("apply needs a tactic argument");
}
if (ctx.ignore_check())
return;
params_ref p = ctx.params().merge_default_params(ps());
tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
{

7
src/math/dd/dd_pdd.cpp
View file

@ -190,7 +190,7 @@ namespace dd {
while (p2 != 0 && !m_todo.empty()) {
PDD r = m_todo.back();
m_todo.pop_back();
if (is_marked(r))
if (is_marked(r))
continue;
set_mark(r);
if (!is_val(r)) {
@ -203,7 +203,7 @@ namespace dd {
p2 = val(r).trailing_zeros();
}
m_todo.reset();
return p2;
return p2;
}
pdd pdd_manager::subst_val(pdd const& p, pdd const& s) {
@ -1816,9 +1816,8 @@ namespace dd {
pdd p = *this;
while (!p.is_val())
p = p.lo();
return p.val();
return p.val();
}
pdd pdd::shl(unsigned n) const {
return (*this) * rational::power_of_two(n);

2
src/math/lp/lar_core_solver.h
View file

@ -222,7 +222,7 @@ public:
m_d_x.resize(m_d_A.column_count());
pop_basis(k);
m_stacked_simplex_strategy.pop(k);
settings().simplex_strategy() = m_stacked_simplex_strategy;
settings().set_simplex_strategy(m_stacked_simplex_strategy);
lp_assert(m_r_solver.basis_heading_is_correct());
lp_assert(!need_to_presolve_with_double_solver() || m_d_solver.basis_heading_is_correct());
}

10
src/math/lp/lar_solver.cpp
View file

@ -300,7 +300,7 @@ namespace lp {
m_term_register.shrink(m_term_count);
m_terms.resize(m_term_count);
m_simplex_strategy.pop(k);
m_settings.simplex_strategy() = m_simplex_strategy;
m_settings.set_simplex_strategy(m_simplex_strategy);
lp_assert(sizes_are_correct());
lp_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
m_usage_in_terms.pop(k);
@ -465,10 +465,10 @@ namespace lp {
switch (settings().simplex_strategy()) {
case simplex_strategy_enum::tableau_rows:
settings().simplex_strategy() = simplex_strategy_enum::tableau_costs;
settings().set_simplex_strategy(simplex_strategy_enum::tableau_costs);
prepare_costs_for_r_solver(term);
ret = maximize_term_on_tableau(term, term_max);
settings().simplex_strategy() = simplex_strategy_enum::tableau_rows;
settings().set_simplex_strategy(simplex_strategy_enum::tableau_rows);
set_costs_to_zero(term);
m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::OPTIMAL);
return ret;
@ -2006,10 +2006,10 @@ namespace lp {
void lar_solver::decide_on_strategy_and_adjust_initial_state() {
lp_assert(strategy_is_undecided());
if (m_columns_to_ul_pairs.size() > m_settings.column_number_threshold_for_using_lu_in_lar_solver) {
m_settings.simplex_strategy() = simplex_strategy_enum::lu;
m_settings.set_simplex_strategy(simplex_strategy_enum::lu);
}
else {
m_settings.simplex_strategy() = simplex_strategy_enum::tableau_rows; // todo: when to switch to tableau_costs?
m_settings.set_simplex_strategy(simplex_strategy_enum::tableau_rows); // todo: when to switch to tableau_costs?
}
adjust_initial_state();
}

2
src/math/lp/lp_core_solver_base.h
View file

@ -74,9 +74,9 @@ public:
vector<X> & m_x; // a feasible solution, the fist time set in the constructor
vector<T> & m_costs;
lp_settings & m_settings;
lu<static_matrix<T, X>> * m_factorization = nullptr;
vector<T> m_y; // the buffer for yB = cb
// a device that is able to solve Bx=c, xB=d, and change the basis
lu<static_matrix<T, X>> * m_factorization;
const column_namer & m_column_names;
indexed_vector<T> m_w; // the vector featuring in 24.3 of the Chvatal book
vector<T> m_d; // the vector of reduced costs

1
src/math/lp/lp_core_solver_base_def.h
View file

@ -55,7 +55,6 @@ lp_core_solver_base(static_matrix<T, X> & A,
m_costs(costs),
m_settings(settings),
m_y(m_m()),
m_factorization(nullptr),
m_column_names(column_names),
m_w(m_m()),
m_d(m_n()),

4
src/math/lp/lp_settings.h
View file

@ -336,8 +336,8 @@ public:
return m_simplex_strategy;
}
simplex_strategy_enum & simplex_strategy() {
return m_simplex_strategy;
void set_simplex_strategy(simplex_strategy_enum s) {
m_simplex_strategy = s;
}
bool use_lu() const {

2
src/math/lp/nla_powers.cpp
View file

@ -131,7 +131,7 @@ namespace nla {
return l_false;
}
if (xval >= 3 && yval != 0 & rval <= yval + 1) {
if (xval >= 3 && yval != 0 && rval <= yval + 1) {
new_lemma lemma(c, "x >= 3, y != 0 => x^y > ln(x)y + 1");
lemma |= ineq(x, llc::LT, rational(3));
lemma |= ineq(y, llc::EQ, rational::zero());

2
src/muz/spacer/spacer_cluster.cpp
View file

@ -378,7 +378,7 @@ void lemma_cluster_finder::cluster(lemma_ref &lemma) {
<< pattern << "\n"
<< " and lemma cube: " << lcube << "\n";);
for (const lemma_ref &l : neighbours) {
for (auto l : neighbours) {
SASSERT(cluster->can_contain(l));
bool added = cluster->add_lemma(l, false);
(void)added;

7
src/qe/qe.cpp
View file

@ -1513,10 +1513,11 @@ namespace qe {
propagate_assignment(*model_eval);
VERIFY(CHOOSE_VAR == update_current(*model_eval, true));
SASSERT(m_current->fml());
if (l_true != m_solver.check()) {
return l_true;
}
if (l_true != m_solver.check())
return l_true;
m_solver.get_model(model);
if (!model)
return l_undef;
model_eval = alloc(model_evaluator, *model);
search_tree* st = m_current;
update_current(*model_eval, false);

2
src/sat/sat_config.cpp
View file

@ -65,6 +65,8 @@ namespace sat {
m_phase = PS_RANDOM;
else if (s == symbol("frozen"))
m_phase = PS_FROZEN;
else if (s == symbol("local_search"))
m_phase = PS_LOCAL_SEARCH;
else
throw sat_param_exception("invalid phase selection strategy: always_false, always_true, basic_caching, caching, random");

1
src/sat/sat_config.h
View file

@ -28,6 +28,7 @@ namespace sat {
PS_ALWAYS_FALSE,
PS_BASIC_CACHING,
PS_SAT_CACHING,
PS_LOCAL_SEARCH,
PS_FROZEN,
PS_RANDOM
};

118
src/sat/sat_ddfw.cpp
View file

@ -49,6 +49,7 @@ namespace sat {
else if (should_parallel_sync()) do_parallel_sync();
else shift_weights();
}
log();
return m_min_sz == 0 ? l_true : l_undef;
}
@ -66,9 +67,9 @@ namespace sat {
<< std::setw(10) << kflips_per_sec
<< std::setw(10) << m_flips
<< std::setw(10) << m_restart_count
<< std::setw(10) << m_reinit_count
<< std::setw(10) << m_unsat_vars.size()
<< std::setw(10) << m_shifts;
<< std::setw(11) << m_reinit_count
<< std::setw(13) << m_unsat_vars.size()
<< std::setw(9) << m_shifts;
if (m_par) verbose_stream() << std::setw(10) << m_parsync_count;
verbose_stream() << ")\n");
m_stopwatch.start();
@ -90,18 +91,18 @@ namespace sat {
unsigned n = 1;
bool_var v0 = null_bool_var;
for (bool_var v : m_unsat_vars) {
int r = reward(v);
if (r > 0) {
double r = reward(v);
if (r > 0.0) {
sum_pos += score(r);
}
else if (r == 0 && sum_pos == 0 && (m_rand() % (n++)) == 0) {
else if (r == 0.0 && sum_pos == 0 && (m_rand() % (n++)) == 0) {
v0 = v;
}
}
if (sum_pos > 0) {
double lim_pos = ((double) m_rand() / (1.0 + m_rand.max_value())) * sum_pos;
for (bool_var v : m_unsat_vars) {
int r = reward(v);
double r = reward(v);
if (r > 0) {
lim_pos -= score(r);
if (lim_pos <= 0) {
@ -121,7 +122,7 @@ namespace sat {
* TBD: map reward value to a score, possibly through an exponential function, such as
* exp(-tau/r), where tau > 0
*/
double ddfw::mk_score(unsigned r) {
double ddfw::mk_score(double r) {
return r;
}
@ -201,7 +202,7 @@ namespace sat {
m_shifts = 0;
m_stopwatch.start();
}
void ddfw::reinit(solver& s) {
add(s);
add_assumptions();
@ -235,7 +236,7 @@ namespace sat {
for (unsigned cls_idx : use_list(*this, lit)) {
clause_info& ci = m_clauses[cls_idx];
ci.del(lit);
unsigned w = ci.m_weight;
double w = ci.m_weight;
// cls becomes false: flip any variable in clause to receive reward w
switch (ci.m_num_trues) {
case 0: {
@ -257,7 +258,7 @@ namespace sat {
}
for (unsigned cls_idx : use_list(*this, nlit)) {
clause_info& ci = m_clauses[cls_idx];
unsigned w = ci.m_weight;
double w = ci.m_weight;
// the clause used to have a single true (pivot) literal, now it has two.
// Then the previous pivot is no longer penalized for flipping.
switch (ci.m_num_trues) {
@ -406,9 +407,8 @@ namespace sat {
void ddfw::save_best_values() {
if (m_unsat.empty()) {
m_model.reserve(num_vars());
for (unsigned i = 0; i < num_vars(); ++i) {
for (unsigned i = 0; i < num_vars(); ++i)
m_model[i] = to_lbool(value(i));
}
}
if (m_unsat.size() < m_min_sz) {
m_models.reset();
@ -422,13 +422,11 @@ namespace sat {
}
unsigned h = value_hash();
if (!m_models.contains(h)) {
for (unsigned v = 0; v < num_vars(); ++v) {
for (unsigned v = 0; v < num_vars(); ++v)
bias(v) += value(v) ? 1 : -1;
}
m_models.insert(h);
if (m_models.size() > m_config.m_max_num_models) {
if (m_models.size() > m_config.m_max_num_models)
m_models.erase(*m_models.begin());
}
}
m_min_sz = m_unsat.size();
}
@ -450,10 +448,9 @@ namespace sat {
3. select multiple clauses instead of just one per clause in unsat.
*/
bool ddfw::select_clause(unsigned max_weight, unsigned max_trues, clause_info const& cn, unsigned& n) {
if (cn.m_num_trues == 0 || cn.m_weight < max_weight) {
bool ddfw::select_clause(double max_weight, clause_info const& cn, unsigned& n) {
if (cn.m_num_trues == 0 || cn.m_weight + 1e-5 < max_weight)
return false;
}
if (cn.m_weight > max_weight) {
n = 2;
return true;
@ -462,51 +459,72 @@ namespace sat {
}
unsigned ddfw::select_max_same_sign(unsigned cf_idx) {
clause const& c = get_clause(cf_idx);
unsigned max_weight = 2;
unsigned max_trues = 0;
auto& ci = m_clauses[cf_idx];
unsigned cl = UINT_MAX; // clause pointer to same sign, max weight satisfied clause.
clause const& c = *ci.m_clause;
double max_weight = m_init_weight;
unsigned n = 1;
for (literal lit : c) {
for (unsigned cn_idx : use_list(*this, lit)) {
auto& cn = m_clauses[cn_idx];
if (select_clause(max_weight, max_trues, cn, n)) {
if (select_clause(max_weight, cn, n)) {
cl = cn_idx;
max_weight = cn.m_weight;
max_trues = cn.m_num_trues;
}
}
}
return cl;
}
void ddfw::transfer_weight(unsigned from, unsigned to, double w) {
auto& cf = m_clauses[to];
auto& cn = m_clauses[from];
if (cn.m_weight < w)
return;
cf.m_weight += w;
cn.m_weight -= w;
for (literal lit : get_clause(to))
inc_reward(lit, w);
if (cn.m_num_trues == 1)
inc_reward(to_literal(cn.m_trues), w);
}
unsigned ddfw::select_random_true_clause() {
unsigned num_clauses = m_clauses.size();
unsigned rounds = 100 * num_clauses;
for (unsigned i = 0; i < rounds; ++i) {
unsigned idx = (m_rand() * m_rand()) % num_clauses;
auto & cn = m_clauses[idx];
if (cn.is_true() && cn.m_weight >= m_init_weight)
return idx;
}
return UINT_MAX;
}
// 1% chance to disregard neighbor
inline bool ddfw::disregard_neighbor() {
return false; // rand() % 1000 == 0;
}
double ddfw::calculate_transfer_weight(double w) {
return (w > m_init_weight) ? m_init_weight : 1;
}
void ddfw::shift_weights() {
++m_shifts;
for (unsigned cf_idx : m_unsat) {
auto& cf = m_clauses[cf_idx];
for (unsigned to_idx : m_unsat) {
auto& cf = m_clauses[to_idx];
SASSERT(!cf.is_true());
unsigned cn_idx = select_max_same_sign(cf_idx);
while (cn_idx == UINT_MAX) {
unsigned idx = (m_rand() * m_rand()) % m_clauses.size();
auto & cn = m_clauses[idx];
if (cn.is_true() && cn.m_weight >= 2) {
cn_idx = idx;
}
}
auto & cn = m_clauses[cn_idx];
unsigned from_idx = select_max_same_sign(to_idx);
if (from_idx == UINT_MAX || disregard_neighbor())
from_idx = select_random_true_clause();
if (from_idx == UINT_MAX)
continue;
auto & cn = m_clauses[from_idx];
SASSERT(cn.is_true());
unsigned wn = cn.m_weight;
SASSERT(wn >= 2);
unsigned inc = (wn > 2) ? 2 : 1;
SASSERT(wn - inc >= 1);
cf.m_weight += inc;
cn.m_weight -= inc;
for (literal lit : get_clause(cf_idx)) {
inc_reward(lit, inc);
}
if (cn.m_num_trues == 1) {
inc_reward(to_literal(cn.m_trues), inc);
}
double w = calculate_transfer_weight(cn.m_weight);
transfer_weight(from_idx, to_idx, w);
}
// DEBUG_CODE(invariant(););
}
@ -543,7 +561,7 @@ namespace sat {
VERIFY(found);
}
for (unsigned v = 0; v < num_vars(); ++v) {
int v_reward = 0;
double v_reward = 0;
literal lit(v, !value(v));
for (unsigned j : m_use_list[lit.index()]) {
clause_info const& ci = m_clauses[j];
@ -559,7 +577,7 @@ namespace sat {
}
}
IF_VERBOSE(0, if (v_reward != reward(v)) verbose_stream() << v << " " << v_reward << " " << reward(v) << "\n");
SASSERT(reward(v) == v_reward);
// SASSERT(reward(v) == v_reward);
}
DEBUG_CODE(
for (auto const& ci : m_clauses) {

62
src/sat/sat_ddfw.h
View file

@ -34,10 +34,10 @@ namespace sat {
class ddfw : public i_local_search {
struct clause_info {
clause_info(clause* cl, unsigned init_weight): m_weight(init_weight), m_trues(0), m_num_trues(0), m_clause(cl) {}
unsigned m_weight; // weight of clause
unsigned m_trues; // set of literals that are true
unsigned m_num_trues; // size of true set
clause_info(clause* cl, double init_weight): m_weight(init_weight), m_clause(cl) {}
double m_weight; // weight of clause
unsigned m_trues = 0; // set of literals that are true
unsigned m_num_trues = 0; // size of true set
clause* m_clause;
bool is_true() const { return m_num_trues > 0; }
void add(literal lit) { ++m_num_trues; m_trues += lit.index(); }
@ -65,23 +65,24 @@ namespace sat {
};
struct var_info {
var_info(): m_value(false), m_reward(0), m_make_count(0), m_bias(0), m_reward_avg(1e-5) {}
bool m_value;
int m_reward;
unsigned m_make_count;
int m_bias;
ema m_reward_avg;
var_info() {}
bool m_value = false;
double m_reward = 0;
unsigned m_make_count = 0;
int m_bias = 0;
ema m_reward_avg = 1e-5;
};
config m_config;
reslimit m_limit;
clause_allocator m_alloc;
config m_config;
reslimit m_limit;
clause_allocator m_alloc;
svector<clause_info> m_clauses;
literal_vector m_assumptions;
svector<var_info> m_vars; // var -> info
svector<double> m_probs; // var -> probability of flipping
svector<double> m_scores; // reward -> score
model m_model; // var -> best assignment
unsigned m_init_weight = 2;
vector<unsigned_vector> m_use_list;
unsigned_vector m_flat_use_list;
@ -90,11 +91,11 @@ namespace sat {
indexed_uint_set m_unsat;
indexed_uint_set m_unsat_vars; // set of variables that are in unsat clauses
random_gen m_rand;
unsigned m_num_non_binary_clauses{ 0 };
unsigned m_restart_count{ 0 }, m_reinit_count{ 0 }, m_parsync_count{ 0 };
uint64_t m_restart_next{ 0 }, m_reinit_next{ 0 }, m_parsync_next{ 0 };
uint64_t m_flips{ 0 }, m_last_flips{ 0 }, m_shifts{ 0 };
unsigned m_min_sz{ 0 };
unsigned m_num_non_binary_clauses = 0;
unsigned m_restart_count = 0, m_reinit_count = 0, m_parsync_count = 0;
uint64_t m_restart_next = 0, m_reinit_next = 0, m_parsync_next = 0;
uint64_t m_flips = 0, m_last_flips = 0, m_shifts = 0;
unsigned m_min_sz = 0;
hashtable<unsigned, unsigned_hash, default_eq<unsigned>> m_models;
stopwatch m_stopwatch;
@ -112,9 +113,9 @@ namespace sat {
void flatten_use_list();
double mk_score(unsigned r);
double mk_score(double r);
inline double score(unsigned r) { return r; } // TBD: { for (unsigned sz = m_scores.size(); sz <= r; ++sz) m_scores.push_back(mk_score(sz)); return m_scores[r]; }
inline double score(double r) { return r; } // TBD: { for (unsigned sz = m_scores.size(); sz <= r; ++sz) m_scores.push_back(mk_score(sz)); return m_scores[r]; }
inline unsigned num_vars() const { return m_vars.size(); }
@ -124,9 +125,9 @@ namespace sat {
inline bool value(bool_var v) const { return m_vars[v].m_value; }
inline int& reward(bool_var v) { return m_vars[v].m_reward; }
inline double& reward(bool_var v) { return m_vars[v].m_reward; }
inline int reward(bool_var v) const { return m_vars[v].m_reward; }
inline double reward(bool_var v) const { return m_vars[v].m_reward; }
inline int& bias(bool_var v) { return m_vars[v].m_bias; }
@ -136,7 +137,7 @@ namespace sat {
inline clause const& get_clause(unsigned idx) const { return *m_clauses[idx].m_clause; }
inline unsigned get_weight(unsigned idx) const { return m_clauses[idx].m_weight; }
inline double get_weight(unsigned idx) const { return m_clauses[idx].m_weight; }
inline bool is_true(unsigned idx) const { return m_clauses[idx].is_true(); }
@ -154,9 +155,9 @@ namespace sat {
if (--make_count(v) == 0) m_unsat_vars.remove(v);
}
inline void inc_reward(literal lit, int inc) { reward(lit.var()) += inc; }
inline void inc_reward(literal lit, double w) { reward(lit.var()) += w; }
inline void dec_reward(literal lit, int inc) { reward(lit.var()) -= inc; }
inline void dec_reward(literal lit, double w) { reward(lit.var()) -= w; }
// flip activity
bool do_flip();
@ -166,17 +167,20 @@ namespace sat {
// shift activity
void shift_weights();
inline double calculate_transfer_weight(double w);
// reinitialize weights activity
bool should_reinit_weights();
void do_reinit_weights();
inline bool select_clause(unsigned max_weight, unsigned max_trues, clause_info const& cn, unsigned& n);
inline bool select_clause(double max_weight, clause_info const& cn, unsigned& n);
// restart activity
bool should_restart();
void do_restart();
void reinit_values();
unsigned select_random_true_clause();
// parallel integration
bool should_parallel_sync();
void do_parallel_sync();
@ -193,6 +197,10 @@ namespace sat {
void add_assumptions();
inline void transfer_weight(unsigned from, unsigned to, double w);
inline bool disregard_neighbor();
public:
ddfw(): m_par(nullptr) {}
@ -210,6 +218,8 @@ namespace sat {
void set_seed(unsigned n) override { m_rand.set_seed(n); }
void add(solver const& s) override;
bool get_value(bool_var v) const override { return value(v); }
std::ostream& display(std::ostream& out) const;

79
src/sat/sat_solver.cpp
View file

@ -1331,17 +1331,37 @@ namespace sat {
ERROR_EX
};
struct solver::scoped_ls {
solver& s;
scoped_ls(solver& s): s(s) {}
~scoped_ls() {
dealloc(s.m_local_search);
s.m_local_search = nullptr;
}
};
void solver::bounded_local_search() {
literal_vector _lits;
scoped_limits scoped_rl(rlimit());
m_local_search = alloc(ddfw);
scoped_ls _ls(*this);
SASSERT(m_local_search);
m_local_search->add(*this);
m_local_search->updt_params(m_params);
m_local_search->set_seed(m_rand());
scoped_rl.push_child(&(m_local_search->rlimit()));
m_local_search->rlimit().push(500000);
m_local_search->reinit(*this);
m_local_search->check(_lits.size(), _lits.data(), nullptr);
for (unsigned i = 0; i < m_phase.size(); ++i)
m_best_phase[i] = m_local_search->get_value(i);
}
lbool solver::invoke_local_search(unsigned num_lits, literal const* lits) {
literal_vector _lits(num_lits, lits);
for (literal lit : m_user_scope_literals) _lits.push_back(~lit);
struct scoped_ls {
solver& s;
scoped_ls(solver& s): s(s) {}
~scoped_ls() {
dealloc(s.m_local_search);
s.m_local_search = nullptr;
}
};
for (literal lit : m_user_scope_literals)
_lits.push_back(~lit);
scoped_ls _ls(*this);
if (inconsistent())
return l_false;
@ -1611,27 +1631,28 @@ namespace sat {
bool solver::guess(bool_var next) {
lbool lphase = m_ext ? m_ext->get_phase(next) : l_undef;
if (lphase != l_undef)
return lphase == l_true;
switch (m_config.m_phase) {
case PS_ALWAYS_TRUE:
return true;
case PS_ALWAYS_FALSE:
return false;
case PS_BASIC_CACHING:
case PS_ALWAYS_TRUE:
return true;
case PS_ALWAYS_FALSE:
return false;
case PS_BASIC_CACHING:
return m_phase[next];
case PS_FROZEN:
return m_best_phase[next];
case PS_SAT_CACHING:
case PS_LOCAL_SEARCH:
if (m_search_state == s_unsat)
return m_phase[next];
case PS_FROZEN:
return m_best_phase[next];
case PS_SAT_CACHING:
if (m_search_state == s_unsat)
return m_phase[next];
return m_best_phase[next];
case PS_RANDOM:
return (m_rand() % 2) == 0;
default:
UNREACHABLE();
return false;
return m_best_phase[next];
case PS_RANDOM:
return (m_rand() % 2) == 0;
default:
UNREACHABLE();
return false;
}
}
@ -2823,7 +2844,7 @@ namespace sat {
}
bool solver::is_two_phase() const {
return m_config.m_phase == PS_SAT_CACHING;
return m_config.m_phase == PS_SAT_CACHING || m_config.m_phase == PS_LOCAL_SEARCH;
}
bool solver::is_sat_phase() const {
@ -2923,6 +2944,10 @@ namespace sat {
case PS_RANDOM:
for (auto& p : m_phase) p = (m_rand() % 2) == 0;
break;
case PS_LOCAL_SEARCH:
if (m_search_state == s_sat)
bounded_local_search();
break;
default:
UNREACHABLE();
break;

2
src/sat/sat_solver.h
View file

@ -589,7 +589,9 @@ namespace sat {
lbool do_ddfw_search(unsigned num_lits, literal const* lits);
lbool do_prob_search(unsigned num_lits, literal const* lits);
lbool invoke_local_search(unsigned num_lits, literal const* lits);
void bounded_local_search();
lbool do_unit_walk();
struct scoped_ls;
// -----------------------
//

2
src/sat/sat_types.h
View file

@ -91,7 +91,7 @@ namespace sat {
virtual model const& get_model() const = 0;
virtual void collect_statistics(statistics& st) const = 0;
virtual double get_priority(bool_var v) const { return 0; }
virtual bool get_value(bool_var v) const { return true; }
};
class proof_hint {

2
src/shell/lp_frontend.cpp
View file

@ -80,7 +80,7 @@ void run_solver(smt_params_helper & params, char const * mps_file_name) {
solver->settings().set_message_ostream(&std::cout);
solver->settings().report_frequency = params.arith_rep_freq();
solver->settings().print_statistics = params.arith_print_stats();
solver->settings().simplex_strategy() = lp:: simplex_strategy_enum::lu;
solver->settings().set_simplex_strategy(lp:: simplex_strategy_enum::lu);
solver->find_maximal_solution();

1
src/smt/theory_fpa.cpp
View file

@ -671,7 +671,6 @@ namespace smt {
out << "equivalence classes:\n";
for (enode * n : ctx.enodes()) {
expr * e = n->get_expr();
expr * r = n->get_root()->get_expr();
out << r->get_id() << " --> " << enode_pp(n, ctx) << "\n";
}

81
src/solver/simplifier_solver.cpp
View file

@ -95,18 +95,30 @@ class simplifier_solver : public solver {
expr_ref_vector m_assumptions;
model_converter_ref m_mc;
bool m_inconsistent = false;
expr_safe_replace m_core_replace;
void replace(expr_ref_vector& r) {
expr_ref tmp(m);
for (unsigned i = 0; i < r.size(); ++i) {
m_core_replace(r.get(i), tmp);
r[i] = tmp;
}
}
void flush(expr_ref_vector& assumptions) {
unsigned qhead = m_preprocess_state.qhead();
if (qhead < m_fmls.size()) {
for (expr* a : assumptions)
m_preprocess_state.freeze(a);
expr_ref_vector orig_assumptions(assumptions);
m_core_replace.reset();
if (qhead < m_fmls.size() || !assumptions.empty()) {
TRACE("solver", tout << "qhead " << qhead << "\n");
m_preprocess_state.replay(qhead, assumptions);
m_preprocess_state.replay(qhead, assumptions);
m_preprocess_state.freeze(assumptions);
m_preprocess.reduce();
if (!m.inc())
return;
m_preprocess_state.advance_qhead();
for (unsigned i = 0; i < assumptions.size(); ++i)
m_core_replace.insert(assumptions.get(i), orig_assumptions.get(i));
}
m_mc = m_preprocess_state.model_trail().get_model_converter();
m_cached_mc = nullptr;
@ -148,6 +160,7 @@ public:
m_preprocess_state(*this),
m_preprocess(m, s->get_params(), m_preprocess_state),
m_assumptions(m),
m_core_replace(m),
m_proof(m)
{
if (fac)
@ -189,7 +202,7 @@ public:
lbool check_sat_core(unsigned num_assumptions, expr* const* assumptions) override {
expr_ref_vector _assumptions(m, num_assumptions, assumptions);
flush(_assumptions);
return s->check_sat_core(num_assumptions, assumptions);
return s->check_sat_core(num_assumptions, _assumptions.data());
}
void collect_statistics(statistics& st) const override {
@ -211,7 +224,7 @@ public:
}
proof_ref m_proof;
proof* get_proof_core() {
proof* get_proof_core() override {
proof* p = s->get_proof();
m_proof = p;
if (p) {
@ -258,7 +271,7 @@ public:
std::string reason_unknown() const override { return s->reason_unknown(); }
void set_reason_unknown(char const* msg) override { s->set_reason_unknown(msg); }
void get_labels(svector<symbol>& r) override { s->get_labels(r); }
void get_unsat_core(expr_ref_vector& r) { s->get_unsat_core(r); }
void get_unsat_core(expr_ref_vector& r) override { s->get_unsat_core(r); replace(r); }
ast_manager& get_manager() const override { return s->get_manager(); }
void reset_params(params_ref const& p) override { s->reset_params(p); }
params_ref const& get_params() const override { return s->get_params(); }
@ -273,15 +286,59 @@ public:
unsigned get_num_assumptions() const override { return s->get_num_assumptions(); }
expr* get_assumption(unsigned idx) const override { return s->get_assumption(idx); }
unsigned get_scope_level() const override { return s->get_scope_level(); }
lbool check_sat_cc(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses) override { return check_sat_cc(cube, clauses); }
void set_progress_callback(progress_callback* callback) override { s->set_progress_callback(callback); }
lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) override {
return s->get_consequences(asms, vars, consequences);
expr_ref_vector es(m);
es.append(asms);
es.append(vars);
flush(es);
expr_ref_vector asms1(m, asms.size(), es.data());
expr_ref_vector vars1(m, vars.size(), es.data() + asms.size());
lbool r = s->get_consequences(asms1, vars1, consequences);
replace(consequences);
return r;
}
lbool check_sat_cc(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses) override {
expr_ref_vector es(m);
es.append(cube);
for (auto const& c : clauses)
es.append(c);
flush(es);
expr_ref_vector cube1(m, cube.size(), es.data());
vector<expr_ref_vector> clauses1;
unsigned offset = cube.size();
for (auto const& c : clauses) {
clauses1.push_back(expr_ref_vector(m, c.size(), es.data() + offset));
offset += c.size();
}
return s->check_sat_cc(cube1, clauses1);
}
lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) override {
expr_ref_vector vars1(vars);
flush(vars1);
lbool r = s->find_mutexes(vars1, mutexes);
for (auto& mux : mutexes)
replace(mux);
return r;
}
lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) override {
expr_ref_vector asms1(asms);
flush(asms1);
lbool r = s->preferred_sat(asms1, cores);
for (auto& c : cores)
replace(c);
return r;
}
lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) override { return s->find_mutexes(vars, mutexes); }
lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) override { return s->preferred_sat(asms, cores); }
expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override { return s->cube(vars, backtrack_level); }
// todo flush?
expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override {
return s->cube(vars, backtrack_level);
}
expr* congruence_root(expr* e) override { return s->congruence_root(e); }
expr* congruence_next(expr* e) override { return s->congruence_next(e); }
std::ostream& display(std::ostream& out, unsigned n, expr* const* assumptions) const override {

2
src/test/lp/lp.cpp
View file

@ -1391,7 +1391,7 @@ void update_settings(argument_parser & args_parser, lp_settings& settings) {
settings.set_random_seed(n);
}
if (get_int_from_args_parser("--simplex_strategy", args_parser, n)) {
settings.simplex_strategy() = static_cast<simplex_strategy_enum>(n);
settings.set_simplex_strategy(static_cast<simplex_strategy_enum>(n));
}
}

12
src/util/tbv.h
View file

@ -30,7 +30,7 @@ enum tbit {
BIT_z = 0x0, // unknown
BIT_0 = 0x1, // for sure 0
BIT_1 = 0x2, // for sure 1
BIT_x = 0x3 // don't care
BIT_x = 0x3 // don't care
};
inline tbit neg(tbit t) {
@ -43,7 +43,7 @@ class tbv_manager {
ptr_vector<tbv> allocated_tbvs;
public:
tbv_manager(unsigned n): m(2*n) {}
tbv_manager(const tbv_manager& m) = delete;
tbv_manager(tbv_manager const& m) = delete;
~tbv_manager();
void reset();
tbv* allocate();
@ -154,11 +154,9 @@ public:
};
inline std::ostream& operator<<(std::ostream& out, tbv_ref const& c) {
const char* names[] = { "z", "0", "1", "x" };
for (unsigned i = c.num_tbits(); i > 0; i--) {
out << names[(unsigned)c[i - 1]];
char const* names[] = { "z", "0", "1", "x" };
for (unsigned i = c.num_tbits(); i-- > 0; ) {
out << names[static_cast<unsigned>(c[i])];
}
return out;
}

16
src/util/util.h
View file

@ -413,22 +413,6 @@ inline size_t megabytes_to_bytes(unsigned mb) {
return r;
}
/** Compact version of std::all_of */
template <typename Container, typename Predicate>
bool all_of(Container const& c, Predicate p)
{
using std::begin, std::end; // allows begin(c) to also find c.begin()
return std::all_of(begin(c), end(c), std::forward<Predicate>(p));
}
/** Compact version of std::any_of */
template <typename Container, typename Predicate>
bool any_of(Container const& c, Predicate p)
{
using std::begin, std::end; // allows begin(c) to also find c.begin()
return std::any_of(begin(c), end(c), std::forward<Predicate>(p));
}
/** Compact version of std::count */
template <typename Container, typename Item>
std::size_t count(Container const& c, Item x)