diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-02 12:25:21 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-02 12:25:21 -0600 |
commit | e05ad4759f2ae01cc06a9ca715c777d188f0f5fd (patch) | |
tree | a292cc67c0b41c3bdf325f5160bdede10346add0 /src/theory/quantifiers | |
parent | 4c1f67446ad59f1c5efe7230b96b0d3ccac0e692 (diff) |
Cleanup some includes (#5847)
In particular, theory_engine.h is included many places spuriously.
A few blocks of code changed indentation, updated to guidelines.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/candidate_generator.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/ho_trigger.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/instantiation_engine.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/model_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 51 | ||||
-rw-r--r-- | src/theory/quantifiers/skolemize.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus_inst.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/term_util.cpp | 1 |
14 files changed, 28 insertions, 41 deletions
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<bool, Node> 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<bool>(); + } + // 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<bool, Node> 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; |