diff options
Diffstat (limited to 'src/prop')
| -rw-r--r-- | src/prop/Makefile.am | 4 | ||||
| -rw-r--r-- | src/prop/cnf_stream.cpp | 2 | ||||
| -rw-r--r-- | src/prop/cnf_stream.h | 2 | ||||
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 2 | ||||
| -rw-r--r-- | src/prop/prop_engine.cpp | 2 | ||||
| -rw-r--r-- | src/prop/sat_module.cpp | 2 | ||||
| -rw-r--r-- | src/prop/theory_proxy.cpp (renamed from src/prop/sat.cpp) | 2 | ||||
| -rw-r--r-- | src/prop/theory_proxy.h (renamed from src/prop/sat.h) | 17 |
8 files changed, 14 insertions, 19 deletions
diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am index e6c8752d6..02a6a4714 100644 --- a/src/prop/Makefile.am +++ b/src/prop/Makefile.am @@ -11,8 +11,8 @@ libprop_la_SOURCES = \ registrar.h \ prop_engine.cpp \ prop_engine.h \ - sat.h \ - sat.cpp \ + theory_proxy.h \ + theory_proxy.cpp \ cnf_stream.h \ cnf_stream.cpp \ sat_module.h \ diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 661221441..676cc4c49 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -27,7 +27,7 @@ #include "util/output.h" #include "expr/command.h" #include "expr/expr.h" -#include "prop/sat.h" +#include "prop/theory_proxy.h" #include <queue> diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 4812c6a21..af2ff2fcd 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -28,7 +28,7 @@ #define __CVC4__PROP__CNF_STREAM_H #include "expr/node.h" -#include "prop/sat.h" +#include "prop/theory_proxy.h" #include "prop/registrar.h" #include <ext/hash_map> diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 980cb1b3f..65ec025b1 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/mtl/Sort.h" #include "prop/minisat/core/Solver.h" -#include "prop/sat.h" +#include "prop/theory_proxy.h" #include "prop/sat_module.h" #include "util/output.h" #include "expr/command.h" diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index b7b3c685f..9d6a2c8f6 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -18,7 +18,7 @@ #include "prop/cnf_stream.h" #include "prop/prop_engine.h" -#include "prop/sat.h" +#include "prop/theory_proxy.h" #include "prop/sat_module.h" #include "theory/theory_engine.h" diff --git a/src/prop/sat_module.cpp b/src/prop/sat_module.cpp index cda32a0e8..5e5b78b44 100644 --- a/src/prop/sat_module.cpp +++ b/src/prop/sat_module.cpp @@ -22,7 +22,7 @@ #include "context/context.h" #include "theory/theory_engine.h" #include "expr/expr_stream.h" -#include "prop/sat.h" +#include "prop/theory_proxy.h" // DPLLT Minisat #include "prop/minisat/simp/SimpSolver.h" diff --git a/src/prop/sat.cpp b/src/prop/theory_proxy.cpp index ab8be39eb..43f7f75af 100644 --- a/src/prop/sat.cpp +++ b/src/prop/theory_proxy.cpp @@ -19,7 +19,7 @@ #include "prop/cnf_stream.h" #include "prop/prop_engine.h" -#include "prop/sat.h" +#include "prop/theory_proxy.h" #include "context/context.h" #include "theory/theory_engine.h" #include "theory/rewriter.h" diff --git a/src/prop/sat.h b/src/prop/theory_proxy.h index 8456e5d88..85dcae68b 100644 --- a/src/prop/sat.h +++ b/src/prop/theory_proxy.h @@ -31,14 +31,6 @@ #include "prop/sat_module.h" -#ifdef __CVC4_USE_MINISAT - -#include "prop/minisat/core/Solver.h" -#include "prop/minisat/core/SolverTypes.h" -#include "prop/minisat/simp/SimpSolver.h" - -#endif /* __CVC4_USE_MINISAT */ - namespace CVC4 { class TheoryEngine; @@ -150,19 +142,22 @@ inline std::ostream& operator <<(std::ostream& out, prop::SatLiteralValue val) { switch(val) { case prop::SatValUnknown: str = "_"; + break; case prop::SatValTrue: str = "1"; + break; case prop::SatValFalse: str = "0"; + break; default: - str = "Error"; + str = "Error"; + break; + } out << str; return out; } -} /* prop namespace */ - }/* CVC4 namespace */ #endif /* __CVC4__PROP__SAT_H */ |