20 inline DdNode *DD::getNode()
const 61 std::string result_tmp_file=
"sKizzo.out";
71 std::string options=
"";
75 "sKizzo -log "+
qbf_tmp_file+options+
" > "+result_tmp_file).c_str());
81 std::ifstream in(result_tmp_file.c_str());
83 bool result_found=
false;
88 std::getline(in, line);
90 if(line!=
"" && line[line.size()-1]==
'\r')
91 line.resize(line.size()-1);
93 if(line==
"The instance evaluates to TRUE.")
99 else if(line==
"The instance evaluates to FALSE.")
114 remove(result_tmp_file.c_str());
145 std::string result_tmp_file=
"ozziKs.out";
146 std::string options=
"-dump qbm=bdd";
150 "ozziKs "+options+
" "+log_file+
" > "+result_tmp_file).c_str());
155 std::ifstream in(result_tmp_file.c_str());
156 std::string key=
" [OK, VALID,";
162 std::getline(in, line);
164 if(line!=
"" && line[line.size()-1]==
'\r')
165 line.resize(line.size()-1);
167 if(line.compare(0, key.size(), key)==0)
181 remove(result_tmp_file.c_str());
182 remove(log_file.c_str());
187 std::vector<int> e_list;
194 std::string key=
"# existentials[";
197 std::getline(in, line);
199 assert(line==
"# QBM file, 1.3");
203 std::getline(in, line);
205 if(line!=
"" && line[line.size()-1]==
'\r')
206 line.resize(line.size()-1);
208 if(line.compare(0, key.size(), key)==0)
215 size_t ob=line.find(
'[');
216 std::string n_es=line.substr(ob+1, line.find(
']')-ob-1);
221 std::string e_lists=line.substr(line.find(
':')+2);
223 for(
int i=0; i<n_e; i++)
225 size_t space=e_lists.find(
' ');
234 e_lists=e_lists.substr(space+1);
238 throw "existential mapping from sKizzo missing";
244 "sed -e \"s/^#.*$/# no comment/\" -i "+
qbf_tmp_file+
".qbm").c_str());
254 char filename[bdd_file.size()+1];
255 snprintf(filename, bdd_file.size()+1,
"%s", bdd_file.c_str());
260 Dddmp_cuddBddArrayLoad(
262 DDDMP_ROOT_MATCHLIST,
273 assert(nroots=2*n_e);
277 for(
unsigned i=0; i<e_list.size(); i++)
280 DdNode *posNode=bdds[2*i];
281 DdNode *negNode=bdds[2*i+1];
283 if(Cudd_DagSize(posNode)<=Cudd_DagSize(negNode))
290 for(
int i=0; i<nroots; i++)
295 remove(bdd_file.c_str());
virtual ~qbf_skizzo_coret()
static mstreamt & eom(mstreamt &m)
bool get_certificate(void)
virtual modeltypet m_get(literalt a) const
virtual size_t no_clauses() const
virtual bool is_in_core(literalt l) const
virtual resultt prop_solve()
virtual size_t no_variables() const override
int unsafe_string2int(const std::string &str, int base)
virtual const std::string solver_text()
virtual void write_qdimacs_cnf(std::ostream &out)