| /dports/graphics/pcl-pointclouds/pcl-pcl-1.12.0/surface/src/on_nurbs/ |
| H A D | fitting_surface_tdm.cpp | 83 m_solver.assign (3 * nrows, 3 * ncp, 1); in assemble()
112 if (m_solver.solve ()) in solve()
131 cp.x = cp_prev.x + damp * (m_solver.x (3 * A + 0, 0) - cp_prev.x); in updateSurf()
132 cp.y = cp_prev.y + damp * (m_solver.x (3 * A + 1, 0) - cp_prev.y); in updateSurf()
245 m_solver.f (row + 0, 0, td (0) * p (0) * weight); in addPointConstraint()
246 m_solver.f (row + 1, 0, td (1) * p (1) * weight); in addPointConstraint()
247 m_solver.f (row + 2, 0, td (2) * p (2) * weight); in addPointConstraint()
256 m_solver.K (row + 0, ci + 0, td (0) * val); in addPointConstraint()
257 m_solver.K (row + 1, ci + 1, td (1) * val); in addPointConstraint()
258 m_solver.K (row + 2, ci + 2, td (2) * val); in addPointConstraint()
[all …]
|
| H A D | global_optimization_tdm.cpp | 94 m_solver.assign (m_nrows, m_ncols, 1); in assemble()
168 m_solver.assign (m_nrows, m_ncols, 1); in assemble()
205 if (m_solver.solve ()) in solve()
670 m_solver.K (row + 0, ci + 0, val); in addParamConstraint()
671 m_solver.K (row + 1, ci + 1, val); in addParamConstraint()
672 m_solver.K (row + 2, ci + 2, val); in addParamConstraint()
763 m_solver.f (row + 0, 0, point (0) * weight); in addPointConstraint()
764 m_solver.f (row + 1, 0, point (1) * weight); in addPointConstraint()
776 m_solver.K (row + 0, ci + 0, val); in addPointConstraint()
777 m_solver.K (row + 1, ci + 1, val); in addPointConstraint()
[all …]
|
| H A D | global_optimization_pdm.cpp | 156 if (m_solver.solve ()) in solve()
503 m_solver.f (row, 0, 0.0); in addParamConstraint()
504 m_solver.f (row, 1, 0.0); in addParamConstraint()
505 m_solver.f (row, 2, 0.0); in addParamConstraint()
666 m_solver.f (row, 0, 0.0); in addCageCornerRegularisation()
667 m_solver.f (row, 1, 0.0); in addCageCornerRegularisation()
668 m_solver.f (row, 2, 0.0); in addCageCornerRegularisation()
681 m_solver.f (row, 0, 0.0); in addCageCornerRegularisation()
682 m_solver.f (row, 1, 0.0); in addCageCornerRegularisation()
683 m_solver.f (row, 2, 0.0); in addCageCornerRegularisation()
[all …]
|
| /dports/math/z3/z3-z3-4.8.13/src/sat/ |
| H A D | sat_elim_eqs.cpp | 26 m_solver(s), in elim_eqs()
93 if (m_solver.m_config.m_drat) { in drat_delete_clause()
120 m_solver.detach_clause(c); in cleanup_clauses()
173 m_solver.del_clause(c); in cleanup_clauses()
179 m_solver.set_conflict(); in cleanup_clauses()
190 m_solver.del_clause(c); in cleanup_clauses()
196 m_solver.del_clause(c); in cleanup_clauses()
232 if (m_solver.m_cut_simplifier) m_solver.m_cut_simplifier->set_root(v, r); in save_elim()
236 …if (m_solver.is_assumption(v) || (m_solver.is_external(v) && (m_solver.is_incremental() || !root_o… in save_elim()
253 m_solver.flush_roots(); in save_elim()
[all …]
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/ |
| H A D | sat_elim_eqs.cpp | 26 m_solver(s), in elim_eqs()
93 if (m_solver.m_config.m_drat) { in drat_delete_clause()
120 m_solver.detach_clause(c); in cleanup_clauses()
173 m_solver.del_clause(c); in cleanup_clauses()
179 m_solver.set_conflict(); in cleanup_clauses()
190 m_solver.del_clause(c); in cleanup_clauses()
196 m_solver.del_clause(c); in cleanup_clauses()
232 if (m_solver.m_cut_simplifier) m_solver.m_cut_simplifier->set_root(v, r); in save_elim()
236 …if (m_solver.is_assumption(v) || (m_solver.is_external(v) && (m_solver.is_incremental() || !root_o… in save_elim()
253 m_solver.flush_roots(); in save_elim()
[all …]
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/fd_solver/ |
| H A D | pb2bv_solver.cpp | 32 mutable ref<solver> m_solver; member in pb2bv_solver
42 m_solver(s), in pb2bv_solver()
69 m_solver->push(); in push_core()
74 m_solver->pop(n); in pop_core()
89 m_solver->collect_statistics(st); in collect_statistics()
93 m_solver->get_model(mdl); in get_model_core()
105 m_solver->get_levels(vars, depth); in get_levels()
109 return m_solver->get_trail(); in get_trail()
151 return m_solver->get_assertion(idx); in get_assertion()
165 m_solver->assert_expr(fml); in flush_assertions()
[all …]
|
| H A D | enum2bv_solver.cpp | 35 ref<solver> m_solver; member in enum2bv_solver
43 m_solver(s), in enum2bv_solver()
66 m_solver->assert_expr(tmp); in assert_expr_core()
68 m_solver->assert_expr(bounds); in assert_expr_core()
73 m_solver->push(); in push_core()
77 m_solver->pop(n); in pop_core()
82 m_solver->updt_params(get_params()); in check_sat_core2()
97 m_solver->get_model(mdl); in get_model_core()
151 m_solver->assert_expr(bounds); in get_consequences_core()
189 m_solver->get_levels(vars, depth); in get_levels()
[all …]
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/fd_solver/ |
| H A D | pb2bv_solver.cpp | 32 mutable ref<solver> m_solver; member in pb2bv_solver
42 m_solver(s), in pb2bv_solver()
69 m_solver->push(); in push_core()
74 m_solver->pop(n); in pop_core()
89 m_solver->collect_statistics(st); in collect_statistics()
93 m_solver->get_model(mdl); in get_model_core()
101 m_solver->get_levels(vars, depth); in get_levels()
105 return m_solver->get_trail(); in get_trail()
147 return m_solver->get_assertion(idx); in get_assertion()
161 m_solver->assert_expr(fml); in flush_assertions()
[all …]
|
| H A D | enum2bv_solver.cpp | 35 ref<solver> m_solver; member in enum2bv_solver
43 m_solver(s), in enum2bv_solver()
66 m_solver->assert_expr(tmp); in assert_expr_core()
68 m_solver->assert_expr(bounds); in assert_expr_core()
73 m_solver->push(); in push_core()
77 m_solver->pop(n); in pop_core()
82 m_solver->updt_params(get_params()); in check_sat_core2()
93 m_solver->get_model(mdl); in get_model_core()
147 m_solver->assert_expr(bounds); in get_consequences_core()
185 m_solver->get_levels(vars, depth); in get_levels()
[all …]
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/spacer/ |
| H A D | spacer_iuc_solver.h | 46 solver& m_solver; variable
76 m_solver(solver),
105 m_solver.get_unsat_core(_core); in get_full_unsat_core()
112 return m_solver.translate(m, p); in translate()
117 void push_params() override { m_solver.push_params(); } in push_params()
118 void pop_params() override { m_solver.pop_params(); } in pop_params()
123 void set_phase(expr* e) override { m_solver.set_phase(e); } in set_phase()
125 void set_phase(phase* p) override { m_solver.set_phase(p); } in set_phase()
138 m_solver.set_progress_callback(callback); in set_progress_callback()
145 return m_solver.display(out, n, es); in display()
[all …]
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/spacer/ |
| H A D | spacer_iuc_solver.h | 46 solver& m_solver; variable
76 m_solver(solver),
105 m_solver.get_unsat_core(_core); in get_full_unsat_core()
112 return m_solver.translate(m, p); in translate()
117 void push_params() override { m_solver.push_params(); } in push_params()
118 void pop_params() override { m_solver.pop_params(); } in pop_params()
121 void assert_expr_core(expr *t) override { m_solver.assert_expr(t); } in assert_expr_core()
134 m_solver.set_progress_callback(callback); in set_progress_callback()
141 return m_solver.display(out, n, es); in display()
150 void get_model_core(model_ref &m) override {m_solver.get_model(m);} in get_model_core()
[all …]
|
| /dports/math/z3/z3-z3-4.8.13/src/nlsat/ |
| H A D | nlsat_scoped_literal_vector.h | 27 solver & m_solver; variable
30 scoped_literal_vector(solver & s):m_solver(s) {} in scoped_literal_vector()
37 m_solver.dec_ref(l); in reset()
42 m_solver.inc_ref(l); in push_back()
46 m_solver.inc_ref(l); in set()
47 m_solver.dec_ref(m_lits[i]); in set()
59 m_solver.dec_ref(m_lits[i]); in shrink()
71 SASSERT(&m_solver == &other.m_solver); in swap()
78 solver & m_solver; variable
84 m_solver.inc_ref(l);
[all …]
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/nlsat/ |
| H A D | nlsat_scoped_literal_vector.h | 27 solver & m_solver; variable
30 scoped_literal_vector(solver & s):m_solver(s) {} in scoped_literal_vector()
37 m_solver.dec_ref(l); in reset()
42 m_solver.inc_ref(l); in push_back()
46 m_solver.inc_ref(l); in set()
47 m_solver.dec_ref(m_lits[i]); in set()
59 m_solver.dec_ref(m_lits[i]); in shrink()
71 SASSERT(&m_solver == &other.m_solver); in swap()
78 solver & m_solver; variable
84 m_solver.inc_ref(l);
[all …]
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/tactic/ |
| H A D | ctx_solver_simplify_tactic.cpp | 89 m_solver.reset(); in cleanup()
106 m_solver.push(); in reduce()
108 m_solver.pop(1); in reduce()
121 m_solver.push(); in reduce()
140 m_solver.pop(1); in reduce()
183 m_solver.push(); in reduce()
275 m_solver.pop(1); in reduce()
285 m_solver.push(); in simplify_bool()
288 m_solver.pop(1); in simplify_bool()
294 m_solver.push(); in simplify_bool()
[all …]
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/tactic/ |
| H A D | ctx_solver_simplify_tactic.cpp | 89 m_solver.reset(); in cleanup()
106 m_solver.push(); in reduce()
108 m_solver.pop(1); in reduce()
121 m_solver.push(); in reduce()
140 m_solver.pop(1); in reduce()
183 m_solver.push(); in reduce()
260 m_solver.pop(1); in reduce()
270 m_solver.push(); in simplify_bool()
273 m_solver.pop(1); in simplify_bool()
279 m_solver.push(); in simplify_bool()
[all …]
|
| /dports/math/z3/z3-z3-4.8.13/src/opt/ |
| H A D | opt_sls_solver.h | 33 ref<solver> m_solver; variable
49 m_solver(s), in sls_solver()
61 m_solver->updt_params(p); in updt_params()
70 m_solver->collect_statistics(st); in collect_statistics()
75 m_solver->assert_expr(t); in assert_expr()
78 m_solver->get_unsat_core(r); in get_unsat_core()
84 return m_solver->get_proof(); in get_proof()
90 m_solver->get_labels(r); in get_labels()
102 m_solver->display(out); in display()
159 m_solver->push(); in push_core()
[all …]
|
| H A D | opt_pareto.cpp | 33 lbool is_sat = m_solver->check_sat(0, nullptr); in operator ()()
36 m_solver->get_model(m_model); in operator ()()
37 solver::scoped_push _s(*m_solver.get()); in operator ()()
44 m_solver->get_labels(m_labels); in operator ()()
52 is_sat = m_solver->check_sat(0, nullptr); in operator ()()
78 m_solver->assert_expr(fml); in mk_dominates()
91 m_solver->assert_expr(fml); in mk_not_dominated_by()
98 solver::scoped_push _s(*m_solver.get()); in operator ()()
99 lbool is_sat = m_solver->check_sat(0, nullptr); in operator ()()
104 m_solver->get_model(m_model); in operator ()()
[all …]
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/opt/ |
| H A D | opt_sls_solver.h | 33 ref<solver> m_solver; variable
49 m_solver(s), in sls_solver()
61 m_solver->updt_params(p); in updt_params()
70 m_solver->collect_statistics(st); in collect_statistics()
75 m_solver->assert_expr(t); in assert_expr()
78 m_solver->get_unsat_core(r); in get_unsat_core()
84 return m_solver->get_proof(); in get_proof()
90 m_solver->get_labels(r); in get_labels()
102 m_solver->display(out); in display()
159 m_solver->push(); in push_core()
[all …]
|
| H A D | opt_pareto.cpp | 33 lbool is_sat = m_solver->check_sat(0, nullptr); in operator ()()
36 m_solver->get_model(m_model); in operator ()()
37 solver::scoped_push _s(*m_solver.get()); in operator ()()
44 m_solver->get_labels(m_labels); in operator ()()
52 is_sat = m_solver->check_sat(0, nullptr); in operator ()()
78 m_solver->assert_expr(fml); in mk_dominates()
91 m_solver->assert_expr(fml); in mk_not_dominated_by()
98 solver::scoped_push _s(*m_solver.get()); in operator ()()
99 lbool is_sat = m_solver->check_sat(0, nullptr); in operator ()()
104 m_solver->get_model(m_model); in operator ()()
[all …]
|
| /dports/math/z3/z3-z3-4.8.13/src/sat/smt/ |
| H A D | sat_dual_solver.cpp | 22 m_solver(m_params, l) in dual_solver()
24 SASSERT(!m_solver.get_config().m_drat); in dual_solver()
29 m_solver.user_push(); in flush()
49 m_solver.user_pop(num_scopes); in pop()
69 w = m_solver.mk_var(); in ext2var()
70 m_solver.set_external(w); in ext2var()
141 m_solver.user_push(); in operator ()()
155 m_solver.user_pop(1); in operator ()()
164 lbool v1 = m_solver.value(v); in display()
177 if (m_solver.value(r) == l_true) in display()
[all …]
|
| /dports/audio/amarok/amarok-3e11ccdd1417e70486eaaa84d8475182eec44c20/src/dynamic/ |
| H A D | BiasedPlaylist.cpp | 44 , m_solver( 0 ) in BiasedPlaylist()
55 , m_solver( 0 ) in BiasedPlaylist()
104 if( m_solver ) { in requestAbort()
105 m_solver->setAutoDelete( true ); in requestAbort()
106 m_solver->requestAbort(); in requestAbort()
107 m_solver = 0; in requestAbort()
117 if( !m_solver ) in startSolver()
195 if( m_solver != sender() ) in solverFinished()
198 Meta::TrackList list = m_solver->solution(); in solverFinished()
207 m_solver->deleteLater(); in solverFinished()
[all …]
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/smt/ |
| H A D | sat_dual_solver.cpp | 26 m_solver(m_params, l) in dual_solver()
28 SASSERT(!m_solver.get_config().m_drat); in dual_solver()
32 m_solver.user_push(); in push()
40 m_solver.user_pop(num_scopes); in pop()
60 w = m_solver.mk_var(); in ext2var()
90 literal root(m_solver.mk_var(), false); in add_root()
109 m_solver.user_push(); in operator ()()
116 for (literal lit : m_solver.get_core()) in operator ()()
125 m_solver.user_pop(1); in operator ()()
134 lbool v1 = m_solver.value(v); in display()
[all …]
|
| /dports/math/gismo/gismo-21.12.0/extensions/gsStructuralAnalysis/ |
| H A D | gsControlDisplacement.h | 38 m_solver(solver), in gsControlDisplacement()
41 m_U = gsVector<T>::Zero(m_solver->numDofs()); in gsControlDisplacement()
47 m_solver->setLoad(m_L + dL); in step()
49 m_solver->setDisplacement(m_U); in step()
51 m_solver->solve(); in step()
53 if (m_solver->converged()) in step()
56 m_U += m_solver->update(); in step()
75 m_solver->reset(); in reset()
79 mutable gsStaticBase<T> * m_solver;
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | smt_implied_equalities.cpp | 97 m_solver.push(); in get_implied_equalities_filter_basic()
100 m_solver.pop(1); in get_implied_equalities_filter_basic()
124 m_solver.push(); in get_implied_equalities_basic()
155 m_solver.push(); in get_implied_equalities_model_based()
174 m_solver.pop(1); in get_implied_equalities_model_based()
336 m_solver.push(); in operator ()()
359 m_solver.pop(1); in operator ()()
392 solver& m_solver;
453 solver& m_solver;
546 m_solver.push();
[all …]
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | smt_implied_equalities.cpp | 97 m_solver.push(); in get_implied_equalities_filter_basic()
100 m_solver.pop(1); in get_implied_equalities_filter_basic()
124 m_solver.push(); in get_implied_equalities_basic()
155 m_solver.push(); in get_implied_equalities_model_based()
174 m_solver.pop(1); in get_implied_equalities_model_based()
336 m_solver.push(); in operator ()()
359 m_solver.pop(1); in operator ()()
392 solver& m_solver;
453 solver& m_solver;
546 m_solver.push();
[all …]
|