From: Andrew Reynolds Date: Mon, 14 May 2018 15:29:08 +0000 (-0500) Subject: Flag to check invariance of entire values in sygus explain (#1908) X-Git-Tag: cvc5-1.0.0~5058 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=33420e77e9f7ee7a429708db3a7f6c28aef7d0ec;p=cvc5.git Flag to check invariance of entire values in sygus explain (#1908) --- 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& vs, std::vector msu; std::vector mexp; msu.insert(msu.end(), ms.begin(), ms.end()); + std::map var_count; for (unsigned k = 0; k < vs.size(); k++) { vsit.setUpdatedTerm(msu[k]); @@ -249,8 +250,13 @@ void Cegis::getRefinementEvalLemmas(const std::vector& 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 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& exp, - SygusInvarianceTest& et) + SygusInvarianceTest& et, + bool strict) { - int sz = -1; std::map var_count; + getExplanationFor(n, vn, exp, et, var_count, strict); +} + +void SygusExplain::getExplanationFor(Node n, + Node vn, + std::vector& exp, + SygusInvarianceTest& et, + std::map& 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& exp, - SygusInvarianceTest& et); + SygusInvarianceTest& et, + bool strict = true); + void getExplanationFor(Node n, + Node vn, + std::vector& exp, + SygusInvarianceTest& et, + std::map& 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 diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 52eb63789..5cb24d072 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1475,6 +1475,7 @@ REG1_TESTS = \ regress1/sygus/commutative.sy \ regress1/sygus/constant.sy \ regress1/sygus/constant-ite-bv.sy \ + regress1/sygus/crci-ssb-unk.sy \ regress1/sygus/dt-test-ns.sy \ regress1/sygus/dup-op.sy \ regress1/sygus/fg_polynomial3.sy \ @@ -1598,7 +1599,9 @@ REG2_TESTS = \ regress2/sygus/process-10-vars-2fun.sy \ regress2/sygus/process-arg-invariance.sy \ regress2/sygus/real-grammar-neg.sy \ + regress2/sygus/sixfuncs.sy \ regress2/sygus/three.sy \ + regress2/sygus/vcb.sy \ regress2/typed_v1l50016-simp.cvc \ regress2/uflia-error0.smt2 \ regress2/xs-09-16-3-4-1-5.decn.smt \ diff --git a/test/regress/regress1/sygus/crci-ssb-unk.sy b/test/regress/regress1/sygus/crci-ssb-unk.sy new file mode 100644 index 000000000..f2b28db9c --- /dev/null +++ b/test/regress/regress1/sygus/crci-ssb-unk.sy @@ -0,0 +1,43 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic BV) + + +(define-fun origCir ( (LN4 Bool) (LN91 Bool) ) Bool + (and LN91 LN4 ) +) + + +(synth-fun skel ( (LN4 Bool) (LN91 Bool) ) Bool + ((Start Bool ( + (and depth1 depth1) + (xor depth1 depth1) + )) + (depth1 Bool ( + (not depth2) + LN91 + )) + (depth2 Bool ( + (and depth3 depth3) + (not depth3) + (or depth3 depth3) + )) + (depth3 Bool ( + (and depth4 depth4) + (not depth4) + (or depth4 depth4) + (xor depth4 depth4) + )) + (depth4 Bool ( + LN4 + ))) +) + + +(declare-var LN4 Bool) +(declare-var LN91 Bool) + +(constraint (= (origCir LN4 LN91 ) (skel LN4 LN91 ))) + +(check-synth) diff --git a/test/regress/regress2/sygus/sixfuncs.sy b/test/regress/regress2/sygus/sixfuncs.sy new file mode 100644 index 000000000..5280ffb20 --- /dev/null +++ b/test/regress/regress2/sygus/sixfuncs.sy @@ -0,0 +1,81 @@ +(set-logic LIA) + +(synth-fun f1 ((p1 Int) (P1 Int)) Int + ((Start Int ( + p1 + P1 + (- Start Start) + (+ Start Start) + ) + ))) + +(synth-fun f2 ((p1 Int) (P1 Int)) Int + ((Start Int ( + p1 + P1 + (+ Start Start) + ) + ))) + +(synth-fun f3 ((p1 Int) (P1 Int)) Int + ((Start Int ( + p1 + P1 + (- Start Start) + (+ Start Start) + ) + ))) + +(synth-fun f4 ((p1 Int) (P1 Int)) Int + ((Start Int ( + p1 + P1 + (- Start Start) + (+ Start Start) + ) + ))) + +(synth-fun f5 ((p1 Int) (P1 Int)) Int + ((Start Int ( + p1 + P1 + (- Start Start) + (+ Start Start) + ) + ))) + +(synth-fun g1 ((p1 Int) (P1 Int)) Int + ((Start Int ( + p1 + P1 + (- Start Start) + (+ Start Start) + ) + ))) + + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (+ (f1 x y) (f1 x y)) (f2 x y))) +(constraint (= (- (+ (f1 x y) (f2 x y)) y) (f3 x y))) +(constraint (= (+ (f2 x y) (f2 x y)) (f4 x y))) +(constraint (= (+ (f4 x y) (f1 x y)) (f5 x y))) + +(constraint (= (- (f1 x y) y) (g1 x y))) + + +(check-synth) + +;; possible solution +;; f1: y+x+1 +;; f2: y+2x+2 +;; f3: y+3x+3 +;; f4: 4y+4x+4 +;; f5: 5y+5x+5 +;; g1: x+1 +;; g2: y+2 +;; g3: y+3 +;; g4: 2y+6 +;; g5: 3y+x+7 + diff --git a/test/regress/regress2/sygus/vcb.sy b/test/regress/regress2/sygus/vcb.sy new file mode 100644 index 000000000..9cc2389f3 --- /dev/null +++ b/test/regress/regress2/sygus/vcb.sy @@ -0,0 +1,54 @@ +(set-logic LIA) + +(synth-fun f1 ((x1 Int) (x2 Int)) Int) + +(synth-fun f2 ((x1 Int) (x2 Int)) Int) + +(define-fun vmin () Int 1) +(define-fun vmax () Int 2) + +(define-fun AllZero ((v1 Int) (v2 Int)) Bool + (and (= v1 0) (= v2 0))) + +(define-fun InV ((v1 Int) (v2 Int)) Bool + (and (and (and (>= v1 vmin) (<= v1 vmax)) (>= v2 vmin)) (<= v2 vmax))) + +(define-fun InVorZero ((v1 Int) (v2 Int)) Bool + (or (InV v1 v2) (AllZero v1 v2))) + +(define-fun UnsafeSame ((x1 Int) (x2 Int) (v1 Int) (v2 Int)) Bool + (or (and (>= x1 x2) (>= (+ x2 v2) (+ x1 v1))) + (and (>= x2 x1) (>= (+ x1 v1) (+ x2 v2))))) + +(define-fun BadSame ((x1 Int) (x2 Int)) Bool + (= x1 x2)) + +(define-fun Bad ((x1 Int) (x2 Int)) Bool + (BadSame x1 x2)) + +(define-fun Unsafe ((x1 Int) (x2 Int) (v1 Int) (v2 Int)) Bool + (UnsafeSame x1 x2 v1 v2)) + + +(declare-var x1 Int) +(declare-var x2 Int) +(declare-var v1 Int) +(declare-var v2 Int) + +(constraint (InVorZero (f1 x1 x2) (f2 x1 x2))) + +(constraint (or (or (not (InV v1 v2)) + (AllZero (f1 x1 x2) (f2 x1 x2))) + (and (not (Unsafe x1 x2 (f1 x1 x2) (f2 x1 x2))) + (not (AllZero (f1 (+ x1 (f1 x1 x2)) (+ x2 (f2 x1 x2))) + (f2 (+ x1 (f1 x1 x2)) (+ x2 (f2 x1 x2)))))))) + +(constraint (or (or (or (not (InV v1 v2)) + (Unsafe x1 x2 v1 v2)) + (AllZero (f1 (+ x1 v1) (+ x2 v2)) (f2 (+ x1 v1) (+ x2 v2)))) + (not (AllZero (f1 x1 x2) (f2 x1 x2))))) + + +(constraint (or (Bad x1 x2) (not (AllZero (f1 x1 x2) (f2 x1 x2))))) + +(check-synth) \ No newline at end of file