00001 /*****************************************************************************/ 00002 /*! 00003 * \file vc_cmd.h 00004 * 00005 * Author: Clark Barrett 00006 * 00007 * Created: Fri Dec 13 22:35:15 2002 00008 * 00009 * <hr> 00010 * 00011 * License to use, copy, modify, sell and/or distribute this software 00012 * and its documentation for any purpose is hereby granted without 00013 * royalty, subject to the terms and conditions defined in the \ref 00014 * LICENSE file provided with this distribution. 00015 * 00016 * <hr> 00017 * 00018 */ 00019 /*****************************************************************************/ 00020 00021 #ifndef _cvc3__vc_cvc__vc_cmd_h_ 00022 #define _cvc3__vc_cvc__vc_cmd_h_ 00023 00024 #include <string> 00025 #include "compat_hash_map.h" 00026 #include "exception.h" 00027 #include "queryresult.h" 00028 00029 namespace CVC3 { 00030 00031 class ValidityChecker; 00032 class Parser; 00033 class Context; 00034 class Expr; 00035 00036 template<class Data> 00037 class ExprMap; 00038 00039 class VCCmd { 00040 ValidityChecker* d_vc; 00041 Parser* d_parser; 00042 // TODO: move state variables into validity checker. 00043 typedef std::hash_map<const char*, Context*> CtxtMap; 00044 std::string d_name_of_cur_ctxt; 00045 CtxtMap d_map; 00046 00047 //! Take a parsed Expr and evaluate it 00048 bool evaluateCommand(const Expr& e); 00049 // Fetch the next command and evaluate it. Return true if 00050 // evaluation was successful, false otherwise. In especially bad 00051 // cases an exception may be thrown. 00052 bool evaluateNext(); 00053 void findAxioms(const Expr& e, ExprMap<bool>& skolemAxioms, 00054 ExprMap<bool>& visited); 00055 Expr skolemizeAx(const Expr& e); 00056 void reportResult(QueryResult qres, bool checkingValidity = true); 00057 00058 public: 00059 VCCmd(ValidityChecker* vc, Parser* parser); 00060 ~VCCmd(); 00061 00062 // Main loop function 00063 void processCommands(); 00064 }; 00065 00066 } 00067 00068 #endif