results.h

/*
 * Copyright 2016, IST Austria
 *
 * This file is part of Limi.
 *
 * Limi is free software: you can redistribute it and/or modify
 * it under the terms of the GNU Lesser General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * Limi is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public License
 * along with Limi.  If not, see <http://www.gnu.org/licenses/>.
 */

#ifndef LIMI_RESULTS_H
#define LIMI_RESULTS_H

#include <unordered_set>
#include <list>
#include <algorithm>
#include "generics.h"

namespace Limi {

template<class Symbol>
struct counterexample_chain {
  Symbol current;
  std::shared_ptr<counterexample_chain> parent;
  
  counterexample_chain(const Symbol& current, const std::shared_ptr<counterexample_chain>& parent) :
  current(current), parent(parent) {  }
  
  std::list<Symbol> to_list() const {
    std::list<Symbol> result;
    const counterexample_chain* c = this;
    while (c) {
      result.push_front(c->current);
      c = c->parent.get();
    }
    return result;
  }
  
  std::vector<Symbol> to_vector() const {
    std::vector<Symbol> result;
    const counterexample_chain* c = this;
    while (c) {
      result.push_back(c->current);
      c = c->parent.get();
    }
    std::reverse(result.begin(), result.end());
    return result;
  }

private:
};


template <class Symbol>
struct inclusion_result {
  bool included = false;
  bool bound_hit = false;
  std::vector<Symbol> counter_example;
  
  void filter_trace(std::function<bool(Symbol)> to_remove) {
    counter_example.erase( std::remove_if(counter_example.begin(), counter_example.end(), to_remove), std::end(counter_example));
  }
    
  unsigned max_bound = 0;
    
  void print_long(std::ostream& stream, const printer_base<Symbol>& symbol_printer) {
    if (included)
      stream << "Included" << std::endl;
    else {
      stream << "Not Included";
      if (bound_hit) stream << "; bound";
      stream << std::endl;
      for (const auto& s : counter_example) {
        stream << symbol_printer(s);
        //s.symbol->instr_id->printPretty(lout, nullptr, pp);
        stream << std::endl;
      }
    }
  }
};


}

#endif //LIMI_RESULTS_H