#include <dirent.h>
#include <string>
#include <sstream>
+#include <sstream>
+#include <string.h>
#include "common.h"
+
using namespace std;
const char * assertstart = "ASSERTSTART";
const char * assertend = "ASSERTEND";
const char * satstart = "SATSTART";
const char * satend = "SATEND";
+const char * varstart = "VARSTART";
+const char * varend = "VAREND";
-int skipahead(const char * token1, const char * token2);
+int skipahead(const char * token1, const char * token2, const char * token3);
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 addVarConstraintToSMTProblem(string & smtProblem, Vector<char *> & varconstraint);
void addSATConstraintToSMTProblem(string &smtProblem, char * sat);
-void createSATtuneDumps (char *assert, char *sat, long long &smtID);
+void createSATtuneDumps (char *assert, char *sat, Vector<char *> & varconstraints, long long &smtID);
std::ifstream * file;
Order * order;
MutableSet * set;
+bool incremental = true;
class intwrapper {
public:
intwrapper(int _val) : value(_val) {
int main(int numargs, char ** argv) {
file = new std::ifstream(argv[1]);
+ if(numargs > 2){
+ incremental = false;
+ }
char * assert = NULL;
char * sat = NULL;
+ char * var = NULL;
+ Vector<char *> varconstraints;
string smtProblem = "";
long long smtID=0L;
Vector<OrderRec*> orderRecs;
orderRecVector = &orderRecs;
while(true) {
- int retval = skipahead(assertstart, satstart);
- printf("%d\n", retval);
+ int retval = skipahead(assertstart, satstart, varstart);
+ //printf("%d\n", retval);
if (retval == 0){
break;
}
assert = NULL;
dumpSMTproblem(smtProblem, smtID);
smtProblem = "";
+ for(uint i=0; i< varconstraints.getSize(); i++){
+ free(varconstraints.get(i));
+ }
+ varconstraints.clear();
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);
+ //printf("[%s]\n", assert);
} else if (retval == 2) {
if (sat != NULL) {
free(sat);
cleanAndFreeOrderRecVector();
} else {
ordertable = new HashtableIW();
+ addVarConstraintToSMTProblem(smtProblem, varconstraints);
}
sat = readuntilend(satend);
- createSATtuneDumps(assert, sat, smtID);
+ createSATtuneDumps(assert, sat, varconstraints, smtID);
addSATConstraintToSMTProblem(smtProblem, sat);
+ if(!incremental){
+ dumpSMTproblem(smtProblem, smtID);
+ }
//cout << "INFO: SMTProblem After adding SAT Constraints\n" << smtProblem << "\n&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&\n";
+ } else if (retval == 3) {
+ var = readuntilend(varend);
+ varconstraints.push(var);
}
}
if(smtID == 0L){
char trueString [] = "true";
ordertable = new HashtableIW();
- createSATtuneDumps(assert, trueString, smtID);
+ createSATtuneDumps(assert, trueString, varconstraints, smtID);
addSATConstraintToSMTProblem(smtProblem, trueString);
}
- dumpSMTproblem(smtProblem, smtID);
+ if(incremental){
+ dumpSMTproblem(smtProblem, smtID);
+ }
cleanAndFreeOrderRecVector();
if(ordertable != NULL){
delete ordertable;
delete file;
}
-void createSATtuneDumps (char *assert, char *sat, long long &smtID){
+void createSATtuneDumps (char *assert, char *sat, Vector<char *> & varconstraints, long long &smtID){
CSolver *solver = new CSolver();
- solver->turnoffOptimizations();
+// solver->turnoffOptimizations();
set = solver->createMutableSet(1);
order = solver->createOrder(SATC_TOTAL, (Set *) set);
int offset = 0;
solver->addConstraint(parseConstraint(solver, sat, offset));
offset = 0;
solver->addConstraint(parseConstraint(solver, assert, offset));
- printf("[%s]\n", sat);
+ for(uint i=0; i<varconstraints.getSize(); i++){
+ offset = 0;
+ processEquality(varconstraints.get(i),offset);
+ offset = 0;
+ solver->addConstraint(parseConstraint(solver, varconstraints.get(i), offset));
+ }
+ //printf("[%s]\n", sat);
solver->finalizeMutableSet(set);
solver->serialize();
- solver->printConstraints();
+ //solver->printConstraints();
smtID= getTimeNano();
renameDumpFile("./", smtID);
+ //solver->solve();
delete solver;
}
delete iterator;
}
+
+void addVarConstraintToSMTProblem(string & smtProblem, Vector<char *> & varconstraints){
+ for(uint i=0; i<varconstraints.getSize(); i++){
+ //cout << "[ " << varconstraints.get(i) << " ]" << endl;
+ smtProblem += "(assert "+ string(varconstraints.get(i)) +")\n";
+ }
+}
+
void addASSERTConstraintToSMTProblem(string & smtProblem, char * assert){
string ssat(assert);
string assertStatement = "(assert "+ ssat + "\n)\n";
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";
+ string satStatement;
+ if(incremental){
+ satStatement = "(push)\n(assert "+ ssat + "\n)\n(check-sat)\n(pop)\n";
+ } else {
+ satStatement = "(assert "+ ssat + "\n)\n(check-sat)\n";
+ }
smtProblem += satStatement;
}
int32_t getBooleanVar(char *constraint, int & offset) {
if (constraint[offset++] != 'S' || constraint[offset++] != '!' ) {
- cout << "Constraint= " << constraint << "\toffset=" << constraint[offset - 1] << " ******\n";
+ cout << "Constraint= " << constraint << "\tconstraint[offset=" << offset - 1 << "]" << &constraint[offset -1] <<"\n";
doExit();
}
int32_t num = 0;
return rec->value;
}
+void processLetExpression (char * constraint){
+ int constrSize = strlen(constraint);
+ char * replace = (char *) malloc(constrSize);
+ for (int i=0; i< constrSize; i++){
+ replace[i] = 0;
+ }
+ int offset = 1;
+ offset +=4;
+ skipwhitespace(constraint, offset);
+ ASSERT(strncmp(&constraint[offset], "((a!1",5) == 0);
+ offset +=5;
+ skipwhitespace(constraint, offset);
+ int startOffset = offset;
+ processEquality(constraint, offset);
+ strncpy(replace, &constraint[startOffset], offset-startOffset);
+ while(constraint[offset] == ')')
+ offset++;
+ skipwhitespace(constraint, offset);
+ string modified = "";
+ while(offset < constrSize){
+ bool done = false;
+ while(strncmp(&constraint[offset], "a!1",3) != 0){
+ modified += constraint[offset++];
+ if(offset >= constrSize -2){ //Not considering ) and \n ...
+ ASSERT(constraint[constrSize-1] == '\n');
+ ASSERT(constraint[constrSize-2] == ')');
+ done = true;
+ break;
+ }
+ }
+ if(done){
+ break;
+ }
+ offset += 3;
+ modified += replace;
+ }
+ strcpy(constraint, modified.c_str());
+ cout << "modified:*****" << modified << "****\n";
+ free(replace);
+}
+
void processEquality(char * constraint, int &offset) {
skipwhitespace(constraint, offset);
if (strncmp(&constraint[offset], "(and",4) == 0) {
}
processEquality(constraint, offset);
}
+ } else if (strncmp(&constraint[offset], "(or",3) == 0) {
+ offset +=3;
+ Vector<BooleanEdge> vec;
+ while(true) {
+ skipwhitespace(constraint, offset);
+ if (constraint[offset] == ')') {
+ offset++;
+ return;
+ }
+ processEquality(constraint, offset);
+ }
+ } else if (strncmp(&constraint[offset], "(let",4) == 0){
+ ASSERT(offset == 1);
+ cout << "Before: " << constraint << endl;
+ processLetExpression(constraint);
+ cout << "After: " << constraint << endl;
+ offset=0;
+ processEquality(constraint, offset);
+ } else if (strncmp(&constraint[offset], "(=>",3) == 0){
+ offset +=3;
+ skipwhitespace(constraint, offset);
+ processEquality(constraint, offset);
+ skipwhitespace(constraint, offset);
+ processEquality(constraint, offset);
+ skipwhitespace(constraint, offset);
+ if (constraint[offset++] != ')'){
+ doExit();
+ }
+ return;
} else if (strncmp(&constraint[offset], "(<", 2) == 0) {
offset+=2;
skipwhitespace(constraint, offset);
}
vec.push(parseConstraint(solver, constraint, offset));
}
+ } else if (strncmp(&constraint[offset], "(or", 3) == 0) {
+ offset +=3;
+ Vector<BooleanEdge> vec;
+ while(true) {
+ skipwhitespace(constraint, offset);
+ if (constraint[offset] == ')') {
+ offset++;
+ return solver->applyLogicalOperation(SATC_OR, vec.expose(), vec.getSize());
+ }
+ vec.push(parseConstraint(solver, constraint, offset));
+ }
+ } else if (strncmp(&constraint[offset], "(=>", 3) == 0){
+ offset += 3;
+ skipwhitespace(constraint, offset);
+ BooleanEdge b1 = parseConstraint(solver, constraint, offset);
+ skipwhitespace(constraint, offset);
+ BooleanEdge b2 = parseConstraint(solver, constraint, offset);
+ skipwhitespace(constraint, offset);
+ if (constraint[offset++] != ')')
+ doExit();
+ return solver->applyLogicalOperation(SATC_IMPLIES, b1, b2);
} else if (strncmp(&constraint[offset], "(<", 2) == 0) {
offset+=2;
skipwhitespace(constraint, offset);
skipwhitespace(constraint, offset);
if (constraint[offset++] != ')')
doExit();
+// int32_t o1 = checkordervar(solver, v1);
+// int32_t o2 = checkordervar(solver, v2);
+// cout << "V1=" << v1 << ",V2=" << v2 << ",O1=" << o1 << ",O2=" << o2<< endl;
+// ASSERT( o1 != o2);
return solver->orderConstraint(order, checkordervar(solver, v1), checkordervar(solver, v2));
} else if (strncmp(&constraint[offset], "(=", 2) == 0) {
offset+=2;
}
}
-int skipahead(const char * token1, const char * token2) {
- int index1 = 0, index2 = 0;
+int skipahead(const char * token1, const char * token2, const char * token3) {
+ int index1 = 0, index2 = 0, index3 = 0;
char buffer[256];
while(true) {
if (token1[index1] == 0)
return 1;
if (token2[index2] == 0)
return 2;
+ if (token3[index3] == 0)
+ return 3;
if (file->eof())
return 0;
file->read(buffer, 1);
index2++;
else
index2 = 0;
+ if (buffer[0] == token3[index3])
+ index3++;
+ else
+ index3 = 0;
}
}
projects / satune.git / blobdiff