diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-30 06:33:23 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-30 06:33:23 -0600 |
commit | f1c8b8cda3b99353adbe424e0bf1259147001f3c (patch) | |
tree | c0b939982d46084e7a0e71c78bb5f1caa4877250 /src/theory/quantifiers/quant_util.cpp | |
parent | 0524281144b562fea63adf10bc3f5d6f75883296 (diff) |
Remove remaining references to QuantArith (#1408)
Diffstat (limited to 'src/theory/quantifiers/quant_util.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 238 |
1 files changed, 0 insertions, 238 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 571c3846a..ccc6e99a8 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -52,244 +52,6 @@ quantifiers::TermDb * QuantifiersModule::getTermDatabase() { quantifiers::TermUtil * QuantifiersModule::getTermUtil() { return d_quantEngine->getTermUtil(); -} - -bool QuantArith::getMonomial( Node n, Node& c, Node& v ){ - if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){ - c = n[0]; - v = n[1]; - return true; - }else{ - return false; - } -} -bool QuantArith::getMonomial( Node n, std::map< Node, Node >& msum ) { - if( n.isConst() ){ - if( msum.find(Node::null())==msum.end() ){ - msum[Node::null()] = n; - return true; - } - }else if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){ - if( msum.find(n[1])==msum.end() ){ - msum[n[1]] = n[0]; - return true; - } - }else{ - if( msum.find(n)==msum.end() ){ - msum[n] = Node::null(); - return true; - } - } - return false; -} - -bool QuantArith::getMonomialSum( Node n, std::map< Node, Node >& msum ) { - if ( n.getKind()==PLUS ){ - for( unsigned i=0; i<n.getNumChildren(); i++) { - if (!getMonomial( n[i], msum )){ - return false; - } - } - return true; - }else{ - return getMonomial( n, msum ); - } -} - -bool QuantArith::getMonomialSumLit( Node lit, std::map< Node, Node >& msum ) { - if( lit.getKind()==GEQ || lit.getKind()==EQUAL ){ - if( getMonomialSum( lit[0], msum ) ){ - if( lit[1].isConst() && lit[1].getConst<Rational>().isZero() ){ - return true; - }else{ - //subtract the other side - std::map< Node, Node > msum2; - if( getMonomialSum( lit[1], msum2 ) ){ - for( std::map< Node, Node >::iterator it = msum2.begin(); it != msum2.end(); ++it ){ - std::map< Node, Node >::iterator it2 = msum.find( it->first ); - if( it2!=msum.end() ){ - Node r = NodeManager::currentNM()->mkNode( MINUS, it2->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it2->second, - it->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it->second ); - msum[it->first] = Rewriter::rewrite( r ); - }else{ - msum[it->first] = it->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(-1) ) : negate( it->second ); - } - } - return true; - } - } - } - } - return false; -} - -Node QuantArith::mkNode( std::map< Node, Node >& msum ) { - std::vector< Node > children; - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - Node m; - if( !it->first.isNull() ){ - if( !it->second.isNull() ){ - m = NodeManager::currentNM()->mkNode( MULT, it->second, it->first ); - }else{ - m = it->first; - } - }else{ - Assert( !it->second.isNull() ); - m = it->second; - } - children.push_back(m); - } - return children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) : (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) )); -} - -Node QuantArith::mkCoeffTerm( Node coeff, Node t ) { - if( coeff.isNull() ){ - return t; - }else{ - return NodeManager::currentNM()->mkNode( kind::MULT, coeff, t ); - } -} - -int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ) { - std::map< Node, Node >::iterator itv = msum.find( v ); - if( itv!=msum.end() ){ - std::vector< Node > children; - Rational r = itv->second.isNull() ? Rational(1) : itv->second.getConst<Rational>(); - if ( r.sgn()!=0 ){ - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - if( it->first!=v ){ - Node m; - if( !it->first.isNull() ){ - if ( !it->second.isNull() ){ - m = NodeManager::currentNM()->mkNode( MULT, it->second, it->first ); - }else{ - m = it->first; - } - }else{ - m = it->second; - } - children.push_back(m); - } - } - val = children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) : - (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) )); - if( !r.isOne() && !r.isNegativeOne() ){ - if( v.getType().isInteger() ){ - veq_c = NodeManager::currentNM()->mkConst( r.abs() ); - }else{ - val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / r.abs() ) ); - } - } - if( r.sgn()==1 ){ - val = negate(val); - }else{ - val = Rewriter::rewrite( val ); - } - return ( r.sgn()==1 || k==EQUAL ) ? 1 : -1; - } - } - return 0; -} - -int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff ) { - Node veq_c; - Node val; - //isolate v in the (in)equality - int ires = isolate( v, msum, veq_c, val, k ); - if( ires!=0 ){ - Node vc = v; - if( !veq_c.isNull() ){ - if( doCoeff ){ - vc = NodeManager::currentNM()->mkNode( MULT, veq_c, vc ); - }else{ - return 0; - } - } - bool inOrder = ires==1; - veq = NodeManager::currentNM()->mkNode( k, inOrder ? vc : val, inOrder ? val : vc ); - } - return ires; -} - -Node QuantArith::solveEqualityFor( Node lit, Node v ) { - Assert( lit.getKind()==EQUAL ); - //first look directly at sides - TypeNode tn = lit[0].getType(); - for( unsigned r=0; r<2; r++ ){ - if( lit[r]==v ){ - return lit[1-r]; - } - } - if( tn.isReal() ){ - if( quantifiers::TermUtil::containsTerm( lit, v ) ){ - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( lit, msum ) ){ - Node val, veqc; - if( QuantArith::isolate( v, msum, veqc, val, EQUAL )!=0 ){ - if( veqc.isNull() ){ - // in this case, we have an integer equality with a coefficient - // on the variable we solved for that could not be eliminated, - // hence we fail. - return val; - } - } - } - } - } - return Node::null(); -} - -bool QuantArith::decompose(Node n, Node v, Node& coeff, Node& rem) -{ - std::map<Node, Node> msum; - if (getMonomialSum(n, msum)) - { - std::map<Node, Node>::iterator it = msum.find(v); - if (it == msum.end()) - { - return false; - } - else - { - coeff = it->second; - msum.erase(v); - rem = mkNode(msum); - return true; - } - } - else - { - return false; - } -} - -Node QuantArith::negate( Node t ) { - Node tt = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) ), t ); - tt = Rewriter::rewrite( tt ); - return tt; -} - -Node QuantArith::offset( Node t, int i ) { - Node tt = NodeManager::currentNM()->mkNode( PLUS, NodeManager::currentNM()->mkConst( Rational(i) ), t ); - tt = Rewriter::rewrite( tt ); - return tt; -} - -void QuantArith::debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c ) { - for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - Trace(c) << " "; - if( !it->second.isNull() ){ - Trace(c) << it->second; - if( !it->first.isNull() ){ - Trace(c) << " * "; - } - } - if( !it->first.isNull() ){ - Trace(c) << it->first; - } - Trace(c) << std::endl; - } - Trace(c) << std::endl; } QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){ |