From b22464914f54de6a64e01cb26b7c0b08d2640dab Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 16 Dec 2015 11:24:09 +0100 Subject: [PATCH] Work on purification for quantifiers, minor updates. --- .../quantifiers/quantifiers_rewriter.cpp | 77 ++++++++++++++++--- src/theory/quantifiers/quantifiers_rewriter.h | 9 ++- 2 files changed, 73 insertions(+), 13 deletions(-) diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 0afc8b1bb..798576ec3 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -85,15 +85,47 @@ bool QuantifiersRewriter::isCube( Node n ){ } int QuantifiersRewriter::getPurifyId( Node n ){ - if( inst::Trigger::isAtomicTriggerKind( n.getKind() ) ){ + if( !TermDb::hasBoundVarAttr( n ) ){ + return 0; + }else if( inst::Trigger::isAtomicTriggerKind( n.getKind() ) ){ return 1; - }else if( TermDb::isBoolConnective( n.getKind() ) || n.getKind()==EQUAL || n.getKind()==BOUND_VARIABLE || !TermDb::hasBoundVarAttr( n ) ){ + }else if( TermDb::isBoolConnective( n.getKind() ) || n.getKind()==EQUAL || n.getKind()==BOUND_VARIABLE ){ return 0; }else{ return -1; } } +int QuantifiersRewriter::getPurifyIdLit2( Node n, std::map< Node, int >& visited ) { + std::map< Node, int >::iterator it = visited.find( n ); + if( visited.find( n )==visited.end() ){ + int ret = 0; + if( TermDb::hasBoundVarAttr( n ) ){ + ret = getPurifyId( n ); + for( unsigned i=0; isecond; + } +} + +int QuantifiersRewriter::getPurifyIdLit( Node n ) { + std::map< Node, int > visited; + return getPurifyIdLit2( n, visited ); +} + void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){ if( n.getKind()==OR ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ @@ -684,7 +716,7 @@ bool QuantifiersRewriter::isConditionalVariableElim( Node n, int pol ){ return false; } -Node QuantifiersRewriter::computeProcessIte( Node body, Node ipl ){ +Node QuantifiersRewriter::computeCondSplit( Node body, Node ipl ){ if( options::iteDtTesterSplitQuant() && body.getKind()==ITE ){ Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl; std::map< Node, Node > pcons; @@ -1408,7 +1440,7 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption }else if( computeOption==COMPUTE_PROCESS_TERMS ){ return true; //return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant(); - }else if( computeOption==COMPUTE_PROCESS_ITE ){ + }else if( computeOption==COMPUTE_COND_SPLIT ){ return options::iteDtTesterSplitQuant() || options::condVarSplitQuant(); }else if( computeOption==COMPUTE_PRENEX ){ return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant(); @@ -1416,6 +1448,8 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption return options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant(); //}else if( computeOption==COMPUTE_CNF ){ // return options::cnfQuant(); + }else if( computeOption==COMPUTE_PURIFY_EXPAND ){ + return options::purifyQuant(); }else{ return false; } @@ -1426,10 +1460,9 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp if( f.getKind()==FORALL ){ Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << ", nested = " << isNested << std::endl; std::vector< Node > args; - for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ + for( unsigned i=0; i defs(kind::AND); Node n = f[1]; Node ipl; if( f.getNumChildren()==3 ){ @@ -1454,8 +1487,8 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp new_conds.push_back( n ); n = NodeManager::currentNM()->mkNode( OR, new_conds ); } - }else if( computeOption==COMPUTE_PROCESS_ITE ){ - n = computeProcessIte( n, ipl ); + }else if( computeOption==COMPUTE_COND_SPLIT ){ + n = computeCondSplit( n, ipl ); }else if( computeOption==COMPUTE_PRENEX ){ n = computePrenex( n, args, true ); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ @@ -1463,13 +1496,21 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp //}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, ipl ); + if( !conj.empty() ){ + return conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ); + }else{ + return f; + } } Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl; if( f[1]==n && args.size()==f[0].getNumChildren() ){ return f; }else{ if( args.empty() ){ - defs << n; + return n; }else{ std::vector< Node > children; children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) ); @@ -1477,9 +1518,8 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp if( !ipl.isNull() ){ children.push_back( ipl ); } - defs << NodeManager::currentNM()->mkNode(kind::FORALL, children ); + return NodeManager::currentNM()->mkNode(kind::FORALL, children ); } - return defs.getNumChildren()==1 ? defs.getChild( 0 ) : defs.constructNode(); } }else{ return f; @@ -1770,3 +1810,18 @@ Node QuantifiersRewriter::computePurify( Node body, std::vector< Node >& args, s return res; } } + +void QuantifiersRewriter::computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, Node ipl ) { + if( body.getKind()==OR ){ + Trace("quantifiers-rewrite-purify-exp") << "Purify expansion : " << body << std::endl; + std::map< int, std::vector< Node > > disj; + std::map< int, std::vector< Node > > fvs; + for( unsigned i=0; imkNode( INST_ATTRIBUTE, body ); + + } +} diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index daf5a8bad..f07b635dc 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -27,11 +27,14 @@ namespace theory { namespace quantifiers { class QuantifiersRewriter { +private: + static int getPurifyIdLit2( Node n, std::map< Node, int >& visited ); public: static bool isClause( Node n ); static bool isLiteral( Node n ); static bool isCube( Node n ); static int getPurifyId( Node n ); + static int getPurifyIdLit( Node n ); private: static void addNodeToOrBuilder( Node n, NodeBuilder<>& t ); static Node mkForAll( std::vector< Node >& args, Node body, Node ipl ); @@ -56,12 +59,13 @@ private: static Node computeProcessTerms( 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 computeProcessIte( Node body, Node ipl ); + static Node computeCondSplit( Node body, Node ipl ); 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 computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ); 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, Node ipl ); private: enum{ COMPUTE_ELIM_SYMBOLS = 0, @@ -71,7 +75,8 @@ private: COMPUTE_PROCESS_TERMS, COMPUTE_PRENEX, COMPUTE_VAR_ELIMINATION, - COMPUTE_PROCESS_ITE, + COMPUTE_COND_SPLIT, + COMPUTE_PURIFY_EXPAND, //COMPUTE_FLATTEN_ARGS_UF, //COMPUTE_CNF, COMPUTE_LAST -- 2.30.2