1 /*++
2 Copyright (c) 2016 Microsoft Corporation
3
4 Module Name:
5
6 bv_bounds.h
7
8 Abstract:
9
10 A class used to determine bounds on bit-vector variables.
11 The satisfiability procedure is polynomial.
12
13
14 Author:
15
16 Mikolas Janota (MikolasJanota)
17
18 Revision History:
19 --*/
20 #pragma once
21 #include "ast/ast.h"
22 #include "ast/bv_decl_plugin.h"
23 #include "ast/rewriter/rewriter_types.h"
24
25 /* \brief A class to analyze constraints on bit vectors.
26
27 The objective is to identify inconsistencies in polynomial time.
28 All bounds/intervals are closed. Methods that add new constraints
29 return false if inconsistency has already been reached.
30 Typical usage is to call repeatedly add_constraint(e) and call is_sat() in the end.
31 */
32 class bv_bounds {
33 public:
34 typedef rational numeral;
35 typedef std::pair<numeral, numeral> interval;
36 typedef obj_map<app, numeral> bound_map;
bv_bounds(ast_manager & m)37 bv_bounds(ast_manager& m) : m_m(m), m_bv_util(m), m_okay(true) {};
38 ~bv_bounds();
39 public: // bounds addition methods
40 br_status rewrite(unsigned limit, func_decl * f, unsigned num, expr * const * args, expr_ref& result);
41
42 /** \brief Add a constraint to the system.
43
44 The added constraints are to be considered by is_sat.
45 Currently, only special types of inequalities are supported, e.g. v <= v+1.
46 Other constraints are ignored.
47 Returns false if the system became trivially unsatisfiable
48 **/
49 bool add_constraint(expr* e);
50
51 bool bound_up(app * v, const numeral& u); // v <= u
52 bool bound_lo(app * v, const numeral& l); // l <= v
53 inline bool add_neg_bound(app * v, const numeral& a, const numeral& b); // not (a<=v<=b)
54 bool add_bound_signed(app * v, const numeral& a, const numeral& b, bool negate);
55 bool add_bound_unsigned(app * v, const numeral& a, const numeral& b, bool negate);
56 public:
57 bool is_sat(); ///< Determine if the set of considered constraints is satisfiable.
58 bool is_okay();
singletons()59 const bound_map& singletons() { return m_singletons; }
bvu()60 bv_util& bvu() { return m_bv_util; }
61 void reset();
62 protected:
63 struct ninterval {
64 //ninterval(app * v, numeral lo, numeral hi, bool negated) : v(v), lo(lo), hi(hi), negated(negated) {}
65 app * v;
66 numeral lo, hi;
67 bool negated;
68 };
69 enum conv_res { CONVERTED, UNSAT, UNDEF };
70 conv_res convert(expr * e, vector<ninterval>& nis, bool negated);
71 conv_res record(app * v, numeral lo, numeral hi, bool negated, vector<ninterval>& nis);
72 conv_res convert_signed(app * v, const numeral& a, const numeral& b, bool negate, vector<ninterval>& nis);
73
74 typedef vector<interval> intervals;
75 typedef obj_map<app, intervals*> intervals_map;
76 ast_manager& m_m;
77 bound_map m_unsigned_lowers;
78 bound_map m_unsigned_uppers;
79 intervals_map m_negative_intervals;
80 bound_map m_singletons;
81 bv_util m_bv_util;
82 bool m_okay;
83 bool is_sat(app * v);
84 bool is_sat_core(app * v);
85 inline bool in_range(app *v, const numeral& l);
86 inline bool is_constant_add(unsigned bv_sz, expr * e, app*& v, numeral& val);
87 void record_singleton(app * v, numeral& singleton_value);
88 inline bool to_bound(const expr * e) const;
89 bool is_uleq(expr * e, expr * & v, numeral & c);
90 };
91
92
is_okay()93 inline bool bv_bounds::is_okay() { return m_okay; }
94
to_bound(const expr * e)95 inline bool bv_bounds::to_bound(const expr * e) const {
96 return is_app(e) && m_bv_util.is_bv(e)
97 && !m_bv_util.is_bv_add(e)
98 && !m_bv_util.is_numeral(e);
99 }
100
in_range(app * v,const bv_bounds::numeral & n)101 inline bool bv_bounds::in_range(app *v, const bv_bounds::numeral& n) {
102 const unsigned bv_sz = m_bv_util.get_bv_size(v);
103 const bv_bounds::numeral zero(0);
104 const bv_bounds::numeral mod(rational::power_of_two(bv_sz));
105 return (zero <= n) && (n < mod);
106 }
107
is_constant_add(unsigned bv_sz,expr * e,app * & v,numeral & val)108 inline bool bv_bounds::is_constant_add(unsigned bv_sz, expr * e, app*& v, numeral& val) {
109 SASSERT(e && !v);
110 SASSERT(m_bv_util.get_bv_size(e) == bv_sz);
111 expr *lhs(nullptr), *rhs(nullptr);
112 if (!m_bv_util.is_bv_add(e, lhs, rhs)) {
113 v = to_app(e);
114 val = rational(0);
115 return true;
116 }
117 if (to_bound(lhs) && m_bv_util.is_numeral(rhs, val, bv_sz)) {
118 v = to_app(lhs);
119 return true;
120 }
121 if (to_bound(rhs) && m_bv_util.is_numeral(lhs, val, bv_sz)) {
122 v = to_app(rhs);
123 return true;
124 }
125 return false;
126 }
127
128
129