using namespace std;
-SMTInterpreter::SMTInterpreter(CSolver *_solver):
- Interpreter(_solver)
+SMTInterpreter::SMTInterpreter(CSolver *_solver) :
+ Interpreter(_solver)
{
output.open(SMTFILENAME);
- if(!output.is_open()){
+ if (!output.is_open()) {
model_print("AlloyEnc:Error in opening the dump file satune.smt\n");
exit(-1);
}
}
-SMTInterpreter::~SMTInterpreter(){
- if(output.is_open()){
+SMTInterpreter::~SMTInterpreter() {
+ if (output.is_open()) {
output.close();
}
}
-ValuedSignature *SMTInterpreter::getBooleanSignature(uint id){
+ValuedSignature *SMTInterpreter::getBooleanSignature(uint id) {
return new SMTBoolSig(id);
}
-ValuedSignature *SMTInterpreter::getElementSignature(uint id, Signature *ssig){
+ValuedSignature *SMTInterpreter::getElementSignature(uint id, Signature *ssig) {
return new SMTElementSig(id, (SMTSetSig *)ssig);
}
-Signature *SMTInterpreter::getSetSignature(uint id, Set *set){
+Signature *SMTInterpreter::getSetSignature(uint id, Set *set) {
return new SMTSetSig(id, set);
}
-void SMTInterpreter::dumpAllConstraints(Vector<char *> &facts){
- for(uint i=0; i< facts.getSize(); i++){
+void SMTInterpreter::dumpAllConstraints(Vector<char *> &facts) {
+ for (uint i = 0; i < facts.getSize(); i++) {
char *cstr = facts.get(i);
writeToFile("(assert " + string(cstr) + ")");
}
}
-void SMTInterpreter::extractValue(char *idline, char *valueline){
+void SMTInterpreter::extractValue(char *idline, char *valueline) {
uint id;
- if (1 == sscanf(idline,"%*[^0123456789]%u", &id)){
+ if (1 == sscanf(idline,"%*[^0123456789]%u", &id)) {
char valuestr [512];
ASSERT(1 == sscanf(valueline,"%s)", valuestr));
uint value;
- if (strcmp (valuestr, "true)") == 0 ){
- value =1;
- }else if (strcmp(valuestr, "false)") == 0){
+ if (strcmp (valuestr, "true)") == 0 ) {
+ value = 1;
+ } else if (strcmp(valuestr, "false)") == 0) {
value = 0;
- }else {
+ } else {
ASSERT(1 == sscanf(valueline, "%*[^0123456789]%u", &value));
}
}
}
-int SMTInterpreter::getResult(){
+int SMTInterpreter::getResult() {
ifstream input(SMTSOLUTIONFILE, ios::in);
string line;
- while(getline(input, line)){
- if(line.find("unsat")!= line.npos){
+ while (getline(input, line)) {
+ if (line.find("unsat") != line.npos) {
return IS_UNSAT;
}
- if(line.find("(define-fun") != line.npos || line.find("( (") != line.npos){
+ if (line.find("(define-fun") != line.npos || line.find("( (") != line.npos) {
string valueline;
ASSERT(getline(input, valueline));
- char cline [line.size()+1];
+ char cline [line.size() + 1];
strcpy ( cline, line.c_str() );
- char vline [valueline.size()+1];
+ char vline [valueline.size() + 1];
strcpy ( vline, valueline.c_str() );
extractValue(cline, vline);
}
return IS_SAT;
}
-void SMTInterpreter::dumpFooter(){
+void SMTInterpreter::dumpFooter() {
output << "(check-sat)" << endl;
output << "(get-model)" << endl;
}
-void SMTInterpreter::dumpHeader(){
+void SMTInterpreter::dumpHeader() {
}
-void SMTInterpreter::compileRunCommand(char * command, size_t size){
+void SMTInterpreter::compileRunCommand(char *command, size_t size) {
model_print("Calling Z3...\n");
snprintf(command, size, "./run.sh z3 -T:%u -in < %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
}
-string SMTInterpreter::negateConstraint(string constr){
+string SMTInterpreter::negateConstraint(string constr) {
return "( not " + constr + " )";
}
-string SMTInterpreter::encodeBooleanLogic( BooleanLogic *bl){
+string SMTInterpreter::encodeBooleanLogic( BooleanLogic *bl) {
uint size = bl->inputs.getSize();
string array[size];
for (uint i = 0; i < size; i++)
array[i] = encodeConstraint(bl->inputs.get(i));
string op;
- switch (bl->op){
- case SATC_OR:
- op = "or";
- break;
- case SATC_AND:
- op = "and";
- break;
- case SATC_NOT:
- op = "not";
- break;
- case SATC_IMPLIES:
- op = "=>";
- break;
- case SATC_XOR:
- default:
- ASSERT(0);
+ switch (bl->op) {
+ case SATC_OR:
+ op = "or";
+ break;
+ case SATC_AND:
+ op = "and";
+ break;
+ case SATC_NOT:
+ op = "not";
+ break;
+ case SATC_IMPLIES:
+ op = "=>";
+ break;
+ case SATC_XOR:
+ default:
+ ASSERT(0);
}
switch (bl->op) {
- case SATC_XOR:
- case SATC_OR:
- case SATC_AND:{
- ASSERT(size >= 2);
- string res = array[0];
- for( uint i=1; i< size; i++){
- res = "( " + op + " " + res + " " + array[i] + " )";
- }
- return res;
+ case SATC_XOR:
+ case SATC_OR:
+ case SATC_AND: {
+ ASSERT(size >= 2);
+ string res = array[0];
+ for ( uint i = 1; i < size; i++) {
+ res = "( " + op + " " + res + " " + array[i] + " )";
}
- case SATC_NOT:{
- return "( not " + array[0] + " )";
- }
- case SATC_IMPLIES:
- return "( " + op + " " + array[0] + " " + array[1] + " )";
- case SATC_IFF:
- default:
- ASSERT(0);
+ return res;
+ }
+ case SATC_NOT: {
+ return "( not " + array[0] + " )";
+ }
+ case SATC_IMPLIES:
+ return "( " + op + " " + array[0] + " " + array[1] + " )";
+ case SATC_IFF:
+ default:
+ ASSERT(0);
}
}
-string SMTInterpreter::encodeBooleanVar( BooleanVar *bv){
- ValuedSignature * boolSig = sigEnc.getBooleanSignature(bv);
+string SMTInterpreter::encodeBooleanVar( BooleanVar *bv) {
+ ValuedSignature *boolSig = sigEnc.getBooleanSignature(bv);
return *boolSig + "";
}
-string SMTInterpreter::processElementFunction(ElementFunction* elemFunc, ValuedSignature *signature){
+string SMTInterpreter::processElementFunction(ElementFunction *elemFunc, ValuedSignature *signature) {
FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
uint numDomains = elemFunc->inputs.getSize();
ASSERT(numDomains > 1);
for (uint i = 0; i < numDomains; i++) {
Element *elem = elemFunc->inputs.get(i);
inputs[i] = sigEnc.getElementSignature(elem);
- if(elem->type == ELEMFUNCRETURN){
+ if (elem->type == ELEMFUNCRETURN) {
result += processElementFunction((ElementFunction *) elem, inputs[i]);
}
}
string op;
- switch(function->op){
- case SATC_ADD:
- op = "+";
- break;
- case SATC_SUB:
- op = "-";
- break;
- default:
- ASSERT(0);
+ switch (function->op) {
+ case SATC_ADD:
+ op = "+";
+ break;
+ case SATC_SUB:
+ op = "-";
+ break;
+ default:
+ ASSERT(0);
}
- result += "( = " + *signature;
+ result += "( = " + *signature;
string tmp = "" + *inputs[0];
for (uint i = 1; i < numDomains; i++) {
tmp = "( " + op + " " + tmp + " " + *inputs[i] + " )";
return result;
}
-string SMTInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2){
+string SMTInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2) {
switch (op) {
- case SATC_EQUALS:
- return "( = " + *elemSig1 + " " + *elemSig2 +" )";
- case SATC_LT:
- return "( < " + *elemSig1 + " " + *elemSig2 + " )";
- case SATC_GT:
- return "(> " + *elemSig1 + " " + *elemSig2 + " )";
- default:
- ASSERT(0);
+ case SATC_EQUALS:
+ return "( = " + *elemSig1 + " " + *elemSig2 + " )";
+ case SATC_LT:
+ return "( < " + *elemSig1 + " " + *elemSig2 + " )";
+ case SATC_GT:
+ return "(> " + *elemSig1 + " " + *elemSig2 + " )";
+ default:
+ ASSERT(0);
}
}
projects / satune.git / blobdiff