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 | |
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')
-rw-r--r-- | src/util/Makefile.am | 4 | ||||
-rwxr-xr-x | src/util/sort_inference.cpp | 393 | ||||
-rwxr-xr-x | src/util/sort_inference.h | 72 |
3 files changed, 468 insertions, 1 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 098024912..aa122905b 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -84,7 +84,9 @@ libutil_la_SOURCES = \ array_store_all.h \ array_store_all.cpp \ util_model.h \ - util_model.cpp + util_model.cpp \ + sort_inference.h \ + sort_inference.cpp libutil_la_LIBADD = \ @builddir@/libutilcudd.la diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp new file mode 100755 index 000000000..5dc60dbb0 --- /dev/null +++ b/src/util/sort_inference.cpp @@ -0,0 +1,393 @@ +/********************* */
+/*! \file sort_inference.cpp
+ ** \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 Sort inference module
+ **
+ ** This class implements sort inference, based on a simple algorithm:
+ ** First, we assume all functions and predicates have distinct uninterpreted types.
+ ** One pass is made through the input assertions, while a union-find data structure
+ ** maintains necessary information regarding constraints on these types.
+ **/
+
+#include <vector>
+
+#include "util/sort_inference.h"
+
+using namespace CVC4;
+using namespace std;
+
+namespace CVC4 {
+
+
+void SortInference::printSort( const char* c, int t ){
+ int rt = getRepresentative( t );
+ if( d_type_types.find( rt )!=d_type_types.end() ){
+ Trace(c) << d_type_types[rt];
+ }else{
+ Trace(c) << "s_" << rt;
+ }
+}
+
+void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){
+ //process all assertions
+ for( unsigned i=0; i<assertions.size(); i++ ){
+ Trace("sort-inference-debug") << "Process " << assertions[i] << std::endl;
+ std::map< Node, Node > var_bound;
+ process( assertions[i], var_bound );
+ }
+ //print debug
+ if( Trace.isOn("sort-inference") ){
+ for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){
+ Trace("sort-inference") << it->first << " : ";
+ if( !d_op_arg_types[ it->first ].empty() ){
+ Trace("sort-inference") << "( ";
+ for( size_t i=0; i<d_op_arg_types[ it->first ].size(); i++ ){
+ printSort( "sort-inference", d_op_arg_types[ it->first ][i] );
+ Trace("sort-inference") << " ";
+ }
+ Trace("sort-inference") << ") -> ";
+ }
+ printSort( "sort-inference", it->second );
+ Trace("sort-inference") << std::endl;
+ }
+ }
+ if( doRewrite ){
+ //simplify all assertions by introducing new symbols wherever necessary (NOTE: this is unsound for quantifiers)
+ for( unsigned i=0; i<assertions.size(); i++ ){
+ std::map< Node, Node > var_bound;
+ assertions[i] = simplify( assertions[i], var_bound );
+ Trace("sort-inference-rewrite") << " --> " << assertions[i] << std::endl;
+ }
+ //now, ensure constants are distinct
+ for( std::map< TypeNode, std::map< Node, Node > >::iterator it = d_const_map.begin(); it != d_const_map.end(); ++it ){
+ std::vector< Node > consts;
+ for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+ consts.push_back( it2->second );
+ }
+ //add lemma enforcing introduced constants to be distinct?
+ }
+ }
+}
+
+int SortInference::getRepresentative( int t ){
+ std::map< int, int >::iterator it = d_type_union_find.find( t );
+ if( it!=d_type_union_find.end() ){
+ if( it->second==t ){
+ return t;
+ }else{
+ int rt = getRepresentative( it->second );
+ d_type_union_find[t] = rt;
+ return rt;
+ }
+ }else{
+ return t;
+ }
+}
+
+void SortInference::setEqual( int t1, int t2 ){
+ if( t1!=t2 ){
+ int rt1 = getRepresentative( t1 );
+ int rt2 = getRepresentative( t2 );
+ if( rt1!=rt2 ){
+ Trace("sort-inference-debug") << "Set equal : ";
+ printSort( "sort-inference-debug", rt1 );
+ Trace("sort-inference-debug") << " ";
+ printSort( "sort-inference-debug", rt2 );
+ Trace("sort-inference-debug") << std::endl;
+ //check if they must be a type
+ std::map< int, TypeNode >::iterator it1 = d_type_types.find( rt1 );
+ std::map< int, TypeNode >::iterator it2 = d_type_types.find( rt2 );
+ if( it2!=d_type_types.end() ){
+ if( it1==d_type_types.end() ){
+ //swap sides
+ int swap = rt1;
+ rt1 = rt2;
+ rt2 = swap;
+ }else{
+ Assert( rt1==rt2 );
+ }
+ }
+ /*
+ d_type_eq_class[rt1].insert( d_type_eq_class[rt1].end(), d_type_eq_class[rt2].begin(), d_type_eq_class[rt2].end() );
+ d_type_eq_class[rt2].clear();
+ Trace("sort-inference-debug") << "EqClass : { ";
+ for( int i=0; i<(int)d_type_eq_class[rt1].size(); i++ ){
+ Trace("sort-inference-debug") << d_type_eq_class[rt1][i] << ", ";
+ }
+ Trace("sort-inference-debug") << "}" << std::endl;
+ */
+ d_type_union_find[rt2] = rt1;
+ }
+ }
+}
+
+int SortInference::getIdForType( TypeNode tn ){
+ //register the return type
+ std::map< TypeNode, int >::iterator it = d_id_for_types.find( tn );
+ if( it==d_id_for_types.end() ){
+ int sc = sortCount;
+ d_type_types[ sortCount ] = tn;
+ d_id_for_types[ tn ] = sortCount;
+ sortCount++;
+ return sc;
+ }else{
+ return it->second;
+ }
+}
+
+int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
+ Trace("sort-inference-debug") << "Process " << n << std::endl;
+ //add to variable bindings
+ if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
+ for( size_t i=0; i<n[0].getNumChildren(); i++ ){
+ //TODO: try applying sort inference to quantified variables
+ //d_var_types[n][ n[0][i] ] = sortCount;
+ //sortCount++;
+
+ //type of the quantified variable must be the same
+ d_var_types[n][ n[0][i] ] = getIdForType( n[0][i].getType() );
+ var_bound[ n[0][i] ] = n;
+ }
+ }
+
+ //process children
+ std::vector< Node > children;
+ std::vector< int > child_types;
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
+ bool processChild = true;
+ if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
+ processChild = i==1;
+ }
+ if( processChild ){
+ children.push_back( n[i] );
+ child_types.push_back( process( n[i], var_bound ) );
+ }
+ }
+
+ //remove from variable bindings
+ if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
+ //erase from variable bound
+ for( size_t i=0; i<n[0].getNumChildren(); i++ ){
+ var_bound.erase( n[0][i] );
+ }
+ }
+
+ 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] );
+ retType = getIdForType( n.getType() );
+ }else if( n.getKind()==kind::APPLY_UF ){
+ Node op = n.getOperator();
+ if( d_op_return_types.find( op )==d_op_return_types.end() ){
+ //assign arbitrary sort for return type
+ d_op_return_types[op] = sortCount;
+ sortCount++;
+ //d_type_eq_class[sortCount].push_back( op );
+ //assign arbitrary sort for argument types
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
+ d_op_arg_types[op].push_back( sortCount );
+ sortCount++;
+ }
+ }
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
+ //the argument of the operator must match the return type of the subterm
+ setEqual( child_types[i], d_op_arg_types[op][i] );
+ }
+ //return type is the return type
+ retType = d_op_return_types[op];
+ }else{
+ std::map< Node, Node >::iterator it = var_bound.find( n );
+ if( it!=var_bound.end() ){
+ Trace("sort-inference-debug") << n << " is a bound variable." << std::endl;
+ //the return type was specified while binding
+ retType = d_var_types[it->second][n];
+ }else if( n.getKind() == kind::VARIABLE ){
+ Trace("sort-inference-debug") << n << " is a variable." << std::endl;
+ if( d_op_return_types.find( n )==d_op_return_types.end() ){
+ //assign arbitrary sort
+ d_op_return_types[n] = sortCount;
+ sortCount++;
+ //d_type_eq_class[sortCount].push_back( n );
+ }
+ retType = d_op_return_types[n];
+ }else if( n.isConst() ){
+ Trace("sort-inference-debug") << n << " is a constant." << std::endl;
+ //can be any type we want
+ retType = sortCount;
+ sortCount++;
+ }else{
+ Trace("sort-inference-debug") << n << " is a interpreted symbol." << std::endl;
+ //it is an interpretted term
+ for( size_t i=0; i<children.size(); i++ ){
+ Trace("sort-inference-debug") << children[i] << " forced to have " << children[i].getType() << std::endl;
+ //must enforce the actual type of the operator on the children
+ int ct = getIdForType( children[i].getType() );
+ setEqual( child_types[i], ct );
+ }
+ //return type must be the actual return type
+ retType = getIdForType( n.getType() );
+ }
+ }
+ Trace("sort-inference-debug") << "Type( " << n << " ) = ";
+ printSort("sort-inference-debug", retType );
+ Trace("sort-inference-debug") << std::endl;
+ return retType;
+}
+
+
+TypeNode SortInference::getOrCreateTypeForId( int t, TypeNode pref ){
+ int rt = getRepresentative( t );
+ if( d_type_types.find( rt )!=d_type_types.end() ){
+ return d_type_types[rt];
+ }else{
+ TypeNode retType;
+ //see if we can assign pref
+ if( !pref.isNull() && d_id_for_types.find( pref )==d_id_for_types.end() ){
+ retType = pref;
+ }else{
+ if( d_subtype_count.find( pref )==d_subtype_count.end() ){
+ d_subtype_count[pref] = 0;
+ }
+ //must create new type
+ std::stringstream ss;
+ ss << "it_" << d_subtype_count[pref] << "_" << pref;
+ d_subtype_count[pref]++;
+ retType = NodeManager::currentNM()->mkSort( ss.str() );
+ }
+ d_id_for_types[ retType ] = rt;
+ d_type_types[ rt ] = retType;
+ return retType;
+ }
+}
+
+TypeNode SortInference::getTypeForId( int t ){
+ int rt = getRepresentative( t );
+ if( d_type_types.find( rt )!=d_type_types.end() ){
+ return d_type_types[rt];
+ }else{
+ return TypeNode::null();
+ }
+}
+
+Node SortInference::getNewSymbol( Node old, TypeNode tn ){
+ if( tn==old.getType() ){
+ return old;
+ }else{
+ std::stringstream ss;
+ ss << "i_$$_" << old;
+ return NodeManager::currentNM()->mkSkolem( ss.str(), tn, "created during sort inference" );
+ }
+}
+
+Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
+ std::vector< Node > children;
+ if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
+ //recreate based on types of variables
+ std::vector< Node > new_children;
+ for( size_t i=0; i<n[0].getNumChildren(); i++ ){
+ TypeNode tn = getOrCreateTypeForId( d_var_types[n][ n[0][i] ], n[0][i].getType() );
+ Node v = getNewSymbol( n[0][i], tn );
+ new_children.push_back( v );
+ var_bound[ n[0][i] ] = v;
+ }
+ children.push_back( NodeManager::currentNM()->mkNode( n[0].getKind(), new_children ) );
+ }
+
+ //process children
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.push_back( n.getOperator() );
+ }
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
+ bool processChild = true;
+ if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
+ processChild = i>=1;
+ }
+ if( processChild ){
+ children.push_back( simplify( n[i], var_bound ) );
+ }
+ }
+
+ //remove from variable bindings
+ if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
+ //erase from variable bound
+ for( size_t i=0; i<n[0].getNumChildren(); i++ ){
+ var_bound.erase( n[0][i] );
+ }
+ return NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }else if( n.getKind()==kind::APPLY_UF ){
+ Node op = n.getOperator();
+ if( d_symbol_map.find( op )==d_symbol_map.end() ){
+ //make the new operator if necessary
+ bool opChanged = false;
+ std::vector< TypeNode > argTypes;
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
+ TypeNode tn = getOrCreateTypeForId( d_op_arg_types[op][i], n[i].getType() );
+ argTypes.push_back( tn );
+ if( tn!=n[i].getType() ){
+ opChanged = true;
+ }
+ }
+ TypeNode retType = getOrCreateTypeForId( d_op_return_types[op], n.getType() );
+ if( retType!=n.getType() ){
+ opChanged = true;
+ }
+ if( opChanged ){
+ std::stringstream ss;
+ 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" );
+ }else{
+ d_symbol_map[op] = op;
+ }
+ }
+ children[0] = d_symbol_map[op];
+ //make sure all children have been taken care of
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
+ TypeNode tn = children[i+1].getType();
+ TypeNode tna = getTypeForId( d_op_arg_types[op][i] );
+ if( tn!=tna ){
+ if( n[i].isConst() ){
+ //must make constant of type tna
+ if( d_const_map[tna].find( n[i] )==d_const_map[tna].end() ){
+ std::stringstream ss;
+ ss << "ic_" << tna << "_" << n[i];
+ d_const_map[tna][ n[i] ] = NodeManager::currentNM()->mkSkolem( ss.str(), tna, "constant created during sort inference" ); //use mkConst???
+ }
+ children[i+1] = d_const_map[tna][ n[i] ];
+ }else{
+ Trace("sort-inference-warn") << "Sort inference created bad child: " << n[i] << " " << tn << " " << tna << std::endl;
+ Assert( false );
+ }
+ }
+ }
+ return NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );
+ }else{
+ std::map< Node, Node >::iterator it = var_bound.find( n );
+ if( it!=var_bound.end() ){
+ return it->second;
+ }else if( n.getKind() == kind::VARIABLE ){
+ if( d_symbol_map.find( n )==d_symbol_map.end() ){
+ TypeNode tn = getOrCreateTypeForId( d_op_return_types[n], n.getType() );
+ d_symbol_map[n] = getNewSymbol( n, tn );
+ }
+ return d_symbol_map[n];
+ }else if( n.isConst() ){
+ //just return n, we will fix at higher scope
+ return n;
+ }else{
+ return NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }
+ }
+
+}
+
+}
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
|