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