f74965b4af8ac92333ca5041d3487e7cacbd7ae7
[satune.git] / src / Backend / satencoder.h
1 #ifndef SATENCODER_H
2 #define SATENCODER_H
3
4 #include "classlist.h"
5 #include "structs.h"
6 #include "inc_solver.h"
7 #include "constraint.h"
8 #include "satelemencoder.h"
9 #include "satorderencoder.h"
10 #include "satfunctableencoder.h"
11
12
13 class SATEncoder {
14  public:
15         uint varcount;
16         CNF *cnf;
17         CSolver *solver;
18
19         SATEncoder(CSolver *solver);
20         ~SATEncoder();
21         void encodeAllSATEncoder(CSolver *csolver);
22         Edge encodeConstraintSATEncoder(Boolean *constraint);
23         MEMALLOC;
24 };
25
26
27         Edge getNewVarSATEncoder(SATEncoder *This);
28         void getArrayNewVarsSATEncoder(SATEncoder *encoder, uint num, Edge *carray);
29
30         Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar *constraint);
31         Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic *constraint);
32         Edge encodePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
33         Edge encodeTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
34         void encodeElementSATEncoder(SATEncoder *encoder, Element *This);
35         void encodeElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This);
36         void encodeTableElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This);
37 #endif