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