/*++ Copyright (c) 2017 Microsoft Corporation Abstract: simplification routines for pdd polys Author: Nikolaj Bjorner (nbjorner) Lev Nachmanson (levnach) --*/ #pragma once #include "util/uint_set.h" #include "math/grobner/pdd_solver.h" namespace dd { class simplifier { typedef solver::equation equation; typedef ptr_vector equation_vector; solver& s; public: simplifier(solver& s): s(s) {} void operator()(); private: struct compare_top_var; bool simplify_linear_step(bool binary); bool simplify_linear_step(equation_vector& linear); typedef vector use_list_t; use_list_t get_use_list(); void add_to_use(equation* e, use_list_t& use_list); void remove_from_use(equation* e, use_list_t& use_list); void remove_from_use(equation* e, use_list_t& use_list, unsigned except_v); bool simplify_cc_step(); bool simplify_elim_pure_step(); bool simplify_elim_dual_step(); bool simplify_leaf_step(); bool simplify_exlin(); void init_orbits(vector const& eqs, vector& orbits); void exlin_augment(vector const& orbits, vector& eqs); void simplify_exlin(vector const& orbits, vector const& eqs, vector& simp_eqs); }; }