From: Andrew Reynolds Date: Wed, 27 Oct 2021 18:40:18 +0000 (-0500) Subject: Fix care graph computation for higher-order (#7474) X-Git-Tag: cvc5-1.0.0~954 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7461cd576c0ad4c19e996644157a63920c67649b;p=cvc5.git Fix care graph computation for higher-order (#7474) Since we apply a lazy schema for app completion, this may omit terms from the care graph that are relevant for theory combination. This corrects the care graph for UF when higher-order is enabled by considering the HO_APPLY version of all partially and fully applied prefixes of APPLY_UF terms during TheoryUF::computeCareGraph. Fixes #5741. Fixes #5744. Fixes #5201. Fixes #5078. Fixes #4758. --- diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 1e240a254..5e9cb0a1d 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -511,9 +511,8 @@ EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) { return EQUALITY_FALSE_IN_MODEL; } -bool TheoryUF::areCareDisequal(TNode x, TNode y){ - Assert(d_equalityEngine->hasTerm(x)); - Assert(d_equalityEngine->hasTerm(y)); +bool TheoryUF::areCareDisequal(TNode x, TNode y) +{ if (d_equalityEngine->isTriggerTerm(x, THEORY_UF) && d_equalityEngine->isTriggerTerm(y, THEORY_UF)) { @@ -534,11 +533,14 @@ void TheoryUF::addCarePairs(const TNodeTrie* t1, unsigned arity, unsigned depth) { + // Note we use d_state instead of d_equalityEngine in this method in several + // places to be robust to cases where the tries have terms that do not + // exist in the equality engine, which can be the case if higher order. if( depth==arity ){ if( t2!=NULL ){ Node f1 = t1->getData(); Node f2 = t2->getData(); - if (!d_equalityEngine->areEqual(f1, f2)) + if (!d_state.areEqual(f1, f2)) { Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl; vector< pair > currentPairs; @@ -546,11 +548,9 @@ void TheoryUF::addCarePairs(const TNodeTrie* t1, { TNode x = f1[k]; TNode y = f2[k]; - Assert(d_equalityEngine->hasTerm(x)); - Assert(d_equalityEngine->hasTerm(y)); - Assert(!d_equalityEngine->areDisequal(x, y, false)); + Assert(!d_state.areDisequal(x, y)); Assert(!areCareDisequal(x, y)); - if (!d_equalityEngine->areEqual(x, y)) + if (!d_state.areEqual(x, y)) { if (d_equalityEngine->isTriggerTerm(x, THEORY_UF) && d_equalityEngine->isTriggerTerm(y, THEORY_UF)) @@ -586,7 +586,7 @@ void TheoryUF::addCarePairs(const TNodeTrie* t1, std::map::const_iterator it2 = it; ++it2; for( ; it2 != t1->d_data.end(); ++it2 ){ - if (!d_equalityEngine->areDisequal(it->first, it2->first, false)) + if (!d_state.areDisequal(it->first, it2->first)) { if( !areCareDisequal(it->first, it2->first) ){ addCarePairs( &it->second, &it2->second, arity, depth+1 ); @@ -600,7 +600,7 @@ void TheoryUF::addCarePairs(const TNodeTrie* t1, { for (const std::pair& tt2 : t2->d_data) { - if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false)) + if (!d_state.areDisequal(tt1.first, tt2.first)) { if (!areCareDisequal(tt1.first, tt2.first)) { @@ -618,11 +618,14 @@ void TheoryUF::computeCareGraph() { { return; } + NodeManager* nm = NodeManager::currentNM(); // Use term indexing. We build separate indices for APPLY_UF and HO_APPLY. // We maintain indices per operator for the former, and indices per // function type for the latter. Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..." << std::endl; + // temporary keep set for higher-order indexing below + std::vector keep; std::map index; std::map hoIndex; std::map arity; @@ -645,6 +648,25 @@ void TheoryUF::computeCareGraph() { Node op = app.getOperator(); index[op].addTerm(app, reps); arity[op] = reps.size(); + if (logicInfo().isHigherOrder() && d_equalityEngine->hasTerm(op)) + { + // Since we use a lazy app-completion scheme for equating fully + // and partially applied versions of terms, we must add all + // sub-chains to the HO index if the operator of this term occurs + // in a higher-order context in the equality engine. In other words, + // for (f a b c), this will add the terms: + // (HO_APPLY f a), (HO_APPLY (HO_APPLY f a) b), + // (HO_APPLY (HO_APPLY (HO_APPLY f a) b) c) to the higher-order + // term index for consideration when computing care pairs. + Node curr = op; + for (const Node& c : app) + { + Node happ = nm->mkNode(kind::HO_APPLY, curr, c); + hoIndex[curr.getType()].addTerm(happ, {curr, c}); + curr = happ; + keep.push_back(happ); + } + } } else { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 52fb41d46..197c22196 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -651,12 +651,16 @@ set(regress_0_tests regress0/ho/issue4990-care-graph.smt2 regress0/ho/issue5233-part1-usort-owner.smt2 regress0/ho/issue5371.smt2 + regress0/ho/issue5741-1-cg-model.smt2 + regress0/ho/issue5741-3-cg-model.smt2 + regress0/ho/issue5744-cg-model.smt2 regress0/ho/issue6526.smt2 regress0/ho/issue6536.smt2 regress0/ho/ite-apply-eq.smt2 regress0/ho/lambda-equality-non-canon.smt2 regress0/ho/match-middle.smt2 regress0/ho/modulo-func-equality.smt2 + regress0/ho/qgu-fuzz-ho-1-dd.smt2 regress0/ho/shadowing-defs.smt2 regress0/ho/simple-matching-partial.smt2 regress0/ho/simple-matching.smt2 @@ -1714,6 +1718,9 @@ set(regress_1_tests regress1/ho/issue4065-no-rep.smt2 regress1/ho/issue4092-sinf.smt2 regress1/ho/issue4134-sinf.smt2 + regress1/ho/issue4758.smt2 + regress1/ho/issue5078-small.smt2 + regress1/ho/issue5201-1.smt2 regress1/ho/issue5741-3.smt2 regress1/ho/NUM638^1.smt2 regress1/ho/NUM925^1.p diff --git a/test/regress/regress0/ho/issue5741-1-cg-model.smt2 b/test/regress/regress0/ho/issue5741-1-cg-model.smt2 new file mode 100644 index 000000000..8989acdc4 --- /dev/null +++ b/test/regress/regress0/ho/issue5741-1-cg-model.smt2 @@ -0,0 +1,18 @@ +(set-logic HO_ALL) +(set-info :status sat) +(declare-fun a ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) +(declare-fun c () (_ BitVec 1)) +(declare-fun d () (_ BitVec 32)) +(declare-fun e () (_ BitVec 32)) +(declare-fun f () (_ BitVec 32)) +(declare-fun g ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32)) +(declare-fun h () (_ BitVec 32)) +(declare-fun i () (_ BitVec 32)) +(declare-fun j () (_ BitVec 1)) +(declare-fun k () (_ BitVec 32)) +(assert (= b (a d e))) +(assert (= f (g h i))) +(assert (distinct j (ite (= i k) (_ bv1 1) (_ bv0 1)))) +(assert (= (ite (= i b) (_ bv1 1) (_ bv0 1)) j (ite (= c (_ bv0 1)) (_ bv1 1) (_ bv0 1)))) +(check-sat) diff --git a/test/regress/regress0/ho/issue5741-3-cg-model.smt2 b/test/regress/regress0/ho/issue5741-3-cg-model.smt2 new file mode 100644 index 000000000..abc4b76a6 --- /dev/null +++ b/test/regress/regress0/ho/issue5741-3-cg-model.smt2 @@ -0,0 +1,5 @@ +(set-logic HO_ALL) +(set-info :status sat) +(declare-fun p ((_ BitVec 17) (_ BitVec 16)) Bool) +(assert (p (_ bv0 17) ((_ sign_extend 15) (ite (p (_ bv0 17) (_ bv0 16)) (_ bv1 1) (_ bv0 1))))) +(check-sat) diff --git a/test/regress/regress0/ho/issue5744-cg-model.smt2 b/test/regress/regress0/ho/issue5744-cg-model.smt2 new file mode 100644 index 000000000..5650351cd --- /dev/null +++ b/test/regress/regress0/ho/issue5744-cg-model.smt2 @@ -0,0 +1,7 @@ +(set-logic HO_ALL) +(set-info :status sat) +(declare-fun r4 () Real) +(declare-fun ufrb5 (Real Real Real Real Real) Bool) +(assert (ufrb5 0.0 0.0 0.0 0.0 0)) +(assert (ufrb5 (+ r4 r4) 0.0 1 0.0 0.0)) +(check-sat) diff --git a/test/regress/regress0/ho/qgu-fuzz-ho-1-dd.smt2 b/test/regress/regress0/ho/qgu-fuzz-ho-1-dd.smt2 new file mode 100644 index 000000000..840db92a9 --- /dev/null +++ b/test/regress/regress0/ho/qgu-fuzz-ho-1-dd.smt2 @@ -0,0 +1,6 @@ +(set-logic HO_ALL) +(set-info :status sat) +(declare-const b (-> Int Int Int)) +(declare-const c (-> Int Int)) +(assert (and (= c (b 1)) (= c (b 0)) (> (b 1 0) 0) (> 0 (b 0 1)) (= 0 (c (b 0 0))))) +(check-sat) diff --git a/test/regress/regress1/ho/issue4758.smt2 b/test/regress/regress1/ho/issue4758.smt2 new file mode 100644 index 000000000..dab284c11 --- /dev/null +++ b/test/regress/regress1/ho/issue4758.smt2 @@ -0,0 +1,6 @@ +(set-logic HO_ALL) +(set-info :status sat) +(declare-fun a () Real) +(declare-fun b (Real Real) Real) +(assert (> (b a 0) (b (- a) 1))) +(check-sat) diff --git a/test/regress/regress1/ho/issue5078-small.smt2 b/test/regress/regress1/ho/issue5078-small.smt2 new file mode 100644 index 000000000..21077434a --- /dev/null +++ b/test/regress/regress1/ho/issue5078-small.smt2 @@ -0,0 +1,8 @@ +(set-logic HO_QF_UFLIA) +(set-info :status sat) +(declare-fun a (Int Int) Int) +(declare-fun d () Int) +(declare-fun e () Int) +(assert (= (a d 0) (a 0 1))) +(assert (= d (mod e 3))) +(check-sat) diff --git a/test/regress/regress1/ho/issue5201-1.smt2 b/test/regress/regress1/ho/issue5201-1.smt2 new file mode 100644 index 000000000..9f6e058da --- /dev/null +++ b/test/regress/regress1/ho/issue5201-1.smt2 @@ -0,0 +1,20 @@ +(set-logic HO_QF_UFLIA) +(set-info :status sat) +(declare-fun a () Int) +(declare-fun b (Int Int) Int) +(declare-fun c (Int Int) Int) +(declare-fun d () Int) +(declare-fun e () Int) +(declare-fun f () Int) +(declare-fun g () Int) +(declare-fun i () Int) +(declare-fun j () Int) +(declare-fun k () Int) +(assert (= d (b j d) a)) +(assert (= e (c e i))) +(assert (= (b k f) a)) +(assert (= d (+ g 4))) +(assert (= j (* g 5))) +(assert (= e (+ g 5))) +(assert (= k 0)) +(check-sat)