2012-11-08 21:54:47 +00:00
|
|
|
#include "LiftedKc.h"
|
|
|
|
#include "LiftedWCNF.h"
|
|
|
|
#include "LiftedCircuit.h"
|
2012-11-12 15:20:42 +00:00
|
|
|
#include "LiftedOperations.h"
|
2012-11-09 18:42:21 +00:00
|
|
|
#include "Indexer.h"
|
2012-11-08 21:54:47 +00:00
|
|
|
|
|
|
|
|
|
|
|
LiftedKc::~LiftedKc (void)
|
|
|
|
{
|
2012-11-12 15:20:42 +00:00
|
|
|
delete lwcnf_;
|
|
|
|
delete circuit_;
|
2012-11-08 21:54:47 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Params
|
2012-11-09 18:42:21 +00:00
|
|
|
LiftedKc::solveQuery (const Grounds& query)
|
2012-11-08 21:54:47 +00:00
|
|
|
{
|
2012-11-14 23:13:46 +00:00
|
|
|
pfList_ = parfactorList;
|
2012-11-12 15:20:42 +00:00
|
|
|
LiftedOperations::shatterAgainstQuery (pfList_, query);
|
2012-11-14 23:13:46 +00:00
|
|
|
LiftedOperations::runWeakBayesBall (pfList_, query);
|
2012-11-12 15:20:42 +00:00
|
|
|
lwcnf_ = new LiftedWCNF (pfList_);
|
|
|
|
circuit_ = new LiftedCircuit (lwcnf_);
|
2012-11-27 16:54:02 +00:00
|
|
|
if (circuit_->isCompilationSucceeded() == false) {
|
2012-12-20 18:07:50 +00:00
|
|
|
cerr << "Error: the circuit compilation has failed." << endl;
|
2012-12-20 17:37:59 +00:00
|
|
|
exit (EXIT_FAILURE);
|
2012-11-27 16:54:02 +00:00
|
|
|
}
|
2012-11-09 18:42:21 +00:00
|
|
|
vector<PrvGroup> groups;
|
|
|
|
Ranges ranges;
|
|
|
|
for (size_t i = 0; i < query.size(); i++) {
|
|
|
|
ParfactorList::const_iterator it = pfList_.begin();
|
|
|
|
while (it != pfList_.end()) {
|
|
|
|
size_t idx = (*it)->indexOfGround (query[i]);
|
|
|
|
if (idx != (*it)->nrArguments()) {
|
|
|
|
groups.push_back ((*it)->argument (idx).group());
|
|
|
|
ranges.push_back ((*it)->range (idx));
|
|
|
|
break;
|
|
|
|
}
|
|
|
|
++ it;
|
|
|
|
}
|
|
|
|
}
|
2012-11-12 15:20:42 +00:00
|
|
|
assert (groups.size() == query.size());
|
2012-11-09 18:42:21 +00:00
|
|
|
Params params;
|
|
|
|
Indexer indexer (ranges);
|
|
|
|
while (indexer.valid()) {
|
|
|
|
for (size_t i = 0; i < groups.size(); i++) {
|
|
|
|
vector<LiteralId> litIds = lwcnf_->prvGroupLiterals (groups[i]);
|
|
|
|
for (size_t j = 0; j < litIds.size(); j++) {
|
|
|
|
if (indexer[i] == j) {
|
2012-11-14 18:40:03 +00:00
|
|
|
lwcnf_->addWeight (litIds[j], LogAware::one(),
|
|
|
|
LogAware::one());
|
2012-11-09 18:42:21 +00:00
|
|
|
} else {
|
2012-11-14 18:40:03 +00:00
|
|
|
lwcnf_->addWeight (litIds[j], LogAware::zero(),
|
|
|
|
LogAware::one());
|
2012-11-09 18:42:21 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
params.push_back (circuit_->getWeightedModelCount());
|
|
|
|
++ indexer;
|
|
|
|
}
|
|
|
|
LogAware::normalize (params);
|
2012-11-14 18:40:03 +00:00
|
|
|
if (Globals::logDomain) {
|
|
|
|
Util::exp (params);
|
|
|
|
}
|
2012-11-09 18:42:21 +00:00
|
|
|
return params;
|
2012-11-08 21:54:47 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
void
|
|
|
|
LiftedKc::printSolverFlags (void) const
|
|
|
|
{
|
|
|
|
stringstream ss;
|
|
|
|
ss << "lifted kc [" ;
|
|
|
|
ss << "log_domain=" << Util::toString (Globals::logDomain);
|
|
|
|
ss << "]" ;
|
|
|
|
cout << ss.str() << endl;
|
|
|
|
}
|
|
|
|
|