mirror of
				https://github.com/Z3Prover/z3
				synced 2025-11-04 13:29:11 +00:00 
			
		
		
		
	address compilation warnings of unused parameters, add shorthands to set parameters on Optimize
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
		
							parent
							
								
									153106a6a7
								
							
						
					
					
						commit
						d4410d0872
					
				
					 4 changed files with 43 additions and 5 deletions
				
			
		| 
						 | 
					@ -53,6 +53,47 @@ namespace Microsoft.Z3
 | 
				
			||||||
            }
 | 
					            }
 | 
				
			||||||
        }
 | 
					        }
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
						/// <summary>
 | 
				
			||||||
 | 
						/// Sets parameter on the optimize solver
 | 
				
			||||||
 | 
						/// </summary>
 | 
				
			||||||
 | 
						public void Set(string name, bool value) { Parameters = Context.MkParams().Add(name, value); }
 | 
				
			||||||
 | 
						/// <summary>
 | 
				
			||||||
 | 
						/// Sets parameter on the optimize solver
 | 
				
			||||||
 | 
						/// </summary>
 | 
				
			||||||
 | 
						public void Set(string name, uint value) { Parameters = Context.MkParams().Add(name, value); }
 | 
				
			||||||
 | 
						/// <summary>
 | 
				
			||||||
 | 
						/// Sets parameter on the optimize solver
 | 
				
			||||||
 | 
						/// </summary>
 | 
				
			||||||
 | 
						public void Set(string name, double value) { Parameters = Context.MkParams().Add(name, value); }
 | 
				
			||||||
 | 
						/// <summary>
 | 
				
			||||||
 | 
						/// Sets parameter on the optimize solver
 | 
				
			||||||
 | 
						/// </summary>
 | 
				
			||||||
 | 
						public void Set(string name, string value) { Parameters = Context.MkParams().Add(name, value); }
 | 
				
			||||||
 | 
						/// <summary>
 | 
				
			||||||
 | 
						/// Sets parameter on the optimize solver
 | 
				
			||||||
 | 
						/// </summary>
 | 
				
			||||||
 | 
						public void Set(string name, Symbol value) { Parameters = Context.MkParams().Add(name, value); }
 | 
				
			||||||
 | 
						/// <summary>
 | 
				
			||||||
 | 
						/// Sets parameter on the optimize solver
 | 
				
			||||||
 | 
						/// </summary>
 | 
				
			||||||
 | 
						public void Set(Symbol name, bool value) { Parameters = Context.MkParams().Add(name, value); }
 | 
				
			||||||
 | 
						/// <summary>
 | 
				
			||||||
 | 
						/// Sets parameter on the optimize solver
 | 
				
			||||||
 | 
						/// </summary>
 | 
				
			||||||
 | 
						public void Set(Symbol name, uint value) { Parameters = Context.MkParams().Add(name, value); }
 | 
				
			||||||
 | 
						/// <summary>
 | 
				
			||||||
 | 
						/// Sets parameter on the optimize solver
 | 
				
			||||||
 | 
						/// </summary>
 | 
				
			||||||
 | 
						public void Set(Symbol name, double value) { Parameters = Context.MkParams().Add(name, value); }
 | 
				
			||||||
 | 
						/// <summary>
 | 
				
			||||||
 | 
						/// Sets parameter on the optimize solver
 | 
				
			||||||
 | 
						/// </summary>
 | 
				
			||||||
 | 
						public void Set(Symbol name, string value) { Parameters = Context.MkParams().Add(name, value); }
 | 
				
			||||||
 | 
						/// <summary>
 | 
				
			||||||
 | 
						/// Sets parameter on the optimize solver
 | 
				
			||||||
 | 
						/// </summary>
 | 
				
			||||||
 | 
						public void Set(Symbol name, Symbol value) { Parameters = Context.MkParams().Add(name, value); }
 | 
				
			||||||
 | 
					
 | 
				
			||||||
        /// <summary>
 | 
					        /// <summary>
 | 
				
			||||||
        /// Retrieves parameter descriptions for Optimize solver.
 | 
					        /// Retrieves parameter descriptions for Optimize solver.
 | 
				
			||||||
        /// </summary>
 | 
					        /// </summary>
 | 
				
			||||||
