1 /*++ 2 Copyright (c) 2020 Microsoft Corporation 3 4 Module Name: 5 6 value_sweep.h 7 8 Abstract: 9 10 Evaluate terms using different random initial assignments. 11 Return the assignments. 12 13 Author: 14 15 Nikolaj Bjorner 2020-04-27 16 17 --*/ 18 19 #pragma once 20 21 #include "ast/value_generator.h" 22 #include "ast/recfun_decl_plugin.h" 23 #include "ast/datatype_decl_plugin.h" 24 #include "ast/rewriter/th_rewriter.h" 25 26 class value_sweep { 27 typedef vector<ptr_vector<app>> parents_t; 28 29 ast_manager& m; 30 value_generator m_gen; 31 recfun::util m_rec; 32 datatype::util m_dt; 33 th_rewriter m_rewrite; 34 expr_ref_vector m_values; 35 expr_ref_vector m_args; 36 expr_ref_vector m_pinned; 37 unsigned m_rounds; 38 unsigned m_range; 39 random_gen m_rand; 40 41 parents_t m_parents; 42 ptr_vector<expr> m_queue; 43 ptr_vector<expr> m_vars; 44 unsigned m_qhead; 45 unsigned m_vhead; 46 47 void init(expr_ref_vector const& terms); 48 49 void set_value_core(expr* e, expr* v); 50 51 expr* get_value(expr* e) const; 52 53 void unassign(unsigned qhead); 54 55 void propagate_values(); 56 57 bool assign_next_value(); 58 59 bool is_reducible(expr* e) const; 60 61 bool all_args_have_values(app* p) const; 62 63 64 public: 65 value_sweep(ast_manager& m); set_rounds(unsigned r)66 void set_rounds(unsigned r) { m_rounds = r; } set_range(unsigned r)67 void set_range(unsigned r) { m_range = r; } 68 void set_value(expr* e, expr* v); 69 void reset_values(); 70 71 void operator()(expr_ref_vector const& terms, 72 vector<expr_ref_vector>& values); 73 }; 74