From 0055254f4cfa35fbe292644f2e954e01a37f70af Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 28 Jul 2016 17:04:06 -0700
Subject: [PATCH] fix build for non C++11

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/automata/symbolic_automata.h     | 70 +++++++++++------------
 src/math/automata/symbolic_automata_def.h |  2 +-
 2 files changed, 36 insertions(+), 36 deletions(-)

diff --git a/src/math/automata/symbolic_automata.h b/src/math/automata/symbolic_automata.h
index 7589a931b..6d7bc8290 100644
--- a/src/math/automata/symbolic_automata.h
+++ b/src/math/automata/symbolic_automata.h
@@ -106,41 +106,41 @@ public:
     automaton_t* mk_product(automaton_t& a, automaton_t& b);
 
 private:
-	automaton_t* mk_determinstic_param(automaton_t& a, bool flip_acceptance);
-
-	vector<std::pair<vector<bool>, ref_t>> generate_min_terms(vector<ref_t> &constraints) {
-		vector<std::pair<vector<bool>, ref_t>> min_terms;
-
-		ref_t curr_pred(m_ba.mk_true(), m);
-		vector<bool> curr_bv;
-
-		generate_min_terms_rec(constraints, min_terms, 0, curr_bv, curr_pred);
-
-		return min_terms;
-	}
-	void generate_min_terms_rec(vector<ref_t> &constraints, vector<std::pair<vector<bool>, ref_t>> &min_terms, unsigned i, vector<bool> &curr_bv, ref_t &curr_pred) {
-		lbool is_sat = m_ba.is_sat(curr_pred);
-		if (is_sat != l_true) {
-			return;
-		}
-
-		if (i == constraints.size()) {
-			min_terms.push_back(std::pair<vector<bool>, ref_t>(curr_bv, curr_pred));
-		}
-		else {
-			//true case
-			curr_bv.push_back(true);
-			ref_t new_pred_pos(m_ba.mk_and(curr_pred, constraints[i]), m);			
-			generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_pos);
-			curr_bv.pop_back();
-
-			//false case
-			curr_bv.push_back(false);
-			ref_t new_pred_neg(m_ba.mk_and(curr_pred, m_ba.mk_not(constraints[i])), m);
-			generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_neg);
-			curr_bv.pop_back();
-		}
-	}
+    automaton_t* mk_determinstic_param(automaton_t& a, bool flip_acceptance);
+    
+    vector<std::pair<vector<bool>, ref_t> > generate_min_terms(vector<ref_t> &constraints) {
+        vector<std::pair<vector<bool>, ref_t> > min_terms;
+        
+        ref_t curr_pred(m_ba.mk_true(), m);
+        vector<bool> curr_bv;
+        
+        generate_min_terms_rec(constraints, min_terms, 0, curr_bv, curr_pred);
+        
+        return min_terms;
+    }
+    void generate_min_terms_rec(vector<ref_t> &constraints, vector<std::pair<vector<bool>, ref_t> > &min_terms, unsigned i, vector<bool> &curr_bv, ref_t &curr_pred) {
+        lbool is_sat = m_ba.is_sat(curr_pred);
+        if (is_sat != l_true) {
+            return;
+        }
+        
+        if (i == constraints.size()) {
+            min_terms.push_back(std::pair<vector<bool>, ref_t>(curr_bv, curr_pred));
+        }
+        else {
+            //true case
+            curr_bv.push_back(true);
+            ref_t new_pred_pos(m_ba.mk_and(curr_pred, constraints[i]), m);			
+            generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_pos);
+            curr_bv.pop_back();
+            
+            //false case
+            curr_bv.push_back(false);
+            ref_t new_pred_neg(m_ba.mk_and(curr_pred, m_ba.mk_not(constraints[i])), m);
+            generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_neg);
+            curr_bv.pop_back();
+        }
+    }
 };
 
 
diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h
index ad03492eb..737dc9e19 100644
--- a/src/math/automata/symbolic_automata_def.h
+++ b/src/math/automata/symbolic_automata_def.h
@@ -285,7 +285,7 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_compl
 
 template<class T, class M>
 typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_determinstic_param(automaton_t& a, bool flip_acceptance = false) {
-	vector<std::pair<vector<bool>, ref_t>> min_terms;
+	vector<std::pair<vector<bool>, ref_t> > min_terms;
 	vector<ref_t> predicates;
 	
 	map<uint_set, unsigned, uint_set::hash, uint_set::eq> s2id;	// set of states to unique id