diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-26 14:40:05 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-26 14:40:16 -0500 |
| commit | 0a6fa189e4e2dc2c47f4050df0aad4a6f3d39b4b (patch) | |
| tree | cdd99891d51b025e207e8b56c34bb13d77977a4a /src/theory/quantifiers/bounded_integers.h | |
| parent | 323c4ebc21ca9e85b76aadc2168a496404bf91fc (diff) | |
Add support for interval models in bounded integers MBQI (in progress).
Diffstat (limited to 'src/theory/quantifiers/bounded_integers.h')
| -rwxr-xr-x | src/theory/quantifiers/bounded_integers.h | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index f40e2180c..96d2a3d20 100755 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h @@ -45,8 +45,12 @@ private: std::map< Node, std::map< Node, Node > > d_range;
std::map< Node, std::map< Node, Node > > d_nground_range;
void hasFreeVar( Node f, Node n );
- void process( Node f, Node n, bool pol );
- void processLiteral( Node f, Node lit, bool pol );
+ void process( Node f, Node n, bool pol,
+ std::map< int, std::map< Node, Node > >& bound_lit_map,
+ std::map< int, std::map< Node, bool > >& bound_lit_pol_map );
+ void processLiteral( Node f, Node lit, bool pol,
+ std::map< int, std::map< Node, Node > >& bound_lit_map,
+ std::map< int, std::map< Node, bool > >& bound_lit_pol_map );
std::vector< Node > d_bound_quants;
private:
class RangeModel {
|