1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3 
4 Module Name:
5 
6     fix_dl_var_tactic.h
7 
8 Abstract:
9 
10     Fix a difference logic variable to 0.
11     If the problem is in the difference logic fragment, that is, all arithmetic terms
12     are of the form (x + k), and the arithmetic atoms are of the
13     form x - y <= k or x - y = k. Then, we can set one variable to 0.
14 
15     This is useful because, many bounds can be exposed after this operation is performed.
16 
17 Author:
18 
19     Leonardo (leonardo) 2011-12-29
20 
21 Notes:
22 
23 --*/
24 #pragma once
25 
26 #include "util/params.h"
27 class ast_manager;
28 class tactic;
29 
30 tactic * mk_fix_dl_var_tactic(ast_manager & m, params_ref const & p = params_ref());
31 
32 /*
33   ADD_TACTIC("fix-dl-var", "if goal is in the difference logic fragment, then fix the variable with the most number of occurrences at 0.", "mk_fix_dl_var_tactic(m, p)")
34 */
35 
36