From 9958f42d5c2561fff0579ea5427e55f59844cfae Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 14 Aug 2018 11:16:44 +0800
Subject: [PATCH] add files

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/util/lp/mon_eq.cpp | 27 +++++++++++++++++++++++++++
 src/util/lp/mon_eq.h   | 25 +++++++++++++++++++++++++
 2 files changed, 52 insertions(+)
 create mode 100644 src/util/lp/mon_eq.cpp
 create mode 100644 src/util/lp/mon_eq.h

diff --git a/src/util/lp/mon_eq.cpp b/src/util/lp/mon_eq.cpp
new file mode 100644
index 000000000..d901353b4
--- /dev/null
+++ b/src/util/lp/mon_eq.cpp
@@ -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;
+}
+
+}
diff --git a/src/util/lp/mon_eq.h b/src/util/lp/mon_eq.h
new file mode 100644
index 000000000..cc44ff5ca
--- /dev/null
+++ b/src/util/lp/mon_eq.h
@@ -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);
+
+}