diff options
35 files changed, 128 insertions, 131 deletions
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 7a4cde04d..8f6ab76c2 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -38,23 +38,8 @@ libtheory_la_SOURCES = \ unconstrained_simplifier.cpp \ quantifiers_engine.h \ quantifiers_engine.cpp \ - instantiator_default.h \ - instantiator_default.cpp \ - rr_inst_match.h \ - rr_inst_match_impl.h \ - rr_inst_match.cpp \ - rr_trigger.h \ - rr_trigger.cpp \ - rr_candidate_generator.h \ - rr_candidate_generator.cpp \ - inst_match.h \ - inst_match.cpp \ - trigger.h \ - trigger.cpp \ model.h \ - model.cpp \ - candidate_generator.h \ - candidate_generator.cpp + model.cpp nodist_libtheory_la_SOURCES = \ rewriter_tables.h \ diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp index f5a722737..844a11c31 100644 --- a/src/theory/arrays/theory_arrays_instantiator.cpp +++ b/src/theory/arrays/theory_arrays_instantiator.cpp @@ -18,7 +18,7 @@ #include "theory/arrays/theory_arrays_instantiator.h" #include "theory/arrays/theory_arrays.h" #include "theory/quantifiers/options.h" -#include "theory/rr_candidate_generator.h" +#include "theory/rewriterules/rr_candidate_generator.h" using namespace std; using namespace CVC4; diff --git a/src/theory/datatypes/theory_datatypes_instantiator.cpp b/src/theory/datatypes/theory_datatypes_instantiator.cpp index 8ecf37fe2..23f3e8950 100644 --- a/src/theory/datatypes/theory_datatypes_instantiator.cpp +++ b/src/theory/datatypes/theory_datatypes_instantiator.cpp @@ -19,7 +19,7 @@ #include "theory/theory_engine.h" #include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" -#include "theory/rr_candidate_generator.h" +#include "theory/rewriterules/rr_candidate_generator.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am index 5172001fc..2b16c9af3 100644 --- a/src/theory/quantifiers/Makefile.am +++ b/src/theory/quantifiers/Makefile.am @@ -15,6 +15,14 @@ libquantifiers_la_SOURCES = \ theory_quantifiers_instantiator.cpp \ instantiation_engine.h \ instantiation_engine.cpp \ + trigger.h \ + trigger.cpp \ + candidate_generator.h \ + candidate_generator.cpp \ + instantiator_default.h \ + instantiator_default.cpp \ + inst_match.h \ + inst_match.cpp \ model_engine.h \ model_engine.cpp \ inst_when_mode.cpp \ diff --git a/src/theory/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index de98d709d..6a7c4c504 100644 --- a/src/theory/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -14,11 +14,11 @@ ** \brief Implementation of theory uf candidate generator class **/ -#include "theory/candidate_generator.h" +#include "theory/quantifiers/candidate_generator.h" #include "theory/theory_engine.h" #include "theory/uf/theory_uf.h" #include "theory/quantifiers/term_database.h" -#include "theory/inst_match.h" +#include "theory/quantifiers/inst_match.h" #include "theory/quantifiers_engine.h" using namespace std; diff --git a/src/theory/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h index 134b0e1b7..a6aa34a62 100644 --- a/src/theory/candidate_generator.h +++ b/src/theory/quantifiers/candidate_generator.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__CANDIDATE_GENERATOR_H -#define __CVC4__CANDIDATE_GENERATOR_H +#ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H +#define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -184,4 +184,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY_UF_INSTANTIATOR_H */ +#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */ diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index afa8dab79..8ad911452 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -80,10 +80,10 @@ public: TermDb* getTermDatabase(); /** to stream function */ void toStream( std::ostream& out ); -}; +};/* class FirstOrderModel */ -} -} -} +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -#endif +#endif /* __CVC4__FIRST_ORDER_MODEL_H */ diff --git a/src/theory/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index f7c21c555..271e04968 100644 --- a/src/theory/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -14,10 +14,10 @@ ** \brief Implementation of inst match class **/ -#include "theory/inst_match.h" +#include "theory/quantifiers/inst_match.h" #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" -#include "theory/candidate_generator.h" +#include "theory/quantifiers/candidate_generator.h" #include "theory/uf/theory_uf_instantiator.h" #include "theory/uf/equality_engine.h" #include "theory/quantifiers/options.h" diff --git a/src/theory/inst_match.h b/src/theory/quantifiers/inst_match.h index 2b402779d..fffa3bc4d 100644 --- a/src/theory/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__INST_MATCH_H -#define __CVC4__INST_MATCH_H +#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H +#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H #include "util/hash.h" @@ -26,7 +26,7 @@ #include <map> #include "context/cdlist.h" -#include "theory/candidate_generator.h" +#include "theory/quantifiers/candidate_generator.h" //#define USE_EFFICIENT_E_MATCHING @@ -391,4 +391,4 @@ typedef CVC4::theory::inst::EqualityQuery EqualityQuery; }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__INST_MATCH_H */ +#endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */ diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 13de210ab..37ee6d801 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__INSTANTIATION_ENGINE_H -#define __CVC4__INSTANTIATION_ENGINE_H +#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H +#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H #include "theory/quantifiers_engine.h" #include "theory/quantifiers/theory_quantifiers.h" @@ -69,10 +69,10 @@ public: public: /** get the corresponding counterexample literal for quantified formula node n */ Node getCounterexampleLiteralFor( Node f ) { return d_ce_lit.find( f )==d_ce_lit.end() ? Node::null() : d_ce_lit[ f ]; } -}; +};/* class InstantiationEngine */ -} -} -} +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -#endif +#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */ diff --git a/src/theory/instantiator_default.cpp b/src/theory/quantifiers/instantiator_default.cpp index cff16962a..ca29f27b6 100644 --- a/src/theory/instantiator_default.cpp +++ b/src/theory/quantifiers/instantiator_default.cpp @@ -14,7 +14,7 @@ ** \brief Implementation of instantiator_default class **/ -#include "theory/instantiator_default.h" +#include "theory/quantifiers/instantiator_default.h" #include "theory/theory_engine.h" using namespace std; diff --git a/src/theory/instantiator_default.h b/src/theory/quantifiers/instantiator_default.h index 967a0c1ca..8e0a8de73 100644 --- a/src/theory/instantiator_default.h +++ b/src/theory/quantifiers/instantiator_default.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__INSTANTIATOR_DEFAULT_H -#define __CVC4__INSTANTIATOR_DEFAULT_H +#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATOR_DEFAULT_H +#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATOR_DEFAULT_H #include <string> #include "theory/quantifiers_engine.h" @@ -45,4 +45,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__INSTANTIATOR_DEFAULT_H */ +#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATOR_DEFAULT_H */ diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 05eb8f55f..344b731e0 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__QUANTIFIERS_MODEL_BUILDER_H -#define __CVC4__QUANTIFIERS_MODEL_BUILDER_H +#ifndef __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H +#define __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H #include "theory/quantifiers_engine.h" #include "theory/model.h" @@ -82,10 +82,10 @@ public: ~Statistics(); }; Statistics d_statistics; -}; +};/* class ModelEngineBuilder */ -} -} -} +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -#endif +#endif /* __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H */ diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 1139332fe..f5d1db736 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__QUANTIFIERS_MODEL_ENGINE_H -#define __CVC4__QUANTIFIERS_MODEL_ENGINE_H +#ifndef __CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H +#define __CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H #include "theory/quantifiers_engine.h" #include "theory/quantifiers/model_builder.h" @@ -81,10 +81,10 @@ public: ~Statistics(); }; Statistics d_statistics; -}; +};/* class ModelEngine */ -} -} -} +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -#endif +#endif /* __CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H */ diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 8c8ea6a42..6ce47d114 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__RELEVANT_DOMAIN_H -#define __CVC4__RELEVANT_DOMAIN_H +#ifndef __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H +#define __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H #include "theory/quantifiers/first_order_model.h" @@ -45,10 +45,10 @@ public: void compute(); //relevant instantiation domain for each quantifier std::map< Node, std::vector< RepDomain > > d_quant_inst_domain; -}; +};/* class RelevantDomain */ -} -} -} +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -#endif +#endif /* __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */ diff --git a/src/theory/quantifiers/rep_set_iterator.h b/src/theory/quantifiers/rep_set_iterator.h index a5ec266a9..85a2f3fd2 100644 --- a/src/theory/quantifiers/rep_set_iterator.h +++ b/src/theory/quantifiers/rep_set_iterator.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__REP_SET_ITERATOR_H -#define __CVC4__REP_SET_ITERATOR_H +#ifndef __CVC4__THEORY__QUANTIFIERS__REP_SET_ITERATOR_H +#define __CVC4__THEORY__QUANTIFIERS__REP_SET_ITERATOR_H #include "theory/quantifiers_engine.h" #include "theory/quantifiers/first_order_model.h" @@ -110,11 +110,10 @@ public: int d_eval_uf_terms; int d_eval_lits; int d_eval_lits_unknown; -}; - +};/* class RepSetEvaluator */ -} -} -} +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ #endif diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 2af6992f7..8106b5715 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__QUANTIFIERS_TERM_DATABASE_H -#define __CVC4__QUANTIFIERS_TERM_DATABASE_H +#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H +#define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H #include "theory/theory.h" @@ -149,8 +149,8 @@ public: Node getFreeVariableForInstConstant( Node n ); };/* class TermDb */ -} -} -} +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -#endif +#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */ diff --git a/src/theory/quantifiers/theory_quantifiers_instantiator.h b/src/theory/quantifiers/theory_quantifiers_instantiator.h index bf17495a1..e837811b0 100644 --- a/src/theory/quantifiers/theory_quantifiers_instantiator.h +++ b/src/theory/quantifiers/theory_quantifiers_instantiator.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__INSTANTIATOR_QUANTIFIERS_H -#define __CVC4__INSTANTIATOR_QUANTIFIERS_H +#ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_INSTANTIATOR_H +#define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_INSTANTIATOR_H #include "theory/quantifiers_engine.h" @@ -51,10 +51,10 @@ private: ~Statistics(); }; Statistics d_statistics; -};/* class InstantiatiorTheoryArith */ +};/* class InstantiatiorTheoryQuantifiers */ -} -} -} +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -#endif
\ No newline at end of file +#endif /* __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_INSTANTIATOR_H */ diff --git a/src/theory/trigger.cpp b/src/theory/quantifiers/trigger.cpp index f895f6814..4bb85287e 100644 --- a/src/theory/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -14,11 +14,11 @@ ** \brief Implementation of trigger class **/ -#include "theory/trigger.h" +#include "theory/quantifiers/trigger.h" #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" #include "theory/uf/theory_uf_instantiator.h" -#include "theory/candidate_generator.h" +#include "theory/quantifiers/candidate_generator.h" #include "theory/uf/equality_engine.h" #include "theory/quantifiers/options.h" diff --git a/src/theory/trigger.h b/src/theory/quantifiers/trigger.h index 84bc7ac2e..207cef5d9 100644 --- a/src/theory/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -16,10 +16,10 @@ #include "cvc4_private.h" -#ifndef __CVC4__TRIGGER_H -#define __CVC4__TRIGGER_H +#ifndef __CVC4__THEORY__QUANTIFIERS__TRIGGER_H +#define __CVC4__THEORY__QUANTIFIERS__TRIGGER_H -#include "theory/inst_match.h" +#include "theory/quantifiers/inst_match.h" namespace CVC4 { namespace theory { @@ -165,9 +165,7 @@ inline std::ostream& operator<<(std::ostream& out, const Trigger & tr) { } }/* CVC4::theory::inst namespace */ - }/* CVC4::theory namespace */ - }/* CVC4 namespace */ -#endif /* __CVC4__TRIGGER_H */ +#endif /* __CVC4__THEORY__QUANTIFIERS__TRIGGER_H */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 4d94d8d83..df08312b1 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -27,7 +27,7 @@ #include "theory/quantifiers/instantiation_engine.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" -#include "theory/rr_candidate_generator.h" +#include "theory/rewriterules/rr_candidate_generator.h" using namespace std; using namespace CVC4; @@ -793,4 +793,4 @@ rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass(TypeNode t) { // if(eq == NULL) return getInstantiator(id)->getRRCanGenClass(); // else return eq; return getRRCanGenClass(); -}
\ No newline at end of file +} diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 2ae620e3d..5afc34bf6 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -21,8 +21,8 @@ #include "theory/theory.h" #include "util/hash.h" -#include "theory/inst_match.h" -#include "theory/rr_inst_match.h" +#include "theory/quantifiers/inst_match.h" +#include "theory/rewriterules/rr_inst_match.h" #include "util/stats.h" diff --git a/src/theory/rewriterules/Makefile.am b/src/theory/rewriterules/Makefile.am index 46cffda11..a9eddb812 100644 --- a/src/theory/rewriterules/Makefile.am +++ b/src/theory/rewriterules/Makefile.am @@ -13,7 +13,14 @@ librewriterules_la_SOURCES = \ theory_rewriterules_rewriter.h \ theory_rewriterules_type_rules.h \ theory_rewriterules_preprocess.h \ - theory_rewriterules_params.h + theory_rewriterules_params.h \ + rr_inst_match.h \ + rr_inst_match_impl.h \ + rr_inst_match.cpp \ + rr_trigger.h \ + rr_trigger.cpp \ + rr_candidate_generator.h \ + rr_candidate_generator.cpp EXTRA_DIST = \ kinds diff --git a/src/theory/rr_candidate_generator.cpp b/src/theory/rewriterules/rr_candidate_generator.cpp index a2e895c7f..f01497bda 100644 --- a/src/theory/rr_candidate_generator.cpp +++ b/src/theory/rewriterules/rr_candidate_generator.cpp @@ -14,7 +14,7 @@ ** \brief Implementation of rr candidate generator class **/ -#include "theory/rr_candidate_generator.h" +#include "theory/rewriterules/rr_candidate_generator.h" #include "theory/theory_engine.h" #include "theory/uf/theory_uf.h" #include "theory/quantifiers/term_database.h" diff --git a/src/theory/rr_candidate_generator.h b/src/theory/rewriterules/rr_candidate_generator.h index 30f6c067d..560504fba 100644 --- a/src/theory/rr_candidate_generator.h +++ b/src/theory/rewriterules/rr_candidate_generator.h @@ -16,12 +16,12 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY_UF_CANDIDATE_GENERATOR_H -#define __CVC4__THEORY_UF_CANDIDATE_GENERATOR_H +#ifndef __CVC4__THEORY__REWRITERULES__RR_CANDIDATE_GENERATOR_H +#define __CVC4__THEORY__REWRITERULES__RR_CANDIDATE_GENERATOR_H #include "theory/quantifiers_engine.h" #include "theory/quantifiers/term_database.h" -#include "theory/rr_inst_match.h" +#include "theory/rewriterules/rr_inst_match.h" using namespace CVC4::theory::quantifiers; @@ -206,4 +206,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY_UF_INSTANTIATOR_H */ +#endif /* __CVC4__THEORY__REWRITERULES__RR_CANDIDATE_GENERATOR_H */ diff --git a/src/theory/rr_inst_match.cpp b/src/theory/rewriterules/rr_inst_match.cpp index 0e3e7b9fa..25b184fe2 100644 --- a/src/theory/rr_inst_match.cpp +++ b/src/theory/rewriterules/rr_inst_match.cpp @@ -14,17 +14,17 @@ ** \brief Implementation of inst match class **/ -#include "theory/inst_match.h" +#include "theory/quantifiers/inst_match.h" #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" #include "theory/uf/theory_uf_instantiator.h" #include "theory/uf/equality_engine.h" #include "theory/arrays/theory_arrays.h" #include "theory/datatypes/theory_datatypes.h" -#include "theory/rr_inst_match.h" -#include "theory/rr_trigger.h" -#include "theory/rr_inst_match_impl.h" -#include "theory/rr_candidate_generator.h" +#include "theory/rewriterules/rr_inst_match.h" +#include "theory/rewriterules/rr_trigger.h" +#include "theory/rewriterules/rr_inst_match_impl.h" +#include "theory/rewriterules/rr_candidate_generator.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/rr_inst_match.h b/src/theory/rewriterules/rr_inst_match.h index 468fe6a89..d2a246769 100644 --- a/src/theory/rr_inst_match.h +++ b/src/theory/rewriterules/rr_inst_match.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__RR_INST_MATCH_H -#define __CVC4__RR_INST_MATCH_H +#ifndef __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_H +#define __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_H #include "theory/theory.h" #include "util/hash.h" @@ -31,7 +31,7 @@ #include "theory/uf/theory_uf.h" #include "context/cdlist.h" -#include "theory/inst_match.h" +#include "theory/quantifiers/inst_match.h" #include "expr/node_manager.h" #include "expr/node_builder.h" @@ -263,4 +263,4 @@ class InstMatchGenerator; }/* CVC4 namespace */ -#endif /* __CVC4__RR_INST_MATCH_H */ +#endif /* __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_H */ diff --git a/src/theory/rr_inst_match_impl.h b/src/theory/rewriterules/rr_inst_match_impl.h index 4bf04cb96..aa6cf81c2 100644 --- a/src/theory/rr_inst_match_impl.h +++ b/src/theory/rewriterules/rr_inst_match_impl.h @@ -16,13 +16,13 @@ #include "cvc4_private.h" -#ifndef __CVC4__RR_INST_MATCH_IMPL_H -#define __CVC4__RR_INST_MATCH_IMPL_H +#ifndef __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_IMPL_H +#define __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_IMPL_H -#include "theory/rr_inst_match.h" +#include "theory/rewriterules/rr_inst_match.h" #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" -#include "theory/rr_candidate_generator.h" +#include "theory/rewriterules/rr_candidate_generator.h" #include "theory/uf/equality_engine.h" namespace CVC4 { @@ -125,4 +125,4 @@ addInstMatch( InstMatch& m, InstMatchTrie2Gen<modEq>::Tree* e ) { }/* CVC4 namespace */ -#endif /* __CVC4__RR_INST_MATCH_IMPL_H */ +#endif /* __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_IMPL_H */ diff --git a/src/theory/rr_trigger.cpp b/src/theory/rewriterules/rr_trigger.cpp index 5d56147e8..78c0e942a 100644 --- a/src/theory/rr_trigger.cpp +++ b/src/theory/rewriterules/rr_trigger.cpp @@ -14,11 +14,11 @@ ** \brief Implementation of trigger class **/ -#include "theory/rr_trigger.h" +#include "theory/rewriterules/rr_trigger.h" #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" #include "theory/uf/theory_uf_instantiator.h" -#include "theory/rr_candidate_generator.h" +#include "theory/rewriterules/rr_candidate_generator.h" #include "theory/uf/equality_engine.h" using namespace std; diff --git a/src/theory/rr_trigger.h b/src/theory/rewriterules/rr_trigger.h index bc12666d0..096fbdb4f 100644 --- a/src/theory/rr_trigger.h +++ b/src/theory/rewriterules/rr_trigger.h @@ -16,10 +16,10 @@ #include "cvc4_private.h" -#ifndef __CVC4__RR_TRIGGER_H -#define __CVC4__RR_TRIGGER_H +#ifndef __CVC4__THEORY__REWRITERULES__RR_TRIGGER_H +#define __CVC4__THEORY__REWRITERULES__RR_TRIGGER_H -#include "theory/rr_inst_match.h" +#include "theory/rewriterules/rr_inst_match.h" namespace CVC4 { namespace theory { @@ -173,4 +173,4 @@ inline std::ostream& operator<<(std::ostream& out, const Trigger & tr) { }/* CVC4 namespace */ -#endif /* __CVC4__RR_TRIGGER_H */ +#endif /* __CVC4__THEORY__REWRITERULES__RR_TRIGGER_H */ diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h index fcbdfe8b9..bb5537474 100644 --- a/src/theory/rewriterules/theory_rewriterules.h +++ b/src/theory/rewriterules/theory_rewriterules.h @@ -27,9 +27,9 @@ #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" #include "context/context_mm.h" -#include "theory/rr_inst_match_impl.h" -#include "theory/rr_trigger.h" -#include "theory/rr_inst_match.h" +#include "theory/rewriterules/rr_inst_match_impl.h" +#include "theory/rewriterules/rr_trigger.h" +#include "theory/rewriterules/rr_inst_match.h" #include "util/stats.h" #include "theory/rewriterules/theory_rewriterules_preprocess.h" #include "theory/model.h" diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 1301da653..77daa5f53 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -19,7 +19,7 @@ #include "theory/theory.h" #include "util/Assert.h" #include "theory/quantifiers_engine.h" -#include "theory/instantiator_default.h" +#include "theory/quantifiers/instantiator_default.h" #include <vector> diff --git a/src/theory/uf/inst_strategy.h b/src/theory/uf/inst_strategy.h index a0091c4b4..663720326 100644 --- a/src/theory/uf/inst_strategy.h +++ b/src/theory/uf/inst_strategy.h @@ -20,7 +20,7 @@ #define __CVC4__INST_STRATEGY_H #include "theory/quantifiers_engine.h" -#include "theory/trigger.h" +#include "theory/quantifiers/trigger.h" #include "context/context.h" #include "context/context_mm.h" diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp index ea253cbdb..90e45775b 100644 --- a/src/theory/uf/theory_uf_instantiator.cpp +++ b/src/theory/uf/theory_uf_instantiator.cpp @@ -17,7 +17,7 @@ #include "theory/uf/theory_uf_instantiator.h" #include "theory/theory_engine.h" #include "theory/uf/theory_uf.h" -#include "theory/rr_candidate_generator.h" +#include "theory/rewriterules/rr_candidate_generator.h" #include "theory/uf/equality_engine.h" #include "theory/quantifiers/options.h" #include "theory/rewriterules/options.h" diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h index d15c0103b..59b8f36a4 100644 --- a/src/theory/uf/theory_uf_instantiator.h +++ b/src/theory/uf/theory_uf_instantiator.h @@ -27,7 +27,7 @@ #include "util/stats.h" #include "theory/uf/theory_uf.h" -#include "theory/trigger.h" +#include "theory/quantifiers/trigger.h" #include "util/ntuple.h" #include "context/cdqueue.h" |