Jump to content

Welcome to Geeks to Go - Register now for FREE

Geeks To Go is a helpful hub, where thousands of volunteer geeks quickly serve friendly answers and support. Check out the forums and get free advice from the experts. Register now to gain access to all of our features, it's FREE and only takes one minute. Once registered and logged in, you will be able to create topics, post replies to existing threads, give reputation to your fellow members, get your own private messenger, post status updates, manage your profile and so much more.

Create Account How it Works
Photo

C++ Help


  • Please log in to reply

#1
Javier

Javier

    New Member

  • Member
  • Pip
  • 8 posts
Im a beginner trying to write a SAT program but get a segmentation fault error.
I cant figure out what the problem is. Its almost like a character vs. a string problem.
can anyone help. here is the code. sorry about the couts i ws truoble shooting. Input file should look something li this: x y z $ x !y p $ z y z $$. Where the formula is in Conjunctive normal form, $ seperates clauses and $$ indicates end of formula. So the above input would really be: ((x OR y OR z)AND (x OR NOTy OR p)AND (z OR y OR z)). If anyone can help that would be great!.



#include <iostream>
#include <vector>
#include <string>
#include <cctype>

using namespace std;

class atom
{
public:
string variable;
bool form;
atom();
atom (string,bool);
bool operator == (atom);
};



class clause
{
vector<atom> atoms;
public:
bool contains(atom);
void insert(atom);
void remove(atom);
bool empty();
};

class formula
{
vector<clause> clauses;
vector<string> variables;
vector<atom> values;
public:
void remove(atom);
bool satisfiable();
void pure();
formula();
formula(formula & f, atom a);
};

int main() //do i need Bool since it is returning true or false??
{
cout << "entering main" << endl;
formula f; // declare a formula variable

if(f.satisfiable())
{
cout <<"marker 200"<< endl;
return true;
}
else
{
cout << "exiting main" << endl;
return false;
}
}
atom:: atom (string s, bool b)
{
cout << "entering atom:: atom" << endl;

variable = s;
form = b;
cout << "exiting atom:: atom" << endl;
}

atom:: atom()
{
cout<< "entering /exiting atom::atom()" <<endl;
}

bool atom:: operator==(atom a)
{
cout << "entering atom:: operator" << endl;
if(a.variable == variable && a.form == form)
return true;

cout << "exiting atom:: operator" << endl;
return false;
}

bool clause:: contains(atom a)
{
cout << "entering clause :: contains" << endl;
for(int i=0;i < atoms.size(); ++i)
if(atoms[i]==a)
{
cout <<" in clause:: contains"<< endl;
return true;
}
{
cout << "exiting clause :: contains" << endl;
return false;
}
}

void clause:: insert(atom a)
{
cout <<"entering clause:: insert" << endl;
atoms.push_back(a);
cout <<"exiting clause:: insert" << endl;
}

void clause:: remove(atom a)
{
cout <<"entering clause:: remove" << endl;
for(vector<atom>::iterator i = atoms.begin(); i != atoms.end(); ++i)
if(*i == a)
atoms.erase(i);
cout <<"exiting clause:: remove" << endl;
}

bool clause:: empty()
{
cout<< "entering clause:: empty"<< endl;

cout <<"exiting clause:: empty"<< endl;
return atoms.empty();
}
void formula:: remove(atom a)
{
cout << "entering formula:: remove" << endl;
for(int i=clauses.size()-1;i>=0;i--)
if(clauses[i].contains(a))
clauses.erase(clauses.begin()+i);
a.form=!a.form;
for(int i=0;i<clauses.size();i++)
if(clauses[i].contains(a))
clauses[i].remove(a);
cout << "exiting formula:: remove" << endl;
}



formula:: formula()
{
cout << "entering formula()" << endl;
string s("");
clause* c=new clause();

for(int i = 0;s != string("$$"); ++i)
{

cin >> s; // reads a string

{
if(s == string("$$"))

{
cout<< "if $$" << endl;
return;
}
if(s == string("$"))
{
clauses.push_back(*c); // stores clause in
c=new clause();
cout<< "if $" << endl;
}
if(s[0]=='!')// creates an atom
{
s.erase(s.begin());

cout<< "if!" << endl;
c->insert(atom(s,false));

}
else
{
c->insert(atom(s,true)); //stores atom in clause c.
cout << "exiting formula()" << endl;
}
}
}
}

formula:: formula(formula &f, atom a)
{
cout << "entering formula:: formula" << endl;
clauses = f.clauses;
variables = f.variables;
values = f.values;

remove(a);
cout << "exiting formula:: formula" << endl;
}



void formula:: pure()
{
cout << "entering formula:: pure" << endl;
for(vector<string>::iterator i = variables.begin();i != variables.end();++i)
{
atom w1(*i,true);
atom w2(*i,false);
atom t;
bool pf=false, nf=false;
for(vector<clause>::iterator j = clauses.begin();j != clauses.end();++j)
{
if((*j).contains(w1))
pf = true;
if((*j).contains(w2))
nf = true;
t = (pf ?w1:w2);// whqat does this do agian?
}
if(!(pf && nf))
{
for(vector<clause>::iterator j = clauses.begin();j != clauses.end();++j)

if((*j).contains(t) )
clauses.erase(j);
}
}
cout << "exiting formula :: pure" << endl;
}

bool formula::satisfiable()
{

cout << "entering formula::satisfiable" << endl;
// call pure, declare 2 variables F1, F2.
// check if its empty.
// create formula F1 and F2
// If either F1 or F2 is satisfiable, return True


pure();
if(clauses.empty())
return true;
cout<< "marker0"<< endl;

//CAN YOU CHEK HERE!!!!!!!!!!
for(vector<clause>::iterator i= clauses.begin(); i != clauses.end();++i)

if((*i).empty())

{
cout << "marker1"<< endl;
return false;
}
//cout << "marker2" << endl;
atom p(variables[0],true);
//cout << "100" <<endl;
atom q(variables[0],false);
//cout << "101" << endl;
variables.erase(variables.begin());
//cout << "102" << endl;
formula F1(*this,p);
//cout << "103" << endl;
formula F2(*this,q);


if(F1.satisfiable())
{
cout<< "105" << endl;
return true;
}
if(F2.satisfiable())
{
cout << "106" << endl;
return true;
}
else
{
cout << "exiting formula :: satisfiable" << endl;
return false;
}
}
  • 0

Advertisements







Similar Topics

0 user(s) are reading this topic

0 members, 0 guests, 0 anonymous users

As Featured On:

Microsoft Yahoo BBC MSN PC Magazine Washington Post HP