diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/equality_infer.cpp | 49 | ||||
-rw-r--r-- | src/theory/quantifiers/equality_infer.h | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match_generator.cpp | 35 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match_generator.h | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 480 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/symmetry_breaking.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 44 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 2 |
9 files changed, 220 insertions, 419 deletions
diff --git a/src/theory/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp index c3064116f..5190025ee 100644 --- a/src/theory/quantifiers/equality_infer.cpp +++ b/src/theory/quantifiers/equality_infer.cpp @@ -53,10 +53,10 @@ void EqualityInference::addToExplanation( std::vector< Node >& exp, Node e ) { } void EqualityInference::addToExplanationEqc( std::vector< Node >& exp, Node eqc ) { - NodeListMap::iterator re_i = d_rep_exp.find( eqc ); + NodeIntMap::iterator re_i = d_rep_exp.find( eqc ); if( re_i!=d_rep_exp.end() ){ - for( unsigned i=0; i<(*re_i).second->size(); i++ ){ - addToExplanation( exp, (*(*re_i).second)[i] ); + for( int i=0; i<(*re_i).second; i++ ){ + addToExplanation( exp, d_rep_exp_data[eqc][i] ); } } //for( unsigned i=0; i<d_eqci[n]->d_rep_exp.size(); i++ ){ @@ -65,16 +65,19 @@ void EqualityInference::addToExplanationEqc( std::vector< Node >& exp, Node eqc } void EqualityInference::addToExplanationEqc( Node eqc, std::vector< Node >& exp_to_add ) { - NodeListMap::iterator re_i = d_rep_exp.find( eqc ); - NodeList* re; + NodeIntMap::iterator re_i = d_rep_exp.find( eqc ); + int n_re = 0; if( re_i != d_rep_exp.end() ){ - re = (*re_i).second; - }else{ - re = new(d_c->getCMM()) NodeList( true, d_c, false, context::ContextMemoryAllocator<TNode>(d_c->getCMM()) ); - d_rep_exp.insertDataFromContextMemory( eqc, re ); + n_re = (*re_i).second; } + d_rep_exp[eqc] = n_re + exp_to_add.size(); for( unsigned i=0; i<exp_to_add.size(); i++ ){ - re->push_back( exp_to_add[i] ); + if( n_re<(int)d_rep_exp_data[eqc].size() ){ + d_rep_exp_data[eqc][n_re] = exp_to_add[i]; + }else{ + d_rep_exp_data[eqc].push_back( exp_to_add[i] ); + } + n_re++; } //for( unsigned i=0; i<exp_to_add.size(); i++ ){ // eqci->d_rep_exp.push_back( exp_to_add[i] ); @@ -204,16 +207,18 @@ void EqualityInference::eqNotifyNewClass(TNode t) { void EqualityInference::addToUseList( Node used, Node eqc ) { #if 1 - NodeListMap::iterator ul_i = d_uselist.find( used ); - NodeList* ul; + NodeIntMap::iterator ul_i = d_uselist.find( used ); + int n_ul = 0; if( ul_i != d_uselist.end() ){ - ul = (*ul_i).second; - }else{ - ul = new(d_c->getCMM()) NodeList( true, d_c, false, context::ContextMemoryAllocator<TNode>(d_c->getCMM()) ); - d_uselist.insertDataFromContextMemory( used, ul ); + n_ul = (*ul_i).second; } + d_uselist[ used ] = n_ul + 1; Trace("eq-infer-debug") << " add to use list : " << used << " -> " << eqc << std::endl; - (*ul).push_back( eqc ); + if( n_ul<(int)d_uselist_data[used].size() ){ + d_uselist_data[used][n_ul] = eqc; + }else{ + d_uselist_data[used].push_back( eqc ); + } #else std::map< Node, EqcInfo * >::iterator itu = d_eqci.find( used ); EqcInfo * eqci_used; @@ -356,12 +361,12 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) { //go through all equivalence classes that may refer to v_solve std::map< Node, bool > processed; processed[v_solve] = true; - NodeListMap::iterator ul_i = d_uselist.find( v_solve ); + NodeIntMap::iterator ul_i = d_uselist.find( v_solve ); if( ul_i != d_uselist.end() ){ - NodeList* ul = (*ul_i).second; - Trace("eq-infer-debug") << " use list size = " << ul->size() << std::endl; - for( unsigned j=0; j<ul->size(); j++ ){ - Node r = (*ul)[j]; + int n_ul = (*ul_i).second; + Trace("eq-infer-debug") << " use list size = " << n_ul << std::endl; + for( int j=0; j<n_ul; j++ ){ + Node r = d_uselist_data[v_solve][j]; //Trace("eq-infer-debug") << " use list size = " << eqci_solved->d_uselist.size() << std::endl; //for( unsigned j=0; j<eqci_solved->d_uselist.size(); j++ ){ // Node r = eqci_solved->d_uselist[j]; diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h index 93c7bd080..80d6ef98b 100644 --- a/src/theory/quantifiers/equality_infer.h +++ b/src/theory/quantifiers/equality_infer.h @@ -39,7 +39,7 @@ class EqualityInference typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; typedef context::CDChunkList<Node> NodeList; - typedef context::CDHashMap< Node, NodeList *, NodeHashFunction > NodeListMap; + typedef context::CDHashMap< Node, int, NodeHashFunction > NodeIntMap; private: context::Context * d_c; Node d_one; @@ -67,11 +67,13 @@ private: BoolMap d_elim_vars; std::map< Node, EqcInfo * > d_eqci; NodeMap d_rep_to_eqc; - NodeListMap d_rep_exp; + NodeIntMap d_rep_exp; + std::map< Node, std::vector< Node > > d_rep_exp_data; /** set eqc rep */ void setEqcRep( Node t, Node r, std::vector< Node >& exp_to_add, EqcInfo * eqci ); /** use list */ - NodeListMap d_uselist; + NodeIntMap d_uselist; + std::map< Node, std::vector< Node > > d_uselist_data; void addToUseList( Node used, Node eqc ); /** pending merges */ NodeList d_pending_merges; diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index bd5100a2e..2d3bf76f6 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -32,6 +32,7 @@ namespace theory { namespace inst { InstMatchGenerator::InstMatchGenerator( Node pat ){ + d_cg = NULL; d_needsReset = true; d_active_add = false; Assert( quantifiers::TermDb::hasInstConstAttr(pat) ); @@ -43,12 +44,20 @@ InstMatchGenerator::InstMatchGenerator( Node pat ){ } InstMatchGenerator::InstMatchGenerator() { + d_cg = NULL; d_needsReset = true; d_active_add = false; d_next = NULL; d_matchPolicy = MATCH_GEN_DEFAULT; } +InstMatchGenerator::~InstMatchGenerator() throw() { + for( unsigned i=0; i<d_children.size(); i++ ){ + delete d_children[i]; + } + delete d_cg; +} + void InstMatchGenerator::setActiveAdd(bool val){ d_active_add = val; if( d_next!=NULL ){ @@ -249,7 +258,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi Trace("matching-debug2") << "Reset children..." << std::endl; //now, fit children into match //we will be requesting candidates for matching terms for each child - for( int i=0; i<(int)d_children.size(); i++ ){ + for( unsigned i=0; i<d_children.size(); i++ ){ d_children[i]->reset( t[ d_children_index[i] ], qe ); } Trace("matching-debug2") << "Continue next " << d_next << std::endl; @@ -484,7 +493,7 @@ d_f( q ){ } Debug("smart-multi-trigger") << std::endl; } - for( int i=0; i<(int)pats.size(); i++ ){ + for( unsigned i=0; i<pats.size(); i++ ){ Node n = pats[i]; //make the match generator d_children.push_back( InstMatchGenerator::mkInstMatchGenerator(q, n, qe ) ); @@ -492,7 +501,7 @@ d_f( q ){ std::vector< int > unique_vars; std::map< int, bool > shared_vars; int numSharedVars = 0; - for( int j=0; j<(int)d_var_contains[n].size(); j++ ){ + for( unsigned j=0; j<d_var_contains[n].size(); j++ ){ if( d_var_to_node[ d_var_contains[n][j] ].size()==1 ){ Debug("smart-multi-trigger") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl; unique_vars.push_back( d_var_contains[n][j] ); @@ -503,7 +512,7 @@ d_f( q ){ } //we use the latest shared variables, then unique variables std::vector< int > vars; - int index = i==0 ? (int)(pats.size()-1) : (i-1); + unsigned index = i==0 ? pats.size()-1 : (i-1); while( numSharedVars>0 && index!=i ){ for( std::map< int, bool >::iterator it = shared_vars.begin(); it != shared_vars.end(); ++it ){ if( it->second ){ @@ -519,16 +528,24 @@ d_f( q ){ } vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() ); Debug("smart-multi-trigger") << " Index[" << i << "]: "; - for( int i=0; i<(int)vars.size(); i++ ){ - Debug("smart-multi-trigger") << vars[i] << " "; + for( unsigned j=0; j<vars.size(); j++ ){ + Debug("smart-multi-trigger") << vars[j] << " "; } Debug("smart-multi-trigger") << std::endl; //make ordered inst match trie - InstMatchTrie::ImtIndexOrder* imtio = new InstMatchTrie::ImtIndexOrder; - imtio->d_order.insert( imtio->d_order.begin(), vars.begin(), vars.end() ); - d_children_trie.push_back( InstMatchTrieOrdered( imtio ) ); + d_imtio[i] = new InstMatchTrie::ImtIndexOrder; + d_imtio[i]->d_order.insert( d_imtio[i]->d_order.begin(), vars.begin(), vars.end() ); + d_children_trie.push_back( InstMatchTrieOrdered( d_imtio[i] ) ); } +} +InstMatchGeneratorMulti::~InstMatchGeneratorMulti() throw() { + for( unsigned i=0; i<d_children.size(); i++ ){ + delete d_children[i]; + } + for( std::map< unsigned, InstMatchTrie::ImtIndexOrder* >::iterator it = d_imtio.begin(); it != d_imtio.end(); ++it ){ + delete it->second; + } } /** reset instantiation round (call this whenever equivalence classes have changed) */ diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index 49e3c1ec5..096774c51 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -91,7 +91,7 @@ public: InstMatchGenerator( Node pat ); InstMatchGenerator(); /** destructor */ - ~InstMatchGenerator() throw() {} + virtual ~InstMatchGenerator() throw(); /** The pattern we are producing matches for. If null, this is a multi trigger that is merging matches from d_children. */ @@ -125,7 +125,7 @@ public: class VarMatchGeneratorBooleanTerm : public InstMatchGenerator { public: VarMatchGeneratorBooleanTerm( Node var, Node comp ); - ~VarMatchGeneratorBooleanTerm() throw() {} + virtual ~VarMatchGeneratorBooleanTerm() throw() {} Node d_comp; bool d_rm_prev; /** reset instantiation round (call this at beginning of instantiation round) */ @@ -142,7 +142,7 @@ public: class VarMatchGeneratorTermSubs : public InstMatchGenerator { public: VarMatchGeneratorTermSubs( Node var, Node subs ); - ~VarMatchGeneratorTermSubs() throw() {} + virtual ~VarMatchGeneratorTermSubs() throw() {} TNode d_var; TypeNode d_var_type; Node d_subs; @@ -183,6 +183,8 @@ private: int d_matchPolicy; /** children generators */ std::vector< InstMatchGenerator* > d_children; + /** order */ + std::map< unsigned, InstMatchTrie::ImtIndexOrder* > d_imtio; /** inst match tries for each child */ std::vector< InstMatchTrieOrdered > d_children_trie; /** calculate matches */ @@ -191,7 +193,7 @@ public: /** constructors */ InstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ); /** destructor */ - ~InstMatchGeneratorMulti() throw() {} + virtual ~InstMatchGeneratorMulti() throw(); /** reset instantiation round (call this whenever equivalence classes have changed) */ void resetInstantiationRound( QuantifiersEngine* qe ); /** reset, eqc is the equivalence class to search in (any if eqc=null) */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 511337b40..68f824c57 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -48,7 +48,7 @@ bool QuantifiersRewriter::isClause( Node n ){ bool QuantifiersRewriter::isLiteral( Node n ){ switch( n.getKind() ){ case NOT: - return isLiteral( n[0] ); + return n[0].getKind()!=NOT && isLiteral( n[0] ); break; case OR: case AND: @@ -59,7 +59,8 @@ bool QuantifiersRewriter::isLiteral( Node n ){ return false; break; case EQUAL: - return n[0].getType()!=NodeManager::currentNM()->booleanType(); + //for boolean terms + return !n[0].getType().isBoolean(); break; default: break; @@ -259,121 +260,98 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { return RewriteResponse( status, ret ); } -Node QuantifiersRewriter::computeElimSymbols( Node body ) { - if( isLiteral( body ) ){ - return body; - }else{ - bool childrenChanged = false; - Kind k = body.getKind(); - if( body.getKind()==IMPLIES ){ - k = OR; - childrenChanged = true; - }else if( body.getKind()==XOR ){ - k = IFF; +bool QuantifiersRewriter::addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged ){ + if( ( k==OR || k==AND ) && options::elimTautQuant() ){ + Node lit = c.getKind()==NOT ? c[0] : c; + bool pol = c.getKind()!=NOT; + std::map< Node, bool >::iterator it = lit_pol.find( lit ); + if( it==lit_pol.end() ){ + lit_pol[lit] = pol; + children.push_back( c ); + }else{ childrenChanged = true; - } - std::vector< Node > children; - std::map< Node, bool > lit_pol; - for( unsigned i=0; i<body.getNumChildren(); i++ ){ - Node c = computeElimSymbols( body[i] ); - if( i==0 && ( body.getKind()==IMPLIES || body.getKind()==XOR ) ){ - c = c.negate(); - } - if( ( k==OR || k==AND ) && options::elimTautQuant() ){ - Node lit = c.getKind()==NOT ? c[0] : c; - bool pol = c.getKind()!=NOT; - std::map< Node, bool >::iterator it = lit_pol.find( lit ); - if( it==lit_pol.end() ){ - lit_pol[lit] = pol; - children.push_back( c ); - }else{ - childrenChanged = true; - if( it->second!=pol ){ - return NodeManager::currentNM()->mkConst( k==OR ); - } - } - }else{ - children.push_back( c ); + if( it->second!=pol ){ + return false; } - childrenChanged = childrenChanged || c!=body[i]; - } - //if( body.getKind()==ITE && isLiteral( body[0] ) ){ - // ret = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] ), - // NodeManager::currentNM()->mkNode( OR, body[0], body[2] ) ); - //} - if( childrenChanged ){ - return ( children.size()==1 && k!=NOT ) ? children[0] : NodeManager::currentNM()->mkNode( k, children ); - }else{ - return body; } + }else{ + children.push_back( c ); } + return true; } -Node QuantifiersRewriter::computeNNF( Node body ){ - if( body.getKind()==NOT ){ +// eliminates IMPLIES/XOR, removes duplicates/infers tautologies of AND/OR, and computes NNF +Node QuantifiersRewriter::computeElimSymbols( Node body ) { + Kind ok = body.getKind(); + Kind k = ok; + bool negAllCh = false; + bool negCh1 = false; + if( ok==IMPLIES ){ + k = OR; + negCh1 = true; + }else if( ok==XOR ){ + k = IFF; + negCh1 = true; + }else if( ok==NOT ){ if( body[0].getKind()==NOT ){ - return computeNNF( body[0][0] ); - }else if( isLiteral( body[0] ) ){ - return body; + return computeElimSymbols( body[0][0] ); + }else if( body[0].getKind()==OR || body[0].getKind()==IMPLIES ){ + k = AND; + negAllCh = true; + negCh1 = body[0].getKind()==IMPLIES; + body = body[0]; + }else if( body[0].getKind()==AND ){ + k = OR; + negAllCh = true; + body = body[0]; + }else if( body[0].getKind()==XOR || body[0].getKind()==IFF ){ + k = IFF; + negCh1 = ( body[0].getKind()==IFF ); + body = body[0]; + }else if( body[0].getKind()==ITE ){ + k = body[0].getKind(); + negAllCh = true; + negCh1 = true; + body = body[0]; }else{ - std::vector< Node > children; - Kind k = body[0].getKind(); - - if( body[0].getKind()==OR || body[0].getKind()==AND ){ - k = body[0].getKind()==AND ? OR : AND; - for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ - Node nc = computeNNF( body[0][i].notNode() ); - if( nc.getKind()==k ){ - for( unsigned j=0; j<nc.getNumChildren(); j++ ){ - children.push_back( nc[j] ); - } - }else{ - children.push_back( nc ); - } - } - }else if( body[0].getKind()==IFF ){ - for( int i=0; i<2; i++ ){ - Node nn = i==0 ? body[0][i] : body[0][i].notNode(); - children.push_back( computeNNF( nn ) ); - } - }else if( body[0].getKind()==ITE ){ - for( int i=0; i<3; i++ ){ - Node nn = i==0 ? body[0][i] : body[0][i].notNode(); - children.push_back( computeNNF( nn ) ); - } - }else{ - Notice() << "Unhandled Quantifiers NNF: " << body << std::endl; - return body; - } - return NodeManager::currentNM()->mkNode( k, children ); + return body; } - }else if( isLiteral( body ) ){ + }else if( ok!=IFF && ok!=ITE && ok!=AND && ok!=OR ){ + //a literal return body; - }else{ - std::vector< Node > children; - bool childrenChanged = false; - bool isAssoc = body.getKind()==AND || body.getKind()==OR; - for( int i=0; i<(int)body.getNumChildren(); i++ ){ - Node nc = computeNNF( body[i] ); - if( isAssoc && nc.getKind()==body.getKind() ){ - for( unsigned j=0; j<nc.getNumChildren(); j++ ){ - children.push_back( nc[j] ); + } + bool childrenChanged = false; + std::vector< Node > children; + std::map< Node, bool > lit_pol; + for( unsigned i=0; i<body.getNumChildren(); i++ ){ + Node c = computeElimSymbols( ( i==0 && negCh1 )!=negAllCh ? body[i].negate() : body[i] ); + bool success = true; + if( c.getKind()==k && ( k==OR || k==AND ) ){ + //flatten + childrenChanged = true; + for( unsigned j=0; j<c.getNumChildren(); j++ ){ + if( !addCheckElimChild( children, c[j], k, lit_pol, childrenChanged ) ){ + success = false; + break; } - childrenChanged = true; - }else{ - children.push_back( nc ); - childrenChanged = childrenChanged || nc!=body[i]; } - } - if( childrenChanged ){ - return NodeManager::currentNM()->mkNode( body.getKind(), children ); }else{ - return body; + success = addCheckElimChild( children, c, k, lit_pol, childrenChanged ); + } + if( !success ){ + // tautology + Assert( k==OR || k==AND ); + return NodeManager::currentNM()->mkConst( k==OR ); } + childrenChanged = childrenChanged || c!=body[i]; + } + if( childrenChanged || k!=ok ){ + return ( children.size()==1 && k!=NOT ) ? children[0] : NodeManager::currentNM()->mkNode( k, children ); + }else{ + return body; } } - void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj ){ if( n.getKind()==ITE && n[0].getKind()==APPLY_TESTER && n[1].getType().isBoolean() ){ @@ -1036,144 +1014,6 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& return body; } -Node QuantifiersRewriter::computeClause( Node n ){ - Assert( isClause( n ) ); - if( isLiteral( n ) ){ - return n; - }else{ - NodeBuilder<> t(OR); - if( n.getKind()==NOT ){ - if( n[0].getKind()==NOT ){ - return computeClause( n[0][0] ); - }else{ - //De-Morgan's law - Assert( n[0].getKind()==AND ); - for( int i=0; i<(int)n[0].getNumChildren(); i++ ){ - Node nn = computeClause( n[0][i].notNode() ); - addNodeToOrBuilder( nn, t ); - } - } - }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - Node nn = computeClause( n[i] ); - addNodeToOrBuilder( nn, t ); - } - } - return t.constructNode(); - } -} - -Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ){ - if( isLiteral( n ) ){ - return n; - }else if( !forcePred && isClause( n ) ){ - return computeClause( n ); - }else{ - Kind k = n.getKind(); - NodeBuilder<> t(k); - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - Node nc = n[i]; - Node ncnf = computeCNF( nc, args, defs, k!=OR ); - if( k==OR ){ - addNodeToOrBuilder( ncnf, t ); - }else{ - t << ncnf; - } - } - if( !forcePred && k==OR ){ - return t.constructNode(); - }else{ - //compute the free variables - Node nt = t; - std::vector< Node > activeArgs; - computeArgVec( args, activeArgs, nt ); - std::vector< TypeNode > argTypes; - for( int i=0; i<(int)activeArgs.size(); i++ ){ - argTypes.push_back( activeArgs[i].getType() ); - } - //create the predicate - Assert( argTypes.size()>0 ); - TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, NodeManager::currentNM()->booleanType() ); - std::stringstream ss; - ss << "cnf_" << n.getKind() << "_" << n.getId(); - Node op = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "was created by the quantifiers rewriter" ); - std::vector< Node > predArgs; - predArgs.push_back( op ); - predArgs.insert( predArgs.end(), activeArgs.begin(), activeArgs.end() ); - Node pred = NodeManager::currentNM()->mkNode( APPLY_UF, predArgs ); - Trace("quantifiers-rewrite-cnf-debug") << "Made predicate " << pred << " for " << nt << std::endl; - //create the bound var list - Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, activeArgs ); - //now, look at the structure of nt - if( nt.getKind()==NOT ){ - //case for NOT - for( int i=0; i<2; i++ ){ - NodeBuilder<> tt(OR); - tt << ( i==0 ? nt[0].notNode() : nt[0] ); - tt << ( i==0 ? pred.notNode() : pred ); - defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() ); - } - }else if( nt.getKind()==OR ){ - //case for OR - for( int i=0; i<(int)nt.getNumChildren(); i++ ){ - NodeBuilder<> tt(OR); - tt << nt[i].notNode() << pred; - defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() ); - } - NodeBuilder<> tt(OR); - for( int i=0; i<(int)nt.getNumChildren(); i++ ){ - tt << nt[i]; - } - tt << pred.notNode(); - defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() ); - }else if( nt.getKind()==AND ){ - //case for AND - for( int i=0; i<(int)nt.getNumChildren(); i++ ){ - NodeBuilder<> tt(OR); - tt << nt[i] << pred.notNode(); - defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() ); - } - NodeBuilder<> tt(OR); - for( int i=0; i<(int)nt.getNumChildren(); i++ ){ - tt << nt[i].notNode(); - } - tt << pred; - defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() ); - }else if( nt.getKind()==IFF ){ - //case for IFF - for( int i=0; i<4; i++ ){ - NodeBuilder<> tt(OR); - tt << ( ( i==0 || i==3 ) ? nt[0].notNode() : nt[0] ); - tt << ( ( i==1 || i==3 ) ? nt[1].notNode() : nt[1] ); - tt << ( ( i==0 || i==1 ) ? pred.notNode() : pred ); - defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() ); - } - }else if( nt.getKind()==ITE ){ - //case for ITE - for( int j=1; j<=2; j++ ){ - for( int i=0; i<2; i++ ){ - NodeBuilder<> tt(OR); - tt << ( ( j==1 ) ? nt[0].notNode() : nt[0] ); - tt << ( ( i==1 ) ? nt[j].notNode() : nt[j] ); - tt << ( ( i==0 ) ? pred.notNode() : pred ); - defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() ); - } - } - for( int i=0; i<2; i++ ){ - NodeBuilder<> tt(OR); - tt << ( i==0 ? nt[1].notNode() : nt[1] ); - tt << ( i==0 ? nt[2].notNode() : nt[2] ); - tt << ( i==1 ? pred.notNode() : pred ); - defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() ); - } - }else{ - Notice() << "Unhandled Quantifiers CNF: " << nt << std::endl; - } - return pred; - } - } -} - Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, bool pol ){ if( body.getKind()==FORALL ){ if( pol && ( options::prenexQuant()==PRENEX_ALL || body.getNumChildren()==2 ) ){ @@ -1181,15 +1021,13 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b std::vector< Node > subs; //for doing prenexing of same-signed quantifiers //must rename each variable that already exists - for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ - //if( std::find( args.begin(), args.end(), body[0][i] )!=args.end() ){ + for( unsigned i=0; i<body[0].getNumChildren(); i++ ){ terms.push_back( body[0][i] ); subs.push_back( NodeManager::currentNM()->mkBoundVar( body[0][i].getType() ) ); } args.insert( args.end(), subs.begin(), subs.end() ); Node newBody = body[1]; newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); - Debug("quantifiers-substitute-debug") << "Did substitute have an effect" << (body[1] != newBody) << body[1] << " became " << newBody << endl; return newBody; }else{ return body; @@ -1198,7 +1036,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b Assert( body.getKind()!=EXISTS ); bool childrenChanged = false; std::vector< Node > newChildren; - for( int i=0; i<(int)body.getNumChildren(); i++ ){ + for( unsigned i=0; i<body.getNumChildren(); i++ ){ bool newHasPol; bool newPol; QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol ); @@ -1224,7 +1062,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b } } -Node QuantifiersRewriter::computeSplit( Node f, std::vector< Node >& args, Node body ) { +Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ) { Assert( body.getKind()==OR ); size_t var_found_count = 0; size_t eqc_count = 0; @@ -1240,8 +1078,8 @@ Node QuantifiersRewriter::computeSplit( Node f, std::vector< Node >& args, Node Node n = body[i]; std::vector< Node > lit_args; computeArgVec( args, lit_args, n ); - if (lit_args.empty()) { - lits.push_back(n); + if( lit_args.empty() ){ + lits.push_back( n ); }else { //collect the equivalence classes this literal belongs to, and the new variables it contributes std::vector< int > eqcs; @@ -1293,8 +1131,8 @@ Node QuantifiersRewriter::computeSplit( Node f, std::vector< Node >& args, Node eqc_to_lit[eqcz].push_back(n); } } - if ( eqc_active>1 || !lits.empty() ){ - Trace("clause-split-debug") << "Split clause " << f << std::endl; + if ( eqc_active>1 || !lits.empty() || var_to_eqc.size()!=args.size() ){ + Trace("clause-split-debug") << "Split quantified formula with body " << body << std::endl; Trace("clause-split-debug") << " Ground literals: " << std::endl; for( size_t i=0; i<lits.size(); i++) { Trace("clause-split-debug") << " " << lits[i] << std::endl; @@ -1317,27 +1155,21 @@ Node QuantifiersRewriter::computeSplit( Node f, std::vector< Node >& args, Node Node fa = NodeManager::currentNM()->mkNode( FORALL, bvl, body ); lits.push_back(fa); } - Assert( lits.size()>1 ); - Node nf = NodeManager::currentNM()->mkNode(OR,lits); + Assert( !lits.empty() ); + Node nf = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode(OR,lits); Trace("clause-split-debug") << "Made node : " << nf << std::endl; return nf; + }else{ + return mkForAll( args, body, qa ); } - return f; } Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ){ - std::vector< Node > activeArgs; - //if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables - if( options::ceGuidedInst() && qa.d_sygus ){ - activeArgs.insert( activeArgs.end(), args.begin(), args.end() ); - }else{ - computeArgVec2( args, activeArgs, body, qa.d_ipl ); - } - if( activeArgs.empty() ){ + if( args.empty() ){ return body; }else{ std::vector< Node > children; - children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, activeArgs ) ); + children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) ); children.push_back( body ); if( !qa.d_ipl.isNull() ){ children.push_back( qa.d_ipl ); @@ -1346,82 +1178,59 @@ Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, QAttri } } -Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, QAttributes& qa ){ +//computes miniscoping, also eliminates variables that do not occur free in body +Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ){ if( body.getKind()==FORALL ){ - //combine arguments + //combine prenex std::vector< Node > newArgs; - for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ + newArgs.insert( newArgs.end(), args.begin(), args.end() ); + for( unsigned i=0; i<body[0].getNumChildren(); i++ ){ newArgs.push_back( body[0][i] ); } - newArgs.insert( newArgs.end(), args.begin(), args.end() ); - return mkForAll( newArgs, body[ 1 ], qa ); - }else{ - if( body.getKind()==NOT ){ - //push not downwards - if( body[0].getKind()==NOT ){ - return computeMiniscoping( f, args, body[0][0], qa ); - }else if( body[0].getKind()==AND ){ - if( options::miniscopeQuantFreeVar() ){ - NodeBuilder<> t(kind::OR); - for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ - t << ( body[0][i].getKind()==NOT ? body[0][i][0] : body[0][i].notNode() ); - } - return computeMiniscoping( f, args, t.constructNode(), qa ); - } - }else if( body[0].getKind()==OR ){ - if( options::miniscopeQuant() ){ - NodeBuilder<> t(kind::AND); - for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ - Node trm = body[0][i].negate(); - t << computeMiniscoping( f, args, trm, qa ); - } - return t.constructNode(); + return mkForAll( newArgs, body[1], qa ); + }else if( body.getKind()==AND ){ + if( options::miniscopeQuant() ){ + //break apart + NodeBuilder<> t(kind::AND); + for( unsigned i=0; i<body.getNumChildren(); i++ ){ + t << computeMiniscoping( args, body[i], qa ); + } + Node retVal = t; + return retVal; + } + }else if( body.getKind()==OR ){ + if( options::quantSplit() ){ + //splitting subsumes free variable miniscoping, apply it with higher priority + return computeSplit( args, body, qa ); + }else if( options::miniscopeQuantFreeVar() ){ + Node newBody = body; + NodeBuilder<> body_split(kind::OR); + NodeBuilder<> tb(kind::OR); + for( unsigned i=0; i<body.getNumChildren(); i++ ){ + Node trm = body[i]; + if( TermDb::containsTerms( body[i], args ) ){ + tb << trm; + }else{ + body_split << trm; } } - }else if( body.getKind()==AND ){ - if( options::miniscopeQuant() ){ - //break apart - NodeBuilder<> t(kind::AND); - for( unsigned i=0; i<body.getNumChildren(); i++ ){ - t << computeMiniscoping( f, args, body[i], qa ); - } - Node retVal = t; - return retVal; - } - }else if( body.getKind()==OR ){ - if( options::quantSplit() ){ - //splitting subsumes free variable miniscoping, apply it with higher priority - Node nf = computeSplit( f, args, body ); - if( nf!=f ){ - return nf; - } - }else if( options::miniscopeQuantFreeVar() ){ - Node newBody = body; - NodeBuilder<> body_split(kind::OR); - NodeBuilder<> tb(kind::OR); - for( unsigned i=0; i<body.getNumChildren(); i++ ){ - Node trm = body[i]; - if( TermDb::containsTerms( body[i], args ) ){ - tb << trm; - }else{ - body_split << trm; - } - } - if( tb.getNumChildren()==0 ){ - return body_split; - }else if( body_split.getNumChildren()>0 ){ - newBody = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb; - body_split << mkForAll( args, newBody, qa ); - return body_split.getNumChildren()==1 ? body_split.getChild( 0 ) : body_split; - } + if( tb.getNumChildren()==0 ){ + return body_split; + }else if( body_split.getNumChildren()>0 ){ + newBody = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb; + std::vector< Node > activeArgs; + computeArgVec2( args, activeArgs, newBody, qa.d_ipl ); + body_split << mkForAll( activeArgs, newBody, qa ); + return body_split.getNumChildren()==1 ? body_split.getChild( 0 ) : body_split; } } + }else if( body.getKind()==NOT ){ + Assert( isLiteral( body[0] ) ); } - //if( body==f[1] ){ - // return f; - //}else{ - return mkForAll( args, body, qa ); - //} + //remove variables that don't occur + std::vector< Node > activeArgs; + computeArgVec2( args, activeArgs, body, qa.d_ipl ); + return mkForAll( activeArgs, body, qa ); } Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& args, Node body ){ @@ -1539,8 +1348,6 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q return is_std; }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ return options::aggressiveMiniscopeQuant() && is_std; - }else if( computeOption==COMPUTE_NNF ){ - return true; }else if( computeOption==COMPUTE_PROCESS_TERMS ){ return options::condRewriteQuant(); }else if( computeOption==COMPUTE_COND_SPLIT ){ @@ -1549,8 +1356,6 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant() && is_std; }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ return ( options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant() ) && is_std; - //}else if( computeOption==COMPUTE_CNF ){ - // return options::cnfQuant(); }else if( computeOption==COMPUTE_PURIFY_EXPAND ){ return options::purifyQuant() && is_std; }else{ @@ -1570,11 +1375,9 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut n = computeElimSymbols( n ); }else if( computeOption==COMPUTE_MINISCOPING ){ //return directly - return computeMiniscoping( f, args, n, qa ); + return computeMiniscoping( args, n, qa ); }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ return computeAggressiveMiniscoping( args, n ); - }else if( computeOption==COMPUTE_NNF ){ - n = computeNNF( n ); }else if( computeOption==COMPUTE_PROCESS_TERMS ){ std::vector< Node > new_conds; n = computeProcessTerms( n, args, new_conds, f, qa ); @@ -1588,9 +1391,6 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut n = computePrenex( n, args, true ); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ n = computeVarElimination( n, args, qa ); - //}else if( computeOption==COMPUTE_CNF ){ - //n = computeCNF( n, args, defs, false ); - //ipl = Node::null(); }else if( computeOption==COMPUTE_PURIFY_EXPAND ){ std::vector< Node > conj; computePurifyExpand( n, conj, args, qa ); @@ -1724,15 +1524,15 @@ struct ContainsQuantAttributeId {}; typedef expr::Attribute<ContainsQuantAttributeId, uint64_t> ContainsQuantAttribute; // check if the given node contains a universal quantifier -bool QuantifiersRewriter::containsQuantifiers(Node n) { +bool QuantifiersRewriter::containsQuantifiers( Node n ){ if( n.hasAttribute(ContainsQuantAttribute()) ){ return n.getAttribute(ContainsQuantAttribute())==1; - } else if(n.getKind() == kind::FORALL) { + }else if( n.getKind() == kind::FORALL ){ return true; - } else { + }else{ bool cq = false; for( unsigned i = 0; i < n.getNumChildren(); ++i ){ - if( containsQuantifiers(n[i]) ){ + if( containsQuantifiers( n[i] ) ){ cq = true; break; } diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 2071d1793..776517109 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -38,6 +38,7 @@ public: static int getPurifyId( Node n ); static int getPurifyIdLit( Node n ); private: + static bool addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged ); static void addNodeToOrBuilder( Node n, NodeBuilder<>& t ); static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ); static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n, std::map< Node, bool >& visited ); @@ -46,7 +47,6 @@ private: static Node computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond, std::map< Node, Node >& cache, std::map< Node, Node >& icache, std::vector< Node >& new_vars, std::vector< Node >& new_conds ); - static Node computeClause( Node n ); static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj ); static bool isConditionalVariableElim( Node n, int pol=0 ); static bool isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent ); @@ -57,15 +57,13 @@ private: static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa, std::map< Node, std::vector< int > >& var_parent ); private: static Node computeElimSymbols( Node body ); - static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, QAttributes& qa ); + static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body ); - static Node computeNNF( Node body ); //cache is dependent upon currCond, icache is not, new_conds are negated conditions static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa ); static Node computeCondSplit( Node body, QAttributes& qa ); - static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ); static Node computePrenex( Node body, std::vector< Node >& args, bool pol ); - static Node computeSplit( Node f, std::vector< Node >& args, Node body ); + static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa ); static Node computePurify( Node body, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent ); static void computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, QAttributes& qa ); @@ -74,7 +72,6 @@ private: COMPUTE_ELIM_SYMBOLS = 0, COMPUTE_MINISCOPING, COMPUTE_AGGRESSIVE_MINISCOPING, - COMPUTE_NNF, COMPUTE_PROCESS_TERMS, COMPUTE_PRENEX, COMPUTE_VAR_ELIMINATION, diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h index 38fea4f45..e682955e7 100644 --- a/src/theory/quantifiers/symmetry_breaking.h +++ b/src/theory/quantifiers/symmetry_breaking.h @@ -42,9 +42,7 @@ class SubsortSymmetryBreaker { typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; - //typedef context::CDChunkList<int> IntList; typedef context::CDList<Node> NodeList; - typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap; private: /** quantifiers engine */ QuantifiersEngine* d_qe; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 5645c3401..c34d86497 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -238,10 +238,15 @@ void TermDb::computeUfTerms( TNode f ) { if( it!=d_op_map.end() ){ eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); Trace("term-db-debug") << "Adding terms for operator " << f << std::endl; + unsigned congruentCount = 0; + unsigned nonCongruentCount = 0; + unsigned alreadyCongruentCount = 0; + unsigned relevantCount = 0; for( unsigned i=0; i<it->second.size(); i++ ){ Node n = it->second[i]; //to be added to term index, term must be relevant, and exist in EE if( hasTermCurrent( n ) && ee->hasTerm( n ) ){ + relevantCount++; if( isTermActive( n ) ){ computeArgReps( n ); @@ -260,7 +265,7 @@ void TermDb::computeUfTerms( TNode f ) { if( at!=n && ee->areEqual( at, n ) ){ setTermInactive( n ); Trace("term-db-debug") << n << " is redundant." << std::endl; - //congruentCount++; + congruentCount++; }else{ if( at!=n && ee->areDisequal( at, n, false ) ){ std::vector< Node > lits; @@ -282,29 +287,22 @@ void TermDb::computeUfTerms( TNode f ) { d_consistent_ee = false; return; } - //nonCongruentCount++; + nonCongruentCount++; d_op_nonred_count[ f ]++; } }else{ Trace("term-db-debug") << n << " is already redundant." << std::endl; - //congruentCount++; - //alreadyCongruentCount++; + alreadyCongruentCount++; } }else{ Trace("term-db-debug") << n << " is not relevant." << std::endl; - //nonRelevantCount++; } } - - /* - if( Trace.isOn("term-db-index") ){ - Trace("term-db-index") << "Term index for " << f << " : " << std::endl; - Trace("term-db-index") << "- " << it->first << std::endl; - d_func_map_trie[ f ].debugPrint("term-db-index", it->second[0]); - Trace("term-db-index") << "Non-Congruent/Congruent/Non-Relevant = "; - Trace("term-db-index") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl; + if( Trace.isOn("tdb") ){ + Trace("tdb") << "Term db size [" << f << "] : " << nonCongruentCount << " / "; + Trace("tdb") << ( nonCongruentCount + congruentCount ) << " / " << ( nonCongruentCount + congruentCount + alreadyCongruentCount ) << " / "; + Trace("tdb") << relevantCount << " / " << it->second.size() << std::endl; } - */ } } } @@ -676,10 +674,6 @@ void TermDb::presolve() { } bool TermDb::reset( Theory::Effort effort ){ - //int nonCongruentCount = 0; - //int congruentCount = 0; - //int alreadyCongruentCount = 0; - //int nonRelevantCount = 0; d_op_nonred_count.clear(); d_arg_reps.clear(); d_func_map_trie.clear(); @@ -743,20 +737,6 @@ bool TermDb::reset( Theory::Effort effort ){ } } */ - /* - Trace("term-db-stats") << "TermDb: Reset" << std::endl; - Trace("term-db-stats") << "Non-Congruent/Congruent/Non-Relevant = "; - Trace("term-db-stats") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl; - if( Trace.isOn("term-db-index") ){ - Trace("term-db-index") << "functions : " << std::endl; - for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ - if( it->second.size()>0 ){ - Trace("term-db-index") << "- " << it->first << std::endl; - d_func_map_trie[ it->first ].debugPrint("term-db-index", it->second[0]); - } - } - } - */ return true; } diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 214a4d055..802acc089 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -86,7 +86,7 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes ) } Trigger::~Trigger() { - if(d_mg != NULL) { delete d_mg; } + delete d_mg; } void Trigger::resetInstantiationRound(){ |