CVC3
|
00001 /*****************************************************************************/ 00002 /*! 00003 * \file circuit.h 00004 * \brief Circuit class 00005 * 00006 * <hr> 00007 * 00008 * License to use, copy, modify, sell and/or distribute this software 00009 * and its documentation for any purpose is hereby granted without 00010 * royalty, subject to the terms and conditions defined in the \ref 00011 * LICENSE file provided with this distribution. 00012 * 00013 * <hr> 00014 * 00015 */ 00016 /*****************************************************************************/ 00017 00018 #ifndef _cvc3__include__circuit_h_ 00019 #define _cvc3__include__circuit_h_ 00020 00021 #include "variable.h" 00022 #include "theorem.h" 00023 00024 using namespace std; 00025 00026 namespace CVC3 00027 { 00028 00029 class SearchEngineFast; 00030 00031 class Circuit 00032 { 00033 private: 00034 Theorem d_thm; 00035 Literal d_lits[4]; 00036 00037 public: 00038 Circuit(SearchEngineFast* se, const Theorem& thm); 00039 bool propagate(SearchEngineFast* se); 00040 }; 00041 00042 } // namespace CVC3 00043 00044 #endif