30 return "QuBE w/ toplevel assignments";
44 std::string result_tmp_file=
"qube.out";
54 std::string options=
"";
58 "QuBE "+options+
" "+
qbf_tmp_file+
" > "+result_tmp_file).c_str());
65 std::ifstream in(result_tmp_file.c_str());
67 bool result_found=
false;
72 std::getline(in, line);
74 if(line!=
"" && line[line.size()-1]==
'\r')
75 line.resize(line.size()-1);
81 assignment[numeric_cast_v<std::size_t>(b.negate())] =
false;
83 assignment[numeric_cast_v<std::size_t>(b)] =
true;
85 else if(line==
"s cnf 1")
91 else if(line==
"s cnf 0")
106 int remove_result=remove(result_tmp_file.c_str());
virtual bool is_in_core(literalt l) const
#define CHECK_RETURN(CONDITION)
virtual ~qbf_qube_coret()
virtual const std::string solver_text()
virtual size_t no_clauses() const
virtual modeltypet m_get(literalt a) const
virtual resultt prop_solve()
mstreamt & result() const
mstreamt & status() const
virtual size_t no_variables() const override
virtual void write_qdimacs_cnf(std::ostream &out)