move implementation of copyClauses to another file
This commit is contained in:
parent
4edbcf86b8
commit
59f653aabd
@ -161,14 +161,12 @@ CompilationFailedNode::weight (void) const
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
Clauses copyClauses (const Clauses& clauses);
|
|
||||||
|
|
||||||
LiftedCircuit::LiftedCircuit (const LiftedWCNF* lwcnf)
|
LiftedCircuit::LiftedCircuit (const LiftedWCNF* lwcnf)
|
||||||
: lwcnf_(lwcnf)
|
: lwcnf_(lwcnf)
|
||||||
{
|
{
|
||||||
root_ = 0;
|
root_ = 0;
|
||||||
compilationSucceeded_ = true;
|
compilationSucceeded_ = true;
|
||||||
Clauses clauses = copyClauses (lwcnf->clauses());
|
Clauses clauses = Clause::copyClauses (lwcnf->clauses());
|
||||||
compile (&root_, clauses);
|
compile (&root_, clauses);
|
||||||
if (Globals::verbosity > 1) {
|
if (Globals::verbosity > 1) {
|
||||||
smoothCircuit (root_);
|
smoothCircuit (root_);
|
||||||
@ -270,18 +268,6 @@ LiftedCircuit::compile (
|
|||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
// TODO
|
|
||||||
Clauses copyClauses (const Clauses& clauses)
|
|
||||||
{
|
|
||||||
Clauses copy;
|
|
||||||
copy.reserve (clauses.size());
|
|
||||||
for (size_t i = 0; i < clauses.size(); i++) {
|
|
||||||
copy.push_back (new Clause (*clauses[i]));
|
|
||||||
}
|
|
||||||
return copy;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
bool
|
bool
|
||||||
LiftedCircuit::tryUnitPropagation (
|
LiftedCircuit::tryUnitPropagation (
|
||||||
@ -289,7 +275,7 @@ LiftedCircuit::tryUnitPropagation (
|
|||||||
Clauses& clauses)
|
Clauses& clauses)
|
||||||
{
|
{
|
||||||
if (Globals::verbosity > 1) {
|
if (Globals::verbosity > 1) {
|
||||||
backupClauses_ = copyClauses (clauses);
|
backupClauses_ = Clause::copyClauses (clauses);
|
||||||
}
|
}
|
||||||
for (size_t i = 0; i < clauses.size(); i++) {
|
for (size_t i = 0; i < clauses.size(); i++) {
|
||||||
if (clauses[i]->isUnit()) {
|
if (clauses[i]->isUnit()) {
|
||||||
@ -391,7 +377,7 @@ LiftedCircuit::tryShannonDecomp (
|
|||||||
Clauses& clauses)
|
Clauses& clauses)
|
||||||
{
|
{
|
||||||
if (Globals::verbosity > 1) {
|
if (Globals::verbosity > 1) {
|
||||||
backupClauses_ = copyClauses (clauses);
|
backupClauses_ = Clause::copyClauses (clauses);
|
||||||
}
|
}
|
||||||
for (size_t i = 0; i < clauses.size(); i++) {
|
for (size_t i = 0; i < clauses.size(); i++) {
|
||||||
const Literals& literals = clauses[i]->literals();
|
const Literals& literals = clauses[i]->literals();
|
||||||
@ -403,7 +389,7 @@ LiftedCircuit::tryShannonDecomp (
|
|||||||
Clause* c2 = new Clause (*c1);
|
Clause* c2 = new Clause (*c1);
|
||||||
c2->literals().front().complement();
|
c2->literals().front().complement();
|
||||||
|
|
||||||
Clauses otherClauses = copyClauses (clauses);
|
Clauses otherClauses = Clause::copyClauses (clauses);
|
||||||
clauses.push_back (c1);
|
clauses.push_back (c1);
|
||||||
otherClauses.push_back (c2);
|
otherClauses.push_back (c2);
|
||||||
|
|
||||||
@ -433,7 +419,7 @@ LiftedCircuit::tryInclusionExclusion (
|
|||||||
Clauses& clauses)
|
Clauses& clauses)
|
||||||
{
|
{
|
||||||
if (Globals::verbosity > 1) {
|
if (Globals::verbosity > 1) {
|
||||||
backupClauses_ = copyClauses (clauses);
|
backupClauses_ = Clause::copyClauses (clauses);
|
||||||
}
|
}
|
||||||
for (size_t i = 0; i < clauses.size(); i++) {
|
for (size_t i = 0; i < clauses.size(); i++) {
|
||||||
Literals depLits = { clauses[i]->literals().front() };
|
Literals depLits = { clauses[i]->literals().front() };
|
||||||
@ -474,8 +460,8 @@ LiftedCircuit::tryInclusionExclusion (
|
|||||||
for (size_t j = 0; j < indepLits.size(); j++) {
|
for (size_t j = 0; j < indepLits.size(); j++) {
|
||||||
c2->addLiteral (indepLits[j]);
|
c2->addLiteral (indepLits[j]);
|
||||||
}
|
}
|
||||||
Clauses plus1Clauses = copyClauses (clauses);
|
Clauses plus1Clauses = Clause::copyClauses (clauses);
|
||||||
Clauses plus2Clauses = copyClauses (clauses);
|
Clauses plus2Clauses = Clause::copyClauses (clauses);
|
||||||
|
|
||||||
plus1Clauses.erase (plus1Clauses.begin() + i);
|
plus1Clauses.erase (plus1Clauses.begin() + i);
|
||||||
plus2Clauses.erase (plus2Clauses.begin() + i);
|
plus2Clauses.erase (plus2Clauses.begin() + i);
|
||||||
@ -513,7 +499,7 @@ LiftedCircuit::tryIndepPartialGrounding (
|
|||||||
// assumes that all literals have logical variables
|
// assumes that all literals have logical variables
|
||||||
// else, shannon decomp was possible
|
// else, shannon decomp was possible
|
||||||
if (Globals::verbosity > 1) {
|
if (Globals::verbosity > 1) {
|
||||||
backupClauses_ = copyClauses (clauses);
|
backupClauses_ = Clause::copyClauses (clauses);
|
||||||
}
|
}
|
||||||
LogVars rootLogVars;
|
LogVars rootLogVars;
|
||||||
LogVarSet lvs = clauses[0]->ipgCandidates();
|
LogVarSet lvs = clauses[0]->ipgCandidates();
|
||||||
@ -595,7 +581,7 @@ LiftedCircuit::tryAtomCounting (
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
if (Globals::verbosity > 1) {
|
if (Globals::verbosity > 1) {
|
||||||
backupClauses_ = copyClauses (clauses);
|
backupClauses_ = Clause::copyClauses (clauses);
|
||||||
}
|
}
|
||||||
for (size_t i = 0; i < clauses.size(); i++) {
|
for (size_t i = 0; i < clauses.size(); i++) {
|
||||||
Literals literals = clauses[i]->literals();
|
Literals literals = clauses[i]->literals();
|
||||||
@ -829,7 +815,7 @@ LiftedCircuit::createSmoothNode (
|
|||||||
if (missingLits.empty() == false) {
|
if (missingLits.empty() == false) {
|
||||||
if (Globals::verbosity > 1) {
|
if (Globals::verbosity > 1) {
|
||||||
// assert (Util::contains (originClausesMap_, prev));
|
// assert (Util::contains (originClausesMap_, prev));
|
||||||
backupClauses_ = originClausesMap_[*prev]; // TODO copyClauses ?
|
backupClauses_ = originClausesMap_[*prev]; // TODO Clause::copyClauses ?
|
||||||
}
|
}
|
||||||
Clauses clauses;
|
Clauses clauses;
|
||||||
for (size_t i = 0; i < missingLits.size(); i++) {
|
for (size_t i = 0; i < missingLits.size(); i++) {
|
||||||
|
@ -308,6 +308,19 @@ Clause::independentClauses (Clause& c1, Clause& c2)
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Clauses
|
||||||
|
Clause::copyClauses (const Clauses& clauses)
|
||||||
|
{
|
||||||
|
Clauses copy;
|
||||||
|
copy.reserve (clauses.size());
|
||||||
|
for (size_t i = 0; i < clauses.size(); i++) {
|
||||||
|
copy.push_back (new Clause (*clauses[i]));
|
||||||
|
}
|
||||||
|
return copy;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
void
|
void
|
||||||
Clause::printClauses (const Clauses& clauses)
|
Clause::printClauses (const Clauses& clauses)
|
||||||
{
|
{
|
||||||
|
@ -132,9 +132,11 @@ class Clause
|
|||||||
void removeLiteral (size_t litIdx);
|
void removeLiteral (size_t litIdx);
|
||||||
|
|
||||||
static bool independentClauses (Clause& c1, Clause& c2);
|
static bool independentClauses (Clause& c1, Clause& c2);
|
||||||
|
|
||||||
|
static vector<Clause*> copyClauses (const vector<Clause*>& clauses);
|
||||||
|
|
||||||
static void printClauses (const vector<Clause*>& clauses);
|
static void printClauses (const vector<Clause*>& clauses);
|
||||||
|
|
||||||
friend std::ostream& operator<< (ostream &os, const Clause& clause);
|
friend std::ostream& operator<< (ostream &os, const Clause& clause);
|
||||||
|
|
||||||
private:
|
private:
|
||||||
|
Reference in New Issue
Block a user