summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/theory/inference_id.cpp7
-rw-r--r--src/theory/inference_id.h35
-rw-r--r--src/theory/uf/cardinality_extension.cpp16
-rw-r--r--src/theory/uf/ho_extension.cpp15
-rw-r--r--src/theory/uf/theory_uf.cpp2
5 files changed, 60 insertions, 15 deletions
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 5a2158d00..81c34cf3f 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -141,6 +141,13 @@ const char* toString(InferenceId i)
case InferenceId::STRINGS_REDUCTION: return "REDUCTION";
case InferenceId::STRINGS_PREFIX_CONFLICT: return "PREFIX_CONFLICT";
+ case InferenceId::UF_HO_APP_ENCODE: return "UF_HO_APP_ENCODE";
+ case InferenceId::UF_HO_APP_CONV_SKOLEM: return "UF_HO_APP_CONV_SKOLEM";
+ case InferenceId::UF_HO_EXTENSIONALITY: return "UF_HO_EXTENSIONALITY";
+ case InferenceId::UF_HO_MODEL_APP_ENCODE: return "UF_HO_MODEL_APP_ENCODE";
+ case InferenceId::UF_HO_MODEL_EXTENSIONALITY:
+ return "UF_HO_MODEL_EXTENSIONALITY";
+
default: return "?";
}
}
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index f28faa037..a48a8c366 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -404,7 +404,40 @@ enum class InferenceId
STRINGS_PREFIX_CONFLICT,
//-------------------------------------- end prefix conflict
- UNKNOWN,
+ // Clause from the uf symmetry breaker
+ UF_BREAK_SYMMETRY,
+ UF_CARD_CLIQUE,
+ UF_CARD_COMBINED,
+ UF_CARD_ENFORCE_NEGATIVE,
+ UF_CARD_EQUIV,
+ UF_CARD_MONOTONE_COMBINED,
+ UF_CARD_SIMPLE_CONFLICT,
+ UF_CARD_SPLIT,
+ //-------------------------------------- begin HO extension to UF
+ // Encodes an n-ary application as a chain of binary HO_APPLY applications
+ // (= (f t1 ... tn) (@ (@ ... (@ f t1) ...) tn))
+ UF_HO_APP_ENCODE,
+ UF_HO_APP_CONV_SKOLEM,
+ // Adds an extensionality lemma to witness that disequal functions have
+ // different applications
+ // (not (= (f sk1 .. skn) (g sk1 .. skn))
+ UF_HO_EXTENSIONALITY,
+ //-------------------------------------- begin model-construction specific part
+ // These rules are necessary to ensure that we build models properly. For more
+ // details see Section 3.3 of Barbosa et al. CADE'19.
+ //
+ // Enforces that a regular APPLY_UF term in the model is equal to its HO_APPLY
+ // equivalent by adding the equality as a lemma
+ // (= (f t1 ... tn) (@ (@ ... (@ f t1) ...) tn))
+ UF_HO_MODEL_APP_ENCODE,
+ // Adds an extensionality lemma to witness that disequal functions have
+ // different applications
+ // (not (= (f sk1 .. skn) (g sk1 .. skn))
+ UF_HO_MODEL_EXTENSIONALITY,
+ //-------------------------------------- end model-construction specific part
+ //-------------------------------------- end HO extension to UF
+
+ UNKNOWN
};
/**
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 697a828a4..861da3558 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -1037,7 +1037,7 @@ int SortModel::addSplit(Region* r)
//split on the equality s
Node lem = NodeManager::currentNM()->mkNode( kind::OR, ss, ss.negate() );
// send lemma, with caching
- if (d_im.lemma(lem, InferenceId::UNKNOWN))
+ if (d_im.lemma(lem, InferenceId::UF_CARD_SPLIT))
{
Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
//tell the sat solver to explore the equals branch first
@@ -1070,7 +1070,7 @@ void SortModel::addCliqueLemma(std::vector<Node>& clique)
eqs.push_back(d_cardinality_literal[d_cardinality].notNode());
Node lem = NodeManager::currentNM()->mkNode(OR, eqs);
// send lemma, with caching
- if (d_im.lemma(lem, InferenceId::UNKNOWN))
+ if (d_im.lemma(lem, InferenceId::UF_CARD_CLIQUE))
{
Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl;
++(d_thss->d_statistics.d_clique_lemmas);
@@ -1082,7 +1082,7 @@ void SortModel::simpleCheckCardinality() {
Node lem = NodeManager::currentNM()->mkNode( AND, getCardinalityLiteral( d_cardinality.get() ),
getCardinalityLiteral( d_maxNegCard.get() ).negate() );
Trace("uf-ss-lemma") << "*** Simple cardinality conflict : " << lem << std::endl;
- d_im.conflict(lem, InferenceId::UNKNOWN);
+ d_im.conflict(lem, InferenceId::UF_CARD_SIMPLE_CONFLICT);
}
}
@@ -1179,7 +1179,7 @@ bool SortModel::checkLastCall()
Node lem = NodeManager::currentNM()->mkNode(
OR, cl, NodeManager::currentNM()->mkAnd(force_cl));
Trace("uf-ss-lemma") << "*** Enforce negative cardinality constraint lemma : " << lem << std::endl;
- d_im.lemma(lem, InferenceId::UNKNOWN, LemmaProperty::NONE, false);
+ d_im.lemma(lem, InferenceId::UF_CARD_ENFORCE_NEGATIVE, LemmaProperty::NONE, false);
return false;
}
}
@@ -1399,7 +1399,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
Node eqv_lit = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, ct, lit[1] );
eqv_lit = lit.eqNode( eqv_lit );
Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit << std::endl;
- d_im.lemma(eqv_lit, InferenceId::UNKNOWN, LemmaProperty::NONE, false);
+ d_im.lemma(eqv_lit, InferenceId::UF_CARD_EQUIV, LemmaProperty::NONE, false);
d_card_assertions_eqv_lemma[lit] = true;
}
}
@@ -1528,7 +1528,7 @@ void CardinalityExtension::check(Theory::Effort level)
Node eq = Rewriter::rewrite( a.eqNode( b ) );
Node lem = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
Trace("uf-ss-lemma") << "*** Split (no-minimal) : " << lem << std::endl;
- d_im.lemma(lem, InferenceId::UNKNOWN, LemmaProperty::NONE, false);
+ d_im.lemma(lem, InferenceId::UF_CARD_SPLIT, LemmaProperty::NONE, false);
d_im.requirePhase(eq, true);
type_proc[tn] = true;
break;
@@ -1707,7 +1707,7 @@ void CardinalityExtension::checkCombinedCardinality()
<< " : " << cf << std::endl;
Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict"
<< " : " << cf << std::endl;
- d_im.conflict(cf, InferenceId::UNKNOWN);
+ d_im.conflict(cf, InferenceId::UF_CARD_MONOTONE_COMBINED);
return;
}
}
@@ -1745,7 +1745,7 @@ void CardinalityExtension::checkCombinedCardinality()
<< std::endl;
Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf
<< std::endl;
- d_im.conflict(cf, InferenceId::UNKNOWN);
+ d_im.conflict(cf, InferenceId::UF_CARD_COMBINED);
}
}
}
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index 55e2500af..a9e48d7ca 100644
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -107,7 +107,7 @@ unsigned HoExtension::applyExtensionality(TNode deq)
Node lem = NodeManager::currentNM()->mkNode(OR, deq[0], conc);
Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem
<< std::endl;
- d_im.lemma(lem, InferenceId::UNKNOWN);
+ d_im.lemma(lem, InferenceId::UF_HO_EXTENSIONALITY);
return 1;
}
return 0;
@@ -167,7 +167,7 @@ Node HoExtension::getApplyUfForHoApply(Node node)
Trace("uf-ho-lemma")
<< "uf-ho-lemma : Skolem definition for apply-conversion : " << lem
<< std::endl;
- d_im.lemma(lem, InferenceId::UNKNOWN);
+ d_im.lemma(lem, InferenceId::UF_HO_APP_CONV_SKOLEM);
d_uf_std_skolem[f] = new_f;
}
else
@@ -256,7 +256,7 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m)
Node lem = nm->mkNode(OR, deq.negate(), eq);
Trace("uf-ho") << "HoExtension: cmi extensionality lemma " << lem
<< std::endl;
- d_im.lemma(lem, InferenceId::UNKNOWN);
+ d_im.lemma(lem, InferenceId::UF_HO_MODEL_EXTENSIONALITY);
return 1;
}
}
@@ -284,7 +284,12 @@ unsigned HoExtension::applyAppCompletion(TNode n)
Node eq = n.eqNode(ret);
Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq
<< std::endl;
- d_im.assertInternalFact(eq, true, InferenceId::UNKNOWN, PfRule::HO_APP_ENCODE, {}, {n});
+ d_im.assertInternalFact(eq,
+ true,
+ InferenceId::UF_HO_APP_ENCODE,
+ PfRule::HO_APP_ENCODE,
+ {},
+ {n});
return 1;
}
Trace("uf-ho-debug") << " ...already have " << ret << " == " << n << "."
@@ -441,7 +446,7 @@ bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m)
Node eq = n.eqNode(hn);
Trace("uf-ho") << "HoExtension: cmi app completion lemma " << eq
<< std::endl;
- d_im.lemma(eq, InferenceId::UNKNOWN);
+ d_im.lemma(eq, InferenceId::UF_HO_MODEL_APP_ENCODE);
return false;
}
}
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index c8cfe295e..3ad94c571 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -315,7 +315,7 @@ void TheoryUF::presolve() {
++i) {
Debug("uf") << "uf: generating a lemma: " << *i << std::endl;
// no proof generator provided
- d_im.lemma(*i, InferenceId::UNKNOWN);
+ d_im.lemma(*i, InferenceId::UF_BREAK_SYMMETRY);
}
}
if( d_thss ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback