added symbolic automata complement for sequences

src/ast/rewriter/seq_rewriter.cpp

@@ -86,20 +86,25 @@ public:
         expr_ref fml(m.mk_true(), m);
         return sym_expr::mk_pred(fml, m.mk_bool_sort());
     }
-    virtual T mk_and(T x, T y) {
+	virtual T mk_and(T x, T y) {
-        if (x->is_char() && y->is_char()) {
+		if (x->is_char() && y->is_char()) {
-            if (x->get_char() == y->get_char()) {
+			if (x->get_char() == y->get_char()) {
-                return x;
+				return x;
-            }
+			}
-            if (m.are_distinct(x->get_char(), y->get_char())) {
+			if (m.are_distinct(x->get_char(), y->get_char())) {
-                expr_ref fml(m.mk_false(), m);
+				expr_ref fml(m.mk_false(), m);
-                return sym_expr::mk_pred(fml, x->get_sort());
+				return sym_expr::mk_pred(fml, x->get_sort());
-            }
+			}
-        }
+		}
-        var_ref v(m.mk_var(0, x->get_sort()), m);
+
-        expr_ref fml1 = x->accept(v);
+		sort* s = x->get_sort();
-        expr_ref fml2 = y->accept(v);
+		if (m.is_bool(s)) s = y->get_sort();
-        if (m.is_true(fml1)) return y;
+		var_ref v(m.mk_var(0, s), m);
+		expr_ref fml1 = x->accept(v);
+		expr_ref fml2 = y->accept(v);
+		if (m.is_true(fml1)) {
+			return y;
+		}
         if (m.is_true(fml2)) return x;
         expr_ref fml(m.mk_and(fml1, fml2), m);
         return sym_expr::mk_pred(fml, x->get_sort());
@@ -166,6 +171,11 @@ public:
         expr_ref fml(m.mk_not(x->accept(v)), m);
         return sym_expr::mk_pred(fml, x->get_sort());
     }
+
+	/*virtual vector<std::pair<vector<bool>, T>> generate_min_terms(vector<T> constraints){
+		
+		return 0;
+	}*/
 };
 
 re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m), m_ba(0), m_sa(0) {}
@@ -233,47 +243,9 @@ eautomaton* re2automaton::re2aut(expr* e) {
             TRACE("seq", tout << "Range expression is not handled: " << mk_pp(e, m) << "\n";);
         }
     }
