Head

GCC Code Coverage Report

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


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Utility for minimizing the number of calls to evaluate a term
 * on substitutions with a fixed domain.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H
#define CVC5__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H

#include <vector>

#include "expr/node.h"
#include "expr/node_trie.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

/**
 * Virtual evaluator class for Example Minimize Eval.
 */
class EmeEval
{
 public:
  EmeEval() {}
  virtual ~EmeEval() {}
  /** Evaluate n given substitution { args -> vals }. */
  virtual Node eval(TNode n,
                    const std::vector<Node>& args,
                    const std::vector<Node>& vals) = 0;
};

/**
 * Example Minimize Eval
 *
 * This class is designed to evaluate a term on a set of substitutions
 * with a fixed domain.
 *
 * Its key feature is that substitutions that are identical over the free
 * variables of the term are not recomputed. For example, say I wish to evaluate
 * x+5 on substitutions having the domain { x, y }. Then, for the substitutions:
 *  { x -> 0, y -> 1 }
 *  { x -> 0, y -> 2 }
 *  { x -> 0, y -> 3 }
 *  { x -> 1, y -> 3 }
 * I would only compute the result of 0+5 once. On the other hand, evaluating
 * x+y for the above substitutions would require 4 evaluations.
 *
 * To use this class, call initialize(n,vars) first and then
 * evaluate(subs_1) ... evaluate(subs_n) as desired. Details on these methods
 * can be found below.
 */
class ExampleMinEval
{
 public:
  /**
   * Initialize this cache to evaluate n on substitutions with domain vars.
   * Argument ece is the evaluator object.
   */
  ExampleMinEval(Node n, const std::vector<Node>& vars, EmeEval* ece);
  ~ExampleMinEval() {}
  /**
   * Return the result of evaluating n * { vars -> subs } where vars is the
   * set of variables passed to initialize above.
   */
  Node evaluate(const std::vector<Node>& subs);

 private:
  /** The node to evaluate */
  Node d_evalNode;
  /** The domain of substitutions */
  std::vector<Node> d_vars;
  /** The indices in d_vars that occur free in n */
  std::vector<size_t> d_indices;
  /**
   * The trie of results. This maps subs[d_indices[0]] .. subs[d_indices[j]]
   * to the result of the evaluation. For the example at the top of this class,
   * this trie would map (0) -> 5, (1) -> 6.
   */
  NodeTrie d_trie;
  /** Pointer to the evaluator object */
  EmeEval* d_ece;
};

class TermDbSygus;

/** An example cache evaluator based on the term database sygus utility */
class EmeEvalTds : public EmeEval
{
 public:
  EmeEvalTds(TermDbSygus* tds, TypeNode tn) : d_tds(tds), d_tn(tn) {}
  virtual ~EmeEvalTds() {}
  /**
   * Evaluate n given substitution { args -> vals } using the term database
   * sygus evaluateBuiltin function.
   */
  Node eval(TNode n,
            const std::vector<Node>& args,
            const std::vector<Node>& vals) override;

 private:
  /** Pointer to the sygus term database */
  TermDbSygus* d_tds;
  /** The sygus type of the node we will be evaluating */
  TypeNode d_tn;
};

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5

#endif


Generated by: GCOVR (Version 3.2)

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