diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-01 23:20:09 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-01 23:20:09 -0500 |
commit | 3f2c2c745ae2f13441c1cabd363e6539c9bdaeb9 (patch) | |
tree | b5c785e9a5e16d430f45b2a40f78e40247111233 /src/theory/sep | |
parent | 4b580ea3876055f701b13e67e0e4e78abbe47674 (diff) |
(Move-only) Split quant util (#1306)
* Initial draft of splitting quant util.
* Minor
* Document recursive term builder.
* Rename file, minor.
* Clang format
Diffstat (limited to 'src/theory/sep')
-rw-r--r-- | src/theory/sep/theory_sep.cpp | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 92ecc0393..71cde2841 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -14,20 +14,20 @@ ** Implementation of the theory of sep. **/ - #include "theory/sep/theory_sep.h" -#include "theory/valuation.h" -#include "expr/kind.h" #include <map> -#include "theory/rewriter.h" -#include "theory/theory_model.h" +#include "expr/kind.h" +#include "options/quantifiers_options.h" #include "options/sep_options.h" #include "options/smt_options.h" #include "smt/logic_exception.h" -#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/quant_epr.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "options/quantifiers_options.h" +#include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" +#include "theory/theory_model.h" +#include "theory/valuation.h" using namespace std; @@ -1089,7 +1089,9 @@ void TheorySep::initializeBounds() { for( std::map< TypeNode, TypeNode >::iterator it = d_loc_to_data_type.begin(); it != d_loc_to_data_type.end(); ++it ){ TypeNode tn = it->first; Trace("sep-bound") << "Initialize bounds for " << tn << "..." << std::endl; - QuantEPR * qepr = getLogicInfo().isQuantified() ? getQuantifiersEngine()->getQuantEPR() : NULL; + quantifiers::QuantEPR* qepr = getLogicInfo().isQuantified() + ? getQuantifiersEngine()->getQuantEPR() + : NULL; //if pto had free variable reference if( d_bound_kind[tn]==bound_herbrand ){ //include Herbrand universe of tn |