#include "csolver.h"
#include "hashset.h"
#include "cppvector.h"
-
+#include <dirent.h>
+#include <string>
+#include <sstream>
+#include "common.h"
+using namespace std;
const char * assertstart = "ASSERTSTART";
const char * assertend = "ASSERTEND";
const char * satstart = "SATSTART";
char * readuntilend(const char * token);
BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset);
void processEquality(char * constraint, int &offset);
+void dumpSMTproblem(string &smtProblem, long long id);
+void renameDumpFile(const char *path, long long id);
+void addASSERTConstraintToSMTProblem(string & smtProblem, char * assert);
+void addSATConstraintToSMTProblem(string &smtProblem, char * sat);
+void createSATtuneDumps (char *assert, char *sat, long long &smtID);
std::ifstream * file;
Order * order;
}
typedef Hashset<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashsetIW;
-
+typedef SetIterator<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashsetIWIterator;
class OrderRec {
public:
OrderRec() : set (NULL), value(-1), alloced(false) {
Vector<OrderRec*> * orderRecVector = NULL;
HashtableIW * ordertable = NULL;
HashtableBV * vartable = new HashtableBV();
+HashsetIW * intSet = new HashsetIW();
+HashsetIW * boolSet = new HashsetIW();
void cleanAndFreeOrderRecVector(){
for(uint i=0; i< orderRecVector->getSize(); i++){
file = new std::ifstream(argv[1]);
char * assert = NULL;
char * sat = NULL;
+ string smtProblem = "";
+ long long smtID=0L;
Vector<OrderRec*> orderRecs;
orderRecVector = &orderRecs;
while(true) {
if (assert != NULL){
free(assert);
assert = NULL;
+ dumpSMTproblem(smtProblem, smtID);
+ smtProblem = "";
+ intSet->reset();
+ boolSet->reset();
}
assert = readuntilend(assertend);
+ addASSERTConstraintToSMTProblem(smtProblem, assert);
+ //cout << "INFO: SMTProblem After adding ASSERT Constraints\n" << smtProblem << "\n&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&\n";
printf("[%s]\n", assert);
} else if (retval == 2) {
if (sat != NULL) {
ordertable = new HashtableIW();
}
sat = readuntilend(satend);
- CSolver *solver = new CSolver();
- solver->turnoffOptimizations();
- set = solver->createMutableSet(1);
- order = solver->createOrder(SATC_TOTAL, (Set *) set);
- int offset = 0;
- processEquality(sat, offset);
- offset = 0;
- processEquality(assert, offset);
- offset = 0;
- solver->addConstraint(parseConstraint(solver, sat, offset));
- offset = 0;
- solver->addConstraint(parseConstraint(solver, assert, offset));
- printf("[%s]\n", sat);
- solver->finalizeMutableSet(set);
- solver->serialize();
- solver->printConstraints();
- delete solver;
+ createSATtuneDumps(assert, sat, smtID);
+ addSATConstraintToSMTProblem(smtProblem, sat);
+ //cout << "INFO: SMTProblem After adding SAT Constraints\n" << smtProblem << "\n&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&\n";
}
}
-
+
+ if(smtID == 0L){
+ char trueString [] = "true";
+ ordertable = new HashtableIW();
+ createSATtuneDumps(assert, trueString, smtID);
+ addSATConstraintToSMTProblem(smtProblem, trueString);
+ }
+ dumpSMTproblem(smtProblem, smtID);
cleanAndFreeOrderRecVector();
if(ordertable != NULL){
delete ordertable;
delete file;
}
+void createSATtuneDumps (char *assert, char *sat, long long &smtID){
+ CSolver *solver = new CSolver();
+ solver->turnoffOptimizations();
+ set = solver->createMutableSet(1);
+ order = solver->createOrder(SATC_TOTAL, (Set *) set);
+ int offset = 0;
+ processEquality(sat, offset);
+ offset = 0;
+ processEquality(assert, offset);
+ offset = 0;
+ solver->addConstraint(parseConstraint(solver, sat, offset));
+ offset = 0;
+ solver->addConstraint(parseConstraint(solver, assert, offset));
+ printf("[%s]\n", sat);
+ solver->finalizeMutableSet(set);
+ solver->serialize();
+ solver->printConstraints();
+ smtID= getTimeNano();
+ renameDumpFile("./", smtID);
+ delete solver;
+}
+
+void doExit(const char * message){
+ printf("%s", message);
+ exit(-1);
+}
+
+void doExit() {
+ doExit("Parse Error\n");
+}
+
+void renameDumpFile(const char *path, long long id) {
+ struct dirent *entry;
+ DIR *dir = opendir(path);
+ if (dir == NULL) {
+ return;
+ }
+ char newname[128] ={0};
+ sprintf(newname, "%lld.dump", id);
+ bool duplicate = false;
+ while ((entry = readdir(dir)) != NULL) {
+ if(strstr(entry->d_name, "DUMP") != NULL){
+ if(duplicate){
+ doExit("Multiplle DUMP file exists. Make sure to clean them all before running the program");
+ }
+ int result= rename( entry->d_name , newname );
+ if ( result == 0 )
+ printf ( "File successfully renamed to %s\n" , newname);
+ else
+ doExit( "Error renaming file" );
+ duplicate = true;
+ }
+ }
+ closedir(dir);
+}
+template <class MyType>
+string to_string(MyType value){
+ string number;
+ std::stringstream strstream;
+ strstream << value;
+ strstream >> number;
+ return number;
+}
+
+void dumpDeclarations(std::ofstream& smtfile){
+ HashsetIWIterator* iterator = intSet->iterator();
+ smtfile << "(set-logic QF_LRA)" << endl;
+ while(iterator->hasNext()){
+ intwrapper * iw = iterator->next();
+ string declare = "(declare-const O!"+ to_string<uint32_t>(iw->value) + " Real)\n";
+ smtfile << declare;
+ }
+ delete iterator;
+
+ iterator = boolSet->iterator();
+ while(iterator->hasNext()){
+ intwrapper * iw = iterator->next();
+ string declare = "(declare-const S!" + to_string<uint32_t>(iw->value) + " Bool)\n";
+ smtfile << declare;
+ }
+ delete iterator;
+}
+
+void addASSERTConstraintToSMTProblem(string & smtProblem, char * assert){
+ string ssat(assert);
+ string assertStatement = "(assert "+ ssat + "\n)\n";
+ smtProblem += assertStatement;
+}
+
+void addSATConstraintToSMTProblem(string &smtProblem, char * sat){
+ string ssat(sat);
+ string satStatement = "(push)\n(assert "+ ssat + "\n)\n(check-sat)\n(get-model)\n(pop)\n";
+ smtProblem += satStatement;
+}
+
+
+void dumpSMTproblem(string &smtProblem, long long id){
+ std::ofstream smtfile;
+ string smtfilename = to_string<long long>(id) + ".smt";
+ smtfile.open (smtfilename.c_str());
+ if(!smtfile.is_open())
+ {
+ doExit("Unable to create file.\n");
+ }
+ dumpDeclarations(smtfile);
+ smtfile << smtProblem;
+ smtfile.close();
+ cout <<"************here is the SMT file*********" << endl << smtProblem <<endl << "****************************" << endl;;
+}
+
+
void skipwhitespace(char * constraint, int & offset) {
//skip whitespace
while (constraint[offset] == ' ' || constraint[offset] == '\n')
offset++;
}
-void doExit() {
- printf("PARSE ERROR\n");
- exit(-1);
-}
-
int32_t getOrderVar(char *constraint, int & offset) {
if (constraint[offset++] != 'O' || constraint[offset++] != '!' ) {
doExit();
}
int32_t getBooleanVar(char *constraint, int & offset) {
- if (constraint[offset++] != 'S' || constraint[offset++] != '!' ) {
- doExit();
- }
+ if (constraint[offset++] != 'S' || constraint[offset++] != '!' ) {
+ cout << "Constraint= " << constraint << "\toffset=" << constraint[offset - 1] << " ******\n";
+ doExit();
+ }
int32_t num = 0;
while(true) {
char next = constraint[offset];
skipwhitespace(constraint, offset);
getOrderVar(constraint, offset);
skipwhitespace(constraint, offset);
- if (constraint[offset++] != ')')
- doExit();
+ if (constraint[offset++] != ')'){
+ doExit();
+ }
return;
} else if (strncmp(&constraint[offset], "(=", 2) == 0) {
offset+=2;
skipwhitespace(constraint, offset);
int v1=getOrderVar(constraint, offset);
+ intwrapper iwv1(v1);
+ if(intSet->get(&iwv1) == NULL){
+ intSet->add(new intwrapper(v1));
+ }
skipwhitespace(constraint, offset);
int v2=getOrderVar(constraint, offset);
+ intwrapper iwv2(v2);
+ if(intSet->get(&iwv2) == NULL){
+ intSet->add(new intwrapper(v2));
+ }
skipwhitespace(constraint, offset);
if (constraint[offset++] != ')')
doExit();
mergeVars(v1, v2);
return;
- } else {
- getBooleanVar(constraint, offset);
- skipwhitespace(constraint, offset);
- return;
+ } else if (strncmp(&constraint[offset], "tr", 2) == 0){
+ offset+=4;
+ skipwhitespace(constraint, offset);
+ return;
+ }
+ else{
+ int32_t b1 = getBooleanVar(constraint, offset);
+ intwrapper iwb1(b1);
+ if(boolSet->get(&iwb1) == NULL){
+ boolSet->add(new intwrapper(b1));
+ }
+ skipwhitespace(constraint, offset);
+return;
}
}
offset+=2;
skipwhitespace(constraint, offset);
int32_t v1 = getOrderVar(constraint, offset);
+ intwrapper iwv1(v1);
+ if(intSet->get(&iwv1) == NULL){
+ intSet->add(new intwrapper(v1));
+ }
skipwhitespace(constraint, offset);
int32_t v2 = getOrderVar(constraint, offset);
+ intwrapper iwv2(v2);
+ if(intSet->get(&iwv2) == NULL){
+ intSet->add(new intwrapper(v2));
+ }
skipwhitespace(constraint, offset);
if (constraint[offset++] != ')')
doExit();
if (constraint[offset++] != ')')
doExit();
return solver->getBooleanTrue();
- } else {
+ }else if (strncmp(&constraint[offset], "tr", 2) == 0){
+ offset+=4;
+ skipwhitespace(constraint, offset);
+ return solver->getBooleanTrue();
+ }
+ else {
int32_t v = getBooleanVar(constraint, offset);
+ intwrapper iwb1(v);
+ if(boolSet->get(&iwb1) == NULL){
+ boolSet->add(new intwrapper(v));
+ }
skipwhitespace(constraint, offset);
return checkBooleanVar(solver, v);
}
projects / satune.git / blobdiff