mirror of
https://github.com/Z3Prover/z3
synced 2025-08-15 23:35:26 +00:00
try the lemma scheme
This commit is contained in:
parent
e31cecf5db
commit
f423642e9b
5 changed files with 72 additions and 123 deletions
|
@ -49,6 +49,6 @@ namespace nla {
|
|||
nlsat::anum const& am_value(lp::var_index v) const;
|
||||
void collect_statistics(::statistics & st);
|
||||
void calculate_implied_bounds_for_monic(lp::lpvar v);
|
||||
void init_bound_propagation();
|
||||
void init_bound_propagation(vector<lemma>&);
|
||||
};
|
||||
}
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue