diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-24 12:52:07 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-24 12:52:21 -0500 |
| commit | 30d21b25af6ee619e5f53d1ca8821b710fad4cb7 (patch) | |
| tree | 409009a6ab55986308cc73d030db53489beef26d /src/util/sort_inference.cpp | |
| parent | 3eaf02c01e74a2a43b2eff7638d6c16171a11a13 (diff) | |
Add options for symmetry breaking in uf+ss totality axiom approach, option for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine
Diffstat (limited to 'src/util/sort_inference.cpp')
| -rw-r--r-- | src/util/sort_inference.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index d44499fa8..13631e590 100644 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -191,7 +191,10 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){ int retType; if( n.getKind()==kind::EQUAL ){ //we only require that the left and right hand side must be equal - setEqual( child_types[0], child_types[1] ); + //setEqual( child_types[0], child_types[1] ); + int eqType = getIdForType( n[0].getType() ); + setEqual( child_types[0], eqType ); + setEqual( child_types[1], eqType ); retType = getIdForType( n.getType() ); }else if( n.getKind()==kind::APPLY_UF ){ Node op = n.getOperator(); |