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

add files

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-08-14 11:16:44 +08:00
parent 92b5a9b134
commit 9958f42d5c
2 changed files with 52 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

27
src/util/lp/mon_eq.cpp Normal file
View file

@ -0,0 +1,27 @@
/*
Copyright (c) 2017 Microsoft Corporation
Author: Nikolaj Bjorner
*/
#include "util/lp/lar_solver.h"
#include "util/lp/mon_eq.h"
namespace nra {
bool check_assignment(mon_eq const& m, variable_map_type & vars) {
rational r1 = vars[m.m_v];
rational r2(1);
for (auto w : m.m_vs) {
r2 *= vars[w];
}
return r1 == r2;
}
bool check_assignments(const vector<mon_eq> & monomials,
const lp::lar_solver& s,
variable_map_type & vars) {
s.get_model(vars);
for (auto const& m : monomials) {
if (!check_assignment(m, vars)) return false;
}
return true;
}
}

25
src/util/lp/mon_eq.h Normal file
View file

@ -0,0 +1,25 @@
/*
Copyright (c) 2017 Microsoft Corporation
Author: Nikolaj Bjorner
*/
#include "util/lp/lp_settings.h"
#include "util/vector.h"
#include "util/lp/lar_solver.h"
namespace nra {
struct mon_eq {
mon_eq(lp::var_index v, unsigned sz, lp::var_index const* vs):
m_v(v), m_vs(sz, vs) {}
lp::var_index m_v;
svector<lp::var_index> m_vs;
unsigned var() const { return m_v; }
};
typedef std::unordered_map<lp::var_index, rational> variable_map_type;
bool check_assignment(mon_eq const& m, variable_map_type & vars);
bool check_assignments(const vector<mon_eq> & monomimials,
const lp::lar_solver& s,
variable_map_type & vars);
}