Branch data Line data Source code
1 : : /****************************************************************************** 2 : : * Top contributors (to current version): 3 : : * Andrew Reynolds, Aina Niemetz 4 : : * 5 : : * This file is part of the cvc5 project. 6 : : * 7 : : * Copyright (c) 2009-2024 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 : : * Expression miner manager, which manages individual expression miners. 14 : : */ 15 : : 16 : : #include "cvc5_private.h" 17 : : 18 : : #ifndef CVC5__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H 19 : : #define CVC5__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H 20 : : 21 : : #include "expr/node.h" 22 : : #include "smt/env_obj.h" 23 : : #include "theory/quantifiers/solution_filter.h" 24 : : 25 : : namespace cvc5::internal { 26 : : namespace theory { 27 : : namespace quantifiers { 28 : : 29 : : /** 30 : : * ExpressionMinerManager 31 : : * 32 : : * NOTE: this should be renamed to "solution filter". 33 : : */ 34 : : class ExpressionMinerManager : protected EnvObj 35 : : { 36 : : public: 37 : : ExpressionMinerManager(Env& env); 38 : 1004 : ~ExpressionMinerManager() {} 39 : : /** Initialize this class, sygus version 40 : : * 41 : : * Initializes this class, informing it that the terms added to this class 42 : : * via calls to addTerm will be generated by the grammar of f. The method 43 : : * takes a pointer to the quantifiers engine qe. If the argument useSygusType 44 : : * is true, the terms added to this class are the sygus datatype terms. 45 : : * If useSygusType is false, the terms are the builtin equivalent of these 46 : : * terms. The argument nsamples is used to initialize the sampler. 47 : : */ 48 : : void initializeSygus(const TypeNode& tn); 49 : : /** add term 50 : : * 51 : : * Expression miners may print information on the output stream out, for 52 : : * instance, candidate-rewrites. The method returns true if the term sol is 53 : : * distinct (up to T-equivalence) with all previous terms added to this class, 54 : : * which is computed based on the miners that this manager enables. 55 : : */ 56 : : bool addTerm(Node sol); 57 : : 58 : : private: 59 : : /** filter strong solutions (--sygus-filter-sol=strong) */ 60 : : void enableFilterStrongSolutions(); 61 : : /** filter weak solutions (--sygus-filter-sol=weak) */ 62 : : void enableFilterWeakSolutions(); 63 : : /** whether we are filtering solutions based on logical strength */ 64 : : bool d_doFilterLogicalStrength; 65 : : /** solution filter based on logical strength */ 66 : : SolutionFilterStrength d_sols; 67 : : /** The variables */ 68 : : std::vector<Node> d_vars; 69 : : }; 70 : : 71 : : } // namespace quantifiers 72 : : } // namespace theory 73 : : } // namespace cvc5::internal 74 : : 75 : : #endif /* CVC5__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H */