From e05ad4759f2ae01cc06a9ca715c777d188f0f5fd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 2 Feb 2021 12:25:21 -0600 Subject: [PATCH] Cleanup some includes (#5847) In particular, theory_engine.h is included many places spuriously. A few blocks of code changed indentation, updated to guidelines. --- src/preprocessing/passes/ackermann.cpp | 1 + src/preprocessing/passes/bv_to_int.cpp | 1 + .../passes/extended_rewriter_pass.cpp | 1 + src/preprocessing/passes/int_to_bv.cpp | 1 + src/preprocessing/passes/ite_removal.cpp | 1 + src/preprocessing/passes/ite_simp.cpp | 1 + src/preprocessing/passes/miplib_trick.cpp | 1 + src/preprocessing/passes/non_clausal_simp.cpp | 1 + .../passes/quantifier_macros.cpp | 1 + .../passes/theory_preprocess.cpp | 1 + src/prop/theory_proxy.cpp | 1 + src/smt/smt_solver.cpp | 1 + src/theory/combination_care_graph.cpp | 1 + src/theory/model_manager.cpp | 2 + .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 2 - .../ematching/candidate_generator.cpp | 2 - .../quantifiers/ematching/ho_trigger.cpp | 2 - .../ematching/instantiation_engine.cpp | 1 - src/theory/quantifiers/fmf/model_engine.cpp | 2 - .../quantifiers/quant_conflict_find.cpp | 51 ++++++++++--------- src/theory/quantifiers/skolemize.cpp | 1 + src/theory/quantifiers/sygus/cegis.cpp | 1 - src/theory/quantifiers/sygus/cegis_unif.cpp | 1 - .../quantifiers/sygus/synth_conjecture.cpp | 2 - src/theory/quantifiers/sygus/synth_engine.cpp | 1 - src/theory/quantifiers/sygus_inst.cpp | 1 - src/theory/quantifiers/term_database.cpp | 1 + src/theory/quantifiers/term_util.cpp | 1 - src/theory/quantifiers_engine.cpp | 1 + src/theory/theory_engine.cpp | 14 +---- src/theory/theory_engine.h | 18 +++---- src/theory/uf/cardinality_extension.cpp | 9 ++-- src/theory/uf/theory_uf_model.cpp | 37 +++++++------- src/theory/uf/theory_uf_model.h | 3 ++ src/theory/valuation.cpp | 1 + 35 files changed, 80 insertions(+), 87 deletions(-) diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index af6cae796..075a50e06 100644 --- a/src/preprocessing/passes/ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -26,6 +26,7 @@ #include "base/check.h" #include "expr/node_algorithm.h" #include "options/options.h" +#include "options/smt_options.h" using namespace CVC4; using namespace CVC4::theory; diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 04d6b7a0c..f5d840a49 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -24,6 +24,7 @@ #include "expr/node.h" #include "expr/node_traversal.h" +#include "options/smt_options.h" #include "options/uf_options.h" #include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h" #include "theory/bv/theory_bv_rewrite_rules_simplification.h" diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp index f1cdd5b5d..95e107328 100644 --- a/src/preprocessing/passes/extended_rewriter_pass.cpp +++ b/src/preprocessing/passes/extended_rewriter_pass.cpp @@ -16,6 +16,7 @@ #include "preprocessing/passes/extended_rewriter_pass.h" +#include "options/smt_options.h" #include "theory/quantifiers/extended_rewrite.h" namespace CVC4 { diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index fd0800f23..5b0465772 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -24,6 +24,7 @@ #include "expr/node.h" #include "expr/node_traversal.h" +#include "options/smt_options.h" #include "theory/rewriter.h" #include "theory/theory.h" diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index 66a32472b..c8b713894 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -17,6 +17,7 @@ #include "preprocessing/passes/ite_removal.h" +#include "options/smt_options.h" #include "theory/rewriter.h" #include "theory/theory_preprocessor.h" diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index 746bf33bd..2a1f4c3e6 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -16,6 +16,7 @@ #include +#include "options/smt_options.h" #include "smt/smt_statistics_registry.h" #include "smt_util/nary_builder.h" #include "theory/arith/arith_ite_utils.h" diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 23a17c939..50dbc4a27 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -19,6 +19,7 @@ #include "expr/node_self_iterator.h" #include "options/arith_options.h" +#include "options/smt_options.h" #include "smt/smt_statistics_registry.h" #include "smt_util/boolean_simplification.h" #include "theory/booleans/circuit_propagator.h" diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index 656822299..6db701565 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -19,6 +19,7 @@ #include #include "context/cdo.h" +#include "options/smt_options.h" #include "smt/smt_statistics_registry.h" #include "theory/theory_model.h" #include "theory/trust_substitutions.h" diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp index 35eeac125..69b665854 100644 --- a/src/preprocessing/passes/quantifier_macros.cpp +++ b/src/preprocessing/passes/quantifier_macros.cpp @@ -19,6 +19,7 @@ #include #include "options/quantifiers_options.h" +#include "options/smt_options.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/arith/arith_msum.h" diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp index 4552d13fc..50831f585 100644 --- a/src/preprocessing/passes/theory_preprocess.cpp +++ b/src/preprocessing/passes/theory_preprocess.cpp @@ -16,6 +16,7 @@ #include "preprocessing/passes/theory_preprocess.h" +#include "options/smt_options.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index a6d570bc2..06e729714 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -19,6 +19,7 @@ #include "context/context.h" #include "decision/decision_engine.h" #include "options/decision_options.h" +#include "options/smt_options.h" #include "proof/cnf_proof.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 433eb9cd0..c47d1c624 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -14,6 +14,7 @@ #include "smt/smt_solver.h" +#include "options/smt_options.h" #include "prop/prop_engine.h" #include "smt/assertions.h" #include "smt/preprocessor.h" diff --git a/src/theory/combination_care_graph.cpp b/src/theory/combination_care_graph.cpp index 402eeeb26..1ebffc8c2 100644 --- a/src/theory/combination_care_graph.cpp +++ b/src/theory/combination_care_graph.cpp @@ -15,6 +15,7 @@ #include "theory/combination_care_graph.h" #include "expr/node_visitor.h" +#include "prop/prop_engine.h" #include "theory/care_graph.h" #include "theory/theory_engine.h" diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp index e4dddfdbf..295b7309e 100644 --- a/src/theory/model_manager.cpp +++ b/src/theory/model_manager.cpp @@ -14,7 +14,9 @@ #include "theory/model_manager.h" +#include "options/smt_options.h" #include "options/theory_options.h" +#include "prop/prop_engine.h" #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index cb31e80d3..c539bfdb0 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -15,7 +15,6 @@ #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" -#include "smt/term_formula_removal.h" #include "theory/arith/partial_model.h" #include "theory/arith/theory_arith.h" #include "theory/arith/theory_arith_private.h" @@ -26,7 +25,6 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" -#include "theory/theory_engine.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 0fe1e6abe..97693fae0 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -22,8 +22,6 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" -#include "theory/theory_engine.h" -#include "theory/uf/theory_uf.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 6d13ef2ee..7479d005a 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -19,8 +19,6 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" -#include "theory/theory_engine.h" -#include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf_rewriter.h" #include "util/hash.h" diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 48c02f288..69c33d329 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -23,7 +23,6 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" -#include "theory/theory_engine.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 427d82e7c..715002f7b 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -23,8 +23,6 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" -#include "theory/theory_engine.h" -#include "theory/uf/equality_engine.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 4359b8b19..c025dc29e 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -26,7 +26,6 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" -#include "theory/theory_engine.h" using namespace CVC4::kind; using namespace std; @@ -643,31 +642,33 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) { Trace("qcf-tconstraint-debug") << "Check : " << lit << std::endl; Node rew = Rewriter::rewrite( lit ); - if( rew==p->d_false ){ - Trace("qcf-tconstraint-debug") << "...constraint " << lit << " is disentailed (rewrites to false)." << std::endl; - return false; - }else if( rew!=p->d_true ){ - //if checking for conflicts, we must be sure that the (negation of) constraint is (not) entailed - if( !chEnt ){ - rew = Rewriter::rewrite( rew.negate() ); - } - //check if it is entailed - Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl; - std::pair et = - p->getQuantifiersEngine()->getTheoryEngine()->entailmentCheck( - options::TheoryOfMode::THEORY_OF_TYPE_BASED, rew); - ++(p->d_statistics.d_entailment_checks); - Trace("qcf-tconstraint-debug") << "ET result : " << et.first << " " << et.second << std::endl; - if( !et.first ){ - Trace("qcf-tconstraint-debug") << "...cannot show entailment of " << rew << "." << std::endl; - return !chEnt; - }else{ - return chEnt; - } - }else{ - Trace("qcf-tconstraint-debug") << "...rewrites to true." << std::endl; - return true; + if (rew.isConst()) + { + Trace("qcf-tconstraint-debug") << "...constraint " << lit << " rewrites to " + << rew << "." << std::endl; + return rew.getConst(); + } + // if checking for conflicts, we must be sure that the (negation of) + // constraint is (not) entailed + if (!chEnt) + { + rew = Rewriter::rewrite(rew.negate()); + } + // check if it is entailed + Trace("qcf-tconstraint-debug") + << "Check entailment of " << rew << "..." << std::endl; + std::pair et = p->getState().getValuation().entailmentCheck( + options::TheoryOfMode::THEORY_OF_TYPE_BASED, rew); + ++(p->d_statistics.d_entailment_checks); + Trace("qcf-tconstraint-debug") + << "ET result : " << et.first << " " << et.second << std::endl; + if (!et.first) + { + Trace("qcf-tconstraint-debug") + << "...cannot show entailment of " << rew << "." << std::endl; + return !chEnt; } + return chEnt; } bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue ) { diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 3ddfc4c9f..4f9a0ee91 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -16,6 +16,7 @@ #include "expr/skolem_manager.h" #include "options/quantifiers_options.h" +#include "options/smt_options.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 9470b4e49..c09c78158 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -21,7 +21,6 @@ #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers_engine.h" -#include "theory/theory_engine.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 42e7e2f13..239fa3c94 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -21,7 +21,6 @@ #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers_engine.h" -#include "theory/theory_engine.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index b007f8716..c1333b85f 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -18,7 +18,6 @@ #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" -#include "prop/prop_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/datatypes/sygus_datatype_utils.h" @@ -33,7 +32,6 @@ #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/smt_engine_subsolver.h" -#include "theory/theory_engine.h" using namespace CVC4::kind; using namespace std; diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 43051eb99..4b35bc545 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -21,7 +21,6 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" -#include "theory/theory_engine.h" using namespace CVC4::kind; using namespace std; diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index c4c722ab2..66c9cbf79 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -24,7 +24,6 @@ #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers_engine.h" -#include "theory/theory_engine.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index c39654aa5..5a6e38b78 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -16,6 +16,7 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" +#include "options/smt_options.h" #include "options/theory_options.h" #include "options/uf_options.h" #include "theory/quantifiers/ematching/trigger_term_info.h" diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index d01d6a83f..b0a067630 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -25,7 +25,6 @@ #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers_engine.h" #include "theory/strings/word.h" -#include "theory/theory_engine.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 6338c30b3..28397fd14 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -16,6 +16,7 @@ #include "options/printer_options.h" #include "options/quantifiers_options.h" +#include "options/smt_options.h" #include "options/uf_options.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index bd03a4d03..66c9b9f20 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -16,33 +16,23 @@ #include "theory/theory_engine.h" -#include -#include - #include "base/map_util.h" #include "decision/decision_engine.h" #include "expr/attribute.h" #include "expr/lazy_proof.h" -#include "expr/node.h" #include "expr/node_builder.h" #include "expr/node_visitor.h" #include "expr/proof_ensure_closed.h" -#include "options/bv_options.h" -#include "options/options.h" #include "options/quantifiers_options.h" +#include "options/smt_options.h" #include "options/theory_options.h" #include "printer/printer.h" +#include "prop/prop_engine.h" #include "smt/dump.h" #include "smt/logic_exception.h" -#include "smt/term_formula_removal.h" -#include "theory/arith/arith_ite_utils.h" -#include "theory/bv/theory_bv_utils.h" -#include "theory/care_graph.h" #include "theory/combination_care_graph.h" #include "theory/decision_manager.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/fmf/model_engine.h" -#include "theory/quantifiers/theory_quantifiers.h" #include "theory/quantifiers_engine.h" #include "theory/relevance_manager.h" #include "theory/rewriter.h" diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 1a9447681..d72a999b2 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -19,20 +19,13 @@ #ifndef CVC4__THEORY_ENGINE_H #define CVC4__THEORY_ENGINE_H -#include #include -#include -#include -#include #include #include "base/check.h" -#include "context/cdhashset.h" +#include "context/cdhashmap.h" #include "expr/node.h" -#include "options/options.h" -#include "options/smt_options.h" #include "options/theory_options.h" -#include "prop/prop_engine.h" #include "theory/atom_requests.h" #include "theory/engine_output_channel.h" #include "theory/interrupted.h" @@ -46,13 +39,13 @@ #include "theory/uf/equality_engine.h" #include "theory/valuation.h" #include "util/hash.h" -#include "util/resource_manager.h" #include "util/statistics_registry.h" #include "util/unsafe_interrupt_exception.h" namespace CVC4 { class ResourceManager; +class OutputManager; class TheoryEngineProofGenerator; /** @@ -92,11 +85,12 @@ class SharedSolver; class DecisionManager; class RelevanceManager; -namespace eq { -class EqualityEngine; -} // namespace eq }/* CVC4::theory namespace */ +namespace prop { +class PropEngine; +} + /** * This is essentially an abstraction for a collection of theories. A * TheoryEngine provides services to a PropEngine, making various diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index 3ea4c88e6..bd69245b8 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -14,13 +14,14 @@ #include "theory/uf/cardinality_extension.h" +#include "options/smt_options.h" #include "options/uf_options.h" -#include "theory/uf/theory_uf.h" -#include "theory/uf/equality_engine.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers_engine.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers_engine.h" +#include "theory/theory_engine.h" #include "theory/theory_model.h" +#include "theory/uf/equality_engine.h" +#include "theory/uf/theory_uf.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index a014cccb2..043ab0dab 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -15,21 +15,15 @@ #include "theory/uf/theory_uf_model.h" #include -#include #include "expr/attribute.h" -#include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/theory_engine.h" -#include "theory/uf/equality_engine.h" -#include "theory/uf/theory_uf.h" -using namespace std; -using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::uf; + +namespace CVC4 { +namespace theory { +namespace uf { //clear void UfModelTreeNode::clear(){ @@ -63,14 +57,17 @@ Node UfModelTreeNode::getFunctionValue(std::vector& args, int index, Node defaultValue = d_data[Node::null()].getFunctionValue(args, index + 1, argDefaultValue, simplify); } - vector caseArgs; - map caseValues; + std::vector caseArgs; + std::map caseValues; - for(map< Node, UfModelTreeNode>::iterator it = d_data.begin(); it != d_data.end(); ++it) { - if(!it->first.isNull()) { - Node val = it->second.getFunctionValue(args, index + 1, defaultValue, simplify); - caseArgs.push_back(it->first); - caseValues[it->first] = val; + for (std::pair& p : d_data) + { + if (!p.first.isNull()) + { + Node val = + p.second.getFunctionValue(args, index + 1, defaultValue, simplify); + caseArgs.push_back(p.first); + caseValues[p.first] = val; } } @@ -86,7 +83,7 @@ Node UfModelTreeNode::getFunctionValue(std::vector& args, int index, Node Node val = caseValues[ caseArgs[ i ] ]; if(val.getKind() == ITE) { // use a stack to reverse the order, since we're traversing outside-in - stack stk; + std::stack stk; do { stk.push(val); val = val[2]; @@ -237,3 +234,7 @@ Node UfModelTree::getFunctionValue( const char* argPrefix, bool simplify ){ } return getFunctionValue( vars, simplify ); } + +} // namespace uf +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index 1165f310c..a1576a26d 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -17,6 +17,9 @@ #ifndef CVC4__THEORY_UF_MODEL_H #define CVC4__THEORY_UF_MODEL_H +#include + +#include "expr/node.h" #include "theory/theory_model.h" namespace CVC4 { diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 6fae8421d..1926c836e 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -18,6 +18,7 @@ #include "expr/node.h" #include "options/theory_options.h" +#include "prop/prop_engine.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" #include "theory/theory_model.h" -- 2.30.2