GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/example_min_eval.h Lines: 5 5 100.0 %
Date: 2021-03-23 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file example_min_eval.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief utility for minimizing the number of calls to evaluate a term
13
 ** on substitutions with a fixed domain.
14
 **/
15
16
#include "cvc4_private.h"
17
18
#ifndef CVC4__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H
19
#define CVC4__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H
20
21
#include <vector>
22
23
#include "expr/node.h"
24
#include "expr/node_trie.h"
25
26
namespace CVC4 {
27
namespace theory {
28
namespace quantifiers {
29
30
/**
31
 * Virtual evaluator class for Example Minimize Eval.
32
 */
33
class EmeEval
34
{
35
 public:
36
26807
  EmeEval() {}
37
26807
  virtual ~EmeEval() {}
38
  /** Evaluate n given substitution { args -> vals }. */
39
  virtual Node eval(TNode n,
40
                    const std::vector<Node>& args,
41
                    const std::vector<Node>& vals) = 0;
42
};
43
44
/**
45
 * Example Minimize Eval
46
 *
47
 * This class is designed to evaluate a term on a set of substitutions
48
 * with a fixed domain.
49
 *
50
 * Its key feature is that substitutions that are identical over the free
51
 * variables of the term are not recomputed. For example, say I wish to evaluate
52
 * x+5 on substitutions having the domain { x, y }. Then, for the substitutions:
53
 *  { x -> 0, y -> 1 }
54
 *  { x -> 0, y -> 2 }
55
 *  { x -> 0, y -> 3 }
56
 *  { x -> 1, y -> 3 }
57
 * I would only compute the result of 0+5 once. On the other hand, evaluating
58
 * x+y for the above substitutions would require 4 evaluations.
59
 *
60
 * To use this class, call initialize(n,vars) first and then
61
 * evaluate(subs_1) ... evaluate(subs_n) as desired. Details on these methods
62
 * can be found below.
63
 */
64
class ExampleMinEval
65
{
66
 public:
67
  /**
68
   * Initialize this cache to evaluate n on substitutions with domain vars.
69
   * Argument ece is the evaluator object.
70
   */
71
  ExampleMinEval(Node n, const std::vector<Node>& vars, EmeEval* ece);
72
26807
  ~ExampleMinEval() {}
73
  /**
74
   * Return the result of evaluating n * { vars -> subs } where vars is the
75
   * set of variables passed to initialize above.
76
   */
77
  Node evaluate(const std::vector<Node>& subs);
78
79
 private:
80
  /** The node to evaluate */
81
  Node d_evalNode;
82
  /** The domain of substitutions */
83
  std::vector<Node> d_vars;
84
  /** The indices in d_vars that occur free in n */
85
  std::vector<size_t> d_indices;
86
  /**
87
   * The trie of results. This maps subs[d_indices[0]] .. subs[d_indices[j]]
88
   * to the result of the evaluation. For the example at the top of this class,
89
   * this trie would map (0) -> 5, (1) -> 6.
90
   */
91
  NodeTrie d_trie;
92
  /** Pointer to the evaluator object */
93
  EmeEval* d_ece;
94
};
95
96
class TermDbSygus;
97
98
/** An example cache evaluator based on the term database sygus utility */
99
class EmeEvalTds : public EmeEval
100
{
101
 public:
102
26807
  EmeEvalTds(TermDbSygus* tds, TypeNode tn) : d_tds(tds), d_tn(tn) {}
103
26807
  virtual ~EmeEvalTds() {}
104
  /**
105
   * Evaluate n given substitution { args -> vals } using the term database
106
   * sygus evaluateBuiltin function.
107
   */
108
  Node eval(TNode n,
109
            const std::vector<Node>& args,
110
            const std::vector<Node>& vals) override;
111
112
 private:
113
  /** Pointer to the sygus term database */
114
  TermDbSygus* d_tds;
115
  /** The sygus type of the node we will be evaluating */
116
  TypeNode d_tn;
117
};
118
119
}  // namespace quantifiers
120
}  // namespace theory
121
} /* namespace CVC4 */
122
123
#endif