diff options
Diffstat (limited to 'src/theory/quantifiers')
37 files changed, 150 insertions, 1186 deletions
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index f047276b0..b18676cbc 100644 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -13,9 +13,9 @@ **/ +#include "options/quantifiers_options.h" #include "theory/quantifiers/ambqi_builder.h" #include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/options.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 2fd595a9f..ceab8394f 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -14,12 +14,12 @@ ** This class manages integer bounds for quantifiers **/ +#include "options/quantifiers_options.h" #include "theory/quantifiers/bounded_integers.h" -#include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/options.h" using namespace CVC4; using namespace std; @@ -425,4 +425,3 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node bool BoundedIntegers::isGroundRange(Node f, Node v) { return isBoundVar(f,v) && !getLowerBound(f,v).hasBoundVar() && !getUpperBound(f,v).hasBoundVar(); } - diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index b67c4bd56..0cdb22be4 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -12,13 +12,13 @@ ** \brief Implementation of theory uf candidate generator class **/ +#include "options/quantifiers_options.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/quantifiers/inst_match.h" +#include "theory/quantifiers/term_database.h" #include "theory/quantifiers_engine.h" -#include "theory/quantifiers/options.h" +#include "theory/theory_engine.h" +#include "theory/uf/theory_uf.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 398ae1ffe..81fe00674 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -12,14 +12,14 @@ ** \brief counterexample guided instantiation class ** **/ - #include "theory/quantifiers/ce_guided_instantiation.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/first_order_model.h" + +#include "expr/datatype.h" +#include "options/quantifiers_options.h" #include "theory/datatypes/datatypes_rewriter.h" -#include "util/datatype.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/term_database.h" +#include "theory/theory_engine.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 6fcfdbc58..8274561ca 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -17,11 +17,11 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H -#include "context/cdhashmap.h" #include "context/cdchunk_list.h" -#include "theory/quantifiers_engine.h" +#include "context/cdhashmap.h" +#include "options/quantifiers_modes.h" #include "theory/quantifiers/ce_guided_single_inv.h" -#include "theory/quantifiers/modes.h" +#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index f533a2bbb..7ef23077f 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -12,18 +12,18 @@ ** \brief utility for processing single invocation synthesis conjectures ** **/ - #include "theory/quantifiers/ce_guided_single_inv.h" + +#include "expr/datatype.h" +#include "options/quantifiers_options.h" +#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/ce_guided_single_inv_ei.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/datatypes/datatypes_rewriter.h" -#include "util/datatype.h" #include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" +#include "theory/theory_engine.h" using namespace CVC4; using namespace CVC4::kind; @@ -1186,4 +1186,4 @@ void SingleInvocationPartition::debugPrint( const char * c ) { Trace(c) << std::endl; } -}
\ No newline at end of file +} diff --git a/src/theory/quantifiers/ce_guided_single_inv_ei.cpp b/src/theory/quantifiers/ce_guided_single_inv_ei.cpp index 18252e190..f45285851 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_ei.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_ei.cpp @@ -13,12 +13,12 @@ ** **/ -#include "theory/quantifiers/ce_guided_single_inv_ei.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/ce_guided_instantiation.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/ce_guided_single_inv_ei.h" #include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/term_database.h" +#include "theory/theory_engine.h" using namespace CVC4; using namespace CVC4::kind; @@ -44,4 +44,4 @@ bool CegEntailmentInfer::getEntailedConjecture( Node& conj, Node& exp ) { return false; } -}
\ No newline at end of file +} diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp index 8fd935368..6ba5bed02 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp @@ -12,18 +12,18 @@ ** \brief utility for processing single invocation synthesis conjectures ** **/ - #include "theory/quantifiers/ce_guided_single_inv_sol.h" -#include "theory/quantifiers/ce_guided_single_inv.h" + +#include "expr/datatype.h" +#include "options/quantifiers_options.h" +#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/ce_guided_instantiation.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/ce_guided_single_inv.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/datatypes/datatypes_rewriter.h" -#include "util/datatype.h" #include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" +#include "theory/theory_engine.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 7c10da90c..cea90621d 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -11,16 +11,16 @@ ** ** \brief Implementation of counterexample-guided quantifier instantiation **/ - #include "theory/quantifiers/ceg_instantiator.h" -#include "theory/arith/theory_arith.h" + +#include "options/quantifiers_options.h" +#include "smt_util/ite_removal.h" #include "theory/arith/partial_model.h" +#include "theory/arith/theory_arith.h" #include "theory/arith/theory_arith_private.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/first_order_model.h" -#include "util/ite_removal.h" +#include "theory/quantifiers/term_database.h" +#include "theory/theory_engine.h" //#define MBP_STRICT_ASSERTIONS diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 9504bd407..5b3c5263f 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -18,8 +18,8 @@ #ifndef __CVC4__CEG_INSTANTIATOR_H #define __CVC4__CEG_INSTANTIATOR_H +#include "expr/statistics_registry.h" #include "theory/quantifiers_engine.h" -#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 1cdad589b..8e083ae1e 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -13,12 +13,12 @@ ** **/ +#include "options/quantifiers_options.h" #include "theory/quantifiers/conjecture_generator.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" -#include "theory/quantifiers/first_order_model.h" +#include "theory/theory_engine.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 36d055b69..095e7868e 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -12,13 +12,13 @@ ** \brief Implementation of model engine model class **/ +#include "options/quantifiers_options.h" +#include "theory/quantifiers/ambqi_builder.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/full_model_check.h" #include "theory/quantifiers/model_engine.h" -#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/full_model_check.h" -#include "theory/quantifiers/ambqi_builder.h" -#include "theory/quantifiers/options.h" +#include "theory/quantifiers/term_database.h" #define USE_INDEX_ORDERING diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index c3a723fce..02c6bbba8 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -12,9 +12,9 @@ ** \brief Implementation of full model check class **/ -#include "theory/quantifiers/full_model_check.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/options.h" +#include "theory/quantifiers/full_model_check.h" #include "theory/quantifiers/term_database.h" using namespace std; diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index f4e8861dc..89c2d4868 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -11,15 +11,15 @@ ** ** [[ Add lengthier description here ]] ** \todo document this file -**/ - + **/ #include "theory/quantifiers/inst_match_generator.h" -#include "theory/quantifiers/trigger.h" -#include "theory/quantifiers/term_database.h" + +#include "expr/datatype.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/candidate_generator.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/trigger.h" #include "theory/quantifiers_engine.h" -#include "theory/quantifiers/options.h" -#include "util/datatype.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index eff1c0d9b..a4632398d 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -11,17 +11,17 @@ ** ** \brief Implementation of counterexample-guided quantifier instantiation strategies **/ - #include "theory/quantifiers/inst_strategy_cbqi.h" -#include "theory/arith/theory_arith.h" + +#include "options/quantifiers_options.h" +#include "smt_util/ite_removal.h" #include "theory/arith/partial_model.h" +#include "theory/arith/theory_arith.h" #include "theory/arith/theory_arith_private.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" -#include "util/ite_removal.h" +#include "theory/theory_engine.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index d14b85111..b8bc25c6a 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -18,11 +18,10 @@ #ifndef __CVC4__INST_STRATEGY_CBQI_H #define __CVC4__INST_STRATEGY_CBQI_H -#include "theory/quantifiers/instantiation_engine.h" +#include "expr/statistics_registry.h" #include "theory/arith/arithvar.h" #include "theory/quantifiers/ceg_instantiator.h" - -#include "util/statistics_registry.h" +#include "theory/quantifiers/instantiation_engine.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 9237d95c2..299eb51fd 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -14,11 +14,11 @@ #include "theory/quantifiers/inst_strategy_e_matching.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/inst_match_generator.h" #include "theory/quantifiers/relevant_domain.h" +#include "theory/quantifiers/term_database.h" +#include "theory/theory_engine.h" using namespace std; using namespace CVC4; @@ -652,4 +652,3 @@ bool FullSaturation::process( Node f, bool fullEffort ){ void FullSaturation::registerQuantifier( Node q ) { } - diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index 2f7e7dcf1..a19bcca76 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -17,14 +17,12 @@ #ifndef __CVC4__INST_STRATEGY_E_MATCHING_H #define __CVC4__INST_STRATEGY_E_MATCHING_H -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/trigger.h" - #include "context/context.h" #include "context/context_mm.h" - -#include "util/statistics_registry.h" +#include "expr/statistics_registry.h" #include "theory/quantifiers/instantiation_engine.h" +#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 16cecb657..88a67e3c8 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -14,12 +14,12 @@ #include "theory/quantifiers/instantiation_engine.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/inst_strategy_e_matching.h" +#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" +#include "theory/theory_engine.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 163005806..a5e3dada8 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -14,16 +14,17 @@ ** This class implements quantifiers macro definitions. **/ +#include "theory/quantifiers/macros.h" + #include <vector> -#include "theory/quantifiers/macros.h" -#include "theory/rewriter.h" +#include "options/quantifiers_modes.h" +#include "options/quantifiers_options.h" #include "proof/proof_manager.h" #include "smt/smt_engine_scope.h" -#include "theory/quantifiers/modes.h" -#include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" +#include "theory/rewriter.h" using namespace CVC4; using namespace std; @@ -485,4 +486,4 @@ void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) { } } } -}
\ No newline at end of file +} diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 79b995ef0..dc18548a5 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -12,18 +12,19 @@ ** \brief Implementation of model builder class **/ +#include "theory/quantifiers/model_builder.h" + +#include "options/quantifiers_options.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/trigger.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" #include "theory/uf/theory_uf_model.h" #include "theory/uf/theory_uf_strong_solver.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/model_builder.h" -#include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/trigger.h" -#include "theory/quantifiers/options.h" using namespace std; using namespace CVC4; @@ -745,5 +746,3 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ Debug("fmf-model-cons") << " Finished constructing model for " << op << "." << std::endl; } } - - diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index f5a063eb8..6a21a50e5 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -13,16 +13,17 @@ **/ #include "theory/quantifiers/model_engine.h" + +#include "options/quantifiers_options.h" +#include "theory/quantifiers/ambqi_builder.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/full_model_check.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/term_database.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" #include "theory/uf/theory_uf_strong_solver.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/full_model_check.h" -#include "theory/quantifiers/ambqi_builder.h" using namespace std; using namespace CVC4; @@ -335,5 +336,3 @@ ModelEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_exh_inst_lemmas); StatisticsRegistry::unregisterStat(&d_mbqi_inst_lemmas); } - - diff --git a/src/theory/quantifiers/modes.cpp b/src/theory/quantifiers/modes.cpp deleted file mode 100644 index 253f23561..000000000 --- a/src/theory/quantifiers/modes.cpp +++ /dev/null @@ -1,86 +0,0 @@ -/********************* */ -/*! \file modes.cpp - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include <iostream> -#include "theory/quantifiers/modes.h" - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mode) { - switch(mode) { - case theory::quantifiers::INST_WHEN_PRE_FULL: - out << "INST_WHEN_PRE_FULL"; - break; - case theory::quantifiers::INST_WHEN_FULL: - out << "INST_WHEN_FULL"; - break; - case theory::quantifiers::INST_WHEN_FULL_LAST_CALL: - out << "INST_WHEN_FULL_LAST_CALL"; - break; - case theory::quantifiers::INST_WHEN_LAST_CALL: - out << "INST_WHEN_LAST_CALL"; - break; - default: - out << "InstWhenMode!UNKNOWN"; - } - - return out; -} - -std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMode mode) { - switch(mode) { - case theory::quantifiers::LITERAL_MATCH_NONE: - out << "LITERAL_MATCH_NONE"; - break; - case theory::quantifiers::LITERAL_MATCH_PREDICATE: - out << "LITERAL_MATCH_PREDICATE"; - break; - case theory::quantifiers::LITERAL_MATCH_EQUALITY: - out << "LITERAL_MATCH_EQUALITY"; - break; - default: - out << "LiteralMatchMode!UNKNOWN"; - } - - return out; -} - -std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) { - switch(mode) { - case theory::quantifiers::MBQI_GEN_EVAL: - out << "MBQI_GEN_EVAL"; - break; - case theory::quantifiers::MBQI_NONE: - out << "MBQI_NONE"; - break; - case theory::quantifiers::MBQI_FMC: - out << "MBQI_FMC"; - break; - case theory::quantifiers::MBQI_ABS: - out << "MBQI_ABS"; - break; - case theory::quantifiers::MBQI_TRUST: - out << "MBQI_TRUST"; - break; - default: - out << "MbqiMode!UNKNOWN"; - } - return out; -} - -}/* CVC4 namespace */ - diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h deleted file mode 100644 index 01d3f0c22..000000000 --- a/src/theory/quantifiers/modes.h +++ /dev/null @@ -1,173 +0,0 @@ -/********************* */ -/*! \file modes.h - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__THEORY__QUANTIFIERS__MODES_H -#define __CVC4__THEORY__QUANTIFIERS__MODES_H - -#include <iostream> - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -typedef enum { - /** Apply instantiation round before full effort (possibly at standard effort) */ - INST_WHEN_PRE_FULL, - /** Apply instantiation round at full effort or above */ - INST_WHEN_FULL, - /** Apply instantiation round at full effort, after all other theories finish, or above */ - INST_WHEN_FULL_DELAY, - /** Apply instantiation round at full effort half the time, and last call always */ - INST_WHEN_FULL_LAST_CALL, - /** Apply instantiation round at full effort after all other theories finish half the time, and last call always */ - INST_WHEN_FULL_DELAY_LAST_CALL, - /** Apply instantiation round at last call only */ - INST_WHEN_LAST_CALL, -} InstWhenMode; - -typedef enum { - /** Do not consider polarity of patterns */ - LITERAL_MATCH_NONE, - /** Consider polarity of boolean predicates only */ - LITERAL_MATCH_PREDICATE, - /** Consider polarity of boolean predicates, as well as equalities */ - LITERAL_MATCH_EQUALITY, -} LiteralMatchMode; - -typedef enum { - /** mbqi from CADE 24 paper */ - MBQI_GEN_EVAL, - /** no mbqi */ - MBQI_NONE, - /** default, mbqi from Section 5.4.2 of AJR thesis */ - MBQI_FMC, - /** mbqi with integer intervals */ - MBQI_FMC_INTERVAL, - /** abstract mbqi algorithm */ - MBQI_ABS, - /** mbqi trust (produce no instantiations) */ - MBQI_TRUST, -} MbqiMode; - -typedef enum { - /** default, apply at full effort */ - QCF_WHEN_MODE_DEFAULT, - /** apply at last call */ - QCF_WHEN_MODE_LAST_CALL, - /** apply at standard effort */ - QCF_WHEN_MODE_STD, - /** apply based on heuristics */ - QCF_WHEN_MODE_STD_H, -} QcfWhenMode; - -typedef enum { - /** default, use qcf for conflicts only */ - QCF_CONFLICT_ONLY, - /** use qcf for conflicts and propagations */ - QCF_PROP_EQ, - /** use qcf for conflicts, propagations and heuristic instantiations */ - QCF_PARTIAL, - /** use qcf for model checking */ - QCF_MC, -} QcfMode; - -typedef enum { - /** use but do not trust */ - USER_PAT_MODE_USE, - /** default, if patterns are supplied for a quantifier, use only those */ - USER_PAT_MODE_TRUST, - /** resort to user patterns only when necessary */ - USER_PAT_MODE_RESORT, - /** ignore user patterns */ - USER_PAT_MODE_IGNORE, - /** interleave use/resort for user patterns */ - USER_PAT_MODE_INTERLEAVE, -} UserPatMode; - -typedef enum { - /** default for trigger selection */ - TRIGGER_SEL_DEFAULT, - /** only consider minimal terms for triggers */ - TRIGGER_SEL_MIN, - /** only consider maximal terms for triggers */ - TRIGGER_SEL_MAX, -} TriggerSelMode; - -typedef enum CVC4_PUBLIC { - /** default : prenex quantifiers without user patterns */ - PRENEX_NO_USER_PAT, - /** prenex all */ - PRENEX_ALL, - /** prenex none */ - PRENEX_NONE, -} PrenexQuantMode; - -typedef enum { - /** enforce fairness by UF corresponding to datatypes size */ - CEGQI_FAIR_UF_DT_SIZE, - /** enforce fairness by datatypes size */ - CEGQI_FAIR_DT_SIZE, - /** enforce fairness by datatypes height bound */ - CEGQI_FAIR_DT_HEIGHT_PRED, - /** do not use fair strategy for CEGQI */ - CEGQI_FAIR_NONE, -} CegqiFairMode; - -typedef enum { - /** consider all terms in master equality engine */ - TERM_DB_ALL, - /** consider only relevant terms */ - TERM_DB_RELEVANT, -} TermDbMode; - -typedef enum { - /** do not lift ITEs in quantified formulas */ - ITE_LIFT_QUANT_MODE_NONE, - /** only lift ITEs in quantified formulas if reduces the term size */ - ITE_LIFT_QUANT_MODE_SIMPLE, - /** lift ITEs */ - ITE_LIFT_QUANT_MODE_ALL, -} IteLiftQuantMode; - -typedef enum { - /** synthesize I( x ) */ - SYGUS_INV_TEMPL_MODE_NONE, - /** synthesize ( pre( x ) V I( x ) ) */ - SYGUS_INV_TEMPL_MODE_PRE, - /** synthesize ( post( x ) ^ I( x ) ) */ - SYGUS_INV_TEMPL_MODE_POST, -} SygusInvTemplMode; - -typedef enum { - /** infer all definitions */ - MACROS_QUANT_MODE_ALL, - /** infer ground definitions */ - MACROS_QUANT_MODE_GROUND, - /** infer ground uf definitions */ - MACROS_QUANT_MODE_GROUND_UF, -} MacrosQuantMode; - -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ - -std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mode) CVC4_PUBLIC; - -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__QUANTIFIERS__MODES_H */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options deleted file mode 100644 index 065da0d5a..000000000 --- a/src/theory/quantifiers/options +++ /dev/null @@ -1,297 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module QUANTIFIERS "theory/quantifiers/options.h" Quantifiers - -#### rewriter options - -# Whether to mini-scope quantifiers. -# For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to -# ( forall x. P( x ) ) ^ ( forall x. Q( x ) ) -option miniscopeQuant --miniscope-quant bool :default true :read-write - miniscope quantifiers -# Whether to mini-scope quantifiers based on formulas with no free variables. -# For example, forall x. ( P( x ) V Q ) will be rewritten to -# ( forall x. P( x ) ) V Q -option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write - miniscope quantifiers for ground subformulas -option quantSplit --quant-split bool :default true - apply splitting to quantified formulas based on variable disjoint disjuncts -option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToPrenexQuantMode :handler-include "theory/quantifiers/options_handlers.h" - prenex mode for quantified formulas -# Whether to variable-eliminate quantifiers. -# For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to -# forall y. P( c, y ) -option varElimQuant --var-elim-quant bool :default true - enable simple variable elimination for quantified formulas -option dtVarExpandQuant --dt-var-exp-quant bool :default true - expand datatype variables bound to one constructor in quantifiers -#ite lift mode for quantified formulas -option iteLiftQuant --ite-lift-quant=MODE CVC4::theory::quantifiers::IteLiftQuantMode :default CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToIteLiftQuantMode :handler-include "theory/quantifiers/options_handlers.h" - ite lifting mode for quantified formulas -option condVarSplitQuant --cond-var-split-quant bool :default true - split quantified formulas that lead to variable eliminations -option condVarSplitQuantAgg --cond-var-split-agg-quant bool :default false - aggressive split quantified formulas that lead to variable eliminations -option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default false - split ites with dt testers as conditions -# Whether to CNF quantifier bodies -# option cnfQuant --cnf-quant bool :default false -# apply CNF conversion to quantified formulas -option nnfQuant --nnf-quant bool :default true - apply NNF conversion to quantified formulas -# Whether to pre-skolemize quantifier bodies. -# For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to -# forall x. P( x ) => f( S( x ) ) = x -option preSkolemQuant --pre-skolem-quant bool :read-write :default false - apply skolemization eagerly to bodies of quantified formulas -option preSkolemQuantNested --pre-skolem-quant-nested bool :read-write :default true - apply skolemization to nested quantified formulass -option preSkolemQuantAgg --pre-skolem-quant-agg bool :read-write :default true - apply skolemization to quantified formulas aggressively -option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false - perform aggressive miniscoping for quantifiers -option elimTautQuant --elim-taut-quant bool :default true - eliminate tautological disjuncts of quantified formulas -option purifyQuant --purify-quant bool :default false - purify quantified formulas - -#### E-matching options - -option eMatching --e-matching bool :read-write :default true - whether to do heuristic E-matching - -option termDbMode --term-db-mode CVC4::theory::quantifiers::TermDbMode :default CVC4::theory::quantifiers::TERM_DB_ALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToTermDbMode :handler-include "theory/quantifiers/options_handlers.h" - which ground terms to consider for instantiation -option registerQuantBodyTerms --register-quant-body-terms bool :default false - consider ground terms within bodies of quantified formulas for matching - -option smartTriggers --smart-triggers bool :default true - enable smart triggers -option relevantTriggers --relevant-triggers bool :default false - prefer triggers that are more relevant based on SInE style analysis -option relationalTriggers --relational-triggers bool :default false - choose relational triggers such as x = f(y), x >= f(y) -option purifyTriggers --purify-triggers bool :default false :read-write - purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1 -option purifyDtTriggers --purify-dt-triggers bool :default false :read-write - purify dt triggers, match all constructors of correct form instead of selectors -option pureThTriggers --pure-th-triggers bool :default false :read-write - use pure theory terms as single triggers -option partialTriggers --partial-triggers bool :default false :read-write - use triggers that do not contain all free variables -option multiTriggerWhenSingle --multi-trigger-when-single bool :default false - select multi triggers when single triggers exist -option multiTriggerPriority --multi-trigger-priority bool :default false - only try multi triggers if single triggers give no instantiations -option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToTriggerSelMode :handler-include "theory/quantifiers/options_handlers.h" - selection mode for triggers -option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToUserPatMode :handler-include "theory/quantifiers/options_handlers.h" - policy for handling user-provided patterns for quantifier instantiation -option incrementTriggers --increment-triggers bool :default true - generate additional triggers as needed during search - -option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" - when to apply instantiation - -option instMaxLevel --inst-max-level=N int :read-write :default -1 - maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) -option instLevelInputOnly --inst-level-input-only bool :default true - only input terms are assigned instantiation level zero -option internalReps --quant-internal-reps bool :default true - instantiate with representatives chosen by quantifiers engine - -option eagerInstQuant --eager-inst-quant bool :default false - apply quantifier instantiation eagerly - -option fullSaturateQuant --full-saturate-quant bool :default false :read-write - when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown -option fullSaturateQuantRd --full-saturate-quant-rd bool :default true - whether to use relevant domain first for full saturation instantiation strategy -option fullSaturateInst --fs-inst bool :default false - interleave full saturate instantiation with other techniques - -option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h" - choose literal matching mode - -### finite model finding options - -option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write - use finite model finding heuristic for quantifier instantiation - -option quantFunWellDefined --quant-fun-wd bool :default false - assume that function defined by quantifiers are well defined -option fmfFunWellDefined --fmf-fun bool :default false :read-write - find models for recursively defined functions, assumes functions are admissible -option fmfFunWellDefinedRelevant --fmf-fun-rlv bool :default false - find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant -option fmfEmptySorts --fmf-empty-sorts bool :default false - allow finite model finding to assume sorts that do not occur in ground assertions are empty - -option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h" - choose mode for model-based quantifier instantiation -option fmfOneInstPerRound --mbqi-one-inst-per-round bool :read-write :default false - only add one instantiation per quantifier per round for mbqi -option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false - only add instantiations for one quantifier per round for mbqi - -option fmfInstEngine --fmf-inst-engine bool :default false - use instantiation engine in conjunction with finite model finding -option fmfInstGen --fmf-inst-gen bool :default true - enable Inst-Gen instantiation techniques for finite model finding -option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false - only perform Inst-Gen instantiation techniques on one quantifier per round -option fmfFreshDistConst --fmf-fresh-dc bool :default false - use fresh distinguished representative when applying Inst-Gen techniques -option fmfFmcSimple --fmf-fmc-simple bool :default true - simple models in full model check for finite model finding -option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write - finite model finding on bounded integer quantification -option fmfBoundIntLazy --fmf-bound-int-lazy bool :default false :read-write - enforce bounds for bounded integer quantification lazily via use of proxy variables - -### conflict-based instantiation options - -option quantConflictFind --quant-cf bool :read-write :default true - enable conflict find mechanism for quantifiers -option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default CVC4::theory::quantifiers::QCF_PROP_EQ :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfMode :handler-include "theory/quantifiers/options_handlers.h" - what effort to apply conflict find mechanism -option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfWhenMode :handler-include "theory/quantifiers/options_handlers.h" - when to invoke conflict find mechanism for quantifiers -option qcfTConstraint --qcf-tconstraint bool :read-write :default false - enable entailment checks for t-constraints in qcf algorithm -option qcfAllConflict --qcf-all-conflict bool :read-write :default false - add all available conflicting instances during conflict-based instantiation - -option instNoEntail --inst-no-entail bool :read-write :default true - do not consider instances of quantified formulas that are currently entailed - -### rewrite rules options - -option quantRewriteRules --rewrite-rules bool :default false - use rewrite rules module -option rrOneInstPerRound --rr-one-inst-per-round bool :default false - add one instance of rewrite rule per round - -### induction options - -option quantInduction --quant-ind bool :default false - use all available techniques for inductive reasoning -option dtStcInduction --dt-stc-ind bool :read-write :default false - apply strengthening for existential quantification over datatypes based on structural induction -option intWfInduction --int-wf-ind bool :read-write :default false - apply strengthening for integers based on well-founded induction -option conjectureGen --conjecture-gen bool :read-write :default false - generate candidate conjectures for inductive proofs - -option conjectureGenPerRound --conjecture-gen-per-round=N int :default 1 - number of conjectures to generate per instantiation round -option conjectureNoFilter --conjecture-no-filter bool :default false - do not filter conjectures -option conjectureFilterActiveTerms --conjecture-filter-active-terms bool :read-write :default true - filter based on active terms -option conjectureFilterCanonical --conjecture-filter-canonical bool :read-write :default true - filter based on canonicity -option conjectureFilterModel --conjecture-filter-model bool :read-write :default true - filter based on model -option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 50 - number of ground terms to generate for model filtering -option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false - more aggressive merging for universal equality engine, introduces terms - -### synthesis options - -option ceGuidedInst --cegqi bool :default false :read-write - counterexample-guided quantifier instantiation -option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h" - if and how to apply fairness for cegqi -option cegqiSingleInv --cegqi-si bool :default false :read-write - process single invocation synthesis conjectures -option cegqiSingleInvPartial --cegqi-si-partial bool :default false - combined techniques for synthesis conjectures that are partially single invocation -option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true - reconstruct solutions for single invocation conjectures in original grammar -option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true - include constants when reconstruct solutions for single invocation conjectures in original grammar -option cegqiSingleInvAbort --cegqi-si-abort bool :default false - abort if synthesis conjecture is not single invocation -option cegqiSingleInvMultiInstAbort --cegqi-si-multi-inst-abort bool :default false - abort if synthesis conjecture is single invocation with no ITE in grammar and multiple instantiations are tried - -option sygusNormalForm --sygus-nf bool :default true - only search for sygus builtin terms that are in normal form -option sygusNormalFormArg --sygus-nf-arg bool :default true - account for relationship between arguments of operations in sygus normal form -option sygusNormalFormGlobal --sygus-nf-sym bool :default true - narrow sygus search space based on global state of current candidate program -option sygusNormalFormGlobalGen --sygus-nf-sym-gen bool :default true - generalize lemmas for global search space narrowing -option sygusNormalFormGlobalArg --sygus-nf-sym-arg bool :default true - generalize based on arguments in global search space narrowing -option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true - generalize based on content in global search space narrowing - -option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToSygusInvTemplMode :handler-include "theory/quantifiers/options_handlers.h" - template mode for sygus invariant synthesis - -# approach applied to general quantified formulas -option cbqiSplx --cbqi-splx bool :read-write :default false - turns on old implementation of counterexample-based quantifier instantiation -option cbqi --cbqi bool :read-write :default false - turns on counterexample-based quantifier instantiation -option recurseCbqi --cbqi-recurse bool :default true - turns on recursive counterexample-based quantifier instantiation -option cbqiSat --cbqi-sat bool :read-write :default true - answer sat when quantifiers are asserted with counterexample-based quantifier instantiation -option cbqiModel --cbqi-model bool :read-write :default true - guide instantiations by model values for counterexample-based quantifier instantiation -option cbqiAll --cbqi-all bool :read-write :default false - apply counterexample-based instantiation to all quantified formulas -option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false - use integer infinity for vts in counterexample-based quantifier instantiation -option cbqiUseInfReal --cbqi-use-inf-real bool :read-write :default false - use real infinity for vts in counterexample-based quantifier instantiation -option cbqiPreRegInst --cbqi-prereg-inst bool :read-write :default false - preregister ground instantiations in counterexample-based quantifier instantiation -option cbqiMinBounds --cbqi-min-bounds bool :default false - use minimally constrained lower/upper bound for counterexample-based quantifier instantiation -option cbqiSymLia --cbqi-sym-lia bool :default false - use symbolic integer division in substitutions for counterexample-based quantifier instantiation -option cbqiRoundUpLowerLia --cbqi-round-up-lia bool :default false - round up integer lower bounds in substitutions for counterexample-based quantifier instantiation -option cbqiMidpoint --cbqi-midpoint bool :default false - choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation -option cbqiNopt --cbqi-nopt bool :default true - non-optimal bounds for counterexample-based quantifier instantiation - -### local theory extensions options - -option localTheoryExt --local-t-ext bool :default false - do instantiation based on local theory extensions -option ltePartialInst --lte-partial-inst bool :default false - partially instantiate local theory quantifiers -option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false - treat arguments of inst closure as restricted terms for instantiation - -### reduction options - -option quantAlphaEquiv --quant-alpha-equiv bool :default true - infer alpha equivalence between quantified formulas -option macrosQuant --macros-quant bool :read-write :default false - perform quantifiers macro expansion -option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMacrosQuantMode :handler-include "theory/quantifiers/options_handlers.h" - mode for quantifiers macro expansion - -### recursive function options - -#option funDefs --fun-defs bool :default false -# enable specialized techniques for recursive function definitions - -### e-unification options - -option quantEqualityEngine --quant-ee bool :default false - maintain congrunce closure over universal equalities - -endmodule diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h deleted file mode 100644 index 02a1a6cf2..000000000 --- a/src/theory/quantifiers/options_handlers.h +++ /dev/null @@ -1,480 +0,0 @@ -/********************* */ -/*! \file options_handlers.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Andrew Reynolds - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H -#define __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H - -#include <string> - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -static const std::string instWhenHelp = "\ -Modes currently supported by the --inst-when option:\n\ -\n\ -full-last-call (default)\n\ -+ Alternate running instantiation rounds at full effort and last\n\ - call. In other words, interleave instantiation and theory combination.\n\ -\n\ -full\n\ -+ Run instantiation round at full effort, before theory combination.\n\ -\n\ -full-delay \n\ -+ Run instantiation round at full effort, before theory combination, after\n\ - all other theories have finished.\n\ -\n\ -full-delay-last-call \n\ -+ Alternate running instantiation rounds at full effort after all other\n\ - theories have finished, and last call. \n\ -\n\ -last-call\n\ -+ Run instantiation at last call effort, after theory combination and\n\ - and theories report sat.\n\ -\n\ -"; - -static const std::string literalMatchHelp = "\ -Literal match modes currently supported by the --literal-match option:\n\ -\n\ -none (default)\n\ -+ Do not use literal matching.\n\ -\n\ -predicate\n\ -+ Consider the phase requirements of predicate literals when applying heuristic\n\ - quantifier instantiation. For example, the trigger P( x ) in the quantified \n\ - formula forall( x ). ( P( x ) V ~Q( x ) ) will only be matched with ground\n\ - terms P( t ) where P( t ) is in the equivalence class of false, and likewise\n\ - Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\ -\n\ -"; -static const std::string mbqiModeHelp = "\ -Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\ -\n\ -default \n\ -+ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\ - Modulo Theories.\n\ -\n\ -none \n\ -+ Disable model-based quantifier instantiation.\n\ -\n\ -gen-ev \n\ -+ Use model-based quantifier instantiation algorithm from CADE 24 finite\n\ - model finding paper based on generalizing evaluations.\n\ -\n\ -fmc-interval \n\ -+ Same as default, but with intervals for models of integer functions.\n\ -\n\ -abs \n\ -+ Use abstract MBQI algorithm (uses disjoint sets). \n\ -\n\ -"; -static const std::string qcfWhenModeHelp = "\ -Quantifier conflict find modes currently supported by the --quant-cf-when option:\n\ -\n\ -default \n\ -+ Default, apply conflict finding at full effort.\n\ -\n\ -last-call \n\ -+ Apply conflict finding at last call, after theory combination and \n\ - and all theories report sat. \n\ -\n\ -std \n\ -+ Apply conflict finding at standard effort.\n\ -\n\ -std-h \n\ -+ Apply conflict finding at standard effort when heuristic says to. \n\ -\n\ -"; -static const std::string qcfModeHelp = "\ -Quantifier conflict find modes currently supported by the --quant-cf option:\n\ -\n\ -prop-eq \n\ -+ Default, apply QCF algorithm to propagate equalities as well as conflicts. \n\ -\n\ -conflict \n\ -+ Apply QCF algorithm to find conflicts only.\n\ -\n\ -partial \n\ -+ Apply QCF algorithm to instantiate heuristically as well. \n\ -\n\ -mc \n\ -+ Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\ -\n\ -"; -static const std::string userPatModeHelp = "\ -User pattern modes currently supported by the --user-pat option:\n\ -\n\ -trust \n\ -+ When provided, use only user-provided patterns for a quantified formula.\n\ -\n\ -use \n\ -+ Use both user-provided and auto-generated patterns when patterns\n\ - are provided for a quantified formula.\n\ -\n\ -resort \n\ -+ Use user-provided patterns only after auto-generated patterns saturate.\n\ -\n\ -ignore \n\ -+ Ignore user-provided patterns. \n\ -\n\ -interleave \n\ -+ Alternate between use/resort. \n\ -\n\ -"; -static const std::string triggerSelModeHelp = "\ -Trigger selection modes currently supported by the --trigger-sel option:\n\ -\n\ -default \n\ -+ Default, consider all subterms of quantified formulas for trigger selection.\n\ -\n\ -min \n\ -+ Consider only minimal subterms that meet criteria for triggers.\n\ -\n\ -max \n\ -+ Consider only maximal subterms that meet criteria for triggers. \n\ -\n\ -"; -static const std::string prenexQuantModeHelp = "\ -Prenex quantifiers modes currently supported by the --prenex-quant option:\n\ -\n\ -default \n\ -+ Default, prenex all nested quantifiers except those with user patterns.\n\ -\n\ -all \n\ -+ Prenex all nested quantifiers.\n\ -\n\ -none \n\ -+ Do no prenex nested quantifiers. \n\ -\n\ -"; -static const std::string cegqiFairModeHelp = "\ -Modes for enforcing fairness for counterexample guided quantifier instantion, supported by --cegqi-fair:\n\ -\n\ -uf-dt-size \n\ -+ Enforce fairness using an uninterpreted function for datatypes size.\n\ -\n\ -default | dt-size \n\ -+ Default, enforce fairness using size theory operator.\n\ -\n\ -dt-height-bound \n\ -+ Enforce fairness by height bound predicate.\n\ -\n\ -none \n\ -+ Do not enforce fairness. \n\ -\n\ -"; -static const std::string termDbModeHelp = "\ -Modes for term database, supported by --term-db-mode:\n\ -\n\ -all \n\ -+ Quantifiers module considers all ground terms.\n\ -\n\ -relevant \n\ -+ Quantifiers module considers only ground terms connected to current assertions. \n\ -\n\ -"; -static const std::string iteLiftQuantHelp = "\ -Modes for term database, supported by --ite-lift-quant:\n\ -\n\ -none \n\ -+ Do not lift if-then-else in quantified formulas.\n\ -\n\ -simple \n\ -+ Lift if-then-else in quantified formulas if results in smaller term size.\n\ -\n\ -all \n\ -+ Lift if-then-else in quantified formulas. \n\ -\n\ -"; -static const std::string sygusInvTemplHelp = "\ -Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\ -\n\ -none \n\ -+ Synthesize invariant directly.\n\ -\n\ -pre \n\ -+ Synthesize invariant based on weakening of precondition .\n\ -\n\ -post \n\ -+ Synthesize invariant based on strengthening of postcondition. \n\ -\n\ -"; -static const std::string macrosQuantHelp = "\ -Template modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\ -\n\ -all \n\ -+ Infer definitions for functions, including those containing quantified formulas.\n\ -\n\ -ground (default) \n\ -+ Only infer ground definitions for functions.\n\ -\n\ -ground-uf \n\ -+ Only infer ground definitions for functions that result in triggers for all free variables.\n\ -\n\ -"; - -inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "pre-full") { - return INST_WHEN_PRE_FULL; - } else if(optarg == "full") { - return INST_WHEN_FULL; - } else if(optarg == "full-delay") { - return INST_WHEN_FULL_DELAY; - } else if(optarg == "full-last-call") { - return INST_WHEN_FULL_LAST_CALL; - } else if(optarg == "full-delay-last-call") { - return INST_WHEN_FULL_DELAY_LAST_CALL; - } else if(optarg == "last-call") { - return INST_WHEN_LAST_CALL; - } else if(optarg == "help") { - puts(instWhenHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --inst-when: `") + - optarg + "'. Try --inst-when help."); - } -} - -inline void checkInstWhenMode(std::string option, InstWhenMode mode, SmtEngine* smt) throw(OptionException) { - if(mode == INST_WHEN_PRE_FULL) { - throw OptionException(std::string("Mode pre-full for ") + option + " is not supported in this release."); - } -} - -inline LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "none") { - return LITERAL_MATCH_NONE; - } else if(optarg == "predicate") { - return LITERAL_MATCH_PREDICATE; - } else if(optarg == "equality") { - return LITERAL_MATCH_EQUALITY; - } else if(optarg == "help") { - puts(literalMatchHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --literal-matching: `") + - optarg + "'. Try --literal-matching help."); - } -} - -inline void checkLiteralMatchMode(std::string option, LiteralMatchMode mode, SmtEngine* smt) throw(OptionException) { - if(mode == LITERAL_MATCH_EQUALITY) { - throw OptionException(std::string("Mode equality for ") + option + " is not supported in this release."); - } -} - -inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "gen-ev") { - return MBQI_GEN_EVAL; - } else if(optarg == "none") { - return MBQI_NONE; - } else if(optarg == "default" || optarg == "fmc") { - return MBQI_FMC; - } else if(optarg == "fmc-interval") { - return MBQI_FMC_INTERVAL; - } else if(optarg == "abs") { - return MBQI_ABS; - } else if(optarg == "trust") { - return MBQI_TRUST; - } else if(optarg == "help") { - puts(mbqiModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --mbqi: `") + - optarg + "'. Try --mbqi help."); - } -} - -inline void checkMbqiMode(std::string option, MbqiMode mode, SmtEngine* smt) throw(OptionException) { - -} - -inline QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "default") { - return QCF_WHEN_MODE_DEFAULT; - } else if(optarg == "last-call") { - return QCF_WHEN_MODE_LAST_CALL; - } else if(optarg == "std") { - return QCF_WHEN_MODE_STD; - } else if(optarg == "std-h") { - return QCF_WHEN_MODE_STD_H; - } else if(optarg == "help") { - puts(qcfWhenModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --quant-cf-when: `") + - optarg + "'. Try --quant-cf-when help."); - } -} -inline QcfMode stringToQcfMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "conflict") { - return QCF_CONFLICT_ONLY; - } else if(optarg == "default" || optarg == "prop-eq") { - return QCF_PROP_EQ; - } else if(optarg == "partial") { - return QCF_PARTIAL; - } else if(optarg == "mc" ) { - return QCF_MC; - } else if(optarg == "help") { - puts(qcfModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --quant-cf-mode: `") + - optarg + "'. Try --quant-cf-mode help."); - } -} - -inline UserPatMode stringToUserPatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "use") { - return USER_PAT_MODE_USE; - } else if(optarg == "default" || optarg == "trust") { - return USER_PAT_MODE_TRUST; - } else if(optarg == "resort") { - return USER_PAT_MODE_RESORT; - } else if(optarg == "ignore") { - return USER_PAT_MODE_IGNORE; - } else if(optarg == "interleave") { - return USER_PAT_MODE_INTERLEAVE; - } else if(optarg == "help") { - puts(userPatModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --user-pat: `") + - optarg + "'. Try --user-pat help."); - } -} - -inline TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "default" || optarg == "all" ) { - return TRIGGER_SEL_DEFAULT; - } else if(optarg == "min") { - return TRIGGER_SEL_MIN; - } else if(optarg == "max") { - return TRIGGER_SEL_MAX; - } else if(optarg == "help") { - puts(triggerSelModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --trigger-sel: `") + - optarg + "'. Try --trigger-sel help."); - } -} - -inline PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "default" ) { - return PRENEX_NO_USER_PAT; - } else if(optarg == "all") { - return PRENEX_ALL; - } else if(optarg == "none") { - return PRENEX_NONE; - } else if(optarg == "help") { - puts(prenexQuantModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --prenex-quant: `") + - optarg + "'. Try --prenex-quant help."); - } -} - -inline CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "uf-dt-size" ) { - return CEGQI_FAIR_UF_DT_SIZE; - } else if(optarg == "default" || optarg == "dt-size") { - return CEGQI_FAIR_DT_SIZE; - } else if(optarg == "dt-height-bound" ){ - return CEGQI_FAIR_DT_HEIGHT_PRED; - } else if(optarg == "none") { - return CEGQI_FAIR_NONE; - } else if(optarg == "help") { - puts(cegqiFairModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --cegqi-fair: `") + - optarg + "'. Try --cegqi-fair help."); - } -} - -inline TermDbMode stringToTermDbMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "all" ) { - return TERM_DB_ALL; - } else if(optarg == "relevant") { - return TERM_DB_RELEVANT; - } else if(optarg == "help") { - puts(termDbModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --term-db-mode: `") + - optarg + "'. Try --term-db-mode help."); - } -} - -inline IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "all" ) { - return ITE_LIFT_QUANT_MODE_ALL; - } else if(optarg == "simple") { - return ITE_LIFT_QUANT_MODE_SIMPLE; - } else if(optarg == "none") { - return ITE_LIFT_QUANT_MODE_NONE; - } else if(optarg == "help") { - puts(iteLiftQuantHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --ite-lift-quant: `") + - optarg + "'. Try --ite-lift-quant help."); - } -} - -inline SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "none" ) { - return SYGUS_INV_TEMPL_MODE_NONE; - } else if(optarg == "pre") { - return SYGUS_INV_TEMPL_MODE_PRE; - } else if(optarg == "post") { - return SYGUS_INV_TEMPL_MODE_POST; - } else if(optarg == "help") { - puts(sygusInvTemplHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --sygus-inv-templ: `") + - optarg + "'. Try --sygus-inv-templ help."); - } -} - -inline MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "all" ) { - return MACROS_QUANT_MODE_ALL; - } else if(optarg == "ground") { - return MACROS_QUANT_MODE_GROUND; - } else if(optarg == "ground-uf") { - return MACROS_QUANT_MODE_GROUND_UF; - } else if(optarg == "help") { - puts(macrosQuantHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --macros-quant-mode: `") + - optarg + "'. Try --macros-quant-mode help."); - } -} - -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H */ diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index ca5d23cd1..b6256980a 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -13,14 +13,15 @@ ** **/ +#include "theory/quantifiers/quant_conflict_find.h" + #include <vector> -#include "theory/quantifiers/quant_conflict_find.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/quant_util.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" +#include "theory/theory_engine.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index ef5b71f9d..8c6b30124 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -13,7 +13,8 @@ **/ #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/options.h" + +#include "options/quantifiers_options.h" #include "theory/quantifiers/term_database.h" using namespace std; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 1e2ac21a0..0afc8b1bb 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -13,9 +13,10 @@ **/ #include "theory/quantifiers/quantifiers_rewriter.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" + +#include "options/quantifiers_options.h" #include "theory/datatypes/datatypes_rewriter.h" +#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" using namespace std; diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index a70d36ac0..4c8050239 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -15,13 +15,14 @@ **/ #include "theory/quantifiers/rewrite_engine.h" -#include "theory/quantifiers/quant_util.h" + +#include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/model_engine.h" -#include "theory/quantifiers/options.h" #include "theory/quantifiers/inst_match_generator.h" -#include "theory/theory_engine.h" +#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_database.h" +#include "theory/theory_engine.h" using namespace CVC4; using namespace std; diff --git a/src/theory/quantifiers/symmetry_breaking.cpp b/src/theory/quantifiers/symmetry_breaking.cpp index 12b16ef06..4c8e24d08 100644 --- a/src/theory/quantifiers/symmetry_breaking.cpp +++ b/src/theory/quantifiers/symmetry_breaking.cpp @@ -13,15 +13,16 @@ ** **/ +#include "theory/quantifiers/symmetry_breaking.h" + #include <vector> -#include "theory/quantifiers/symmetry_breaking.h" -#include "theory/rewriter.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" +#include "theory/sort_inference.h" #include "theory/theory_engine.h" -#include "util/sort_inference.h" -#include "theory/uf/theory_uf_strong_solver.h" #include "theory/uf/theory_uf.h" +#include "theory/uf/theory_uf_strong_solver.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h index c3ba92214..43e5ec765 100644 --- a/src/theory/quantifiers/symmetry_breaking.h +++ b/src/theory/quantifiers/symmetry_breaking.h @@ -17,20 +17,19 @@ #ifndef __CVC4__QUANT_SYMMETRY_BREAKING_H #define __CVC4__QUANT_SYMMETRY_BREAKING_H -#include "theory/theory.h" - #include <iostream> +#include <map> #include <string> #include <vector> -#include <map> -#include "expr/node.h" -#include "expr/type_node.h" -#include "util/sort_inference.h" +#include "context/cdchunk_list.h" +#include "context/cdhashmap.h" #include "context/context.h" #include "context/context_mm.h" -#include "context/cdhashmap.h" -#include "context/cdchunk_list.h" +#include "expr/node.h" +#include "expr/type_node.h" +#include "theory/sort_inference.h" +#include "theory/theory.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 724f16947..f3bbc65cc 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -13,22 +13,23 @@ **/ #include "theory/quantifiers/term_database.h" -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/trigger.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/theory_quantifiers.h" -#include "util/datatype.h" + +#include "expr/datatype.h" +#include "options/quantifiers_options.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/ce_guided_instantiation.h" -#include "theory/quantifiers/rewrite_engine.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fun_def_engine.h" +#include "theory/quantifiers/rewrite_engine.h" +#include "theory/quantifiers/theory_quantifiers.h" +#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers_engine.h" +#include "theory/theory_engine.h" //for sygus +#include "smt/smt_engine_scope.h" #include "theory/bv/theory_bv_utils.h" #include "util/bitvector.h" -#include "smt/smt_engine_scope.h" using namespace std; using namespace CVC4; @@ -2807,4 +2808,3 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > out << n; } } - diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 48891732b..e9ff60137 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -14,17 +14,18 @@ ** Implementation of the theory of quantifiers. **/ - #include "theory/quantifiers/theory_quantifiers.h" -#include "theory/valuation.h" -#include "theory/quantifiers_engine.h" + + +#include "base/cvc4_assert.h" +#include "expr/kind.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/instantiation_engine.h" #include "theory/quantifiers/model_engine.h" -#include "expr/kind.h" -#include "util/cvc4_assert.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers_engine.h" +#include "theory/valuation.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 0f16f0e80..98f486145 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -19,15 +19,15 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H #define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H -#include "context/cdhashmap.h" -#include "theory/theory.h" -#include "util/hash.h" -#include "util/statistics_registry.h" - #include <ext/hash_set> #include <iostream> #include <map> +#include "context/cdhashmap.h" +#include "expr/statistics_registry.h" +#include "theory/theory.h" +#include "util/hash.h" + namespace CVC4 { class TheoryEngine; diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index 3ce0250fe..1fb8ddaf9 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -19,7 +19,7 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H #define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H -#include "util/matcher.h" +#include "expr/matcher.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index fdfa77b02..9aee18317 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -13,13 +13,14 @@ **/ #include "theory/quantifiers/trigger.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers_engine.h" + +#include "options/quantifiers_options.h" #include "theory/quantifiers/candidate_generator.h" -#include "theory/uf/equality_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/inst_match_generator.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers_engine.h" +#include "theory/theory_engine.h" +#include "theory/uf/equality_engine.h" using namespace std; using namespace CVC4; |