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