| 
						 | 
					
 | 
				
			||||||
| 
						 | 
					@ -605,7 +605,6 @@ bool array_recognizers::is_const(expr* e, expr*& v) const {
 | 
				
			||||||
}
 | 
					}
 | 
				
			||||||
 | 
					
 | 
				
			||||||
bool array_recognizers::is_store_ext(expr* _e, expr_ref& a, expr_ref_vector& args, expr_ref& value) {
 | 
					bool array_recognizers::is_store_ext(expr* _e, expr_ref& a, expr_ref_vector& args, expr_ref& value) {
 | 
				
			||||||
    ast_manager& m = a.m();
 | 
					 | 
				
			||||||
    if (is_store(_e)) {
 | 
					    if (is_store(_e)) {
 | 
				
			||||||
        app* e = to_app(_e);
 | 
					        app* e = to_app(_e);
 | 
				
			||||||
        a = e->get_arg(0);
 | 
					        a = e->get_arg(0);
 | 
				
			||||||
| 
						 | 
					
 | 
				
			||||||
| 
						 | 
					@ -2508,13 +2508,12 @@ namespace sat {
 | 
				
			||||||
        TRACE("sat_lemma", tout << "new lemma size: " << m_lemma.size() << "\n" << m_lemma << "\n";);
 | 
					        TRACE("sat_lemma", tout << "new lemma size: " << m_lemma.size() << "\n" << m_lemma << "\n";);
 | 
				
			||||||
 | 
					
 | 
				
			||||||
        unsigned new_scope_lvl       = 0;
 | 
					        unsigned new_scope_lvl       = 0;
 | 
				
			||||||
        bool sub_min = false, res_min = false;
 | 
					 | 
				
			||||||
        if (!m_lemma.empty()) {
 | 
					        if (!m_lemma.empty()) {
 | 
				
			||||||
            if (m_config.m_minimize_lemmas) {
 | 
					            if (m_config.m_minimize_lemmas) {
 | 
				
			||||||
                res_min = minimize_lemma();
 | 
					                minimize_lemma();
 | 
				
			||||||
                reset_lemma_var_marks();
 | 
					                reset_lemma_var_marks();
 | 
				
			||||||
                if (m_config.m_dyn_sub_res)
 | 
					                if (m_config.m_dyn_sub_res)
 | 
				
			||||||
                    sub_min = dyn_sub_res();
 | 
					                    dyn_sub_res();
 | 
				
			||||||
                TRACE("sat_lemma", tout << "new lemma (after minimization) size: " << m_lemma.size() << "\n" << m_lemma << "\n";);
 | 
					                TRACE("sat_lemma", tout << "new lemma (after minimization) size: " << m_lemma.size() << "\n" << m_lemma << "\n";);
 | 
				
			||||||
            }
 | 
					            }
 | 
				
			||||||
            else
 | 
					            else
 | 
				
			||||||
| 
						 | 
					
 | 
				
			||||||
| 
						 | 
					@ -135,7 +135,6 @@ void special_relations_tactic::operator()(goal_ref const & g, goal_ref_buffer &
 | 
				
			||||||
    func_decl_replace replace(m);
 | 
					    func_decl_replace replace(m);
 | 
				
			||||||
    unsigned_vector to_delete;
 | 
					    unsigned_vector to_delete;
 | 
				
			||||||
    for(auto const& kv : goal_features) {
 | 
					    for(auto const& kv : goal_features) {
 | 
				
			||||||
        func_decl* sp = nullptr;
 | 
					 | 
				
			||||||
        sr_property feature = kv.m_value.m_sp_features;
 | 
					        sr_property feature = kv.m_value.m_sp_features;
 | 
				
			||||||
        switch (feature) {
 | 
					        switch (feature) {
 | 
				
			||||||
        case sr_po:
 | 
					        case sr_po:
 | 
				
			||||||
| 
						 | 
					
 | 
				
			||||||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue