mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
na
This commit is contained in:
parent
e7ded9cdbd
commit
3293aeb7c7
|
@ -419,6 +419,7 @@ namespace arith {
|
|||
void false_case_of_check_nla(const nla::lemma& l);
|
||||
void dbg_finalize_model(model& mdl);
|
||||
|
||||
|
||||
public:
|
||||
solver(euf::solver& ctx, theory_id id);
|
||||
~solver() override;
|
||||
|
@ -426,6 +427,8 @@ namespace arith {
|
|||
void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) override;
|
||||
void asserted(literal l) override;
|
||||
sat::check_result check() override;
|
||||
void simplify() override;
|
||||
void init_search() override;
|
||||
|
||||
std::ostream& display(std::ostream& out) const override;
|
||||
std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
|
||||
|
|
|
@ -173,6 +173,10 @@ public:
|
|||
return *this;
|
||||
}
|
||||
|
||||
rational& operator-=(int r) {
|
||||
(*this) -= rational(r);
|
||||
return *this;
|
||||
}
|
||||
|
||||
rational & operator*=(rational const & r) {
|
||||
m().mul(m_val, r.m_val, m_val);
|
||||
|
|
Loading…
Reference in a new issue