-    else if (u.re.is_complement(e, e0)) {
+	else if (u.re.is_complement(e, e0) && (a = re2aut(e0)) && m_sa) {
-        // TBD non-standard semantics of complementation.
+		return m_sa->mk_complement(*a);
-        if (u.re.is_range(e0, e1, e2) && u.str.is_string(e1, s1) && u.str.is_string(e2, s2) &&
+	}
-            s1.length() == 1 && s2.length() == 1) {
-            unsigned start = s1[0];
-            unsigned stop = s2[0];
-            unsigned nb = s1.num_bits();
-            sort_ref s(bv.mk_sort(nb), m);          
-            expr_ref v(m.mk_var(0, s), m);
-            expr_ref _start(bv.mk_numeral(start, nb), m);
-            expr_ref _stop(bv.mk_numeral(stop, nb), m);
-            expr_ref _pred(m.mk_not(m.mk_and(bv.mk_ule(_start, v), bv.mk_ule(v, _stop))), m);
-            a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred, s));
-            display_expr1 disp(m);
-            TRACE("seq", tout << mk_pp(e, m) << "\n"; a->display(tout, disp););
-            return a.detach();
-        }
-        else if (u.re.is_to_re(e0, e1) && u.str.is_string(e1, s1) && s1.length() == 1) {
-            unsigned nb = s1.num_bits();
-            sort_ref s(bv.mk_sort(nb), m);          
-            expr_ref v(m.mk_var(0, s), m);
-            expr_ref _ch(bv.mk_numeral(s1[0], nb), m);          
-            expr_ref _pred(m.mk_not(m.mk_eq(v, _ch)), m);
-            a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred, s));
-            display_expr1 disp(m);
-            TRACE("seq", tout << mk_pp(e, m) << "\n"; a->display(tout, disp););
-            return a.detach();
-        }
-        else if (u.re.is_to_re(e0, e1) && u.str.is_unit(e1, e2)) {
-            sort* s = m.get_sort(e2);
-            expr_ref v(m.mk_var(0, s), m);
-            expr_ref _pred(m.mk_not(m.mk_eq(v, e2)), m);
-            a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred, s));
-            display_expr1 disp(m);
-            TRACE("seq", tout << mk_pp(e, m) << "\n"; a->display(tout, disp););
-            return a.detach();
-        }
-        else {
-            TRACE("seq", tout << "Complement expression is not handled: " << mk_pp(e, m) << "\n";);
-        }
-    }
     else if (u.re.is_loop(e, e1, lo, hi) && (a = re2aut(e1))) {
         scoped_ptr<eautomaton> eps = eautomaton::mk_epsilon(sm);
         b = eautomaton::mk_epsilon(sm);

src/math/automata/automaton.h

@@ -467,10 +467,17 @@ public:
     unsigned out_degree(unsigned state) const { return m_delta[state].size(); }
     move const& get_move_from(unsigned state) const { SASSERT(m_delta[state].size() == 1); return m_delta[state][0]; }
     move const& get_move_to(unsigned state) const { SASSERT(m_delta_inv[state].size() == 1); return m_delta_inv[state][0]; }
-    moves const& get_moves_from(unsigned state) const { return m_delta[state]; }
+    moves const& get_moves_from(unsigned state) const { return m_delta[state]; }	
     moves const& get_moves_to(unsigned state) const { return m_delta_inv[state]; }
     bool initial_state_is_source() const { return m_delta_inv[m_init].empty(); }
     bool is_final_state(unsigned s) const { return m_final_set.contains(s); }
+	bool is_final_configuration(uint_set s) const { 
+		for (uint_set::iterator it = s.begin(), end = s.end(); it != end; ++it) {
+			if (is_final_state(*it))
+				return true;
+		}
+		return false; 
+	}
     bool is_epsilon_free() const {
         for (unsigned i = 0; i < m_delta.size(); ++i) {
             moves const& mvs = m_delta[i];
@@ -517,6 +524,13 @@ public:
     void get_moves_from(unsigned state, moves& mvs, bool epsilon_closure = true) const {
         get_moves(state, m_delta, mvs, epsilon_closure);
     }
+	void get_moves_from_states(uint_set states, moves& mvs, bool epsilon_closure = true) const {
+		for (uint_set::iterator it = states.begin(), end = states.end(); it != end; ++it) {
+			moves curr;
+			get_moves(*it, m_delta, curr, epsilon_closure);
+			mvs.append(curr);
+		}
+	}
     void get_moves_to(unsigned state, moves& mvs, bool epsilon_closure = true) {
         get_moves(state, m_delta_inv, mvs, epsilon_closure);
     }

src/math/automata/boolean_algebra.h

@@ -38,7 +38,7 @@ public:
 template<class T>
 class boolean_algebra : public positive_boolean_algebra<T> {
 public:
-    virtual T mk_not(T x) = 0;
+    virtual T mk_not(T x) = 0;	
     //virtual lbool are_equivalent(T x, T y) = 0;
     //virtual T simplify(T x) = 0;    
 };

src/math/automata/symbolic_automata.h

@@ -96,16 +96,54 @@ class symbolic_automata {
 
 public:
     symbolic_automata(M& m, ba_t& ba): m(m), m_ba(ba) {}
-    //automaton_t* mk_determinstic(automaton_t& a);
+    automaton_t* mk_determinstic(automaton_t& a);
-    //automaton_t* mk_complement(automaton_t& a);
+    automaton_t* mk_complement(automaton_t& a);
     automaton_t* remove_epsilons(automaton_t& a);
     automaton_t* mk_total(automaton_t& a);
     automaton_t* mk_minimize(automaton_t& a);
     automaton_t* mk_minimize_total(automaton_t& a);
     automaton_t* mk_difference(automaton_t& a, automaton_t& b);
     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();
+		}
+	}
 };
 
 
 
+
 #endif 

src/math/automata/symbolic_automata_def.h

@@ -273,6 +273,95 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minim
     return alloc(automaton_t, m, new_init, new_final, new_moves);
 }
 
