GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/datatypes/sygus_simple_sym.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_simple_sym.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 Simple symmetry breaking for sygus.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
18
#define CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
19
20
#include "expr/dtype.h"
21
#include "theory/quantifiers/sygus/term_database_sygus.h"
22
23
namespace CVC4 {
24
namespace theory {
25
namespace datatypes {
26
27
/** SygusSimpleSymBreak
28
 *
29
 * This class implements queries that can be queried statically about sygus
30
 * grammars, for example, concerning which constructors need not appear at
31
 * argument positions of others. This is used by the sygus extension of the
32
 * quantifier-free datatypes procedure for adding symmetry breaking lemmas.
33
 * We call this class of techniques "simple static symmetry breaking". These
34
 * techniques have the advantage over "dynamic symmetry breaking" (blocking
35
 * redundant solutions on demand in datatypes_sygus.h) in that we can design
36
 * efficient encodings of symmetry breaking constraints, whereas dynamic
37
 * symmetry breaking may in the worst case block solutions one by one.
38
 */
39
class SygusSimpleSymBreak
40
{
41
 public:
42
  SygusSimpleSymBreak(quantifiers::TermDbSygus* tds);
43
2188
  ~SygusSimpleSymBreak() {}
44
  /** consider argument kind
45
   *
46
   * This method returns false if the arg^th argument of terms of parent kind
47
   * pk need not be of kind k. The type tnp is the sygus type of type
48
   * containing pk, and tn is the sygus type of the arg^th argument of the
49
   * constructor whose builtin kind is pk.
50
   *
51
   * For example, given grammar:
52
   *   A -> A + A | 0 | 1 | x | -A
53
   * This method will return false for inputs such as:
54
   *   A, A, -, -, 0  (due to cancelling of double unary minus)
55
   *   A, A, +, +, 1  (due to commutativity of addition, we can assume all
56
   *                   nested + occurs in the 0^th argument)
57
   */
58
  bool considerArgKind(TypeNode tn, TypeNode tnp, Kind k, Kind pk, int arg);
59
  /** consider constant
60
   *
61
   * Similar to the above function, this method returns false if the arg^th
62
   * argument of terms of parent kind pk need not be the constant c. The type
63
   * tnp is the sygus type of type containing pk, and tn is the sygus type of
64
   * the arg^th argument of the constructor whose builtin kind is pk.
65
   *
66
   * For example, given grammar:
67
   *   A -> B * B | A + A | 0 | 1 | x | -A
68
   *   B -> 0 | x
69
   * This method will return false for inputs such as:
70
   *   A, A, 0, +, 0 (due to identity of addition with zero)
71
   *   B, A, 0, *, 0 (due to simplification 0*x --> 0, and 0 is generated by A)
72
   */
73
  bool considerConst(TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg);
74
  /** solve for argument
75
   *
76
   * If this method returns a non-negative integer n, then all terms at
77
   * the arg^th position of the cindex^th constructor of sygus type tnp need
78
   * only be of the n^th constructor of that argument.
79
   *
80
   * For example, given grammar:
81
   *   A -> A - A | A + A | 0 | 1 | x | y
82
   * Say solveForArgument(A, 0, 0)=2. This indicates that all terms of the form
83
   * x1-x2 need only be such that x1 is 0.
84
   */
85
  int solveForArgument(TypeNode tnp, unsigned cindex, unsigned arg);
86
87
 private:
88
  /** Pointer to the sygus term database */
89
  quantifiers::TermDbSygus* d_tds;
90
  /** return the index of the first argument position of c that has type tn */
91
  int getFirstArgOccurrence(const DTypeConstructor& c, TypeNode tn);
92
  /**
93
   * Helper function for consider const above, pdt is the datatype of the type
94
   * of tnp.
95
   */
96
  bool considerConst(const DType& pdt, TypeNode tnp, Node c, Kind pk, int arg);
97
};
98
99
}  // namespace datatypes
100
}  // namespace theory
101
}  // namespace CVC4
102
103
#endif /* CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H */