summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/arrays/kinds2
-rw-r--r--src/theory/arrays/theory_arrays.cpp17
-rw-r--r--src/theory/arrays/theory_arrays.h11
-rw-r--r--src/theory/datatypes/kinds2
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp20
-rw-r--r--src/theory/datatypes/theory_datatypes.h14
-rw-r--r--src/theory/sep/kinds2
-rw-r--r--src/theory/sep/theory_sep.cpp13
-rw-r--r--src/theory/sep/theory_sep.h15
-rw-r--r--src/theory/sets/kinds2
-rw-r--r--src/theory/sets/theory_sets.cpp4
-rw-r--r--src/theory/sets/theory_sets.h1
-rw-r--r--src/theory/sets/theory_sets_private.cpp2
-rw-r--r--src/theory/sets/theory_sets_private.h2
-rw-r--r--src/theory/strings/kinds2
-rw-r--r--src/theory/strings/theory_strings.cpp13
-rw-r--r--src/theory/strings/theory_strings.h13
-rw-r--r--src/theory/uf/kinds2
-rw-r--r--src/theory/uf/theory_uf.cpp15
-rw-r--r--src/theory/uf/theory_uf.h14
20 files changed, 60 insertions, 106 deletions
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 659f05ae8..629064d99 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -8,7 +8,7 @@ theory THEORY_ARRAYS ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_
typechecker "theory/arrays/theory_arrays_type_rules.h"
properties polite stable-infinite parametric
-properties check propagate presolve
+properties check presolve
rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arrays_rewriter.h"
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 9c1e22940..d659aff11 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -414,14 +414,17 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs
// T-PROPAGATION / REGISTRATION
/////////////////////////////////////////////////////////////////////////////
-
-bool TheoryArrays::propagate(TNode literal)
+bool TheoryArrays::propagateLit(TNode literal)
{
- Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ")" << std::endl;
+ Debug("arrays") << spaces(getSatContext()->getLevel())
+ << "TheoryArrays::propagateLit(" << literal << ")"
+ << std::endl;
// If already in conflict, no more propagation
if (d_conflict) {
- Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << "): already in conflict" << std::endl;
+ Debug("arrays") << spaces(getSatContext()->getLevel())
+ << "TheoryArrays::propagateLit(" << literal
+ << "): already in conflict" << std::endl;
return false;
}
@@ -861,12 +864,6 @@ void TheoryArrays::preRegisterTerm(TNode node)
}
}
-
-void TheoryArrays::propagate(Effort e)
-{
- // direct propagation now
-}
-
TrustNode TheoryArrays::explain(TNode literal)
{
Node explanation = explain(literal, NULL);
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 2d09c55fe..24ebb4916 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -213,7 +213,7 @@ class TheoryArrays : public Theory {
context::CDO<unsigned> d_literalsToPropagateIndex;
/** Should be called to propagate the literal. */
- bool propagate(TNode literal);
+ bool propagateLit(TNode literal);
/** Explain why this literal is true by adding assumptions */
void explain(TNode literal, std::vector<TNode>& assumptions,
@@ -227,7 +227,6 @@ class TheoryArrays : public Theory {
public:
void preRegisterTerm(TNode n) override;
- void propagate(Effort e) override;
Node explain(TNode n, eq::EqProof* proof);
TrustNode explain(TNode n) override;
@@ -306,9 +305,9 @@ class TheoryArrays : public Theory {
<< (value ? "true" : "false") << ")" << std::endl;
// Just forward to arrays
if (value) {
- return d_arrays.propagate(predicate);
+ return d_arrays.propagateLit(predicate);
}
- return d_arrays.propagate(predicate.notNode());
+ return d_arrays.propagateLit(predicate.notNode());
}
bool eqNotifyTriggerTermEquality(TheoryId tag,
@@ -324,14 +323,14 @@ class TheoryArrays : public Theory {
}
}
// Propagate equality between shared terms
- return d_arrays.propagate(t1.eqNode(t2));
+ return d_arrays.propagateLit(t1.eqNode(t2));
} else {
if (t1.getType().isArray()) {
if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) {
return true;
}
}
- return d_arrays.propagate(t1.eqNode(t2).notNode());
+ return d_arrays.propagateLit(t1.eqNode(t2).notNode());
}
return true;
}
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 4b80529d2..26bff20b7 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -7,7 +7,7 @@
theory THEORY_DATATYPES ::CVC4::theory::datatypes::TheoryDatatypes "theory/datatypes/theory_datatypes.h"
typechecker "theory/datatypes/theory_datatypes_type_rules.h"
-properties check presolve parametric propagate
+properties check parametric
rewriter ::CVC4::theory::datatypes::DatatypesRewriter "theory/datatypes/datatypes_rewriter.h"
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 08ec4322e..65264bb3f 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -701,11 +701,6 @@ TrustNode TheoryDatatypes::expandDefinition(Node n)
return TrustNode::null();
}
-void TheoryDatatypes::presolve()
-{
- Debug("datatypes") << "TheoryDatatypes::presolve()" << endl;
-}
-
TrustNode TheoryDatatypes::ppRewrite(TNode in)
{
Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl;
@@ -739,17 +734,14 @@ void TheoryDatatypes::addSharedTerm(TNode t) {
Debug("datatypes") << "TheoryDatatypes::addSharedTerm() finished" << std::endl;
}
-/** propagate */
-void TheoryDatatypes::propagate(Effort effort){
-
-}
-
-/** propagate */
-bool TheoryDatatypes::propagate(TNode literal){
- Debug("dt::propagate") << "TheoryDatatypes::propagate(" << literal << ")" << std::endl;
+bool TheoryDatatypes::propagateLit(TNode literal)
+{
+ Debug("dt::propagate") << "TheoryDatatypes::propagateLit(" << literal << ")"
+ << std::endl;
// If already in conflict, no more propagation
if (d_conflict) {
- Debug("dt::propagate") << "TheoryDatatypes::propagate(" << literal << "): already in conflict" << std::endl;
+ Debug("dt::propagate") << "TheoryDatatypes::propagateLit(" << literal
+ << "): already in conflict" << std::endl;
return false;
}
Trace("dt-prop") << "dtPropagate " << literal << std::endl;
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 0465a7788..137aae469 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -62,9 +62,9 @@ class TheoryDatatypes : public Theory {
{
Debug("dt") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
if (value) {
- return d_dt.propagate(predicate);
+ return d_dt.propagateLit(predicate);
}
- return d_dt.propagate(predicate.notNode());
+ return d_dt.propagateLit(predicate.notNode());
}
bool eqNotifyTriggerTermEquality(TheoryId tag,
TNode t1,
@@ -73,10 +73,9 @@ class TheoryDatatypes : public Theory {
{
Debug("dt") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
if (value) {
- return d_dt.propagate(t1.eqNode(t2));
- } else {
- return d_dt.propagate(t1.eqNode(t2).notNode());
+ return d_dt.propagateLit(t1.eqNode(t2));
}
+ return d_dt.propagateLit(t1.eqNode(t2).notNode());
}
void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
{
@@ -270,9 +269,7 @@ private:
//--------------------------------- end initialization
/** propagate */
- void propagate(Effort effort) override;
- /** propagate */
- bool propagate(TNode literal);
+ bool propagateLit(TNode literal);
/** explain */
void addAssumptions( std::vector<TNode>& assumptions, std::vector<TNode>& tassumptions );
void explainEquality( TNode a, TNode b, bool polarity, std::vector<TNode>& assumptions );
@@ -293,7 +290,6 @@ private:
void preRegisterTerm(TNode n) override;
TrustNode expandDefinition(Node n) override;
TrustNode ppRewrite(TNode n) override;
- void presolve() override;
void addSharedTerm(TNode t) override;
EqualityStatus getEqualityStatus(TNode a, TNode b) override;
bool collectModelInfo(TheoryModel* m) override;
diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds
index 235b61172..7a3fb00a4 100644
--- a/src/theory/sep/kinds
+++ b/src/theory/sep/kinds
@@ -8,7 +8,7 @@ theory THEORY_SEP ::CVC4::theory::sep::TheorySep "theory/sep/theory_sep.h"
typechecker "theory/sep/theory_sep_type_rules.h"
properties polite stable-infinite parametric
-properties check propagate presolve
+properties check presolve
rewriter ::CVC4::theory::sep::TheorySepRewriter "theory/sep/theory_sep_rewriter.h"
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index f75eb4472..cf3cf2f9a 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -111,13 +111,13 @@ Theory::PPAssertStatus TheorySep::ppAssert(TNode in, SubstitutionMap& outSubstit
// T-PROPAGATION / REGISTRATION
/////////////////////////////////////////////////////////////////////////////
-
-bool TheorySep::propagate(TNode literal)
+bool TheorySep::propagateLit(TNode literal)
{
- Debug("sep") << "TheorySep::propagate(" << literal << ")" << std::endl;
+ Debug("sep") << "TheorySep::propagateLit(" << literal << ")" << std::endl;
// If already in conflict, no more propagation
if (d_conflict) {
- Debug("sep") << "TheorySep::propagate(" << literal << "): already in conflict" << std::endl;
+ Debug("sep") << "TheorySep::propagateLit(" << literal
+ << "): already in conflict" << std::endl;
return false;
}
bool ok = d_out->propagate(literal);
@@ -146,11 +146,6 @@ void TheorySep::explain(TNode literal, std::vector<TNode>& assumptions) {
}
}
-
-void TheorySep::propagate(Effort e){
-
-}
-
TrustNode TheorySep::explain(TNode literal)
{
Debug("sep") << "TheorySep::explain(" << literal << ")" << std::endl;
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index b178b97db..bbb37a3a2 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -105,13 +105,12 @@ class TheorySep : public Theory {
private:
/** Should be called to propagate the literal. */
- bool propagate(TNode literal);
+ bool propagateLit(TNode literal);
/** Explain why this literal is true by adding assumptions */
void explain(TNode literal, std::vector<TNode>& assumptions);
public:
- void propagate(Effort e) override;
TrustNode explain(TNode n) override;
public:
@@ -163,9 +162,9 @@ class TheorySep : public Theory {
// Just forward to sep
if (value)
{
- return d_sep.propagate(predicate);
+ return d_sep.propagateLit(predicate);
}
- return d_sep.propagate(predicate.notNode());
+ return d_sep.propagateLit(predicate.notNode());
}
bool eqNotifyTriggerTermEquality(TheoryId tag,
TNode t1,
@@ -178,13 +177,9 @@ class TheorySep : public Theory {
if (value)
{
// Propagate equality between shared terms
- return d_sep.propagate(t1.eqNode(t2));
+ return d_sep.propagateLit(t1.eqNode(t2));
}
- else
- {
- return d_sep.propagate(t1.eqNode(t2).notNode());
- }
- return true;
+ return d_sep.propagateLit(t1.eqNode(t2).notNode());
}
void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index 452acfea0..d3c42ef27 100644
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -12,7 +12,7 @@ rewriter ::CVC4::theory::sets::TheorySetsRewriter \
"theory/sets/theory_sets_rewriter.h"
properties parametric
-properties check propagate presolve
+properties check presolve
# constants
constant EMPTYSET \
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 2627f72e3..647a7bb47 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -196,10 +196,6 @@ void TheorySets::presolve() {
d_internal->presolve();
}
-void TheorySets::propagate(Effort e) {
- d_internal->propagate(e);
-}
-
bool TheorySets::isEntailed( Node n, bool pol ) {
return d_internal->isEntailed( n, pol );
}
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 36e6ac65d..9e04b89a7 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -70,7 +70,6 @@ class TheorySets : public Theory
TrustNode expandDefinition(Node n) override;
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
void presolve() override;
- void propagate(Effort) override;
bool isEntailed(Node n, bool pol);
private:
/** Functions to handle callbacks from equality engine */
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index f7c7ae7f9..3c9414606 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1392,8 +1392,6 @@ Node mkAnd(const std::vector<TNode>& conjunctions)
return conjunction;
} /* mkAnd() */
-void TheorySetsPrivate::propagate(Theory::Effort effort) {}
-
bool TheorySetsPrivate::propagate(TNode literal)
{
Debug("sets-prop") << " propagate(" << literal << ")" << std::endl;
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 9a786598c..af780eadc 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -219,8 +219,6 @@ class TheorySetsPrivate {
void presolve();
- void propagate(Theory::Effort);
-
/** get default output channel */
OutputChannel* getOutputChannel();
/** get the valuation */
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 131a48ae9..78c6ab1f1 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -6,7 +6,7 @@
theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/theory_strings.h"
-properties check parametric propagate presolve
+properties check parametric presolve
rewriter ::CVC4::theory::strings::SequencesRewriter "theory/strings/sequences_rewriter.h"
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 6d81c742a..e42796354 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -181,16 +181,15 @@ EqualityStatus TheoryStrings::getEqualityStatus(TNode a, TNode b) {
return EQUALITY_UNKNOWN;
}
-void TheoryStrings::propagate(Effort e) {
- // direct propagation now
-}
-
-bool TheoryStrings::propagate(TNode literal) {
- Debug("strings-propagate") << "TheoryStrings::propagate(" << literal << ")" << std::endl;
+bool TheoryStrings::propagateLit(TNode literal)
+{
+ Debug("strings-propagate")
+ << "TheoryStrings::propagateLit(" << literal << ")" << std::endl;
// If already in conflict, no more propagation
if (d_state.isInConflict())
{
- Debug("strings-propagate") << "TheoryStrings::propagate(" << literal << "): already in conflict" << std::endl;
+ Debug("strings-propagate") << "TheoryStrings::propagateLit(" << literal
+ << "): already in conflict" << std::endl;
return false;
}
// Propagate out
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index da48ece90..8a1afe6b3 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -84,8 +84,6 @@ class TheoryStrings : public Theory {
//--------------------------------- end initialization
/** Identify this theory */
std::string identify() const override;
- /** Propagate */
- void propagate(Effort e) override;
/** Explain */
TrustNode explain(TNode literal) override;
/** Get current substitution */
@@ -130,9 +128,9 @@ class TheoryStrings : public Theory {
{
Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
if (value) {
- return d_str.propagate(predicate);
+ return d_str.propagateLit(predicate);
}
- return d_str.propagate(predicate.notNode());
+ return d_str.propagateLit(predicate.notNode());
}
bool eqNotifyTriggerTermEquality(TheoryId tag,
TNode t1,
@@ -141,10 +139,9 @@ class TheoryStrings : public Theory {
{
Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
if (value) {
- return d_str.propagate(t1.eqNode(t2));
- } else {
- return d_str.propagate(t1.eqNode(t2).notNode());
+ return d_str.propagateLit(t1.eqNode(t2));
}
+ return d_str.propagateLit(t1.eqNode(t2).notNode());
}
void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
{
@@ -175,7 +172,7 @@ class TheoryStrings : public Theory {
SolverState& d_state;
};/* class TheoryStrings::NotifyClass */
/** propagate method */
- bool propagate(TNode literal);
+ bool propagateLit(TNode literal);
/** compute care graph */
void computeCareGraph() override;
/**
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index 109e6d0a1..9564899fe 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -8,7 +8,7 @@ theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h"
typechecker "theory/uf/theory_uf_type_rules.h"
properties stable-infinite parametric
-properties check propagate ppStaticLearn presolve
+properties check ppStaticLearn presolve
rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h"
parameterized APPLY_UF VARIABLE 1: "application of an uninterpreted function; first parameter is the function, remaining ones are parameters to that function"
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 0b97d8a5d..29014d33f 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -261,11 +261,14 @@ void TheoryUF::preRegisterTerm(TNode node) {
}
}/* TheoryUF::preRegisterTerm() */
-bool TheoryUF::propagate(TNode literal) {
- Debug("uf::propagate") << "TheoryUF::propagate(" << literal << ")" << std::endl;
+bool TheoryUF::propagateLit(TNode literal)
+{
+ Debug("uf::propagate") << "TheoryUF::propagateLit(" << literal << ")"
+ << std::endl;
// If already in conflict, no more propagation
if (d_conflict) {
- Debug("uf::propagate") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
+ Debug("uf::propagate") << "TheoryUF::propagateLit(" << literal
+ << "): already in conflict" << std::endl;
return false;
}
// Propagate out
@@ -276,12 +279,6 @@ bool TheoryUF::propagate(TNode literal) {
return ok;
}/* TheoryUF::propagate(TNode) */
-void TheoryUF::propagate(Effort effort) {
- //if (d_thss != NULL) {
- // return d_thss->propagate(effort);
- //}
-}
-
void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf) {
// Do the work
bool polarity = literal.getKind() != kind::NOT;
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 7d17fdb86..8efaf79e3 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -49,10 +49,9 @@ public:
{
Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
if (value) {
- return d_uf.propagate(predicate);
- } else {
- return d_uf.propagate(predicate.notNode());
+ return d_uf.propagateLit(predicate);
}
+ return d_uf.propagateLit(predicate.notNode());
}
bool eqNotifyTriggerTermEquality(TheoryId tag,
@@ -62,10 +61,9 @@ public:
{
Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
if (value) {
- return d_uf.propagate(t1.eqNode(t2));
- } else {
- return d_uf.propagate(t1.eqNode(t2).notNode());
+ return d_uf.propagateLit(t1.eqNode(t2));
}
+ return d_uf.propagateLit(t1.eqNode(t2).notNode());
}
void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
@@ -119,7 +117,7 @@ private:
* Should be called to propagate the literal. We use a node here
* since some of the propagated literals are not kept anywhere.
*/
- bool propagate(TNode literal);
+ bool propagateLit(TNode literal);
/**
* Explain why this literal is true by adding assumptions
@@ -189,8 +187,6 @@ private:
void addSharedTerm(TNode n) override;
void computeCareGraph() override;
- void propagate(Effort effort) override;
-
EqualityStatus getEqualityStatus(TNode a, TNode b) override;
std::string identify() const override { return "THEORY_UF"; }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback