[Javier]

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;
}
}