mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

helper functions to add constraints to univariate_solver

Browse source
This commit is contained in:
Jakob Rath 2022-03-17 14:06:18 +01:00
parent edeba9b56a
commit 9d47d7959d
10 changed files with 52 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/dd/dd_pdd.h
View file

@ -418,6 +418,7 @@ namespace dd {
bool is_monomial() const { return m.is_monomial(root); }
bool is_univariate() const { return m.is_univariate(root); }
void get_univariate_coefficients(vector<rational>& coeff) const { m.get_univariate_coefficients(root, coeff); }
vector<rational> get_univariate_coefficients() const { vector<rational> coeff; m.get_univariate_coefficients(root, coeff); return coeff; }
bool is_never_zero() const { return m.is_never_zero(root); }
bool var_is_leaf(unsigned v) const { return m.var_is_leaf(root, v); }

10
src/math/polysat/constraint.h
View file

@ -17,6 +17,7 @@ Author:
#include "math/polysat/types.h"
#include "math/polysat/interval.h"
#include "math/polysat/search_state.h"
#include "math/polysat/univariate/univariate_solver.h"
namespace polysat {
@ -213,9 +214,12 @@ namespace polysat {
void unset_mark() { m_is_marked = false; }
bool is_marked() const { return m_is_marked; }
bool is_active() const { return m_is_active; }
void set_active(bool f) { m_is_active = f; }
/// Assuming the constraint is univariate under the current assignment of 's',
/// adds the constraint to the univariate solver 'us'.
virtual void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const = 0;
};
inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
@ -256,10 +260,11 @@ namespace polysat {
void narrow(solver& s, bool first) { get()->narrow(s, is_positive(), first); }
inequality as_inequality() const { return get()->as_inequality(is_positive()); }
void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep) const { get()->add_to_univariate_solver(s, us, dep, is_positive()); }
sat::bool_var bvar() const { return m_constraint->bvar(); }
sat::literal blit() const { return sat::literal(bvar(), is_negative()); }
constraint* get() const { return m_constraint; }
explicit operator bool() const { return !!m_constraint; }
bool operator!() const { return !m_constraint; }
@ -270,7 +275,6 @@ namespace polysat {
bool is_eq() const;
pdd const& eq() const;
signed_constraint& operator=(std::nullptr_t) { m_constraint = nullptr; return *this; }
unsigned hash() const {

6
src/math/polysat/mul_ovfl_constraint.cpp
View file

@ -166,4 +166,10 @@ namespace polysat {
bool mul_ovfl_constraint::operator==(constraint const& other) const {
return other.is_mul_ovfl() && p() == other.to_mul_ovfl().p() && q() == other.to_mul_ovfl().q();
}
void mul_ovfl_constraint::add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const {
auto p_coeff = s.subst(p()).get_univariate_coefficients();
auto q_coeff = s.subst(q()).get_univariate_coefficients();
us.add_umul_ovfl(p_coeff, q_coeff, !is_positive, dep);
}
}

2
src/math/polysat/mul_ovfl_constraint.h
View file

@ -48,6 +48,8 @@ namespace polysat {
unsigned hash() const override;
bool operator==(constraint const& other) const override;
bool is_eq() const override { return false; }
void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
};
}

17
src/math/polysat/op_constraint.cpp
View file

@ -298,4 +298,21 @@ namespace polysat {
return l_undef;
}
void op_constraint::add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const {
auto p_coeff = s.subst(p()).get_univariate_coefficients();
auto q_coeff = s.subst(q()).get_univariate_coefficients();
auto r_coeff = s.subst(r()).get_univariate_coefficients();
switch (m_op) {
case code::lshr_op:
us.add_lshr(p_coeff, q_coeff, r_coeff, !is_positive, dep);
break;
case code::and_op:
us.add_and(p_coeff, q_coeff, r_coeff, !is_positive, dep);
break;
default:
NOT_IMPLEMENTED_YET();
break;
}
}
}

2
src/math/polysat/op_constraint.h
View file

@ -65,6 +65,8 @@ namespace polysat {
unsigned hash() const override;
bool operator==(constraint const& other) const override;
bool is_eq() const override { return false; }
void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
};
}

9
src/math/polysat/smul_fl_constraint.cpp
View file

@ -118,4 +118,13 @@ namespace polysat {
&& p() == other.to_smul_fl().p()
&& q() == other.to_smul_fl().q();
}
void smul_fl_constraint::add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const {
auto p_coeff = s.subst(p()).get_univariate_coefficients();
auto q_coeff = s.subst(q()).get_univariate_coefficients();
if (is_overflow())
us.add_smul_ovfl(p_coeff, q_coeff, !is_positive, dep);
else
us.add_smul_udfl(p_coeff, q_coeff, !is_positive, dep);
}
}

2
src/math/polysat/smul_fl_constraint.h
View file

@ -45,6 +45,8 @@ namespace polysat {
unsigned hash() const override;
bool operator==(constraint const& other) const override;
bool is_eq() const override { return false; }
void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
};
}

5
src/math/polysat/ule_constraint.cpp
View file

@ -207,4 +207,9 @@ namespace polysat {
return other.is_ule() && lhs() == other.to_ule().lhs() && rhs() == other.to_ule().rhs();
}
void ule_constraint::add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const {
auto p_coeff = s.subst(lhs()).get_univariate_coefficients();
auto q_coeff = s.subst(rhs()).get_univariate_coefficients();
us.add_ule(p_coeff, q_coeff, !is_positive, dep);
}
}

2
src/math/polysat/ule_constraint.h
View file

@ -46,7 +46,7 @@ namespace polysat {
bool operator==(constraint const& other) const override;
bool is_eq() const override { return m_rhs.is_zero(); }
bool is_diseq() const override { return m_lhs.is_one(); }
// pdd const& p() const { SASSERT(is_eq()); return m_lhs; }
void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
};
}