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