diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/equality_infer.h | 13 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 71 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_util.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 8 |
4 files changed, 16 insertions, 78 deletions
diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h index 4a6943119..70b05c351 100644 --- a/src/theory/quantifiers/equality_infer.h +++ b/src/theory/quantifiers/equality_infer.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef EQUALITY_INFER_H -#define EQUALITY_INFER_H +#ifndef __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H +#define __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H #include <ext/hash_set> #include <iostream> @@ -60,14 +60,17 @@ private: /** use list */ NodeListMap d_uselist; void addToUseList( Node used, Node eqc ); + /** pending merges */ + NodeList d_pending_merges; public: EqualityInference(context::Context* c); virtual ~EqualityInference(); - /** notification when equality engine is updated */ + /** input : notification when equality engine is updated */ void eqNotifyNewClass(TNode t); void eqNotifyMerge(TNode t1, TNode t2); - - NodeList d_pending_merges; + /** output : inferred equalities */ + unsigned getNumPendingMerges() { return d_pending_merges.size(); } + Node getPendingMerge( unsigned i ) { return d_pending_merges[i]; } }; } diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 3d649f302..1f1efa2a8 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -113,9 +113,8 @@ Node QuantArith::mkNode( std::map< Node, Node >& msum ) { // given (msum <k> 0), solve (veq_c * v <k> val) or (val <k> veq_c * v), where: // veq_c is either null (meaning 1), or positive. -// return value -1: veq_c*v is LHS. - -int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff ) { +// return value 1: veq_c*v is RHS, -1: veq_c*v is LHS, 0: failed. +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; @@ -136,75 +135,20 @@ int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind children.push_back(m); } } - veq = children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) : + val = children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) : (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) )); - Node vc = v; - if( !r.isOne() && !r.isNegativeOne() ){ - if( vc.getType().isInteger() ){ - if( doCoeff ){ - vc = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( r.abs() ), vc ); - }else{ - return 0; - } - }else{ - veq = NodeManager::currentNM()->mkNode( MULT, veq, NodeManager::currentNM()->mkConst( Rational(1) / r.abs() ) ); - } - } - if( r.sgn()==1 ){ - veq = negate(veq); - } - veq = Rewriter::rewrite( veq ); - bool inOrder = r.sgn()==1 || k==EQUAL; - veq = NodeManager::currentNM()->mkNode( k, inOrder ? vc : veq, inOrder ? veq : vc ); - return inOrder ? 1 : -1; - } - } - return 0; -} - -int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ) { - Node vatom; - //isolate pv in the inequality - int ires = isolate( v, msum, vatom, k, true ); - if( ires!=0 ){ - val = vatom[ ires==1 ? 1 : 0 ]; - Node pvm = vatom[ ires==1 ? 0 : 1 ]; - //get monomial - if( pvm!=v ){ - Node veq_v; - if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){ - Assert( veq_v==v ); - } - } - } - return ires; -} - -/* -int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ) { - Assert( k==EQUAL || k==GEQ ); - std::map< Node, Node >::iterator itv = msum.find( v ); - if( itv!=msum.end() ){ - Rational r = itv->second.isNull() ? Rational(1) : itv->second.getConst<Rational>(); - if( r.sgn()!=0 ){ - veq_c = itv->second; - msum.erase( itv ); - val = mkNode( msum ); - msum[v] = veq_c; 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() ) ); - veq_c = Node::null(); } - }else{ - veq_c = Node::null(); } if( r.sgn()==1 ){ - val = negate( val ); + val = negate(val); + }else{ + val = Rewriter::rewrite( val ); } - val = Rewriter::rewrite( val ); return ( r.sgn()==1 || k==EQUAL ) ? 1 : -1; } } @@ -230,7 +174,6 @@ int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind } return ires; } -*/ Node QuantArith::solveEqualityFor( Node lit, Node v ) { Assert( lit.getKind()==EQUAL || lit.getKind()==IFF ); @@ -241,7 +184,7 @@ Node QuantArith::solveEqualityFor( Node lit, Node v ) { return lit[1-r]; } } - if( tn.isInteger() || tn.isReal() ){ + if( tn.isReal() ){ if( quantifiers::TermDb::containsTerm( lit, v ) ){ std::map< Node, Node > msum; if( QuantArith::getMonomialSumLit( lit, msum ) ){ diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 0327651d7..31743d352 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -38,8 +38,8 @@ public: static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum ); static Node mkNode( std::map< Node, Node >& msum ); //return 1 : solved on LHS, return -1 : solved on RHS, return 0: failed - static int isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff = false ); static int isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ); + static int isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff = false ); static Node solveEqualityFor( Node lit, Node v ); static Node negate( Node t ); static Node offset( Node t, int i ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index a2ce9c368..3b74cf352 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -319,14 +319,6 @@ TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsR TNode nn = d_func_map_trie[f].existsTerm( args ); Trace("term-db-eval") << "Got term " << nn << std::endl; return nn; - if( !nn.isNull() ){ - if( ee->hasTerm( nn ) ){ - Trace("term-db-eval") << "return rep " << std::endl; - return ee->getRepresentative( nn ); - }else{ - //Assert( false ); - } - } } } } |