00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
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 }
00043
00044 #endif