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

use standard name conventions and add file headers

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-08-12 08:29:06 -10:00
parent 33f0256e20
commit 8999e1a340
6 changed files with 67 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/nlsat/nlsat_explain.h
View file

@ -8,7 +8,8 @@ Module Name:
Abstract: Abstract:
Functor that implements the "explain" procedure defined in Dejan and Leo's paper. 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: Author:
Leonardo de Moura (leonardo) 2012-01-13. Leonardo de Moura (leonardo) 2012-01-13.

26
src/nlsat/nlsat_simple_checker.cpp
View file

@ -1,25 +1,7 @@
#include "nlsat/nlsat_simple_checker.h" #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 { namespace nlsat {
struct Simple_Checker::imp { struct simple_checker::imp {
// solver &sol; // solver &sol;
pmanager &pm; pmanager &pm;
anum_manager &am; anum_manager &am;
@ -1569,13 +1551,13 @@ else { // ( == 0) + (c > 0) -> > 0
return true; 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); m_imp = alloc(imp, _pm, _am, _clauses, _learned_unit, _atoms, _arith_var_num);
} }
Simple_Checker::~Simple_Checker() { simple_checker::~simple_checker() {
dealloc(m_imp); dealloc(m_imp);
} }
bool Simple_Checker::operator()() { bool simple_checker::operator()() {
return m_imp->operator()(); return m_imp->operator()();
} }
} }

25
src/nlsat/nlsat_simple_checker.h
View file

@ -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 "math/polynomial/algebraic_numbers.h"
#include "nlsat/nlsat_clause.h" #include "nlsat/nlsat_clause.h"
namespace nlsat { namespace nlsat {
class Simple_Checker { class simple_checker {
struct imp; struct imp;
imp * m_imp; imp * m_imp;
public: 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(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();
bool operator()(); bool operator()();
}; };
} }

4
src/nlsat/nlsat_solver.cpp
View file

@ -1783,7 +1783,7 @@ namespace nlsat {
// test_anum(); // test_anum();
literal_vector learned_unit; 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_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()) if (!checker())
return false; return false;
for (unsigned i = 0, sz = learned_unit.size(); i < sz; ++i) { 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';); TRACE("reorder", tout << "runing vos: " << m_variable_ordering_strategy << '\n';);
unsigned num = num_vars(); 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_clauses);
vos_collector.collect(m_learned); vos_collector.collect(m_learned);

30
src/nlsat/nlsat_variable_ordering_strategy.cpp
View file

@ -1,7 +1,7 @@
#include "nlsat/nlsat_variable_ordering_strategy.h" #include "nlsat/nlsat_variable_ordering_strategy.h"
namespace nlsat { namespace nlsat {
struct VOS_Var_Info_Collector::imp { struct vos_var_info_collector::imp {
pmanager & pm; pmanager & pm;
atom_vector const & m_atoms; atom_vector const & m_atoms;
unsigned num_vars; unsigned num_vars;
@ -138,8 +138,8 @@ namespace nlsat {
struct univariate_reorder_lt { struct univariate_reorder_lt {
VOS_Var_Info_Collector::imp const *m_info; vos_var_info_collector::imp const *m_info;
univariate_reorder_lt(VOS_Var_Info_Collector::imp const *info):m_info(info) {} univariate_reorder_lt(vos_var_info_collector::imp const *info):m_info(info) {}
bool operator()(var x, var y) const { bool operator()(var x, var y) const {
if (m_info->m_num_uni[x] != m_info->m_num_uni[y]) 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]; return m_info->m_num_uni[x] > m_info->m_num_uni[y];
@ -148,8 +148,8 @@ namespace nlsat {
}; };
struct feature_reorder_lt { struct feature_reorder_lt {
VOS_Var_Info_Collector::imp const *m_info; vos_var_info_collector::imp const *m_info;
feature_reorder_lt(VOS_Var_Info_Collector::imp const * info): m_info(info){} feature_reorder_lt(vos_var_info_collector::imp const * info): m_info(info){}
bool operator()(var x, var y) const { bool operator()(var x, var y) const {
if (m_info->m_max_degree[x] != m_info->m_max_degree[y]) 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]; return m_info->m_max_degree[x] > m_info->m_max_degree[y];
@ -162,8 +162,8 @@ namespace nlsat {
} }
}; };
struct brown_reorder_lt { struct brown_reorder_lt {
VOS_Var_Info_Collector::imp const *m_info; vos_var_info_collector::imp const *m_info;
brown_reorder_lt(VOS_Var_Info_Collector::imp const *info):m_info(info) {} brown_reorder_lt(vos_var_info_collector::imp const *info):m_info(info) {}
bool operator()(var x, var y) const { bool operator()(var x, var y) const {
// if (a.max_degree != b.max_degree) // if (a.max_degree != b.max_degree)
// return a.max_degree > b.max_degree; // return a.max_degree > b.max_degree;
@ -180,8 +180,8 @@ namespace nlsat {
} }
}; };
struct triangular_reorder_lt { struct triangular_reorder_lt {
const VOS_Var_Info_Collector::imp *m_info; const vos_var_info_collector::imp *m_info;
triangular_reorder_lt(VOS_Var_Info_Collector::imp const *info):m_info(info) {} triangular_reorder_lt(vos_var_info_collector::imp const *info):m_info(info) {}
bool operator()(var x, var y) const { bool operator()(var x, var y) const {
// if (a.max_degree != b.max_degree) // if (a.max_degree != b.max_degree)
// return a.max_degree > b.max_degree; // return a.max_degree > b.max_degree;
@ -198,8 +198,8 @@ namespace nlsat {
} }
}; };
struct onlypoly_reorder_lt { struct onlypoly_reorder_lt {
const VOS_Var_Info_Collector::imp *m_info; const vos_var_info_collector::imp *m_info;
onlypoly_reorder_lt(VOS_Var_Info_Collector::imp const *info):m_info(info) {} onlypoly_reorder_lt(vos_var_info_collector::imp const *info):m_info(info) {}
bool operator()(var x, var y) const { bool operator()(var x, var y) const {
// high degree first // high degree first
if (m_info->m_max_degree[x] != m_info->m_max_degree[y]) if (m_info->m_max_degree[x] != m_info->m_max_degree[y])
@ -267,16 +267,16 @@ namespace nlsat {
// return out; // 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); 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); 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); 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); m_imp->operator()(perm);
} }
} }

27
src/nlsat/nlsat_variable_ordering_strategy.h
View file

@ -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" #include "nlsat/nlsat_clause.h"
@ -11,16 +30,14 @@ namespace nlsat {
typedef polynomial::manager::numeral_vector numeral_vector; 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}; 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; struct imp;
imp * m_imp; imp * m_imp;
public: public:
VOS_Var_Info_Collector(pmanager & _pm, atom_vector const & atoms, unsigned _num_vars, unsigned _vos_type); vos_var_info_collector(pmanager & _pm, atom_vector const & atoms, unsigned _num_vars, unsigned _vos_type);
~VOS_Var_Info_Collector(); ~vos_var_info_collector();
void operator()(var_vector &perm); void operator()(var_vector &perm);
void collect(clause_vector const & cs); void collect(clause_vector const & cs);
}; };