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