Source

z3 / src / sat / sat_elim_eqs.h

/*++
Copyright (c) 2011 Microsoft Corporation

Module Name:

    sat_elim_eqs.h

Abstract:

    Helper class for eliminating eqs.

Author:

    Leonardo de Moura (leonardo) 2011-05-27.

Revision History:

--*/
#ifndef _SAT_ELIM_EQS_H_
#define _SAT_ELIM_EQS_H_

#include"sat_types.h"

namespace sat {
    class solver;
    
    class elim_eqs {
        solver & m_solver;
        void save_elim(literal_vector const & roots, bool_var_vector const & to_elim);
        void cleanup_clauses(literal_vector const & roots, clause_vector & cs);
        void cleanup_bin_watches(literal_vector const & roots);
        bool check_clauses(literal_vector const & roots) const;
    public:
        elim_eqs(solver & s);
        void operator()(literal_vector const & roots, bool_var_vector const & to_elim);
    };

};

#endif
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.