From 519cdc2d4b44a9785ee68d181e2682d74890e89a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 22 Mar 2021 12:45:19 -0500 Subject: [PATCH] Function types are always first-class (#6167) This eliminates one of the dependencies of TypeNode on options. In particular, this makes it so that function types are always considered first-class. This change makes it so that higher-order types can always be constructed; logic exceptions should occur if they are used in constraints. --- src/api/checks.h | 20 +++++---- src/expr/node_manager.cpp | 2 - src/expr/type_node.cpp | 13 ++---- src/theory/uf/theory_uf.cpp | 75 ++++++++++++++++++++++++++-------- src/theory/uf/theory_uf.h | 9 +++- test/unit/api/solver_black.cpp | 29 +++++++------ test/unit/api/sort_black.cpp | 4 +- 7 files changed, 102 insertions(+), 50 deletions(-) diff --git a/src/api/checks.h b/src/api/checks.h index c2869f463..d5408d312 100644 --- a/src/api/checks.h +++ b/src/api/checks.h @@ -429,16 +429,18 @@ namespace api { /** * Codomain sort check for member functions of class Solver. * Check if codomain sort is not null, associated with this solver, and a - * first-class sort. + * first-class, non-function sort. */ -#define CVC4_API_SOLVER_CHECK_CODOMAIN_SORT(sort) \ - do \ - { \ - CVC4_API_ARG_CHECK_NOT_NULL(sort); \ - CVC4_API_CHECK(this == sort.d_solver) \ - << "Given sort is not associated with this solver"; \ - CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) \ - << "first-class sort as codomain sort"; \ +#define CVC4_API_SOLVER_CHECK_CODOMAIN_SORT(sort) \ + do \ + { \ + CVC4_API_ARG_CHECK_NOT_NULL(sort); \ + CVC4_API_CHECK(this == sort.d_solver) \ + << "Given sort is not associated with this solver"; \ + CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) \ + << "first-class sort as codomain sort"; \ + CVC4_API_ARG_CHECK_EXPECTED(!sort.isFunction(), sort) \ + << "function sort as codomain sort"; \ } while (0) /* Term checks. ------------------------------------------------------------- */ diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 2d5ed36fb..fdd7e5f5a 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -31,8 +31,6 @@ #include "expr/node_manager_attributes.h" #include "expr/skolem_manager.h" #include "expr/type_checker.h" -#include "options/options.h" -#include "options/smt_options.h" #include "util/resource_manager.h" #include "util/statistics_registry.h" diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 8b0d6d7f7..8cf4fbccd 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -20,9 +20,7 @@ #include "expr/node_manager_attributes.h" #include "expr/type_properties.h" #include "options/base_options.h" -#include "options/expr_options.h" #include "options/quantifiers_options.h" -#include "options/uf_options.h" #include "theory/type_enumerator.h" using namespace std; @@ -286,13 +284,10 @@ bool TypeNode::isClosedEnumerable() } bool TypeNode::isFirstClass() const { - return ( getKind() != kind::FUNCTION_TYPE || options::ufHo() ) && - getKind() != kind::CONSTRUCTOR_TYPE && - getKind() != kind::SELECTOR_TYPE && - getKind() != kind::TESTER_TYPE && - getKind() != kind::SEXPR_TYPE && - ( getKind() != kind::TYPE_CONSTANT || - getConst() != REGEXP_TYPE ); + return getKind() != kind::CONSTRUCTOR_TYPE && getKind() != kind::SELECTOR_TYPE + && getKind() != kind::TESTER_TYPE && getKind() != kind::SEXPR_TYPE + && (getKind() != kind::TYPE_CONSTANT + || getConst() != REGEXP_TYPE); } bool TypeNode::isWellFounded() const { diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index ac25ede14..aaa9d60f0 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -210,7 +210,9 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector& lems) { Trace("uf-exp-def") << "TheoryUF::ppRewrite: expanding definition : " << node << std::endl; - if( node.getKind()==kind::HO_APPLY ){ + Kind k = node.getKind(); + if (k == kind::HO_APPLY) + { if( !options::ufHo() ){ std::stringstream ss; ss << "Partial function applications are not supported in default mode, try --uf-ho."; @@ -224,6 +226,18 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector& lems) return TrustNode::mkTrustRewrite(node, ret, nullptr); } } + else if (k == kind::APPLY_UF) + { + // check for higher-order + // logic exception if higher-order is not enabled + if (isHigherOrderType(node.getOperator().getType()) && !options::ufHo()) + { + std::stringstream ss; + ss << "UF received an application whose operator has higher-order type " + << node << ", which is not supported by default, try --uf-ho"; + throw LogicException(ss.str()); + } + } return TrustNode::null(); } @@ -239,23 +253,30 @@ void TheoryUF::preRegisterTerm(TNode node) //Assert( node.getKind()!=kind::APPLY_UF || !options::ufHo() ); Assert(node.getKind() != kind::HO_APPLY || options::ufHo()); - switch (node.getKind()) { - case kind::EQUAL: - // Add the trigger for equality - d_equalityEngine->addTriggerPredicate(node); - break; - case kind::APPLY_UF: - case kind::HO_APPLY: - // Maybe it's a predicate - if (node.getType().isBoolean()) { - // Get triggered for both equal and dis-equal + Kind k = node.getKind(); + switch (k) + { + case kind::EQUAL: + // Add the trigger for equality d_equalityEngine->addTriggerPredicate(node); - } else { - // Function applications/predicates - d_equalityEngine->addTerm(node); + break; + case kind::APPLY_UF: + case kind::HO_APPLY: + { + // Maybe it's a predicate + if (node.getType().isBoolean()) + { + // Get triggered for both equal and dis-equal + d_equalityEngine->addTriggerPredicate(node); + } + else + { + // Function applications/predicates + d_equalityEngine->addTerm(node); + } + // Remember the function and predicate terms + d_functionsTerms.push_back(node); } - // Remember the function and predicate terms - d_functionsTerms.push_back(node); break; case kind::CARDINALITY_CONSTRAINT: case kind::COMBINED_CARDINALITY_CONSTRAINT: @@ -648,6 +669,28 @@ void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } } +bool TheoryUF::isHigherOrderType(TypeNode tn) +{ + Assert(tn.isFunction()); + std::map::iterator it = d_isHoType.find(tn); + if (it != d_isHoType.end()) + { + return it->second; + } + bool ret = false; + const std::vector& argTypes = tn.getArgTypes(); + for (const TypeNode& tnc : argTypes) + { + if (tnc.isFunction()) + { + ret = true; + break; + } + } + d_isHoType[tn] = ret; + return ret; +} + } /* namespace CVC4::theory::uf */ } /* namespace CVC4::theory */ } /* namespace CVC4 */ diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index e1184a829..8d2edaffe 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -162,7 +162,12 @@ private: const TNodeTrie* t2, unsigned arity, unsigned depth); - + /** + * Is t a higher order type? A higher-order type is a function type having + * an argument type that is also a function type. This is used for checking + * logic exceptions. + */ + bool isHigherOrderType(TypeNode tn); TheoryUfRewriter d_rewriter; /** Proof rule checker */ UfProofRuleChecker d_ufProofChecker; @@ -172,6 +177,8 @@ private: TheoryInferenceManager d_im; /** The notify class */ NotifyClass d_notify; + /** Cache for isHigherOrderType */ + std::map d_isHoType; };/* class TheoryUF */ }/* CVC4::theory::uf namespace */ diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index e5589f81e..18a8f9cc8 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -200,7 +200,11 @@ TEST_F(TestApiBlackSolver, mkFunctionSort) d_solver.getIntegerSort())); Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()); - ASSERT_THROW(d_solver.mkFunctionSort(funSort, d_solver.getIntegerSort()), + // function arguments are allowed + ASSERT_NO_THROW(d_solver.mkFunctionSort(funSort, d_solver.getIntegerSort())); + // non-first-class arguments are not allowed + Sort reSort = d_solver.getRegExpSort(); + ASSERT_THROW(d_solver.mkFunctionSort(reSort, d_solver.getIntegerSort()), CVC4ApiException); ASSERT_THROW(d_solver.mkFunctionSort(d_solver.getIntegerSort(), funSort), CVC4ApiException); @@ -209,10 +213,10 @@ TEST_F(TestApiBlackSolver, mkFunctionSort) d_solver.getIntegerSort())); Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()); - ASSERT_THROW( + // function arguments are allowed + ASSERT_NO_THROW( d_solver.mkFunctionSort({funSort2, d_solver.mkUninterpretedSort("u")}, - d_solver.getIntegerSort()), - CVC4ApiException); + d_solver.getIntegerSort())); ASSERT_THROW(d_solver.mkFunctionSort({d_solver.getIntegerSort(), d_solver.mkUninterpretedSort("u")}, funSort2), @@ -248,8 +252,9 @@ TEST_F(TestApiBlackSolver, mkPredicateSort) ASSERT_THROW(d_solver.mkPredicateSort({}), CVC4ApiException); Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()); - ASSERT_THROW(d_solver.mkPredicateSort({d_solver.getIntegerSort(), funSort}), - CVC4ApiException); + // functions as arguments are allowed + ASSERT_NO_THROW( + d_solver.mkPredicateSort({d_solver.getIntegerSort(), funSort})); Solver slv; ASSERT_THROW(slv.mkPredicateSort({d_solver.getIntegerSort()}), @@ -954,8 +959,8 @@ TEST_F(TestApiBlackSolver, declareFun) ASSERT_NO_THROW( d_solver.declareFun("f3", {bvSort, d_solver.getIntegerSort()}, bvSort)); ASSERT_THROW(d_solver.declareFun("f2", {}, funSort), CVC4ApiException); - ASSERT_THROW(d_solver.declareFun("f4", {bvSort, funSort}, bvSort), - CVC4ApiException); + // functions as arguments is allowed + ASSERT_NO_THROW(d_solver.declareFun("f4", {bvSort, funSort}, bvSort)); ASSERT_THROW(d_solver.declareFun("f5", {bvSort, bvSort}, funSort), CVC4ApiException); Solver slv; @@ -1007,8 +1012,8 @@ TEST_F(TestApiBlackSolver, defineFun) ASSERT_THROW(d_solver.defineFun("fff", {b1}, bvSort, v3), CVC4ApiException); ASSERT_THROW(d_solver.defineFun("ffff", {b1}, funSort2, v3), CVC4ApiException); - ASSERT_THROW(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1), - CVC4ApiException); + // b3 has function sort, which is allowed as an argument + ASSERT_NO_THROW(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1)); ASSERT_THROW(d_solver.defineFun(f1, {v1, b11}, v1), CVC4ApiException); ASSERT_THROW(d_solver.defineFun(f1, {b1}, v1), CVC4ApiException); ASSERT_THROW(d_solver.defineFun(f1, {b1, b11}, v2), CVC4ApiException); @@ -1078,8 +1083,8 @@ TEST_F(TestApiBlackSolver, defineFunRec) CVC4ApiException); ASSERT_THROW(d_solver.defineFunRec("ffff", {b1}, funSort2, v3), CVC4ApiException); - ASSERT_THROW(d_solver.defineFunRec("fffff", {b1, b3}, bvSort, v1), - CVC4ApiException); + // b3 has function sort, which is allowed as an argument + ASSERT_NO_THROW(d_solver.defineFunRec("fffff", {b1, b3}, bvSort, v1)); ASSERT_THROW(d_solver.defineFunRec(f1, {b1}, v1), CVC4ApiException); ASSERT_THROW(d_solver.defineFunRec(f1, {b1, b11}, v2), CVC4ApiException); ASSERT_THROW(d_solver.defineFunRec(f1, {b1, b11}, v3), CVC4ApiException); diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp index e52bd6103..625af9342 100644 --- a/test/unit/api/sort_black.cpp +++ b/test/unit/api/sort_black.cpp @@ -230,7 +230,9 @@ TEST_F(TestApiBlackSort, isFirstClass) Sort fun_sort = d_solver.mkFunctionSort(d_solver.getRealSort(), d_solver.getIntegerSort()); ASSERT_TRUE(d_solver.getIntegerSort().isFirstClass()); - ASSERT_FALSE(fun_sort.isFirstClass()); + ASSERT_TRUE(fun_sort.isFirstClass()); + Sort reSort = d_solver.getRegExpSort(); + ASSERT_FALSE(reSort.isFirstClass()); ASSERT_NO_THROW(Sort().isFirstClass()); } -- 2.30.2