+template<class T, class M>
+typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_determinstic(automaton_t& a) {
+	return mk_determinstic_param(a);
+}
+
+template<class T, class M>
+typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_complement(automaton_t& a) {
+	return mk_determinstic_param(a, true);
+}
+
+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<ref_t> predicates;
+	
+	map<uint_set, unsigned, uint_set::hash, uint_set::eq> s2id;	// set of states to unique id
+	vector<uint_set> id2s;										// unique id to set of b-states
+	uint_set set;
+	unsigned_vector vector;
+	moves_t new_mvs;                                           // moves in the resulting automaton
+	unsigned_vector new_final_states;                            // new final states
+	unsigned p_state_id = 0;                                    // next state identifier
+
+	// adds non-final states of a to final if flipping and and final otherwise
+	if (a.is_final_configuration(set) != flip_acceptance) {
+		new_final_states.push_back(p_state_id);
+	}
+
+	set.insert(a.init());										// initial state as aset
+	s2id.insert(set, p_state_id++);                              // the index to the initial state is 0
+	id2s.push_back(set);
+
+	svector<uint_set> todo; //States to visit
+	todo.push_back(set);
+
+	uint_set state;
+	moves_t mvsA;
+	
+	new_mvs.reset();
+
+	// or just make todo a vector whose indices coincide with state_id.
+	while (!todo.empty()) {
+		uint_set state = todo.back();
+
+		unsigned state_id = s2id[state];
+		todo.pop_back();
+		mvsA.reset();
+
+		min_terms.reset();
+		predicates.reset();
+
+		a.get_moves_from_states(state, mvsA);
+
+		for (unsigned j = 0; j < mvsA.size(); ++j) {			
+			ref_t mv_guard(mvsA[j].t(),m);			
+			predicates.push_back(mv_guard);
+		}
+
+		min_terms = generate_min_terms(predicates);
+		for (unsigned j = 0; j < min_terms.size(); ++j) {
+			set = uint_set();
+			for (unsigned i = 0; i < mvsA.size(); ++i) {
+				if (min_terms[j].first[i])
+					set.insert(mvsA[i].dst());
+			}
+
+			bool is_new = !s2id.contains(set);
+			if (is_new) {
+				if (a.is_final_configuration(set) != flip_acceptance) {
+					new_final_states.push_back(p_state_id);
+				}
+
+				s2id.insert(set, p_state_id++);
+				id2s.push_back(set);
+				todo.push_back(set);
+			}			
+			new_mvs.push_back(move_t(m, state_id, s2id[set], min_terms[j].second));
+		}
+	}
+
+	if (new_final_states.empty()) {
+		return alloc(automaton_t, m);
+	}
+
+	return alloc(automaton_t, m, 0, new_final_states, new_mvs);
+}
+
+
+
 template<class T, class M>
 typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_product(automaton_t& a, automaton_t& b) {
     u2_map<unsigned> pair2id;
@@ -362,130 +451,11 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_produ
     }
 } 
 
