summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/skolem_manager.cpp6
-rw-r--r--src/expr/skolem_manager.h14
-rw-r--r--src/theory/datatypes/infer_proof_cons.cpp6
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp22
-rw-r--r--src/theory/datatypes/theory_datatypes.h4
-rw-r--r--src/theory/strings/skolem_cache.cpp7
-rw-r--r--src/theory/strings/skolem_cache.h2
-rw-r--r--src/theory/strings/theory_strings.cpp3
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp2
9 files changed, 33 insertions, 33 deletions
diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index 1d66cbee2..773159b09 100644
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -50,6 +50,8 @@ const char* toString(SkolemFunId id)
case SkolemFunId::INT_DIV_BY_ZERO: return "INT_DIV_BY_ZERO";
case SkolemFunId::MOD_BY_ZERO: return "MOD_BY_ZERO";
case SkolemFunId::SQRT: return "SQRT";
+ case SkolemFunId::SELECTOR_WRONG: return "SELECTOR_WRONG";
+ case SkolemFunId::SEQ_NTH_OOB: return "SEQ_NTH_OOB";
default: return "?";
}
}
@@ -190,8 +192,8 @@ Node SkolemManager::mkPurifySkolem(Node t,
Node SkolemManager::mkSkolemFunction(SkolemFunId id, TypeNode tn, Node cacheVal)
{
- std::pair<SkolemFunId, Node> key(id, cacheVal);
- std::map<std::pair<SkolemFunId, Node>, Node>::iterator it =
+ std::tuple<SkolemFunId, TypeNode, Node> key(id, tn, cacheVal);
+ std::map<std::tuple<SkolemFunId, TypeNode, Node>, Node>::iterator it =
d_skolemFuns.find(key);
if (it == d_skolemFuns.end())
{
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 426202b7e..dd228e598 100644
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -29,14 +29,18 @@ class ProofGenerator;
/** Skolem function identifier */
enum class SkolemFunId
{
- /* an uninterpreted function f s.t. f(x) = x / 0.0 (real division) */
+ /** an uninterpreted function f s.t. f(x) = x / 0.0 (real division) */
DIV_BY_ZERO,
- /* an uninterpreted function f s.t. f(x) = x / 0 (integer division) */
+ /** an uninterpreted function f s.t. f(x) = x / 0 (integer division) */
INT_DIV_BY_ZERO,
- /* an uninterpreted function f s.t. f(x) = x mod 0 */
+ /** an uninterpreted function f s.t. f(x) = x mod 0 */
MOD_BY_ZERO,
- /* an uninterpreted function f s.t. f(x) = sqrt(x) */
+ /** an uninterpreted function f s.t. f(x) = sqrt(x) */
SQRT,
+ /** a wrongly applied selector */
+ SELECTOR_WRONG,
+ /** an application of seq.nth that is out of bounds */
+ SEQ_NTH_OOB,
};
/** Converts a skolem function name to a string. */
const char* toString(SkolemFunId id);
@@ -283,7 +287,7 @@ class SkolemManager
/**
* Cached of skolem functions for mkSkolemFunction above.
*/
- std::map<std::pair<SkolemFunId, Node>, Node> d_skolemFuns;
+ std::map<std::tuple<SkolemFunId, TypeNode, Node>, Node> d_skolemFuns;
/**
* Mapping from witness terms to proof generators.
*/
diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
index 9d3532368..5ab8a563f 100644
--- a/src/theory/datatypes/infer_proof_cons.cpp
+++ b/src/theory/datatypes/infer_proof_cons.cpp
@@ -222,6 +222,12 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
success = true;
}
break;
+ case InferenceId::DATATYPES_PURIFY:
+ {
+ cdp->addStep(conc, PfRule::MACRO_SR_PRED_INTRO, {}, {});
+ success = true;
+ }
+ break;
// inferences currently not supported
case InferenceId::DATATYPES_LABEL_EXH:
case InferenceId::DATATYPES_BISIMILAR:
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 60fd87731..01ef77172 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -523,9 +523,11 @@ TrustNode TheoryDatatypes::expandDefinition(Node n)
{
ret = sel;
}else{
- mkExpDefSkolem(selector, ndt, n.getType());
- Node sk =
- nm->mkNode(kind::APPLY_UF, d_exp_def_skolem[ndt][selector], n[0]);
+ SkolemManager* sm = nm->getSkolemManager();
+ TypeNode tnw = nm->mkFunctionType(ndt, n.getType());
+ Node f =
+ sm->mkSkolemFunction(SkolemFunId::SELECTOR_WRONG, tnw, selector);
+ Node sk = nm->mkNode(kind::APPLY_UF, f, n[0]);
if (tst == nm->mkConst(false))
{
ret = sk;
@@ -835,17 +837,6 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >
}
}
-void TheoryDatatypes::mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt ) {
- if( d_exp_def_skolem[dt].find( sel )==d_exp_def_skolem[dt].end() ){
- NodeManager* nm = NodeManager::currentNM();
- SkolemManager* sm = nm->getSkolemManager();
- std::stringstream ss;
- ss << sel << "_uf";
- d_exp_def_skolem[dt][sel] =
- sm->mkDummySkolem(ss.str().c_str(), nm->mkFunctionType(dt, rt));
- }
-}
-
Node TheoryDatatypes::getTermSkolemFor( Node n ) {
if( n.getKind()==APPLY_CONSTRUCTOR ){
NodeMap::const_iterator it = d_term_sk.find( n );
@@ -853,8 +844,7 @@ Node TheoryDatatypes::getTermSkolemFor( Node n ) {
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
//add purification unit lemma ( k = n )
- Node k =
- sm->mkDummySkolem("k", n.getType(), "reference skolem for datatypes");
+ Node k = sm->mkPurifySkolem(n, "kdt");
d_term_sk[n] = k;
Node eq = k.eqNode( n );
Trace("datatypes-infer") << "DtInfer : ref : " << eq << std::endl;
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 7997b9429..5617682ef 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -96,8 +96,6 @@ private:
bool hasTester( Node n );
/** get the possible constructors for n */
void getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& cons );
- /** mkExpDefSkolem */
- void mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt );
/** skolems for terms */
NodeMap d_term_sk;
Node getTermSkolemFor( Node n );
@@ -153,8 +151,6 @@ private:
context::CDList<TNode> d_functionTerms;
/** counter for forcing assignments (ensures fairness) */
unsigned d_dtfCounter;
- /** expand definition skolem functions */
- std::map< TypeNode, std::map< Node, Node > > d_exp_def_skolem;
/** uninterpreted constant to variable map */
std::map< Node, Node > d_uc_to_fresh_var;
private:
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index f68d7805b..eb2df1285 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -141,15 +141,18 @@ Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
Node SkolemCache::mkSkolemSeqNth(TypeNode seqType, const char* c)
{
+ // Note this method is static and does not rely on any local caching.
+ // It is used by expand definitions and by (dynamic) reductions, thus
+ // it is centrally located here.
Assert(seqType.isSequence());
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
std::vector<TypeNode> argTypes;
argTypes.push_back(seqType);
argTypes.push_back(nm->integerType());
TypeNode elemType = seqType.getSequenceElementType();
TypeNode ufType = nm->mkFunctionType(argTypes, elemType);
- return mkTypedSkolemCached(
- ufType, Node::null(), Node::null(), SkolemCache::SK_NTH, c);
+ return sm->mkSkolemFunction(SkolemFunId::SEQ_NTH_OOB, ufType);
}
Node SkolemCache::mkSkolem(const char* c)
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index 1006a758c..d64e4d5ae 100644
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -164,7 +164,7 @@ class SkolemCache
* Specific version for seq.nth, used for cases where the index is out of
* range for sequence type seqType.
*/
- Node mkSkolemSeqNth(TypeNode seqType, const char* c);
+ static Node mkSkolemSeqNth(TypeNode seqType, const char* c);
/** Returns a (uncached) skolem of type string with name c */
Node mkSkolem(const char* c);
/** Returns true if n is a skolem allocated by this class */
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index ea0fc5ea8..0ed003cc7 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -560,7 +560,6 @@ TrustNode TheoryStrings::expandDefinition(Node node)
if (node.getKind() == kind::SEQ_NTH)
{
NodeManager* nm = NodeManager::currentNM();
- SkolemCache* sc = d_termReg.getSkolemCache();
Node s = node[0];
Node n = node[1];
// seq.nth(s, n) --> ite(0 <= n < len(s), seq.nth_total(s,n), Uf(s, n))
@@ -568,7 +567,7 @@ TrustNode TheoryStrings::expandDefinition(Node node)
nm->mkNode(LEQ, d_zero, n),
nm->mkNode(LT, n, nm->mkNode(STRING_LENGTH, s)));
Node ss = nm->mkNode(SEQ_NTH_TOTAL, s, n);
- Node uf = sc->mkSkolemSeqNth(s.getType(), "Uf");
+ Node uf = SkolemCache::mkSkolemSeqNth(s.getType(), "Uf");
Node u = nm->mkNode(APPLY_UF, uf, s, n);
Node ret = nm->mkNode(ITE, cond, ss, u);
Trace("strings-exp-def") << "...return " << ret << std::endl;
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 1fd2bb519..5e6b27e1b 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -445,7 +445,7 @@ Node StringsPreprocess::reduce(Node t,
Node b1 = nm->mkNode(AND, b11, b12, b13);
// nodes for the case where `seq.nth` is undefined.
- Node uf = sc->mkSkolemSeqNth(s.getType(), "Uf");
+ Node uf = SkolemCache::mkSkolemSeqNth(s.getType(), "Uf");
Node b2 = nm->mkNode(EQUAL, skt, nm->mkNode(APPLY_UF, uf, s, n));
// the full ite, split on definedness of `seq.nth`
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback