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]);
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())
{
}
else
{
+ // revert
trb.replaceChild(i, vn[i]);
}
}
// 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);
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;
* - (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,
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 */
}
}
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;
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
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 \
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 \
--- /dev/null
+; 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)
--- /dev/null
+(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
+
--- /dev/null
+(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
projects / cvc5.git / commitdiff