00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022 #ifndef _cvc3__include__vcl_h_
00023 #define _cvc3__include__vcl_h_
00024
00025 #include <queue>
00026
00027 #include "vc.h"
00028 #include "command_line_flags.h"
00029 #include "statistics.h"
00030 #include "cdmap.h"
00031
00032 namespace CVC3 {
00033
00034 class SearchEngine;
00035 class Theory;
00036 class TheoryCore;
00037 class TheoryUF;
00038 class TheoryArith;
00039 class TheoryArray;
00040 class TheoryQuant;
00041 class TheoryRecords;
00042 class TheorySimulate;
00043 class TheoryBitvector;
00044 class TheoryDatatype;
00045 class Translator;
00046
00047 class CVC_DLL VCL : public ValidityChecker {
00048
00049
00050 ExprManager* d_em;
00051 ContextManager* d_cm;
00052 TheoremManager* d_tm;
00053 SearchEngine* d_se;
00054
00055
00056 TheoryCore* d_theoryCore;
00057 TheoryUF* d_theoryUF;
00058 TheoryArith* d_theoryArith;
00059 TheoryArray* d_theoryArray;
00060 TheoryQuant* d_theoryQuant;
00061 TheoryRecords* d_theoryRecords;
00062 TheorySimulate* d_theorySimulate;
00063 TheoryBitvector* d_theoryBitvector;
00064 TheoryDatatype* d_theoryDatatype;
00065 Translator* d_translator;
00066
00067
00068
00069 std::vector<Theory*> d_theories;
00070
00071
00072 CLFlags *d_flags;
00073
00074
00075 CDO<int> *d_stackLevel;
00076
00077
00078 Statistics d_statistics;
00079
00080
00081 size_t d_nextIdx;
00082
00083
00084 class UserAssertion {
00085 size_t d_idx;
00086 Theorem d_thm;
00087 Theorem d_tcc;
00088 public:
00089
00090 UserAssertion() { }
00091
00092 UserAssertion(const Theorem& thm, const Theorem& tcc, size_t idx)
00093 : d_idx(idx), d_thm(thm), d_tcc(tcc) { }
00094
00095 const Theorem& thm() const { return d_thm; }
00096
00097 const Theorem& tcc() const { return d_tcc; }
00098
00099 operator Theorem() { return d_thm; }
00100
00101 friend bool operator<(const UserAssertion& a1, const UserAssertion& a2) {
00102 return (a1.d_idx < a2.d_idx);
00103 }
00104 };
00105
00106
00107 CDMap<Expr,UserAssertion>* d_userAssertions;
00108
00109
00110
00111
00112 Theorem3 d_lastQuery;
00113
00114
00115 Theorem d_lastQueryTCC;
00116
00117
00118 Theorem3 d_lastClosure;
00119
00120
00121 bool d_dump;
00122
00123
00124
00125
00126 Theorem3 deriveClosure(const Theorem3& thm);
00127
00128
00129
00130
00131
00132
00133 void getAssumptionsRec(const Theorem& thm,
00134 std::set<UserAssertion>& assumptions,
00135 bool addTCCs);
00136
00137
00138 void getAssumptions(const Assumptions& a, std::vector<Expr>& assumptions);
00139
00140
00141 Theorem checkTCC(const Expr& tcc);
00142
00143 #ifdef DEBUG
00144
00145 void dumpTrace(int scope);
00146 #endif
00147
00148 public:
00149
00150 VCL(const CLFlags& flags);
00151 ~VCL();
00152
00153
00154
00155 CLFlags& getFlags() const { return *d_flags; }
00156 void reprocessFlags();
00157
00158 TheoryCore* core();
00159
00160 Type boolType();
00161 Type realType();
00162 Type intType();
00163 Type subrangeType(const Expr& l, const Expr& r);
00164 Type subtypeType(const Expr& pred, const Expr& witness);
00165 Type tupleType(const Type& type0, const Type& type1);
00166 Type tupleType(const Type& type0, const Type& type1, const Type& type2);
00167 Type tupleType(const std::vector<Type>& types);
00168 Type recordType(const std::string& field, const Type& type);
00169 Type recordType(const std::string& field0, const Type& type0,
00170 const std::string& field1, const Type& type1);
00171 Type recordType(const std::string& field0, const Type& type0,
00172 const std::string& field1, const Type& type1,
00173 const std::string& field2, const Type& type2);
00174 Type recordType(const std::vector<std::string>& fields,
00175 const std::vector<Type>& types);
00176 Type dataType(const std::string& name,
00177 const std::string& constructor,
00178 const std::vector<std::string>& selectors,
00179 const std::vector<Expr>& types);
00180 Type dataType(const std::string& name,
00181 const std::vector<std::string>& constructors,
00182 const std::vector<std::vector<std::string> >& selectors,
00183 const std::vector<std::vector<Expr> >& types);
00184 void dataType(const std::vector<std::string>& names,
00185 const std::vector<std::vector<std::string> >& constructors,
00186 const std::vector<std::vector<std::vector<std::string> > >& selectors,
00187 const std::vector<std::vector<std::vector<Expr> > >& types,
00188 std::vector<Type>& returnTypes);
00189 Type arrayType(const Type& typeIndex, const Type& typeData);
00190 Type bitvecType(int n);
00191 Type funType(const Type& typeDom, const Type& typeRan);
00192 Type funType(const std::vector<Type>& typeDom, const Type& typeRan);
00193 Type createType(const std::string& typeName);
00194 Type createType(const std::string& typeName, const Type& def);
00195 Type lookupType(const std::string& typeName);
00196
00197 ExprManager* getEM() { return d_em; }
00198 Expr varExpr(const std::string& name, const Type& type);
00199 Expr varExpr(const std::string& name, const Type& type, const Expr& def);
00200 Expr boundVarExpr(const std::string& name, const std::string& uid,
00201 const Type& type);
00202 Expr lookupVar(const std::string& name, Type* type);
00203 Type getType(const Expr& e);
00204 Type getBaseType(const Expr& e);
00205 Type getBaseType(const Type& e);
00206 Expr getTypePred(const Type&t, const Expr& e);
00207 Expr stringExpr(const std::string& str);
00208 Expr idExpr(const std::string& name);
00209 Expr listExpr(const std::vector<Expr>& kids);
00210 Expr listExpr(const Expr& e1);
00211 Expr listExpr(const Expr& e1, const Expr& e2);
00212 Expr listExpr(const Expr& e1, const Expr& e2, const Expr& e3);
00213 Expr listExpr(const std::string& op, const std::vector<Expr>& kids);
00214 Expr listExpr(const std::string& op, const Expr& e1);
00215 Expr listExpr(const std::string& op, const Expr& e1,
00216 const Expr& e2);
00217 Expr listExpr(const std::string& op, const Expr& e1,
00218 const Expr& e2, const Expr& e3);
00219 void printExpr(const Expr& e);
00220 void printExpr(const Expr& e, std::ostream& os);
00221 Expr parseExpr(const Expr& e);
00222 Type parseType(const Expr& e);
00223 Expr importExpr(const Expr& e);
00224 Type importType(const Type& t);
00225
00226 Expr trueExpr();
00227 Expr falseExpr();
00228 Expr notExpr(const Expr& child);
00229 Expr andExpr(const Expr& left, const Expr& right);
00230 Expr andExpr(const std::vector<Expr>& children);
00231 Expr orExpr(const Expr& left, const Expr& right);
00232 Expr orExpr(const std::vector<Expr>& children);
00233 Expr impliesExpr(const Expr& hyp, const Expr& conc);
00234 Expr iffExpr(const Expr& left, const Expr& right);
00235 Expr eqExpr(const Expr& child0, const Expr& child1);
00236 Expr iteExpr(const Expr& ifpart, const Expr& thenpart, const Expr& elsepart);
00237
00238 Op createOp(const std::string& name, const Type& type);
00239 Op createOp(const std::string& name, const Type& type, const Expr& def);
00240 Expr funExpr(const Op& op, const Expr& child);
00241 Expr funExpr(const Op& op, const Expr& left, const Expr& right);
00242 Expr funExpr(const Op& op, const Expr& child0, const Expr& child1, const Expr& child2);
00243 Expr funExpr(const Op& op, const std::vector<Expr>& children);
00244
00245 Expr ratExpr(int n, int d);
00246 Expr ratExpr(const std::string& n, const std::string& d, int base);
00247 Expr ratExpr(const std::string& n, int base);
00248 Expr uminusExpr(const Expr& child);
00249 Expr plusExpr(const Expr& left, const Expr& right);
00250 Expr minusExpr(const Expr& left, const Expr& right);
00251 Expr multExpr(const Expr& left, const Expr& right);
00252 Expr powExpr(const Expr& x, const Expr& n);
00253 Expr divideExpr(const Expr& left, const Expr& right);
00254 Expr ltExpr(const Expr& left, const Expr& right);
00255 Expr leExpr(const Expr& left, const Expr& right);
00256 Expr gtExpr(const Expr& left, const Expr& right);
00257 Expr geExpr(const Expr& left, const Expr& right);
00258
00259 Expr recordExpr(const std::string& field, const Expr& expr);
00260 Expr recordExpr(const std::string& field0, const Expr& expr0,
00261 const std::string& field1, const Expr& expr1);
00262 Expr recordExpr(const std::string& field0, const Expr& expr0,
00263 const std::string& field1, const Expr& expr1,
00264 const std::string& field2, const Expr& expr2);
00265 Expr recordExpr(const std::vector<std::string>& fields,
00266 const std::vector<Expr>& exprs);
00267 Expr recSelectExpr(const Expr& record, const std::string& field);
00268 Expr recUpdateExpr(const Expr& record, const std::string& field,
00269 const Expr& newValue);
00270
00271 Expr readExpr(const Expr& array, const Expr& index);
00272 Expr writeExpr(const Expr& array, const Expr& index, const Expr& newValue);
00273
00274 Expr newBVConstExpr(const std::string& s, int base);
00275 Expr newBVConstExpr(const std::vector<bool>& bits);
00276 Expr newBVConstExpr(const Rational& r, int len);
00277 Expr newConcatExpr(const Expr& t1, const Expr& t2);
00278 Expr newConcatExpr(const std::vector<Expr>& kids);
00279 Expr newBVExtractExpr(const Expr& e, int hi, int low);
00280 Expr newBVNegExpr(const Expr& t1);
00281 Expr newBVAndExpr(const Expr& t1, const Expr& t2);
00282 Expr newBVAndExpr(const std::vector<Expr>& kids);
00283 Expr newBVOrExpr(const Expr& t1, const Expr& t2);
00284 Expr newBVOrExpr(const std::vector<Expr>& kids);
00285 Expr newBVXorExpr(const Expr& t1, const Expr& t2);
00286 Expr newBVXorExpr(const std::vector<Expr>& kids);
00287 Expr newBVXnorExpr(const Expr& t1, const Expr& t2);
00288 Expr newBVXnorExpr(const std::vector<Expr>& kids);
00289 Expr newBVNandExpr(const Expr& t1, const Expr& t2);
00290 Expr newBVNorExpr(const Expr& t1, const Expr& t2);
00291 Expr newBVLTExpr(const Expr& t1, const Expr& t2);
00292 Expr newBVLEExpr(const Expr& t1, const Expr& t2);
00293 Expr newBVSLTExpr(const Expr& t1, const Expr& t2);
00294 Expr newBVSLEExpr(const Expr& t1, const Expr& t2);
00295 Expr newSXExpr(const Expr& t1, int len);
00296 Expr newBVUminusExpr(const Expr& t1);
00297 Expr newBVSubExpr(const Expr& t1, const Expr& t2);
00298 Expr newBVPlusExpr(int numbits, const std::vector<Expr>& k);
00299 Expr newBVMultExpr(int numbits, const Expr& t1, const Expr& t2);
00300 Expr newFixedLeftShiftExpr(const Expr& t1, int r);
00301 Expr newFixedConstWidthLeftShiftExpr(const Expr& t1, int r);
00302 Expr newFixedRightShiftExpr(const Expr& t1, int r);
00303
00304 Expr tupleExpr(const std::vector<Expr>& exprs);
00305 Expr tupleSelectExpr(const Expr& tuple, int index);
00306 Expr tupleUpdateExpr(const Expr& tuple, int index, const Expr& newValue);
00307 Expr datatypeConsExpr(const std::string& constructor,
00308 const std::vector<Expr>& args);
00309 Expr datatypeSelExpr(const std::string& selector, const Expr& arg);
00310 Expr datatypeTestExpr(const std::string& constructor, const Expr& arg);
00311 Expr forallExpr(const std::vector<Expr>& vars, const Expr& body);
00312 Expr existsExpr(const std::vector<Expr>& vars, const Expr& body);
00313 Op lambdaExpr(const std::vector<Expr>& vars, const Expr& body);
00314 Expr simulateExpr(const Expr& f, const Expr& s0,
00315 const std::vector<Expr>& inputs, const Expr& n);
00316
00317 void setResourceLimit(unsigned limit);
00318 void assertFormula(const Expr& e);
00319 void registerAtom(const Expr& e);
00320 Expr getImpliedLiteral();
00321 Expr simplify(const Expr& e);
00322 Theorem simplifyThm(const Expr& e);
00323 QueryResult query(const Expr& e);
00324 QueryResult checkUnsat(const Expr& e);
00325 QueryResult checkContinue();
00326 QueryResult restart(const Expr& e);
00327 void returnFromCheck();
00328 void getUserAssumptions(std::vector<Expr>& assumptions);
00329 void getInternalAssumptions(std::vector<Expr>& assumptions);
00330 void getAssumptions(std::vector<Expr>& assumptions);
00331 void getAssumptionsUsed(std::vector<Expr>& assumptions);
00332 void getCounterExample(std::vector<Expr>& assumptions, bool inOrder);
00333 void getConcreteModel(ExprMap<Expr> & m);
00334 bool inconsistent(std::vector<Expr>& assumptions);
00335 bool incomplete();
00336 bool incomplete(std::vector<std::string>& reasons);
00337 Proof getProof();
00338 Expr getTCC();
00339 void getAssumptionsTCC(std::vector<Expr>& assumptions);
00340 Proof getProofTCC();
00341 Expr getClosure();
00342 Proof getProofClosure();
00343
00344 int stackLevel();
00345 void push();
00346 void pop();
00347 void popto(int stackLevel);
00348 int scopeLevel();
00349 void pushScope();
00350 void popScope();
00351 void poptoScope(int scopeLevel);
00352 Context* getCurrentContext();
00353
00354 void loadFile(const std::string& fileName,
00355 InputLanguage lang = PRESENTATION_LANG,
00356 bool interactive = false);
00357 void loadFile(std::istream& is,
00358 InputLanguage lang = PRESENTATION_LANG,
00359 bool interactive = false);
00360
00361 Statistics& getStatistics() { return d_statistics; }
00362 void printStatistics() { std::cout << d_statistics << std::endl; }
00363 unsigned long printMemory();
00364
00365 };
00366
00367 }
00368
00369 #endif