-#if 0
+
-template<class T, class M>
-unsigned symbolic_automata<T, M>::get_product_state_id(u2_map<unsigned>& pair2id, unsigned_pair const& p, unsigned& id) {
-    unsigned result = 0;
-    if (!pair2id.find(p, result)) {
-        result = id++;
-        pair2id.insert(p, result);
-    }
-    return result;
-}
-#endif
 
 template<class T, class M>
 typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_difference(automaton_t& a, automaton_t& b) {
-#if 0
+	return mk_product(a,mk_complement(b));
-    map<uint_set, unsigned, uint_set_hash, uint_set_eq> bs2id;   // set of b-states to unique id
-    vector<uintset> id2bs;                                       // unique id to set of b-states
-    u2_map<unsigned> pair2id;                                    // pair of states to new state id
-    unsigned sink_state = UINT_MAX;
-    uint_set bset;
-    moves_t new_moves;                                           // moves in the resulting automaton
-    unsigned_vector new_final_states;                            // new final states
-    unsigned p_state_id = 0;                                     // next state identifier
-    bs2id.insert(uint_set(), sink_state);                        // the sink state has no b-states
-    bset.insert(b.init());                                       // the initial state has a single initial b state
-    bs2id.insert(bset, 0);                                       // the index to the initial b state is 0
-    id2bs.push_back(bset);
-    if (!b.is_final_state(b.init()) && a.is_final_state(a.init())) {
-        new_final_states.push_back(p_state_id);
-    }
-
-    svector<unsigned_pair> todo;
-    unsigned_pair state(a.init(), 0);
-    todo.push_back(state);
-    pair2id.insert(state, p_state_id++);
-
-    // or just make todo a vector whose indices coincide with state_id.
-    while (!todo.empty()) {
-        state = todo.back();
-        unsigned state_id = pair2id[state];
-        todo.pop_back();
-        mvsA.reset();
-        a.get_moves_from(state.first, mvsA, true);
-        if (state.second == sink_state) {
-            for (unsigned i = 0; i < mvsA.size(); ++i) {
-                unsigned_pair dst(mvsA[i].dst(), sink_state);
-                bool is_new = !pair2id.contains(dst);
-                unsigned dst_id = get_product_state_id(pair2id, dst, p_state_id);
-                new_moves.push_back(move_t(m, state_id, dst_id, mvsA[i].t()));
-                if (is_new && a.is_final_state(mvsA[i].dst())) {
-                    new_final_states.push_back(dst_id);
-                    todo.push_back(dst);
-                }
-            }
-        }
-        else {
-            get_moves_from(b, id2bs[state.second], mvsB);
-            generate_min_terms(mvsB, min_terms);
-            for (unsigned j = 0; j < min_terms.size(); ++j) {
-                for (unsigned i = 0; i < mvsA.size(); ++i) {
-                    ref_t cond(m_ba.mk_and(mvsA[i].t(), min_terms[j].second), m);
-                    switch (m_ba.is_sat(cond)) {
-                    case l_false:
-                        break;
-                    case l_true:
-                        ab_combinations.push_back(ab_comb(i, min_terms[j].first, cond));
-                        break;
-                    case l_undef:
-                        return 0;
-                    }
-                }
-            }
-
-            for (unsigned i = 0; i < ab_combinations.size(); ++i) {
-                move_t const& mvA = mvsA[ab_combinations[i].A];
-                bset.reset();
-                bool is_final = a.is_final_state(mvA.dst());
-                for (unsigned j = 0; j < mvsB.size(); ++j) {
-                    if (ab_combinations[i].B[j]) {
-                        bset.insert(mvsB[j].dst());
-                        is_final &= !b.is_final_state(mvsB[j].dst());
-                    }
-                }
-                unsigned new_b;
-                if (bset.empty()) {
-                    new_b = sink_state;
-                }
-                else if (!bs2id.find(bset, new_b)) {
-                    new_b = id2bs.size();
-                    id2bs.push_back(bset);
-                    bs2id.insert(bset, new_b);
-                }
-                unsigned_pair dst(mvA.dst(), new_b);
-                bool is_new = !pair2id.contains(dst);
-                dst_id = get_product_state_id(pair2id, dst, p_state_id);
-                move_t new_move(m, state_id, dst_id, ab_combinations[i].cond);
-                new_moves.push_back(new_move);
-                if (is_new) {
-                    if (is_final) {
-                        new_final_states.push_back(dst_id);
-                    }
-                    todo.push_back(dst);
-                }   
-            }
-        }
-    }
-    
-    
-    if (new_final_states.empty()) {
-        return alloc(automaton_t, m);
-    }
-
-    automaton_t* result = alloc(automaton_t, m, 0, new_final_states, new_moves); 
-
-#if 0
-    result->isEpsilonFree = true;
-    if (A.IsDeterministic)
-        result->isDeterministic = true;    
-    result->EliminateDeadStates();
-#endif
-    return result;
-
-#endif
-    return 0;
 }
 
 #endif