1 /*++ 2 Copyright (c) 2015 Microsoft Corporation 3 4 Module Name: 5 6 eq2bv_tactic.h 7 8 Abstract: 9 10 Extract integer variables that are used as finite domain indicators. 11 The integer variables can only occur in equalities. 12 13 Author: 14 15 Nikolaj Bjorner (nbjorner) 2015-8-19 16 17 Notes: 18 19 --*/ 20 #pragma once 21 22 #include "util/params.h" 23 class ast_manager; 24 class tactic; 25 26 tactic * mk_eq2bv_tactic(ast_manager & m); 27 28 /* 29 ADD_TACTIC("eq2bv", "convert integer variables used as finite domain elements to bit-vectors.", "mk_eq2bv_tactic(m)") 30 */ 31 32 33