From aed7130284c04f7ada79db1ed3d4a8ddb08d3543 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 4 Feb 2013 17:30:18 -0500 Subject: fixed files with DOS newlines; fixed contrib/ scripts to use git --- src/util/sort_inference.h | 152 +++++++++++++++++++++++----------------------- 1 file changed, 76 insertions(+), 76 deletions(-) mode change 100755 => 100644 src/util/sort_inference.h (limited to 'src/util/sort_inference.h') diff --git a/src/util/sort_inference.h b/src/util/sort_inference.h old mode 100755 new mode 100644 index 1378a266c..0b1f96f85 --- a/src/util/sort_inference.h +++ b/src/util/sort_inference.h @@ -1,76 +1,76 @@ -/********************* */ -/*! \file sort_inference.h - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Pre-process step for performing sort inference - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__SORT_INFERENCE_H -#define __CVC4__SORT_INFERENCE_H - -#include -#include -#include -#include -#include "expr/node.h" -#include "expr/type_node.h" - -namespace CVC4 { - -class SortInference{ -private: - //for debugging - //std::map< int, std::vector< Node > > d_type_eq_class; -private: - int sortCount; - std::map< int, int > d_type_union_find; - std::map< int, TypeNode > d_type_types; - std::map< TypeNode, int > d_id_for_types; - //for apply uf operators - std::map< Node, int > d_op_return_types; - std::map< Node, std::vector< int > > d_op_arg_types; - //for bound variables - std::map< Node, std::map< Node, int > > d_var_types; - //get representative - int getRepresentative( int t ); - void setEqual( int t1, int t2 ); - int getIdForType( TypeNode tn ); - void printSort( const char* c, int t ); - //process - int process( Node n, std::map< Node, Node >& var_bound ); -private: - //mapping from old symbols to new symbols - std::map< Node, Node > d_symbol_map; - //mapping from constants to new symbols - std::map< TypeNode, std::map< Node, Node > > d_const_map; - //number of subtypes generated - std::map< TypeNode, int > d_subtype_count; - //helper functions for simplify - TypeNode getOrCreateTypeForId( int t, TypeNode pref ); - TypeNode getTypeForId( int t ); - Node getNewSymbol( Node old, TypeNode tn ); - //simplify - Node simplify( Node n, std::map< Node, Node >& var_bound ); -public: - SortInference() : sortCount( 0 ){} - ~SortInference(){} - - void simplify( std::vector< Node >& assertions, bool doRewrite = false ); - int getSortId( Node n ); - int getSortId( Node f, Node v ); - //set that sk is the skolem variable of v for quantifier f - void setSkolemVar( Node f, Node v, Node sk ); -}; - -} - -#endif +/********************* */ +/*! \file sort_inference.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Pre-process step for performing sort inference + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__SORT_INFERENCE_H +#define __CVC4__SORT_INFERENCE_H + +#include +#include +#include +#include +#include "expr/node.h" +#include "expr/type_node.h" + +namespace CVC4 { + +class SortInference{ +private: + //for debugging + //std::map< int, std::vector< Node > > d_type_eq_class; +private: + int sortCount; + std::map< int, int > d_type_union_find; + std::map< int, TypeNode > d_type_types; + std::map< TypeNode, int > d_id_for_types; + //for apply uf operators + std::map< Node, int > d_op_return_types; + std::map< Node, std::vector< int > > d_op_arg_types; + //for bound variables + std::map< Node, std::map< Node, int > > d_var_types; + //get representative + int getRepresentative( int t ); + void setEqual( int t1, int t2 ); + int getIdForType( TypeNode tn ); + void printSort( const char* c, int t ); + //process + int process( Node n, std::map< Node, Node >& var_bound ); +private: + //mapping from old symbols to new symbols + std::map< Node, Node > d_symbol_map; + //mapping from constants to new symbols + std::map< TypeNode, std::map< Node, Node > > d_const_map; + //number of subtypes generated + std::map< TypeNode, int > d_subtype_count; + //helper functions for simplify + TypeNode getOrCreateTypeForId( int t, TypeNode pref ); + TypeNode getTypeForId( int t ); + Node getNewSymbol( Node old, TypeNode tn ); + //simplify + Node simplify( Node n, std::map< Node, Node >& var_bound ); +public: + SortInference() : sortCount( 0 ){} + ~SortInference(){} + + void simplify( std::vector< Node >& assertions, bool doRewrite = false ); + int getSortId( Node n ); + int getSortId( Node f, Node v ); + //set that sk is the skolem variable of v for quantifier f + void setSkolemVar( Node f, Node v, Node sk ); +}; + +} + +#endif -- cgit v1.2.3