diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-02-07 13:26:57 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-02-07 13:26:57 -0600 |
| commit | 3837f84ab251d1563726f3d13b95f541eaa331a4 (patch) | |
| tree | 7afb6eb470b837b7e7600437356a8080fc329eb5 /src/theory/quantifiers/bounded_integers.h | |
| parent | 0dd2aa21f35b221ea96d277e9ea7cbc816ffe83c (diff) | |
Generalize finite bound inference to unifiable variables in set membership literals.
Diffstat (limited to 'src/theory/quantifiers/bounded_integers.h')
| -rw-r--r-- | src/theory/quantifiers/bounded_integers.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index 5c5a52855..f367b328c 100644 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h @@ -74,6 +74,7 @@ private: std::map< int, std::map< Node, Node > >& bound_int_range_term, std::map< Node, std::vector< Node > >& bound_fixed_set ); bool processEqDisjunct( Node q, Node n, Node& v, std::vector< Node >& v_cases ); + void processMatchBoundVars( Node q, Node n, std::vector< Node >& bvs, std::map< Node, bool >& visited ); std::vector< Node > d_bound_quants; private: class RangeModel { @@ -164,6 +165,7 @@ private: //for set range Node getSetRange( Node q, Node v, RepSetIterator * rsi ); Node getSetRangeValue( Node q, Node v, RepSetIterator * rsi ); + Node matchBoundVar( Node v, Node t, Node e ); bool getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi ); public: |