Skip to content

Commit

Permalink
use standard name conventions and add file headers
Browse files Browse the repository at this point in the history 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
  • Loading branch information
@levnach
levnach committed Aug 12, 2024
1 parent 33f0256 commit 8999e1a
Show file tree
Hide file tree
Showing 6 changed files with 67 additions and 48 deletions.
3 changes: 2 additions & 1 deletion src/nlsat/nlsat_explain.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
26 changes: 4 additions & 22 deletions src/nlsat/nlsat_simple_checker.cpp
View file
Original file line number Diff line number Diff line change
@@ -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 &sol;
pmanager &pm;
anum_manager &am;
Expand Down Expand Up @@ -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()();
}
}
25 changes: 22 additions & 3 deletions src/nlsat/nlsat_simple_checker.h
View file
Original file line number Diff line number Diff line change
@@ -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()();
};
}
4 changes: 2 additions & 2 deletions src/nlsat/nlsat_solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand All @@ -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);

Expand Down
30 changes: 15 additions & 15 deletions src/nlsat/nlsat_variable_ordering_strategy.cpp
View file
Original file line number Diff line number Diff line change
@@ -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;
Expand Down Expand Up @@ -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];
Expand All @@ -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];
Expand All @@ -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;
Expand All @@ -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;
Expand All @@ -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])
Expand Down Expand Up @@ -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);
}
}
27 changes: 22 additions & 5 deletions src/nlsat/nlsat_variable_ordering_strategy.h
View file
Original file line number Diff line number Diff line change
@@ -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"


Expand All @@ -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);
};
Expand Down

0 comments on commit 8999e1a

Please sign in to comment.