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