1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 probe_arith.h 7 8 Abstract: 9 10 Some probes for arithmetic problems. 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2012-03-01. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 class probe; 22 probe * mk_arith_avg_bw_probe(); 23 probe * mk_arith_max_bw_probe(); 24 probe * mk_arith_avg_degree_probe(); 25 probe * mk_arith_max_degree_probe(); 26 27 /* 28 ADD_PROBE("arith-max-deg", "max polynomial total degree of an arithmetic atom.", "mk_arith_max_degree_probe()") 29 ADD_PROBE("arith-avg-deg", "avg polynomial total degree of an arithmetic atom.", "mk_arith_avg_degree_probe()") 30 ADD_PROBE("arith-max-bw", "max coefficient bit width.", "mk_arith_max_bw_probe()") 31 ADD_PROBE("arith-avg-bw", "avg coefficient bit width.", "mk_arith_avg_bw_probe()") 32 */ 33 34 probe * mk_is_qflia_probe(); 35 probe * mk_is_qfauflia_probe(); 36 probe * mk_is_qflra_probe(); 37 probe * mk_is_qflira_probe(); 38 probe * mk_is_ilp_probe(); 39 probe * mk_is_mip_probe(); 40 41 /* 42 ADD_PROBE("is-qflia", "true if the goal is in QF_LIA.", "mk_is_qflia_probe()") 43 ADD_PROBE("is-qfauflia", "true if the goal is in QF_AUFLIA.", "mk_is_qfauflia_probe()") 44 ADD_PROBE("is-qflra", "true if the goal is in QF_LRA.", "mk_is_qflra_probe()") 45 ADD_PROBE("is-qflira", "true if the goal is in QF_LIRA.", "mk_is_qflira_probe()") 46 ADD_PROBE("is-ilp", "true if the goal is ILP.", "mk_is_ilp_probe()") 47 */ 48 49 probe * mk_is_qfnia_probe(); 50 probe * mk_is_qfnra_probe(); 51 probe * mk_is_nia_probe(); 52 probe * mk_is_nra_probe(); 53 probe * mk_is_nira_probe(); 54 probe * mk_is_lia_probe(); 55 probe * mk_is_lra_probe(); 56 probe * mk_is_lira_probe(); 57 probe * mk_is_qfufnra_probe(); 58 59 /* 60 ADD_PROBE("is-qfnia", "true if the goal is in QF_NIA (quantifier-free nonlinear integer arithmetic).", "mk_is_qfnia_probe()") 61 ADD_PROBE("is-qfnra", "true if the goal is in QF_NRA (quantifier-free nonlinear real arithmetic).", "mk_is_qfnra_probe()") 62 ADD_PROBE("is-nia", "true if the goal is in NIA (nonlinear integer arithmetic, formula may have quantifiers).", "mk_is_nia_probe()") 63 ADD_PROBE("is-nra", "true if the goal is in NRA (nonlinear real arithmetic, formula may have quantifiers).", "mk_is_nra_probe()") 64 ADD_PROBE("is-nira", "true if the goal is in NIRA (nonlinear integer and real arithmetic, formula may have quantifiers).", "mk_is_nira_probe()") 65 ADD_PROBE("is-lia", "true if the goal is in LIA (linear integer arithmetic, formula may have quantifiers).", "mk_is_lia_probe()") 66 ADD_PROBE("is-lra", "true if the goal is in LRA (linear real arithmetic, formula may have quantifiers).", "mk_is_lra_probe()") 67 ADD_PROBE("is-lira", "true if the goal is in LIRA (linear integer and real arithmetic, formula may have quantifiers).", "mk_is_lira_probe()") 68 ADD_PROBE("is-qfufnra", "true if the goal is QF_UFNRA (quantifier-free nonlinear real arithmetic with other theories).", "mk_is_qfufnra_probe()") 69 */ 70