diff options
149 files changed, 2897 insertions, 879 deletions
diff --git a/.github/actions/run-tests/action.yml b/.github/actions/run-tests/action.yml index e5557bb2d..2b2326699 100644 --- a/.github/actions/run-tests/action.yml +++ b/.github/actions/run-tests/action.yml @@ -7,6 +7,10 @@ inputs: default: false check-unit-tests: default: true + regressions-args: + default: "--no-check-unsat-cores --no-check-proofs" + regressions-exclude: + default: "3-4" runs: using: composite steps: @@ -15,9 +19,9 @@ runs: run: | make -j${{ env.num_proc }} check env: - ARGS: --output-on-failure -LE regress[${{ matrix.exclude_regress }}] + ARGS: --output-on-failure -LE regress[${{ inputs.regressions-exclude }}] CVC5_REGRESSION_ARGS: --no-early-exit - RUN_REGRESSION_ARGS: ${{ matrix.run_regression_args }} + RUN_REGRESSION_ARGS: ${{ inputs.regressions-args }} working-directory: build - name: Run Unit Tests diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 8d88cad49..b8ee51837 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -89,6 +89,8 @@ jobs: check-examples: ${{ matrix.check-examples }} check-python-bindings: ${{ matrix.python-bindings }} check-unit-tests: ${{ matrix.check-units }} + regressions-args: ${{ matrix.run_regression_args }} + regressions-exclude: ${{ matrix.exclude_regress }} - name: Build documentation if: matrix.build-documentation diff --git a/.github/workflows/cmake-version.yml b/.github/workflows/cmake-version.yml index d61c59088..24d87ba3b 100644 --- a/.github/workflows/cmake-version.yml +++ b/.github/workflows/cmake-version.yml @@ -9,7 +9,7 @@ jobs: strategy: matrix: cmake_version: [ - "3.12", "3.13", "3.14", "3.15", "3.16", + "3.8", "3.9", "3.10", "3.11", "3.12", "3.13", "3.14", "3.15", "3.16", "3.17", "3.18", "3.19", "3.20", "3.21" ] @@ -21,6 +21,10 @@ jobs: - uses: actions/checkout@v2 + - name: Adapt cmake version checks + run: | + sed -i'orig' -E 's/cmake_minimum_required\(VERSION [0-9.]+\)/cmake_minimum_required(VERSION ${{ matrix.cmake_version }})/' CMakeLists.txt + - name: Install dependencies uses: ./.github/actions/install-dependencies with: diff --git a/.github/workflows/docs_upload.yml b/.github/workflows/docs_upload.yml index d9e81b05e..7bdd186a1 100644 --- a/.github/workflows/docs_upload.yml +++ b/.github/workflows/docs_upload.yml @@ -55,7 +55,11 @@ jobs: - name: Setup Context run: | HASH=${{ github.event.workflow_run.head_commit.id }} - if [ "${{ github.event.workflow_run.event }}" == "push" ] ; then + ISTAG=${{ startsWith(github.ref, 'refs/tags/') }} + if [ "$ISTAG" = true ] ; then + NAME=${{ github.event.workflow_run.head_branch }} + echo "Identified tag $NAME" + elif [ "${{ github.event.workflow_run.event }}" == "push" ] ; then NAME=${{ github.event.workflow_run.head_branch }} echo "Identified branch $NAME" elif [ "${{ github.event.workflow_run.event }}" == "pull_request" ] ; then @@ -66,6 +70,7 @@ jobs: fi echo "NAME=$NAME" >> $GITHUB_ENV echo "HASH=$HASH" >> $GITHUB_ENV + echo "ISTAG=$ISTAG" >> $GITHUB_ENV - name: Update docs continue-on-error: true @@ -76,7 +81,9 @@ jobs: mv docs-new target/docs-$NAME-$HASH cd target/ - if diff -r -x "*.zip" docs-master/ docs-$NAME-$HASH + isdiff=$(diff -r -x "*.zip" docs-master/ docs-$NAME-$HASH >&2; echo $?; exit 0) + + if [[ ("$ISTAG" != true) && ($isdiff = 0) ]] then echo "Ignored run, documentation is the same as for current master" else diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2021 b/contrib/competitions/smt-comp/run-script-smtcomp2021 index 9b4f534b0..faa368670 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp2021 +++ b/contrib/competitions/smt-comp/run-script-smtcomp2021 @@ -56,7 +56,7 @@ QF_LIA) finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites --ite-simp --simp-ite-compress ;; QF_NIA) - trywith 420 --nl-ext-tplanes --decision=justification + trywith 420 --nl-ext-tplanes --decision=justification --jh-rlv-order trywith 60 --nl-ext-tplanes --decision=internal trywith 60 --nl-ext-tplanes --decision=justification-old trywith 60 --no-nl-ext-tplanes --decision=internal @@ -132,7 +132,7 @@ LIA|LRA) ;; QF_AUFBV) trywith 600 - finishwith --decision=justification-stoponly + finishwith --decision=stoponly ;; QF_ABV) trywith 50 --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv @@ -153,7 +153,7 @@ QF_AUFNIA) ;; QF_ALIA) trywith 140 --decision=justification --arrays-weak-equiv - finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas + finishwith --decision=stoponly --no-arrays-eager-index --arrays-eager-lemmas ;; QF_S|QF_SLIA) trywith 300 --strings-exp --strings-fmf --no-jh-rlv-order diff --git a/docs/api/cpp/cpp.rst b/docs/api/cpp/cpp.rst index c10ae7517..04f731203 100644 --- a/docs/api/cpp/cpp.rst +++ b/docs/api/cpp/cpp.rst @@ -30,5 +30,6 @@ C++ API Documentation sort statistics term + unknownexplanation diff --git a/docs/api/cpp/unknownexplanation.rst b/docs/api/cpp/unknownexplanation.rst new file mode 100644 index 000000000..9a64ec4aa --- /dev/null +++ b/docs/api/cpp/unknownexplanation.rst @@ -0,0 +1,6 @@ +UnknownExplanation +============ + +.. doxygenenum:: cvc5::api::Result::UnknownExplanation + :project: cvc5 + diff --git a/docs/api/python/grammar.rst b/docs/api/python/grammar.rst new file mode 100644 index 000000000..a2059fa93 --- /dev/null +++ b/docs/api/python/grammar.rst @@ -0,0 +1,6 @@ +Grammar +================ + +.. autoclass:: pycvc5.Grammar + :members: + :undoc-members: diff --git a/docs/api/python/op.rst b/docs/api/python/op.rst new file mode 100644 index 000000000..7769b33f0 --- /dev/null +++ b/docs/api/python/op.rst @@ -0,0 +1,6 @@ +Op +================ + +.. autoclass:: pycvc5.Op + :members: + :undoc-members: diff --git a/docs/api/python/python.rst b/docs/api/python/python.rst index d815f837a..a6aca2cf9 100644 --- a/docs/api/python/python.rst +++ b/docs/api/python/python.rst @@ -19,3 +19,8 @@ Python API Documentation datatypeconstructordecl datatypedecl datatypeselector + grammar + op + result + roundingmode + unknownexplanation diff --git a/docs/api/python/result.rst b/docs/api/python/result.rst new file mode 100644 index 000000000..9edb12b92 --- /dev/null +++ b/docs/api/python/result.rst @@ -0,0 +1,6 @@ +Result +================ + +.. autoclass:: pycvc5.Result + :members: + :undoc-members: diff --git a/docs/api/python/roundingmode.rst b/docs/api/python/roundingmode.rst new file mode 100644 index 000000000..0c226082e --- /dev/null +++ b/docs/api/python/roundingmode.rst @@ -0,0 +1,6 @@ +RoundingMode +================ + +.. autoclass:: pycvc5.RoundingMode + :members: + :undoc-members: diff --git a/docs/api/python/unknownexplanation.rst b/docs/api/python/unknownexplanation.rst new file mode 100644 index 000000000..54c37665b --- /dev/null +++ b/docs/api/python/unknownexplanation.rst @@ -0,0 +1,6 @@ +UnknownExplanation +================ + +.. autoclass:: pycvc5.UnknownExplanation + :members: + :undoc-members: diff --git a/proofs/lfsc/signatures/nary_programs.plf b/proofs/lfsc/signatures/nary_programs.plf new file mode 100644 index 000000000..f04e6ba40 --- /dev/null +++ b/proofs/lfsc/signatures/nary_programs.plf @@ -0,0 +1,179 @@ +; depends: core_defs.plf util_defs.plf + +; This file defines a library of methods for reasoning about n-ary functions. +; Notice that since LFSC does not have support for n-ary function symbols, we +; represent n-ary function applications in a null-terminated, Curried form. +; In particular, the term `(or A B C)` is represented in LFSC as: +; `(apply (apply f_or A) (apply (apply f_or B) (apply (apply f_or C) false)))` +; i.e. using the macro definitions in core_defs: +; `(or A (or B (or C false)))` +; where notice that `false` is the null-terminator for `or`. Many operators +; are treated in this way, including Boolean connectives `and` and `or`, +; arithmetic plus and multiplication, string concatenation, and so on. +; We call the term like the one above "an f_or-application in n-ary form". +; When applicable, we simply write "f-application" to refer to a term that is +; in n-ary form. We call A, B, C the "elements" of the f-application above. +; We say that an f-application is a "singleton" if it consists of a single +; element, e.g. `(or A false)`. +; +; This file defines a set of side conditions that are useful in defining +; theory-specific proof rules involving n-ary functions and are agnostic to the +; function in question. When applicable, the side conditions take the n-ary +; function `f` as an argument, or its null terminator `null`. + +; Head and tail for n-ary operators with null terminators. These methods +; fail if t is not an f-application. +(program nary_head ((f term) (t term)) term + (match t ((apply t1 t2) (getarg f t1)))) +(program nary_tail ((f term) (t term)) term + (match t ((apply t1 t2) (let t12 (getarg f t1) t2)))) + +; Remove the first occurrence of term l from t. This side condition fails if t +; is not an f-application, or if t does not contain l. +(program nary_rm_first ((f term) (t term) (l term)) term + (match t + ((apply t1 t2) ; otherwise at end, l not found + (let t12 (getarg f t1) + (ifequal t12 l t2 (apply t1 (nary_rm_first f t2 l)))))) + ; otherwise not an f-app in n-ary form +) + +; Same as `nary_rm_first`, but also checks whether t is l itself and returns null if so, +; where null is a null terminator. +(program nary_rm_first_or_self ((f term) (t term) (l term) (null term)) term + (ifequal t l null (nary_rm_first f t l)) +) + +; Does t contain l? This side condition may fail if t is not an f-application. +(program nary_ctn ((f term) (t term) (l term)) flag + (match t + ((apply t1 t2) + (let t12 (getarg f t1) + (ifequal t12 l tt (nary_ctn f t2 l)))) + ; otherwise not an f-app in n-ary form + (default ff)) +) + +; Same as `nary_ctn`, but also checks if t is l, returning true if so. +(program nary_ctn_or_self ((f term) (t term) (l term)) flag + (ifequal t l tt (nary_ctn f t l)) +) + +; Returns true if t is a subset of s, when these terms were interpreted as sets. +; This side condition may fail if t or s is not an f-application. +(program nary_is_subset ((f term) (t term) (s term)) flag + (match t + ((apply t1 t2) + (let t12 (getarg f t1) + (ifequal (nary_ctn_or_self f s t12) tt (nary_is_subset f t2 s) ff))) + ; otherwise not in n-ary form + (default tt)) +) + +; Concatenates terms t1 and t2 that are f-applications in n-ary form. +(program nary_concat ((f term) (t1 term) (t2 term) (null term)) term + (match t1 + ((apply t11 t12) + (let t112 (getarg f t11) + (apply t11 (nary_concat f t12 t2 null)))) + (default t2)) ; any non-application term is interpreted as null +) + +; Insert element elem at the beginning of the f-application t. +(program nary_insert ((f term) (elem term) (t term) (null term)) term + (ifequal elem null t (apply (apply f elem) t))) + +; Dual to `nary_insert`. Returns a term pair ( elem, t' ) where elem is the +; head of t, and t' is the tail of t. +(program nary_decompose ((f term) (t term) (null term)) termPair + (match t + ((apply t1 t2) + (match t1 + ((apply t11 t12) (ifequal t11 f (pair t12 t2) (pair null t))) + (default (pair null t)))) + (default (pair null t))) +) + +; N-ary elimination. This replaces a singleton f-application with its element. +; For example, this replaces e.g. (or t false) with t. +(program nary_elim ((f term) (t term) (null term)) term + (match t + ((apply t1 t2) + ; if null terminated, then we return the head, otherwise not in n-ary form + (ifequal t2 null (getarg f t1) t)) + (default (ifequal t null t (fail term)))) +) + +; N-ary introduction, which is the inverse of nary_elim. This turns a term t into +; a (singleton) f-application if it is not already in n-ary form. For example, +; this replaces t with (or t false) if t is not already in n-ary form. +(program nary_intro ((f term) (t term) (null term)) term + (match t + ((apply t1 t2) + (match t1 + ((apply t11 t12) (ifequal t11 f t (apply (apply f t) null))) + (default (apply (apply f t) null)))) + (default (ifequal t null t (apply (apply f t) null)))) +) + +; Extract the n^th element of f-application t. This side condition fails if +; t is not an f-application, or contains fewer than n elements. +(program nary_extract ((f term) (t term) (n mpz)) term + (match t + ((apply t1 t2) + (mp_ifzero n + (getarg f t1) + (nary_extract f t2 (mp_add n (mp_neg 1)))))) +) + +; Helper for dropping duplicates from an f-application t. Elements occur in +; the returned f-application in the order they first appear in t. +; This side condition takes an accumulator tacc which tracks which terms it is +; adding to the return value. We require an explicit accumulator to ensure +; propering ordering for cases like (or A B B A), where (or A B) should be +; returned instead of (or B A). +; This method fails if t is not an f-application. +(program nary_drop_dups_rec ((f term) (t term) (tacc term)) term + (match t + ((apply t1 t2) + (let t12 (getarg f t1) + (let c (nary_ctn f tacc t12) + (let t2d (nary_drop_dups_rec f t2 (ifequal c tt tacc (apply t1 tacc))) + (ifequal c tt t2d (apply t1 t2d)))))) + (default t)) +) + +; Drop all duplicates in an f-application t using the helper method +; `nary_drop_dups_rec`. +(program nary_drop_dups ((f term) (t term) (null term)) term + (nary_elim f (nary_drop_dups_rec f t null) null) +) + +; Truncate, which returns the f-application in which the subterm c has been +; replaced by the null terminator, where c is an f-application that is a +; suffix of t. For example, (or t1 ... tn c) ---> (or t1 ... tn false). +; This side condition fails if c is not a suffix of f-application t. +(program nary_truncate ((f term) (t term) (c term) (null term)) term + (ifequal t c null + (match t + ((apply t1 t2) + (let t12 (getarg f t1) + (apply t1 (nary_truncate f t2 c null)))))) +) + +; Helper for reverse, which takes an accumulator of terms we have added in +; reverse order to the value we will return. This side condition fails if +; t is not an f-application. +(program nary_reverse_rec ((f term) (t term) (acc term) (null term)) term + (match t + ((apply t1 t2) + (let t12 (getarg f t1) + (nary_reverse_rec f t2 (apply t1 acc) null))) + (default (ifequal t null acc (fail term)))) +) + +; Reverse the elements in f-application t using the helper method +; `nary_reverse_rec`. +(program nary_reverse ((f term) (t term) (null term)) term + (nary_reverse_rec f t null null) +) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 733186d16..a2b5966e1 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -795,6 +795,8 @@ libcvc5_add_sources( theory/quantifiers/ematching/instantiation_engine.h theory/quantifiers/ematching/pattern_term_selector.cpp theory/quantifiers/ematching/pattern_term_selector.h + theory/quantifiers/ematching/relational_match_generator.cpp + theory/quantifiers/ematching/relational_match_generator.h theory/quantifiers/ematching/trigger.cpp theory/quantifiers/ematching/trigger.h theory/quantifiers/ematching/trigger_database.cpp @@ -805,6 +807,8 @@ libcvc5_add_sources( theory/quantifiers/ematching/trigger_trie.h theory/quantifiers/ematching/var_match_generator.cpp theory/quantifiers/ematching/var_match_generator.h + theory/quantifiers/entailment_check.cpp + theory/quantifiers/entailment_check.h theory/quantifiers/equality_query.cpp theory/quantifiers/equality_query.h theory/quantifiers/expr_miner.cpp @@ -1079,6 +1083,8 @@ libcvc5_add_sources( theory/strings/normal_form.h theory/strings/proof_checker.cpp theory/strings/proof_checker.h + theory/strings/regexp_enumerator.cpp + theory/strings/regexp_enumerator.h theory/strings/regexp_elim.cpp theory/strings/regexp_elim.h theory/strings/regexp_entail.cpp @@ -1402,7 +1408,6 @@ if(USE_GLPK) if(ENABLE_STATIC_LIBRARY) target_link_libraries(cvc5-static PUBLIC ${GLPK_LIBRARIES}) endif() - target_link_libraries(cvc5-obj PUBLIC ${GLPK_LIBRARIES}) endif() if(USE_POLY) add_dependencies(cvc5-obj Polyxx_SHARED) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 778f700c0..bb39ae86d 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -1682,7 +1682,7 @@ size_t Sort::getSortConstructorArity() const /* Bit-vector sort ----------------------------------------------------- */ -uint32_t Sort::getBVSize() const +uint32_t Sort::getBitVectorSize() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; @@ -1695,7 +1695,7 @@ uint32_t Sort::getBVSize() const /* Floating-point sort ------------------------------------------------- */ -uint32_t Sort::getFPExponentSize() const +uint32_t Sort::getFloatingPointExponentSize() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; @@ -1706,7 +1706,7 @@ uint32_t Sort::getFPExponentSize() const CVC5_API_TRY_CATCH_END; } -uint32_t Sort::getFPSignificandSize() const +uint32_t Sort::getFloatingPointSignificandSize() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; @@ -5082,7 +5082,7 @@ Term Solver::mkTermFromKind(Kind kind) const CVC5_API_KIND_CHECK_EXPECTED(kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA || kind == SEP_EMP, kind) - << "PI or REGEXP_EMPTY or REGEXP_SIGMA"; + << "PI, REGEXP_EMPTY, REGEXP_SIGMA or SEP_EMP"; //////// all checks before this line Node res; cvc5::Kind k = extToIntKind(kind); @@ -5822,6 +5822,18 @@ Term Solver::mkEmptyBag(const Sort& sort) const CVC5_API_TRY_CATCH_END; } +Term Solver::mkSepEmp() const +{ + CVC5_API_TRY_CATCH_BEGIN; + //////// all checks before this line + Node res = getNodeManager()->mkNullaryOperator(d_nodeMgr->booleanType(), + cvc5::Kind::SEP_EMP); + (void)res.getType(true); /* kick off type checking */ + return Term(this, res); + //////// + CVC5_API_TRY_CATCH_END; +} + Term Solver::mkSepNil(const Sort& sort) const { CVC5_API_TRY_CATCH_BEGIN; @@ -6030,10 +6042,11 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const CVC5_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "a value > 0"; CVC5_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "a value > 0"; uint32_t bw = exp + sig; - CVC5_API_ARG_CHECK_EXPECTED(bw == val.getSort().getBVSize(), val) + CVC5_API_ARG_CHECK_EXPECTED(bw == val.d_node->getType().getBitVectorSize(), + val) << "a bit-vector constant with bit-width '" << bw << "'"; CVC5_API_ARG_CHECK_EXPECTED( - val.getSort().isBitVector() && val.d_node->isConst(), val) + val.d_node->getType().isBitVector() && val.d_node->isConst(), val) << "bit-vector constant"; //////// all checks before this line return mkValHelper<cvc5::FloatingPoint>( @@ -7204,7 +7217,7 @@ std::string Solver::getProof(void) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(d_slv->getOptions().smt.produceProofs) - << "Cannot get proof explicitly enabled (try --produce-proofs)"; + << "Cannot get proof unless proofs are enabled (try --produce-proofs)"; CVC5_API_RECOVERABLE_CHECK(d_slv->getSmtMode() == SmtMode::UNSAT) << "Cannot get proof unless in unsat mode."; return d_slv->getProof(); @@ -7455,6 +7468,8 @@ bool Solver::getAbduct(const Term& conj, Term& output) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(conj); + CVC5_API_CHECK(d_slv->getOptions().smt.produceAbducts) + << "Cannot get abduct unless abducts are enabled (try --produce-abducts)"; //////// all checks before this line Node result; bool success = d_slv->getAbduct(*conj.d_node, result); @@ -7471,6 +7486,8 @@ bool Solver::getAbduct(const Term& conj, Grammar& grammar, Term& output) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(conj); + CVC5_API_CHECK(d_slv->getOptions().smt.produceAbducts) + << "Cannot get abduct unless abducts are enabled (try --produce-abducts)"; //////// all checks before this line Node result; bool success = diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 3db581db6..c46b00d0e 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -700,19 +700,19 @@ class CVC5_EXPORT Sort /** * @return the bit-width of the bit-vector sort */ - uint32_t getBVSize() const; + uint32_t getBitVectorSize() const; /* Floating-point sort ------------------------------------------------- */ /** * @return the bit-width of the exponent of the floating-point sort */ - uint32_t getFPExponentSize() const; + uint32_t getFloatingPointExponentSize() const; /** * @return the width of the significand of the floating-point sort */ - uint32_t getFPSignificandSize() const; + uint32_t getFloatingPointSignificandSize() const; /* Datatype sort ------------------------------------------------------- */ @@ -1353,6 +1353,8 @@ class CVC5_EXPORT Term std::pair<int64_t, uint64_t> getReal64Value() const; /** * @return true if the term is a rational value. + * + * Note that a term of kind PI is not considered to be a real value. */ bool isRealValue() const; /** @@ -1448,6 +1450,17 @@ class CVC5_EXPORT Term /** * @return true if the term is a set value. + * + * A term is a set value if it is considered to be a (canonical) constant set + * value. A canonical set value is one whose AST is: + * ``` + * (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n)))) + * ``` + * where `c1 ... cn` are values ordered by id such that `c1 > ... > cn` (see + * also @ref Term::operator>(const Term&) const). + * + * Note that a universe set term (kind UNIVERSE_SET) is not considered to be + * a set value. */ bool isSetValue() const; /** @@ -2464,7 +2477,7 @@ class CVC5_EXPORT Grammar /** * Allow \p ntSymbol to be any input variable to corresponding * synth-fun/synth-inv with the same sort as \p ntSymbol. - * @param ntSymbol the non-terminal allowed to be any input constant + * @param ntSymbol the non-terminal allowed to be any input variable */ void addAnyVariable(const Term& ntSymbol); @@ -3431,6 +3444,12 @@ class CVC5_EXPORT Solver Term mkEmptyBag(const Sort& sort) const; /** + * Create a separation logic empty term. + * @return the separation logic empty term + */ + Term mkSepEmp() const; + + /** * Create a separation logic nil term. * @param sort the sort of the nil term * @return the separation logic nil term diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 0ff05022f..fe87df934 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -766,6 +766,9 @@ enum CVC5_EXPORT Kind : int32_t /** * Pi constant. * + * Note that PI is considered a special symbol of sort Real, but is not + * a real value, i.e., `Term::isRealValue() const` will return false. + * * Create with: * - `Solver::mkPi() const` * - `Solver::mkTerm(Kind kind) const` @@ -2228,6 +2231,10 @@ enum CVC5_EXPORT Kind : int32_t * Finite universe set. * All set variables must be interpreted as subsets of it. * + * Note that UNIVERSE_SET is considered a special symbol of the theory of + * sets and is not considered as a set value, + * i.e., `Term::isSetValue() const` will return false. + * * Create with: * - `Solver::mkUniverseSet(const Sort& sort) const` */ diff --git a/src/api/java/cvc5/Solver.java b/src/api/java/cvc5/Solver.java index b0bee500c..c46d60aee 100644 --- a/src/api/java/cvc5/Solver.java +++ b/src/api/java/cvc5/Solver.java @@ -882,6 +882,18 @@ public class Solver implements IPointer private native long mkEmptyBag(long pointer, long sortPointer); /** + * Create a separation logic empty term. + * @return the separation logic empty term + */ + public Term mkSepEmp() + { + long termPointer = mkSepEmp(pointer); + return new Term(this, termPointer); + } + + private native long mkSepEmp(long pointer); + + /** * Create a separation logic nil term. * @param sort the sort of the nil term * @return the separation logic nil term diff --git a/src/api/java/cvc5/Sort.java b/src/api/java/cvc5/Sort.java index f1f541e35..434c07424 100644 --- a/src/api/java/cvc5/Sort.java +++ b/src/api/java/cvc5/Sort.java @@ -725,34 +725,34 @@ public class Sort extends AbstractPointer implements Comparable<Sort> /** * @return the bit-width of the bit-vector sort */ - public int getBVSize() + public int getBitVectorSize() { - return getBVSize(pointer); + return getBitVectorSize(pointer); } - private native int getBVSize(long pointer); + private native int getBitVectorSize(long pointer); /* Floating-point sort ------------------------------------------------- */ /** * @return the bit-width of the exponent of the floating-point sort */ - public int getFPExponentSize() + public int getFloatingPointExponentSize() { - return getFPExponentSize(pointer); + return getFloatingPointExponentSize(pointer); } - private native int getFPExponentSize(long pointer); + private native int getFloatingPointExponentSize(long pointer); /** * @return the width of the significand of the floating-point sort */ - public int getFPSignificandSize() + public int getFloatingPointSignificandSize() { - return getFPSignificandSize(pointer); + return getFloatingPointSignificandSize(pointer); } - private native int getFPSignificandSize(long pointer); + private native int getFloatingPointSignificandSize(long pointer); /* Datatype sort ------------------------------------------------------- */ diff --git a/src/api/java/jni/cvc5_Solver.cpp b/src/api/java/jni/cvc5_Solver.cpp index c28ea412f..53c050c96 100644 --- a/src/api/java/jni/cvc5_Solver.cpp +++ b/src/api/java/jni/cvc5_Solver.cpp @@ -1061,6 +1061,22 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkEmptyBag(JNIEnv* env, /* * Class: cvc5_Solver + * Method: mkSepEmp + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSepEmp(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* retPointer = new Term(solver->mkSepEmp()); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver * Method: mkSepNil * Signature: (JJ)J */ @@ -2591,4 +2607,4 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullDatatypeDecl(JNIEnv* env, DatatypeDecl* ret = new DatatypeDecl(); return reinterpret_cast<jlong>(ret); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); -}
\ No newline at end of file +} diff --git a/src/api/java/jni/cvc5_Sort.cpp b/src/api/java/jni/cvc5_Sort.cpp index a2754f032..36ba81249 100644 --- a/src/api/java/jni/cvc5_Sort.cpp +++ b/src/api/java/jni/cvc5_Sort.cpp @@ -978,46 +978,44 @@ JNIEXPORT jint JNICALL Java_cvc5_Sort_getSortConstructorArity(JNIEnv* env, /* * Class: cvc5_Sort - * Method: getBVSize + * Method: getBitVectorSize * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Sort_getBVSize(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL Java_cvc5_Sort_getBitVectorSize(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); - return static_cast<jint>(current->getBVSize()); + return static_cast<jint>(current->getBitVectorSize()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } /* * Class: cvc5_Sort - * Method: getFPExponentSize + * Method: getFloatingPointExponentSize * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Sort_getFPExponentSize(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL +Java_cvc5_Sort_getFloatingPointExponentSize(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); - return static_cast<jint>(current->getFPExponentSize()); + return static_cast<jint>(current->getFloatingPointExponentSize()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } /* * Class: cvc5_Sort - * Method: getFPSignificandSize + * Method: getFloatingPointSignificandSize * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Sort_getFPSignificandSize(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL Java_cvc5_Sort_getFloatingPointSignificandSize( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); - return static_cast<jint>(current->getFPSignificandSize()); + return static_cast<jint>(current->getFloatingPointSignificandSize()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index ef9971c20..02b572120 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -219,6 +219,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Term mkRegexpSigma() except + Term mkEmptySet(Sort s) except + Term mkEmptyBag(Sort s) except + + Term mkSepEmp() except + Term mkSepNil(Sort sort) except + Term mkString(const string& s) except + Term mkString(const wstring& s) except + @@ -308,6 +309,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": bint operator>(const Sort&) except + bint operator<=(const Sort&) except + bint operator>=(const Sort&) except + + bint isNull() except + bint isBoolean() except + bint isInteger() except + bint isReal() except + @@ -321,6 +323,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": bint isConstructor() except + bint isSelector() except + bint isTester() except + + bint isUpdater() except + bint isFunction() except + bint isPredicate() except + bint isTuple() except + @@ -357,9 +360,9 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": vector[Sort] getUninterpretedSortParamSorts() except + string getSortConstructorName() except + size_t getSortConstructorArity() except + - uint32_t getBVSize() except + - uint32_t getFPExponentSize() except + - uint32_t getFPSignificandSize() except + + uint32_t getBitVectorSize() except + + uint32_t getFloatingPointExponentSize() except + + uint32_t getFloatingPointSignificandSize() except + vector[Sort] getDatatypeParamSorts() except + size_t getDatatypeArity() except + size_t getTupleLength() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 0f6b54dc6..4627859b9 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -95,7 +95,10 @@ cdef c_hash[c_Term] ctermhash = c_hash[c_Term]() cdef class Datatype: - """Wrapper class for :cpp:class:`cvc5::api::Datatype`.""" + """ + A cvc5 datatype. + Wrapper class for :cpp:class:`cvc5::api::Datatype`. + """ cdef c_Datatype cd cdef Solver solver def __cinit__(self, Solver solver): @@ -114,7 +117,7 @@ cdef class Datatype: def getConstructor(self, str name): """ :param name: the name of the constructor. - :return: a constructor by name. + :return: a constructor by name. """ cdef DatatypeConstructor dc = DatatypeConstructor(self.solver) dc.cdc = self.cd.getConstructor(name.encode()) @@ -151,34 +154,35 @@ cdef class Datatype: return self.cd.getNumConstructors() def isParametric(self): - """:return: whether this datatype is parametric.""" + """:return: True if this datatype is parametric.""" return self.cd.isParametric() def isCodatatype(self): - """:return: whether this datatype corresponds to a co-datatype.""" + """:return: True if this datatype corresponds to a co-datatype.""" return self.cd.isCodatatype() def isTuple(self): - """:return: whether this datatype corresponds to a tuple.""" + """:return: True if this datatype corresponds to a tuple.""" return self.cd.isTuple() def isRecord(self): - """:return: whether this datatype corresponds to a record.""" + """:return: True if this datatype corresponds to a record.""" return self.cd.isRecord() def isFinite(self): - """:return: whether this datatype is finite.""" + """:return: True if this datatype is finite.""" return self.cd.isFinite() def isWellFounded(self): - """:return: whether this datatype is well-founded (see :cpp:func:`Datatype::isWellFounded() <cvc5::api::Datatype::isWellFounded>`).""" + """:return: True if this datatype is well-founded (see :cpp:func:`Datatype::isWellFounded() <cvc5::api::Datatype::isWellFounded>`).""" return self.cd.isWellFounded() def hasNestedRecursion(self): - """:return: whether this datatype has nested recursion (see :cpp:func:`Datatype::hasNestedRecursion() <cvc5::api::Datatype::hasNestedRecursion>`).""" + """:return: True if this datatype has nested recursion (see :cpp:func:`Datatype::hasNestedRecursion() <cvc5::api::Datatype::hasNestedRecursion>`).""" return self.cd.hasNestedRecursion() def isNull(self): + """:return: True if this Datatype is a null object.""" return self.cd.isNull() def __str__(self): @@ -195,7 +199,10 @@ cdef class Datatype: cdef class DatatypeConstructor: - """Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructor`.""" + """ + A cvc5 datatype constructor. + Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructor`. + """ cdef c_DatatypeConstructor cdc cdef Solver solver def __cinit__(self, Solver solver): @@ -270,6 +277,7 @@ cdef class DatatypeConstructor: return term def isNull(self): + """:return: True if this DatatypeConstructor is a null object.""" return self.cdc.isNull() def __str__(self): @@ -286,7 +294,10 @@ cdef class DatatypeConstructor: cdef class DatatypeConstructorDecl: - """Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructorDecl`.""" + """ + A cvc5 datatype constructor declaration. + Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructorDecl`. + """ cdef c_DatatypeConstructorDecl cddc cdef Solver solver @@ -311,6 +322,7 @@ cdef class DatatypeConstructorDecl: self.cddc.addSelectorSelf(name.encode()) def isNull(self): + """:return: True if this DatatypeConstructorDecl is a null object.""" return self.cddc.isNull() def __str__(self): @@ -321,7 +333,10 @@ cdef class DatatypeConstructorDecl: cdef class DatatypeDecl: - """Wrapper class for :cpp:class:`cvc5::api::DatatypeDecl`.""" + """ + A cvc5 datatype declaration. + Wrapper class for :cpp:class:`cvc5::api::DatatypeDecl`. + """ cdef c_DatatypeDecl cdd cdef Solver solver def __cinit__(self, Solver solver): @@ -354,6 +369,7 @@ cdef class DatatypeDecl: return self.cdd.getName().decode() def isNull(self): + """:return: True if this DatatypeDecl is a null object.""" return self.cdd.isNull() def __str__(self): @@ -364,7 +380,10 @@ cdef class DatatypeDecl: cdef class DatatypeSelector: - """Wrapper class for :cpp:class:`cvc5::api::DatatypeSelector`.""" + """ + A cvc5 datatype selector. + Wrapper class for :cpp:class:`cvc5::api::DatatypeSelector`. + """ cdef c_DatatypeSelector cds cdef Solver solver def __cinit__(self, Solver solver): @@ -402,6 +421,7 @@ cdef class DatatypeSelector: return sort def isNull(self): + """:return: True if this DatatypeSelector is a null object.""" return self.cds.isNull() def __str__(self): @@ -412,6 +432,13 @@ cdef class DatatypeSelector: cdef class Op: + """ + A cvc5 operator. + An operator is a term that represents certain operators, + instantiated with its required parameters, e.g., + a term of kind :cpp:enumerator:`BITVECTOR_EXTRACT`. + Wrapper class for :cpp:class:`cvc5::api::Op`. + """ cdef c_Op cop cdef Solver solver def __cinit__(self, Solver solver): @@ -434,18 +461,33 @@ cdef class Op: return cophash(self.cop) def getKind(self): + """ + :return: the kind of this operator. + """ return kind(<int> self.cop.getKind()) def isIndexed(self): + """ + :return: True iff this operator is indexed. + """ return self.cop.isIndexed() def isNull(self): + """ + :return: True iff this operator is a null term. + """ return self.cop.isNull() def getNumIndices(self): + """ + :return: number of indices of this op. + """ return self.cop.getNumIndices() def getIndices(self): + """ + :return: the indices used to create this Op (see :cpp:func:`Op::getIndices() <cvc5::api::Op::getIndices>`). + """ indices = None try: indices = self.cop.getIndices[string]().decode() @@ -468,6 +510,10 @@ cdef class Op: return indices cdef class Grammar: + """ + A Sygus Grammar. + Wrapper class for :cpp:class:`cvc5::api::Grammar`. + """ cdef c_Grammar cgrammar cdef Solver solver def __cinit__(self, Solver solver): @@ -475,46 +521,100 @@ cdef class Grammar: self.cgrammar = c_Grammar() def addRule(self, Term ntSymbol, Term rule): + """ + Add ``rule`` to the set of rules corresponding to ``ntSymbol``. + + :param ntSymbol: the non-terminal to which the rule is added. + :param rule: the rule to add. + """ self.cgrammar.addRule(ntSymbol.cterm, rule.cterm) def addAnyConstant(self, Term ntSymbol): + """ + Allow ``ntSymbol`` to be an arbitrary constant. + + :param ntSymbol: the non-terminal allowed to be constant. + """ self.cgrammar.addAnyConstant(ntSymbol.cterm) def addAnyVariable(self, Term ntSymbol): + """ + Allow ``ntSymbol`` to be any input variable to corresponding synth-fun/synth-inv with the same sort as ``ntSymbol``. + + :param ntSymbol: the non-terminal allowed to be any input variable. + """ self.cgrammar.addAnyVariable(ntSymbol.cterm) def addRules(self, Term ntSymbol, rules): + """ + Add ``ntSymbol`` to the set of rules corresponding to ``ntSymbol``. + + :param ntSymbol: the non-terminal to which the rules are added. + :param rules: the rules to add. + """ cdef vector[c_Term] crules for r in rules: crules.push_back((<Term?> r).cterm) self.cgrammar.addRules(ntSymbol.cterm, crules) cdef class Result: + """ + Encapsulation of a three-valued solver result, with explanations. + Wrapper class for :cpp:class:`cvc5::api::Result`. + """ cdef c_Result cr def __cinit__(self): # gets populated by solver self.cr = c_Result() def isNull(self): + """ + :return: True if Result is empty, i.e., a nullary Result, + and not an actual result returned from a :cpp:func:`Solver::checkSat() <cvc5::api::Solver::checkSat>` (and friends) query. + """ return self.cr.isNull() def isSat(self): + """ + :return: True if query was a satisfiable :cpp:func:`Solver::checkSat() <cvc5::api::Solver::checkSat>` or :cpp:func:`Solver::checkSatAssuming() <cvc5::api::Solver::checkSatAssuming>` query. + """ return self.cr.isSat() def isUnsat(self): + """ + :return: True if query was an usatisfiable :cpp:func:`Solver::checkSat() <cvc5::api::Solver::checkSat>` or :cpp:func:`Solver::checkSatAssuming() <cvc5::api::Solver::checkSatAssuming>` query. + """ return self.cr.isUnsat() def isSatUnknown(self): + """ + :return: True if query was a :cpp:func:`Solver::checkSat() <cvc5::api::Solver::checkSat>` or :cpp:func:`Solver::checkSatAssuming() <cvc5::api::Solver::checkSatAssuming>` query and cvc5 was not able to determine (un)satisfiability. + """ return self.cr.isSatUnknown() def isEntailed(self): + """ + :return: True if corresponding query was an entailed :cpp:func:`Solver::checkEntailed() <cvc5::api::Solver::checkEntailed>` query. + """ return self.cr.isEntailed() def isNotEntailed(self): + """ + :return: True if corresponding query was a :cpp:func:`Solver::checkEntailed() <cvc5::api::Solver::checkEntailed>` query that is not entailed. + """ return self.cr.isNotEntailed() def isEntailmentUnknown(self): + """ + :return: True if query was a :cpp:func:`Solver::checkEntailed() <cvc5::api::Solver::checkEntailed>` query query and cvc5 was not able to determine if it is entailed. + """ return self.cr.isEntailmentUnknown() + + def getUnknownExplanation(self): + """ + :return: an explanation for an unknown query result. + """ + return UnknownExplanation(<int> self.cr.getUnknownExplanation()) def __eq__(self, Result other): return self.cr == other.cr @@ -522,9 +622,6 @@ cdef class Result: def __ne__(self, Result other): return self.cr != other.cr - def getUnknownExplanation(self): - return UnknownExplanation(<int> self.cr.getUnknownExplanation()) - def __str__(self): return self.cr.toString().decode() @@ -533,6 +630,20 @@ cdef class Result: cdef class RoundingMode: + """ + Rounding modes for floating-point numbers. + + For many floating-point operations, infinitely precise results may not be + representable with the number of available bits. Thus, the results are + rounded in a certain way to one of the representable floating-point numbers. + + These rounding modes directly follow the SMT-LIB theory for floating-point + arithmetic, which in turn is based on IEEE Standard 754 :cite:`IEEE754`. + The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE + Standard 754. + + Wrapper class for :cpp:enum:`cvc5::api::RoundingMode`. + """ cdef c_RoundingMode crm cdef str name def __cinit__(self, int rm): @@ -557,6 +668,9 @@ cdef class RoundingMode: cdef class UnknownExplanation: + """ + Wrapper class for :cpp:enum:`cvc5::api::Result::UnknownExplanation`. + """ cdef c_UnknownExplanation cue cdef str name def __cinit__(self, int ue): @@ -907,9 +1021,10 @@ cdef class Solver: - ``Op mkOp(Kind kind, const string& arg)`` - ``Op mkOp(Kind kind, uint32_t arg)`` - ``Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1)`` + - ``Op mkOp(Kind kind, [uint32_t arg0, ...])`` (used for the TupleProject kind) """ cdef Op op = Op(self) - cdef vector[int] v + cdef vector[uint32_t] v if len(args) == 0: op.cop = self.csolver.mkOp(k.k) @@ -922,7 +1037,10 @@ cdef class Solver: op.cop = self.csolver.mkOp(k.k, <int?> args[0]) elif isinstance(args[0], list): for a in args[0]: - v.push_back((<int?> a)) + if a < 0 or a >= 2 ** 31: + raise ValueError("Argument {} must fit in a uint32_t".format(a)) + + v.push_back((<uint32_t?> a)) op.cop = self.csolver.mkOp(k.k, <const vector[uint32_t]&> v) else: raise ValueError("Unsupported signature" @@ -1050,6 +1168,15 @@ cdef class Solver: term.cterm = self.csolver.mkEmptyBag(s.csort) return term + def mkSepEmp(self): + """Create a separation logic empty term. + + :return: the separation logic empty term + """ + cdef Term term = Term(self) + term.cterm = self.csolver.mkSepEmp() + return term + def mkSepNil(self, Sort sort): """Create a separation logic nil term. @@ -2087,6 +2214,9 @@ cdef class Sort: def __hash__(self): return csorthash(self.csort) + def isNull(self): + return self.csort.isNull() + def isBoolean(self): return self.csort.isBoolean() @@ -2126,6 +2256,9 @@ cdef class Sort: def isTester(self): return self.csort.isTester() + def isUpdater(self): + return self.csort.isUpdater() + def isFunction(self): return self.csort.isFunction() @@ -2278,14 +2411,14 @@ cdef class Sort: def getSortConstructorArity(self): return self.csort.getSortConstructorArity() - def getBVSize(self): - return self.csort.getBVSize() + def getBitVectorSize(self): + return self.csort.getBitVectorSize() - def getFPExponentSize(self): - return self.csort.getFPExponentSize() + def getFloatingPointExponentSize(self): + return self.csort.getFloatingPointExponentSize() - def getFPSignificandSize(self): - return self.csort.getFPSignificandSize() + def getFloatingPointSignificandSize(self): + return self.csort.getFloatingPointSignificandSize() def getDatatypeParamSorts(self): param_sorts = [] diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index e73960676..45ce01edb 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -26,6 +26,8 @@ libcvc5_add_sources( bound_var_manager.h cardinality_constraint.cpp cardinality_constraint.h + codatatype_bound_variable.cpp + codatatype_bound_variable.h emptyset.cpp emptyset.h emptybag.cpp @@ -95,6 +97,8 @@ libcvc5_add_sources( sygus_datatype.h uninterpreted_constant.cpp uninterpreted_constant.h + variadic_trie.cpp + variadic_trie.h ) libcvc5_add_sources(GENERATED diff --git a/src/expr/codatatype_bound_variable.cpp b/src/expr/codatatype_bound_variable.cpp new file mode 100644 index 000000000..a6a9d8e3e --- /dev/null +++ b/src/expr/codatatype_bound_variable.cpp @@ -0,0 +1,113 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Representation of bound variables in codatatype values + */ + +#include "expr/codatatype_bound_variable.h" + +#include <algorithm> +#include <iostream> +#include <sstream> +#include <string> + +#include "base/check.h" +#include "expr/type_node.h" + +using namespace std; + +namespace cvc5 { + +CodatatypeBoundVariable::CodatatypeBoundVariable(const TypeNode& type, + Integer index) + : d_type(new TypeNode(type)), d_index(index) +{ + PrettyCheckArgument(type.isCodatatype(), + type, + "codatatype bound variables can only be created for " + "codatatype sorts, not `%s'", + type.toString().c_str()); + PrettyCheckArgument( + index >= 0, + index, + "index >= 0 required for codatatype bound variable index, not `%s'", + index.toString().c_str()); +} + +CodatatypeBoundVariable::~CodatatypeBoundVariable() {} + +CodatatypeBoundVariable::CodatatypeBoundVariable( + const CodatatypeBoundVariable& other) + : d_type(new TypeNode(other.getType())), d_index(other.getIndex()) +{ +} + +const TypeNode& CodatatypeBoundVariable::getType() const { return *d_type; } +const Integer& CodatatypeBoundVariable::getIndex() const { return d_index; } +bool CodatatypeBoundVariable::operator==( + const CodatatypeBoundVariable& cbv) const +{ + return getType() == cbv.getType() && d_index == cbv.d_index; +} +bool CodatatypeBoundVariable::operator!=( + const CodatatypeBoundVariable& cbv) const +{ + return !(*this == cbv); +} + +bool CodatatypeBoundVariable::operator<( + const CodatatypeBoundVariable& cbv) const +{ + return getType() < cbv.getType() + || (getType() == cbv.getType() && d_index < cbv.d_index); +} +bool CodatatypeBoundVariable::operator<=( + const CodatatypeBoundVariable& cbv) const +{ + return getType() < cbv.getType() + || (getType() == cbv.getType() && d_index <= cbv.d_index); +} +bool CodatatypeBoundVariable::operator>( + const CodatatypeBoundVariable& cbv) const +{ + return !(*this <= cbv); +} +bool CodatatypeBoundVariable::operator>=( + const CodatatypeBoundVariable& cbv) const +{ + return !(*this < cbv); +} + +std::ostream& operator<<(std::ostream& out, const CodatatypeBoundVariable& cbv) +{ + std::stringstream ss; + ss << cbv.getType(); + std::string st(ss.str()); + // must remove delimiting quotes from the name of the type + // this prevents us from printing symbols like |@cbv_|T|_n| + std::string q("|"); + size_t pos; + while ((pos = st.find(q)) != std::string::npos) + { + st.replace(pos, 1, ""); + } + return out << "cbv_" << st.c_str() << "_" << cbv.getIndex(); +} + +size_t CodatatypeBoundVariableHashFunction::operator()( + const CodatatypeBoundVariable& cbv) const +{ + return std::hash<TypeNode>()(cbv.getType()) + * IntegerHashFunction()(cbv.getIndex()); +} + +} // namespace cvc5 diff --git a/src/expr/codatatype_bound_variable.h b/src/expr/codatatype_bound_variable.h new file mode 100644 index 000000000..9af8476d5 --- /dev/null +++ b/src/expr/codatatype_bound_variable.h @@ -0,0 +1,91 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Representation of bound variables in codatatype values + */ + +#include "cvc5_public.h" + +#ifndef CVC5__EXPR__CODATATYPE_BOUND_VARIABLE_H +#define CVC5__EXPR__CODATATYPE_BOUND_VARIABLE_H + +#include <iosfwd> +#include <memory> + +#include "util/integer.h" + +namespace cvc5 { + +class TypeNode; + +/** + * In theory, codatatype values are represented in using a MU-notation form, + * where recursive values may contain free constants indexed by their de Bruijn + * indices. This is sometimes written: + * MU x. (cons 0 x). + * where the MU binder is label for a term position, which x references. + * Instead of constructing an explicit MU binder (which is problematic for + * canonicity), we use de Bruijn indices for representing bound variables, + * whose index indicates the level in which it is nested. For example, we + * represent the above value as: + * (cons 0 @cbv_0) + * In the above value, @cbv_0 is a pointer to its direct parent, so the above + * value represents the infinite list (cons 0 (cons 0 (cons 0 ... ))). + * Another example, the value: + * (cons 0 (cons 1 @cbv_1)) + * @cbv_1 is pointer to the top most node of this value, so this is value + * represents the infinite list (cons 0 (cons 1 (cons 0 (cons 1 ...)))). The + * value: + * (cons 0 (cons 1 @cbv_0)) + * on the other hand represents the lasso: + * (cons 0 (cons 1 (cons 1 (cons 1 ... )))) + * + * This class is used for representing the indexed bound variables in the above + * values. It is considered a constant (isConst is true). However, constants + * of codatatype type are normalized by the rewriter (see datatypes rewriter + * normalizeCodatatypeConstant) to ensure their canonicity, via a variant + * of Hopcroft's algorithm. + */ +class CodatatypeBoundVariable +{ + public: + CodatatypeBoundVariable(const TypeNode& type, Integer index); + ~CodatatypeBoundVariable(); + + CodatatypeBoundVariable(const CodatatypeBoundVariable& other); + + const TypeNode& getType() const; + const Integer& getIndex() const; + bool operator==(const CodatatypeBoundVariable& cbv) const; + bool operator!=(const CodatatypeBoundVariable& cbv) const; + bool operator<(const CodatatypeBoundVariable& cbv) const; + bool operator<=(const CodatatypeBoundVariable& cbv) const; + bool operator>(const CodatatypeBoundVariable& cbv) const; + bool operator>=(const CodatatypeBoundVariable& cbv) const; + + private: + std::unique_ptr<TypeNode> d_type; + const Integer d_index; +}; +std::ostream& operator<<(std::ostream& out, const CodatatypeBoundVariable& cbv); + +/** + * Hash function for codatatype bound variables. + */ +struct CodatatypeBoundVariableHashFunction +{ + size_t operator()(const CodatatypeBoundVariable& cbv) const; +}; + +} // namespace cvc5 + +#endif /* CVC5__UNINTERPRETED_CONSTANT_H */ diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp index ef354568d..709ec112f 100644 --- a/src/expr/uninterpreted_constant.cpp +++ b/src/expr/uninterpreted_constant.cpp @@ -31,7 +31,11 @@ UninterpretedConstant::UninterpretedConstant(const TypeNode& type, Integer index) : d_type(new TypeNode(type)), d_index(index) { - //PrettyCheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str()); + PrettyCheckArgument(type.isSort(), + type, + "uninterpreted constants can only be created for " + "uninterpreted sorts, not `%s'", + type.toString().c_str()); PrettyCheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str()); } diff --git a/src/expr/variadic_trie.cpp b/src/expr/variadic_trie.cpp new file mode 100644 index 000000000..bd27780e9 --- /dev/null +++ b/src/expr/variadic_trie.cpp @@ -0,0 +1,55 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Variadic trie utility + */ + +#include "expr/variadic_trie.h" + +namespace cvc5 { + +bool VariadicTrie::add(Node n, const std::vector<Node>& i) +{ + VariadicTrie* curr = this; + for (const Node& ic : i) + { + curr = &(curr->d_children[ic]); + } + if (curr->d_data.isNull()) + { + curr->d_data = n; + return true; + } + return false; +} + +bool VariadicTrie::hasSubset(const std::vector<Node>& is) const +{ + if (!d_data.isNull()) + { + return true; + } + for (const std::pair<const Node, VariadicTrie>& p : d_children) + { + Node n = p.first; + if (std::find(is.begin(), is.end(), n) != is.end()) + { + if (p.second.hasSubset(is)) + { + return true; + } + } + } + return false; +} + +} // namespace cvc5 diff --git a/src/expr/variadic_trie.h b/src/expr/variadic_trie.h new file mode 100644 index 000000000..aa7ca1e37 --- /dev/null +++ b/src/expr/variadic_trie.h @@ -0,0 +1,54 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Variadic trie utility + */ + +#include "cvc5_private.h" + +#ifndef CVC5__EXPR__VARIADIC_TRIE_H +#define CVC5__EXPR__VARIADIC_TRIE_H + +#include <map> +#include <vector> + +#include "expr/node.h" + +namespace cvc5 { + +/** + * A trie that stores data at undetermined depth. Storing data at + * undetermined depth is in contrast to the NodeTrie (expr/node_trie.h), which + * assumes all data is stored at a fixed depth. + * + * Since data can be stored at any depth, we require both a d_children field + * and a d_data field. + */ +class VariadicTrie +{ + public: + /** the children of this node */ + std::map<Node, VariadicTrie> d_children; + /** the data at this node */ + Node d_data; + /** + * Add data with identifier n indexed by i, return true if data is not already + * stored at the node indexed by i. + */ + bool add(Node n, const std::vector<Node>& i); + /** Is there any data in this trie that is indexed by any subset of is? */ + bool hasSubset(const std::vector<Node>& is) const; +}; + +} // namespace cvc5 + +#endif /* CVC5__EXPR__VARIADIC_TRIE_H */ diff --git a/src/options/managed_streams.cpp b/src/options/managed_streams.cpp index 81bb242cf..90090df25 100644 --- a/src/options/managed_streams.cpp +++ b/src/options/managed_streams.cpp @@ -100,34 +100,54 @@ std::istream* openIStream(const std::string& filename) } } // namespace detail -std::ostream* ManagedErr::defaultValue() const { return &std::cerr; } +ManagedErr::ManagedErr() : ManagedStream(&std::cerr, "stderr") {} bool ManagedErr::specialCases(const std::string& value) { if (value == "stderr" || value == "--") { - d_stream.reset(); + d_nonowned = &std::cerr; + d_owned.reset(); + d_description = "stderr"; + return true; + } + else if (value == "stdout") + { + d_nonowned = &std::cout; + d_owned.reset(); + d_description = "stdout"; return true; } return false; } -std::istream* ManagedIn::defaultValue() const { return &std::cin; } +ManagedIn::ManagedIn() : ManagedStream(&std::cin, "stdin") {} bool ManagedIn::specialCases(const std::string& value) { if (value == "stdin" || value == "--") { - d_stream.reset(); + d_nonowned = &std::cin; + d_owned.reset(); + d_description = "stdin"; return true; } return false; } -std::ostream* ManagedOut::defaultValue() const { return &std::cout; } +ManagedOut::ManagedOut() : ManagedStream(&std::cout, "stdout") {} bool ManagedOut::specialCases(const std::string& value) { if (value == "stdout" || value == "--") { - d_stream.reset(); + d_nonowned = &std::cout; + d_owned.reset(); + d_description = "stdout"; + return true; + } + else if (value == "stderr") + { + d_nonowned = &std::cerr; + d_owned.reset(); + d_description = "stderr"; return true; } return false; diff --git a/src/options/managed_streams.h b/src/options/managed_streams.h index 56bb21c2e..cf1820de6 100644 --- a/src/options/managed_streams.h +++ b/src/options/managed_streams.h @@ -50,7 +50,8 @@ template <typename Stream> class ManagedStream { public: - ManagedStream() {} + ManagedStream(Stream* nonowned, std::string description) + : d_nonowned(nonowned), d_description(std::move(description)) {} virtual ~ManagedStream() {} /** @@ -62,11 +63,15 @@ class ManagedStream if (specialCases(value)) return; if constexpr (std::is_same<Stream, std::ostream>::value) { - d_stream.reset(detail::openOStream(value)); + d_nonowned = nullptr; + d_owned.reset(detail::openOStream(value)); + d_description = value; } else if constexpr (std::is_same<Stream, std::istream>::value) { - d_stream.reset(detail::openIStream(value)); + d_nonowned = nullptr; + d_owned.reset(detail::openIStream(value)); + d_description = value; } } @@ -75,12 +80,14 @@ class ManagedStream operator Stream&() const { return *getPtr(); } operator Stream*() const { return getPtr(); } + const std::string& description() const { return d_description; } + protected: - std::shared_ptr<Stream> d_stream; + Stream* d_nonowned; + std::shared_ptr<Stream> d_owned; + std::string d_description = "<null>"; private: - /** Returns the value to be used if d_stream is not set. */ - virtual Stream* defaultValue() const = 0; /** * Check if there is a special case for this value. If so, the implementation * should set d_stream appropriately and return true to skip the default @@ -88,18 +95,18 @@ class ManagedStream */ virtual bool specialCases(const std::string& value) = 0; - /** Return the pointer, either from d_stream of from defaultValue(). */ + /** Return the pointer, either from d_nonowned or d_owned. */ Stream* getPtr() const { - if (d_stream) return d_stream.get(); - return defaultValue(); + if (d_nonowned != nullptr) return d_nonowned; + return d_owned.get(); } }; template <typename Stream> std::ostream& operator<<(std::ostream& os, const ManagedStream<Stream>& ms) { - return os << "ManagedStream"; + return os << ms.description(); } /** @@ -108,7 +115,10 @@ std::ostream& operator<<(std::ostream& os, const ManagedStream<Stream>& ms) */ class ManagedErr : public ManagedStream<std::ostream> { - std::ostream* defaultValue() const override final; + public: + ManagedErr(); + + private: bool specialCases(const std::string& value) override final; }; @@ -118,7 +128,10 @@ class ManagedErr : public ManagedStream<std::ostream> */ class ManagedIn : public ManagedStream<std::istream> { - std::istream* defaultValue() const override final; + public: + ManagedIn(); + + private: bool specialCases(const std::string& value) override final; }; @@ -128,7 +141,10 @@ class ManagedIn : public ManagedStream<std::istream> */ class ManagedOut : public ManagedStream<std::ostream> { - std::ostream* defaultValue() const override final; + public: + ManagedOut(); + + private: bool specialCases(const std::string& value) override final; }; diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index a8f631de6..57f8b64e6 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -480,17 +480,6 @@ def generate_module_option_names(module): 'static constexpr const char* {name}__name = "{long_name}";', relevant) -def generate_module_setdefaults_decl(module): - res = [] - for option in module.options: - if option.name is None: - continue - funcname = option.name[0].capitalize() + option.name[1:] - res.append('void setDefault{}(Options& opts, {} value);'.format( - funcname, option.type)) - return '\n'.join(res) - - ################################################################################ # for options/<module>.cpp @@ -581,27 +570,6 @@ def generate_module_mode_impl(module): return '\n'.join(res) -TPL_SETDEFAULT_IMPL = '''void setDefault{capname}(Options& opts, {type} value) -{{ - if (!opts.{module}.{name}WasSetByUser) opts.{module}.{name} = value; -}}''' - - -def generate_module_setdefaults_impl(module): - res = [] - for option in module.options: - if option.name is None: - continue - fmt = { - 'capname': option.name[0].capitalize() + option.name[1:], - 'type': option.type, - 'module': module.id, - 'name': option.name, - } - res.append(TPL_SETDEFAULT_IMPL.format(**fmt)) - return '\n'.join(res) - - ################################################################################ # for main/options.cpp @@ -875,11 +843,9 @@ def codegen_module(module, dst_dir, tpls): 'holder_decl': generate_module_holder_decl(module), 'wrapper_functions': generate_module_wrapper_functions(module), 'option_names': generate_module_option_names(module), - 'setdefaults_decl': generate_module_setdefaults_decl(module), # module source 'header': module.header, 'modes_impl': generate_module_mode_impl(module), - 'setdefaults_impl': generate_module_setdefaults_impl(module), } for tpl in tpls: filename = tpl['output'].replace('module', module.filename) diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp index ee5260f34..d2ece3f13 100644 --- a/src/options/module_template.cpp +++ b/src/options/module_template.cpp @@ -28,11 +28,4 @@ namespace cvc5::options { ${modes_impl}$ // clang-format on -namespace ${id}$ -{ -// clang-format off -${setdefaults_impl}$ -// clang-format on -} - } // namespace cvc5::options diff --git a/src/options/module_template.h b/src/options/module_template.h index 61d689b72..d9b591f11 100644 --- a/src/options/module_template.h +++ b/src/options/module_template.h @@ -56,8 +56,6 @@ namespace ${id}$ { // clang-format off ${option_names}$ - -${setdefaults_decl}$ // clang-format on } diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 93b08a858..ec6c831e4 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -387,7 +387,10 @@ void OptionsHandler::checkBvSatSolver(const std::string& option, + " does not support lazy bit-blasting.\n" + "Try --bv-sat-solver=minisat"); } - options::bv::setDefaultBitvectorToBool(*d_options, true); + if (!d_options->bv.bitvectorToBoolWasSetByUser) + { + d_options->bv.bitvectorToBool = true; + } } } diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 19862cab2..420496190 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -259,6 +259,7 @@ name = "SMT Layer" category = "common" long = "produce-assertions" type = "bool" + alias = ["interactive-mode"] help = "keep an assertions list (enables get-assertions command)" [[option]] diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 84c0bd17c..9f34b5647 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -737,6 +737,36 @@ void Parser::pushScope(bool isUserContext) d_symman->pushScope(isUserContext); } +void Parser::pushGetValueScope() +{ + pushScope(); + // we must bind all relevant uninterpreted constants, which coincide with + // the set of uninterpreted constants that are printed in the definition + // of a model. + std::vector<api::Sort> declareSorts = d_symman->getModelDeclareSorts(); + Trace("parser") << "Push get value scope, with " << declareSorts.size() + << " declared sorts" << std::endl; + for (const api::Sort& s : declareSorts) + { + std::vector<api::Term> elements = d_solver->getModelDomainElements(s); + for (const api::Term& e : elements) + { + // Uninterpreted constants are abstract values, which by SMT-LIB are + // required to be annotated with their type, e.g. (as @uc_Foo_0 Foo). + // Thus, the element is not printed simply as its name. + std::string en = e.toString(); + size_t index = en.find("(as "); + if (index == 0) + { + index = en.find(" ", 4); + en = en.substr(4, index - 4); + } + Trace("parser") << "Get value scope : " << en << " -> " << e << std::endl; + defineVar(en, e); + } + } +} + void Parser::popScope() { d_symman->popScope(); diff --git a/src/parser/parser.h b/src/parser/parser.h index 4b04c77b7..19e5b8531 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -716,6 +716,14 @@ public: */ void pushScope(bool isUserContext = false); + /** Push scope for get-value + * + * This pushes a scope by a call to pushScope that binds all relevant bindings + * required for parsing the SMT-LIB command `get-value`. This includes + * all uninterpreted constant values in user-defined uninterpreted sorts. + */ + void pushGetValueScope(); + void popScope(); virtual void reset(); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 478edb651..e3aee250e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -343,7 +343,13 @@ command [std::unique_ptr<cvc5::Command>* cmd] | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd] | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] | /* value query */ - GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); } + GET_VALUE_TOK + { + PARSER_STATE->checkThatLogicIsSet(); + // bind all symbols specific to the model, e.g. uninterpreted constant + // values + PARSER_STATE->pushGetValueScope(); + } ( LPAREN_TOK termList[terms,expr] RPAREN_TOK { cmd->reset(new GetValueCommand(terms)); } | ~LPAREN_TOK @@ -352,6 +358,7 @@ command [std::unique_ptr<cvc5::Command>* cmd] "parentheses?"); } ) + { PARSER_STATE->popScope(); } | /* get-assignment */ GET_ASSIGNMENT_TOK { PARSER_STATE->checkThatLogicIsSet(); } { cmd->reset(new GetAssignmentCommand()); } @@ -793,7 +800,7 @@ smt25Command[std::unique_ptr<cvc5::Command>* cmd] /* echo */ | ECHO_TOK - ( simpleSymbolicExpr[s] + ( str[s, true] { cmd->reset(new EchoCommand(s)); } | { cmd->reset(new EchoCommand()); } ) @@ -1648,7 +1655,7 @@ identifier[cvc5::ParseOp& p] if (!f.getSort().isConstructor()) { PARSER_STATE->parseError( - "Bad syntax for test (_ is X), X must be a constructor."); + "Bad syntax for (_ is X), X must be a constructor."); } // get the datatype that f belongs to api::Sort sf = f.getSort().getConstructorCodomainSort(); @@ -1662,7 +1669,7 @@ identifier[cvc5::ParseOp& p] if (!f.getSort().isSelector()) { PARSER_STATE->parseError( - "Bad syntax for test (_ update X), X must be a selector."); + "Bad syntax for (_ update X), X must be a selector."); } std::string sname = f.toString(); // get the datatype that f belongs to @@ -1673,13 +1680,6 @@ identifier[cvc5::ParseOp& p] // get the updater term p.d_expr = ds.getUpdaterTerm(); } - | TUPLE_SEL_TOK m=INTEGER_LITERAL - { - // we adopt a special syntax (_ tupSel n) - p.d_kind = api::APPLY_SELECTOR; - // put m in expr so that the caller can deal with this case - p.d_expr = SOLVER->mkInteger(AntlrInput::tokenToUnsigned($m)); - } | TUPLE_PROJECT_TOK nonemptyNumeralList[numerals] { // we adopt a special syntax (_ tuple_project i_1 ... i_n) where @@ -1697,9 +1697,10 @@ identifier[cvc5::ParseOp& p] { std::string opName = AntlrInput::tokenText($sym); api::Kind k = PARSER_STATE->getIndexedOpKind(opName); - if (k == api::APPLY_UPDATER) + if (k == api::APPLY_SELECTOR || k == api::APPLY_UPDATER) { - // we adopt a special syntax (_ tuple_update n) for tuple updaters + // we adopt a special syntax (_ tuple_select n) and (_ tuple_update n) + // for tuple selectors and updaters if (numerals.size() != 1) { PARSER_STATE->parseError( @@ -2314,7 +2315,6 @@ FORALL_TOK : 'forall'; CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char'; TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple'; -TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple_select'; TUPLE_PROJECT_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple_project'; HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index b186c2b2a..be7bdcb0f 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -135,6 +135,11 @@ void Smt2::addDatatypesOperators() { Parser::addOperator(api::APPLY_UPDATER); addOperator(api::DT_SIZE, "dt.size"); + // Notice that tuple operators, we use the generic APPLY_SELECTOR and + // APPLY_UPDATER kinds. These are processed based on the context + // in which they are parsed, e.g. when parsing identifiers. + addIndexedOperator( + api::APPLY_SELECTOR, api::APPLY_SELECTOR, "tuple_select"); addIndexedOperator(api::APPLY_UPDATER, api::APPLY_UPDATER, "tuple_update"); } } @@ -258,14 +263,16 @@ void Smt2::addFloatingPointOperators() { } void Smt2::addSepOperators() { + defineVar("sep.emp", d_solver->mkSepEmp()); + // the Boolean sort is a placeholder here since we don't have type info + // without type annotation + defineVar("sep.nil", d_solver->mkSepNil(d_solver->getBooleanSort())); addOperator(api::SEP_STAR, "sep"); addOperator(api::SEP_PTO, "pto"); addOperator(api::SEP_WAND, "wand"); - addOperator(api::SEP_EMP, "emp"); Parser::addOperator(api::SEP_STAR); Parser::addOperator(api::SEP_PTO); Parser::addOperator(api::SEP_WAND); - Parser::addOperator(api::SEP_EMP); } void Smt2::addCoreSymbols() @@ -288,7 +295,7 @@ void Smt2::addOperator(api::Kind kind, const std::string& name) Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )" << std::endl; Parser::addOperator(kind); - operatorKindMap[name] = kind; + d_operatorKindMap[name] = kind; } void Smt2::addIndexedOperator(api::Kind tKind, @@ -302,11 +309,11 @@ void Smt2::addIndexedOperator(api::Kind tKind, api::Kind Smt2::getOperatorKind(const std::string& name) const { // precondition: isOperatorEnabled(name) - return operatorKindMap.find(name)->second; + return d_operatorKindMap.find(name)->second; } bool Smt2::isOperatorEnabled(const std::string& name) const { - return operatorKindMap.find(name) != operatorKindMap.end(); + return d_operatorKindMap.find(name) != d_operatorKindMap.end(); } bool Smt2::isTheoryEnabled(theory::TheoryId theory) const @@ -437,7 +444,7 @@ void Smt2::reset() { d_logicSet = false; d_seenSetLogic = false; d_logic = LogicInfo(); - operatorKindMap.clear(); + d_operatorKindMap.clear(); d_lastNamedTerm = std::pair<api::Term, std::string>(); } @@ -546,7 +553,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) if (d_logic.areTranscendentalsUsed()) { - defineVar("real.pi", d_solver->mkTerm(api::PI)); + defineVar("real.pi", d_solver->mkPi()); addTranscendentalOperators(); } if (!strictModeEnabled()) @@ -672,12 +679,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) addFloatingPointOperators(); } - if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) { - // the Boolean sort is a placeholder here since we don't have type info - // without type annotation - defineVar("sep.nil", d_solver->mkSepNil(d_solver->getBooleanSort())); - defineVar("sep.emp", d_solver->mkTerm(api::SEP_EMP)); - + if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) + { addSepOperators(); } @@ -1119,11 +1122,6 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) Debug("parser") << "applyParseOp: return uminus " << ret << std::endl; return ret; } - if (kind == api::EQ_RANGE && d_solver->getOption("arrays-exp") != "true") - { - parseError( - "eqrange predicate requires option --arrays-exp to be enabled."); - } if (kind == api::SINGLETON && args.size() == 1) { api::Term ret = d_solver->mkTerm(api::SINGLETON, args[0]); diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index fd68732fe..8d8f8febe 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -50,7 +50,7 @@ class Smt2 : public Parser bool d_seenSetLogic; LogicInfo d_logic; - std::unordered_map<std::string, api::Kind> operatorKindMap; + std::unordered_map<std::string, api::Kind> d_operatorKindMap; /** * Maps indexed symbols to the kind of the operator (e.g. "extract" to * BITVECTOR_EXTRACT). diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 32b195be2..1da2a3c7b 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1723,15 +1723,7 @@ void Smt2Printer::toStreamCmdEmpty(std::ostream& out, void Smt2Printer::toStreamCmdEcho(std::ostream& out, const std::string& output) const { - std::string s = output; - // escape all double-quotes - size_t pos = 0; - while ((pos = s.find('"', pos)) != string::npos) - { - s.replace(pos, 1, "\"\""); - pos += 2; - } - out << "(echo \"" << s << "\")" << std::endl; + out << "(echo " << cvc5::quoteString(output) << ')' << std::endl; } /* @@ -1930,14 +1922,9 @@ static void toStream(std::ostream& out, const CommandUnsupported* s, Variant v) #endif /* CVC5_COMPETITION_MODE */ } -static void errorToStream(std::ostream& out, std::string message, Variant v) { - // escape all double-quotes - size_t pos = 0; - while((pos = message.find('"', pos)) != string::npos) { - message.replace(pos, 1, "\"\""); - pos += 2; - } - out << "(error \"" << message << "\")" << endl; +static void errorToStream(std::ostream& out, std::string message, Variant v) +{ + out << "(error " << cvc5::quoteString(message) << ')' << endl; } static void toStream(std::ostream& out, const CommandFailure* s, Variant v) { diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 6312f3140..ef7735b44 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -55,6 +55,79 @@ bool AletheProofPostprocessCallback::update(Node res, switch (id) { + // To keep the original shape of the proof node it is necessary to rederive + // the original conclusion. However, the term that should be printed might + // be different from that conclusion. Thus, it is stored as an additional + // argument in the proof node. Usually, the only difference is an additional + // cl operator or the outmost or operator being replaced by a cl operator. + // + // When steps are added to the proof that have not been there previously, + // it is unwise to add them in the same manner. To illustrate this the + // following counterexample shows the pitfalls of this approach: + // + // (or a (or b c)) (not a) + // --------------------------- RESOLUTION + // (or b c) + // + // is converted into an Alethe proof that should be printed as + // + // (cl a (or b c)) (cl (not a)) + // -------------------------------- RESOLUTION + // (cl (or b c)) + // --------------- OR + // (cl b c) + // + // Here, (cl (or b c)) and (cl b c) cannot correspond to the same proof node + // (or b c). Thus, we build a new proof node using the kind SEXPR + // that is then printed as (cl (or b c)). We denote this wrapping of a proof + // node by using an extra pair of parenthesis, i.e. ((or b c)) is the proof + // node printed as (cl (or b c)). + // + // + // Some proof rules have a close correspondence in Alethe. There are two + // very frequent patterns that, to avoid repetition, are described here and + // referred to in the comments on the specific proof rules below. + // + // The first pattern, which will be called singleton pattern in the + // following, adds the original proof node F with the corresponding rule R' + // of the Alethe calculus and uses the same premises as the original proof + // node (P1:F1) ... (Pn:Fn). However, the conclusion is printed as (cl F). + // + // This means a cvc5 rule R that looks as follows: + // + // (P1:F1) ... (Pn:Fn) + // --------------------- R + // F + // + // is transformed into: + // + // (P1:F1) ... (Pn:Fn) + // --------------------- R' + // (cl F)* + // + // * the corresponding proof node is F + // + // The second pattern, which will be called clause pattern in the following, + // has a disjunction (or G1 ... Gn) as conclusion. It also adds the orignal + // proof node (or G1 ... Gn) with the corresponding rule R' of the Alethe + // calculus and uses the same premises as the original proof node (P1:F1) + // ... (Pn:Fn). However, the conclusion is printed as (cl G1 ... Gn), i.e. + // the or is replaced by the cl operator. + // + // This means a cvc5 rule R that looks as follows: + // + // (P1:F1) ... (Pn:Fn) + // --------------------- R + // (or G1 ... Gn) + // + // Is transformed into: + // + // (P1:F1) ... (Pn:Fn) + // --------------------- R' + // (cl G1 ... Gn)* + // + // * the corresponding proof node is (or G1 ... Gn) + // //================================================= Core rules //======================== Assume and Scope case PfRule::ASSUME: diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp index a3ef944e0..8b4b332a1 100644 --- a/src/proof/proof_node_manager.cpp +++ b/src/proof/proof_node_manager.cpp @@ -28,7 +28,8 @@ using namespace cvc5::kind; namespace cvc5 { -ProofNodeManager::ProofNodeManager(ProofChecker* pc) : d_checker(pc) +ProofNodeManager::ProofNodeManager(theory::Rewriter* rr, ProofChecker* pc) + : d_rewriter(rr), d_checker(pc) { d_true = NodeManager::currentNM()->mkConst(true); // we always allocate a proof checker, regardless of the proof checking mode @@ -160,14 +161,14 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope( computedAcr = true; for (const Node& acc : ac) { - Node accr = theory::Rewriter::rewrite(acc); + Node accr = d_rewriter->rewrite(acc); if (accr != acc) { acr[accr] = acc; } } } - Node ar = theory::Rewriter::rewrite(a); + Node ar = d_rewriter->rewrite(a); std::unordered_map<Node, Node>::iterator itr = acr.find(ar); if (itr != acr.end()) { diff --git a/src/proof/proof_node_manager.h b/src/proof/proof_node_manager.h index 928aabb76..533f6d173 100644 --- a/src/proof/proof_node_manager.h +++ b/src/proof/proof_node_manager.h @@ -28,6 +28,10 @@ namespace cvc5 { class ProofChecker; class ProofNode; +namespace theory { +class Rewriter; +} + /** * A manager for proof node objects. This is a trusted interface for creating * and updating ProofNode objects. @@ -54,7 +58,7 @@ class ProofNode; class ProofNodeManager { public: - ProofNodeManager(ProofChecker* pc = nullptr); + ProofNodeManager(theory::Rewriter* rr, ProofChecker* pc = nullptr); ~ProofNodeManager() {} /** * This constructs a ProofNode with the given arguments. The expected @@ -184,6 +188,8 @@ class ProofNodeManager static ProofNode* cancelDoubleSymm(ProofNode* pn); private: + /** The rewriter */ + theory::Rewriter* d_rewriter; /** The (optional) proof checker */ ProofChecker* d_checker; /** the true node */ diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index f148d1018..5d16c12ce 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -31,8 +31,7 @@ using namespace cvc5::theory; namespace cvc5 { namespace smt { -CheckModels::CheckModels(Env& e) : d_env(e) {} -CheckModels::~CheckModels() {} +CheckModels::CheckModels(Env& e) : EnvObj(e) {} void CheckModels::checkModel(TheoryModel* m, const context::CDList<Node>& al, @@ -50,6 +49,12 @@ void CheckModels::checkModel(TheoryModel* m, throw RecoverableModalException( "Cannot run check-model on a model with approximate values."); } + Node sepHeap, sepNeq; + if (m->getHeapModel(sepHeap, sepNeq)) + { + throw RecoverableModalException( + "Cannot run check-model on a model with a separation logic heap."); + } theory::SubstitutionMap& sm = d_env.getTopLevelSubstitutions().get(); Trace("check-model") << "checkModel: Check assertions..." << std::endl; @@ -71,7 +76,7 @@ void CheckModels::checkModel(TheoryModel* m, Notice() << "SolverEngine::checkModel(): -- substitutes to " << n << std::endl; - n = Rewriter::rewrite(n); + n = rewrite(n); Notice() << "SolverEngine::checkModel(): -- rewrites to " << n << std::endl; // We look up the value before simplifying. If n contains quantifiers, diff --git a/src/smt/check_models.h b/src/smt/check_models.h index d785b53d5..2b3447010 100644 --- a/src/smt/check_models.h +++ b/src/smt/check_models.h @@ -20,11 +20,10 @@ #include "context/cdlist.h" #include "expr/node.h" +#include "smt/env_obj.h" namespace cvc5 { -class Env; - namespace theory { class TheoryModel; } @@ -34,11 +33,10 @@ namespace smt { /** * This utility is responsible for checking the current model. */ -class CheckModels +class CheckModels : protected EnvObj { public: CheckModels(Env& e); - ~CheckModels(); /** * Check model m against the current set of input assertions al. * @@ -48,10 +46,6 @@ class CheckModels void checkModel(theory::TheoryModel* m, const context::CDList<Node>& al, bool hardFailure); - - private: - /** Reference to the environment */ - Env& d_env; }; } // namespace smt diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 311d6713a..e8ee6d59c 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -38,6 +38,7 @@ #include "proof/unsat_core.h" #include "smt/dump.h" #include "smt/model.h" +#include "util/smt2_quote_string.h" #include "util/unsafe_interrupt_exception.h" #include "util/utility.h" @@ -302,19 +303,10 @@ void EmptyCommand::toStream(std::ostream& out, /* class EchoCommand */ /* -------------------------------------------------------------------------- */ -EchoCommand::EchoCommand(std::string output) -{ - // escape all double-quotes - size_t pos = 0; - while ((pos = output.find('"', pos)) != string::npos) - { - output.replace(pos, 1, "\"\""); - pos += 2; - } - d_output = '"' + output + '"'; -} +EchoCommand::EchoCommand(std::string output) : d_output(output) {} std::string EchoCommand::getOutput() const { return d_output; } + void EchoCommand::invoke(api::Solver* solver, SymbolManager* sm) { /* we don't have an output stream here, nothing to do */ @@ -325,7 +317,7 @@ void EchoCommand::invoke(api::Solver* solver, SymbolManager* sm, std::ostream& out) { - out << d_output << std::endl; + out << cvc5::quoteString(d_output) << std::endl; Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~" << std::endl; d_commandStatus = CommandSuccess::instance(); @@ -335,6 +327,7 @@ void EchoCommand::invoke(api::Solver* solver, } Command* EchoCommand::clone() const { return new EchoCommand(d_output); } + std::string EchoCommand::getCommandName() const { return "echo"; } void EchoCommand::toStream(std::ostream& out, diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp index cbc388331..e8c1ff07f 100644 --- a/src/smt/model_blocker.cpp +++ b/src/smt/model_blocker.cpp @@ -25,6 +25,8 @@ using namespace cvc5::kind; namespace cvc5 { +ModelBlocker::ModelBlocker(Env& e) : EnvObj(e) {} + Node ModelBlocker::getModelBlocker(const std::vector<Node>& assertions, theory::TheoryModel* m, options::BlockModelsMode mode, diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h index 42219e220..5e41de6a3 100644 --- a/src/smt/model_blocker.h +++ b/src/smt/model_blocker.h @@ -22,6 +22,7 @@ #include "expr/node.h" #include "options/smt_options.h" +#include "smt/env_obj.h" namespace cvc5 { @@ -32,9 +33,10 @@ class TheoryModel; /** * A utility for blocking the current model. */ -class ModelBlocker +class ModelBlocker : protected EnvObj { public: + ModelBlocker(Env& e); /** get model blocker * * This returns a disjunction of literals ~L1 V ... V ~Ln with the following @@ -63,7 +65,7 @@ class ModelBlocker * our input. In other words, we do not return ~(x < 0) V ~(w < 0) since the * left disjunct is always false. */ - static Node getModelBlocker( + Node getModelBlocker( const std::vector<Node>& assertions, theory::TheoryModel* m, options::BlockModelsMode mode, diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 4b16b9391..3aed58b30 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -150,7 +150,7 @@ Node Preprocessor::simplify(const Node& node) d_env.getPrinter().toStreamCmdSimplify(d_env.getDumpOut(), node); } Node ret = expandDefinitions(node); - ret = theory::Rewriter::rewrite(ret); + ret = rewrite(ret); return ret; } diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 2e08ab2df..4b4291075 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -41,7 +41,7 @@ PfManager::PfManager(Env& env) d_pchecker(new ProofChecker( options().proof.proofCheck == options::ProofCheckMode::EAGER, options().proof.proofPedantic)), - d_pnm(new ProofNodeManager(d_pchecker.get())), + d_pnm(new ProofNodeManager(env.getRewriter(), d_pchecker.get())), d_pppg(new PreprocessProofGenerator( d_pnm.get(), env.getUserContext(), "smt::PreprocessProofGenerator")), d_pfpp(nullptr), diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index adc15ca2c..04a36c1c0 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -42,7 +42,7 @@ ProofPostprocessCallback::ProofPostprocessCallback(Env& env, : d_env(env), d_pnm(env.getProofNodeManager()), d_pppg(pppg), - d_wfpm(env.getProofNodeManager()), + d_wfpm(env), d_updateScopedAssumptions(updateScopedAssumptions) { d_true = NodeManager::currentNM()->mkConst(true); @@ -654,7 +654,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // apply transitivity if necessary Node eq = addProofForTrans(tchildren, cdp); - cdp->addStep(args[0], PfRule::EQ_RESOLVE, {children[0], eq}, {}); + cdp->addStep(eq[1], PfRule::EQ_RESOLVE, {children[0], eq}, {}); return args[0]; } else if (id == PfRule::MACRO_RESOLUTION diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 911e0a960..fc6ec3915 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -417,10 +417,10 @@ void SolverEngine::setInfo(const std::string& key, const std::string& value) bool SolverEngine::isValidGetInfoFlag(const std::string& key) const { - if (key == "all-statistics" || key == "error-behavior" || key == "name" - || key == "version" || key == "authors" || key == "status" - || key == "reason-unknown" || key == "assertion-stack-levels" - || key == "all-options" || key == "time") + if (key == "all-statistics" || key == "error-behavior" || key == "filename" + || key == "name" || key == "version" || key == "authors" + || key == "status" || key == "time" || key == "reason-unknown" + || key == "assertion-stack-levels" || key == "all-options") { return true; } @@ -455,7 +455,7 @@ std::string SolverEngine::getInfo(const std::string& key) const } if (key == "authors") { - return toSExpr(Configuration::about()); + return toSExpr("the " + Configuration::getName() + " authors"); } if (key == "status") { @@ -1081,7 +1081,7 @@ Node SolverEngine::getValue(const Node& ex) const // AJR : necessary? if (!n.getType().isFunction()) { - n = Rewriter::rewrite(n); + n = d_env->getRewriter()->rewrite(n); } Trace("smt") << "--- getting value of " << n << endl; @@ -1224,7 +1224,8 @@ Result SolverEngine::blockModel() // get expanded assertions std::vector<Node> eassertsProc = getExpandedAssertions(); - Node eblocker = ModelBlocker::getModelBlocker( + ModelBlocker mb(*d_env.get()); + Node eblocker = mb.getModelBlocker( eassertsProc, m, d_env->getOptions().smt.blockModelsMode); Trace("smt") << "Block formula: " << eblocker << std::endl; return assertFormula(eblocker); @@ -1247,7 +1248,8 @@ Result SolverEngine::blockModelValues(const std::vector<Node>& exprs) // get expanded assertions std::vector<Node> eassertsProc = getExpandedAssertions(); // we always do block model values mode here - Node eblocker = ModelBlocker::getModelBlocker( + ModelBlocker mb(*d_env.get()); + Node eblocker = mb.getModelBlocker( eassertsProc, m, options::BlockModelsMode::VALUES, exprs); return assertFormula(eblocker); } diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 2a1d4e6c6..5db9804c6 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -377,7 +377,7 @@ void SygusSolver::checkSynthSolution(Assertions& as) // problem are rewritten to true. If this is not the case, then the // assertions module of the subsolver will complain about assertions // with free variables. - Node ar = theory::Rewriter::rewrite(a); + Node ar = rewrite(a); solChecker->assertFormula(ar); } Result r = solChecker->checkSat(); diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp index 8e998b9cf..16d297495 100644 --- a/src/smt/witness_form.cpp +++ b/src/smt/witness_form.cpp @@ -16,21 +16,27 @@ #include "smt/witness_form.h" #include "expr/skolem_manager.h" +#include "smt/env.h" #include "theory/rewriter.h" namespace cvc5 { namespace smt { -WitnessFormGenerator::WitnessFormGenerator(ProofNodeManager* pnm) - : d_tcpg(pnm, +WitnessFormGenerator::WitnessFormGenerator(Env& env) + : d_rewriter(env.getRewriter()), + d_tcpg(env.getProofNodeManager(), nullptr, TConvPolicy::FIXPOINT, TConvCachePolicy::NEVER, "WfGenerator::TConvProofGenerator", nullptr, true), - d_wintroPf(pnm, nullptr, nullptr, "WfGenerator::LazyCDProof"), - d_pskPf(pnm, nullptr, "WfGenerator::PurifySkolemProof") + d_wintroPf(env.getProofNodeManager(), + nullptr, + nullptr, + "WfGenerator::LazyCDProof"), + d_pskPf( + env.getProofNodeManager(), nullptr, "WfGenerator::PurifySkolemProof") { } @@ -114,12 +120,12 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t) bool WitnessFormGenerator::requiresWitnessFormTransform(Node t, Node s) const { - return theory::Rewriter::rewrite(t) != theory::Rewriter::rewrite(s); + return d_rewriter->rewrite(t) != d_rewriter->rewrite(s); } bool WitnessFormGenerator::requiresWitnessFormIntro(Node t) const { - Node tr = theory::Rewriter::rewrite(t); + Node tr = d_rewriter->rewrite(t); return !tr.isConst() || !tr.getConst<bool>(); } diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h index 8522d41f0..06d60c1ed 100644 --- a/src/smt/witness_form.h +++ b/src/smt/witness_form.h @@ -25,6 +25,13 @@ #include "proof/proof_generator.h" namespace cvc5 { + +class Env; + +namespace theory { +class Rewriter; +} + namespace smt { /** @@ -37,7 +44,7 @@ namespace smt { class WitnessFormGenerator : public ProofGenerator { public: - WitnessFormGenerator(ProofNodeManager* pnm); + WitnessFormGenerator(Env& env); ~WitnessFormGenerator() {} /** * Get proof for, which expects an equality of the form t = toWitness(t). @@ -85,6 +92,8 @@ class WitnessFormGenerator : public ProofGenerator * Return a proof generator that can prove the given axiom exists. */ ProofGenerator* convertExistsInternal(Node exists); + /** The rewriter we are using */ + theory::Rewriter* d_rewriter; /** The term conversion proof generator */ TConvProofGenerator d_tcpg; /** The nodes we have already added rewrite steps for in d_tcpg */ diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 76a0c363d..cf2373b9f 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -193,9 +193,9 @@ void TheoryArith::postCheck(Effort level) if (Theory::fullEffort(level)) { d_arithModelCache.clear(); + std::set<Node> termSet; if (d_nonlinearExtension != nullptr) { - std::set<Node> termSet; updateModelCache(termSet); d_nonlinearExtension->checkFullEffort(d_arithModelCache, termSet); } @@ -204,6 +204,15 @@ void TheoryArith::postCheck(Effort level) // set incomplete d_im.setIncomplete(IncompleteId::ARITH_NL_DISABLED); } + // If we won't be doing a last call effort check (which implies that + // models will be computed), we must sanity check the integer model + // from the linear solver now. We also must update the model cache + // if we did not do so above. + if (d_nonlinearExtension == nullptr) + { + updateModelCache(termSet); + } + sanityCheckIntegerModel(); } } @@ -274,12 +283,6 @@ bool TheoryArith::collectModelValues(TheoryModel* m, updateModelCache(termSet); - if (sanityCheckIntegerModel()) - { - // We added a lemma - return false; - } - // We are now ready to assert the model. for (const std::pair<const Node, Node>& p : d_arithModelCache) { @@ -383,9 +386,9 @@ bool TheoryArith::sanityCheckIntegerModel() Trace("arith-check") << p.first << " -> " << p.second << std::endl; if (p.first.getType().isInteger() && !p.second.getType().isInteger()) { - Assert(false) << "TheoryArithPrivate generated a bad model value for " - "integer variable " - << p.first << " : " << p.second; + Warning() << "TheoryArithPrivate generated a bad model value for " + "integer variable " + << p.first << " : " << p.second; // must branch and bound TrustNode lem = d_bab.branchIntegerVariable(p.first, p.second.getConst<Rational>()); diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 9e69c9f71..93eadde43 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -296,7 +296,19 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck TrustNode TheoryArrays::ppRewrite(TNode term, std::vector<SkolemLemma>& lems) { - // first, see if we need to expand definitions + // first, check for logic exceptions + Kind k = term.getKind(); + if (!options().arrays.arraysExp) + { + if (k == kind::EQ_RANGE) + { + std::stringstream ss; + ss << "Term of kind " << k + << " not supported in default mode, try --arrays-exp"; + throw LogicException(ss.str()); + } + } + // see if we need to expand definitions TrustNode texp = d_rewriter.expandDefinition(term); if (!texp.isNull()) { @@ -309,7 +321,8 @@ TrustNode TheoryArrays::ppRewrite(TNode term, std::vector<SkolemLemma>& lems) d_ppEqualityEngine.addTerm(term); NodeManager* nm = NodeManager::currentNM(); Node ret; - switch (term.getKind()) { + switch (k) + { case kind::SELECT: { // select(store(a,i,v),j) = select(a,j) // IF i != j diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp index e1b4813ec..433768e5d 100644 --- a/src/theory/arrays/theory_arrays_type_rules.cpp +++ b/src/theory/arrays/theory_arrays_type_rules.cpp @@ -18,6 +18,7 @@ // for array-constant attributes #include "expr/array_store_all.h" #include "theory/arrays/theory_arrays_rewriter.h" +#include "theory/builtin/theory_builtin_type_rules.h" #include "theory/type_enumerator.h" #include "util/cardinality.h" @@ -249,7 +250,24 @@ bool ArraysProperties::isWellFounded(TypeNode type) Node ArraysProperties::mkGroundTerm(TypeNode type) { - return *TypeEnumerator(type); + Assert(type.getKind() == kind::ARRAY_TYPE); + TypeNode elemType = type.getArrayConstituentType(); + Node elem = elemType.mkGroundTerm(); + if (elem.isConst()) + { + return NodeManager::currentNM()->mkConst(ArrayStoreAll(type, elem)); + } + // Note the distinction between mkGroundTerm and mkGroundValue. While + // an arbitrary value can be obtained by calling the type enumerator here, + // that is wrong for types that are not closed enumerable since it may + // return a term containing values that should not appear in e.g. assertions. + // For example, arrays whose element type is an uninterpreted sort will + // incorrectly introduce uninterpreted sort values if this is done. + // It is currently infeasible to construct an ArrayStoreAll with the element + // type's mkGroundTerm as an argument when that term is not constant. + // Thus, we must simply return a fresh Skolem here, using the same utility + // as that of uninterpreted sorts. + return builtin::SortProperties::mkGroundTerm(type); } TypeNode ArrayPartialSelectTypeRule::computeType(NodeManager* nodeManager, diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index c446504fd..fd957baaa 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -16,12 +16,12 @@ #include "theory/datatypes/datatypes_rewriter.h" #include "expr/ascription_type.h" +#include "expr/codatatype_bound_variable.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "expr/skolem_manager.h" #include "expr/sygus_datatype.h" -#include "expr/uninterpreted_constant.h" #include "options/datatypes_options.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/datatypes/theory_datatypes_utils.h" @@ -729,7 +729,7 @@ Node DatatypesRewriter::collectRef(Node n, else { // a loop - const Integer& i = n.getConst<UninterpretedConstant>().getIndex(); + const Integer& i = n.getConst<CodatatypeBoundVariable>().getIndex(); uint32_t index = i.toUnsignedInt(); if (index >= sk.size()) { @@ -771,7 +771,7 @@ Node DatatypesRewriter::normalizeCodatatypeConstantEqc( { int debruijn = depth - it->second - 1; return NodeManager::currentNM()->mkConst( - UninterpretedConstant(n.getType(), debruijn)); + CodatatypeBoundVariable(n.getType(), debruijn)); } std::vector<Node> children; bool childChanged = false; @@ -798,10 +798,10 @@ Node DatatypesRewriter::replaceDebruijn(Node n, TypeNode orig_tn, unsigned depth) { - if (n.getKind() == kind::UNINTERPRETED_CONSTANT && n.getType() == orig_tn) + if (n.getKind() == kind::CODATATYPE_BOUND_VARIABLE && n.getType() == orig_tn) { unsigned index = - n.getConst<UninterpretedConstant>().getIndex().toUnsignedInt(); + n.getConst<CodatatypeBoundVariable>().getIndex().toUnsignedInt(); if (index == depth) { return orig; diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 41d5ded76..cb3a78cf2 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -145,4 +145,13 @@ parameterized TUPLE_PROJECT TUPLE_PROJECT_OP 1 \ typerule TUPLE_PROJECT_OP "SimpleTypeRule<RBuiltinOperator>" typerule TUPLE_PROJECT ::cvc5::theory::datatypes::TupleProjectTypeRule +# For representing codatatype values +constant CODATATYPE_BOUND_VARIABLE \ + class \ + CodatatypeBoundVariable \ + ::cvc5::CodatatypeBoundVariableHashFunction \ + "expr/codatatype_bound_variable.h" \ + "the kind of expressions representing bound variables in codatatype constants, which are de Bruijn indexed variables; payload is an instance of the cvc5::CodatatypeBoundVariable class (used in models)" +typerule CODATATYPE_BOUND_VARIABLE ::cvc5::theory::datatypes::CodatatypeBoundVariableTypeRule + endtheory diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index c892ffc11..0cbeaa515 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -18,11 +18,11 @@ #include <sstream> #include "base/check.h" +#include "expr/codatatype_bound_variable.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/kind.h" #include "expr/skolem_manager.h" -#include "expr/uninterpreted_constant.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" @@ -1290,10 +1290,10 @@ bool TheoryDatatypes::collectModelValues(TheoryModel* m, Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, int >& vmap, int depth ){ std::map< Node, int >::iterator itv = vmap.find( n ); + NodeManager* nm = NodeManager::currentNM(); if( itv!=vmap.end() ){ int debruijn = depth - 1 - itv->second; - return NodeManager::currentNM()->mkConst( - UninterpretedConstant(n.getType(), debruijn)); + return nm->mkConst(CodatatypeBoundVariable(n.getType(), debruijn)); }else if( n.getType().isDatatype() ){ Node nc = eqc_cons[n]; if( !nc.isNull() ){ @@ -1308,7 +1308,7 @@ Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_c children.push_back( rv ); } vmap.erase( n ); - return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); + return nm->mkNode(APPLY_CONSTRUCTOR, children); } } return n; diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp index 503eaf4df..86a11357b 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.cpp +++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp @@ -18,6 +18,7 @@ #include <sstream> #include "expr/ascription_type.h" +#include "expr/codatatype_bound_variable.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/type_matcher.h" @@ -597,6 +598,13 @@ TypeNode TupleProjectTypeRule::computeType(NodeManager* nm, TNode n, bool check) return nm->mkTupleType(types); } +TypeNode CodatatypeBoundVariableTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + return n.getConst<CodatatypeBoundVariable>().getType(); +} + } // namespace datatypes } // namespace theory } // namespace cvc5 diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index cf57a6c0d..7cf98aa74 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -99,6 +99,12 @@ class TupleProjectTypeRule static TypeNode computeType(NodeManager* nm, TNode n, bool check); }; +class CodatatypeBoundVariableTypeRule +{ + public: + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; + } // namespace datatypes } // namespace theory } // namespace cvc5 diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index 39b48ece9..6528f1052 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -16,6 +16,7 @@ #include "theory/datatypes/type_enumerator.h" #include "expr/ascription_type.h" +#include "expr/codatatype_bound_variable.h" #include "expr/dtype_cons.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes_utils.h" @@ -108,8 +109,8 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ { if (d_child_enum) { - ret = NodeManager::currentNM()->mkConst( - UninterpretedConstant(d_type, d_size_limit)); + NodeManager* nm = NodeManager::currentNM(); + ret = nm->mkConst(CodatatypeBoundVariable(d_type, d_size_limit)); } else { diff --git a/src/theory/incomplete_id.cpp b/src/theory/incomplete_id.cpp index a2a3baa0f..c763fb9a0 100644 --- a/src/theory/incomplete_id.cpp +++ b/src/theory/incomplete_id.cpp @@ -40,6 +40,8 @@ const char* toString(IncompleteId i) case IncompleteId::STRINGS_LOOP_SKIP: return "STRINGS_LOOP_SKIP"; case IncompleteId::STRINGS_REGEXP_NO_SIMPLIFY: return "STRINGS_REGEXP_NO_SIMPLIFY"; + case IncompleteId::SEQ_FINITE_DYNAMIC_CARDINALITY: + return "SEQ_FINITE_DYNAMIC_CARDINALITY"; case IncompleteId::UF_HO_EXT_DISABLED: return "UF_HO_EXT_DISABLED"; case IncompleteId::UF_CARD_DISABLED: return "UF_CARD_DISABLED"; case IncompleteId::UF_CARD_MODE: return "UF_CARD_MODE"; diff --git a/src/theory/incomplete_id.h b/src/theory/incomplete_id.h index 951c2a94f..aaa458d8e 100644 --- a/src/theory/incomplete_id.h +++ b/src/theory/incomplete_id.h @@ -52,6 +52,11 @@ enum class IncompleteId STRINGS_LOOP_SKIP, // we could not simplify a regular expression membership STRINGS_REGEXP_NO_SIMPLIFY, + // incomplete due to sequence of a dynamic finite type (e.g. a type that + // we know is finite, but its exact cardinality is not fixed. For example, + // when finite model finding is enabled, uninterpreted sorts have a + // cardinality that depends on their interpretation in the current model). + SEQ_FINITE_DYNAMIC_CARDINALITY, // HO extensionality axiom was disabled UF_HO_EXT_DISABLED, // UF+cardinality solver was disabled diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index b98088a71..d778a679e 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -245,6 +245,7 @@ Node ConjectureGenerator::getUniversalRepresentative(TNode n, bool add) // now, do instantiation-based merging for each of these terms Trace("thm-ee-debug") << "Merge equivalence classes based on instantiations of terms..." << std::endl; //merge all pending equalities + EntailmentCheck* echeck = d_treg.getEntailmentCheck(); while( !d_upendingAdds.empty() ){ Trace("sg-pending") << "Add " << d_upendingAdds.size() << " pending terms..." << std::endl; std::vector< Node > pending; @@ -256,7 +257,7 @@ Node ConjectureGenerator::getUniversalRepresentative(TNode n, bool add) Trace("thm-ee-add") << "UEE : Add universal term " << t << std::endl; std::vector< Node > eq_terms; //if occurs modulo equality at ground level, it is equivalent to representative of ground equality engine - Node gt = getTermDatabase()->evaluateTerm(t); + Node gt = echeck->evaluateTerm(t); if( !gt.isNull() && gt!=t ){ eq_terms.push_back( gt ); } @@ -1362,7 +1363,8 @@ bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode } Trace("sg-cconj-debug") << "Evaluate RHS : : " << rhs << std::endl; //get the representative of rhs with substitution subs - TNode grhs = getTermDatabase()->getEntailedTerm( rhs, subs, true ); + EntailmentCheck* echeck = d_treg.getEntailmentCheck(); + TNode grhs = echeck->getEntailedTerm(rhs, subs, true); Trace("sg-cconj-debug") << "...done evaluating term, got : " << grhs << std::endl; if( !grhs.isNull() ){ if( glhs!=grhs ){ diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index a8ab760ce..d2b0b0542 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -238,6 +238,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id) d_lchildren.clear(); d_arg_to_arg_rep.clear(); d_arg_vector.clear(); + EntailmentCheck* echeck = d_treg.getEntailmentCheck(); for (std::pair<const TNode, std::vector<Node> >& ha : ho_var_apps_subs) { TNode var = ha.first; @@ -291,8 +292,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id) { if (!d_qstate.areEqual(itf->second, args[k])) { - if (!d_treg.getTermDatabase()->isEntailed( - itf->second.eqNode(args[k]), true)) + if (!echeck->isEntailed(itf->second.eqNode(args[k]), true)) { fixed_vals[k] = Node::null(); } diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index d8e3b7950..075299583 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -23,6 +23,7 @@ #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h" #include "theory/quantifiers/ematching/inst_match_generator_simple.h" #include "theory/quantifiers/ematching/pattern_term_selector.h" +#include "theory/quantifiers/ematching/relational_match_generator.h" #include "theory/quantifiers/ematching/var_match_generator.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_state.h" @@ -618,7 +619,7 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( InstMatchGenerator* init; std::map< Node, InstMatchGenerator * >::iterator iti = pat_map_init.find( pats[pCounter] ); if( iti==pat_map_init.end() ){ - init = new InstMatchGenerator(tparent, pats[pCounter]); + init = getInstMatchGenerator(tparent, q, pats[pCounter]); }else{ init = iti->second; } @@ -645,6 +646,7 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent, Node q, Node n) { + // maybe variable match generator if (n.getKind() != INST_CONSTANT) { Trace("var-trigger-debug") @@ -672,6 +674,16 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent, return vmg; } } + Trace("relational-trigger") + << "Is " << n << " a relational trigger?" << std::endl; + // relational triggers + bool hasPol, pol; + Node lit; + if (TriggerTermInfo::isUsableRelationTrigger(n, hasPol, pol, lit)) + { + Trace("relational-trigger") << "...yes, for literal " << lit << std::endl; + return new RelationalMatchGenerator(tparent, lit, hasPol, pol); + } return new InstMatchGenerator(tparent, n); } diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 30be83ecc..fdb0d0db3 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -339,20 +339,18 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ TriggerDatabase::TR_GET_OLD, d_num_trigger_vars[f]); } - if (tr == nullptr) + // if we generated a trigger above, add it + if (tr != nullptr) { - // did not generate a trigger - continue; - } - addTrigger(tr, f); - if (tr->isMultiTrigger()) - { - // only add a single multi-trigger - continue; + addTrigger(tr, f); + if (tr->isMultiTrigger()) + { + // only add a single multi-trigger + continue; + } } // if we are generating additional triggers... - size_t index = 0; - if (index < patTerms.size()) + if (patTerms.size() > 1) { // check if similar patterns exist, and if so, add them additionally unsigned nqfs_curr = 0; @@ -361,7 +359,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ nqfs_curr = d_quant_rel->getNumQuantifiersForSymbol(patTerms[0].getOperator()); } - index++; + size_t index = 1; bool success = true; while (success && index < patTerms.size() && d_is_single_trigger[patTerms[index]]) @@ -527,16 +525,22 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f) Trace("auto-gen-trigger-debug") << "...required polarity for " << pat << " is " << rpol << ", eq=" << rpoleq << std::endl; + // Currently, we have ad-hoc treatment for relational triggers that + // are not handled by RelationalMatchGen. + bool isAdHocRelationalTrigger = + TriggerTermInfo::isRelationalTrigger(pat) + && !TriggerTermInfo::isUsableRelationTrigger(pat); if (rpol != 0) { Assert(rpol == 1 || rpol == -1); - if (TriggerTermInfo::isRelationalTrigger(pat)) + if (isAdHocRelationalTrigger) { pat = rpol == -1 ? pat.negate() : pat; } else { - Assert(TriggerTermInfo::isAtomicTrigger(pat)); + Assert(TriggerTermInfo::isAtomicTrigger(pat) + || TriggerTermInfo::isUsableRelationTrigger(pat)); if (pat.getType().isBoolean() && rpoleq.isNull()) { if (options().quantifiers.literalMatchMode @@ -575,13 +579,10 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f) } Trace("auto-gen-trigger-debug") << "...got : " << pat << std::endl; } - else + else if (isAdHocRelationalTrigger) { - if (TriggerTermInfo::isRelationalTrigger(pat)) - { - // consider both polarities - addPatternToPool(f, pat.negate(), num_fv, mpat); - } + // consider both polarities + addPatternToPool(f, pat.negate(), num_fv, mpat); } addPatternToPool(f, pat, num_fv, mpat); } diff --git a/src/theory/quantifiers/ematching/relational_match_generator.cpp b/src/theory/quantifiers/ematching/relational_match_generator.cpp new file mode 100644 index 000000000..8981a7a2d --- /dev/null +++ b/src/theory/quantifiers/ematching/relational_match_generator.cpp @@ -0,0 +1,125 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Relational match generator class. + */ + +#include "theory/quantifiers/ematching/relational_match_generator.h" + +#include "theory/quantifiers/term_util.h" +#include "util/rational.h" + +using namespace cvc5::kind; + +namespace cvc5 { +namespace theory { +namespace quantifiers { +namespace inst { + +RelationalMatchGenerator::RelationalMatchGenerator(Trigger* tparent, + Node rtrigger, + bool hasPol, + bool pol) + : InstMatchGenerator(tparent, Node::null()), + d_vindex(-1), + d_hasPol(hasPol), + d_pol(pol), + d_counter(0) +{ + Assert((rtrigger.getKind() == EQUAL && rtrigger[0].getType().isReal()) + || rtrigger.getKind() == GEQ); + Trace("relational-match-gen") + << "Relational trigger: " << rtrigger << ", hasPol/pol = " << hasPol + << "/" << pol << std::endl; + for (size_t i = 0; i < 2; i++) + { + if (rtrigger[i].getKind() == INST_CONSTANT) + { + d_var = rtrigger[i]; + d_vindex = d_var.getAttribute(InstVarNumAttribute()); + d_rhs = rtrigger[1 - i]; + Assert(!quantifiers::TermUtil::hasInstConstAttr(d_rhs)); + Kind k = rtrigger.getKind(); + d_rel = (i == 0 ? k : (k == GEQ ? LEQ : k)); + break; + } + } + Trace("relational-match-gen") << "...processed " << d_var << " (" << d_vindex + << ") " << d_rel << " " << d_rhs << std::endl; + AlwaysAssert(!d_var.isNull()) + << "Failed to initialize RelationalMatchGenerator"; +} + +bool RelationalMatchGenerator::reset(Node eqc) +{ + d_counter = 0; + return true; +} + +int RelationalMatchGenerator::getNextMatch(Node q, InstMatch& m) +{ + Trace("relational-match-gen") << "getNextMatch, rel match gen" << std::endl; + // try (up to) two different terms + Node s; + Node rhs = d_rhs; + bool rmPrev = m.get(d_vindex).isNull(); + while (d_counter < 2) + { + bool checkPol = false; + if (d_counter == 0) + { + checkPol = d_pol; + } + else + { + Assert(d_counter == 1); + if (d_hasPol) + { + break; + } + // try the opposite polarity + checkPol = !d_pol; + } + NodeManager* nm = NodeManager::currentNM(); + // falsify ( d_var <d_rel> d_rhs ) = checkPol + s = rhs; + if (!checkPol) + { + s = nm->mkNode(PLUS, s, nm->mkConst(Rational(d_rel == GEQ ? -1 : 1))); + } + d_counter++; + Trace("relational-match-gen") + << "...try set " << s << " for " << checkPol << std::endl; + if (m.set(d_qstate, d_vindex, s)) + { + Trace("relational-match-gen") << "...success" << std::endl; + int ret = continueNextMatch(q, m, InferenceId::UNKNOWN); + if (ret > 0) + { + Trace("relational-match-gen") << "...returned " << ret << std::endl; + return ret; + } + Trace("relational-match-gen") << "...failed to gen inst" << std::endl; + // failed + if (rmPrev) + { + m.d_vals[d_vindex] = Node::null(); + } + } + } + return -1; +} + +} // namespace inst +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/relational_match_generator.h b/src/theory/quantifiers/ematching/relational_match_generator.h new file mode 100644 index 000000000..eead2876a --- /dev/null +++ b/src/theory/quantifiers/ematching/relational_match_generator.h @@ -0,0 +1,92 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Relational match generator class. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__QUANTIFIERS__RELATIONAL_MATCH_GENERATOR_H +#define CVC5__THEORY__QUANTIFIERS__RELATIONAL_MATCH_GENERATOR_H + +#include "expr/node.h" +#include "theory/quantifiers/ematching/inst_match_generator.h" + +namespace cvc5 { +namespace theory { +namespace quantifiers { +namespace inst { + +/** + * Match generator for relational triggers x ~ t where t is a ground term. + * This match generator tries a small fixed set of terms based on the kind of + * relation and the required polarity of the trigger in the quantified formula. + * + * For example, for quantified formula (forall ((x Int)) (=> (> x n) (P x))), + * we have that (> x n) is a relational trigger with required polarity "true". + * This generator will try the match `x -> n+1` only, where notice that n+1 is + * the canonical term chosen to satisfy x>n. Canonical terms for arithmetic + * relations (~ x n) are in set { n, n+1, n-1 }. + * + * If a relational trigger does not have a required polarity, then up to 2 + * terms are tried, a term that satisfies the relation, and one that does not. + * If (>= x n) is a relational trigger with no polarity, then `x -> n` and + * `x -> n-1` will be generated. + * + * Currently this class handles only equality between real or integer valued + * terms, or inequalities (kind GEQ). It furthermore only considers ground terms + * t for the right hand side of relations. + */ +class RelationalMatchGenerator : public InstMatchGenerator +{ + public: + /** + * @param tparent The parent trigger that this match generator belongs to + * @param rtrigger The relational trigger + * @param hasPol Whether the trigger has an entailed polarity + * @param pol The entailed polarity of the relational trigger. + */ + RelationalMatchGenerator(Trigger* tparent, + Node rtrigger, + bool hasPol, + bool pol); + + /** Reset */ + bool reset(Node eqc) override; + /** Get the next match. */ + int getNextMatch(Node q, InstMatch& m) override; + + private: + /** the variable */ + Node d_var; + /** The index of the variable */ + int64_t d_vindex; + /** the relation kind */ + Kind d_rel; + /** the right hand side */ + Node d_rhs; + /** whether we have a required polarity */ + bool d_hasPol; + /** the required polarity, if it exists */ + bool d_pol; + /** + * The current number of terms we have generated since the last call to reset + */ + size_t d_counter; +}; + +} // namespace inst +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 + +#endif diff --git a/src/theory/quantifiers/ematching/trigger_term_info.cpp b/src/theory/quantifiers/ematching/trigger_term_info.cpp index 600797f4e..f31ec088a 100644 --- a/src/theory/quantifiers/ematching/trigger_term_info.cpp +++ b/src/theory/quantifiers/ematching/trigger_term_info.cpp @@ -70,6 +70,46 @@ bool TriggerTermInfo::isRelationalTriggerKind(Kind k) return k == EQUAL || k == GEQ; } +bool TriggerTermInfo::isUsableRelationTrigger(Node n) +{ + bool hasPol, pol; + Node lit; + return isUsableRelationTrigger(n, hasPol, pol, lit); +} +bool TriggerTermInfo::isUsableRelationTrigger(Node n, + bool& hasPol, + bool& pol, + Node& lit) +{ + // relational triggers (not) (= (~ x t) true|false), where ~ in { =, >= }. + hasPol = false; + pol = n.getKind() != NOT; + lit = pol ? n : n[0]; + if (lit.getKind() == EQUAL && lit[1].getType().isBoolean() + && lit[1].isConst()) + { + hasPol = true; + pol = lit[1].getConst<bool>() ? pol : !pol; + lit = lit[0]; + } + // is it a relational trigger? + if ((lit.getKind() == EQUAL && lit[0].getType().isReal()) + || lit.getKind() == GEQ) + { + // if one side of the relation is a variable and the other side is a ground + // term, we can treat this using the relational match generator + for (size_t i = 0; i < 2; i++) + { + if (lit[i].getKind() == INST_CONSTANT + && !quantifiers::TermUtil::hasInstConstAttr(lit[1 - i])) + { + return true; + } + } + } + return false; +} + bool TriggerTermInfo::isSimpleTrigger(Node n) { Node t = n.getKind() == NOT ? n[0] : n; @@ -105,7 +145,7 @@ int32_t TriggerTermInfo::getTriggerWeight(Node n) { return 0; } - if (isAtomicTrigger(n)) + if (isAtomicTrigger(n) || isUsableRelationTrigger(n)) { return 1; } diff --git a/src/theory/quantifiers/ematching/trigger_term_info.h b/src/theory/quantifiers/ematching/trigger_term_info.h index 753d0850c..3816d0988 100644 --- a/src/theory/quantifiers/ematching/trigger_term_info.h +++ b/src/theory/quantifiers/ematching/trigger_term_info.h @@ -108,6 +108,19 @@ class TriggerTermInfo static bool isRelationalTrigger(Node n); /** Is k a relational trigger kind? */ static bool isRelationalTriggerKind(Kind k); + /** + * Is n a usable relational trigger, which is true if RelationalMatchGenerator + * can process n. + */ + static bool isUsableRelationTrigger(Node n); + /** + * Same as above, but lit / hasPol / pol are updated to the required + * constructor arguments for RelationalMatchGenerator. + */ + static bool isUsableRelationTrigger(Node n, + bool& hasPol, + bool& pol, + Node& lit); /** is n a simple trigger (see inst_match_generator.h)? */ static bool isSimpleTrigger(Node n); /** get trigger weight @@ -116,7 +129,8 @@ class TriggerTermInfo * trigger term n, where the smaller the value, the easier. * * Returns 0 for triggers that are APPLY_UF terms. - * Returns 1 for other triggers whose kind is atomic. + * Returns 1 for other triggers whose kind is atomic, or are usable + * relational triggers. * Returns 2 otherwise. */ static int32_t getTriggerWeight(Node n); diff --git a/src/theory/quantifiers/entailment_check.cpp b/src/theory/quantifiers/entailment_check.cpp new file mode 100644 index 000000000..543414a4e --- /dev/null +++ b/src/theory/quantifiers/entailment_check.cpp @@ -0,0 +1,411 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of entailment check class. + */ + +#include "theory/quantifiers/entailment_check.h" + +#include "theory/quantifiers/quantifiers_state.h" +#include "theory/quantifiers/term_database.h" + +using namespace cvc5::kind; +using namespace cvc5::context; + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +EntailmentCheck::EntailmentCheck(Env& env, QuantifiersState& qs, TermDb& tdb) + : EnvObj(env), d_qstate(qs), d_tdb(tdb) +{ + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); +} + +EntailmentCheck::~EntailmentCheck() {} + +Node EntailmentCheck::evaluateTerm2(TNode n, + std::map<TNode, Node>& visited, + std::map<TNode, TNode>& subs, + bool subsRep, + bool useEntailmentTests, + bool reqHasTerm) +{ + std::map<TNode, Node>::iterator itv = visited.find(n); + if (itv != visited.end()) + { + return itv->second; + } + Trace("term-db-eval") << "evaluate term : " << n << std::endl; + Node ret = n; + Kind k = n.getKind(); + if (k == FORALL) + { + // do nothing + } + else if (k == BOUND_VARIABLE) + { + std::map<TNode, TNode>::iterator it = subs.find(n); + if (it != subs.end()) + { + if (!subsRep) + { + Assert(d_qstate.hasTerm(it->second)); + ret = d_qstate.getRepresentative(it->second); + } + else + { + ret = it->second; + } + } + } + else if (d_qstate.hasTerm(n)) + { + Trace("term-db-eval") << "...exists in ee, return rep" << std::endl; + ret = d_qstate.getRepresentative(n); + reqHasTerm = false; + } + else if (n.hasOperator()) + { + std::vector<TNode> args; + bool ret_set = false; + for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++) + { + TNode c = evaluateTerm2( + n[i], visited, subs, subsRep, useEntailmentTests, reqHasTerm); + if (c.isNull()) + { + ret = Node::null(); + ret_set = true; + break; + } + else if (c == d_true || c == d_false) + { + // short-circuiting + if ((k == AND && c == d_false) || (k == OR && c == d_true)) + { + ret = c; + ret_set = true; + reqHasTerm = false; + break; + } + else if (k == ITE && i == 0) + { + ret = evaluateTerm2(n[c == d_true ? 1 : 2], + visited, + subs, + subsRep, + useEntailmentTests, + reqHasTerm); + ret_set = true; + reqHasTerm = false; + break; + } + } + Trace("term-db-eval") << " child " << i << " : " << c << std::endl; + args.push_back(c); + } + if (!ret_set) + { + // get the (indexed) operator of n, if it exists + TNode f = d_tdb.getMatchOperator(n); + // if it is an indexed term, return the congruent term + if (!f.isNull()) + { + // if f is congruent to a term indexed by this class + TNode nn = d_tdb.getCongruentTerm(f, args); + Trace("term-db-eval") << " got congruent term " << nn + << " from DB for " << n << std::endl; + if (!nn.isNull()) + { + ret = d_qstate.getRepresentative(nn); + Trace("term-db-eval") << "return rep" << std::endl; + ret_set = true; + reqHasTerm = false; + Assert(!ret.isNull()); + } + } + if (!ret_set) + { + Trace("term-db-eval") << "return rewrite" << std::endl; + // a theory symbol or a new UF term + if (n.getMetaKind() == metakind::PARAMETERIZED) + { + args.insert(args.begin(), n.getOperator()); + } + ret = NodeManager::currentNM()->mkNode(n.getKind(), args); + ret = rewrite(ret); + if (ret.getKind() == EQUAL) + { + if (d_qstate.areDisequal(ret[0], ret[1])) + { + ret = d_false; + } + } + if (useEntailmentTests) + { + if (ret.getKind() == EQUAL || ret.getKind() == GEQ) + { + Valuation& val = d_qstate.getValuation(); + for (unsigned j = 0; j < 2; j++) + { + std::pair<bool, Node> et = val.entailmentCheck( + options::TheoryOfMode::THEORY_OF_TYPE_BASED, + j == 0 ? ret : ret.negate()); + if (et.first) + { + ret = j == 0 ? d_true : d_false; + break; + } + } + } + } + } + } + } + // must have the term + if (reqHasTerm && !ret.isNull()) + { + Kind rk = ret.getKind(); + if (rk != OR && rk != AND && rk != EQUAL && rk != ITE && rk != NOT + && rk != FORALL) + { + if (!d_qstate.hasTerm(ret)) + { + ret = Node::null(); + } + } + } + Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret + << ", reqHasTerm = " << reqHasTerm << std::endl; + visited[n] = ret; + return ret; +} + +TNode EntailmentCheck::getEntailedTerm2(TNode n, + std::map<TNode, TNode>& subs, + bool subsRep) +{ + Trace("term-db-entail") << "get entailed term : " << n << std::endl; + if (d_qstate.hasTerm(n)) + { + Trace("term-db-entail") << "...exists in ee, return rep " << std::endl; + return n; + } + else if (n.getKind() == BOUND_VARIABLE) + { + std::map<TNode, TNode>::iterator it = subs.find(n); + if (it != subs.end()) + { + Trace("term-db-entail") + << "...substitution is : " << it->second << std::endl; + if (subsRep) + { + Assert(d_qstate.hasTerm(it->second)); + Assert(d_qstate.getRepresentative(it->second) == it->second); + return it->second; + } + return getEntailedTerm2(it->second, subs, subsRep); + } + } + else if (n.getKind() == ITE) + { + for (uint32_t i = 0; i < 2; i++) + { + if (isEntailed2(n[0], subs, subsRep, i == 0)) + { + return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep); + } + } + } + else + { + if (n.hasOperator()) + { + TNode f = d_tdb.getMatchOperator(n); + if (!f.isNull()) + { + std::vector<TNode> args; + for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++) + { + TNode c = getEntailedTerm2(n[i], subs, subsRep); + if (c.isNull()) + { + return TNode::null(); + } + c = d_qstate.getRepresentative(c); + Trace("term-db-entail") << " child " << i << " : " << c << std::endl; + args.push_back(c); + } + TNode nn = d_tdb.getCongruentTerm(f, args); + Trace("term-db-entail") + << " got congruent term " << nn << " for " << n << std::endl; + return nn; + } + } + } + return TNode::null(); +} + +Node EntailmentCheck::evaluateTerm(TNode n, + std::map<TNode, TNode>& subs, + bool subsRep, + bool useEntailmentTests, + bool reqHasTerm) +{ + std::map<TNode, Node> visited; + return evaluateTerm2( + n, visited, subs, subsRep, useEntailmentTests, reqHasTerm); +} + +Node EntailmentCheck::evaluateTerm(TNode n, + bool useEntailmentTests, + bool reqHasTerm) +{ + std::map<TNode, Node> visited; + std::map<TNode, TNode> subs; + return evaluateTerm2(n, visited, subs, false, useEntailmentTests, reqHasTerm); +} + +TNode EntailmentCheck::getEntailedTerm(TNode n, + std::map<TNode, TNode>& subs, + bool subsRep) +{ + return getEntailedTerm2(n, subs, subsRep); +} + +TNode EntailmentCheck::getEntailedTerm(TNode n) +{ + std::map<TNode, TNode> subs; + return getEntailedTerm2(n, subs, false); +} + +bool EntailmentCheck::isEntailed2(TNode n, + std::map<TNode, TNode>& subs, + bool subsRep, + bool pol) +{ + Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol + << std::endl; + Assert(n.getType().isBoolean()); + if (n.getKind() == EQUAL && !n[0].getType().isBoolean()) + { + TNode n1 = getEntailedTerm2(n[0], subs, subsRep); + if (!n1.isNull()) + { + TNode n2 = getEntailedTerm2(n[1], subs, subsRep); + if (!n2.isNull()) + { + if (n1 == n2) + { + return pol; + } + else + { + Assert(d_qstate.hasTerm(n1)); + Assert(d_qstate.hasTerm(n2)); + if (pol) + { + return d_qstate.areEqual(n1, n2); + } + else + { + return d_qstate.areDisequal(n1, n2); + } + } + } + } + } + else if (n.getKind() == NOT) + { + return isEntailed2(n[0], subs, subsRep, !pol); + } + else if (n.getKind() == OR || n.getKind() == AND) + { + bool simPol = (pol && n.getKind() == OR) || (!pol && n.getKind() == AND); + for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++) + { + if (isEntailed2(n[i], subs, subsRep, pol)) + { + if (simPol) + { + return true; + } + } + else + { + if (!simPol) + { + return false; + } + } + } + return !simPol; + // Boolean equality here + } + else if (n.getKind() == EQUAL || n.getKind() == ITE) + { + for (size_t i = 0; i < 2; i++) + { + if (isEntailed2(n[0], subs, subsRep, i == 0)) + { + size_t ch = (n.getKind() == EQUAL || i == 0) ? 1 : 2; + bool reqPol = (n.getKind() == ITE || i == 0) ? pol : !pol; + return isEntailed2(n[ch], subs, subsRep, reqPol); + } + } + } + else if (n.getKind() == APPLY_UF) + { + TNode n1 = getEntailedTerm2(n, subs, subsRep); + if (!n1.isNull()) + { + Assert(d_qstate.hasTerm(n1)); + if (n1 == d_true) + { + return pol; + } + else if (n1 == d_false) + { + return !pol; + } + else + { + return d_qstate.getRepresentative(n1) == (pol ? d_true : d_false); + } + } + } + else if (n.getKind() == FORALL && !pol) + { + return isEntailed2(n[1], subs, subsRep, pol); + } + return false; +} + +bool EntailmentCheck::isEntailed(TNode n, bool pol) +{ + std::map<TNode, TNode> subs; + return isEntailed2(n, subs, false, pol); +} + +bool EntailmentCheck::isEntailed(TNode n, + std::map<TNode, TNode>& subs, + bool subsRep, + bool pol) +{ + return isEntailed2(n, subs, subsRep, pol); +} + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/quantifiers/entailment_check.h b/src/theory/quantifiers/entailment_check.h new file mode 100644 index 000000000..ecf74fe85 --- /dev/null +++ b/src/theory/quantifiers/entailment_check.h @@ -0,0 +1,156 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Entailment check class + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__QUANTIFIERS__ENTAILMENT_CHECK_H +#define CVC5__THEORY__QUANTIFIERS__ENTAILMENT_CHECK_H + +#include <map> +#include <vector> + +#include "expr/node.h" +#include "smt/env_obj.h" + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +class QuantifiersState; +class TermDb; + +/** + * Entailment check utility, which determines whether formulas are entailed + * in the current context. The main focus of this class is on UF formulas. + * It works by looking at the term argument trie data structures in term + * database. For details, see e.g. Section 4.1 of Reynolds et al TACAS 2018. + */ +class EntailmentCheck : protected EnvObj +{ + public: + EntailmentCheck(Env& env, QuantifiersState& qs, TermDb& tdb); + ~EntailmentCheck(); + /** evaluate term + * + * Returns a term n' such that n * subs = n' is entailed based on the current + * set of equalities, where ( n * subs ) is term n under the substitution + * subs. + * + * This function may generate new terms. In particular, we typically rewrite + * subterms of n of maximal size (in terms of the AST) to terms that exist + * in the equality engine. + * + * useEntailmentTests is whether to call the theory engine's entailmentTest + * on literals n for which this call fails to find a term n' that is + * equivalent to n, for increased precision. This is not frequently used. + * + * If reqHasTerm, then we require that the returned term is a Boolean + * combination of terms that exist in the equality engine used by this call. + * If no such term is constructable, this call returns null. The motivation + * for setting this to true is to "fail fast" if we require the return value + * of this function to only involve existing terms. This is used e.g. in + * the "propagating instances" portion of conflict-based instantiation + * (quant_conflict_find.h). + * + * @param n The term under consideration + * @param subs The substitution under consideration + * @param subsRep Whether the range of subs are representatives in the current + * equality engine + * @param useEntailmentTests Whether to use entailment tests to show + * n * subs is equivalent to true/false. + * @param reqHasTerm Whether we require the returned term to be a Boolean + * combination of terms known to the current equality engine + * @return the term n * subs evaluates to + */ + Node evaluateTerm(TNode n, + std::map<TNode, TNode>& subs, + bool subsRep, + bool useEntailmentTests = false, + bool reqHasTerm = false); + /** Same as above, without a substitution */ + Node evaluateTerm(TNode n, + bool useEntailmentTests = false, + bool reqHasTerm = false); + /** get entailed term + * + * If possible, returns a term n' such that: + * (1) n' exists in the current equality engine (as specified by the state), + * (2) n = n' is entailed in the current context. + * It returns null if no such term can be found. + * Wrt evaluateTerm, this version does not construct new terms, and + * thus is less aggressive. + */ + TNode getEntailedTerm(TNode n); + /** get entailed term + * + * If possible, returns a term n' such that: + * (1) n' exists in the current equality engine (as specified by the state), + * (2) n * subs = n' is entailed in the current context, where * denotes + * substitution application. + * It returns null if no such term can be found. + * subsRep is whether the substitution maps to terms that are representatives + * according to the quantifiers state. + * Wrt evaluateTerm, this version does not construct new terms, and + * thus is less aggressive. + */ + TNode getEntailedTerm(TNode n, std::map<TNode, TNode>& subs, bool subsRep); + /** is entailed + * Checks whether the current context entails n with polarity pol, based on + * the equality information in the quantifiers state. Returns true if the + * entailment can be successfully shown. + */ + bool isEntailed(TNode n, bool pol); + /** is entailed + * + * Checks whether the current context entails ( n * subs ) with polarity pol, + * based on the equality information in the quantifiers state, + * where * denotes substitution application. + * subsRep is whether the substitution maps to terms that are representatives + * according to in the quantifiers state. + */ + bool isEntailed(TNode n, + std::map<TNode, TNode>& subs, + bool subsRep, + bool pol); + + protected: + /** helper for evaluate term */ + Node evaluateTerm2(TNode n, + std::map<TNode, Node>& visited, + std::map<TNode, TNode>& subs, + bool subsRep, + bool useEntailmentTests, + bool reqHasTerm); + /** helper for get entailed term */ + TNode getEntailedTerm2(TNode n, std::map<TNode, TNode>& subs, bool subsRep); + /** helper for is entailed */ + bool isEntailed2(TNode n, + std::map<TNode, TNode>& subs, + bool subsRep, + bool pol); + /** The quantifiers state object */ + QuantifiersState& d_qstate; + /** Reference to the term database */ + TermDb& d_tdb; + /** boolean terms */ + Node d_true; + Node d_false; +}; /* class EntailmentCheck */ + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__THEORY__QUANTIFIERS__ENTAILMENT_CHECK_H */ diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 7c1d36ce8..94351274a 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -951,10 +951,15 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n Node r = n; if( !n.isConst() ){ TypeNode tn = n.getType(); - if( !fm->hasTerm(n) && tn.isFirstClass() ){ - r = getSomeDomainElement(fm, tn ); + if (!fm->hasTerm(n) && tn.isFirstClass()) + { + // if the term is unknown, we do not assume any value for it + r = Node::null(); + } + else + { + r = fm->getRepresentative(r); } - r = fm->getRepresentative( r ); } Trace("fmc-debug") << "Add constant entry..." << std::endl; d.addEntry(fm, mkCondDefault(fm, f), r); diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index f756fcfd1..be04f9404 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -25,6 +25,7 @@ #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" +#include "theory/quantifiers/entailment_check.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_preprocess.h" @@ -183,7 +184,7 @@ bool Instantiate::addInstantiation(Node q, #endif } - TermDb* tdb = d_treg.getTermDatabase(); + EntailmentCheck* ec = d_treg.getEntailmentCheck(); // Note we check for entailment before checking for term vector duplication. // Although checking for term vector duplication is a faster check, it is // included automatically with recordInstantiationInternal, hence we prefer @@ -206,7 +207,7 @@ bool Instantiate::addInstantiation(Node q, { subs[q[0][i]] = terms[i]; } - if (tdb->isEntailed(q[1], subs, false, true)) + if (ec->isEntailed(q[1], subs, false, true)) { Trace("inst-add-debug") << " --> Currently entailed." << std::endl; ++(d_statistics.d_inst_duplicate_ent); @@ -217,6 +218,7 @@ bool Instantiate::addInstantiation(Node q, // check based on instantiation level if (options::instMaxLevel() != -1) { + TermDb* tdb = d_treg.getTermDatabase(); for (Node& t : terms) { if (!tdb->isTermEligibleForInstantiation(t, q)) @@ -409,7 +411,7 @@ bool Instantiate::addInstantiationExpFail(Node q, // will never succeed with 1 variable return false; } - TermDb* tdb = d_treg.getTermDatabase(); + EntailmentCheck* echeck = d_treg.getEntailmentCheck(); Trace("inst-exp-fail") << "Explain inst failure..." << terms << std::endl; // set up information for below std::vector<Node>& vars = d_qreg.d_vars[q]; @@ -445,7 +447,7 @@ bool Instantiate::addInstantiationExpFail(Node q, if (options::instNoEntail()) { Trace("inst-exp-fail") << " check entailment" << std::endl; - success = tdb->isEntailed(q[1], subs, false, true); + success = echeck->isEntailed(q[1], subs, false, true); Trace("inst-exp-fail") << " entailed: " << success << std::endl; } // check whether the instantiation rewrites to the same thing diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 361adfd54..323398879 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -52,12 +52,6 @@ QuantInfo::~QuantInfo() { d_var_mg.clear(); } -QuantifiersInferenceManager& QuantInfo::getInferenceManager() -{ - Assert(d_parent != nullptr); - return d_parent->getInferenceManager(); -} - void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) { d_parent = p; d_q = q; @@ -577,30 +571,33 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, { if( options::qcfEagerTest() ){ //check whether the instantiation evaluates as expected + EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck(); + std::map<TNode, TNode> subs; + for (size_t i = 0, tsize = terms.size(); i < tsize; i++) + { + Trace("qcf-instance-check") << " " << terms[i] << std::endl; + subs[d_q[0][i]] = terms[i]; + } + for (size_t i = 0, evsize = d_extra_var.size(); i < evsize; i++) + { + Node n = getCurrentExpValue(d_extra_var[i]); + Trace("qcf-instance-check") + << " " << d_extra_var[i] << " -> " << n << std::endl; + subs[d_extra_var[i]] = n; + } if (p->atConflictEffort()) { Trace("qcf-instance-check") << "Possible conflict instance for " << d_q << " : " << std::endl; - std::map< TNode, TNode > subs; - for( unsigned i=0; i<terms.size(); i++ ){ - Trace("qcf-instance-check") << " " << terms[i] << std::endl; - subs[d_q[0][i]] = terms[i]; - } - TermDb* tdb = p->getTermDatabase(); - for( unsigned i=0; i<d_extra_var.size(); i++ ){ - Node n = getCurrentExpValue( d_extra_var[i] ); - Trace("qcf-instance-check") << " " << d_extra_var[i] << " -> " << n << std::endl; - subs[d_extra_var[i]] = n; - } - if (!tdb->isEntailed(d_q[1], subs, false, false)) + if (!echeck->isEntailed(d_q[1], subs, false, false)) { Trace("qcf-instance-check") << "...not entailed to be false." << std::endl; return true; } }else{ - Node inst = - getInferenceManager().getInstantiate()->getInstantiation(d_q, terms); - inst = Rewriter::rewrite(inst); - Node inst_eval = p->getTermDatabase()->evaluateTerm( - inst, options::qcfTConstraint(), true); + // see if the body of the quantified formula evaluates to a Boolean + // combination of known terms under the current substitution. We use + // the helper method evaluateTerm from the entailment check utility. + Node inst_eval = echeck->evaluateTerm( + d_q[1], subs, false, options::qcfTConstraint(), true); if( Trace.isOn("qcf-instance-check") ){ Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl; for( unsigned i=0; i<terms.size(); i++ ){ @@ -608,6 +605,10 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, } Trace("qcf-instance-check") << "...evaluates to " << inst_eval << std::endl; } + // If it is the case that instantiation can be rewritten to a Boolean + // combination of terms that exist in the current context, then inst_eval + // is non-null. Moreover, we insist that inst_eval is not true, or else + // the instantiation is trivially entailed and hence is spurious. if (inst_eval.isNull() || (inst_eval.isConst() && inst_eval.getConst<bool>())) { @@ -1219,11 +1220,11 @@ bool MatchGen::reset_round(QuantConflictFind* p) // d_ground_eval[0] = p->d_false; //} // modified - TermDb* tdb = p->getTermDatabase(); + EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck(); QuantifiersState& qs = p->getState(); for (unsigned i = 0; i < 2; i++) { - if (tdb->isEntailed(d_n, i == 0)) + if (echeck->isEntailed(d_n, i == 0)) { d_ground_eval[0] = i==0 ? p->d_true : p->d_false; } @@ -1233,13 +1234,13 @@ bool MatchGen::reset_round(QuantConflictFind* p) } } }else if( d_type==typ_eq ){ - TermDb* tdb = p->getTermDatabase(); + EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck(); QuantifiersState& qs = p->getState(); for (unsigned i = 0, size = d_n.getNumChildren(); i < size; i++) { if (!expr::hasBoundVar(d_n[i])) { - TNode t = tdb->getEntailedTerm(d_n[i]); + TNode t = echeck->getEntailedTerm(d_n[i]); if (qs.isInConflict()) { return false; @@ -1289,13 +1290,9 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { TNode n = qi->getCurrentValue( d_n ); int vn = qi->getCurrentRepVar( qi->getVarNum( n ) ); if( vn==-1 ){ - //evaluate the value, see if it is compatible - //int e = p->evaluate( n ); - //if( ( e==1 && d_tgt ) || ( e==0 && !d_tgt ) ){ - // d_child_counter = 0; - //} - //modified - if( p->getTermDatabase()->isEntailed( n, d_tgt ) ){ + EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck(); + if (echeck->isEntailed(n, d_tgt)) + { d_child_counter = 0; } }else{ @@ -2168,8 +2165,8 @@ void QuantConflictFind::checkQuantifiedFormula(Node q, Node inst = qinst->getInstantiation(q, terms); Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; - Assert(!getTermDatabase()->isEntailed(inst, true)); - Assert(getTermDatabase()->isEntailed(inst, false) + Assert(!getTermRegistry().getEntailmentCheck()->isEntailed(inst, true)); + Assert(getTermRegistry().getEntailmentCheck()->isEntailed(inst, false) || d_effort > EFFORT_CONFLICT); } // Process the lemma: either add an instantiation or specific lemmas diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 927a74ff2..d14e281fb 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -132,8 +132,6 @@ public: public: QuantInfo(); ~QuantInfo(); - /** Get quantifiers inference manager */ - QuantifiersInferenceManager& getInferenceManager(); std::vector< TNode > d_vars; std::vector< TypeNode > d_var_types; std::map< TNode, int > d_var_num; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 7c7c7aade..52e90e26e 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/quantifiers_rewriter.h" +#include "expr/ascription_type.h" #include "expr/bound_var_manager.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" @@ -895,12 +896,25 @@ bool QuantifiersRewriter::getVarElimLit(Node body, const DType& dt = datatypes::utils::datatypeOf(tester); const DTypeConstructor& c = dt[index]; std::vector<Node> newChildren; - newChildren.push_back(c.getConstructor()); + Node cons = c.getConstructor(); + TypeNode tspec; + // take into account if parametric + if (dt.isParametric()) + { + tspec = c.getSpecializedConstructorType(lit[0].getType()); + cons = nm->mkNode( + APPLY_TYPE_ASCRIPTION, nm->mkConst(AscriptionType(tspec)), cons); + } + else + { + tspec = cons.getType(); + } + newChildren.push_back(cons); std::vector<Node> newVars; BoundVarManager* bvm = nm->getBoundVarManager(); - for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++) + for (size_t j = 0, nargs = c.getNumArgs(); j < nargs; j++) { - TypeNode tn = c[j].getRangeType(); + TypeNode tn = tspec[j]; Node rn = nm->mkConst(Rational(j)); Node cacheVal = BoundVarManager::getCacheValue(body, lit, rn); Node v = bvm->mkBoundVar<QRewDtExpandAttribute>(cacheVal, tn); diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index c8e14e4bd..fdc0b28e0 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -39,6 +39,7 @@ Cegis::Cegis(Env& env, SynthConjecture* p) : SygusModule(env, qs, qim, tds, p), d_eval_unfold(tds->getEvalUnfold()), + d_cexClosedEnum(false), d_cegis_sampler(env), d_usingSymCons(false) { @@ -47,11 +48,18 @@ Cegis::Cegis(Env& env, bool Cegis::initialize(Node conj, Node n, const std::vector<Node>& candidates) { d_base_body = n; + d_cexClosedEnum = true; if (d_base_body.getKind() == NOT && d_base_body[0].getKind() == FORALL) { for (const Node& v : d_base_body[0][0]) { d_base_vars.push_back(v); + if (!v.getType().isClosedEnumerable()) + { + // not closed enumerable, refinement lemmas cannot be sent to the + // quantifier-free datatype solver + d_cexClosedEnum = false; + } } d_base_body = d_base_body[0][1]; } @@ -467,14 +475,18 @@ void Cegis::addRefinementLemmaConjunct(unsigned wcounter, void Cegis::registerRefinementLemma(const std::vector<Node>& vars, Node lem) { addRefinementLemma(lem); - // Make the refinement lemma and add it to lems. - // This lemma is guarded by the parent's guard, which has the semantics - // "this conjecture has a solution", hence this lemma states: - // if the parent conjecture has a solution, it satisfies the specification - // for the given concrete point. - Node rlem = - NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), lem); - d_qim.addPendingLemma(rlem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE); + // must be closed enumerable + if (d_cexClosedEnum && options().quantifiers.sygusEvalUnfold) + { + // Make the refinement lemma and add it to lems. + // This lemma is guarded by the parent's guard, which has the semantics + // "this conjecture has a solution", hence this lemma states: + // if the parent conjecture has a solution, it satisfies the specification + // for the given concrete point. + Node rlem = NodeManager::currentNM()->mkNode( + OR, d_parent->getGuard().negate(), lem); + d_qim.addPendingLemma(rlem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE); + } } bool Cegis::usingRepairConst() { return true; } diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 8e0fffdd1..8d1f0a1b2 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -119,6 +119,13 @@ class Cegis : public SygusModule std::vector<Node> d_rl_vals; /** all variables appearing in refinement lemmas */ std::unordered_set<Node> d_refinement_lemma_vars; + /** + * Are the counterexamples we are handling in this class of only closed + * enumerable types (see TypeNode::isClosedEnumerable). If this is false, + * then CEGIS refinement lemmas can contain terms that are unhandled by + * theory solvers, e.g. uninterpreted constants. + */ + bool d_cexClosedEnum; /** adds lem as a refinement lemma */ void addRefinementLemma(Node lem); diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 43c958ff9..9b4cfb9e1 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -20,6 +20,7 @@ #include "expr/ascription_type.h" #include "expr/dtype_cons.h" +#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" #include "theory/datatypes/sygus_datatype_utils.h" @@ -420,6 +421,8 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, { // generate constant array over the first element of the constituent type Node c = type.mkGroundTerm(); + // note that c should never contain an uninterpreted constant + Assert(!expr::hasSubtermKind(UNINTERPRETED_CONSTANT, c)); ops.push_back(c); } else if (type.isRoundingMode()) diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index b1537a390..573cab7bf 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -451,366 +451,6 @@ bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) { } } -Node TermDb::evaluateTerm2(TNode n, - std::map<TNode, Node>& visited, - std::vector<Node>& exp, - bool useEntailmentTests, - bool computeExp, - bool reqHasTerm) -{ - std::map< TNode, Node >::iterator itv = visited.find( n ); - if( itv != visited.end() ){ - return itv->second; - } - size_t prevSize = exp.size(); - Trace("term-db-eval") << "evaluate term : " << n << std::endl; - Node ret = n; - if( n.getKind()==FORALL || n.getKind()==BOUND_VARIABLE ){ - //do nothing - } - else if (d_qstate.hasTerm(n)) - { - Trace("term-db-eval") << "...exists in ee, return rep" << std::endl; - ret = d_qstate.getRepresentative(n); - if (computeExp) - { - if (n != ret) - { - exp.push_back(n.eqNode(ret)); - } - } - reqHasTerm = false; - } - else if (n.hasOperator()) - { - std::vector<TNode> args; - bool ret_set = false; - Kind k = n.getKind(); - std::vector<Node> tempExp; - for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++) - { - TNode c = evaluateTerm2(n[i], - visited, - tempExp, - useEntailmentTests, - computeExp, - reqHasTerm); - if (c.isNull()) - { - ret = Node::null(); - ret_set = true; - break; - } - else if (c == d_true || c == d_false) - { - // short-circuiting - if ((k == AND && c == d_false) || (k == OR && c == d_true)) - { - ret = c; - ret_set = true; - reqHasTerm = false; - break; - } - else if (k == ITE && i == 0) - { - ret = evaluateTerm2(n[c == d_true ? 1 : 2], - visited, - tempExp, - useEntailmentTests, - computeExp, - reqHasTerm); - ret_set = true; - reqHasTerm = false; - break; - } - } - if (computeExp) - { - exp.insert(exp.end(), tempExp.begin(), tempExp.end()); - } - Trace("term-db-eval") << " child " << i << " : " << c << std::endl; - args.push_back(c); - } - if (ret_set) - { - // if we short circuited - if (computeExp) - { - exp.clear(); - exp.insert(exp.end(), tempExp.begin(), tempExp.end()); - } - } - else - { - // get the (indexed) operator of n, if it exists - TNode f = getMatchOperator(n); - // if it is an indexed term, return the congruent term - if (!f.isNull()) - { - // if f is congruent to a term indexed by this class - TNode nn = getCongruentTerm(f, args); - Trace("term-db-eval") << " got congruent term " << nn - << " from DB for " << n << std::endl; - if (!nn.isNull()) - { - if (computeExp) - { - Assert(nn.getNumChildren() == n.getNumChildren()); - for (unsigned i = 0, nchild = nn.getNumChildren(); i < nchild; i++) - { - if (nn[i] != n[i]) - { - exp.push_back(nn[i].eqNode(n[i])); - } - } - } - ret = d_qstate.getRepresentative(nn); - Trace("term-db-eval") << "return rep" << std::endl; - ret_set = true; - reqHasTerm = false; - Assert(!ret.isNull()); - if (computeExp) - { - if (n != ret) - { - exp.push_back(nn.eqNode(ret)); - } - } - } - } - if( !ret_set ){ - Trace("term-db-eval") << "return rewrite" << std::endl; - // a theory symbol or a new UF term - if (n.getMetaKind() == metakind::PARAMETERIZED) - { - args.insert(args.begin(), n.getOperator()); - } - ret = NodeManager::currentNM()->mkNode(n.getKind(), args); - ret = rewrite(ret); - if (ret.getKind() == EQUAL) - { - if (d_qstate.areDisequal(ret[0], ret[1])) - { - ret = d_false; - } - } - if (useEntailmentTests) - { - if (ret.getKind() == EQUAL || ret.getKind() == GEQ) - { - Valuation& val = d_qstate.getValuation(); - for (unsigned j = 0; j < 2; j++) - { - std::pair<bool, Node> et = val.entailmentCheck( - options::TheoryOfMode::THEORY_OF_TYPE_BASED, - j == 0 ? ret : ret.negate()); - if (et.first) - { - ret = j == 0 ? d_true : d_false; - if (computeExp) - { - exp.push_back(et.second); - } - break; - } - } - } - } - } - } - } - // must have the term - if (reqHasTerm && !ret.isNull()) - { - Kind k = ret.getKind(); - if (k != OR && k != AND && k != EQUAL && k != ITE && k != NOT - && k != FORALL) - { - if (!d_qstate.hasTerm(ret)) - { - ret = Node::null(); - } - } - } - Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret - << ", reqHasTerm = " << reqHasTerm << std::endl; - // clear the explanation if failed - if (computeExp && ret.isNull()) - { - exp.resize(prevSize); - } - visited[n] = ret; - return ret; -} - -TNode TermDb::getEntailedTerm2(TNode n, - std::map<TNode, TNode>& subs, - bool subsRep, - bool hasSubs) -{ - Trace("term-db-entail") << "get entailed term : " << n << std::endl; - if (d_qstate.hasTerm(n)) - { - Trace("term-db-entail") << "...exists in ee, return rep " << std::endl; - return n; - }else if( n.getKind()==BOUND_VARIABLE ){ - if( hasSubs ){ - std::map< TNode, TNode >::iterator it = subs.find( n ); - if( it!=subs.end() ){ - Trace("term-db-entail") << "...substitution is : " << it->second << std::endl; - if( subsRep ){ - Assert(d_qstate.hasTerm(it->second)); - Assert(d_qstate.getRepresentative(it->second) == it->second); - return it->second; - } - return getEntailedTerm2(it->second, subs, subsRep, hasSubs); - } - } - }else if( n.getKind()==ITE ){ - for( unsigned i=0; i<2; i++ ){ - if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0)) - { - return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep, hasSubs); - } - } - }else{ - if( n.hasOperator() ){ - TNode f = getMatchOperator( n ); - if( !f.isNull() ){ - std::vector< TNode > args; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - TNode c = getEntailedTerm2(n[i], subs, subsRep, hasSubs); - if( c.isNull() ){ - return TNode::null(); - } - c = d_qstate.getRepresentative(c); - Trace("term-db-entail") << " child " << i << " : " << c << std::endl; - args.push_back( c ); - } - TNode nn = getCongruentTerm(f, args); - Trace("term-db-entail") << " got congruent term " << nn << " for " << n << std::endl; - return nn; - } - } - } - return TNode::null(); -} - -Node TermDb::evaluateTerm(TNode n, - bool useEntailmentTests, - bool reqHasTerm) -{ - std::map< TNode, Node > visited; - std::vector<Node> exp; - return evaluateTerm2(n, visited, exp, useEntailmentTests, false, reqHasTerm); -} - -Node TermDb::evaluateTerm(TNode n, - std::vector<Node>& exp, - bool useEntailmentTests, - bool reqHasTerm) -{ - std::map<TNode, Node> visited; - return evaluateTerm2(n, visited, exp, useEntailmentTests, true, reqHasTerm); -} - -TNode TermDb::getEntailedTerm(TNode n, - std::map<TNode, TNode>& subs, - bool subsRep) -{ - return getEntailedTerm2(n, subs, subsRep, true); -} - -TNode TermDb::getEntailedTerm(TNode n) -{ - std::map< TNode, TNode > subs; - return getEntailedTerm2(n, subs, false, false); -} - -bool TermDb::isEntailed2( - TNode n, std::map<TNode, TNode>& subs, bool subsRep, bool hasSubs, bool pol) -{ - Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl; - Assert(n.getType().isBoolean()); - if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){ - TNode n1 = getEntailedTerm2(n[0], subs, subsRep, hasSubs); - if( !n1.isNull() ){ - TNode n2 = getEntailedTerm2(n[1], subs, subsRep, hasSubs); - if( !n2.isNull() ){ - if( n1==n2 ){ - return pol; - }else{ - Assert(d_qstate.hasTerm(n1)); - Assert(d_qstate.hasTerm(n2)); - if( pol ){ - return d_qstate.areEqual(n1, n2); - }else{ - return d_qstate.areDisequal(n1, n2); - } - } - } - } - }else if( n.getKind()==NOT ){ - return isEntailed2(n[0], subs, subsRep, hasSubs, !pol); - }else if( n.getKind()==OR || n.getKind()==AND ){ - bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ); - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if (isEntailed2(n[i], subs, subsRep, hasSubs, pol)) - { - if( simPol ){ - return true; - } - }else{ - if( !simPol ){ - return false; - } - } - } - return !simPol; - //Boolean equality here - }else if( n.getKind()==EQUAL || n.getKind()==ITE ){ - for( unsigned i=0; i<2; i++ ){ - if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0)) - { - unsigned ch = ( n.getKind()==EQUAL || i==0 ) ? 1 : 2; - bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol; - return isEntailed2(n[ch], subs, subsRep, hasSubs, reqPol); - } - } - }else if( n.getKind()==APPLY_UF ){ - TNode n1 = getEntailedTerm2(n, subs, subsRep, hasSubs); - if( !n1.isNull() ){ - Assert(d_qstate.hasTerm(n1)); - if( n1==d_true ){ - return pol; - }else if( n1==d_false ){ - return !pol; - }else{ - return d_qstate.getRepresentative(n1) == (pol ? d_true : d_false); - } - } - }else if( n.getKind()==FORALL && !pol ){ - return isEntailed2(n[1], subs, subsRep, hasSubs, pol); - } - return false; -} - -bool TermDb::isEntailed(TNode n, bool pol) -{ - Assert(d_consistent_ee); - std::map< TNode, TNode > subs; - return isEntailed2(n, subs, false, false, pol); -} - -bool TermDb::isEntailed(TNode n, - std::map<TNode, TNode>& subs, - bool subsRep, - bool pol) -{ - Assert(d_consistent_ee); - return isEntailed2(n, subs, subsRep, true, pol); -} - bool TermDb::isTermActive( Node n ) { return d_inactive_map.find( n )==d_inactive_map.end(); //return !n.getAttribute(NoMatchAttribute()); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index af0b87bd8..0e5c7bc01 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -176,78 +176,6 @@ class TermDb : public QuantifiersUtil { * equivalence class of r. */ bool inRelevantDomain(TNode f, unsigned i, TNode r); - /** evaluate term - * - * Returns a term n' such that n = n' is entailed based on the equality - * information ee. This function may generate new terms. In particular, - * we typically rewrite subterms of n of maximal size to terms that exist in - * the equality engine specified by ee. - * - * useEntailmentTests is whether to call the theory engine's entailmentTest - * on literals n for which this call fails to find a term n' that is - * equivalent to n, for increased precision. This is not frequently used. - * - * The vector exp stores the explanation for why n evaluates to that term, - * that is, if this call returns a non-null node n', then: - * exp => n = n' - * - * If reqHasTerm, then we require that the returned term is a Boolean - * combination of terms that exist in the equality engine used by this call. - * If no such term is constructable, this call returns null. The motivation - * for setting this to true is to "fail fast" if we require the return value - * of this function to only involve existing terms. This is used e.g. in - * the "propagating instances" portion of conflict-based instantiation - * (quant_conflict_find.h). - */ - Node evaluateTerm(TNode n, - std::vector<Node>& exp, - bool useEntailmentTests = false, - bool reqHasTerm = false); - /** same as above, without exp */ - Node evaluateTerm(TNode n, - bool useEntailmentTests = false, - bool reqHasTerm = false); - /** get entailed term - * - * If possible, returns a term n' such that: - * (1) n' exists in the current equality engine (as specified by the state), - * (2) n = n' is entailed in the current context. - * It returns null if no such term can be found. - * Wrt evaluateTerm, this version does not construct new terms, and - * thus is less aggressive. - */ - TNode getEntailedTerm(TNode n); - /** get entailed term - * - * If possible, returns a term n' such that: - * (1) n' exists in the current equality engine (as specified by the state), - * (2) n * subs = n' is entailed in the current context, where * denotes - * substitution application. - * It returns null if no such term can be found. - * subsRep is whether the substitution maps to terms that are representatives - * according to the quantifiers state. - * Wrt evaluateTerm, this version does not construct new terms, and - * thus is less aggressive. - */ - TNode getEntailedTerm(TNode n, std::map<TNode, TNode>& subs, bool subsRep); - /** is entailed - * Checks whether the current context entails n with polarity pol, based on - * the equality information in the quantifiers state. Returns true if the - * entailment can be successfully shown. - */ - bool isEntailed(TNode n, bool pol); - /** is entailed - * - * Checks whether the current context entails ( n * subs ) with polarity pol, - * based on the equality information in the quantifiers state, - * where * denotes substitution application. - * subsRep is whether the substitution maps to terms that are representatives - * according to in the quantifiers state. - */ - bool isEntailed(TNode n, - std::map<TNode, TNode>& subs, - bool subsRep, - bool pol); /** is the term n active in the current context? * * By default, all terms are active. A term is inactive if: @@ -355,24 +283,6 @@ class TermDb : public QuantifiersUtil { //----------------------------- end implementation-specific /** set has term */ void setHasTerm( Node n ); - /** helper for evaluate term */ - Node evaluateTerm2(TNode n, - std::map<TNode, Node>& visited, - std::vector<Node>& exp, - bool useEntailmentTests, - bool computeExp, - bool reqHasTerm); - /** helper for get entailed term */ - TNode getEntailedTerm2(TNode n, - std::map<TNode, TNode>& subs, - bool subsRep, - bool hasSubs); - /** helper for is entailed */ - bool isEntailed2(TNode n, - std::map<TNode, TNode>& subs, - bool subsRep, - bool hasSubs, - bool pol); /** compute uf eqc terms : * Ensure entries for f are in d_func_map_eqc_trie for all equivalence classes */ diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp index ab999ad9b..d11fb0b8d 100644 --- a/src/theory/quantifiers/term_registry.cpp +++ b/src/theory/quantifiers/term_registry.cpp @@ -18,6 +18,7 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" +#include "theory/quantifiers/entailment_check.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/first_order_model_fmc.h" #include "theory/quantifiers/ho_term_database.h" @@ -39,6 +40,7 @@ TermRegistry::TermRegistry(Env& env, d_termPools(new TermPools(env, qs)), d_termDb(logicInfo().isHigherOrder() ? new HoTermDb(env, qs, qr) : new TermDb(env, qs, qr)), + d_echeck(new EntailmentCheck(env, qs, *d_termDb.get())), d_sygusTdb(nullptr), d_qmodel(nullptr) { @@ -132,6 +134,11 @@ TermDbSygus* TermRegistry::getTermDatabaseSygus() const return d_sygusTdb.get(); } +EntailmentCheck* TermRegistry::getEntailmentCheck() const +{ + return d_echeck.get(); +} + TermEnumeration* TermRegistry::getTermEnumeration() const { return d_termEnum.get(); diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h index 175d450df..60a87a91f 100644 --- a/src/theory/quantifiers/term_registry.h +++ b/src/theory/quantifiers/term_registry.h @@ -23,6 +23,7 @@ #include "context/cdhashset.h" #include "smt/env_obj.h" +#include "theory/quantifiers/entailment_check.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" @@ -83,6 +84,8 @@ class TermRegistry : protected EnvObj TermDb* getTermDatabase() const; /** get term database sygus */ TermDbSygus* getTermDatabaseSygus() const; + /** get entailment check utility */ + EntailmentCheck* getEntailmentCheck() const; /** get term enumeration utility */ TermEnumeration* getTermEnumeration() const; /** get the term pools utility */ @@ -103,6 +106,8 @@ class TermRegistry : protected EnvObj std::unique_ptr<TermPools> d_termPools; /** term database */ std::unique_ptr<TermDb> d_termDb; + /** entailment check */ + std::unique_ptr<EntailmentCheck> d_echeck; /** sygus term database */ std::unique_ptr<TermDbSygus> d_sygusTdb; /** extended model object */ diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 6cb3bf3ff..361d90dcd 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -32,13 +32,6 @@ using namespace std; namespace cvc5 { namespace theory { -/** Attribute true for nodes that have been rewritten with proofs enabled */ -struct RewriteWithProofsAttributeId -{ -}; -typedef expr::Attribute<RewriteWithProofsAttributeId, bool> - RewriteWithProofsAttribute; - // Note that this function is a simplified version of Theory::theoryOf for // (type-based) theoryOfMode. We expand and simplify it here for the sake of // efficiency. @@ -173,7 +166,6 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node, TConvProofGenerator* tcpg) { - RewriteWithProofsAttribute rpfa; #ifdef CVC5_ASSERTIONS bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean()); @@ -187,7 +179,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, // Check if it's been cached already Node cached = getPostRewriteCache(theoryId, node); - if (!cached.isNull() && (tcpg == nullptr || node.getAttribute(rpfa))) + if (!cached.isNull() && (tcpg == nullptr || hasRewrittenWithProofs(node))) { return cached; } @@ -217,7 +209,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, cached = getPreRewriteCache(rewriteStackTop.getTheoryId(), rewriteStackTop.d_node); if (cached.isNull() - || (tcpg != nullptr && !rewriteStackTop.d_node.getAttribute(rpfa))) + || (tcpg != nullptr + && !hasRewrittenWithProofs(rewriteStackTop.d_node))) { // Rewrite until fix-point is reached for(;;) { @@ -256,7 +249,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, rewriteStackTop.d_node); // If not, go through the children if (cached.isNull() - || (tcpg != nullptr && !rewriteStackTop.d_node.getAttribute(rpfa))) + || (tcpg != nullptr && !hasRewrittenWithProofs(rewriteStackTop.d_node))) { // The child we need to rewrite unsigned child = rewriteStackTop.d_nextChild++; @@ -343,7 +336,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, if (tcpg != nullptr) { // if proofs are enabled, mark that we've rewritten with proofs - rewriteStackTop.d_original.setAttribute(rpfa, true); + d_tpgNodes.insert(rewriteStackTop.d_original); if (!cached.isNull()) { // We may have gotten a different node, due to non-determinism in @@ -474,5 +467,10 @@ void Rewriter::clearCaches() clearCachesInternal(); } +bool Rewriter::hasRewrittenWithProofs(TNode n) const +{ + return d_tpgNodes.find(n) != d_tpgNodes.end(); +} + } // namespace theory } // namespace cvc5 diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index f96062b61..d90af4a31 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -159,6 +159,11 @@ class Rewriter { void clearCachesInternal(); + /** + * Has n been rewritten with proofs? This checks if n is in d_tpgNodes. + */ + bool hasRewrittenWithProofs(TNode n) const; + /** The resource manager, for tracking resource usage */ ResourceManager* d_resourceManager; @@ -167,6 +172,12 @@ class Rewriter { /** The proof generator */ std::unique_ptr<TConvProofGenerator> d_tpg; + /** + * Nodes rewritten with proofs. Since d_tpg contains a reference to all + * nodes that have been rewritten with proofs, we can keep only a TNode + * here. + */ + std::unordered_set<TNode> d_tpgNodes; #ifdef CVC5_ASSERTIONS std::unique_ptr<std::unordered_set<Node>> d_rewriteStack = nullptr; #endif /* CVC5_ASSERTIONS */ diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h index eb839e1c0..35d06a510 100644 --- a/src/theory/sets/normal_form.h +++ b/src/theory/sets/normal_form.h @@ -58,7 +58,7 @@ class NormalForm { } /** - * Returns true if n is considered a to be a (canonical) constant set value. + * Returns true if n is considered to be a (canonical) constant set value. * A canonical set value is one whose AST is: * (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n)))) * where c1 ... cn are constants and the node identifier of these constants diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index b675d2444..9396e3e87 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -17,6 +17,7 @@ #include "theory/strings/base_solver.h" #include "expr/sequence.h" +#include "options/quantifiers_options.h" #include "options/strings_options.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" @@ -539,8 +540,41 @@ void BaseSolver::checkCardinalityType(TypeNode tn, // infinite cardinality, we are fine return; } - // TODO (cvc4-projects #23): how to handle sequence for finite types? - return; + // we check the cardinality class of the type, assuming that FMF is + // disabled. + if (isCardinalityClassFinite(etn.getCardinalityClass(), false)) + { + Cardinality c = etn.getCardinality(); + bool smallCardinality = false; + if (!c.isLargeFinite()) + { + Integer ci = c.getFiniteCardinality(); + if (ci.fitsUnsignedInt()) + { + smallCardinality = true; + typeCardSize = ci.toUnsignedInt(); + } + } + if (!smallCardinality) + { + // if it is large finite, then there is no way we could have + // constructed that many terms in memory, hence there is nothing + // to do. + return; + } + } + else + { + Assert(options().quantifiers.finiteModelFind); + // we are in a case where the cardinality of the type is infinite + // if not FMF, and finite given the Env's option value for FMF. In this + // case, FMF must be true, and the cardinality is finite and dynamic + // (i.e. it depends on the model's finite interpretation for uninterpreted + // sorts). We do not know how to handle this case, we set incomplete. + // TODO (cvc4-projects #23): how to handle sequence for finite types? + d_im.setIncomplete(IncompleteId::SEQ_FINITE_DYNAMIC_CARDINALITY); + return; + } } // for each collection for (unsigned i = 0, csize = cols.size(); i < csize; ++i) diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 34597c8be..5eba8663a 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -59,6 +59,11 @@ void InferProofCons::notifyFact(const InferInfo& ii) d_lazyFactMap.insert(ii.d_conc, iic); } +void InferProofCons::notifyLemma(const InferInfo& ii) +{ + d_lazyFactMap[ii.d_conc] = std::make_shared<InferInfo>(ii); +} + bool InferProofCons::addProofTo(CDProof* pf, Node conc, InferenceId infer, diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h index 110d231cf..02b266fd7 100644 --- a/src/theory/strings/infer_proof_cons.h +++ b/src/theory/strings/infer_proof_cons.h @@ -69,6 +69,11 @@ class InferProofCons : public ProofGenerator * only for facts that are explained. */ void notifyFact(const InferInfo& ii); + /** + * Same as above, but always overwrites. This is used for lemmas and + * conflicts, which do not necessarily have unique conclusions. + */ + void notifyLemma(const InferInfo& ii); /** * This returns the proof for fact. This is required for using this class as diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 0e971fc54..1f531a97c 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -42,7 +42,8 @@ InferenceManager::InferenceManager(Env& env, d_termReg(tr), d_extt(e), d_statistics(statistics), - d_ipc(pnm ? new InferProofCons(context(), pnm, d_statistics) : nullptr) + d_ipc(pnm ? new InferProofCons(context(), pnm, d_statistics) : nullptr), + d_ipcl(pnm ? new InferProofCons(context(), pnm, d_statistics) : nullptr) { NodeManager* nm = NodeManager::currentNM(); d_zero = nm->mkConst(Rational(0)); @@ -279,12 +280,12 @@ void InferenceManager::processConflict(const InferInfo& ii) { Assert(!d_state.isInConflict()); // setup the fact to reproduce the proof in the call below - if (d_ipc != nullptr) + if (d_ipcl != nullptr) { - d_ipc->notifyFact(ii); + d_ipcl->notifyLemma(ii); } // make the trust node - TrustNode tconf = mkConflictExp(ii.d_premises, d_ipc.get()); + TrustNode tconf = mkConflictExp(ii.d_premises, d_ipcl.get()); Assert(tconf.getKind() == TrustNodeKind::CONFLICT); Trace("strings-assert") << "(assert (not " << tconf.getNode() << ")) ; conflict " << ii.getId() << std::endl; @@ -335,11 +336,11 @@ TrustNode InferenceManager::processLemma(InferInfo& ii, LemmaProperty& p) } // ensure that the proof generator is ready to explain the final conclusion // of the lemma (ii.d_conc). - if (d_ipc != nullptr) + if (d_ipcl != nullptr) { - d_ipc->notifyFact(ii); + d_ipcl->notifyLemma(ii); } - TrustNode tlem = mkLemmaExp(ii.d_conc, exp, noExplain, d_ipc.get()); + TrustNode tlem = mkLemmaExp(ii.d_conc, exp, noExplain, d_ipcl.get()); Trace("strings-pending") << "Process pending lemma : " << tlem.getNode() << std::endl; diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index 49f10d7cb..9f4cd1986 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -249,8 +249,15 @@ class InferenceManager : public InferenceManagerBuffered ExtTheory& d_extt; /** Reference to the statistics for the theory of strings/sequences. */ SequencesStatistics& d_statistics; - /** Conversion from inferences to proofs */ + /** Conversion from inferences to proofs for facts */ std::unique_ptr<InferProofCons> d_ipc; + /** + * Conversion from inferences to proofs for lemmas and conflicts. This is + * separate from the above proof generator to avoid rare cases where the + * conclusion of a lemma is a duplicate of the conclusion of another lemma, + * or is a fact in the current equality engine. + */ + std::unique_ptr<InferProofCons> d_ipcl; /** Common constants */ Node d_true; Node d_false; diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index aa95ef2f8..9faa935e1 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -56,6 +56,10 @@ enumerator STRING_TYPE \ "::cvc5::theory::strings::StringEnumerator" \ "theory/strings/type_enumerator.h" +enumerator REGEXP_TYPE \ + "::cvc5::theory::strings::RegExpEnumerator" \ + "theory/strings/regexp_enumerator.h" + constant CONST_STRING \ class \ String \ diff --git a/src/theory/strings/regexp_enumerator.cpp b/src/theory/strings/regexp_enumerator.cpp new file mode 100644 index 000000000..261d0008e --- /dev/null +++ b/src/theory/strings/regexp_enumerator.cpp @@ -0,0 +1,49 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of enumerator for regular expressions. + */ + +#include "theory/strings/regexp_enumerator.h" + +namespace cvc5 { +namespace theory { +namespace strings { + +RegExpEnumerator::RegExpEnumerator(TypeNode type, TypeEnumeratorProperties* tep) + : TypeEnumeratorBase<RegExpEnumerator>(type), d_senum(type, tep) +{ +} + +RegExpEnumerator::RegExpEnumerator(const RegExpEnumerator& enumerator) + : TypeEnumeratorBase<RegExpEnumerator>(enumerator.getType()), + d_senum(enumerator.d_senum) +{ +} + +Node RegExpEnumerator::operator*() +{ + NodeManager* nm = NodeManager::currentNM(); + return nm->mkNode(kind::STRING_TO_REGEXP, *d_senum); +} + +RegExpEnumerator& RegExpEnumerator::operator++() +{ + ++d_senum; + return *this; +} + +bool RegExpEnumerator::isFinished() { return d_senum.isFinished(); } + +} // namespace strings +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/strings/regexp_enumerator.h b/src/theory/strings/regexp_enumerator.h new file mode 100644 index 000000000..289c8b046 --- /dev/null +++ b/src/theory/strings/regexp_enumerator.h @@ -0,0 +1,59 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Enumerators for regular expressions. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__STRINGS__REGEXP_ENUMERATOR_H +#define CVC5__THEORY__STRINGS__REGEXP_ENUMERATOR_H + +#include <vector> + +#include "expr/node.h" +#include "expr/type_node.h" +#include "theory/strings/type_enumerator.h" + +namespace cvc5 { +namespace theory { +namespace strings { + +/** + * Simple regular expression enumerator, generates only singleton language + * regular expressions from a string enumeration, in other words: + * (str.to_re s1) ... (str.to_re sn) .... + * where s1 ... sn ... is the enumeration for strings. + */ +class RegExpEnumerator : public TypeEnumeratorBase<RegExpEnumerator> +{ + public: + RegExpEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr); + RegExpEnumerator(const RegExpEnumerator& enumerator); + ~RegExpEnumerator() {} + /** get the current term */ + Node operator*() override; + /** increment */ + RegExpEnumerator& operator++() override; + /** is this enumerator finished? */ + bool isFinished() override; + + private: + /** underlying string enumerator */ + StringEnumerator d_senum; +}; + +} // namespace strings +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__THEORY__STRINGS__TYPE_ENUMERATOR_H */ diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 614a5e6e0..898c0f1b7 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -546,7 +546,10 @@ bool RegExpSolver::checkPDerivative( { std::vector<Node> noExplain; noExplain.push_back(atom); - noExplain.push_back(x.eqNode(d_emptyString)); + if (x != d_emptyString) + { + noExplain.push_back(x.eqNode(d_emptyString)); + } std::vector<Node> iexp = nf_exp; iexp.insert(iexp.end(), noExplain.begin(), noExplain.end()); d_im.sendInference(iexp, noExplain, d_false, InferenceId::STRINGS_RE_DELTA_CONF); diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 33dbe9ffa..1a0549a0a 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -224,7 +224,7 @@ bool TheoryEngineModelBuilder::isExcludedCdtValue( { Trace("model-builder-debug") << " ...matches with " << eqc << " -> " << eqc_m << std::endl; - if (eqc_m.getKind() == kind::UNINTERPRETED_CONSTANT) + if (eqc_m.getKind() == kind::CODATATYPE_BOUND_VARIABLE) { Trace("model-builder-debug") << "*** " << val << " is excluded datatype for " << eqc diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index 096a47c86..fd7cd467e 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -43,13 +43,16 @@ HoExtension::HoExtension(Env& env, Node HoExtension::ppRewrite(Node node) { // convert HO_APPLY to APPLY_UF if fully applied - if (node[0].getType().getNumChildren() == 2) + if (node.getKind() == HO_APPLY) { - Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl; - Node ret = getApplyUfForHoApply(node); - Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret - << std::endl; - return ret; + if (node[0].getType().getNumChildren() == 2) + { + Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl; + Node ret = getApplyUfForHoApply(node); + Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret + << std::endl; + return ret; + } } return node; } diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index cd974d3e4..ca7dc6a73 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -212,7 +212,7 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems) Trace("uf-exp-def") << "TheoryUF::ppRewrite: expanding definition : " << node << std::endl; Kind k = node.getKind(); - if (k == kind::HO_APPLY) + if (k == kind::HO_APPLY || (node.isVar() && node.getType().isFunction())) { if (!logicInfo().isHigherOrder()) { diff --git a/src/util/smt2_quote_string.cpp b/src/util/smt2_quote_string.cpp index 82750c48b..e2ab4a74c 100644 --- a/src/util/smt2_quote_string.cpp +++ b/src/util/smt2_quote_string.cpp @@ -42,4 +42,16 @@ std::string quoteSymbol(const std::string& s){ return s; } +std::string quoteString(const std::string& s) { + // escape all double-quotes + std::string output = s; + size_t pos = 0; + while ((pos = output.find('"', pos)) != std::string::npos) + { + output.replace(pos, 1, "\"\""); + pos += 2; + } + return '"' + output + '"'; +} + } // namespace cvc5 diff --git a/src/util/smt2_quote_string.h b/src/util/smt2_quote_string.h index 98b2f89dd..f8be53c0c 100644 --- a/src/util/smt2_quote_string.h +++ b/src/util/smt2_quote_string.h @@ -27,6 +27,11 @@ namespace cvc5 { */ std::string quoteSymbol(const std::string& s); +/** + * SMT-LIB 2 quoting for strings + */ +std::string quoteString(const std::string& s); + } // namespace cvc5 #endif /* CVC5__UTIL__SMT2_QUOTE_STRING_H */ diff --git a/test/api/issue6111.cpp b/test/api/issue6111.cpp index bd7be2ad0..c0366ce23 100644 --- a/test/api/issue6111.cpp +++ b/test/api/issue6111.cpp @@ -27,7 +27,7 @@ int main() solver.setLogic("QF_BV"); Sort bvsort12979 = solver.mkBitVectorSort(12979); Term input2_1 = solver.mkConst(bvsort12979, "intpu2_1"); - Term zero = solver.mkBitVector(bvsort12979.getBVSize(), "0", 10); + Term zero = solver.mkBitVector(bvsort12979.getBitVectorSize(), "0", 10); vector<Term> args1; args1.push_back(zero); diff --git a/test/python/unit/api/test_op.py b/test/python/unit/api/test_op.py index 07a57a5c6..5126a481d 100644 --- a/test/python/unit/api/test_op.py +++ b/test/python/unit/api/test_op.py @@ -86,6 +86,9 @@ def test_get_num_indices(solver): assert 2 == floatingpoint_to_fp_generic.getNumIndices() assert 2 == regexp_loop.getNumIndices() +def test_op_indices_list(solver): + with_list = solver.mkOp(kinds.TupleProject, [4, 25]) + assert 2 == with_list.getNumIndices() def test_get_indices_string(solver): x = Op(solver) diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py index db49f8bea..6052a057f 100644 --- a/test/python/unit/api/test_solver.py +++ b/test/python/unit/api/test_solver.py @@ -381,15 +381,6 @@ def test_mk_rounding_mode(solver): solver.mkRoundingMode(pycvc5.RoundTowardZero) -def test_mk_uninterpreted_const(solver): - solver.mkUninterpretedConst(solver.getBooleanSort(), 1) - with pytest.raises(RuntimeError): - solver.mkUninterpretedConst(pycvc5.Sort(solver), 1) - slv = pycvc5.Solver() - with pytest.raises(RuntimeError): - slv.mkUninterpretedConst(solver.getBooleanSort(), 1) - - def test_mk_abstract_value(solver): solver.mkAbstractValue("1") with pytest.raises(ValueError): @@ -653,6 +644,10 @@ def test_mk_regexp_sigma(solver): solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpSigma()) +def test_mk_sep_emp(solver): + solver.mkSepEmp(); + + def test_mk_sep_nil(solver): solver.mkSepNil(solver.getBooleanSort()) with pytest.raises(RuntimeError): diff --git a/test/python/unit/api/test_sort.py b/test/python/unit/api/test_sort.py index def539cf4..98cf76d76 100644 --- a/test/python/unit/api/test_sort.py +++ b/test/python/unit/api/test_sort.py @@ -60,6 +60,11 @@ def test_operators_comparison(solver): solver.getIntegerSort() > Sort(solver) solver.getIntegerSort() >= Sort(solver) +def test_is_null(solver): + x = Sort(solver) + assert x.isNull() + x = solver.getBooleanSort() + assert not x.isNull() def test_is_boolean(solver): assert solver.getBooleanSort().isBoolean() @@ -140,6 +145,12 @@ def test_is_tester(solver): assert cons_sort.isTester() Sort(solver).isTester() +def test_is_updater(solver): + dt_sort = create_datatype_sort(solver) + dt = dt_sort.getDatatype() + updater_sort = dt[0][0].getUpdaterTerm().getSort() + assert updater_sort.isUpdater() + Sort(solver).isUpdater() def test_is_function(solver): fun_sort = solver.mkFunctionSort(solver.getRealSort(), @@ -438,26 +449,26 @@ def test_get_uninterpreted_sort_constructor_arity(solver): def test_get_bv_size(solver): bvSort = solver.mkBitVectorSort(32) - bvSort.getBVSize() + bvSort.getBitVectorSize() setSort = solver.mkSetSort(solver.getIntegerSort()) with pytest.raises(RuntimeError): - setSort.getBVSize() + setSort.getBitVectorSize() def test_get_fp_exponent_size(solver): fpSort = solver.mkFloatingPointSort(4, 8) - fpSort.getFPExponentSize() + fpSort.getFloatingPointExponentSize() setSort = solver.mkSetSort(solver.getIntegerSort()) with pytest.raises(RuntimeError): - setSort.getFPExponentSize() + setSort.getFloatingPointExponentSize() def test_get_fp_significand_size(solver): fpSort = solver.mkFloatingPointSort(4, 8) - fpSort.getFPSignificandSize() + fpSort.getFloatingPointSignificandSize() setSort = solver.mkSetSort(solver.getIntegerSort()) with pytest.raises(RuntimeError): - setSort.getFPSignificandSize() + setSort.getFloatingPointSignificandSize() def test_get_datatype_paramsorts(solver): diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8969f8b7a..3ea588e01 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -499,6 +499,7 @@ set(regress_0_tests regress0/datatypes/is_test.smt2 regress0/datatypes/issue1433.smt2 regress0/datatypes/issue2838.cvc.smt2 + regress0/datatypes/issue4393-cdt-model.smt2 regress0/datatypes/issue5280-no-nrec.smt2 regress0/datatypes/jsat-2.6.smt2 regress0/datatypes/list-bool.smt2 @@ -558,6 +559,7 @@ set(regress_0_tests regress0/distinct.smtv1.smt2 regress0/dump-unsat-core-full.smt2 regress0/echo.smt2 + regress0/eqrange0.smt2 regress0/eqrange1.smt2 regress0/eqrange2.smt2 regress0/eqrange3.smt2 @@ -766,10 +768,12 @@ set(regress_0_tests regress0/nl/very-simple-unsat.smt2 regress0/opt-abd-no-use.smt2 regress0/options/ast-and-sexpr.smt2 + regress0/options/interactive-mode.smt2 regress0/options/invalid_dump.smt2 regress0/options/set-after-init.smt2 regress0/options/set-and-get-options.smt2 regress0/options/statistics.smt2 + regress0/options/stream-printing.smt2 regress0/parallel-let.smt2 regress0/parser/as.smt2 regress0/parser/bv_arity_smt2.6.smt2 @@ -780,6 +784,7 @@ set(regress_0_tests regress0/parser/force_logic_set_logic.smt2 regress0/parser/force_logic_success.smt2 regress0/parser/issue5163.smt2 + regress0/parser/issue6908-get-value-uc.smt2 regress0/parser/issue7274.smt2 regress0/parser/linear_arithmetic_err1.smt2 regress0/parser/linear_arithmetic_err2.smt2 @@ -876,6 +881,7 @@ set(regress_0_tests regress0/push-pop/incremental-subst-bug.cvc.smt2 regress0/push-pop/issue1986.smt2 regress0/push-pop/issue2137.min.smt2 + regress0/push-pop/issue6535-inc-solve.smt2 regress0/push-pop/quant-fun-proc-unfd.smt2 regress0/push-pop/real-as-int-incremental.smt2 regress0/push-pop/simple_unsat_cores.smt2 @@ -918,10 +924,12 @@ set(regress_0_tests regress0/quantifiers/issue4576.smt2 regress0/quantifiers/issue5645-dt-cm-spurious.smt2 regress0/quantifiers/issue5693-prenex.smt2 + regress0/quantifiers/issue6475-rr-const.smt2 regress0/quantifiers/issue6603-dt-bool-cegqi.smt2 regress0/quantifiers/issue6838-qpdt.smt2 regress0/quantifiers/issue6996-trivial-elim.smt2 regress0/quantifiers/issue6999-deq-elim.smt2 + regress0/quantifiers/issue7353-var-elim-par-dt.smt2 regress0/quantifiers/lra-triv-gn.smt2 regress0/quantifiers/macro-back-subs-sat.smt2 regress0/quantifiers/macros-int-real.smt2 @@ -965,6 +973,7 @@ set(regress_0_tests regress0/quantifiers/simp-len.smt2 regress0/quantifiers/simp-typ-test.smt2 regress0/quantifiers/ufnia-fv-delta.smt2 + regress0/quantifiers/veqt-delta.smt2 regress0/rec-fun-const-parse-bug.smt2 regress0/rels/addr_book_0.cvc.smt2 regress0/rels/atom_univ2.cvc.smt2 @@ -1500,6 +1509,8 @@ set(regress_1_tests regress1/arith/issue3952-rew-eq.smt2 regress1/arith/issue4985-model-success.smt2 regress1/arith/issue4985b-model-success.smt2 + regress1/arith/issue6774-sanity-int-model.smt2 + regress1/arith/issue7252-arith-sanity.smt2 regress1/arith/issue789.smt2 regress1/arith/miplib3.cvc.smt2 regress1/arith/mod.02.smt2 @@ -1571,6 +1582,7 @@ set(regress_1_tests regress1/constarr3.cvc.smt2 regress1/constarr3.smt2 regress1/cores/issue5604.smt2 + regress1/cores/issue6988-arith-sanity.smt2 regress1/datatypes/acyclicity-sr-ground096.smt2 regress1/datatypes/cee-prs-small-dd2.smt2 regress1/datatypes/dt-color-2.6.smt2 @@ -1639,8 +1651,11 @@ set(regress_1_tests regress1/fmf/issue4225-univ-fun.smt2 regress1/fmf/issue5738-dt-interp-finite.smt2 regress1/fmf/issue6690-re-enum.smt2 + regress1/fmf/issue6744-2-unc-bool-var.smt2 + regress1/fmf/issue6744-3-unc-bool-var.smt2 regress1/fmf/issue916-fmf-or.smt2 regress1/fmf/jasmin-cdt-crash.smt2 + regress1/fmf/ko-bound-set.cvc.smt2 regress1/fmf/loopy_coda.smt2 regress1/fmf/lst-no-self-rev-exp.smt2 regress1/fmf/memory_model-R_cpp-dd.cvc.smt2 @@ -1662,6 +1677,7 @@ set(regress_1_tests regress1/ho/issue4065-no-rep.smt2 regress1/ho/issue4092-sinf.smt2 regress1/ho/issue4134-sinf.smt2 + regress1/ho/issue5741-3.smt2 regress1/ho/NUM638^1.smt2 regress1/ho/NUM925^1.p regress1/ho/soundness_fmf_SYO362^5-delta.p @@ -1680,6 +1696,7 @@ set(regress_1_tests regress1/model-blocker-simple.smt2 regress1/model-blocker-values.smt2 regress1/nl/approx-sqrt.smt2 + regress1/nl/approx-sqrt-unsat.smt2 regress1/nl/arctan2-expdef.smt2 regress1/nl/arrowsmith-050317.smt2 regress1/nl/bad-050217.smt2 @@ -1708,8 +1725,10 @@ set(regress_1_tests regress1/nl/issue3656.smt2 regress1/nl/issue3803-nl-check-model.smt2 regress1/nl/issue3955-ee-double-notify.smt2 + regress1/nl/issue3966-conf-coeff.smt2 regress1/nl/issue4791-llr.smt2 regress1/nl/issue5372-2-no-m-presolve.smt2 + regress1/nl/issue5660-mb-success.smt2 regress1/nl/issue5662-nl-tc.smt2 regress1/nl/issue5662-nl-tc-min.smt2 regress1/nl/metitarski-1025.smt2 @@ -1753,6 +1772,7 @@ set(regress_1_tests regress1/proofs/issue6625-unsat-core-proofs.smt2 regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2 regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2 + regress1/proofs/qgu-fuzz-1-strings-pp.smt2 regress1/proofs/quant-alpha-eq.smt2 regress1/proofs/sat-trivial-cycle.smt2 regress1/proofs/unsat-cores-proofs.smt2 @@ -1843,6 +1863,7 @@ set(regress_1_tests regress1/quantifiers/cee-npnt-dd.smt2 regress1/quantifiers/cee-os-delta.smt2 regress1/quantifiers/cdt-0208-to.smt2 + regress1/quantifiers/choice-move-delta-relt.smt2 regress1/quantifiers/const.cvc.smt2 regress1/quantifiers/constfunc.cvc.smt2 regress1/quantifiers/ddatv-delta2.smt2 @@ -1888,6 +1909,7 @@ set(regress_1_tests regress1/quantifiers/issue4849-nqe.smt2 regress1/quantifiers/issue5019-cegqi-i.smt2 regress1/quantifiers/issue5279-nqe.smt2 + regress1/quantifiers/issue5288-vts-real-int.smt2 regress1/quantifiers/issue5365-nqe.smt2 regress1/quantifiers/issue5378-witness.smt2 regress1/quantifiers/issue5469-aext.smt2 @@ -1899,9 +1921,16 @@ set(regress_1_tests regress1/quantifiers/issue5506-qe.smt2 regress1/quantifiers/issue5507-qe.smt2 regress1/quantifiers/issue5658-qe.smt2 + regress1/quantifiers/issue5735-subtypes.smt2 + regress1/quantifiers/issue5735-2-subtypes.smt2 regress1/quantifiers/issue5766-wrong-sel-trigger.smt2 regress1/quantifiers/issue5899-qe.smt2 + regress1/quantifiers/issue6607-witness-te.smt2 + regress1/quantifiers/issue6638-sygus-inst.smt2 + regress1/quantifiers/issue6642-em-types.smt2 regress1/quantifiers/issue6699-nc-shadow.smt2 + regress1/quantifiers/issue6775-vts-int.smt2 + regress1/quantifiers/issue6845-nl-lemma-tc.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lia-witness-div-pp.smt2 @@ -1947,10 +1976,12 @@ set(regress_1_tests regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 regress1/quantifiers/qs-has-term.smt2 regress1/quantifiers/recfact.cvc.smt2 + regress1/quantifiers/rel-trigger-unusable.smt2 regress1/quantifiers/repair-const-nterm.smt2 regress1/quantifiers/rew-to-0211-dd.smt2 regress1/quantifiers/ricart-agrawala6.smt2 regress1/quantifiers/set-choice-koikonomou.cvc.smt2 + regress1/quantifiers/set3.smt2 regress1/quantifiers/set8.smt2 regress1/quantifiers/seu169+1.smt2 regress1/quantifiers/seq-solved-enum.smt2 @@ -1961,6 +1992,7 @@ set(regress_1_tests regress1/quantifiers/smtlib46f14a.smt2 regress1/quantifiers/smtlibe99bbe.smt2 regress1/quantifiers/smtlibf957ea.smt2 + regress1/quantifiers/stream-x2014-09-18-unsat.smt2 regress1/quantifiers/sygus-infer-nested.smt2 regress1/quantifiers/sygus-inst-nia-psyco-060.smt2 regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2 @@ -2179,6 +2211,7 @@ set(regress_1_tests regress1/strings/issue6101-2.smt2 regress1/strings/issue6132-non-unique-skolem.smt2 regress1/strings/issue6142-repl-inv-rew.smt2 + regress1/strings/issue6184-unsat-core.smt2 regress1/strings/issue6191-replace-all.smt2 regress1/strings/issue6203-1-substr-ctn-strip.smt2 regress1/strings/issue6203-2-re-ccache.smt2 @@ -2195,11 +2228,13 @@ set(regress_1_tests regress1/strings/issue6604-2.smt2 regress1/strings/issue6635-rre.smt2 regress1/strings/issue6653-2-update-c-len.smt2 + regress1/strings/issue6653-3-seq.smt2 regress1/strings/issue6653-4-rre.smt2 regress1/strings/issue6653-rre.smt2 regress1/strings/issue6653-rre-small.smt2 regress1/strings/issue6777-seq-nth-eval-cm.smt2 regress1/strings/issue6913.smt2 + regress1/strings/issue6973-dup-lemma-conc.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 @@ -2251,6 +2286,7 @@ set(regress_1_tests regress1/strings/rev-ex5.smt2 regress1/strings/rew-020618.smt2 regress1/strings/rew-check1.smt2 + regress1/strings/seq-cardinality.smt2 regress1/strings/seq-quant-infinite-branch.smt2 regress1/strings/simple-re-consume.smt2 regress1/strings/stoi-400million.smt2 @@ -2290,6 +2326,7 @@ set(regress_1_tests regress1/sygus/abv.sy regress1/sygus/array-grammar-store.sy regress1/sygus/array_search_5-Q-easy.sy + regress1/sygus/array-uc.sy regress1/sygus/bvudiv-by-2.sy regress1/sygus/cegar1.sy regress1/sygus/cegis-unif-inv-eq-fair.sy @@ -2524,6 +2561,7 @@ set(regress_2_tests regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2 regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 regress2/quantifiers/cee-event-wrong-sat.smt2 + regress2/quantifiers/exp-trivially-dd3.smt2 regress2/quantifiers/gn-wrong-091018.smt2 regress2/quantifiers/issue3481-unsat1.smt2 regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 @@ -2702,16 +2740,12 @@ set(regression_disabled_tests ### regress1/bug472.smt2 regress1/datatypes/non-simple-rec-set.smt2 - # TODO: fix models (projects #276) - regress1/fmf/ko-bound-set.cvc.smt2 # results in an assertion failure (see issue #1650). regress1/ho/hoa0102.smt2 # after disallowing solving for terms with quantifiers regress1/ho/nested_lambdas-AGT034^2.smt2 regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 regress1/ho/SYO056^1.p - # slow on some builds after changes to tangent planes - regress1/nl/approx-sqrt-unsat.smt2 # times out after update to circuit propagator regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 # times out after update to tangent planes @@ -2728,12 +2762,6 @@ set(regression_disabled_tests regress1/quantifiers/macro-subtype-param.smt2 # times out with competition build, ok with other builds: regress1/quantifiers/model_6_1_bv.smt2 - # timeout after changes to nonlinear on PR #5351 - regress1/quantifiers/rel-trigger-unusable.smt2 - # does not terminate/takes a long time when doing a coverage build with LFSC. - regress1/quantifiers/set3.smt2 - # changes to expand definitions, related to trigger selection for selectors - regress1/quantifiers/stream-x2014-09-18-unsat.smt2 # ajreynol: different error messages on production and debug: regress1/quantifiers/subtype-param-unk.smt2 regress1/quantifiers/subtype-param.smt2 @@ -2770,7 +2798,6 @@ set(regression_disabled_tests # previously sygus inference did not apply, now (correctly) times out regress1/sygus/issue3498.smt2 regress2/arith/miplib-opt1217--27.smt2 - regress2/quantifiers/exp-trivially-dd3.smt2 regress2/nl/dumortier-050317.smt2 # timeout on some builds after changes to justification heuristic regress2/nl/nt-lemmas-bad.smt2 diff --git a/test/regress/regress0/datatypes/issue4393-cdt-model.smt2 b/test/regress/regress0/datatypes/issue4393-cdt-model.smt2 new file mode 100644 index 000000000..950cb61a9 --- /dev/null +++ b/test/regress/regress0/datatypes/issue4393-cdt-model.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_DTLIA) +(set-info :status sat) +(declare-codatatypes ((a 0)) (((b (c Int) (d a))))) +(declare-fun e () a) +(declare-fun f () a) +(assert (distinct f (b 0 f))) +(assert (= e f)) +(check-sat) diff --git a/test/regress/regress0/eqrange0.smt2 b/test/regress/regress0/eqrange0.smt2 new file mode 100644 index 000000000..01713d18f --- /dev/null +++ b/test/regress/regress0/eqrange0.smt2 @@ -0,0 +1,6 @@ +; EXPECT: (error "Term of kind EQ_RANGE not supported in default mode, try --arrays-exp") +; EXIT: 1 +(set-logic QF_AUFLIA) +(declare-const a (Array Int Int)) +(assert (eqrange a a 0 0)) +(check-sat) diff --git a/test/regress/regress0/options/interactive-mode.smt2 b/test/regress/regress0/options/interactive-mode.smt2 new file mode 100644 index 000000000..549fdfd24 --- /dev/null +++ b/test/regress/regress0/options/interactive-mode.smt2 @@ -0,0 +1,10 @@ +; EXPECT: true +; EXPECT: true +; EXPECT: false +; EXPECT: false +(set-option :interactive-mode true) +(get-option :interactive-mode) +(get-option :produce-assertions) +(set-option :produce-assertions false) +(get-option :interactive-mode) +(get-option :produce-assertions)
\ No newline at end of file diff --git a/test/regress/regress0/options/stream-printing.smt2 b/test/regress/regress0/options/stream-printing.smt2 new file mode 100644 index 000000000..21ea85aa1 --- /dev/null +++ b/test/regress/regress0/options/stream-printing.smt2 @@ -0,0 +1,18 @@ +; EXPECT: stdout +; EXPECT: stderr +; EXPECT: stdin +; EXPECT-ERROR: stderr +; EXPECT-ERROR: stdout +; EXPECT-ERROR: stdin + +(get-option :regular-output-channel) +(get-option :diagnostic-output-channel) +(get-option :in) + +(set-option :regular-output-channel stderr) +(set-option :diagnostic-output-channel stdout) +(set-option :in stdin) + +(get-option :regular-output-channel) +(get-option :diagnostic-output-channel) +(get-option :in) diff --git a/test/regress/regress0/parser/issue6908-get-value-uc.smt2 b/test/regress/regress0/parser/issue6908-get-value-uc.smt2 new file mode 100644 index 000000000..b6825fe27 --- /dev/null +++ b/test/regress/regress0/parser/issue6908-get-value-uc.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --produce-models +; EXPECT: sat +; EXPECT: (((f (as @uc_Foo_0 Foo)) 3)) +(set-logic ALL) +(set-option :produce-models true) +(declare-sort Foo 0) +(declare-fun f (Foo) Int) +(assert (exists ((x Foo)) (= (f x) 3))) +(check-sat) +(get-value ((f @uc_Foo_0))) diff --git a/test/regress/regress0/push-pop/issue6535-inc-solve.smt2 b/test/regress/regress0/push-pop/issue6535-inc-solve.smt2 new file mode 100644 index 000000000..c4a9a770f --- /dev/null +++ b/test/regress/regress0/push-pop/issue6535-inc-solve.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: -i +; EXPECT: sat +(set-logic ALL) +(declare-fun f0_2 (Real Real) Real) +(declare-fun x8 () Real) +(assert (= 0.0 (f0_2 x8 1.0))) +(push) +(assert (= x8 1.0)) +(check-sat) diff --git a/test/regress/regress0/quantifiers/issue6475-rr-const.smt2 b/test/regress/regress0/quantifiers/issue6475-rr-const.smt2 new file mode 100644 index 000000000..11cc56547 --- /dev/null +++ b/test/regress/regress0/quantifiers/issue6475-rr-const.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :macros-quant true) +(declare-sort I_fb 0) +(declare-fun fb_arg_0_1 (I_fb) Int) +(declare-fun name!0 (I_fb) Int) +(assert (forall ((?j I_fb)) (! (= (name!0 ?j) (fb_arg_0_1 ?j)) :qid k!9))) +(check-sat) diff --git a/test/regress/regress0/quantifiers/issue7353-var-elim-par-dt.smt2 b/test/regress/regress0/quantifiers/issue7353-var-elim-par-dt.smt2 new file mode 100644 index 000000000..8c9d9eb66 --- /dev/null +++ b/test/regress/regress0/quantifiers/issue7353-var-elim-par-dt.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL) +(set-info :status sat) +(declare-datatype Option (par (T) ((none) (some (extractSome T))))) +(assert + (forall ((x (Option Int))) + (=> (and ((_ is some) x) + (= (extractSome x) 0)) + (= x (some 0))))) +(check-sat) diff --git a/test/regress/regress0/quantifiers/veqt-delta.smt2 b/test/regress/regress0/quantifiers/veqt-delta.smt2 new file mode 100644 index 000000000..dfac015c6 --- /dev/null +++ b/test/regress/regress0/quantifiers/veqt-delta.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --relational-triggers +; EXPECT: unsat +(set-logic ALL) +(declare-sort S 0) +(declare-fun f () S) +(assert (forall ((? S)) (= ? f))) +(assert (exists ((? S) (v S)) (distinct ? v))) +(check-sat) diff --git a/test/regress/regress1/arith/issue6774-sanity-int-model.smt2 b/test/regress/regress1/arith/issue6774-sanity-int-model.smt2 new file mode 100644 index 000000000..732b709f9 --- /dev/null +++ b/test/regress/regress1/arith/issue6774-sanity-int-model.smt2 @@ -0,0 +1,21 @@ +; COMMAND-LINE: -i -q +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +(set-logic ALIRA) +(declare-const x Real) +(declare-fun i () Int) +(declare-fun i1 () Int) +(push) +(assert (< 1 (- i))) +(check-sat) +(pop) +(push) +(assert (or (>= i1 (* 5 (- i))))) +(check-sat) +(pop) +(assert (or (> i1 1) (= x (to_real i)))) +(check-sat) +(assert (not (is_int x))) +(check-sat) diff --git a/test/regress/regress1/arith/issue7252-arith-sanity.smt2 b/test/regress/regress1/arith/issue7252-arith-sanity.smt2 new file mode 100644 index 000000000..dd7a1fa2e --- /dev/null +++ b/test/regress/regress1/arith/issue7252-arith-sanity.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(declare-fun d () Int) +(declare-fun e () Int) +(declare-fun f () Int) +(declare-fun g () Int) +(assert (> 0 (* a (mod 0 b)))) +(assert (or (and (> (* b d) (* 2 (+ g c))) (= g (- c)) (> (+ e c) 0)) (> f 0))) +(check-sat) diff --git a/test/regress/regress1/cores/issue6988-arith-sanity.smt2 b/test/regress/regress1/cores/issue6988-arith-sanity.smt2 new file mode 100644 index 000000000..622d64375 --- /dev/null +++ b/test/regress/regress1/cores/issue6988-arith-sanity.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: -i -q +; EXPECT: sat +; EXPECT: sat +(set-logic ANIA) +(declare-const x Bool) +(set-option :produce-unsat-cores true) +(declare-fun i () Int) +(declare-fun i5 () Int) +(declare-fun i8 () Int) +(assert (or x (< i5 0))) +(push) +(assert (and (= i8 1) (= i5 (+ 1 i)) (= i8 (+ 1 i)))) +(push) +(check-sat) +(pop) +(pop) +(assert (= i8 (* i8 3 (+ i8 1)))) +(check-sat) diff --git a/test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2 b/test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2 new file mode 100644 index 000000000..024d5b6a3 --- /dev/null +++ b/test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(set-option :finite-model-find true) +(set-info :status sat) +(declare-fun v () Bool) +(declare-fun v2 () Bool) +(assert (exists ((q (Array Bool (Array Bool (Array Int Bool))))) (forall ((q3 (Array Bool (Array Bool (Array Int Bool))))) (xor v2 v2 v v2 (or v2 (not (= q3 q))))))) +(check-sat) diff --git a/test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2 b/test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2 new file mode 100644 index 000000000..eb0c35f68 --- /dev/null +++ b/test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2 @@ -0,0 +1,5 @@ +(set-logic UFC) +(set-info :status sat) +(declare-fun v () Bool) +(assert (and (forall ((q Bool)) (not (xor v (exists ((q Bool)) true) (and (not v) (not q))))))) +(check-sat) diff --git a/test/regress/regress1/ho/issue5741-3.smt2 b/test/regress/regress1/ho/issue5741-3.smt2 new file mode 100644 index 000000000..abc4b76a6 --- /dev/null +++ b/test/regress/regress1/ho/issue5741-3.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/regress1/nl/issue3966-conf-coeff.smt2 b/test/regress/regress1/nl/issue3966-conf-coeff.smt2 new file mode 100644 index 000000000..7bfbf4140 --- /dev/null +++ b/test/regress/regress1/nl/issue3966-conf-coeff.smt2 @@ -0,0 +1,22 @@ +(set-logic QF_UFNIA) +(set-info :status sat) +(set-option :nl-ext-ent-conf true) +(declare-const v0 Bool) +(declare-const v1 Bool) +(declare-const v2 Bool) +(declare-const v3 Bool) +(declare-const i0 Int) +(declare-const i1 Int) +(declare-const i2 Int) +(declare-const i4 Int) +(declare-const i5 Int) +(declare-const i9 Int) +(declare-const i10 Int) +(declare-const i12 Int) +(declare-const i13 Int) +(assert v0) +(declare-sort S0 0) +(declare-const v4 Bool) +(assert (xor v2 v1 (> i12 i2) (and v3 v3) (> i12 i2) v4 v2 v1 v0 v3)) +(assert (xor (<= 52 (div 15 (- i1 84 i0 99 i5))) v4 (=> v4 (>= i5 88)) (> i12 i2) (and v3 v3) (<= 52 (div 15 (- i1 84 i0 99 i5))) v1 (> i12 i2) (distinct i0 615) v0)) +(check-sat) diff --git a/test/regress/regress1/nl/issue5660-mb-success.smt2 b/test/regress/regress1/nl/issue5660-mb-success.smt2 new file mode 100644 index 000000000..6284b0580 --- /dev/null +++ b/test/regress/regress1/nl/issue5660-mb-success.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_AUFNRA) +(set-info :status sat) +(declare-fun r2 () Real) +(declare-fun r9 () Real) +(declare-fun r13 () Real) +(declare-fun ufrb5 (Real Real Real Real Real) Bool) +(declare-fun v3 () Bool) +(declare-fun v4 () Bool) +(declare-fun arr0 () (Array Bool Real)) +(declare-fun arr1 () (Array Bool (Array Bool Real))) +(declare-fun v5 () Bool) +(declare-fun v7 () Bool) +(declare-fun v8 () Bool) +(declare-fun v71 () Bool) +(declare-fun v81 () Bool) +(declare-fun v161 () Bool) +(assert (or v161 (and v3 (not v7)))) +(assert (or v8 (distinct v7 (and v7 v81) (ufrb5 0.0 1.0 0.0 1.0 (/ r13 r9))))) +(assert (or v161 (distinct v71 v8 (= v4 v81)))) +(assert (or v81 (= arr0 (store (select (store arr1 (xor v81 (and (= r2 1.0) (= r13 1))) arr0) v7) v81 (select (store arr0 v5 1.0) false))))) +(check-sat) diff --git a/test/regress/regress1/proofs/qgu-fuzz-1-strings-pp.smt2 b/test/regress/regress1/proofs/qgu-fuzz-1-strings-pp.smt2 new file mode 100644 index 000000000..c0c1f16f7 --- /dev/null +++ b/test/regress/regress1/proofs/qgu-fuzz-1-strings-pp.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun x () String) +(assert (let ((_let_1 (str.to_re "B"))) (and (str.in_re x (re.++ re.allchar (str.to_re (str.++ "B" "A")))) (str.in_re x (re.* (re.union re.allchar (str.to_re "A")))) (str.in_re x (re.* (re.union re.allchar _let_1))) (str.in_re x (re.* (re.++ re.allchar _let_1)))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/choice-move-delta-relt.smt2 b/test/regress/regress1/quantifiers/choice-move-delta-relt.smt2 new file mode 100644 index 000000000..a8fd0d498 --- /dev/null +++ b/test/regress/regress1/quantifiers/choice-move-delta-relt.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --relational-triggers --user-pat=use +; EXPECT: unsat +(set-logic ALL) +(declare-fun F (Int) Bool) +(assert (forall ((v Int)) (! (= (F 0) (< v 0)) :qid |outputbpl.194:24| :pattern ((F 0))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue5288-vts-real-int.smt2 b/test/regress/regress1/quantifiers/issue5288-vts-real-int.smt2 new file mode 100644 index 000000000..b36b8cc94 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5288-vts-real-int.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(assert + (forall ((a Int) (b Int)) + (or (< a (/ 3 b (- 2))) + (forall ((c Int)) (or (<= c b) (>= c a)))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue5735-2-subtypes.smt2 b/test/regress/regress1/quantifiers/issue5735-2-subtypes.smt2 new file mode 100644 index 000000000..76a58bdb7 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5735-2-subtypes.smt2 @@ -0,0 +1,4 @@ +(set-logic ALL) +(set-info :status unsat) +(assert (forall ((a Real)) (exists ((b Int)) (= (exists ((c Int)) (<= a c (+ a 1))) (and (>= b (/ a (+ a 1))) (< 1 (+ a 1))))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue5735-subtypes.smt2 b/test/regress/regress1/quantifiers/issue5735-subtypes.smt2 new file mode 100644 index 000000000..300819007 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5735-subtypes.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun a () Bool) +(assert (forall ((b Int) (c Bool) (d Int)) +(or (= d (/ 1 (ite c 9 0))) (<= (ite a 1 b) (/ 1 (ite c 9 0)))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue6607-witness-te.smt2 b/test/regress/regress1/quantifiers/issue6607-witness-te.smt2 new file mode 100644 index 000000000..ff426c139 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue6607-witness-te.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --no-check-models +(set-logic ALL) +(set-info :status sat) +(assert (exists ((skoY Real)) (forall ((skoX Real)) (or (= 0.0 (* skoY skoY)) (and (< skoY 0.0) (or (= skoY skoX) (= 2 (* skoY skoY)))))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue6638-sygus-inst.smt2 b/test/regress/regress1/quantifiers/issue6638-sygus-inst.smt2 new file mode 100644 index 000000000..b7cc50885 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue6638-sygus-inst.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --sygus-inst --no-check-models +; EXPECT: sat +(set-logic ALL) +(declare-fun b (Int) Int) +(assert (distinct 0 (ite (exists ((t Int)) (and (forall ((tt Int) (t Int)) (! (or (distinct 0 tt) (> 0 (+ tt t)) (> (+ tt t) 0) (= (b 0) (b t))) :qid k!7)))) 1 (b 0)))) +(check-sat) + +; check-models disabled due to intermediate terms from sygus-inst diff --git a/test/regress/regress1/quantifiers/issue6642-em-types.smt2 b/test/regress/regress1/quantifiers/issue6642-em-types.smt2 new file mode 100644 index 000000000..19dc11227 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue6642-em-types.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --full-saturate-quant +; EXPECT: unsat +(set-logic ALL) +(declare-fun b () String) +(assert (forall ((c (Seq Int))) (exists ((a String)) (and (= 1 (seq.len c)) (not (= b a)))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue6775-vts-int.smt2 b/test/regress/regress1/quantifiers/issue6775-vts-int.smt2 new file mode 100644 index 000000000..39b92a6ad --- /dev/null +++ b/test/regress/regress1/quantifiers/issue6775-vts-int.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: -i --no-check-models +; EXPECT: sat +; EXPECT: sat +(set-logic NIA) +(declare-const x43799 Bool) +(declare-const x32 Bool) +(declare-fun v11 () Bool) +(declare-fun i2 () Int) +(declare-fun i3 () Int) +(declare-fun i () Int) +(assert (or (< 0 i2) (not x32) (not v11))) +(assert (or x32 (exists ((q Int)) (not (= x32 (> q (abs i3))))))) +(assert (< i2 i)) +(check-sat) +(assert (or (not v11) x43799)) +(assert (= (+ 3 i (* 13 4 5 (abs i3))) (* 157 4 (- 1) (+ 1 1 i2 i)))) +(check-sat) + +; check-models disabled due to intermediate terms from sygus-inst diff --git a/test/regress/regress1/quantifiers/issue6845-nl-lemma-tc.smt2 b/test/regress/regress1/quantifiers/issue6845-nl-lemma-tc.smt2 new file mode 100644 index 000000000..087137653 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue6845-nl-lemma-tc.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: -i +; EXPECT: sat +; EXPECT: sat +(set-logic NIRA) +(declare-const x Bool) +(declare-fun i () Int) +(declare-fun i1 () Int) +(assert (< 1.0 (to_real i))) +(assert (distinct 0 (/ 7 (to_real i)))) +(push) +(assert (or (exists ((q Int)) (= 0 (* i i1))))) +(check-sat) +(pop) +(assert (or (= i1 1) x)) +(check-sat) diff --git a/test/regress/regress1/strings/issue6184-unsat-core.smt2 b/test/regress/regress1/strings/issue6184-unsat-core.smt2 new file mode 100644 index 000000000..6673dc3b9 --- /dev/null +++ b/test/regress/regress1/strings/issue6184-unsat-core.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(set-option :check-unsat-cores true) +(declare-fun i8 () Int) +(declare-fun st6 () (Set String)) +(declare-fun st8 () (Set String)) +(declare-fun str6 () String) +(declare-fun str7 () String) +(assert (= 0 (card st8))) +(assert (str.in_re str6 (re.opt re.none))) +(assert (str.in_re (str.substr str7 0 i8) re.allchar)) +(assert (xor true (subset st8 st6) (not (= str7 str6)) true)) +(check-sat) diff --git a/test/regress/regress1/strings/issue6653-3-seq.smt2 b/test/regress/regress1/strings/issue6653-3-seq.smt2 new file mode 100644 index 000000000..a48fc7664 --- /dev/null +++ b/test/regress/regress1/strings/issue6653-3-seq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic QF_SLIA) +(set-info :status sat) +(set-option :strings-lazy-pp false) +(declare-fun z () Int) +(declare-fun a () (Seq Int)) +(assert (not (= (seq.nth a 1) (seq.nth a z)))) +(assert (= z (- 1))) +(check-sat) diff --git a/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 b/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 new file mode 100644 index 000000000..4c6fe5c62 --- /dev/null +++ b/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 @@ -0,0 +1,15 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun a () String) +(assert + (str.in_re "" + (re.++ (re.diff (re.comp re.all) (re.++ (str.to_re a) (re.comp re.all))) + (str.to_re + (ite + (str.in_re "" + (re.++ (str.to_re (ite (str.in_re "" (re.++ (str.to_re a) (re.comp re.all))) a "")) + (re.inter (str.to_re a) + (re.++ (str.to_re a) + (re.comp (re.union (re.++ (str.to_re a) (re.comp re.all)) re.all)))))) + a ""))))) +(check-sat) diff --git a/test/regress/regress1/strings/seq-cardinality.smt2 b/test/regress/regress1/strings/seq-cardinality.smt2 new file mode 100644 index 000000000..93a4985d4 --- /dev/null +++ b/test/regress/regress1/strings/seq-cardinality.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun x () (Seq (_ BitVec 1))) +(declare-fun y () (Seq (_ BitVec 1))) +(declare-fun z () (Seq (_ BitVec 1))) + +(assert (= (seq.len x) 1)) +(assert (= (seq.len y) 1)) +(assert (= (seq.len z) 1)) +(assert (distinct x y z)) +(check-sat) diff --git a/test/regress/regress1/sygus/array-uc.sy b/test/regress/regress1/sygus/array-uc.sy new file mode 100644 index 000000000..b3d950436 --- /dev/null +++ b/test/regress/regress1/sygus/array-uc.sy @@ -0,0 +1,14 @@ +; COMMAND-LINE: --sygus-out=status +; EXPECT: unsat +(set-logic ALL) +(declare-sort U 0) +(synth-fun f ((x (Array U Int)) (y U)) Bool) + +(declare-var x (Array U Int)) +(declare-var y U) + +(constraint (= (f (store x y 0) y) true)) +(constraint (= (f (store x y 1) y) false)) + +; f can be (= (select x y) 0) +(check-synth) diff --git a/test/unit/api/java/cvc5/SolverTest.java b/test/unit/api/java/cvc5/SolverTest.java index d153b8a91..6f9d8206d 100644 --- a/test/unit/api/java/cvc5/SolverTest.java +++ b/test/unit/api/java/cvc5/SolverTest.java @@ -623,6 +623,11 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma())); } + @Test void mkSepEmp() + { + assertDoesNotThrow(() -> d_solver.mkSepEmp()); + } + @Test void mkSepNil() { assertDoesNotThrow(() -> d_solver.mkSepNil(d_solver.getBooleanSort())); @@ -2342,4 +2347,4 @@ class SolverTest + "\"Z\")))", projection.toString()); } -}
\ No newline at end of file +} diff --git a/test/unit/api/java/cvc5/SortTest.java b/test/unit/api/java/cvc5/SortTest.java index f2f9edaed..1ea703268 100644 --- a/test/unit/api/java/cvc5/SortTest.java +++ b/test/unit/api/java/cvc5/SortTest.java @@ -458,28 +458,28 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getSortConstructorArity()); } - @Test void getBVSize() throws CVC5ApiException + @Test void getBitVectorSize() throws CVC5ApiException { Sort bvSort = d_solver.mkBitVectorSort(32); - assertDoesNotThrow(() -> bvSort.getBVSize()); + assertDoesNotThrow(() -> bvSort.getBitVectorSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - assertThrows(CVC5ApiException.class, () -> setSort.getBVSize()); + assertThrows(CVC5ApiException.class, () -> setSort.getBitVectorSize()); } - @Test void getFPExponentSize() throws CVC5ApiException + @Test void getFloatingPointExponentSize() throws CVC5ApiException { Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - assertDoesNotThrow(() -> fpSort.getFPExponentSize()); + assertDoesNotThrow(() -> fpSort.getFloatingPointExponentSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - assertThrows(CVC5ApiException.class, () -> setSort.getFPExponentSize()); + assertThrows(CVC5ApiException.class, () -> setSort.getFloatingPointExponentSize()); } - @Test void getFPSignificandSize() throws CVC5ApiException + @Test void getFloatingPointSignificandSize() throws CVC5ApiException { Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - assertDoesNotThrow(() -> fpSort.getFPSignificandSize()); + assertDoesNotThrow(() -> fpSort.getFloatingPointSignificandSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - assertThrows(CVC5ApiException.class, () -> setSort.getFPSignificandSize()); + assertThrows(CVC5ApiException.class, () -> setSort.getFloatingPointSignificandSize()); } @Test void getDatatypeParamSorts() throws CVC5ApiException diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 19113ae13..c9527c2d4 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -376,15 +376,6 @@ TEST_F(TestApiBlackSolver, mkRoundingMode) ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); } -TEST_F(TestApiBlackSolver, mkUninterpretedConst) -{ - ASSERT_NO_THROW(d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1)); - ASSERT_THROW(d_solver.mkUninterpretedConst(Sort(), 1), CVC5ApiException); - Solver slv; - ASSERT_THROW(slv.mkUninterpretedConst(d_solver.getBooleanSort(), 1), - CVC5ApiException); -} - TEST_F(TestApiBlackSolver, mkAbstractValue) { ASSERT_NO_THROW(d_solver.mkAbstractValue(std::string("1"))); @@ -606,6 +597,8 @@ TEST_F(TestApiBlackSolver, mkRegexpSigma) d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma())); } +TEST_F(TestApiBlackSolver, mkSepEmp) { ASSERT_NO_THROW(d_solver.mkSepEmp()); } + TEST_F(TestApiBlackSolver, mkSepNil) { ASSERT_NO_THROW(d_solver.mkSepNil(d_solver.getBooleanSort())); @@ -1234,6 +1227,23 @@ TEST_F(TestApiBlackSolver, getAbduct) ASSERT_EQ(output2, truen); } +TEST_F(TestApiBlackSolver, getAbduct2) +{ + d_solver.setLogic("QF_LIA"); + d_solver.setOption("incremental", "false"); + Sort intSort = d_solver.getIntegerSort(); + Term zero = d_solver.mkInteger(0); + Term x = d_solver.mkConst(intSort, "x"); + Term y = d_solver.mkConst(intSort, "y"); + // Assumptions for abduction: x > 0 + d_solver.assertFormula(d_solver.mkTerm(GT, x, zero)); + // Conjecture for abduction: y > 0 + Term conj = d_solver.mkTerm(GT, y, zero); + Term output; + // Fails due to option not set + ASSERT_THROW(d_solver.getAbduct(conj, output), CVC5ApiException); +} + TEST_F(TestApiBlackSolver, getInterpolant) { d_solver.setLogic("QF_LIA"); @@ -2536,5 +2546,21 @@ TEST_F(TestApiBlackSolver, Output) ASSERT_NE(cvc5::null_os.rdbuf(), d_solver.getOutput("inst").rdbuf()); } + +TEST_F(TestApiBlackSolver, issue7000) +{ + Sort s1 = d_solver.getIntegerSort(); + Sort s2 = d_solver.mkFunctionSort(s1, s1); + Sort s3 = d_solver.getRealSort(); + Term t4 = d_solver.mkPi(); + Term t7 = d_solver.mkConst(s3, "_x5"); + Term t37 = d_solver.mkConst(s2, "_x32"); + Term t59 = d_solver.mkConst(s2, "_x51"); + Term t72 = d_solver.mkTerm(EQUAL, t37, t59); + Term t74 = d_solver.mkTerm(GT, t4, t7); + // throws logic exception since logic is not higher order by default + ASSERT_THROW(d_solver.checkEntailed({t72, t74, t72, t72}), CVC5ApiException); +} + } // namespace test } // namespace cvc5 diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp index 757bacad6..d0c755cf7 100644 --- a/test/unit/api/sort_black.cpp +++ b/test/unit/api/sort_black.cpp @@ -61,6 +61,14 @@ TEST_F(TestApiBlackSort, operators_comparison) ASSERT_NO_THROW(d_solver.getIntegerSort() >= Sort()); } +TEST_F(TestApiBlackSort, isNull) +{ + Sort x; + ASSERT_TRUE(x.isNull()); + x = d_solver.getBooleanSort(); + ASSERT_FALSE(x.isNull()); +} + TEST_F(TestApiBlackSort, isBoolean) { ASSERT_TRUE(d_solver.getBooleanSort().isBoolean()); @@ -470,28 +478,28 @@ TEST_F(TestApiBlackSort, getUninterpretedSortConstructorArity) ASSERT_THROW(bvSort.getSortConstructorArity(), CVC5ApiException); } -TEST_F(TestApiBlackSort, getBVSize) +TEST_F(TestApiBlackSort, getBitVectorSize) { Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_NO_THROW(bvSort.getBVSize()); + ASSERT_NO_THROW(bvSort.getBitVectorSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - ASSERT_THROW(setSort.getBVSize(), CVC5ApiException); + ASSERT_THROW(setSort.getBitVectorSize(), CVC5ApiException); } -TEST_F(TestApiBlackSort, getFPExponentSize) +TEST_F(TestApiBlackSort, getFloatingPointExponentSize) { Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - ASSERT_NO_THROW(fpSort.getFPExponentSize()); + ASSERT_NO_THROW(fpSort.getFloatingPointExponentSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - ASSERT_THROW(setSort.getFPExponentSize(), CVC5ApiException); + ASSERT_THROW(setSort.getFloatingPointExponentSize(), CVC5ApiException); } -TEST_F(TestApiBlackSort, getFPSignificandSize) +TEST_F(TestApiBlackSort, getFloatingPointSignificandSize) { Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - ASSERT_NO_THROW(fpSort.getFPSignificandSize()); + ASSERT_NO_THROW(fpSort.getFloatingPointSignificandSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - ASSERT_THROW(setSort.getFPSignificandSize(), CVC5ApiException); + ASSERT_THROW(setSort.getFloatingPointSignificandSize(), CVC5ApiException); } TEST_F(TestApiBlackSort, getDatatypeParamSorts) |