From 1ee275804ae31dbd13b67aaab01e757ec115c177 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 14 Mar 2022 22:16:41 -0500 Subject: [PATCH] Fix to consider leafs of theory sets to be variables (#8305) Fixes cvc5/cvc5-projects#494. With this fix, we now properly consider terms that belong to other theories that are of set type, e.g. (select x (as set.universe (Set RoundingMode)) in this example to be "variables" according to the theory of sets procedure. The benchmark is unsat because there are 5 rounding modes and we are selecting an index in a sequence storing "false" at the first 6 indices. --- src/theory/sets/solver_state.cpp | 8 +++++--- test/regress/CMakeLists.txt | 1 + .../regress1/sets/proj-issue494-finite-leafof.smt2 | 9 +++++++++ 3 files changed, 15 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress1/sets/proj-issue494-finite-leafof.smt2 diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp index 3f619dcad..62ae32a14 100644 --- a/src/theory/sets/solver_state.cpp +++ b/src/theory/sets/solver_state.cpp @@ -141,10 +141,12 @@ void SolverState::registerTerm(Node r, TypeNode tnn, Node n) d_allCompSets.push_back(n); Trace("sets-debug2") << "Comp-set[" << r << "] : " << n << std::endl; } - else if (n.isVar() && !d_skCache.isSkolem(n)) + else if (Theory::isLeafOf(n, THEORY_SETS) && !d_skCache.isSkolem(n)) { - // it is important that we check it is a variable, but not an internally - // introduced skolem, due to the semantics of the universe set. + // It is important that we check it is a leaf, due to parametric theories + // that may be used to construct terms of set type. It is also important to + // exclude internally introduced skolems, due to the semantics of the + // universe set. if (tnn.isSet()) { if (d_var_set.find(r) == d_var_set.end()) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 84aebd5ae..398c08cbb 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2411,6 +2411,7 @@ set(regress_1_tests regress1/sets/lemmabug-ListElts317minimized.smt2 regress1/sets/proj-issue164.smt2 regress1/sets/proj-issue178.smt2 + regress1/sets/proj-issue494-finite-leafof.smt2 regress1/sets/remove_check_free_31_6.smt2 regress1/sets/sets-disequal.smt2 regress1/sets/sets-tuple-poly.cvc.smt2 diff --git a/test/regress/regress1/sets/proj-issue494-finite-leafof.smt2 b/test/regress/regress1/sets/proj-issue494-finite-leafof.smt2 new file mode 100644 index 000000000..24f0a51db --- /dev/null +++ b/test/regress/regress1/sets/proj-issue494-finite-leafof.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL) +(set-info :status unsat) +(set-option :strings-exp true) +(set-option :sets-ext true) +(declare-const x (Array (Set RoundingMode) (Set RoundingMode))) +(check-sat-assuming ( +(seq.nth +(seq.++ (seq.++ (seq.unit false) (seq.unit false)) (seq.++ (seq.unit false) (seq.unit false)) (seq.++ (seq.unit false) (seq.unit false))) +(set.card (select x (as set.universe (Set RoundingMode))))))) -- 2.30.2