diff options
author | ajreynol <reynolds@larapc05.epfl.ch> | 2014-06-17 15:25:58 +0200 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-06-19 18:24:39 -0400 |
commit | 0fe78eebc0c0f2d01c7aa64725bee08ba5aa2274 (patch) | |
tree | 475b094989b0828d7d82e41160a010a6134e8674 /src/util | |
parent | 35cdae503bd88633a52333bf06fbf80cd81926e2 (diff) |
For casc : print models of functions rewritten by sort inference.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/sort_inference.cpp | 2 | ||||
-rw-r--r-- | src/util/sort_inference.h | 6 |
2 files changed, 6 insertions, 2 deletions
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index b38ed7d63..90382c365 100644 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -580,6 +580,8 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ ss << "io_" << op; TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, retType ); d_symbol_map[op] = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during sort inference" ); + Trace("setp-model") << "Function " << op << " is replaced with " << d_symbol_map[op] << std::endl; + d_model_replace_f[op] = d_symbol_map[op]; }else{ d_symbol_map[op] = op; } diff --git a/src/util/sort_inference.h b/src/util/sort_inference.h index cd80f57d8..4cf2ab732 100644 --- a/src/util/sort_inference.h +++ b/src/util/sort_inference.h @@ -26,7 +26,7 @@ namespace CVC4 { -class SortInference{ +class SortInference { private: //all subsorts std::vector< int > d_sub_sorts; @@ -69,7 +69,6 @@ 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 ); @@ -107,6 +106,9 @@ public: bool isWellSorted( Node n ); //get constraints for being well-typed according to computed sub-types void getSortConstraints( Node n, SortInference::UnionFind& uf ); +public: + //list of all functions and the uninterpreted symbols they were replaced with + std::map< Node, Node > d_model_replace_f; }; } |