summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp2
-rw-r--r--src/theory/quantifiers/ematching/candidate_generator.cpp2
-rw-r--r--src/theory/quantifiers/ematching/ho_trigger.cpp2
-rw-r--r--src/theory/quantifiers/ematching/instantiation_engine.cpp1
-rw-r--r--src/theory/quantifiers/fmf/model_engine.cpp2
-rw-r--r--src/theory/quantifiers/quant_conflict_find.cpp51
-rw-r--r--src/theory/quantifiers/skolemize.cpp1
-rw-r--r--src/theory/quantifiers/sygus/cegis.cpp1
-rw-r--r--src/theory/quantifiers/sygus/cegis_unif.cpp1
-rw-r--r--src/theory/quantifiers/sygus/synth_conjecture.cpp2
-rw-r--r--src/theory/quantifiers/sygus/synth_engine.cpp1
-rw-r--r--src/theory/quantifiers/sygus_inst.cpp1
-rw-r--r--src/theory/quantifiers/term_database.cpp1
-rw-r--r--src/theory/quantifiers/term_util.cpp1
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback