From 8999e1a340810dd181eddc7abbe14f3e2f828585 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 12 Aug 2024 08:29:06 -1000 Subject: [PATCH] use standard name conventions and add file headers Signed-off-by: Lev Nachmanson --- src/nlsat/nlsat_explain.h | 3 +- src/nlsat/nlsat_simple_checker.cpp | 26 +++------------- src/nlsat/nlsat_simple_checker.h | 25 ++++++++++++++-- src/nlsat/nlsat_solver.cpp | 4 +-- .../nlsat_variable_ordering_strategy.cpp | 30 +++++++++---------- src/nlsat/nlsat_variable_ordering_strategy.h | 27 +++++++++++++---- 6 files changed, 67 insertions(+), 48 deletions(-) diff --git a/src/nlsat/nlsat_explain.h b/src/nlsat/nlsat_explain.h index 2fdb76b11..f44a9ae92 100644 --- a/src/nlsat/nlsat_explain.h +++ b/src/nlsat/nlsat_explain.h @@ -8,7 +8,8 @@ Module Name: Abstract: Functor that implements the "explain" procedure defined in Dejan and Leo's paper. - + Uses paper Haokun Li and Bican Xia, "Solving Satisfiability of Polynomial Formulas By Sample - Cell Projection",https://arxiv.org/abs/2003.00409, + and code from https://github.com/hybridSMT/hybridSMT.git Author: Leonardo de Moura (leonardo) 2012-01-13. diff --git a/src/nlsat/nlsat_simple_checker.cpp b/src/nlsat/nlsat_simple_checker.cpp index 3e1e8dd1c..f61bc97ad 100644 --- a/src/nlsat/nlsat_simple_checker.cpp +++ b/src/nlsat/nlsat_simple_checker.cpp @@ -1,25 +1,7 @@ #include "nlsat/nlsat_simple_checker.h" -struct Debug_Tracer { - std::string tag_str; - Debug_Tracer(std::string _tag_str) { - tag_str = _tag_str; - TRACE("simple_checker", - tout << "Debug_Tracer begin\n"; - tout << tag_str << "\n"; - ); - } - ~Debug_Tracer() { - TRACE("simple_checker", - tout << "Debug_Tracer end\n"; - tout << tag_str << "\n"; - ); - } -}; - - namespace nlsat { - struct Simple_Checker::imp { + struct simple_checker::imp { // solver / pmanager ± anum_manager &am; @@ -1569,13 +1551,13 @@ else { // ( == 0) + (c > 0) -> > 0 return true; } }; - Simple_Checker::Simple_Checker(pmanager &_pm, anum_manager &_am, const clause_vector &_clauses, literal_vector &_learned_unit, const atom_vector &_atoms, const unsigned &_arith_var_num) { + simple_checker::simple_checker(pmanager &_pm, anum_manager &_am, const clause_vector &_clauses, literal_vector &_learned_unit, const atom_vector &_atoms, const unsigned &_arith_var_num) { m_imp = alloc(imp, _pm, _am, _clauses, _learned_unit, _atoms, _arith_var_num); } - Simple_Checker::~Simple_Checker() { + simple_checker::~simple_checker() { dealloc(m_imp); } - bool Simple_Checker::operator()() { + bool simple_checker::operator()() { return m_imp->operator()(); } } diff --git a/src/nlsat/nlsat_simple_checker.h b/src/nlsat/nlsat_simple_checker.h index 1a854e855..c13e2669c 100644 --- a/src/nlsat/nlsat_simple_checker.h +++ b/src/nlsat/nlsat_simple_checker.h @@ -1,14 +1,33 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + nlsat_simple_checker.cpp + +Abstract: + + Attempts to find a conflict by using simple polynomial forms. +Author: + + Mengyu Zhao (Linxi) and Shaowei Cai + +Revision History: + +--*/ + +#pragma once #include "math/polynomial/algebraic_numbers.h" #include "nlsat/nlsat_clause.h" namespace nlsat { - class Simple_Checker { + class simple_checker { struct imp; imp * m_imp; public: - Simple_Checker(pmanager &_pm, anum_manager &_am, const clause_vector &_clauses, literal_vector &_learned_unit, const atom_vector &_atoms, const unsigned &_arith_var_num); - ~Simple_Checker(); + simple_checker(pmanager &_pm, anum_manager &_am, const clause_vector &_clauses, literal_vector &_learned_unit, const atom_vector &_atoms, const unsigned &_arith_var_num); + ~simple_checker(); bool operator()(); }; } \ No newline at end of file diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 1c4aabe50..7c2dd1def 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -1783,7 +1783,7 @@ namespace nlsat { // test_anum(); literal_vector learned_unit; // Simple_Checker checker(m_solver, m_pm, m_am, m_clauses, m_learned, m_atoms, m_is_int.size()); - Simple_Checker checker(m_pm, m_am, m_clauses, learned_unit, m_atoms, m_is_int.size()); + simple_checker checker(m_pm, m_am, m_clauses, learned_unit, m_atoms, m_is_int.size()); if (!checker()) return false; for (unsigned i = 0, sz = learned_unit.size(); i < sz; ++i) { @@ -1800,7 +1800,7 @@ namespace nlsat { TRACE("reorder", tout << "runing vos: " << m_variable_ordering_strategy << '\n';); unsigned num = num_vars(); - VOS_Var_Info_Collector vos_collector(m_pm, m_atoms, num, m_variable_ordering_strategy); + vos_var_info_collector vos_collector(m_pm, m_atoms, num, m_variable_ordering_strategy); vos_collector.collect(m_clauses); vos_collector.collect(m_learned); diff --git a/src/nlsat/nlsat_variable_ordering_strategy.cpp b/src/nlsat/nlsat_variable_ordering_strategy.cpp index dfcc14201..5b91501e3 100644 --- a/src/nlsat/nlsat_variable_ordering_strategy.cpp +++ b/src/nlsat/nlsat_variable_ordering_strategy.cpp @@ -1,7 +1,7 @@ #include "nlsat/nlsat_variable_ordering_strategy.h" namespace nlsat { - struct VOS_Var_Info_Collector::imp { + struct vos_var_info_collector::imp { pmanager & pm; atom_vector const & m_atoms; unsigned num_vars; @@ -138,8 +138,8 @@ namespace nlsat { struct univariate_reorder_lt { - VOS_Var_Info_Collector::imp const *m_info; - univariate_reorder_lt(VOS_Var_Info_Collector::imp const *info):m_info(info) {} + vos_var_info_collector::imp const *m_info; + univariate_reorder_lt(vos_var_info_collector::imp const *info):m_info(info) {} bool operator()(var x, var y) const { if (m_info->m_num_uni[x] != m_info->m_num_uni[y]) return m_info->m_num_uni[x] > m_info->m_num_uni[y]; @@ -148,8 +148,8 @@ namespace nlsat { }; struct feature_reorder_lt { - VOS_Var_Info_Collector::imp const *m_info; - feature_reorder_lt(VOS_Var_Info_Collector::imp const * info): m_info(info){} + vos_var_info_collector::imp const *m_info; + feature_reorder_lt(vos_var_info_collector::imp const * info): m_info(info){} bool operator()(var x, var y) const { if (m_info->m_max_degree[x] != m_info->m_max_degree[y]) return m_info->m_max_degree[x] > m_info->m_max_degree[y]; @@ -162,8 +162,8 @@ namespace nlsat { } }; struct brown_reorder_lt { - VOS_Var_Info_Collector::imp const *m_info; - brown_reorder_lt(VOS_Var_Info_Collector::imp const *info):m_info(info) {} + vos_var_info_collector::imp const *m_info; + brown_reorder_lt(vos_var_info_collector::imp const *info):m_info(info) {} bool operator()(var x, var y) const { // if (a.max_degree != b.max_degree) // return a.max_degree > b.max_degree; @@ -180,8 +180,8 @@ namespace nlsat { } }; struct triangular_reorder_lt { - const VOS_Var_Info_Collector::imp *m_info; - triangular_reorder_lt(VOS_Var_Info_Collector::imp const *info):m_info(info) {} + const vos_var_info_collector::imp *m_info; + triangular_reorder_lt(vos_var_info_collector::imp const *info):m_info(info) {} bool operator()(var x, var y) const { // if (a.max_degree != b.max_degree) // return a.max_degree > b.max_degree; @@ -198,8 +198,8 @@ namespace nlsat { } }; struct onlypoly_reorder_lt { - const VOS_Var_Info_Collector::imp *m_info; - onlypoly_reorder_lt(VOS_Var_Info_Collector::imp const *info):m_info(info) {} + const vos_var_info_collector::imp *m_info; + onlypoly_reorder_lt(vos_var_info_collector::imp const *info):m_info(info) {} bool operator()(var x, var y) const { // high degree first if (m_info->m_max_degree[x] != m_info->m_max_degree[y]) @@ -267,16 +267,16 @@ namespace nlsat { // return out; // } }; - VOS_Var_Info_Collector::VOS_Var_Info_Collector(pmanager & _pm, atom_vector const & _atoms, unsigned _num_vars, unsigned _vos_type) { + vos_var_info_collector::vos_var_info_collector(pmanager & _pm, atom_vector const & _atoms, unsigned _num_vars, unsigned _vos_type) { m_imp = alloc(imp, _pm, _atoms, _num_vars, _vos_type); } - VOS_Var_Info_Collector::~VOS_Var_Info_Collector() { + vos_var_info_collector::~vos_var_info_collector() { dealloc(m_imp); } - void VOS_Var_Info_Collector::collect(clause_vector const & cs) { + void vos_var_info_collector::collect(clause_vector const & cs) { m_imp->collect(cs); } - void VOS_Var_Info_Collector::operator()(var_vector &perm) { + void vos_var_info_collector::operator()(var_vector &perm) { m_imp->operator()(perm); } } diff --git a/src/nlsat/nlsat_variable_ordering_strategy.h b/src/nlsat/nlsat_variable_ordering_strategy.h index 6e01825c3..b29bece27 100644 --- a/src/nlsat/nlsat_variable_ordering_strategy.h +++ b/src/nlsat/nlsat_variable_ordering_strategy.h @@ -1,3 +1,22 @@ +/*++ +Copyright (c) 2024 Microsoft Corporation + +Module Name: + + nlsat_simple_checker.cpp + +Abstract: + + +Author: + + Mengyu Zhao (Linxi) and Shaowei Cai, ported from https://github.com/hybridSMT/hybridSMT.git + +Revision History: + +--*/ + +#pragma once #include "nlsat/nlsat_clause.h" @@ -11,16 +30,14 @@ namespace nlsat { typedef polynomial::manager::numeral_vector numeral_vector; - // enum Variable_Ordering_Strategy_Type {NONE = 0, BROWN, TRIANGULAR, ONLYPOLY}; - enum Variable_Ordering_Strategy_Type {NONE = 0, BROWN, TRIANGULAR, ONLYPOLY, UNIVARIATE, FEATURE, ROOT}; - class VOS_Var_Info_Collector { + class vos_var_info_collector { struct imp; imp * m_imp; public: - VOS_Var_Info_Collector(pmanager & _pm, atom_vector const & atoms, unsigned _num_vars, unsigned _vos_type); - ~VOS_Var_Info_Collector(); + vos_var_info_collector(pmanager & _pm, atom_vector const & atoms, unsigned _num_vars, unsigned _vos_type); + ~vos_var_info_collector(); void operator()(var_vector &perm); void collect(clause_vector const & cs); };