00001 /*****************************************************************************/ 00002 /*! 00003 *\file queryresult.h 00004 *\brief enumerated type for result of queries 00005 * 00006 * Author: Clark Barrett 00007 * 00008 * Created: Thu May 18 12:36:25 2006 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 #ifndef _cvc3__include__queryresult_h_ 00022 #define _cvc3__include__queryresult_h_ 00023 00024 namespace CVC3 { 00025 00026 /*****************************************************************************/ 00027 /* 00028 * Type for result of queries. VALID and UNSATISFIABLE are treated as 00029 * equivalent, as are SATISFIABLE and INVALID. 00030 */ 00031 /*****************************************************************************/ 00032 typedef enum QueryResult { 00033 SATISFIABLE = 0, 00034 INVALID = 0, 00035 VALID = 1, 00036 UNSATISFIABLE = 1, 00037 ABORT, 00038 UNKNOWN 00039 } QueryResult; 00040 00041 } 00042 00043 #endif