Home
last modified time | relevance | path

Searched refs:model_generator (Results 1 – 25 of 80) sorted by relevance

1234

/dports/math/z3/z3-z3-4.8.13/src/smt/
H A Dsmt_model_generator.cpp41 model_generator::model_generator(ast_manager & m): in model_generator() function in smt::model_generator
49 model_generator::~model_generator() { in ~model_generator()
53 void model_generator::reset() { in reset()
61 void model_generator::init_model() { in init_model()
74 void model_generator::mk_bool_model() { in mk_bool_model()
292 void model_generator::mk_values() { in mk_values()
371 …model_generator::scoped_reset::scoped_reset(model_generator& mg, ptr_vector<model_value_proc>& pro… in scoped_reset()
374 model_generator::scoped_reset::~scoped_reset() { in ~scoped_reset()
399 void model_generator::mk_func_interps() { in mk_func_interps()
482 void model_generator::register_macros() { in register_macros()
[all …]
H A Dsmt_model_generator.h149 virtual app * mk_value(model_generator & m, expr_ref_vector const & values) = 0;
164 … app * mk_value(model_generator & m, expr_ref_vector const & values) override { return m_value; } in mk_value()
172 …app * mk_value(model_generator & m, expr_ref_vector const & values) override { return to_app(value… in mk_value()
179 class model_generator {
209 model_generator& mg;
211 scoped_reset(model_generator& mg, ptr_vector<model_value_proc>& procs);
216 model_generator(ast_manager & m);
217 ~model_generator();
H A Dtheory_special_relations.h159 expr_ref mk_inj(relation& r, model_generator& m);
160 expr_ref mk_class(relation& r, model_generator& m);
161 … expr_ref mk_interval(relation& r, model_generator& mg, unsigned_vector & lo, unsigned_vector& hi);
162 void init_model_lo(relation& r, model_generator& m);
163 void init_model_to(relation& r, model_generator& m);
164 void init_model_po(relation& r, model_generator& m, bool is_reflexive);
165 void init_model_plo(relation& r, model_generator& m);
197 model_value_proc * mk_value(enode * n, model_generator & mg) override;
198 void init_model(model_generator & m) override;
H A Dtheory_fpa.h58 app * mk_value(model_generator & mg, expr_ref_vector const & values) override;
79 app * mk_value(model_generator & mg, expr_ref_vector const & values) override;
107 model_value_proc * mk_value(enode * n, model_generator & mg) override;
111 void init_model(model_generator & m) override;
112 void finalize_model(model_generator & mg) override;
H A Dtheory_char.h79 void init_model(model_generator & mg) override;
80 model_value_proc * mk_value(enode * n, model_generator & mg) override;
H A Dtheory_lra.h82 void init_model(model_generator & m) override;
84 model_value_proc * mk_value(enode * n, model_generator & mg) override;
H A Dsmt_theory.h29 class model_generator; variable
567 virtual void init_model(model_generator & m) { in init_model()
570 virtual void finalize_model(model_generator & m) { in finalize_model()
576 virtual model_value_proc * mk_value(enode * n, model_generator & mg) { in mk_value()
H A Dtheory_array_base.h198 void init_model(model_generator & m) override;
206 void finalize_model(model_generator & m) override;
207 model_value_proc * mk_value(enode * n, model_generator & m) override;
H A Duser_propagator.h119 model_value_proc * mk_value(enode * n, model_generator & mg) override { return nullptr; } in mk_value()
120 void init_model(model_generator & m) override {} in init_model()
H A Dtheory_dl.cpp79 app * mk_value(smt::model_generator & mg, expr_ref_vector const & ) override { in mk_value()
160 void init_model(smt::model_generator & m) override { in init_model()
164 smt::model_value_proc * mk_value(smt::enode * n, smt::model_generator&) override { in mk_value() argument
H A Dtheory_datatype.h137 void init_model(model_generator & m) override;
138 model_value_proc * mk_value(enode * n, model_generator & m) override;
H A Dsmt_types.h55 class model_generator; variable
H A Dtheory_seq_empty.h40 void init_model(model_generator & mg) override { in init_model()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/
H A Dsmt_model_generator.cpp41 model_generator::model_generator(ast_manager & m): in model_generator() function in smt::model_generator
49 model_generator::~model_generator() { in ~model_generator()
53 void model_generator::reset() { in reset()
61 void model_generator::init_model() { in init_model()
74 void model_generator::mk_bool_model() { in mk_bool_model()
292 void model_generator::mk_values() { in mk_values()
371 …model_generator::scoped_reset::scoped_reset(model_generator& mg, ptr_vector<model_value_proc>& pro… in scoped_reset()
374 model_generator::scoped_reset::~scoped_reset() { in ~scoped_reset()
400 void model_generator::mk_func_interps() { in mk_func_interps()
483 void model_generator::register_macros() { in register_macros()
[all …]
H A Dsmt_model_generator.h149 virtual app * mk_value(model_generator & m, expr_ref_vector const & values) = 0;
164 … app * mk_value(model_generator & m, expr_ref_vector const & values) override { return m_value; } in mk_value()
172 …app * mk_value(model_generator & m, expr_ref_vector const & values) override { return to_app(value… in mk_value()
179 class model_generator {
209 model_generator& mg;
211 scoped_reset(model_generator& mg, ptr_vector<model_value_proc>& procs);
216 model_generator(ast_manager & m);
217 ~model_generator();
H A Dtheory_special_relations.h159 expr_ref mk_inj(relation& r, model_generator& m);
160 expr_ref mk_class(relation& r, model_generator& m);
161 … expr_ref mk_interval(relation& r, model_generator& mg, unsigned_vector & lo, unsigned_vector& hi);
162 void init_model_lo(relation& r, model_generator& m);
163 void init_model_to(relation& r, model_generator& m);
164 void init_model_po(relation& r, model_generator& m, bool is_reflexive);
165 void init_model_plo(relation& r, model_generator& m);
197 model_value_proc * mk_value(enode * n, model_generator & mg) override;
198 void init_model(model_generator & m) override;
H A Dtheory_fpa.h59 app * mk_value(model_generator & mg, expr_ref_vector const & values) override;
80 app * mk_value(model_generator & mg, expr_ref_vector const & values) override;
108 model_value_proc * mk_value(enode * n, model_generator & mg) override;
112 void init_model(model_generator & m) override;
113 void finalize_model(model_generator & mg) override;
H A Dtheory_lra.h82 void init_model(model_generator & m) override;
84 model_value_proc * mk_value(enode * n, model_generator & mg) override;
H A Dsmt_theory.h29 class model_generator; variable
561 virtual void init_model(model_generator & m) { in init_model()
564 virtual void finalize_model(model_generator & m) { in finalize_model()
570 virtual model_value_proc * mk_value(enode * n, model_generator & mg) { in mk_value()
H A Dtheory_array_base.h198 void init_model(model_generator & m) override;
206 void finalize_model(model_generator & m) override;
207 model_value_proc * mk_value(enode * n, model_generator & m) override;
H A Duser_propagator.h119 model_value_proc * mk_value(enode * n, model_generator & mg) override { return nullptr; }
120 void init_model(model_generator & m) override {}
H A Dtheory_dl.cpp79 app * mk_value(smt::model_generator & mg, expr_ref_vector const & ) override {
160 void init_model(smt::model_generator & m) override {
164 smt::model_value_proc * mk_value(smt::enode * n, smt::model_generator&) override {
H A Dtheory_datatype.h137 void init_model(model_generator & m) override;
138 model_value_proc * mk_value(enode * n, model_generator & m) override;
H A Dsmt_types.h54 class model_generator; variable
/dports/www/chromium-legacy/chromium-88.0.4324.182/components/feed/core/v2/
H A Dfeed_stream_unittest.cc1121 StreamModelUpdateRequestGenerator model_generator; in TEST_F() local
1122 model_generator.signed_in = false; in TEST_F()
1129 response_translator_.InjectResponse(model_generator.MakeFirstPage(), in TEST_F()
1154 response_translator_.InjectResponse(model_generator.MakeNextPage()); in TEST_F()
1175 model_generator.signed_in = true; in TEST_F()
2574 StreamModelUpdateRequestGenerator model_generator; in TEST_F() local
2575 model_generator.signed_in = false; in TEST_F()
2694 StreamModelUpdateRequestGenerator model_generator; in TEST_F() local
2695 model_generator.signed_in = false; in TEST_F()
2757 StreamModelUpdateRequestGenerator model_generator; in TEST_F() local
[all …]

1234