mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
try another build fix
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
7b6f51941c
commit
24f56fd74c
|
@ -7457,8 +7457,7 @@ def WithParams(t, p):
|
|||
>>> t((x + 1)*(y + 2) == 0)
|
||||
[[2*x + y + x*y == -2]]
|
||||
"""
|
||||
ctx = keys.pop('ctx', None)
|
||||
t = _to_tactic(t, ctx)
|
||||
t = _to_tactic(t, None)
|
||||
return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx)
|
||||
|
||||
def Repeat(t, max=4294967295, ctx=None):
|
||||
|
|
|
@ -83,12 +83,12 @@ public:
|
|||
void apply_from_right(vector<T> & w) override;
|
||||
void apply_from_right(indexed_vector<T> & w) override;
|
||||
|
||||
T get_elem(unsigned i, unsigned j) const;
|
||||
T get_elem(unsigned i, unsigned j) const override;
|
||||
#ifdef Z3DEBUG
|
||||
unsigned row_count() const { return m_length; }
|
||||
unsigned column_count() const { return m_length; }
|
||||
void set_number_of_rows(unsigned m) { m_length = m; }
|
||||
void set_number_of_columns(unsigned n) { m_length = n; }
|
||||
unsigned row_count() const override { return m_length; }
|
||||
unsigned column_count() const override { return m_length; }
|
||||
void set_number_of_rows(unsigned m) override { m_length = m; }
|
||||
void set_number_of_columns(unsigned n) override { m_length = n; }
|
||||
#endif
|
||||
void divide_by_diagonal_element() {
|
||||
m_column_vector.divide(m_diagonal_element);
|
||||
|
|
Loading…
Reference in a new issue