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         snprintf(command, size, "./z3 -T:%u -in < %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
 105 }
 106
 107 string SMTInterpreter::negateConstraint(string constr){
 108         return "( not " + constr + " )";
 109 }
 110
 111 string SMTInterpreter::encodeBooleanLogic( BooleanLogic *bl){
 112         uint size = bl->inputs.getSize();
 113         string array[size];
 114         for (uint i = 0; i < size; i++)
 115                 array[i] = encodeConstraint(bl->inputs.get(i));
 116         string op;
 117         switch (bl->op){
 118                 case SATC_OR:
 119                         op = "or";
 120                         break;
 121                 case SATC_AND:
 122                         op = "and";
 123                         break;
 124                 case SATC_NOT:
 125                         op = "not";
 126                         break;
 127                 case SATC_IMPLIES:
 128                         op = "=>";
 129                         break;
 130                 case SATC_XOR:
 131                 default:
 132                         ASSERT(0);
 133         }
 134         switch (bl->op) {
 135                 case SATC_XOR:
 136                 case SATC_OR:
 137                 case SATC_AND:{
 138                         ASSERT(size >= 2);
 139                         string res = array[0];
 140                         for( uint i=1; i< size; i++){
 141                                 res = "( " + op + " " + res + " " +  array[i] + " )";
 142                         }
 143                         return res;
 144                 }
 145                 case SATC_NOT:{
 146                         return "( not " + array[0] + " )";
 147                 }
 148                 case SATC_IMPLIES:
 149                         return "( " + op + " " + array[0] + " " + array[1] + " )";
 150                 case SATC_IFF:
 151                 default:
 152                         ASSERT(0);
 153
 154         }
 155 }
 156
 157 string SMTInterpreter::encodeBooleanVar( BooleanVar *bv){
 158         ValuedSignature * boolSig = sigEnc.getBooleanSignature(bv);
 159         return *boolSig + "";
 160 }
 161
 162 string SMTInterpreter::processElementFunction(ElementFunction* elemFunc, ValuedSignature *signature){
 163         FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
 164         uint numDomains = elemFunc->inputs.getSize();
 165         ASSERT(numDomains > 1);
 166         ValuedSignature *inputs[numDomains];
 167         string result;
 168         for (uint i = 0; i < numDomains; i++) {
 169                 Element *elem = elemFunc->inputs.get(i);
 170                 inputs[i] = sigEnc.getElementSignature(elem);
 171                 if(elem->type == ELEMFUNCRETURN){
 172                         result += processElementFunction((ElementFunction *) elem, inputs[i]);
 173                 }
 174         }
 175         string op;
 176         switch(function->op){
 177                 case SATC_ADD:
 178                         op = "+";
 179                         break;
 180                 case SATC_SUB:
 181                         op = "-";
 182                         break;
 183                 default:
 184                         ASSERT(0);
 185         }
 186         result += "( = " + *signature;
 187         string tmp = "" + *inputs[0];
 188         for (uint i = 1; i < numDomains; i++) {
 189                 tmp = "( " + op + " " + tmp + " " + *inputs[i] + " )";
 190         }
 191         result += tmp + " )";
 192         return result;
 193 }
 194
 195 string SMTInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2){
 196         switch (op) {
 197                 case SATC_EQUALS:
 198                         return "( = " + *elemSig1 + " " + *elemSig2 +" )";
 199                 case SATC_LT:
 200                         return "( < " + *elemSig1 + " " + *elemSig2 + " )";
 201                 case SATC_GT:
 202                         return "(> " + *elemSig1 + " " + *elemSig2 + " )";
 203                 default:
 204                         ASSERT(0);
 205         }
 206 }
 207
 208