diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-09-30 10:14:32 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-09-30 10:14:42 -0500 |
commit | 0c2eafec69b694a507ac914bf285fe0574be085f (patch) | |
tree | 0f3601964ee8f883c93d506f1f0476e5888936ae /src/util/sort_inference.h | |
parent | 546e6aca016ea1f9b7da0bcfda5bed833a7a13ec (diff) |
Bug fixes and improvements for symmetry breaking, it now supports multiple sorts. Working on monotonicity inference.
Diffstat (limited to 'src/util/sort_inference.h')
-rw-r--r-- | src/util/sort_inference.h | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/src/util/sort_inference.h b/src/util/sort_inference.h index 53dff823f..8f0fc5e9f 100644 --- a/src/util/sort_inference.h +++ b/src/util/sort_inference.h @@ -28,8 +28,10 @@ namespace CVC4 { class SortInference{ private: - //for debugging - //std::map< int, std::vector< Node > > d_type_eq_class; + //all subsorts + std::vector< int > d_sub_sorts; + std::map< int, bool > d_non_monotonic_sorts; + void recordSubsort( int s ); public: class UnionFind { public: @@ -66,6 +68,12 @@ private: void printSort( const char* c, int t ); //process int process( Node n, std::map< Node, Node >& var_bound ); + +//for monotonicity inference +private: + void processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound ); + +//for rewriting private: //mapping from old symbols to new symbols std::map< Node, Node > d_symbol_map; @@ -79,6 +87,7 @@ private: Node getNewSymbol( Node old, TypeNode tn ); //simplify Node simplify( Node n, std::map< Node, Node >& var_bound ); + public: SortInference() : sortCount( 1 ){} ~SortInference(){} |