diff options
-rw-r--r-- | src/smt/smt_engine.cpp | 45 | ||||
-rw-r--r-- | src/theory/sets/theory_sets.cpp | 4 | ||||
-rw-r--r-- | src/theory/sets/theory_sets.h | 2 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 21 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.h | 32 | ||||
-rw-r--r-- | src/theory/theory.h | 6 | ||||
-rw-r--r-- | test/regress/regress0/fmf/quant_real_univ.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_0.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_0_1.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_1.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_1_1.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_2.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_2_1.cvc | 3 | ||||
-rw-r--r-- | test/regress/regress0/sets/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/sets/arjun-set-univ.cvc | 8 | ||||
-rw-r--r-- | test/regress/regress0/sets/univ-set-uf-elim.smt2 | 16 |
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) |