CVC3: vcl.h Source 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 #include "cdlist.h"
00032 
00033 namespace CVC3 {
00034 
00035   class SearchEngine;
00036   class Theory;
00037   class TheoryCore;
00038   class TheoryUF;
00039   class TheoryArith;
00040   class TheoryArray;
00041   class TheoryQuant;
00042   class TheoryRecords;
00043   class TheorySimulate;
00044   class TheoryBitvector;
00045   class TheoryDatatype;
00046   class Translator;
00047 
00048 class CVC_DLL VCL : public ValidityChecker {
00049 
00050   //! Pointers to main system components
00051   ExprManager* d_em;
00052   ContextManager* d_cm;
00053   TheoremManager* d_tm;
00054   SearchEngine* d_se;
00055 
00056   //! Pointers to theories
00057   TheoryCore* d_theoryCore;
00058   TheoryUF* d_theoryUF;
00059   TheoryArith* d_theoryArith;
00060   TheoryArray* d_theoryArray;
00061   TheoryQuant* d_theoryQuant;
00062   TheoryRecords* d_theoryRecords;
00063   TheorySimulate* d_theorySimulate;
00064   TheoryBitvector* d_theoryBitvector;
00065   TheoryDatatype* d_theoryDatatype;
00066   Translator* d_translator;
00067 
00068   //! All theories are stored in this common vector
00069   /*! This includes TheoryCore and TheoryArith. */
00070   std::vector<Theory*> d_theories;
00071 
00072   //! Command line flags
00073   CLFlags *d_flags;
00074 
00075   //! User-level view of the scope stack
00076   CDO<int> *d_stackLevel;
00077 
00078   //! Run-time statistics
00079   Statistics* d_statistics;
00080 
00081   //! Next index for user assertion
00082   size_t d_nextIdx;
00083 
00084   //! Structure to hold user assertions indexed by declaration order
00085   class UserAssertion {
00086     size_t d_idx;
00087     Theorem d_thm; //! The theorem of the assertion (a |- a)
00088     Theorem d_tcc; //! The proof of its TCC
00089   public:
00090     //! Default constructor
00091     UserAssertion() { }
00092     //! Constructor
00093     UserAssertion(const Theorem& thm, const Theorem& tcc, size_t idx)
00094       : d_idx(idx), d_thm(thm), d_tcc(tcc) { }
00095     //! Fetching a Theorem
00096     const Theorem& thm() const { return d_thm; }
00097     //! Fetching a TCC
00098     const Theorem& tcc() const { return d_tcc; }
00099     //! Auto-conversion to Theorem
00100     operator Theorem() { return d_thm; }
00101     //! Comparison for use in std::map, to sort in declaration order
00102     friend bool operator<(const UserAssertion& a1, const UserAssertion& a2) {
00103       return (a1.d_idx < a2.d_idx);
00104     }
00105   };
00106 
00107   //! Backtracking map of user assertions
00108   CDMap<Expr,UserAssertion>* d_userAssertions;
00109 
00110   //! Backtracking map of assertions when assertion batching is on
00111   CDList<Expr>* d_batchedAssertions;
00112 
00113   //! Index into batched Assertions
00114   CDO<unsigned>* d_batchedAssertionsIdx;
00115 
00116   //! Result of the last query()
00117   /*! Saved for printing assumptions and proofs.  Normally it is
00118    * Theorem3, but query() on a TCC returns a 2-valued Theorem. */
00119   Theorem3 d_lastQuery;
00120 
00121   //! Result of the last query(e, true) (for a TCC).
00122   Theorem d_lastQueryTCC;
00123 
00124   //! Closure of the last query(e): |- Gamma => e
00125   Theorem3 d_lastClosure;
00126 
00127   //! Whether to dump a trace (or a translated version)
00128   bool d_dump;
00129 
00130   // Private methods
00131 
00132   //! Construct the closure "|-_3 Gamma => phi" of thm = "Gamma |-_3 phi"
00133   Theorem3 deriveClosure(const Theorem3& thm);
00134 
00135   //! Recursive assumption graph traversal to find user assumptions
00136   /*!
00137    *  If an assumption has a TCC, traverse the proof of TCC and add its
00138    *  assumptions to the set recursively.
00139    */
00140   void getAssumptionsRec(const Theorem& thm,
00141        std::set<UserAssertion>& assumptions,
00142        bool addTCCs);
00143 
00144   //! Get set of user assertions from the set of assumptions
00145   void getAssumptions(const Assumptions& a, std::vector<Expr>& assumptions);
00146 
00147   //! Check the tcc
00148   Theorem checkTCC(const Expr& tcc);
00149 
00150 #ifdef _CVC3_DEBUG_MODE
00151     //! Print an entry to the dump file: change of scope
00152     void dumpTrace(int scope);
00153 #endif
00154 
00155   //! Initialize everything except flags
00156   void init(void);
00157   //! Destroy everything except flags
00158   void destroy(void);
00159 
00160 public:
00161   // Takes the vector of command line flags.
00162   VCL(const CLFlags& flags);
00163   ~VCL();
00164 
00165   // Implementation of vc.h virtual functions
00166 
00167   CLFlags& getFlags() const { return *d_flags; }
00168   void reprocessFlags();
00169 
00170   TheoryCore* core();
00171 
00172   Type boolType();
00173   Type realType();
00174   Type intType();
00175   Type subrangeType(const Expr& l, const Expr& r);
00176   Type subtypeType(const Expr& pred, const Expr& witness);
00177   Type tupleType(const Type& type0, const Type& type1);
00178   Type tupleType(const Type& type0, const Type& type1, const Type& type2);
00179   Type tupleType(const std::vector<Type>& types);
00180   Type recordType(const std::string& field, const Type& type);
00181   Type recordType(const std::string& field0, const Type& type0,
00182         const std::string& field1, const Type& type1);
00183   Type recordType(const std::string& field0, const Type& type0,
00184         const std::string& field1, const Type& type1,
00185         const std::string& field2, const Type& type2);
00186   Type recordType(const std::vector<std::string>& fields,
00187       const std::vector<Type>& types);
00188   Type dataType(const std::string& name,
00189                 const std::string& constructor,
00190                 const std::vector<std::string>& selectors,
00191                 const std::vector<Expr>& types);
00192   Type dataType(const std::string& name,
00193                 const std::vector<std::string>& constructors,
00194                 const std::vector<std::vector<std::string> >& selectors,
00195                 const std::vector<std::vector<Expr> >& types);
00196   void dataType(const std::vector<std::string>& names,
00197                 const std::vector<std::vector<std::string> >& constructors,
00198                 const std::vector<std::vector<std::vector<std::string> > >& selectors,
00199                 const std::vector<std::vector<std::vector<Expr> > >& types,
00200                 std::vector<Type>& returnTypes);
00201   Type arrayType(const Type& typeIndex, const Type& typeData);
00202   Type bitvecType(int n);
00203   Type funType(const Type& typeDom, const Type& typeRan);
00204   Type funType(const std::vector<Type>& typeDom, const Type& typeRan);
00205   Type createType(const std::string& typeName);
00206   Type createType(const std::string& typeName, const Type& def);
00207   Type lookupType(const std::string& typeName);
00208 
00209   ExprManager* getEM() { return d_em; }
00210   Expr varExpr(const std::string& name, const Type& type);
00211   Expr varExpr(const std::string& name, const Type& type, const Expr& def);
00212   Expr lookupVar(const std::string& name, Type* type);
00213   Type getType(const Expr& e);
00214   Type getBaseType(const Expr& e);
00215   Type getBaseType(const Type& e);
00216   Expr getTypePred(const Type&t, const Expr& e);
00217   Expr stringExpr(const std::string& str);
00218   Expr idExpr(const std::string& name);
00219   Expr listExpr(const std::vector<Expr>& kids);
00220   Expr listExpr(const Expr& e1);
00221   Expr listExpr(const Expr& e1, const Expr& e2);
00222   Expr listExpr(const Expr& e1, const Expr& e2, const Expr& e3);
00223   Expr listExpr(const std::string& op, const std::vector<Expr>& kids);
00224   Expr listExpr(const std::string& op, const Expr& e1);
00225   Expr listExpr(const std::string& op, const Expr& e1,
00226       const Expr& e2);
00227   Expr listExpr(const std::string& op, const Expr& e1,
00228     const Expr& e2, const Expr& e3);
00229   void printExpr(const Expr& e);
00230   void printExpr(const Expr& e, std::ostream& os);
00231   Expr parseExpr(const Expr& e);
00232   Type parseType(const Expr& e);
00233   Expr importExpr(const Expr& e);
00234   Type importType(const Type& t);
00235   void cmdsFromString(const std::string& s, InputLanguage lang);
00236   Expr exprFromString(const std::string& s);
00237 
00238   Expr trueExpr();
00239   Expr falseExpr();
00240   Expr notExpr(const Expr& child);
00241   Expr andExpr(const Expr& left, const Expr& right);
00242   Expr andExpr(const std::vector<Expr>& children);
00243   Expr orExpr(const Expr& left, const Expr& right);
00244   Expr orExpr(const std::vector<Expr>& children);
00245   Expr impliesExpr(const Expr& hyp, const Expr& conc);
00246   Expr iffExpr(const Expr& left, const Expr& right);
00247   Expr eqExpr(const Expr& child0, const Expr& child1);
00248   Expr distinctExpr(const std::vector<Expr>& children);
00249   Expr iteExpr(const Expr& ifpart, const Expr& thenpart, const Expr& elsepart);
00250 
00251   Op createOp(const std::string& name, const Type& type);
00252   Op createOp(const std::string& name, const Type& type, const Expr& def);
00253   Op lookupOp(const std::string& name, Type* type);
00254   Expr funExpr(const Op& op, const Expr& child);
00255   Expr funExpr(const Op& op, const Expr& left, const Expr& right);
00256   Expr funExpr(const Op& op, const Expr& child0, const Expr& child1, const Expr& child2);
00257   Expr funExpr(const Op& op, const std::vector<Expr>& children);
00258 
00259   bool addPairToArithOrder(const Expr& smaller, const Expr& bigger);
00260   Expr ratExpr(int n, int d);
00261   Expr ratExpr(const std::string& n, const std::string& d, int base);
00262   Expr ratExpr(const std::string& n, int base);
00263   Expr uminusExpr(const Expr& child);
00264   Expr plusExpr(const Expr& left, const Expr& right);
00265   Expr plusExpr(const std::vector<Expr>& children);
00266   Expr minusExpr(const Expr& left, const Expr& right);
00267   Expr multExpr(const Expr& left, const Expr& right);
00268   Expr powExpr(const Expr& x, const Expr& n);
00269   Expr divideExpr(const Expr& left, const Expr& right);
00270   Expr ltExpr(const Expr& left, const Expr& right);
00271   Expr leExpr(const Expr& left, const Expr& right);
00272   Expr gtExpr(const Expr& left, const Expr& right);
00273   Expr geExpr(const Expr& left, const Expr& right);
00274 
00275   Expr recordExpr(const std::string& field, const Expr& expr);
00276   Expr recordExpr(const std::string& field0, const Expr& expr0,
00277         const std::string& field1, const Expr& expr1);
00278   Expr recordExpr(const std::string& field0, const Expr& expr0,
00279         const std::string& field1, const Expr& expr1,
00280         const std::string& field2, const Expr& expr2);
00281   Expr recordExpr(const std::vector<std::string>& fields,
00282       const std::vector<Expr>& exprs);
00283   Expr recSelectExpr(const Expr& record, const std::string& field);
00284   Expr recUpdateExpr(const Expr& record, const std::string& field,
00285          const Expr& newValue);
00286 
00287   Expr readExpr(const Expr& array, const Expr& index);
00288   Expr writeExpr(const Expr& array, const Expr& index, const Expr& newValue);
00289 
00290   Expr newBVConstExpr(const std::string& s, int base);
00291   Expr newBVConstExpr(const std::vector<bool>& bits);
00292   Expr newBVConstExpr(const Rational& r, int len);
00293   Expr newConcatExpr(const Expr& t1, const Expr& t2);
00294   Expr newConcatExpr(const std::vector<Expr>& kids);
00295   Expr newBVExtractExpr(const Expr& e, int hi, int low);
00296   Expr newBVNegExpr(const Expr& t1);
00297   Expr newBVAndExpr(const Expr& t1, const Expr& t2);
00298   Expr newBVAndExpr(const std::vector<Expr>& kids);
00299   Expr newBVOrExpr(const Expr& t1, const Expr& t2);
00300   Expr newBVOrExpr(const std::vector<Expr>& kids);
00301   Expr newBVXorExpr(const Expr& t1, const Expr& t2);
00302   Expr newBVXorExpr(const std::vector<Expr>& kids);
00303   Expr newBVXnorExpr(const Expr& t1, const Expr& t2);
00304   Expr newBVXnorExpr(const std::vector<Expr>& kids);
00305   Expr newBVNandExpr(const Expr& t1, const Expr& t2);
00306   Expr newBVNorExpr(const Expr& t1, const Expr& t2);
00307   Expr newBVCompExpr(const Expr& t1, const Expr& t2);
00308   Expr newBVLTExpr(const Expr& t1, const Expr& t2);
00309   Expr newBVLEExpr(const Expr& t1, const Expr& t2);
00310   Expr newBVSLTExpr(const Expr& t1, const Expr& t2);
00311   Expr newBVSLEExpr(const Expr& t1, const Expr& t2);
00312   Expr newSXExpr(const Expr& t1, int len);
00313   Expr newBVUminusExpr(const Expr& t1);
00314   Expr newBVSubExpr(const Expr& t1, const Expr& t2);
00315   Expr newBVPlusExpr(int numbits, const std::vector<Expr>& k);
00316   Expr newBVPlusExpr(int numbits, const Expr& t1, const Expr& t2);
00317   Expr newBVMultExpr(int numbits, const Expr& t1, const Expr& t2);
00318   Expr newBVUDivExpr(const Expr& t1, const Expr& t2);
00319   Expr newBVURemExpr(const Expr& t1, const Expr& t2);
00320   Expr newBVSDivExpr(const Expr& t1, const Expr& t2);
00321   Expr newBVSRemExpr(const Expr& t1, const Expr& t2);
00322   Expr newBVSModExpr(const Expr& t1, const Expr& t2);
00323   Expr newFixedLeftShiftExpr(const Expr& t1, int r);
00324   Expr newFixedConstWidthLeftShiftExpr(const Expr& t1, int r);
00325   Expr newFixedRightShiftExpr(const Expr& t1, int r);
00326   Rational computeBVConst(const Expr& e);
00327 
00328   Expr tupleExpr(const std::vector<Expr>& exprs);
00329   Expr tupleSelectExpr(const Expr& tuple, int index);
00330   Expr tupleUpdateExpr(const Expr& tuple, int index, const Expr& newValue);
00331   Expr datatypeConsExpr(const std::string& constructor,
00332                         const std::vector<Expr>& args);
00333   Expr datatypeSelExpr(const std::string& selector, const Expr& arg);
00334   Expr datatypeTestExpr(const std::string& constructor, const Expr& arg);
00335   Expr boundVarExpr(const std::string& name, const std::string& uid,
00336         const Type& type);
00337   Expr forallExpr(const std::vector<Expr>& vars, const Expr& body);
00338   Expr forallExpr(const std::vector<Expr>& vars, const Expr& body,
00339       const std::vector<std::vector<Expr> >& triggers);
00340   void setTriggers(const Expr& e, const std::vector<std::vector<Expr> >& triggers);
00341   Expr existsExpr(const std::vector<Expr>& vars, const Expr& body);
00342   Op lambdaExpr(const std::vector<Expr>& vars, const Expr& body);
00343   Op transClosure(const Op& op);
00344   Expr simulateExpr(const Expr& f, const Expr& s0,
00345         const std::vector<Expr>& inputs, const Expr& n);
00346 
00347   void setResourceLimit(unsigned limit);
00348   void setTimeLimit(unsigned limit);
00349   void assertFormula(const Expr& e);
00350   void registerAtom(const Expr& e);
00351   Expr getImpliedLiteral();
00352   Expr simplify(const Expr& e);
00353   Theorem simplifyThm(const Expr& e);
00354   QueryResult query(const Expr& e);
00355   QueryResult checkUnsat(const Expr& e);
00356   QueryResult checkContinue();
00357   QueryResult restart(const Expr& e);
00358   void returnFromCheck();
00359   void getUserAssumptions(std::vector<Expr>& assumptions);
00360   void getInternalAssumptions(std::vector<Expr>& assumptions);
00361   void getAssumptions(std::vector<Expr>& assumptions);
00362   void getAssumptionsUsed(std::vector<Expr>& assumptions);
00363   Expr getProofQuery();
00364   void getCounterExample(std::vector<Expr>& assumptions, bool inOrder);
00365   void getConcreteModel(ExprMap<Expr> & m);
00366   QueryResult tryModelGeneration();
00367   FormulaValue value(const Expr& e);
00368   bool inconsistent(std::vector<Expr>& assumptions);
00369   bool inconsistent();
00370   bool incomplete();
00371   bool incomplete(std::vector<std::string>& reasons);
00372   Proof getProof();
00373   Expr getTCC();
00374   void getAssumptionsTCC(std::vector<Expr>& assumptions);
00375   Proof getProofTCC();
00376   Expr getClosure();
00377   Proof getProofClosure();
00378 
00379   int stackLevel();
00380   void push();
00381   void pop();
00382   void popto(int stackLevel);
00383   int scopeLevel();
00384   void pushScope();
00385   void popScope();
00386   void poptoScope(int scopeLevel);
00387   Context* getCurrentContext();
00388   void reset();
00389 
00390   void loadFile(const std::string& fileName,
00391     InputLanguage lang = PRESENTATION_LANG,
00392     bool interactive = false,
00393                 bool calledFromParser = false);
00394   void loadFile(std::istream& is,
00395     InputLanguage lang = PRESENTATION_LANG,
00396     bool interactive = false);
00397 
00398   Statistics& getStatistics() { return *d_statistics; }
00399   void printStatistics() { std::cout << *d_statistics << std::endl; }
00400   unsigned long getMemory(int verbosity = 0);
00401 
00402 };
00403 
00404 }
00405 
00406 #endif