From 26b8cc7f672d580dfc7355dac1c4352a3c7c32e8 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 10 Sep 2015 10:12:36 +0200 Subject: Fix bug 670. Minor. --- src/theory/datatypes/datatypes_rewriter.h | 34 ++++++++++-- src/theory/datatypes/type_enumerator.cpp | 7 ++- src/theory/quantifiers/alpha_equivalence.cpp | 78 +++++++++++++-------------- src/theory/quantifiers/alpha_equivalence.h | 5 +- src/theory/quantifiers/options_handlers.h | 4 +- src/theory/quantifiers/quantifiers_rewriter.h | 1 - 6 files changed, 81 insertions(+), 48 deletions(-) diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 14d966458..4f5b93b39 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -385,7 +385,7 @@ public: tn.isTuple() || tn.isRecord(); } private: - static Node collectRef( Node n, std::vector< Node >& sk, std::map< Node, Node >& rf, std::vector< Node >& rf_pending ){ + static Node collectRef( Node n, std::vector< Node >& sk, std::map< Node, Node >& rf, std::vector< Node >& rf_pending, std::vector< Node >& terms ){ Assert( n.isConst() ); TypeNode tn = n.getType(); if( tn.isDatatype() ){ @@ -396,7 +396,7 @@ private: children.push_back( n.getOperator() ); bool childChanged = false; for( unsigned i=0; i().getIndex(); @@ -441,18 +444,43 @@ public: std::map< Node, Node > rf; std::vector< Node > sk; std::vector< Node > rf_pending; - Node s = collectRef( n, sk, rf, rf_pending ); + std::vector< Node > terms; + Node s = collectRef( n, sk, rf, rf_pending, terms ); if( !s.isNull() ){ Trace("dt-nconst") << "...symbolic normalized is : " << s << std::endl; for( std::map< Node, Node >::iterator it = rf.begin(); it != rf.end(); ++it ){ Trace("dt-nconst") << " " << it->first << " = " << it->second << std::endl; } + Trace("dt-nconst") << " " << terms.size() << " total subterms." << std::endl; + //now run bisimulations on all terms + return n; }else{ Trace("dt-nconst") << "...invalid." << std::endl; return Node::null(); } } + //normalize constant : apply to top-level codatatype constants + static Node normalizeConstant( Node n ){ + Assert( n.getType().isDatatype() ); + const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype(); + if( dt.isCodatatype() ){ + return normalizeMuConstant( n ); + }else{ + std::vector< Node > children; + bool childrenChanged = false; + for( unsigned i = 0; imkNode( n.getKind(), children ); + }else{ + return n; + } + } + } };/* class DatatypesRewriter */ }/* CVC4::theory::datatypes namespace */ diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index a4af183c5..0bcc0168e 100755 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -100,7 +100,12 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type << std::endl; Node ret; if( indexmkConst(UninterpretedConstant(d_type.toType(), d_size_limit)); + if( d_child_enum ){ + ret = NodeManager::currentNM()->mkConst(UninterpretedConstant(d_type.toType(), d_size_limit)); + }else{ + //no top-level variables + return Node::null(); + } }else{ Debug("dt-enum-debug") << "Look at constructor " << (index - d_has_debruijn) << std::endl; DatatypeConstructor ctor = d_datatype[index - d_has_debruijn]; diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index e4dcccdff..84bf2ec14 100755 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -29,54 +29,54 @@ struct sortTypeOrder { } }; -bool AlphaEquivalenceNode::registerNode( QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) { - if( tt.size()==arg_index.size()+1 ){ - Node t = tt.back(); - Node op = t.hasOperator() ? t.getOperator() : t; - arg_index.push_back( 0 ); - Trace("aeq-debug") << op << " "; - return d_children[op][t.getNumChildren()].registerNode( qe, q, tt, arg_index ); - }else if( tt.empty() ){ - //we are finished - Trace("aeq-debug") << std::endl; - if( d_quant.isNull() ){ - d_quant = q; - return true; +bool AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) { + while( !tt.empty() ){ + if( tt.size()==arg_index.size()+1 ){ + Node t = tt.back(); + Node op = t.hasOperator() ? t.getOperator() : t; + arg_index.push_back( 0 ); + Trace("aeq-debug") << op << " "; + aen = &(aen->d_children[op][t.getNumChildren()]); }else{ - //lemma ( q <=> d_quant ) - Trace("alpha-eq") << "Alpha equivalent : " << std::endl; - Trace("alpha-eq") << " " << q << std::endl; - Trace("alpha-eq") << " " << d_quant << std::endl; - qe->getOutputChannel().lemma( q.iffNode( d_quant ) ); - return false; + Node t = tt.back(); + int i = arg_index.back(); + if( i==(int)t.getNumChildren() ){ + tt.pop_back(); + arg_index.pop_back(); + }else{ + tt.push_back( t[i] ); + arg_index[arg_index.size()-1]++; + } } + } + Trace("aeq-debug") << std::endl; + if( aen->d_quant.isNull() ){ + aen->d_quant = q; + return true; }else{ - Node t = tt.back(); - int i = arg_index.back(); - if( i==(int)t.getNumChildren() ){ - tt.pop_back(); - arg_index.pop_back(); - }else{ - tt.push_back( t[i] ); - arg_index[arg_index.size()-1]++; - } - return registerNode( qe, q, tt, arg_index ); + //lemma ( q <=> d_quant ) + Trace("alpha-eq") << "Alpha equivalent : " << std::endl; + Trace("alpha-eq") << " " << q << std::endl; + Trace("alpha-eq") << " " << aen->d_quant << std::endl; + qe->getOutputChannel().lemma( q.iffNode( aen->d_quant ) ); + return false; } } -bool AlphaEquivalenceTypeNode::registerNode( QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index ){ - if( index==(int)typs.size() ){ - std::vector< Node > tt; - std::vector< int > arg_index; - tt.push_back( t ); - Trace("aeq-debug") << " : "; - return d_data.registerNode( qe, q, tt, arg_index ); - }else{ +bool AlphaEquivalenceTypeNode::registerNode( AlphaEquivalenceTypeNode* aetn, + QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index ){ + while( index<(int)typs.size() ){ TypeNode curr = typs[index]; Assert( typ_count.find( curr )!=typ_count.end() ); Trace("aeq-debug") << "[" << curr << " " << typ_count[curr] << "] "; - return d_children[curr][typ_count[curr]].registerNode( qe, q, t, typs, typ_count, index+1 ); + aetn = &(aetn->d_children[curr][typ_count[curr]]); + index = index + 1; } + std::vector< Node > tt; + std::vector< int > arg_index; + tt.push_back( t ); + Trace("aeq-debug") << " : "; + return AlphaEquivalenceNode::registerNode( &(aetn->d_data), qe, q, tt, arg_index ); } bool AlphaEquivalence::registerQuantifier( Node q ) { @@ -99,7 +99,7 @@ bool AlphaEquivalence::registerQuantifier( Node q ) { sto.d_tdb = d_qe->getTermDatabase(); std::sort( typs.begin(), typs.end(), sto ); Trace("aeq-debug") << " "; - bool ret = d_ae_typ_trie.registerNode( d_qe, q, t, typs, typ_count ); + bool ret = AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count ); Trace("aeq") << " ...result : " << ret << std::endl; return ret; } diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index fa2109ccc..99517fd2a 100755 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -28,14 +28,15 @@ class AlphaEquivalenceNode { public: std::map< Node, std::map< int, AlphaEquivalenceNode > > d_children; Node d_quant; - bool registerNode( QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ); + static bool registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ); }; class AlphaEquivalenceTypeNode { public: std::map< TypeNode, std::map< int, AlphaEquivalenceTypeNode > > d_children; AlphaEquivalenceNode d_data; - bool registerNode( QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index = 0 ); + static bool registerNode( AlphaEquivalenceTypeNode* aetn, + QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index = 0 ); }; class AlphaEquivalence { diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 791ad6e90..e5e484625 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -207,13 +207,13 @@ relevant \n\ static const std::string iteLiftQuantHelp = "\ Modes for term database, supported by --ite-lift-quant:\n\ \n\ -all \n\ +none \n\ + Do not lift if-then-else in quantified formulas.\n\ \n\ simple \n\ + Lift if-then-else in quantified formulas if results in smaller term size.\n\ \n\ -none \n\ +all \n\ + Lift if-then-else in quantified formulas. \n\ \n\ "; diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 0f477b828..828099984 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -62,7 +62,6 @@ private: COMPUTE_VAR_ELIMINATION, //COMPUTE_FLATTEN_ARGS_UF, //COMPUTE_CNF, - COMPUTE_SPLIT, COMPUTE_LAST }; static Node computeOperation( Node f, bool isNested, int computeOption ); -- cgit v1.2.3