1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 sat_integrity_checker.h 7 8 Abstract: 9 10 Checker whether the SAT solver internal datastructures 11 are consistent or not. 12 13 Author: 14 15 Leonardo de Moura (leonardo) 2011-05-21. 16 17 Revision History: 18 19 --*/ 20 #pragma once 21 22 #include "sat/sat_types.h" 23 #include "sat/sat_watched.h" 24 25 namespace sat { 26 class integrity_checker { 27 solver const & s; 28 public: 29 integrity_checker(solver const & s); 30 31 bool check_clause(clause const & c) const; 32 bool check_clauses(clause * const * begin, clause * const * end) const; 33 bool check_clauses() const; 34 bool check_learned_clauses() const; 35 bool check_assignment() const; 36 bool check_bool_vars() const; 37 bool check_watches() const; 38 bool check_watches(literal l, watch_list const& wlist) const; 39 bool check_watches(literal l) const; 40 bool check_reinit_stack() const; 41 bool check_disjoint_clauses() const; 42 bool operator()() const; 43 }; 44 }; 45