mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

remove experimental code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-09-20 15:04:24 -07:00
parent 24512d5ec2
commit 7a74b099ba
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_arith_nl.h
View file

@ -511,7 +511,6 @@ bool theory_arith<Ext>::propagate_nl_downward(expr * n, var_power_pair const& p)
*/
template<typename Ext>
bool theory_arith<Ext>::propagate_nl_bounds(expr * m) {
return false;
TRACE("non_linear", tout << "propagate several bounds using:\n"; display_monomial(tout, m); tout << "\n";);
bool result = propagate_nl_upward(m);
buffer<var_power_pair> vp;
@ -531,7 +530,6 @@ bool theory_arith<Ext>::propagate_nl_bounds(expr * m) {
*/
template<typename Ext>
bool theory_arith<Ext>::propagate_nl_bounds() {
return false;
m_dep_manager.reset();
bool propagated = false;
for (unsigned i = 0; i < m_nl_monomials.size(); i++) {
@ -1634,7 +1632,6 @@ bool theory_arith<Ext>::is_cross_nested_consistent(row const & r) {
*/
template<typename Ext>
bool theory_arith<Ext>::is_cross_nested_consistent(svector<theory_var> const & nl_cluster) {
return true;
for (theory_var v : nl_cluster) {
if (!is_base(v))
continue;