1 #include "smtinterpreter.h"
3 #include "signatureenc.h"
11 #include "inc_solver.h"
13 #include "cppvector.h"
18 #define SMTFILENAME "satune.smt"
19 #define SMTSOLUTIONFILE "solution.sol"
21 SMTInterpreter::SMTInterpreter(CSolver *_solver):
24 output.open(SMTFILENAME);
25 if(!output.is_open()){
26 model_print("AlloyEnc:Error in opening the dump file satune.smt\n");
31 SMTInterpreter::~SMTInterpreter(){
38 ValuedSignature *SMTInterpreter::getBooleanSignature(uint id){
39 return new SMTBoolSig(id);
42 ValuedSignature *SMTInterpreter::getElementSignature(uint id, Signature *ssig){
43 return new SMTElementSig(id, (SMTSetSig *)ssig);
46 Signature *SMTInterpreter::getSetSignature(uint id, Set *set){
47 return new SMTSetSig(id, set);
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) + ")");
57 void SMTInterpreter::extractValue(char *idline, char *valueline){
59 if (1 == sscanf(idline,"%*[^0123456789]%u", &id)){
61 ASSERT(1 == sscanf(valueline,"%s)", valuestr));
63 if (strcmp (valuestr, "true)") == 0 ){
65 }else if (strcmp(valuestr, "false)") == 0){
68 ASSERT(1 == sscanf(valueline, "%*[^0123456789]%u", &value));
71 model_print("Signature%u = %u\n", id, value);
72 sigEnc.setValue(id, value);
78 int SMTInterpreter::getResult(){
79 ifstream input(SMTSOLUTIONFILE, ios::in);
81 while(getline(input, line)){
82 if(line.find("unsat")!= line.npos){
85 if(line.find("(define-fun") != line.npos){
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);
98 void SMTInterpreter::dumpFooter(){
99 output << "(check-sat)" << endl;
100 output << "(get-model)" << endl;
103 void SMTInterpreter::dumpHeader(){
106 void SMTInterpreter::compileRunCommand(char * command, size_t size){
107 snprintf(command, size, "./z3 -T:%u -in < %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
110 string SMTInterpreter::negateConstraint(string constr){
111 return "( not " + constr + " )";
114 string SMTInterpreter::encodeBooleanLogic( BooleanLogic *bl){
115 uint size = bl->inputs.getSize();
117 for (uint i = 0; i < size; i++)
118 array[i] = encodeConstraint(bl->inputs.get(i));
142 string res = array[0];
143 for( uint i=1; i< size; i++){
144 res = "( " + op + " " + res + " " + array[i] + " )";
149 return "( not " + array[0] + " )";
152 return "( " + op + " " + array[0] + " " + array[1] + " )";
160 string SMTInterpreter::encodeBooleanVar( BooleanVar *bv){
161 ValuedSignature * boolSig = sigEnc.getBooleanSignature(bv);
162 return *boolSig + "";
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];
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]);
179 switch(function->op){
189 result += "( = " + *signature;
190 string tmp = "" + *inputs[0];
191 for (uint i = 1; i < numDomains; i++) {
192 tmp = "( " + op + " " + tmp + " " + *inputs[i] + " )";
194 result += tmp + " )";
198 string SMTInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2){
201 return "( = " + *elemSig1 + " " + *elemSig2 +" )";
203 return "( < " + *elemSig1 + " " + *elemSig2 + " )";
205 return "(> " + *elemSig1 + " " + *elemSig2 + " )";