From 30de76b5290543e5ed229e4d748723954ffc404f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 May 2020 20:50:27 -0700 Subject: [PATCH] add occurs check to other nla_basic lemmas Signed-off-by: Nikolaj Bjorner --- src/math/lp/matrix.h | 11 ---- src/math/lp/nex.h | 15 +---- src/math/lp/nex_creator.cpp | 15 +---- src/math/lp/nex_creator.h | 16 +----- src/math/lp/nla_basics_lemmas.cpp | 87 ++++++++++++++--------------- src/math/lp/nla_basics_lemmas.h | 15 +---- src/math/lp/nla_common.cpp | 15 +---- src/math/lp/nla_common.h | 15 +---- src/math/lp/nla_core.cpp | 10 ++-- src/math/lp/nla_core.h | 6 +- src/math/lp/nla_defs.h | 11 +--- src/math/lp/nla_intervals.h | 15 +---- src/math/lp/nla_monotone_lemmas.cpp | 16 +----- src/math/lp/nla_monotone_lemmas.h | 16 +----- src/math/lp/nla_order_lemmas.cpp | 46 ++++++--------- src/math/lp/nla_order_lemmas.h | 15 +---- src/math/lp/nla_settings.h | 11 ---- src/math/lp/nla_solver.cpp | 16 +----- src/math/lp/nla_solver.h | 13 +---- src/math/lp/nla_tangent_lemmas.cpp | 15 +---- src/math/lp/nla_tangent_lemmas.h | 16 +----- 21 files changed, 94 insertions(+), 301 deletions(-) diff --git a/src/math/lp/matrix.h b/src/math/lp/matrix.h index df2b97bc7..80ddb1228 100644 --- a/src/math/lp/matrix.h +++ b/src/math/lp/matrix.h @@ -1,21 +1,10 @@ /*++ Copyright (c) 2017 Microsoft Corporation -Module Name: - - - -Abstract: - - - Author: Lev Nachmanson (levnach) -Revision History: - - --*/ #pragma once #include "math/lp/numeric_pair.h" diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h index 6b9bb6b2f..0d57c571c 100644 --- a/src/math/lp/nex.h +++ b/src/math/lp/nex.h @@ -1,21 +1,10 @@ /*++ Copyright (c) 2017 Microsoft Corporation - Module Name: - - - - Abstract: - - - Author: - Lev Nachmanson (levnach) + Lev Nachmanson (levnach) +--*/ - Revision History: - - - --*/ #pragma once #include #include "math/lp/nla_defs.h" diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp index f9b1aeaed..11b791ef8 100644 --- a/src/math/lp/nex_creator.cpp +++ b/src/math/lp/nex_creator.cpp @@ -1,21 +1,8 @@ /*++ Copyright (c) 2017 Microsoft Corporation - Module Name: - - - - Abstract: - - - Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) - - Revision History: - - + Lev Nachmanson (levnach) --*/ #include "util/lbool.h" #include "math/lp/nex_creator.h" diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h index 3a9477c94..9bce46395 100644 --- a/src/math/lp/nex_creator.h +++ b/src/math/lp/nex_creator.h @@ -1,21 +1,9 @@ /*++ Copyright (c) 2017 Microsoft Corporation - Module Name: - - - - Abstract: - - - Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) - - Revision History: - - + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) --*/ #pragma once #include diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp index 5859b50fe..8847ae766 100644 --- a/src/math/lp/nla_basics_lemmas.cpp +++ b/src/math/lp/nla_basics_lemmas.cpp @@ -1,22 +1,12 @@ /*++ Copyright (c) 2017 Microsoft Corporation - Module Name: - - - - Abstract: - - - Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) - Revision History: +--*/ - - --*/ #include "math/lp/nla_basics_lemmas.h" #include "math/lp/nla_core.h" #include "math/lp/factorization_factory_imp.h" @@ -42,7 +32,7 @@ void basics::generate_zero_lemmas(const monic& m) { lpvar zero_j = find_best_zero(m, fixed_zeros); SASSERT(is_set(zero_j)); unsigned zero_power = 0; - for (lpvar j : m.vars()){ + for (lpvar j : m.vars()) { if (j == zero_j) { zero_power++; continue; @@ -92,7 +82,7 @@ void basics::basic_sign_lemma_model_based_one_mon(const monic& m, int product_si generate_zero_lemmas(m); } else { new_lemma lemma(c(), __FUNCTION__); - for(lpvar j: m.vars()) { + for (lpvar j: m.vars()) { negate_strict_sign(j); } c().mk_ineq(m.var(), product_sign == 1? llc::GT : llc::LT); @@ -116,7 +106,7 @@ bool basics::basic_sign_lemma_model_based() { } -bool basics::basic_sign_lemma_on_mon(lpvar v, std::unordered_set & explored){ +bool basics::basic_sign_lemma_on_mon(lpvar v, std::unordered_set & explored) { if (!try_insert(v, explored)) { return false; } @@ -148,7 +138,7 @@ bool basics::basic_sign_lemma(bool derived) { return basic_sign_lemma_model_based(); std::unordered_set explored; - for (lpvar j : c().m_to_refine){ + for (lpvar j : c().m_to_refine) { if (basic_sign_lemma_on_mon(j, explored)) return true; } @@ -164,16 +154,14 @@ void basics::generate_sign_lemma(const monic& m, const monic& n, const rational& ); c().mk_ineq(m.var(), -sign, n.var(), llc::EQ); explain(m); - TRACE("nla_solver", tout << "m exp = "; _().print_explanation(_().current_expl(), tout);); explain(n); - TRACE("nla_solver", tout << "n exp = "; _().print_explanation(_().current_expl(), tout);); } // try to find a variable j such that val(j) = 0 // and the bounds on j contain 0 as an inner point lpvar basics::find_best_zero(const monic& m, unsigned_vector & fixed_zeros) const { lpvar zero_j = null_lpvar; - for (unsigned j : m.vars()){ - if (val(j).is_zero()){ + for (unsigned j : m.vars()) { + if (val(j).is_zero()) { if (c().var_is_fixed_to_zero(j)) fixed_zeros.push_back(j); @@ -193,7 +181,7 @@ void basics::generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, in // we know all the signs new_lemma lemma(c(), "strict case 0"); c().mk_ineq(zero_j, (sign_of_zj == 1? llc::GT : llc::LT)); - for (unsigned j : m.vars()){ + for (unsigned j : m.vars()) { if (j != zero_j) { negate_strict_sign(j); } @@ -333,11 +321,12 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_derived(const monic& rm lpvar jl = null_lpvar; for (auto fc : f ) { lpvar j = var(fc); - if (abs(val(j)) == abs_mv && c().vars_are_equiv(j, mon_var) && + if (abs(val(j)) == abs_mv && c().vars_are_equiv(j, mon_var) && (mon_var_is_sep_from_zero || c().var_is_separated_from_zero(j))) { jl = j; - break; } + else if (j == jl) + return false; } if (jl == null_lpvar) return false; @@ -495,7 +484,7 @@ bool basics::factorization_has_real(const factorization& f) const { // here we use the fact xy = 0 -> x = 0 or y = 0 void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factorization& f) { TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout);); - SASSERT(var_val(rm).is_zero()&& ! c().rm_check(rm)); + SASSERT(var_val(rm).is_zero() && !c().rm_check(rm)); new_lemma lemma(c(), "xy = 0 -> x = 0 or y = 0"); if (!is_separated_from_zero(f)) { c().mk_ineq(var(rm), llc::NE); @@ -546,16 +535,16 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const mo for (auto j : m.vars() ) { if (abs(val(j)) == abs_mv) { jl = j; - break; } + else if (jl == j) + return false; } if (jl == null_lpvar) return false; + lpvar not_one_j = null_lpvar; - unsigned num_occs = 0; for (auto j : m.vars() ) { if (j == jl) { - ++num_occs; continue; } if (abs(val(j)) != rational(1)) { @@ -563,9 +552,6 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const mo break; } } - - if (num_occs > 1) - return false; if (not_one_j == null_lpvar) { return false; @@ -589,19 +575,28 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const mo return true; } -// use the fact -// 1 * 1 ... * 1 * x * 1 ... * 1 = x +/** + m = f1 * f2 * .. * fn + where + - at most one fi evaluates to something different from +1 or -1 + - sign = f1 * ... f_{i-1} * f_{i+1} * .. + - sign = +1 or -1 + - add lemma + - /\_{j != i} f_j = val(f_j) => m = sign * f_i + or + - /\_j f_j = val(f_j) => m = sign +*/ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based_fm(const monic& m) { lpvar not_one = null_lpvar; rational sign(1); TRACE("nla_solver_bl", tout << "m = "; c().print_monic(m, tout);); - for (auto j : m.vars()){ + for (auto j : m.vars()) { auto v = val(j); if (v == rational(1)) { continue; } if (v == -rational(1)) { - sign = - sign; + sign = -sign; continue; } if (not_one == null_lpvar) { @@ -620,7 +615,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based_fm(co } new_lemma lemma(c(), __FUNCTION__); - for (auto j : m.vars()){ + for (auto j : m.vars()) { if (not_one == j) continue; c().mk_ineq(j, llc::NE, val(j)); } @@ -648,21 +643,24 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic return false; } lpvar jl = null_lpvar; - for (auto j : f ) { - if (abs(val(j)) == abs_mv) { - jl = var(j); - break; + for (auto fc : f) { + lpvar j = var(fc); + if (abs(val(fc)) == abs_mv) { + jl = j; } + else if (j == jl) + return false; } if (jl == null_lpvar) return false; + lpvar not_one_j = null_lpvar; - for (auto j : f ) { - if (var(j) == jl) { + for (auto fc : f) { + if (var(fc) == jl) { continue; } - if (abs(val(j)) != rational(1)) { - not_one_j = var(j); + if (abs(val(fc)) != rational(1)) { + not_one_j = var(fc); break; } } @@ -704,7 +702,6 @@ void basics::basic_lemma_for_mon_neutral_model_based(const monic& rm, const fact } /** - - m := f1*f2*.. - f_i are factors of m - at most one variable among f_i evaluates to something else than -1, +1. diff --git a/src/math/lp/nla_basics_lemmas.h b/src/math/lp/nla_basics_lemmas.h index 57cee8339..0e99e7fec 100644 --- a/src/math/lp/nla_basics_lemmas.h +++ b/src/math/lp/nla_basics_lemmas.h @@ -1,20 +1,9 @@ /*++ Copyright (c) 2017 Microsoft Corporation - Module Name: - - - - Abstract: - - - Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) - - Revision History: - + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) --*/ #pragma once diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp index ebb0a8a30..5630f09c1 100644 --- a/src/math/lp/nla_common.cpp +++ b/src/math/lp/nla_common.cpp @@ -1,21 +1,10 @@ /*++ Copyright (c) 2017 Microsoft Corporation - Module Name: - - - - Abstract: - - Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) - - Revision History: - - + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) --*/ #include "math/lp/nla_common.h" #include "math/lp/nla_core.h" diff --git a/src/math/lp/nla_common.h b/src/math/lp/nla_common.h index c15246915..c202dc427 100644 --- a/src/math/lp/nla_common.h +++ b/src/math/lp/nla_common.h @@ -1,20 +1,9 @@ /*++ Copyright (c) 2017 Microsoft Corporation - Module Name: - - - - Abstract: - - - Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) - - Revision History: - + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) --*/ #pragma once diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index dcb2dcaa3..8ca9d7cc7 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -6,8 +6,8 @@ Module Name: nla_core.cpp Author: - Nikolaj Bjorner (nbjorner) Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) --*/ #include "math/lp/nla_core.h" @@ -504,7 +504,7 @@ void core::fill_explanation_and_lemma_sign(const monic& a, const monic & b, rati tout << "used constraints: "; for (auto &p : current_expl()) m_lar_solver.constraints().display(tout, p.second); tout << "\n"; - ); + ); SASSERT(current_ineqs().size() == 0); mk_ineq(rational(1), a.var(), -sign, b.var(), llc::EQ, rational::zero()); TRACE("nla_solver", print_lemma(tout);); @@ -843,7 +843,7 @@ bool core::is_octagon_term(const lp::lar_term& t, bool & sign, lpvar& i, lpvar & return false; bool seen_minus = false; bool seen_plus = false; - i = -1; + i = null_lpvar; for(const auto & p : t) { const auto & c = p.coeff(); if (c == 1) { @@ -853,12 +853,12 @@ bool core::is_octagon_term(const lp::lar_term& t, bool & sign, lpvar& i, lpvar & } else { return false; } - if (i == static_cast(-1)) + if (i == null_lpvar) i = p.column(); else j = p.column(); } - SASSERT(j != static_cast(-1)); + SASSERT(j != null_lpvar); sign = (seen_minus && seen_plus)? false : true; return true; } diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index e971a2b78..4b594b15d 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -6,8 +6,8 @@ nla_core.h Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) --*/ #pragma once @@ -46,7 +46,7 @@ const lpvar null_lpvar = UINT_MAX; inline int rat_sign(const rational& r) { return r.is_pos()? 1 : ( r.is_neg()? -1 : 0); } inline rational rrat_sign(const rational& r) { return rational(rat_sign(r)); } -inline bool is_set(unsigned j) { return static_cast(j) != -1; } +inline bool is_set(unsigned j) { return j != null_lpvar; } inline bool is_even(unsigned k) { return (k >> 1) << 1 == k; } struct ineq { lp::lconstraint_kind m_cmp; diff --git a/src/math/lp/nla_defs.h b/src/math/lp/nla_defs.h index 111165431..df9158b42 100644 --- a/src/math/lp/nla_defs.h +++ b/src/math/lp/nla_defs.h @@ -1,19 +1,10 @@ /*++ Copyright (c) 2017 Microsoft Corporation - Module Name: - - - - Abstract: - - Author: - Nikolaj Bjorner (nbjorner) Lev Nachmanson (levnach) - - Revision History: + Nikolaj Bjorner (nbjorner) --*/ diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 4ce9c59d1..0545e9933 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -1,20 +1,9 @@ /*++ Copyright (c) 2017 Microsoft Corporation - Module Name: - - - - Abstract: - - - Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) - - Revision History: - + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) --*/ #pragma once diff --git a/src/math/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp index b88586a19..5d1fecb50 100644 --- a/src/math/lp/nla_monotone_lemmas.cpp +++ b/src/math/lp/nla_monotone_lemmas.cpp @@ -1,21 +1,9 @@ /*++ Copyright (c) 2017 Microsoft Corporation - Module Name: - - - - Abstract: - - - Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) - - Revision History: - - + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) --*/ #include "math/lp/nla_basics_lemmas.h" #include "math/lp/nla_core.h" diff --git a/src/math/lp/nla_monotone_lemmas.h b/src/math/lp/nla_monotone_lemmas.h index 5b8a066dd..fa8a64e75 100644 --- a/src/math/lp/nla_monotone_lemmas.h +++ b/src/math/lp/nla_monotone_lemmas.h @@ -1,21 +1,9 @@ /*++ Copyright (c) 2017 Microsoft Corporation - Module Name: - - - - Abstract: - - - Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) - - Revision History: - - + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) --*/ #pragma once namespace nla { diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index 0f65f4793..d0a47db9c 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -1,20 +1,9 @@ /*++ Copyright (c) 2017 Microsoft Corporation - Module Name: - - - - Abstract: - - - Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) - - Revision History: - + Nikolaj Bjorner (nbjorner) + Lev Nachmanson (levnach) --*/ #include "math/lp/nla_order_lemmas.h" @@ -105,7 +94,8 @@ void order::order_lemma_on_factor_binomial_explore(const monic& ac, bool k) { lpvar c = ac.vars()[k]; for (monic const& bd : _().emons().get_products_of(c)) { - if (bd.var() == ac.var()) continue; + if (bd.var() == ac.var()) + continue; TRACE("nla_solver", tout << "bd = " << pp_mon_with_vars(_(), bd);); order_lemma_on_factor_binomial_rm(ac, k, bd); if (done()) { @@ -262,13 +252,13 @@ void order::generate_ol_eq(const monic& ac, const factor& b) { new_lemma lemma(_(), __FUNCTION__); -#if 0 - IF_VERBOSE(0, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac - << " " << ab_cmp << " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n" - << " a " << sign_a << "*v" << var(a) << " " << val(a) << "\n" - << " b " << sign_b << "*v" << var(b) << " " << val(b) << "\n" - << " c " << sign_c << "*v" << var(c) << " " << val(c) << "\n"); -#endif + IF_VERBOSE(100, + verbose_stream() + << var_val(ac) << "(" << mul_val(ac) << "): " << ac + << " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n" + << " a " << "*v" << var(a) << " " << val(a) << "\n" + << " b " << "*v" << var(b) << " " << val(b) << "\n" + << " c " << "*v" << var(c) << " " << val(c) << "\n"); // ac == bc mk_ineq(c.var(),llc::EQ); // c is not equal to zero mk_ineq(ac.var(), -rational(1), bc.var(), llc::NE); @@ -288,13 +278,11 @@ void order::generate_ol(const monic& ac, const factor& b) { new_lemma lemma(_(), __FUNCTION__); -#if 0 - IF_VERBOSE(0, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac - << " " << ab_cmp << " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n" - << " a " << sign_a << "*v" << var(a) << " " << val(a) << "\n" - << " b " << sign_b << "*v" << var(b) << " " << val(b) << "\n" - << " c " << sign_c << "*v" << var(c) << " " << val(c) << "\n"); -#endif + IF_VERBOSE(100, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac + << " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n" + << " a " << "*v" << var(a) << " " << val(a) << "\n" + << " b " << "*v" << var(b) << " " << val(b) << "\n" + << " c " << "*v" << var(c) << " " << val(c) << "\n"); // fix the sign of c _().negate_relation(c.var(), rational(0)); _().negate_var_relation_strictly(ac.var(), bc.var()); @@ -326,7 +314,7 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac, generate_ol(ac, a, c, bc, b); return true; } else { - if((var_val(ac) == var_val(bc)) && (av_c_s != bv_c_s)) { + if ((var_val(ac) == var_val(bc)) && (av_c_s != bv_c_s)) { generate_ol_eq(ac, a, c, bc, b); } } diff --git a/src/math/lp/nla_order_lemmas.h b/src/math/lp/nla_order_lemmas.h index dbd579bae..272a070dc 100644 --- a/src/math/lp/nla_order_lemmas.h +++ b/src/math/lp/nla_order_lemmas.h @@ -1,20 +1,9 @@ /*++ Copyright (c) 2017 Microsoft Corporation - Module Name: - - - - Abstract: - - - Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) - - Revision History: - + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) --*/ #pragma once diff --git a/src/math/lp/nla_settings.h b/src/math/lp/nla_settings.h index 0baab2d38..4ba271afb 100644 --- a/src/math/lp/nla_settings.h +++ b/src/math/lp/nla_settings.h @@ -1,21 +1,10 @@ /*++ Copyright (c) 2017 Microsoft Corporation -Module Name: - - - -Abstract: - - - Author: Lev Nachmanson (levnach) -Revision History: - - --*/ #pragma once diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 766b43b0c..3c46c7897 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -1,21 +1,9 @@ /*++ Copyright (c) 2017 Microsoft Corporation - Module Name: - - - - Abstract: - - - Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) - - Revision History: - - + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) --*/ #include "math/lp/nla_solver.h" #include diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index 08eb346b5..7520c3fe0 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -1,20 +1,9 @@ /*++ Copyright (c) 2017 Microsoft Corporation -Module Name: - - - -Abstract: - - - Author: - Nikolaj Bjorner (nbjorner) Lev Nachmanson (levnach) - -Revision History: - + Nikolaj Bjorner (nbjorner) --*/ #pragma once diff --git a/src/math/lp/nla_tangent_lemmas.cpp b/src/math/lp/nla_tangent_lemmas.cpp index a32415cf9..2d6d1691d 100644 --- a/src/math/lp/nla_tangent_lemmas.cpp +++ b/src/math/lp/nla_tangent_lemmas.cpp @@ -1,20 +1,9 @@ /*++ Copyright (c) 2017 Microsoft Corporation - Module Name: - - - - Abstract: - - - Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) - - Revision History: - + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) --*/ #include "math/lp/nla_tangent_lemmas.h" diff --git a/src/math/lp/nla_tangent_lemmas.h b/src/math/lp/nla_tangent_lemmas.h index 95c771150..66f9c695b 100644 --- a/src/math/lp/nla_tangent_lemmas.h +++ b/src/math/lp/nla_tangent_lemmas.h @@ -1,21 +1,9 @@ /*++ Copyright (c) 2017 Microsoft Corporation - Module Name: - - - - Abstract: - - - Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) - - Revision History: - - + Lev Nachmanson (levnach) + Nikolaj Bjorner (nbjorner) --*/ #pragma once #include "util/rational.h"