3 #include "signatureenc.h"
12 #include "inc_solver.h"
18 const char * AlloyEnc::alloyFileName = "satune.als";
19 const char * AlloyEnc::solutionFile = "solution.sol";
21 AlloyEnc::AlloyEnc(CSolver *_solver):
25 output.open(alloyFileName);
26 if(!output.is_open()){
27 model_print("AlloyEnc:Error in opening the dump file satune.als\n");
32 AlloyEnc::~AlloyEnc(){
38 void AlloyEnc::encode(){
40 SetIteratorBooleanEdge *iterator = csolver->getConstraints();
42 while(iterator->hasNext()){
43 BooleanEdge constraint = iterator->next();
44 string constr = encodeConstraint(constraint);
45 char *cstr = new char [constr.length()+1];
46 strcpy (cstr, constr.c_str());
49 output << "fact {" << endl;
50 for(uint i=0; i< facts.getSize(); i++){
51 char *cstr = facts.get(i);
55 output << "}" << endl;
59 void tokenize(string const &str, const char delim, vector<std::string> &out)
64 while ((start = str.find_first_not_of(delim, end)) != string::npos)
66 end = str.find(delim, start);
67 out.push_back(str.substr(start, end - start));
71 int AlloyEnc::getResult(){
72 ifstream input(solutionFile, ios::in);
74 while(getline(input, line)){
75 if(line.find("Unsatisfiable.")== 0){
78 if(line.find("univ") == 0){
81 if(line.find("this/AbsBool<:value") == 0 || line.find("this/AbsElement<:value=") == 0){
82 vector<string> values;
83 const char delim = ',';
84 tokenize(line, delim, values);
85 for (uint i=0; i<values.size(); i++){
87 if (3 == sscanf(values[i].c_str(),"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%u", &i1, &i2, &i3)){
88 model_print("Signature%u = %u\n", i1, i3);
89 sigEnc.setValue(i1, i3);
97 void AlloyEnc::dumpAlloyFooter(){
98 output << "pred show {}" << endl;
99 output << "run show for " << sigEnc.getAlloyIntScope() << " int" << endl;
102 uint AlloyEnc::getTimeout(){
103 uint timeout =csolver->getSatSolverTimeout();
104 return timeout == (uint)NOTIMEOUT? 1000: timeout;
107 void AlloyEnc::dumpAlloyHeader(){
108 output << "open util/integer" << endl;
111 int AlloyEnc::solve(){
113 int result = IS_INDETER;
115 if( output.is_open()){
118 snprintf(buffer, sizeof(buffer), "./run.sh timeout %u java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", getTimeout(), alloyFileName, solutionFile);
119 int status = system(buffer);
121 //Read data in from results file
122 result = getResult();
127 string AlloyEnc::encodeConstraint(BooleanEdge c){
128 Boolean *constraint = c.getBoolean();
130 switch(constraint->type){
132 res = encodeBooleanLogic((BooleanLogic *) constraint);
136 res = encodePredicate((BooleanPredicate *) constraint);
140 res = encodeBooleanVar( (BooleanVar *) constraint);
147 return "not ( " + res + " )";
152 string AlloyEnc::encodeBooleanLogic( BooleanLogic *bl){
153 uint size = bl->inputs.getSize();
155 for (uint i = 0; i < size; i++)
156 array[i] = encodeConstraint(bl->inputs.get(i));
184 for( uint i=1; i< size; i++){
185 res += op + array[i];
191 return "not ( " + array[0] + " )";
195 return "( " + array[0] + op + array[1] + " )";
203 string AlloyEnc::encodePredicate( BooleanPredicate *bp){
204 switch (bp->predicate->type) {
208 return encodeOperatorPredicate(bp);
214 string AlloyEnc::encodeBooleanVar( BooleanVar *bv){
215 BooleanSig * boolSig = sigEnc.getBooleanSignature(bv);
216 return *boolSig + " = 1";
219 string AlloyEnc::processElementFunction(ElementFunction* elemFunc, ElementSig *signature){
220 FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
221 uint numDomains = elemFunc->inputs.getSize();
222 ASSERT(numDomains > 1);
223 ElementSig *inputs[numDomains];
225 for (uint i = 0; i < numDomains; i++) {
226 Element *elem = elemFunc->inputs.get(i);
227 inputs[i] = sigEnc.getElementSignature(elem);
228 if(elem->type == ELEMFUNCRETURN){
229 result += processElementFunction((ElementFunction *) elem, inputs[i]);
233 switch(function->op){
243 result += *signature + " = " + *inputs[0];
244 for (uint i = 1; i < numDomains; i++) {
245 result += op + "["+ *inputs[i] +"]";
251 string AlloyEnc::encodeOperatorPredicate(BooleanPredicate *constraint){
252 PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
253 ASSERT(constraint->inputs.getSize() == 2);
255 Element *elem0 = constraint->inputs.get(0);
256 ASSERT(elem0->type == ELEMSET || elem0->type == ELEMFUNCRETURN || elem0->type == ELEMCONST);
257 ElementSig *elemSig1 = sigEnc.getElementSignature(elem0);
258 if(elem0->type == ELEMFUNCRETURN){
259 str += processElementFunction((ElementFunction *) elem0, elemSig1);
261 Element *elem1 = constraint->inputs.get(1);
262 ASSERT(elem1->type == ELEMSET || elem1->type == ELEMFUNCRETURN || elem1->type == ELEMCONST);
263 ElementSig *elemSig2 = sigEnc.getElementSignature(elem1);
264 if(elem1->type == ELEMFUNCRETURN){
265 str += processElementFunction((ElementFunction *) elem1, elemSig2);
267 switch (predicate->getOp()) {
269 str += *elemSig1 + " = " + *elemSig2;
272 str += *elemSig1 + " < " + *elemSig2;
275 str += *elemSig1 + " > " + *elemSig2;
283 void AlloyEnc::writeToFile(string str){
284 output << str << endl;
287 bool AlloyEnc::getBooleanValue(Boolean *b){
288 return (bool)sigEnc.getValue(b);
291 uint64_t AlloyEnc::getValue(Element * element){
292 return (uint64_t)sigEnc.getValue(element);