1 #include "alloyinterpreter.h"
3 #include "signatureenc.h"
12 #include "inc_solver.h"
14 #include "cppvector.h"
19 #define ALLOYFILENAME "satune.als"
20 #define ALLOYSOLUTIONFILE "solution.sol"
22 AlloyInterpreter::AlloyInterpreter(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 AlloyInterpreter::~AlloyInterpreter() {
33 if (output.is_open()) {
38 ValuedSignature *AlloyInterpreter::getBooleanSignature(uint id) {
39 return new AlloyBoolSig(id);
42 ValuedSignature *AlloyInterpreter::getElementSignature(uint id, Signature *ssig) {
43 return new AlloyElementSig(id, ssig);
46 Signature *AlloyInterpreter::getSetSignature(uint id, Set *set) {
47 return new AlloySetSig(id, set);
50 void AlloyInterpreter::dumpAllConstraints(Vector<char *> &facts) {
51 output << "fact {" << endl;
52 for (uint i = 0; i < facts.getSize(); i++) {
53 char *cstr = facts.get(i);
56 output << "}" << endl;
60 int AlloyInterpreter::getResult() {
61 ifstream input(ALLOYSOLUTIONFILE, ios::in);
63 while (getline(input, line)) {
64 if (line.find("Unsatisfiable.") == 0) {
67 if (line.find("univ") == 0) {
70 if (line.find("this/AbsBool<:value") == 0 || line.find("this/AbsElement<:value=") == 0) {
71 const char delim [2] = ",";
72 char cline [line.size() + 1];
73 strcpy ( cline, line.c_str() );
74 char *token = strtok(cline, delim);
75 while ( token != NULL ) {
77 if (3 == sscanf(token,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%u", &i1, &i2, &i3)) {
78 model_print("Signature%u = %u\n", i1, i3);
79 sigEnc.setValue(i1, i3);
81 token = strtok(NULL, delim);
89 int AlloyInterpreter::getAlloyIntScope() {
90 double mylog = log2(sigEnc.getMaxValue() + 1);
91 return floor(mylog) == mylog ? (int)mylog + 1 : (int)mylog + 2;
94 void AlloyInterpreter::dumpFooter() {
95 output << "pred show {}" << endl;
96 output << "run show for " << getAlloyIntScope() << " int" << endl;
99 void AlloyInterpreter::dumpHeader() {
100 output << "open util/integer" << endl;
103 void AlloyInterpreter::compileRunCommand(char *command, size_t size) {
104 model_print("Calling Alloy...\n");
105 snprintf(command, size, "./run.sh timeout %u java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", getTimeout(), ALLOYFILENAME, ALLOYSOLUTIONFILE);
108 string AlloyInterpreter::negateConstraint(string constr) {
109 return "not ( " + constr + " )";
112 string AlloyInterpreter::encodeBooleanLogic( BooleanLogic *bl) {
113 uint size = bl->inputs.getSize();
115 for (uint i = 0; i < size; i++)
116 array[i] = encodeConstraint(bl->inputs.get(i));
144 for ( uint i = 1; i < size; i++) {
145 res += op + array[i];
151 return "not ( " + array[0] + " )";
155 return "( " + array[0] + op + array[1] + " )";
163 string AlloyInterpreter::encodeBooleanVar( BooleanVar *bv) {
164 ValuedSignature *boolSig = sigEnc.getBooleanSignature(bv);
165 return *boolSig + " = 1";
168 string AlloyInterpreter::processElementFunction(ElementFunction *elemFunc, ValuedSignature *signature) {
169 FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
170 uint numDomains = elemFunc->inputs.getSize();
171 ASSERT(numDomains > 1);
172 ValuedSignature *inputs[numDomains];
174 for (uint i = 0; i < numDomains; i++) {
175 Element *elem = elemFunc->inputs.get(i);
176 inputs[i] = sigEnc.getElementSignature(elem);
177 if (elem->type == ELEMFUNCRETURN) {
178 result += processElementFunction((ElementFunction *) elem, inputs[i]);
182 switch (function->op) {
192 result += *signature + " = " + *inputs[0];
193 for (uint i = 1; i < numDomains; i++) {
194 result += op + "[" + *inputs[i] + "]";
200 string AlloyInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2) {
203 return *elemSig1 + " = " + *elemSig2;
205 return *elemSig1 + " < " + *elemSig2;
207 return *elemSig1 + " > " + *elemSig2;