GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_grammar_red.h Lines: 2 2 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_grammar_red.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
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 sygus_grammar_red
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
18
#define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
19
20
#include <map>
21
#include <vector>
22
23
#include "expr/node.h"
24
25
namespace CVC4 {
26
namespace theory {
27
namespace quantifiers {
28
29
class TermDbSygus;
30
31
/** SygusRedundantCons
32
 *
33
 * This class computes the subset of indices of the constructors of a sygus type
34
 * that are redundant. To use this class, first call initialize( qe, tn ),
35
 * where tn is a sygus tn. Then, use getRedundant and/or isRedundant to get the
36
 * indicies of the constructors of tn that are redundant.
37
 */
38
class SygusRedundantCons
39
{
40
 public:
41
729
  SygusRedundantCons() {}
42
729
  ~SygusRedundantCons() {}
43
  /** register type tn
44
   *
45
   * qe : pointer to the quantifiers engine,
46
   * tn : the (sygus) type to compute redundant constructors for
47
   */
48
  void initialize(TermDbSygus* tds, TypeNode tn);
49
  /** Get the indices of the redundant constructors of the register type */
50
  void getRedundant(std::vector<unsigned>& indices);
51
  /**
52
   * This function returns true if the i^th constructor of the registered type
53
   * is redundant.
54
   */
55
  bool isRedundant(unsigned i);
56
57
 private:
58
  /** the registered type */
59
  TypeNode d_type;
60
  /** redundant status
61
   *
62
   * For each constructor, status indicating whether the constructor is
63
   * redundant, where:
64
   *
65
   * 0 : not redundant,
66
   * 1 : redundant since another constructor can be used to construct values for
67
   * this constructor.
68
   *
69
   * For example, for grammar:
70
   *   A -> C > B | B < C | not D
71
   *   B -> x | y
72
   *   C -> 0 | 1 | C+C
73
   *   D -> B >= C
74
   * If A is register with this class, then we store may store { 0, 1, 0 },
75
   * noting that the second constructor of A can be simulated with the first.
76
   * Notice that the third constructor is not considered redundant.
77
   */
78
  std::vector<int> d_sygus_red_status;
79
  /**
80
   * Map from constructor indices to the generic term for that constructor,
81
   * where the generic term for a constructor is the (canonical) term returned
82
   * by a call to TermDbSygus::mkGeneric.
83
   */
84
  std::map<unsigned, Node> d_gen_terms;
85
  /**
86
   * Map from the rewritten form of generic terms for constructors of the
87
   * registered type to their corresponding constructor index.
88
   */
89
  std::map<Node, unsigned> d_gen_cons;
90
  /** get generic list
91
   *
92
   * This function constructs all well-typed variants of a term of the form
93
   *    op( x1, ..., xn )
94
   * where op is the builtin operator for dt[c], and xi = pre[i] for i=1,...,n.
95
   *
96
   * It constructs a list of terms of the form g * sigma, where sigma
97
   * is an automorphism on { x1...xn } such that for all xi -> xj in sigma,
98
   * the type for arguments i and j of dt[c] are the same. We store this
99
   * list of terms in terms.
100
   *
101
   * This function recurses on the arguments of g, index is the current argument
102
   * we are processing, and pre stores the current arguments of
103
   *
104
   * For example, for a sygus grammar
105
   *   A -> and( A, A, B )
106
   *   B -> false
107
   * passing arguments such that g=and( x1, x2, x3 ) to this function will add:
108
   *   and( x1, x2, x3 ) and and( x2, x1, x3 )
109
   * to terms.
110
   */
111
  void getGenericList(TermDbSygus* tds,
112
                      const DType& dt,
113
                      unsigned c,
114
                      unsigned index,
115
                      std::map<int, Node>& pre,
116
                      std::vector<Node>& terms);
117
};
118
119
} /* CVC4::theory::quantifiers namespace */
120
} /* CVC4::theory namespace */
121
} /* CVC4 namespace */
122
123
#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H */