Skip to content

Addressing linting errors in solvers/qbf #412

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jan 16, 2017
Merged

Addressing linting errors in solvers/qbf #412

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
160 changes: 87 additions & 73 deletions src/solvers/qbf/qbf_bdd_core.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,16 +14,28 @@ Author: CM Wintersteiger

#include <langapi/language_util.h>

#include <solvers/prop/literal.h>

#include <cuddObj.hh> // CUDD Library

/*! \cond */
// FIX FOR THE CUDD LIBRARY

inline DdNode *
DD::getNode() const
/*******************************************************************\

Function: DD::getNode

Inputs:

Outputs:

Purpose:

\*******************************************************************/

inline DdNode *DD::getNode() const
{
return node;

} // DD::getNode
/*! \endcond */

Expand All @@ -44,7 +56,7 @@ Function: qbf_bdd_certificatet::qbf_bdd_certificatet

qbf_bdd_certificatet::qbf_bdd_certificatet(void) : qdimacs_coret()
{
bdd_manager=new Cudd(0,0);
bdd_manager=new Cudd(0, 0);
}

/*******************************************************************\
Expand All @@ -61,11 +73,10 @@ Function: qbf_bdd_certificatet::~qbf_bdd_certificatet

qbf_bdd_certificatet::~qbf_bdd_certificatet(void)
{
for(model_bddst::iterator it=model_bdds.begin();
it!=model_bdds.end();
it++)
for(const BDD* model : model_bdds)
{
if(*it!=NULL) { delete(*it); *it=NULL; }
if(model)
delete model;
}
model_bdds.clear();

Expand Down Expand Up @@ -127,16 +138,18 @@ Function: qbf_bdd_coret::~qbf_bdd_coret

qbf_bdd_coret::~qbf_bdd_coret()
{
for(bdd_variable_mapt::iterator it=bdd_variable_map.begin();
it!=bdd_variable_map.end();
it++)
for(const BDD* variable : bdd_variable_map)
{
if (*it) { delete(*it); *it=NULL; }
if(variable)
delete variable;
}
bdd_variable_map.clear();

if(matrix) delete(matrix);
matrix=NULL;
if(matrix)
{
delete(matrix);
matrix=NULL;
}
}

/*******************************************************************\
Expand Down Expand Up @@ -189,17 +202,15 @@ Function: qbf_bdd_coret::prop_solve
propt::resultt qbf_bdd_coret::prop_solve()
{
{
std::string msg=
solver_text() + ": "+
std::to_string(no_variables())+" variables, "+
std::to_string(matrix->nodeCount())+" nodes";
messaget::status() << msg << messaget::eom;
status() << solver_text() << ": "
<< std::to_string(no_variables()) << " variables, "
<< std::to_string(matrix->nodeCount()) << " nodes" << eom;
}

model_bdds.resize(no_variables()+1, NULL);

// Eliminate variables
for(quantifierst::const_reverse_iterator it=quantifiers.rbegin();
for(auto it=quantifiers.rbegin();
it!=quantifiers.rend();
it++)
{
Expand All @@ -212,13 +223,14 @@ propt::resultt qbf_bdd_coret::prop_solve()
matrix->nodeCount() << " nodes" << std::endl;
#endif

BDD* model = new BDD();
BDD *model=new BDD();
const BDD &varbdd=*bdd_variable_map[var];
*model = matrix->AndAbstract(varbdd.Xnor(bdd_manager->bddOne()),
varbdd);
*model=matrix->AndAbstract(
varbdd.Xnor(bdd_manager->bddOne()),
varbdd);
model_bdds[var]=model;

*matrix = matrix->ExistAbstract(*bdd_variable_map[var]);
*matrix=matrix->ExistAbstract(*bdd_variable_map[var]);
}
else if(it->type==quantifiert::UNIVERSAL)
{
Expand All @@ -227,10 +239,10 @@ propt::resultt qbf_bdd_coret::prop_solve()
matrix->nodeCount() << " nodes" << std::endl;
#endif

*matrix = matrix->UnivAbstract(*bdd_variable_map[var]);
*matrix=matrix->UnivAbstract(*bdd_variable_map[var]);
}
else
throw ("Unquantified variable");
throw "unquantified variable";
}

if(*matrix==bdd_manager->bddOne())
Expand Down Expand Up @@ -261,7 +273,7 @@ Function: qbf_bdd_coret::is_in_core

bool qbf_bdd_coret::is_in_core(literalt l) const
{
throw ("NYI");
throw "nyi";
}

/*******************************************************************\
Expand All @@ -278,7 +290,7 @@ Function: qbf_bdd_coret::m_get

qdimacs_coret::modeltypet qbf_bdd_coret::m_get(literalt a) const
{
throw ("NYI");
throw "nyi";
}

/*******************************************************************\
Expand All @@ -299,7 +311,7 @@ literalt qbf_bdd_coret::new_variable()

bdd_variable_map.resize(res.var_no()+1, NULL);
BDD &var=*(new BDD());
var = bdd_manager->bddVar();
var=bdd_manager->bddVar();
bdd_variable_map[res.var_no()]=&var;

return res;
Expand All @@ -326,17 +338,17 @@ void qbf_bdd_coret::lcnf(const bvt &bv)

BDD clause(bdd_manager->bddZero());

for(unsigned long i=0; i<new_bv.size(); i++)
for(const literalt &l : new_bv)
{
literalt l=new_bv[i];
BDD v(*bdd_variable_map[l.var_no()]);

if(l.sign()) v = ~v;
if(l.sign())
v=~v;

clause |= v;
clause|=v;
}

*matrix &= clause;
*matrix&=clause;
}

/*******************************************************************\
Expand All @@ -353,15 +365,17 @@ Function: qbf_bdd_coret::lor

literalt qbf_bdd_coret::lor(literalt a, literalt b)
{
literalt nl = new_variable();
literalt nl=new_variable();

BDD abdd(*bdd_variable_map[a.var_no()]);
BDD bbdd(*bdd_variable_map[b.var_no()]);

if(a.sign()) abdd = ~abdd;
if(b.sign()) bbdd = ~bbdd;
if(a.sign())
abdd=~abdd;
if(b.sign())
bbdd=~bbdd;

*bdd_variable_map[nl.var_no()] |= abdd | bbdd;
*bdd_variable_map[nl.var_no()]|=abdd | bbdd;

return nl;
}
Expand All @@ -380,25 +394,26 @@ Function: qbf_bdd_coret::lor

literalt qbf_bdd_coret::lor(const bvt &bv)
{
forall_literals(it, bv)
if(*it==const_literal(true))
return const_literal(true);
for(const literalt &literal : bv)
{
if(literal==const_literal(true))
return literal;
}

literalt nl = new_variable();
literalt nl=new_variable();

BDD &orbdd = *bdd_variable_map[nl.var_no()];
BDD &orbdd=*bdd_variable_map[nl.var_no()];

forall_literals(it, bv)
for(const literalt &literal : bv)
{
literalt l=*it;

if(l==const_literal(false))
if(literal==const_literal(false))
continue;

BDD v(*bdd_variable_map[l.var_no()]);
if(l.sign()) v = ~v;
BDD v(*bdd_variable_map[literal.var_no()]);
if(literal.sign())
v=~v;

orbdd |= v;
orbdd|=v;
}

return nl;
Expand All @@ -420,23 +435,19 @@ void qbf_bdd_coret::compress_certificate(void)
{
status() << "Compressing Certificate" << eom;

for(quantifierst::const_iterator it=quantifiers.begin();
it!=quantifiers.end();
it++)
for(const quantifiert& quantifier : quantifiers)
{
if(it->type==quantifiert::EXISTENTIAL)
if(quantifier.type==quantifiert::EXISTENTIAL)
{
const BDD &var=*bdd_variable_map[it->var_no];
const BDD &model=*model_bdds[it->var_no];
const BDD &var=*bdd_variable_map[quantifier.var_no];
const BDD &model=*model_bdds[quantifier.var_no];

if(model==bdd_manager->bddOne() ||
model==bdd_manager->bddZero())
{
for(quantifierst::const_iterator it2=it;
it2!=quantifiers.end();
it2++)
for(const quantifiert &quantifier2 : quantifier)
{
BDD &model2=*model_bdds[it2->var_no];
BDD &model2=*model_bdds[quantifier2.var_no];

if(model==bdd_manager->bddZero())
model2=model2.AndAbstract(~var, var);
Expand Down Expand Up @@ -464,7 +475,7 @@ const exprt qbf_bdd_certificatet::f_get(literalt l)
{
quantifiert q;
if(!find_quantifier(l, q))
throw ("No model for unquantified variable");
throw "no model for unquantified variable";

// universal?
if(q.type==quantifiert::UNIVERSAL)
Expand All @@ -473,7 +484,7 @@ const exprt qbf_bdd_certificatet::f_get(literalt l)
variable_mapt::const_iterator it=variable_map.find(l.var_no());

if(it==variable_map.end())
throw "Variable map error";
throw "variable map error";

const exprt &sym=it->second.first;
unsigned index=it->second.second;
Expand All @@ -485,7 +496,8 @@ const exprt qbf_bdd_certificatet::f_get(literalt l)
uint_type.set(ID_width, 32);
extract_expr.copy_to_operands(from_integer(index, uint_type));

if(l.sign()) extract_expr.negate();
if(l.sign())
extract_expr.negate();

return extract_expr;
}
Expand Down Expand Up @@ -517,17 +529,17 @@ const exprt qbf_bdd_certificatet::f_get(literalt l)
model.PrintMinterm();
#endif

int* cube;
int *cube;
DdGen *generator;
// CUDD_VALUE_TYPE value;

exprt result=or_exprt();

Cudd_ForeachPrime(bdd_manager->getManager(),
model.getNode(), model.getNode(),
generator,
cube)
// Cudd_ForeachCube(bdd_manager->getManager(), model.getNode(), generator, cube, value)
Cudd_ForeachPrime(
bdd_manager->getManager(),
model.getNode(),
model.getNode(),
generator,
cube)
{
exprt prime=and_exprt();

Expand All @@ -540,7 +552,8 @@ const exprt qbf_bdd_certificatet::f_get(literalt l)

for(signed i=0; i<bdd_manager->ReadSize(); i++)
{
if(quantifiers[i].var_no==l.var_no()) break; // is this sound?
if(quantifiers[i].var_no==l.var_no())
break; // is this sound?

if(cube[i]!=2)
{
Expand All @@ -567,9 +580,10 @@ const exprt qbf_bdd_certificatet::f_get(literalt l)
final=false_exprt();
else if(result.operands().size()==1)
final=result.op0();
else final=result;
else
final=result;

function_cache[l.var_no()] = final;
function_cache[l.var_no()]=final;

if(l.sign())
return not_exprt(final);
Expand Down
8 changes: 4 additions & 4 deletions src/solvers/qbf/qbf_bdd_core.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,13 +14,13 @@ Author: CM Wintersteiger

#include "qdimacs_core.h"

class Cudd;
class BDD;
class Cudd; // NOLINT(*)
class BDD; // NOLINT(*)

class qbf_bdd_certificatet : public qdimacs_coret
class qbf_bdd_certificatet:public qdimacs_coret
{
protected:
Cudd* bdd_manager;
Cudd *bdd_manager;

typedef std::vector<BDD*> model_bddst;
model_bddst model_bdds;
Expand Down
10 changes: 3 additions & 7 deletions src/solvers/qbf/qbf_quantor.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -110,14 +110,10 @@ propt::resultt qbf_quantort::prop_solve()
write_qdimacs_cnf(out);
}

//std::string options=" --equivalences=0";
std::string options="";

// solve it
int res=system(("quantor "+qbf_tmp_file+
options+
" -o "+result_tmp_file).c_str());
assert(0 == res);
int res=system((
"quantor "+qbf_tmp_file+" -o "+result_tmp_file).c_str());
assert(0==res);

bool result=false;

Expand Down
Loading