summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.cpp45
-rw-r--r--src/theory/sets/theory_sets.cpp4
-rw-r--r--src/theory/sets/theory_sets.h2
-rw-r--r--src/theory/sets/theory_sets_private.cpp21
-rw-r--r--src/theory/sets/theory_sets_private.h32
-rw-r--r--src/theory/theory.h6
-rw-r--r--test/regress/regress0/fmf/quant_real_univ.cvc1
-rw-r--r--test/regress/regress0/rels/joinImg_0.cvc1
-rw-r--r--test/regress/regress0/rels/joinImg_0_1.cvc1
-rw-r--r--test/regress/regress0/rels/joinImg_1.cvc1
-rw-r--r--test/regress/regress0/rels/joinImg_1_1.cvc1
-rw-r--r--test/regress/regress0/rels/joinImg_2.cvc1
-rw-r--r--test/regress/regress0/rels/joinImg_2_1.cvc3
-rw-r--r--test/regress/regress0/sets/Makefile.am4
-rw-r--r--test/regress/regress0/sets/arjun-set-univ.cvc8
-rw-r--r--test/regress/regress0/sets/univ-set-uf-elim.smt216
16 files changed, 112 insertions, 35 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f360ae2fd..b2f7d6ccc 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2277,8 +2277,8 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
if(!childrenPushed) {
Kind k = n.getKind();
- // Apart from apply, we can short circuit leaves
- if(k != kind::APPLY && n.getNumChildren() == 0) {
+ // we can short circuit (variable) leaves
+ if(n.isVar()) {
SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(n);
if(i != d_smt.d_definedFunctions->end()) {
// replacement must be closed
@@ -2372,15 +2372,6 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
node = t->expandDefinition(req, n);
}
- // there should be children here, otherwise we short-circuited a result-push/continue, above
- if (node.getNumChildren() == 0) {
- Debug("expand") << "Unexpectedly no children..." << node << endl;
- }
- // This invariant holds at the moment but it is concievable that a new theory
- // might introduce a kind which can have children before definition expansion but doesn't
- // afterwards. If this happens, remove this assertion.
- Assert(node.getNumChildren() > 0);
-
// the partial functions can fall through, in which case we still
// consider their children
worklist.push(make_triple(Node(n), node, true)); // Original and rewritten result
@@ -2394,22 +2385,24 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
// Reconstruct the node from it's (now rewritten) children on the stack
Debug("expand") << "cons : " << node << endl;
- //cout << "cons : " << node << endl;
- NodeBuilder<> nb(node.getKind());
- if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
- Debug("expand") << "op : " << node.getOperator() << endl;
- //cout << "op : " << node.getOperator() << endl;
- nb << node.getOperator();
- }
- for(size_t i = 0; i < node.getNumChildren(); ++i) {
- Assert(!result.empty());
- Node expanded = result.top();
- result.pop();
- //cout << "exchld : " << expanded << endl;
- Debug("expand") << "exchld : " << expanded << endl;
- nb << expanded;
+ if(node.getNumChildren()>0) {
+ //cout << "cons : " << node << endl;
+ NodeBuilder<> nb(node.getKind());
+ if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ Debug("expand") << "op : " << node.getOperator() << endl;
+ //cout << "op : " << node.getOperator() << endl;
+ nb << node.getOperator();
+ }
+ for(size_t i = 0; i < node.getNumChildren(); ++i) {
+ Assert(!result.empty());
+ Node expanded = result.top();
+ result.pop();
+ //cout << "exchld : " << expanded << endl;
+ Debug("expand") << "exchld : " << expanded << endl;
+ nb << expanded;
+ }
+ node = nb;
}
- node = nb;
cache[n] = n == node ? Node::null() : node; // Only cache once all subterms are expanded
result.push(node);
}
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 4992f654f..263d61934 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -74,6 +74,10 @@ void TheorySets::preRegisterTerm(TNode node) {
d_internal->preRegisterTerm(node);
}
+Node TheorySets::expandDefinition(LogicRequest &logicRequest, Node n) {
+ return d_internal->expandDefinition(logicRequest, n);
+}
+
Theory::PPAssertStatus TheorySets::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
return d_internal->ppAssert( in, outSubstitutions );
}
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index bbc6ae0c4..3ecd404bb 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -66,6 +66,8 @@ public:
void preRegisterTerm(TNode node);
+ Node expandDefinition(LogicRequest &logicRequest, Node n);
+
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
void presolve();
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index a2a56e137..3013711eb 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -604,13 +604,8 @@ void TheorySetsPrivate::fullEffortCheck(){
}else if( n.getKind()==kind::EMPTYSET ){
d_eqc_emptyset[tnn] = eqc;
}else if( n.getKind()==kind::UNIVERSE_SET ){
- if( options::setsExt() ){
- d_eqc_univset[tnn] = eqc;
- }else{
- std::stringstream ss;
- ss << "Symbols complement and universe set are not supported in default mode, try --sets-ext." << std::endl;
- throw LogicException(ss.str());
- }
+ Assert( options::setsExt() );
+ d_eqc_univset[tnn] = eqc;
}else{
Node r1 = d_equalityEngine.getRepresentative( n[0] );
Node r2 = d_equalityEngine.getRepresentative( n[1] );
@@ -2155,8 +2150,20 @@ void TheorySetsPrivate::preRegisterTerm(TNode node)
}
}
+Node TheorySetsPrivate::expandDefinition(LogicRequest &logicRequest, Node n) {
+ Debug("sets-proc") << "expandDefinition : " << n << std::endl;
+ if( n.getKind()==kind::UNIVERSE_SET || n.getKind()==kind::COMPLEMENT || n.getKind()==kind::JOIN_IMAGE ){
+ if( !options::setsExt() ){
+ std::stringstream ss;
+ ss << "Extended set operators are not supported in default mode, try --sets-ext.";
+ throw LogicException(ss.str());
+ }
+ }
+ return n;
+}
Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
+ Debug("sets-proc") << "ppAssert : " << in << std::endl;
Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
//TODO: allow variable elimination for sets when setsExt = true
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 7bc17c927..175e82bb8 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -188,6 +188,38 @@ public:
void preRegisterTerm(TNode node);
+ /** expandDefinition
+ * If the sets-ext option is not set and we have an extended operator,
+ * we throw an exception. This function is a no-op otherwise.
+ *
+ * This is related to github issue #1076
+ * TheorySets uses expandDefinition as an entry point to see if the input
+ * contains extended operators.
+ *
+ * We need to be notified when a universe set occurs in our input,
+ * before preprocessing and simplification takes place. Otherwise the models
+ * may be inaccurate when setsExt is false, here is an example:
+ *
+ * x,y : (Set Int)
+ * x = (as univset (Set Int));
+ * 0 in y;
+ * check-sat;
+ *
+ * If setsExt is enabled, the model value of (as univset (Set Int)) is always accurate.
+ *
+ * If setsExt is not enabled, the following can happen for the above example:
+ * x = (as univset (Set Int)) is made into a model substitution during
+ * simplification. This means (as univset (Set Int)) is not a term in any assertion,
+ * and hence we do not throw an exception, nor do we infer that 0 is a member of
+ * (as univset (Set Int)). We instead report a model where x = {}. The correct behavior
+ * is to throw an exception that says universe set is not supported when setsExt disabled.
+ * Hence we check for the existence of universe set before simplification here.
+ *
+ * Another option to fix this is to make TheoryModel::getValue more general
+ * so that it makes theory-specific calls to evaluate interpreted symbols.
+ */
+ Node expandDefinition(LogicRequest &logicRequest, Node n);
+
Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
void presolve();
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 73102a6e2..1a72944ff 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -424,6 +424,12 @@ public:
* used, definitions should only be used when rewrites are not
* possible, for example in handling under-specified operations
* using partially defined functions.
+ *
+ * TODO (github issue #1076):
+ * some theories like sets use expandDefinition as a "context
+ * independent preRegisterTerm". This is required for cases where
+ * a theory wants to be notified about a term before preprocessing
+ * and simplification but doesn't necessarily want to rewrite it.
*/
virtual Node expandDefinition(LogicRequest &logicRequest, Node node) {
// by default, do nothing
diff --git a/test/regress/regress0/fmf/quant_real_univ.cvc b/test/regress/regress0/fmf/quant_real_univ.cvc
index c3cefd767..c3dbb2cd6 100644
--- a/test/regress/regress0/fmf/quant_real_univ.cvc
+++ b/test/regress/regress0/fmf/quant_real_univ.cvc
@@ -1,5 +1,6 @@
% EXPECT: sat
OPTION "fmf-bound";
+OPTION "sets-ext";
Atom : TYPE;
REAL_UNIVERSE : SET OF [REAL];
ATOM_UNIVERSE : SET OF [Atom];
diff --git a/test/regress/regress0/rels/joinImg_0.cvc b/test/regress/regress0/rels/joinImg_0.cvc
index e36c6a647..297898a81 100644
--- a/test/regress/regress0/rels/joinImg_0.cvc
+++ b/test/regress/regress0/rels/joinImg_0.cvc
@@ -1,5 +1,6 @@
% EXPECT: unsat
OPTION "logic" "ALL_SUPPORTED";
+OPTION "sets-ext";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
diff --git a/test/regress/regress0/rels/joinImg_0_1.cvc b/test/regress/regress0/rels/joinImg_0_1.cvc
index 602c4fe3f..4e69394bd 100644
--- a/test/regress/regress0/rels/joinImg_0_1.cvc
+++ b/test/regress/regress0/rels/joinImg_0_1.cvc
@@ -1,5 +1,6 @@
% EXPECT: sat
OPTION "logic" "ALL_SUPPORTED";
+OPTION "sets-ext";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
diff --git a/test/regress/regress0/rels/joinImg_1.cvc b/test/regress/regress0/rels/joinImg_1.cvc
index 47e57c1fb..81f208fc4 100644
--- a/test/regress/regress0/rels/joinImg_1.cvc
+++ b/test/regress/regress0/rels/joinImg_1.cvc
@@ -1,5 +1,6 @@
% EXPECT: unsat
OPTION "logic" "ALL_SUPPORTED";
+OPTION "sets-ext";
Atom: TYPE;
x : SET OF [Atom, Atom];
y : SET OF [Atom, Atom];
diff --git a/test/regress/regress0/rels/joinImg_1_1.cvc b/test/regress/regress0/rels/joinImg_1_1.cvc
index a7927f7e2..003770a1b 100644
--- a/test/regress/regress0/rels/joinImg_1_1.cvc
+++ b/test/regress/regress0/rels/joinImg_1_1.cvc
@@ -1,5 +1,6 @@
% EXPECT: sat
OPTION "logic" "ALL_SUPPORTED";
+OPTION "sets-ext";
Atom: TYPE;
x : SET OF [Atom, Atom];
y : SET OF [Atom, Atom];
diff --git a/test/regress/regress0/rels/joinImg_2.cvc b/test/regress/regress0/rels/joinImg_2.cvc
index bbf57629b..a4acfe6c6 100644
--- a/test/regress/regress0/rels/joinImg_2.cvc
+++ b/test/regress/regress0/rels/joinImg_2.cvc
@@ -1,5 +1,6 @@
% EXPECT: unsat
OPTION "logic" "ALL_SUPPORTED";
+OPTION "sets-ext";
Atom: TYPE;
x : SET OF [Atom, Atom];
y : SET OF [Atom, Atom];
diff --git a/test/regress/regress0/rels/joinImg_2_1.cvc b/test/regress/regress0/rels/joinImg_2_1.cvc
index b38bfab06..03f88be37 100644
--- a/test/regress/regress0/rels/joinImg_2_1.cvc
+++ b/test/regress/regress0/rels/joinImg_2_1.cvc
@@ -1,5 +1,6 @@
% EXPECT: sat
OPTION "logic" "ALL_SUPPORTED";
+OPTION "sets-ext";
Atom: TYPE;
x : SET OF [Atom, Atom];
y : SET OF [Atom, Atom];
@@ -21,4 +22,4 @@ ASSERT y = {(f, g), (b, c), (d, e), (c, e)};
ASSERT x = {(f, g), (b, c), (d, e), (c, e)};
ASSERT (NOT(a = b)) OR (NOT(a = f));
-CHECKSAT; \ No newline at end of file
+CHECKSAT;
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index c8e416a42..de2170768 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -86,7 +86,9 @@ TESTS = \
sets-poly-nonint.smt2 \
int-real-univ.smt2 \
int-real-univ-unsat.smt2 \
- sets-tuple-poly.cvc
+ sets-tuple-poly.cvc \
+ arjun-set-univ.cvc \
+ univ-set-uf-elim.smt2
EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/sets/arjun-set-univ.cvc b/test/regress/regress0/sets/arjun-set-univ.cvc
new file mode 100644
index 000000000..3c35a62a5
--- /dev/null
+++ b/test/regress/regress0/sets/arjun-set-univ.cvc
@@ -0,0 +1,8 @@
+% EXPECT: Extended set operators are not supported in default mode, try --sets-ext.
+% EXIT: 1
+OPTION "produce-models" true;
+x,y,z : SET OF BOOLEAN;
+ASSERT x = {TRUE};
+ASSERT y = {FALSE};
+CHECKSAT z = ~ y;
+COUNTERMODEL;
diff --git a/test/regress/regress0/sets/univ-set-uf-elim.smt2 b/test/regress/regress0/sets/univ-set-uf-elim.smt2
new file mode 100644
index 000000000..a22f2a44f
--- /dev/null
+++ b/test/regress/regress0/sets/univ-set-uf-elim.smt2
@@ -0,0 +1,16 @@
+; EXPECT: (error "Extended set operators are not supported in default mode, try --sets-ext.")
+; EXIT: 1
+(set-logic ALL)
+(declare-fun a () Int)
+(declare-fun f ((Set Bool)) Int)
+(declare-fun s () (Set Bool))
+
+(assert (member true s))
+(assert (member false s))
+(assert (= a (f (as univset (Set Bool)))))
+
+(assert (= (f (as emptyset (Set Bool))) 1))
+(assert (= (f (singleton true)) 2))
+(assert (= (f (singleton false)) 3))
+(assert (= (f (union (singleton true) (singleton false))) 4))
+(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback