src/Interpreter/smtinterpreter.cc

   1 #include "smtinterpreter.h"
   2 #include <string>
   3 #include "signatureenc.h"
   4 #include "structs.h"
   5 #include "csolver.h"
   6 #include "boolean.h"
   7 #include "predicate.h"
   8 #include "element.h"
   9 #include "set.h"
  10 #include "function.h"
  11 #include "inc_solver.h"
  12 #include <fstream>
  13 #include "cppvector.h"
  14 #include "smtsig.h"
  15
  16 using namespace std;
  17
  18 SMTInterpreter::SMTInterpreter(CSolver *_solver) :
  19         Interpreter(_solver)
  20 {
  21         output.open(SMTFILENAME);
  22         if (!output.is_open()) {
  23                 model_print("AlloyEnc:Error in opening the dump file satune.smt\n");
  24                 exit(-1);
  25         }
  26 }
  27
  28 SMTInterpreter::~SMTInterpreter() {
  29         if (output.is_open()) {
  30                 output.close();
  31         }
  32 }
  33
  34
  35 ValuedSignature *SMTInterpreter::getBooleanSignature(uint id) {
  36         return new SMTBoolSig(id);
  37 }
  38
  39 ValuedSignature *SMTInterpreter::getElementSignature(uint id, Signature *ssig) {
  40         return new SMTElementSig(id, (SMTSetSig *)ssig);
  41 }
  42
  43 Signature *SMTInterpreter::getSetSignature(uint id, Set *set) {
  44         return new SMTSetSig(id, set);
  45 }
  46
  47 void SMTInterpreter::dumpAllConstraints(Vector<char *> &facts) {
  48         for (uint i = 0; i < facts.getSize(); i++) {
  49                 char *cstr = facts.get(i);
  50                 writeToFile("(assert " + string(cstr) + ")");
  51         }
  52 }
  53
  54 void SMTInterpreter::extractValue(char *idline, char *valueline) {
  55         uint id;
  56         if (1 == sscanf(idline,"%*[^0123456789]%u", &id)) {
  57                 char valuestr [512];
  58                 ASSERT(1 == sscanf(valueline,"%s)", valuestr));
  59                 uint value;
  60                 if (strcmp (valuestr, "true)") == 0 ) {
  61                         value = 1;
  62                 } else if (strcmp(valuestr, "false)") == 0) {
  63                         value = 0;
  64                 } else {
  65                         ASSERT(1 == sscanf(valueline, "%*[^0123456789]%u", &value));
  66                 }
  67
  68                 model_print("Signature%u = %u\n", id, value);
  69                 sigEnc.setValue(id, value);
  70         } else {
  71                 ASSERT(0);
  72         }
  73 }
  74
  75 int SMTInterpreter::getResult() {
  76         ifstream input(SMTSOLUTIONFILE, ios::in);
  77         string line;
  78         while (getline(input, line)) {
  79                 if (line.find("unsat") != line.npos) {
  80                         return IS_UNSAT;
  81                 }
  82                 if (line.find("(define-fun") != line.npos || line.find("( (") != line.npos) {
  83                         string valueline;
  84                         ASSERT(getline(input, valueline));
  85                         char cline [line.size() + 1];
  86                         strcpy ( cline, line.c_str() );
  87                         char vline [valueline.size() + 1];
  88                         strcpy ( vline, valueline.c_str() );
  89                         extractValue(cline, vline);
  90                 }
  91         }
  92         return IS_SAT;
  93 }
  94
  95 void SMTInterpreter::dumpFooter() {
  96         output << "(check-sat)" << endl;
  97         output << "(get-model)" << endl;
  98 }
  99
 100 void SMTInterpreter::dumpHeader() {
 101 }
 102
 103 void SMTInterpreter::compileRunCommand(char *command, size_t size) {
 104         model_print("Calling Z3...\n");
 105         snprintf(command, size, "./run.sh z3 -T:%u -in < %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
 106 }
 107
 108 string SMTInterpreter::negateConstraint(string constr) {
 109         return "( not " + constr + " )";
 110 }
 111
 112 string SMTInterpreter::encodeBooleanLogic( BooleanLogic *bl) {
 113         uint size = bl->inputs.getSize();
 114         string array[size];
 115         for (uint i = 0; i < size; i++)
 116                 array[i] = encodeConstraint(bl->inputs.get(i));
 117         string op;
 118         switch (bl->op) {
 119         case SATC_OR:
 120                 op = "or";
 121                 break;
 122         case SATC_AND:
 123                 op = "and";
 124                 break;
 125         case SATC_NOT:
 126                 op = "not";
 127                 break;
 128         case SATC_IMPLIES:
 129                 op = "=>";
 130                 break;
 131         case SATC_XOR:
 132         default:
 133                 ASSERT(0);
 134         }
 135         switch (bl->op) {
 136         case SATC_XOR:
 137         case SATC_OR:
 138         case SATC_AND: {
 139                 ASSERT(size >= 2);
 140                 string res = array[0];
 141                 for ( uint i = 1; i < size; i++) {
 142                         res = "( " + op + " " + res + " " +  array[i] + " )";
 143                 }
 144                 return res;
 145         }
 146         case SATC_NOT: {
 147                 return "( not " + array[0] + " )";
 148         }
 149         case SATC_IMPLIES:
 150                 return "( " + op + " " + array[0] + " " + array[1] + " )";
 151         case SATC_IFF:
 152         default:
 153                 ASSERT(0);
 154
 155         }
 156 }
 157
 158 string SMTInterpreter::encodeBooleanVar( BooleanVar *bv) {
 159         ValuedSignature *boolSig = sigEnc.getBooleanSignature(bv);
 160         return *boolSig + "";
 161 }
 162
 163 string SMTInterpreter::processElementFunction(ElementFunction *elemFunc, ValuedSignature *signature) {
 164         FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
 165         uint numDomains = elemFunc->inputs.getSize();
 166         ASSERT(numDomains > 1);
 167         ValuedSignature *inputs[numDomains];
 168         string result;
 169         for (uint i = 0; i < numDomains; i++) {
 170                 Element *elem = elemFunc->inputs.get(i);
 171                 inputs[i] = sigEnc.getElementSignature(elem);
 172                 if (elem->type == ELEMFUNCRETURN) {
 173                         result += processElementFunction((ElementFunction *) elem, inputs[i]);
 174                 }
 175         }
 176         string op;
 177         switch (function->op) {
 178         case SATC_ADD:
 179                 op = "+";
 180                 break;
 181         case SATC_SUB:
 182                 op = "-";
 183                 break;
 184         default:
 185                 ASSERT(0);
 186         }
 187         result += "( = " + *signature;
 188         string tmp = "" + *inputs[0];
 189         for (uint i = 1; i < numDomains; i++) {
 190                 tmp = "( " + op + " " + tmp + " " + *inputs[i] + " )";
 191         }
 192         result += tmp + " )";
 193         return result;
 194 }
 195
 196 string SMTInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2) {
 197         switch (op) {
 198         case SATC_EQUALS:
 199                 return "( = " + *elemSig1 + " " + *elemSig2 + " )";
 200         case SATC_LT:
 201                 return "( < " + *elemSig1 + " " + *elemSig2 + " )";
 202         case SATC_GT:
 203                 return "(> " + *elemSig1 + " " + *elemSig2 + " )";
 204         default:
 205                 ASSERT(0);
 206         }
 207 }
 208
 209