axiom_evaluator.h 1.07 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41
#ifndef SEARCH_SYMPLE_AXIOMS_AXIOM_EVALUATOR_H_
#define SEARCH_SYMPLE_AXIOMS_AXIOM_EVALUATOR_H_

#include <meddly.h>
#include <map>
#include <memory>
#include <vector>

class AbstractTask;

namespace symple {
class SymVariables;

class SymAxiomEvaluator {
 protected:
  std::shared_ptr<SymVariables> sym_vars;
  std::shared_ptr<AbstractTask> task;
  std::vector<int> axiom_body_layer;  // max. layer of vars in the body
  std::map<int, MEDDLY::dd_edge> primary_representation;

  bool is_primary(int var) const;
  bool is_in_body(int var, int axiom_id) const;
  bool is_trivial(int axiom_id) const;
  int get_axiom_head(int axiom_id) const;

  MEDDLY::dd_edge get_body_evmdd(int axiom_id) const;
  void create_axiom_body_layer();

  void create_primary_representation(int layer);
  void create_primary_representation();

 public:
  SymAxiomEvaluator(std::shared_ptr<SymVariables> sym_vars,
                    std::shared_ptr<AbstractTask> task);

  MEDDLY::dd_edge get_primary_representation(int var, int val) const;
};

}  // namespace symple

#endif /* SEARCH_SYMPLE_AXIOMS_AXIOM_EVALUATOR_H_ */