1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 add_bounds.h 7 8 Abstract: 9 10 Tactic for bounding unbounded variables. 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2011-06-30. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include "util/params.h" 22 23 class ast_manager; 24 class goal; 25 class tactic; 26 class probe; 27 28 bool is_unbounded(goal const & g); 29 probe * mk_is_unbounded_probe(); 30 31 tactic * mk_add_bounds_tactic(ast_manager & m, params_ref const & p = params_ref()); 32 33 /* 34 ADD_TACTIC("add-bounds", "add bounds to unbounded variables (under approximation).", "mk_add_bounds_tactic(m, p)") 35 ADD_PROBE("is-unbounded", "true if the goal contains integer/real constants that do not have lower/upper bounds.", "mk_is_unbounded_probe()") 36 */ 37 38