diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-14 10:29:08 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-14 10:29:08 -0500 |
commit | 33420e77e9f7ee7a429708db3a7f6c28aef7d0ec (patch) | |
tree | de1d33cc21a9453caf0c0c1799b375d7ab53d5c9 /src/theory | |
parent | 53c73505c5aed92401cfe02b669abaf8e6a30e32 (diff) |
Flag to check invariance of entire values in sygus explain (#1908)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_explain.cpp | 29 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_explain.h | 18 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 39 |
4 files changed, 80 insertions, 16 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 92fea9586..e8d29835a 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -236,6 +236,7 @@ void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, std::vector<Node> msu; std::vector<Node> mexp; msu.insert(msu.end(), ms.begin(), ms.end()); + std::map<TypeNode, int> var_count; for (unsigned k = 0; k < vs.size(); k++) { vsit.setUpdatedTerm(msu[k]); @@ -249,8 +250,13 @@ void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, Trace("sygus-cref-eval2-debug") << " compute min explain of : " << vs[k] << " = " << ut << std::endl; - tds->getExplain()->getExplanationFor(vs[k], ut, mexp, vsit); - msu[k] = ut; + tds->getExplain()->getExplanationFor( + vs[k], ut, mexp, vsit, var_count, false); + Trace("sygus-cref-eval2-debug") + << "exp now: " << mexp << std::endl; + msu[k] = vsit.getUpdatedTerm(); + Trace("sygus-cref-eval2-debug") + << "updated term : " << msu[k] << std::endl; } if (!mexp.empty()) { diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp index f76edb1c3..2be6c9d91 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.cpp +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -205,6 +205,7 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb, } else { + // revert trb.replaceChild(i, vn[i]); } } @@ -273,7 +274,7 @@ void SygusExplain::getExplanationFor(Node n, // naive : // return getExplanationForEquality( n, vn, exp ); - // set up the recursion object + // set up the recursion object; std::map<TypeNode, int> var_count; TermRecBuild trb; trb.init(vn); @@ -292,10 +293,32 @@ void SygusExplain::getExplanationFor(Node n, void SygusExplain::getExplanationFor(Node n, Node vn, std::vector<Node>& exp, - SygusInvarianceTest& et) + SygusInvarianceTest& et, + bool strict) { - int sz = -1; std::map<TypeNode, int> var_count; + getExplanationFor(n, vn, exp, et, var_count, strict); +} + +void SygusExplain::getExplanationFor(Node n, + Node vn, + std::vector<Node>& exp, + SygusInvarianceTest& et, + std::map<TypeNode, int>& var_count, + bool strict) +{ + if (!strict) + { + // check if it is invariant over the entire node + TypeNode vtn = vn.getType(); + Node x = d_tdb->getFreeVarInc(vtn, var_count); + if (et.is_invariant(d_tdb, x, x)) + { + return; + } + var_count[vtn]--; + } + int sz = -1; TermRecBuild trb; trb.init(vn); Node vnr; diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h index 818f51438..056ea7ed5 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.h +++ b/src/theory/quantifiers/sygus/sygus_explain.h @@ -182,6 +182,15 @@ class SygusExplain * - (if applicable) exp => ( n != vnr ). * * This function updates sz to be the term size of [[exp]]_n. + * + * If strict is false, then we also test whether the invariance test holds + * independently of the entire value of vn. + * + * The argument var_count is used for tracking the variables that we introduce + * to generalize the shape of vn. This map is passed to + * TermDbSygus::getFreeVarInc. This argument should be used if we are + * calling this function multiple times and the generalization should not + * introduce variables that shadow the variables introduced on previous calls. */ void getExplanationFor(Node n, Node vn, @@ -192,7 +201,14 @@ class SygusExplain void getExplanationFor(Node n, Node vn, std::vector<Node>& exp, - SygusInvarianceTest& et); + SygusInvarianceTest& et, + bool strict = true); + void getExplanationFor(Node n, + Node vn, + std::vector<Node>& exp, + SygusInvarianceTest& et, + std::map<TypeNode, int>& var_count, + bool strict = true); private: /** sygus term database associated with this utility */ diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index c45d4971e..774ba2180 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -285,11 +285,15 @@ public: } } if( !d_req_type.isNull() ){ + Trace("sygus-sb-debug") << "- check if " << tn << " is type " + << d_req_type << std::endl; if( tn!=d_req_type ){ return false; } } if( d_req_kind!=UNDEFINED_KIND ){ + Trace("sygus-sb-debug") << "- check if " << tn << " has " << d_req_kind + << std::endl; int c = tdb->getKindConsNum( tn, d_req_kind ); if( c!=-1 ){ bool ret = true; @@ -327,22 +331,37 @@ bool TermDbSygus::considerArgKind( TypeNode tn, TypeNode tnp, Kind k, Kind pk, i const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); Assert( hasKind( tn, k ) ); Assert( hasKind( tnp, pk ) ); - Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk << ", arg = " << arg << "?" << std::endl; + Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk + << ", arg = " << arg << " in " << tnp << "?" + << std::endl; int c = getKindConsNum( tn, k ); int pc = getKindConsNum( tnp, pk ); - if( k==pk ){ //check for associativity - if( quantifiers::TermUtil::isAssoc( k ) ){ - //if the operator is associative, then a repeated occurrence should only occur in the leftmost argument position - int firstArg = getFirstArgOccurrence( pdt[pc], tn ); - Assert( firstArg!=-1 ); - if( arg!=firstArg ){ - Trace("sygus-sb-simple") << " sb-simple : do not consider " << k << " at child arg " << arg << " of " << k << " since it is associative, with first arg = " << firstArg << std::endl; - return false; - }else{ + if (k == pk && quantifiers::TermUtil::isAssoc(k)) + { + // if the operator is associative, then a repeated occurrence should only + // occur in the leftmost argument position + int firstArg = getFirstArgOccurrence(pdt[pc], tn); + Assert(firstArg != -1); + if (arg == firstArg) + { + return true; + } + // the argument types of the child must be the parent's type + for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++) + { + TypeNode tn = TypeNode::fromType(dt[c].getArgType(i)); + if (tn != tnp) + { return true; } } + Trace("sygus-sb-simple") + << " sb-simple : do not consider " << k << " at child arg " << arg + << " of " << k + << " since it is associative, with first arg = " << firstArg + << std::endl; + return false; } //describes the shape of an alternate term to construct // we check whether this term is in the sygus grammar below |