diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-10 17:49:13 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-10 17:49:13 -0600 |
commit | d0df704a60696d7f824eb01781b413d91a0e4202 (patch) | |
tree | 501058c359ff029cad024a3a715efdf33968c426 /src/theory/quantifiers/quant_conflict_find.cpp | |
parent | 346c85d145f6938ce7dce74e7e7cb855d5a6025a (diff) |
Faster conditional rewriting for and/or beneath quantifiers. Improvements to sort inference, related to constants. Add several quantifiers options, minor refactoring.
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 779c0c44e..93cd4be91 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -843,7 +843,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) d_qni_size++; d_type_not = false; d_n = n; - //Node f = getOperator( n ); + //Node f = getMatchOperator( n ); for( unsigned j=0; j<d_n.getNumChildren(); j++ ){ Node nn = d_n[j]; Trace("qcf-qregister-debug") << " " << d_qni_size; @@ -1106,7 +1106,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { } }else if( d_type==typ_var ){ Assert( isHandledUfTerm( d_n ) ); - Node f = getOperator( p, d_n ); + Node f = getMatchOperator( p, d_n ); Debug("qcf-match-debug") << " reset: Var will match operators of " << f << std::endl; TermArgTrie * qni = p->getTermDatabase()->getTermArgTrie( Node::null(), f ); if( qni!=NULL ){ @@ -1339,7 +1339,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { /* if( d_type==typ_var && p->d_effort==QuantConflictFind::effort_mc && !d_matched_basis ){ d_matched_basis = true; - Node f = getOperator( d_n ); + Node f = getMatchOperator( d_n ); TNode mbo = p->getTermDatabase()->getModelBasisOpTerm( f ); if( qi->setMatch( p, d_qni_var_num[0], mbo ) ){ success = true; @@ -1702,9 +1702,9 @@ bool MatchGen::isHandledUfTerm( TNode n ) { return inst::Trigger::isAtomicTriggerKind( n.getKind() ); } -Node MatchGen::getOperator( QuantConflictFind * p, Node n ) { +Node MatchGen::getMatchOperator( QuantConflictFind * p, Node n ) { if( isHandledUfTerm( n ) ){ - return p->getTermDatabase()->getOperator( n ); + return p->getTermDatabase()->getMatchOperator( n ); }else{ return Node::null(); } @@ -1896,7 +1896,7 @@ void QuantConflictFind::assertNode( Node q ) { Node QuantConflictFind::evaluateTerm( Node n ) { if( MatchGen::isHandledUfTerm( n ) ){ - Node f = MatchGen::getOperator( this, n ); + Node f = MatchGen::getMatchOperator( this, n ); Node nn; if( getEqualityEngine()->hasTerm( n ) ){ nn = getTermDatabase()->existsTerm( f, n ); |