diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-12 16:46:51 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-12 16:46:51 +0000 |
| commit | 0ba075e240b2083163ab35a3580547cae6927b6c (patch) | |
| tree | 47be765d608aff213ee58749adab458f315fcf89 /src/util/sort_inference.h | |
| parent | 341794b1cbd5693010c78b9f5bfe232ee90404b0 (diff) | |
minor bug fixes for quantifiers, added sort inference module (not ready to be used yet), added new totality lemma option for uf strong solver
Diffstat (limited to 'src/util/sort_inference.h')
| -rwxr-xr-x | src/util/sort_inference.h | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/src/util/sort_inference.h b/src/util/sort_inference.h new file mode 100755 index 000000000..363dbd84d --- /dev/null +++ b/src/util/sort_inference.h @@ -0,0 +1,72 @@ +/********************* */
+/*! \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 <iostream>
+#include <string>
+#include <vector>
+#include <map>
+#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 );
+};
+
+}
+
+#endif
|