1 #include "alloyinterpreter.h"
3 #include "signatureenc.h"
12 #include "inc_solver.h"
14 #include "cppvector.h"
18 #define ALLOYFILENAME "satune.als"
19 #define ALLOYSOLUTIONFILE "solution.sol"
21 AlloyInterpreter::AlloyInterpreter(CSolver *_solver):
24 output.open(ALLOYFILENAME);
25 if(!output.is_open()){
26 model_print("AlloyEnc:Error in opening the dump file satune.als\n");
31 AlloyInterpreter::~AlloyInterpreter(){
37 void AlloyInterpreter::dumpAllConstraints(Vector<char *> &facts){
38 output << "fact {" << endl;
39 for(uint i=0; i< facts.getSize(); i++){
40 char *cstr = facts.get(i);
43 output << "}" << endl;
47 int AlloyInterpreter::getResult(){
48 ifstream input(ALLOYSOLUTIONFILE, ios::in);
50 while(getline(input, line)){
51 if(line.find("Unsatisfiable.")== 0){
54 if(line.find("univ") == 0){
57 if(line.find("this/AbsBool<:value") == 0 || line.find("this/AbsElement<:value=") == 0){
58 const char delim [2] = ",";
59 char cline [line.size()+1];
60 strcpy ( cline, line.c_str() );
61 char *token = strtok(cline, delim);
62 while( token != NULL ) {
63 printf( " %s\n", token );
65 if (3 == sscanf(token,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%u", &i1, &i2, &i3)){
66 model_print("Signature%u = %u\n", i1, i3);
67 sigEnc.setValue(i1, i3);
69 token = strtok(NULL, delim);
76 void AlloyInterpreter::dumpFooter(){
77 output << "pred show {}" << endl;
78 output << "run show for " << sigEnc.getAlloyIntScope() << " int" << endl;
81 void AlloyInterpreter::dumpHeader(){
82 output << "open util/integer" << endl;
85 void AlloyInterpreter::compileRunCommand(char * command, size_t size){
86 snprintf(command, size, "./run.sh timeout %u java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", getTimeout(), ALLOYFILENAME, ALLOYSOLUTIONFILE);
89 string AlloyInterpreter::negateConstraint(string constr){
90 return "not ( " + constr + " )";
93 string AlloyInterpreter::encodeBooleanLogic( BooleanLogic *bl){
94 uint size = bl->inputs.getSize();
96 for (uint i = 0; i < size; i++)
97 array[i] = encodeConstraint(bl->inputs.get(i));
125 for( uint i=1; i< size; i++){
126 res += op + array[i];
132 return "not ( " + array[0] + " )";
136 return "( " + array[0] + op + array[1] + " )";
144 string AlloyInterpreter::encodeBooleanVar( BooleanVar *bv){
145 BooleanSig * boolSig = sigEnc.getBooleanSignature(bv);
146 return *boolSig + " = 1";
149 string AlloyInterpreter::processElementFunction(ElementFunction* elemFunc, ElementSig *signature){
150 FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
151 uint numDomains = elemFunc->inputs.getSize();
152 ASSERT(numDomains > 1);
153 ElementSig *inputs[numDomains];
155 for (uint i = 0; i < numDomains; i++) {
156 Element *elem = elemFunc->inputs.get(i);
157 inputs[i] = sigEnc.getElementSignature(elem);
158 if(elem->type == ELEMFUNCRETURN){
159 result += processElementFunction((ElementFunction *) elem, inputs[i]);
163 switch(function->op){
173 result += *signature + " = " + *inputs[0];
174 for (uint i = 1; i < numDomains; i++) {
175 result += op + "["+ *inputs[i] +"]";
181 string AlloyInterpreter::operatorPredicateConstraint(CompOp op, ElementSig *elemSig1, ElementSig *elemSig2){
184 return *elemSig1 + " = " + *elemSig2;
186 return *elemSig1 + " < " + *elemSig2;
188 return *elemSig1 + " > " + *elemSig2;