vcl.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file vcl.h
00004  * \brief Main implementation of ValidityChecker for CVC3.
00005  * 
00006  * Author: Clark Barrett
00007  * 
00008  * Created: Wed Dec 11 14:40:39 2002
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
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   //! Pointers to main system components
00050   ExprManager* d_em;
00051   ContextManager* d_cm;
00052   TheoremManager* d_tm;
00053   SearchEngine* d_se;
00054 
00055   //! Pointers to theories
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   //! All theories are stored in this common vector
00068   /*! This includes TheoryCore and TheoryArith. */
00069   std::vector<Theory*> d_theories;
00070 
00071   //! Command line flags
00072   CLFlags *d_flags;
00073 
00074   //! User-level view of the scope stack
00075   CDO<int> *d_stackLevel;
00076 
00077   //! Run-time statistics
00078   Statistics d_statistics;
00079 
00080   //! Next index for user assertion
00081   size_t d_nextIdx;
00082 
00083   //! Structure to hold user assertions indexed by declaration order
00084   class UserAssertion {
00085     size_t d_idx;
00086     Theorem d_thm; //! The theorem of the assertion (a |- a)
00087     Theorem d_tcc; //! The proof of its TCC
00088   public:
00089     //! Default constructor
00090     UserAssertion() { }
00091     //! Constructor
00092     UserAssertion(const Theorem& thm, const Theorem& tcc, size_t idx)
00093       : d_idx(idx), d_thm(thm), d_tcc(tcc) { }
00094     //! Fetching a Theorem
00095     const Theorem& thm() const { return d_thm; }
00096     //! Fetching a TCC
00097     const Theorem& tcc() const { return d_tcc; }
00098     //! Auto-conversion to Theorem
00099     operator Theorem() { return d_thm; }
00100     //! Comparison for use in std::map, to sort in declaration order
00101     friend bool operator<(const UserAssertion& a1, const UserAssertion& a2) {
00102       return (a1.d_idx < a2.d_idx);
00103     }
00104   };
00105 
00106   //! Backtracking map of user assertions
00107   CDMap<Expr,UserAssertion>* d_userAssertions;
00108 
00109   //! Result of the last query()
00110   /*! Saved for printing assumptions and proofs.  Normally it is
00111    * Theorem3, but query() on a TCC returns a 2-valued Theorem. */
00112   Theorem3 d_lastQuery;
00113 
00114   //! Result of the last query(e, true) (for a TCC).
00115   Theorem d_lastQueryTCC;
00116 
00117   //! Closure of the last query(e): |- Gamma => e
00118   Theorem3 d_lastClosure;
00119 
00120   //! Whether to dump a trace (or a translated version)
00121   bool d_dump;
00122 
00123   // Private methods
00124 
00125   //! Construct the closure "|-_3 Gamma => phi" of thm = "Gamma |-_3 phi"
00126   Theorem3 deriveClosure(const Theorem3& thm);
00127 
00128   //! Recursive assumption graph traversal to find user assumptions
00129   /*!
00130    *  If an assumption has a TCC, traverse the proof of TCC and add its
00131    *  assumptions to the set recursively.
00132    */
00133   void getAssumptionsRec(const Theorem& thm,
00134        std::set<UserAssertion>& assumptions,
00135        bool addTCCs);
00136 
00137   //! Get set of user assertions from the set of assumptions
00138   void getAssumptions(const Assumptions& a, std::vector<Expr>& assumptions);
00139 
00140   //! Check the tcc
00141   Theorem checkTCC(const Expr& tcc);
00142 
00143 #ifdef DEBUG
00144     //! Print an entry to the dump file: change of scope
00145     void dumpTrace(int scope);
00146 #endif
00147 
00148 public:
00149   // Takes the vector of command line flags.
00150   VCL(const CLFlags& flags);
00151   ~VCL();
00152 
00153   // Implementation of vc.h virtual functions
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

Generated on Tue Jul 3 14:33:42 2007 for CVC3 by  doxygen 1.5.1