1 /********************* */ 2 /*! \file candidate_rewrite_database.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 candidate_rewrite_database 13 **/ 14 15 #include "cvc4_private.h" 16 17 #ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H 18 #define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H 19 20 #include <map> 21 #include <memory> 22 #include <unordered_set> 23 #include <vector> 24 #include "theory/quantifiers/candidate_rewrite_filter.h" 25 #include "theory/quantifiers/expr_miner.h" 26 #include "theory/quantifiers/sygus_sampler.h" 27 28 namespace CVC4 { 29 namespace theory { 30 namespace quantifiers { 31 32 /** CandidateRewriteDatabase 33 * 34 * This maintains the necessary data structures for generating a database 35 * of candidate rewrite rules (see Reynolds et al "Rewrites for SMT Solvers 36 * Using Syntax-Guided Enumeration" SMT 2018). The primary responsibilities 37 * of this class are to perform the "equivalence checking" and "congruence 38 * and matching filtering" in Figure 1. The equivalence checking is done 39 * through a combination of the sygus sampler object owned by this class 40 * and the calls made to copies of the SmtEngine in ::addTerm. The rewrite 41 * rule filtering (based on congruence, matching, variable ordering) is also 42 * managed by the sygus sampler object. 43 */ 44 class CandidateRewriteDatabase : public ExprMiner 45 { 46 public: 47 CandidateRewriteDatabase(); ~CandidateRewriteDatabase()48 ~CandidateRewriteDatabase() {} 49 /** Initialize this class */ 50 void initialize(const std::vector<Node>& var, 51 SygusSampler* ss = nullptr) override; 52 /** Initialize this class 53 * 54 * Serves the same purpose as the above function, but we will be using 55 * sygus to enumerate terms and generate samples. 56 * 57 * qe : pointer to quantifiers engine. We use the sygus term database of this 58 * quantifiers engine, and the extended rewriter of the corresponding term 59 * database when computing candidate rewrites, 60 * f : a term of some SyGuS datatype type whose values we will be 61 * testing under the free variables in the grammar of f. This is the 62 * "candidate variable" CegConjecture::d_candidates. 63 */ 64 void initializeSygus(const std::vector<Node>& vars, 65 QuantifiersEngine* qe, 66 Node f, 67 SygusSampler* ss = nullptr); 68 /** add term 69 * 70 * Notifies this class that the solution sol was enumerated. This may 71 * cause a candidate-rewrite to be printed on the output stream out. 72 * We return true if the term sol is distinct (up to equivalence) with 73 * all previous terms added to this class. The argument rew_print is set to 74 * true if this class printed a rewrite involving sol. 75 * 76 * If the flag rec is true, then we also recursively add all subterms of sol 77 * to this class as well. 78 */ 79 bool addTerm(Node sol, bool rec, std::ostream& out, bool& rew_print); 80 bool addTerm(Node sol, bool rec, std::ostream& out); 81 bool addTerm(Node sol, std::ostream& out) override; 82 /** sets whether this class should output candidate rewrites it finds */ 83 void setSilent(bool flag); 84 /** set the (extended) rewriter used by this class */ 85 void setExtendedRewriter(ExtendedRewriter* er); 86 87 private: 88 /** reference to quantifier engine */ 89 QuantifiersEngine* d_qe; 90 /** (required) pointer to the sygus term database of d_qe */ 91 TermDbSygus* d_tds; 92 /** an extended rewriter object */ 93 ExtendedRewriter* d_ext_rewrite; 94 /** the function-to-synthesize we are testing (if sygus) */ 95 Node d_candidate; 96 /** whether we are using sygus */ 97 bool d_using_sygus; 98 /** candidate rewrite filter */ 99 CandidateRewriteFilter d_crewrite_filter; 100 /** the cache for results of addTerm */ 101 std::unordered_map<Node, bool, NodeHashFunction> d_add_term_cache; 102 /** if true, we silence the output of candidate rewrites */ 103 bool d_silent; 104 }; 105 106 /** 107 * This class generates and stores candidate rewrite databases for multiple 108 * types as needed. 109 */ 110 class CandidateRewriteDatabaseGen 111 { 112 public: 113 /** constructor 114 * 115 * vars : the variables we are testing substitutions for, for all types, 116 * nsamples : number of sample points this class will test for all types. 117 */ 118 CandidateRewriteDatabaseGen(std::vector<Node>& vars, unsigned nsamples); 119 /** add term 120 * 121 * This registers term n with this class. We generate the candidate rewrite 122 * database of the appropriate type (if not allocated already), and register 123 * n with this database. This may result in "candidate-rewrite" being 124 * printed on the output stream out. We return true if the term sol is 125 * distinct (up to equivalence) with all previous terms added to this class. 126 */ 127 bool addTerm(Node n, std::ostream& out); 128 129 private: 130 /** reference to quantifier engine */ 131 QuantifiersEngine* d_qe; 132 /** the variables */ 133 std::vector<Node> d_vars; 134 /** sygus sampler object for each type */ 135 std::map<TypeNode, SygusSampler> d_sampler; 136 /** the number of samples */ 137 unsigned d_nsamples; 138 /** candidate rewrite databases for each type */ 139 std::map<TypeNode, CandidateRewriteDatabase> d_cdbs; 140 /** an extended rewriter object */ 141 ExtendedRewriter d_ext_rewrite; 142 }; 143 144 } /* CVC4::theory::quantifiers namespace */ 145 } /* CVC4::theory namespace */ 146 } /* CVC4 namespace */ 147 148 #endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H */ 149