blob: 93d59423452c87fc82db1deb507b4d14335977be (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
#if ! defined _pres_dnf_h
#define _pres_dnf_h 1
#include <omega/pres_gen.h>
namespace omega {
//
// Disjunctive Normal Form -- list of Conjuncts
//
class DNF {
public:
void print(FILE *out_file);
void prefix_print(FILE *out_file, int debug = 1, bool parent_names_setup=false);
bool is_definitely_false() const;
bool is_definitely_true() const;
int length() const;
Conjunct *single_conjunct() const;
bool has_single_conjunct() const;
Conjunct *rm_first_conjunct();
void clear();
int query_guaranteed_leading_0s(int what_to_return_for_empty_dnf);
int query_possible_leading_0s(int what_to_return_for_empty_dnf);
int query_leading_dir();
private:
// all DNFize functions need to access the dnf builders:
friend class F_And;
friend class F_Or;
friend class Conjunct;
friend DNF * negate_conj(Conjunct *);
friend class Rel_Body;
friend_rel_ops;
DNF();
~DNF();
DNF* copy(Rel_Body *);
void simplify();
void make_level_carried_to(int level);
void count_leading_0s();
void add_conjunct(Conjunct*);
void join_DNF(DNF*);
void rm_conjunct(Conjunct *c);
void rm_redundant_conjs(int effort);
void rm_redundant_inexact_conjs();
void DNF_to_formula(Formula* root);
friend void remap_DNF_vars(Rel_Body *new_rel, Rel_Body *old_rel);
void remap();
void setup_names();
void remove_inexact_conj();
// These may need to get at the conjList itself:
friend DNF* DNF_and_DNF(DNF*, DNF*);
friend DNF* DNF_and_conj(DNF*, Conjunct*);
friend DNF* conj_and_not_dnf(Conjunct *pos_conj, DNF *neg_conjs, bool weak);
friend class DNF_Iterator;
List<Conjunct*> conjList;
};
DNF* conj_and_not_dnf(Conjunct *pos_conj, DNF *neg_conjs, bool weak=false);
//
// DNF iterator
//
class DNF_Iterator : public List_Iterator<Conjunct*> {
public:
DNF_Iterator(DNF*dnf) : List_Iterator<Conjunct*>(dnf->conjList) {}
DNF_Iterator() {}
void curr_set(Conjunct *c) { *(*this) = c; }
};
} // namespace
#endif
|
