diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-10 10:12:36 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-10 10:12:36 +0200 |
commit | 26b8cc7f672d580dfc7355dac1c4352a3c7c32e8 (patch) | |
tree | bb10dfe7883e73345815bd47b5bb62214cb1035f /src/theory/quantifiers | |
parent | 68d3518e446b1e0f1ac16c2146c162580fa377f9 (diff) |
Fix bug 670. Minor.
Diffstat (limited to 'src/theory/quantifiers')
-rwxr-xr-x | src/theory/quantifiers/alpha_equivalence.cpp | 78 | ||||
-rwxr-xr-x | src/theory/quantifiers/alpha_equivalence.h | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/options_handlers.h | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 1 |
4 files changed, 44 insertions, 44 deletions
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 ); |