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