Fix tabbing

[satune.git] / src / Interpreter / smtsig.cc

diff --git a/src/Interpreter/smtsig.cc b/src/Interpreter/smtsig.cc
index 4c77493f7d2025bf44ccaa00fe9deed74b8aac60..6ccbd224e641ca028b929f117ebb8079cfac9b60 100644 (file)
--- a/src/Interpreter/smtsig.cc
+++ b/src/Interpreter/smtsig.cc
@@ -1,39 +1,39 @@
 #include "smtsig.h"
 #include "set.h"
 
-SMTBoolSig::SMTBoolSig(uint id):
+SMTBoolSig::SMTBoolSig(uint id) :
        ValuedSignature(id)
 {
 }
 
-string SMTBoolSig::toString() const{
+string SMTBoolSig::toString() const {
        return "b" + to_string(id);
 }
 
-string SMTBoolSig::getSignature() const{
+string SMTBoolSig::getSignature() const {
        return "(declare-const b" + to_string(id) + " Bool)";
 }
 
-string SMTBoolSig::getAbsSignature() const{
+string SMTBoolSig::getAbsSignature() const {
        return "";
 }
 
-SMTElementSig::SMTElementSig(uint id, SMTSetSig *_ssig): 
+SMTElementSig::SMTElementSig(uint id, SMTSetSig *_ssig) :
        ValuedSignature(id),
        ssig(_ssig)
 {
 }
 
-string SMTElementSig::toString() const{
+string SMTElementSig::toString() const {
        return "e" + to_string(id);
 }
 
-string SMTElementSig::getSignature() const{
+string SMTElementSig::getSignature() const {
        string str = "(declare-const e" + to_string(id) + " Int)\n";
        string constraint = ssig->getAbsSignature();
        size_t start_pos;
        string placeholder = "$";
-       while((start_pos = constraint.find(placeholder)) != string::npos){
+       while ((start_pos = constraint.find(placeholder)) != string::npos) {
                constraint.replace(start_pos, placeholder.size(), to_string(id));
        }
        //constraint.replace(constraint.begin(), constraint.end(), "$", );
@@ -41,41 +41,41 @@ string SMTElementSig::getSignature() const{
        return str;
 }
 
-string SMTElementSig::getAbsSignature() const{
+string SMTElementSig::getAbsSignature() const {
        return "";
-       
+
 }
 
-SMTSetSig::SMTSetSig(uint id, Set *set): Signature(id){
+SMTSetSig::SMTSetSig(uint id, Set *set) : Signature(id) {
        ASSERT(set->getSize() > 0);
-       int min = set->getElement(0), max = set->getElement(set->getSize()-1);
+       int min = set->getElement(0), max = set->getElement(set->getSize() - 1);
        Vector<int> holes;
        int prev = set->getElement(0);
-       for(uint i=1; i< set->getSize(); i++){
+       for (uint i = 1; i < set->getSize(); i++) {
                int curr = set->getElement(i);
-               if(prev != curr -1){
-                       for(int j=prev+1; j< curr; j++){
+               if (prev != curr - 1) {
+                       for (int j = prev + 1; j < curr; j++) {
                                holes.push(j);
                        }
                }
                prev = curr;
        }
-       constraint = "(assert (<= e$ " + to_string(max) +"))\n";
-       constraint += "(assert (>= e$ " + to_string(min) +"))\n";
-       for(uint i=0; i< holes.getSize(); i++){
-               constraint += "(assert (not (= e$ " + to_string(holes.get(i)) +")))\n";
+       constraint = "(assert (<= e$ " + to_string(max) + "))\n";
+       constraint += "(assert (>= e$ " + to_string(min) + "))\n";
+       for (uint i = 0; i < holes.getSize(); i++) {
+               constraint += "(assert (not (= e$ " + to_string(holes.get(i)) + ")))\n";
        }
 }
 
-string SMTSetSig::toString() const{
+string SMTSetSig::toString() const {
        return "";
 }
 
-string SMTSetSig::getSignature() const{
+string SMTSetSig::getSignature() const {
        return "";
 }
 
-string SMTSetSig::getAbsSignature() const{
+string SMTSetSig::getAbsSignature() const {
        return constraint;
-       
+
 }