From c347018cb87ad93e7c2cfb60e3008640922ea75b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Feb 2017 11:49:30 -0800 Subject: [PATCH] testing lookahead Signed-off-by: Nikolaj Bjorner --- src/test/sat_lookahead.cpp | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 src/test/sat_lookahead.cpp diff --git a/src/test/sat_lookahead.cpp b/src/test/sat_lookahead.cpp new file mode 100644 index 000000000..d6993421b --- /dev/null +++ b/src/test/sat_lookahead.cpp @@ -0,0 +1,30 @@ +#include "sat_solver.h" +#include "sat_lookahead.h" +#include "dimacs.h" + +void tst_sat_lookahead(char ** argv, int argc, int& i) { + if (argc != i + 2) { + std::cout << "require dimacs file name\n"; + return; + } + enable_trace("sat"); + reslimit limit; + params_ref params; + sat::solver solver(params, limit); + sat::lookahead lh(solver); + char const* file_name = argv[i + 1]; + ++i; + + { + std::ifstream in(file_name); + if (in.bad() || in.fail()) { + std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl; + exit(ERR_OPEN_FILE); + } + parse_dimacs(in, solver); + } + + IF_VERBOSE(20, solver.display_status(verbose_stream());); + + std::cout << lh.check() << "\n"; +}