00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021 #ifndef _cvc3__include__cnf_manager_h_
00022 #define _cvc3__include__cnf_manager_h_
00023
00024 #include "cnf.h"
00025 #include "expr.h"
00026 #include "expr_map.h"
00027 #include "cdmap.h"
00028 #include "statistics.h"
00029
00030 namespace CVC3 {
00031
00032 class CommonProofRules;
00033 class CNF_Rules;
00034 class ValidityChecker;
00035 class Statistics;
00036
00037 }
00038
00039 namespace SAT {
00040
00041 class CNF_Manager {
00042
00043
00044 CVC3::ValidityChecker* d_vc;
00045
00046
00047 bool d_minimizeClauses;
00048
00049
00050 CVC3::CommonProofRules* d_commonRules;
00051
00052
00053 CVC3::CNF_Rules* d_rules;
00054
00055
00056 struct Varinfo {
00057 CVC3::Expr expr;
00058 std::vector<Lit> fanins;
00059 std::vector<Var> fanouts;
00060 };
00061
00062
00063 std::vector<Varinfo> d_varInfo;
00064
00065
00066 CVC3::ExprMap<Var> d_cnfVars;
00067
00068
00069 CVC3::ExprMap<CVC3::Theorem> d_iteMap;
00070
00071
00072
00073
00074
00075
00076
00077 int d_clauseIdNext;
00078
00079
00080
00081
00082
00083 int d_bottomScope;
00084
00085
00086 std::deque<CVC3::Theorem> d_translateQueueThms;
00087
00088
00089 std::deque<Var> d_translateQueueVars;
00090
00091
00092 std::deque<bool> d_translateQueueFlags;
00093
00094
00095 CVC3::Statistics& d_statistics;
00096
00097 public:
00098
00099 class CNFCallback {
00100 public:
00101 CNFCallback() {}
00102 virtual ~CNFCallback() {}
00103
00104 virtual void registerAtom(const CVC3::Expr& e,
00105 const CVC3::Theorem& thm) = 0;
00106 };
00107
00108 private:
00109
00110 CNFCallback* d_cnfCallback;
00111
00112 CVC3::CNF_Rules* createProofRules(CVC3::TheoremManager* tm);
00113
00114
00115 void registerAtom(const CVC3::Expr& e, const CVC3::Theorem& thm);
00116
00117
00118
00119
00120
00121 Lit translateExprRec(const CVC3::Expr& e, CNF_Formula& cnf,
00122 const CVC3::Theorem& thmIn);
00123
00124
00125
00126
00127
00128 CVC3::Theorem replaceITErec(const CVC3::Expr& e, Var v, bool translateOnly);
00129
00130
00131
00132
00133 Lit translateExpr(const CVC3::Theorem& thmIn, CNF_Formula& cnf);
00134
00135
00136
00137
00138
00139
00140
00141
00142
00143
00144 public:
00145 CNF_Manager(CVC3::TheoremManager* tm, CVC3::Statistics& statistics, bool minimizeClauses);
00146 ~CNF_Manager();
00147
00148
00149 void registerCNFCallback(CNFCallback* cnfCallback)
00150 { d_cnfCallback = cnfCallback; }
00151
00152
00153 void setBottomScope(int scope) { d_bottomScope = scope; }
00154
00155
00156 unsigned numVars() { return d_varInfo.size(); }
00157
00158
00159
00160
00161
00162
00163
00164 unsigned numFanins(Lit c) {
00165 if (!c.isVar()) return 0;
00166 int index = c.getVar();
00167 if ((unsigned)index >= d_varInfo.size()) return 0;
00168 return d_varInfo[index].fanins.size();
00169 }
00170
00171
00172 Lit getFanin(Lit c, unsigned i) {
00173 DebugAssert(i < numFanins(c), "attempt to access unknown fanin");
00174 return d_varInfo[c.getVar()].fanins[i];
00175 }
00176
00177
00178
00179
00180
00181 unsigned numFanouts(Lit c) {
00182 if (!c.isVar()) return 0;
00183 int index = c.getVar();
00184 if ((unsigned)index >= d_varInfo.size()) return 0;
00185 return d_varInfo[index].fanouts.size();
00186 }
00187
00188
00189 Lit getFanout(Lit c, unsigned i) {
00190 DebugAssert(i < numFanouts(c), "attempt to access unknown fanin");
00191 return Lit(d_varInfo[c.getVar()].fanouts[i]);
00192 }
00193
00194
00195
00196
00197 CVC3::Expr concreteLit(Lit l, bool checkTranslated = true) {
00198 if (l.isNull()) return CVC3::Expr();
00199 bool inverted = !l.isPositive();
00200 int index = l.getVar();
00201 if ((unsigned)index >= d_varInfo.size() ||
00202 (checkTranslated && !d_varInfo[index].expr.isTranslated()))
00203 return CVC3::Expr();
00204 return inverted ? !d_varInfo[index].expr : d_varInfo[index].expr;
00205 }
00206
00207
00208
00209
00210 Lit getCNFLit(const CVC3::Expr& e) {
00211 if (e.isFalse()) return Lit::getFalse();
00212 if (e.isTrue()) return Lit::getTrue();
00213 if (e.isNot()) return !getCNFLit(e[0]);
00214 CVC3::ExprMap<Var>::iterator i = d_cnfVars.find(e);
00215 if (!e.isTranslated() || i == d_cnfVars.end()) return Lit();
00216 return Lit((*i).second);
00217 }
00218
00219 void cons(unsigned lb, unsigned ub, const CVC3::Expr& e2, std::vector<unsigned>& newLits);
00220
00221
00222
00223 void convertLemma(const CVC3::Theorem& thm, Clause& c);
00224
00225
00226
00227
00228 Lit addAssumption(const CVC3::Theorem& thm, CNF_Formula& cnf);
00229
00230
00231
00232
00233
00234
00235 Lit addLemma(const CVC3::Theorem& thm, CNF_Formula& cnf);
00236
00237 };
00238
00239 }
00240
00241 #endif