diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-09 21:56:40 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-09 21:56:40 -0500 |
commit | 96a0bc3b022b67b5ab79bf2ab087573c65a8d248 (patch) | |
tree | 427223e34ce9bd100ef4443c80b95a9526169363 /src/theory/quantifiers/quantifiers_rewriter.cpp | |
parent | 3b0ce95e7b7d1cbc351df9a7d2acbf3b6e13f9e7 (diff) |
Split term database (#1206)
* Move equality query to own file, move equality inference to quantifiers engine.
* Move quantifiers attributes out of TermDb and into QuantAttribute.
* Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header.
* Split term database into term util.
* Partial fix for #1205 that eliminates need for dependency in node.cpp.
* Add more references to github issues.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 02f1b8509..9f6617d5a 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -15,7 +15,9 @@ #include "theory/quantifiers/quantifiers_rewriter.h" #include "options/quantifiers_options.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" using namespace std; @@ -196,7 +198,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { }else{ //compute attributes QAttributes qa; - TermDb::computeQuantAttributes( in, qa ); + QuantAttributes::computeQuantAttributes( in, qa ); if( !qa.isRewriteRule() ){ for( int op=0; op<COMPUTE_LAST; op++ ){ if( doOperation( in, op, qa ) ){ @@ -504,10 +506,10 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n std::map< Node, Node > cache; std::map< Node, Node > icache; if( qa.isFunDef() ){ - Node h = TermDb::getFunDefHead( q ); + Node h = QuantAttributes::getFunDefHead( q ); Assert( !h.isNull() ); // if it is a function definition, rewrite the body independently - Node fbody = TermDb::getFunDefBody( q ); + Node fbody = QuantAttributes::getFunDefBody( q ); Assert( !body.isNull() ); Trace("quantifiers-rewrite-debug") << "Decompose " << h << " / " << fbody << " as function definition for " << q << "." << std::endl; Node r = computeProcessTerms2( fbody, true, true, curr_cond, 0, cache, icache, new_vars, new_conds, false ); @@ -745,7 +747,7 @@ bool QuantifiersRewriter::isConditionalVariableElim( Node n, int pol ){ }else if( n.getKind()==EQUAL ){ for( unsigned i=0; i<2; i++ ){ if( n[i].getKind()==BOUND_VARIABLE ){ - if( !TermDb::containsTerm( n[1-i], n[i] ) ){ + if( !TermUtil::containsTerm( n[1-i], n[i] ) ){ return true; } } @@ -843,7 +845,7 @@ Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){ } bool QuantifiersRewriter::isVariableElim( Node v, Node s ) { - if( TermDb::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){ + if( TermUtil::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){ return false; }else{ return true; @@ -973,7 +975,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto if( lit.getKind()==GEQ || lit.getKind()==GT ){ //compute variables in itm->first, these are not eligible for elimination std::vector< Node > bvs; - TermDb::getBoundVars( itm->first, bvs ); + TermUtil::getBoundVars( itm->first, bvs ); for( unsigned j=0; j<bvs.size(); j++ ){ Trace("var-elim-ineq-debug") << "...ineligible " << bvs[j] << " since it is contained in monomial." << std::endl; num_bounds[bvs[j]][true].clear(); @@ -1410,7 +1412,7 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo NodeBuilder<> tb(kind::OR); for( unsigned i=0; i<body.getNumChildren(); i++ ){ Node trm = body[i]; - if( TermDb::containsTerms( body[i], args ) ){ + if( TermUtil::containsTerms( body[i], args ) ){ tb << trm; }else{ body_split << trm; @@ -1791,7 +1793,7 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v Node sub; std::vector< unsigned > sub_vars; //return skolemized body - return TermDb::mkSkolemizedBody( n, nn, fvTypes, fvs, sk, sub, sub_vars ); + return TermUtil::mkSkolemizedBody( n, nn, fvTypes, fvs, sk, sub, sub_vars ); } }else{ //check if it contains a quantifier as a subterm |