diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 195 |
1 files changed, 1 insertions, 194 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 6d8570287..c66324445 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -548,8 +548,7 @@ Node QuantifiersRewriter::computeExtendedRewrite(Node q) { Node body = q[1]; // apply extended rewriter - ExtendedRewriter er; - Node bodyr = er.extendedRewrite(body); + Node bodyr = Rewriter::callExtendedRewrite(body); if (body != bodyr) { std::vector<Node> children; @@ -1407,92 +1406,6 @@ Node QuantifiersRewriter::computePrenex(Node q, return body; } -Node QuantifiersRewriter::computePrenexAgg(Node n, - std::map<Node, Node>& visited) -{ - std::map< Node, Node >::iterator itv = visited.find( n ); - if( itv!=visited.end() ){ - return itv->second; - } - if (!expr::hasClosure(n)) - { - // trivial - return n; - } - NodeManager* nm = NodeManager::currentNM(); - Node ret = n; - if (n.getKind() == NOT) - { - ret = computePrenexAgg(n[0], visited).negate(); - } - else if (n.getKind() == FORALL) - { - std::vector<Node> children; - children.push_back(computePrenexAgg(n[1], visited)); - std::vector<Node> args; - args.insert(args.end(), n[0].begin(), n[0].end()); - // for each child, strip top level quant - for (unsigned i = 0; i < children.size(); i++) - { - if (children[i].getKind() == FORALL) - { - args.insert(args.end(), children[i][0].begin(), children[i][0].end()); - children[i] = children[i][1]; - } - } - // keep the pattern - std::vector<Node> iplc; - if (n.getNumChildren() == 3) - { - iplc.insert(iplc.end(), n[2].begin(), n[2].end()); - } - Node nb = children.size() == 1 ? children[0] : nm->mkNode(OR, children); - ret = mkForall(args, nb, iplc, true); - } - else - { - std::unordered_set<Node> argsSet; - std::unordered_set<Node> nargsSet; - Node q; - Node nn = computePrenex(q, n, argsSet, nargsSet, true, true); - Assert(n != nn || argsSet.empty()); - Assert(n != nn || nargsSet.empty()); - if (n != nn) - { - Node nnn = computePrenexAgg(nn, visited); - // merge prenex - if (nnn.getKind() == FORALL) - { - argsSet.insert(nnn[0].begin(), nnn[0].end()); - nnn = nnn[1]; - // pos polarity variables are inner - if (!argsSet.empty()) - { - nnn = mkForall({argsSet.begin(), argsSet.end()}, nnn, true); - } - argsSet.clear(); - } - else if (nnn.getKind() == NOT && nnn[0].getKind() == FORALL) - { - nargsSet.insert(nnn[0][0].begin(), nnn[0][0].end()); - nnn = nnn[0][1].negate(); - } - if (!nargsSet.empty()) - { - nnn = mkForall({nargsSet.begin(), nargsSet.end()}, nnn.negate(), true) - .negate(); - } - if (!argsSet.empty()) - { - nnn = mkForall({argsSet.begin(), argsSet.end()}, nnn, true); - } - ret = nnn; - } - } - visited[n] = ret; - return ret; -} - Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ) { Assert(body.getKind() == OR); size_t var_found_count = 0; @@ -2000,112 +1913,6 @@ bool QuantifiersRewriter::isPrenexNormalForm( Node n ) { } } -Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs ){ - Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << endl; - if( n.getKind()==kind::NOT ){ - Node nn = preSkolemizeQuantifiers( n[0], !polarity, fvTypes, fvs ); - return nn.negate(); - }else if( n.getKind()==kind::FORALL ){ - if (n.getNumChildren() == 3) - { - // Do not pre-skolemize quantified formulas with three children. - // This includes non-standard quantified formulas - // like recursive function definitions, or sygus conjectures, and - // quantified formulas with triggers. - return n; - } - else if (polarity) - { - if( options::preSkolemQuant() && options::preSkolemQuantNested() ){ - vector< Node > children; - children.push_back( n[0] ); - //add children to current scope - std::vector< TypeNode > fvt; - std::vector< TNode > fvss; - fvt.insert( fvt.begin(), fvTypes.begin(), fvTypes.end() ); - fvss.insert( fvss.begin(), fvs.begin(), fvs.end() ); - for( int i=0; i<(int)n[0].getNumChildren(); i++ ){ - fvt.push_back( n[0][i].getType() ); - fvss.push_back( n[0][i] ); - } - //process body - children.push_back( preSkolemizeQuantifiers( n[1], polarity, fvt, fvss ) ); - //return processed quantifier - return NodeManager::currentNM()->mkNode( kind::FORALL, children ); - } - }else{ - //process body - Node nn = preSkolemizeQuantifiers( n[1], polarity, fvTypes, fvs ); - std::vector< Node > sk; - Node sub; - std::vector< unsigned > sub_vars; - //return skolemized body - return Skolemize::mkSkolemizedBody( - n, nn, fvTypes, fvs, sk, sub, sub_vars); - } - }else{ - //check if it contains a quantifier as a subterm - //if so, we will write this node - if (expr::hasClosure(n)) - { - if( ( n.getKind()==kind::ITE && n.getType().isBoolean() ) || ( n.getKind()==kind::EQUAL && n[0].getType().isBoolean() ) ){ - if( options::preSkolemQuantAgg() ){ - Node nn; - //must remove structure - if( n.getKind()==kind::ITE ){ - nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ), - NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) ); - }else if( n.getKind()==kind::EQUAL ){ - nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ), - NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) ); - } - return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs ); - } - }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){ - vector< Node > children; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvTypes, fvs ) ); - } - return NodeManager::currentNM()->mkNode( n.getKind(), children ); - } - } - } - return n; -} - -TrustNode QuantifiersRewriter::preprocess(Node n, bool isInst) -{ - Node prev = n; - - if( options::preSkolemQuant() ){ - if( !isInst || !options::preSkolemQuantNested() ){ - Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl; - //apply pre-skolemization to existential quantifiers - std::vector< TypeNode > fvTypes; - std::vector< TNode > fvs; - n = preSkolemizeQuantifiers( prev, true, fvTypes, fvs ); - } - } - //pull all quantifiers globally - if (options::prenexQuant() == options::PrenexQuantMode::NORMAL) - { - Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl; - std::map<Node, Node> visited; - n = computePrenexAgg(n, visited); - n = Rewriter::rewrite( n ); - Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl; - //Assert( isPrenexNormalForm( n ) ); - } - if( n!=prev ){ - Trace("quantifiers-preprocess") << "Preprocess " << prev << std::endl; - Trace("quantifiers-preprocess") << "..returned " << n << std::endl; - return TrustNode::mkTrustRewrite(prev, n, nullptr); - } - return TrustNode::null(); -} - } // namespace quantifiers } // namespace theory } // namespace cvc5 |