diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-12-16 08:10:47 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-12-16 08:10:47 -0600 |
| commit | 5d2daf534a6b23dc31c359e38e0b93a2fe907ed4 (patch) | |
| tree | 3b9b587fb8d500784f635af4f532ec0c747ef098 | |
| parent | 577d4b6bde6c31bd77254de9355666f6b698cc45 (diff) | |
| parent | 4a7c0c73f69aabb20be4c79c47047ce23d3358b0 (diff) | |
Merge branch 'master' into deleteInvalidMkConstdeleteInvalidMkConst
45 files changed, 1139 insertions, 376 deletions
diff --git a/docs/api/java/java.rst b/docs/api/java/java.rst index 725e2bf7c..71a70023b 100644 --- a/docs/api/java/java.rst +++ b/docs/api/java/java.rst @@ -1,5 +1,5 @@ Java API -====================== +======== The Java API for cvc5 mostly mirrors the :doc:`C++ API <../cpp/cpp>` and supports operator overloading, iterators, and exceptions. @@ -56,7 +56,7 @@ Building cvc5 Java API (< (+ a b) 1) `Package io.github.cvc5.api <io/github/cvc5/api/package-summary.html>`_ -^^^^^^^^^^^^^^^ +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ * class `Datatype <io/github/cvc5/api/Datatype.html>`_ * class `DatatypeConstructor <io/github/cvc5/api/DatatypeConstructor.html>`_ diff --git a/docs/api/python/z3compat/boolean.rst b/docs/api/python/z3compat/boolean.rst index e48e7f9e9..8ccc649c5 100644 --- a/docs/api/python/z3compat/boolean.rst +++ b/docs/api/python/z3compat/boolean.rst @@ -2,7 +2,7 @@ Core & Booleans ================ Basic Boolean Term Builders -------------------- +--------------------------- .. autofunction:: cvc5_z3py_compat.Bool .. autofunction:: cvc5_z3py_compat.Bools .. autofunction:: cvc5_z3py_compat.BoolVal @@ -11,13 +11,13 @@ Basic Boolean Term Builders .. autofunction:: cvc5_z3py_compat.BoolVector Basic Generic Term Builders -------------------- +--------------------------- .. autofunction:: cvc5_z3py_compat.Const .. autofunction:: cvc5_z3py_compat.Consts .. autofunction:: cvc5_z3py_compat.FreshConst Boolean Operators -------------------- +----------------- .. autofunction:: cvc5_z3py_compat.And .. autofunction:: cvc5_z3py_compat.Or .. autofunction:: cvc5_z3py_compat.Not @@ -26,7 +26,7 @@ Boolean Operators .. autofunction:: cvc5_z3py_compat.Xor Generic Operators -------------------- +----------------- .. autofunction:: cvc5_z3py_compat.If .. autofunction:: cvc5_z3py_compat.Distinct @@ -41,7 +41,7 @@ for building equality and disequality terms. Testers -------------------- +------- .. autofunction:: cvc5_z3py_compat.is_bool .. autofunction:: cvc5_z3py_compat.is_true .. autofunction:: cvc5_z3py_compat.is_false @@ -55,7 +55,7 @@ Testers Classes --------- +------- .. autoclass:: cvc5_z3py_compat.ExprRef :members: :special-members: diff --git a/docs/ext/smtliblexer.py b/docs/ext/smtliblexer.py index 54441ca25..f6f1679c0 100644 --- a/docs/ext/smtliblexer.py +++ b/docs/ext/smtliblexer.py @@ -16,16 +16,18 @@ class SmtLibLexer(RegexLexer): name = 'smtlib' COMMANDS = [ - 'assert', 'check-sat', 'check-sat-assuming', 'declare-const', - 'declare-datatype', 'declare-datatypes', 'declare-codatatypes', - 'declare-fun', 'declare-sort', 'define-fun', 'define-fun-rec', - 'define-funs-rec', 'define-sort', 'echo', 'exit', 'get-assertions', - 'get-assignment', 'get-info', 'get-model', 'get-option', 'get-proof', + 'assert', 'block-model', 'block-model-values', 'check-sat', + 'check-sat-assuming', 'declare-const', 'declare-datatype', + 'declare-datatypes', 'declare-codatatypes', 'declare-fun', + 'declare-sort', 'define-fun', 'define-fun-rec', 'define-funs-rec', + 'define-sort', 'echo', 'exit', 'get-abduct', 'get-assertions', + 'get-assignment', 'get-info', 'get-interpol', 'get-model', + 'get-option', 'get-proof', 'get-qe', 'get-qe-disjunct', 'get-unsat-assumptions', 'get-unsat-core', 'get-value', 'pop', 'push', 'reset', 'reset-assertions', 'set-info', 'set-logic', 'set-option', # SyGuS v2 - 'declare-var', 'constraint', 'inv-constraint', 'synth-fun', - 'check-synth', 'synth-inv', 'declare-pool', + 'assume', 'check-synth', 'constraint', 'declare-var', 'inv-constraint', + 'synth-fun', 'synth-inv', 'declare-pool', ] SORTS = [ 'Array', 'BitVec', 'Bool', 'FloatingPoint', 'Float[0-9]+', 'Int', diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1d57dfeb4..fde0088e8 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -912,10 +912,12 @@ libcvc5_add_sources( theory/quantifiers/sygus/sygus_pbe.h theory/quantifiers/sygus/sygus_process_conj.cpp theory/quantifiers/sygus/sygus_process_conj.h - theory/quantifiers/sygus/sygus_reconstruct.cpp - theory/quantifiers/sygus/sygus_reconstruct.h theory/quantifiers/sygus/sygus_qe_preproc.cpp theory/quantifiers/sygus/sygus_qe_preproc.h + theory/quantifiers/sygus/sygus_random_enumerator.cpp + theory/quantifiers/sygus/sygus_random_enumerator.h + theory/quantifiers/sygus/sygus_reconstruct.cpp + theory/quantifiers/sygus/sygus_reconstruct.h theory/quantifiers/sygus/sygus_repair_const.cpp theory/quantifiers/sygus/sygus_repair_const.h theory/quantifiers/sygus/sygus_stats.cpp diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index e3f64349f..ec7b92088 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -1510,13 +1510,13 @@ class CVC5_EXPORT Term * * 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)))) - * ``` + * + * (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 A universe set term (kind SET_UNIVERSE) is not considered to be + * @note A universe set term `(kind SET_UNIVERSE)` is not considered to be * a set value. */ bool isSetValue() const; @@ -1532,7 +1532,7 @@ class CVC5_EXPORT Term bool isSequenceValue() const; /** * Asserts isSequenceValue(). - * @note It is usually necessary for sequences to call `Solver::simplify()` + * @note It is usually necessary for sequences to call Solver::simplify() * to turn a sequence that is constructed by, e.g., concatenation of * unit sequences, into a sequence value. * @return the representation of a sequence value as a vector of terms. @@ -1983,13 +1983,26 @@ class CVC5_EXPORT DatatypeConstructor * * This method is required for constructors of parametric datatypes whose * return type cannot be determined by type inference. For example, given: - * (declare-datatype List (par (T) ((nil) (cons (head T) (tail (List T)))))) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (declare-datatype List + * (par (T) ((nil) (cons (head T) (tail (List T)))))) + * \endverbatim + * * The type of nil terms need to be provided by the user. In SMT version 2.6, * this is done via the syntax for qualified identifiers: - * (as nil (List Int)) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (as nil (List Int)) + * \endverbatim + * * This method is equivalent of applying the above, where this * DatatypeConstructor is the one corresponding to nil, and retSort is - * (List Int). + * ``(List Int)``. * * @note the returned constructor term ``t`` is an operator, while * ``Solver::mkTerm(APPLY_CONSTRUCTOR, t)`` is used to construct the @@ -3691,10 +3704,14 @@ class CVC5_EXPORT Solver /** * Create (first-order) constant (0-arity function symbol). + * * SMT-LIB: - * \verbatim - * ( declare-const <symbol> <sort> ) - * ( declare-fun <symbol> ( ) <sort> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (declare-const <symbol> <sort>) + * (declare-fun <symbol> () <sort>) * \endverbatim * * @param sort the sort of the constant @@ -3779,30 +3796,45 @@ class CVC5_EXPORT Solver /** * Assert a formula. + * * SMT-LIB: - * \verbatim - * ( assert <term> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (assert <term>) * \endverbatim + * * @param term the formula to assert */ void assertFormula(const Term& term) const; /** * Check satisfiability. + * * SMT-LIB: - * \verbatim - * ( check-sat ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (check-sat) * \endverbatim + * * @return the result of the satisfiability check. */ Result checkSat() const; /** * Check satisfiability assuming the given formula. + * * SMT-LIB: - * \verbatim - * ( check-sat-assuming ( <prop_literal> ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (check-sat-assuming ( <prop_literal> )) * \endverbatim + * * @param assumption the formula to assume * @return the result of the satisfiability check. */ @@ -3810,10 +3842,15 @@ class CVC5_EXPORT Solver /** * Check satisfiability assuming the given formulas. + * * SMT-LIB: - * \verbatim - * ( check-sat-assuming ( <prop_literal>+ ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (check-sat-assuming ( <prop_literal>+ )) * \endverbatim + * * @param assumptions the formulas to assume * @return the result of the satisfiability check. */ @@ -3836,10 +3873,15 @@ class CVC5_EXPORT Solver /** * Create datatype sort. + * * SMT-LIB: - * \verbatim - * ( declare-datatype <symbol> <datatype_decl> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (declare-datatype <symbol> <datatype_decl>) * \endverbatim + * * @param symbol the name of the datatype sort * @param ctors the constructor declarations of the datatype sort * @return the datatype sort @@ -3849,10 +3891,15 @@ class CVC5_EXPORT Solver /** * Declare n-ary function symbol. + * * SMT-LIB: - * \verbatim - * ( declare-fun <symbol> ( <sort>* ) <sort> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (declare-fun <symbol> ( <sort>* ) <sort>) * \endverbatim + * * @param symbol the name of the function * @param sorts the sorts of the parameters to this function * @param sort the sort of the return value of this function @@ -3864,10 +3911,15 @@ class CVC5_EXPORT Solver /** * Declare uninterpreted sort. + * * SMT-LIB: - * \verbatim - * ( declare-sort <symbol> <numeral> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (declare-sort <symbol> <numeral>) * \endverbatim + * * @param symbol the name of the sort * @param arity the arity of the sort * @return the sort @@ -3876,10 +3928,15 @@ class CVC5_EXPORT Solver /** * Define n-ary function. + * * SMT-LIB: - * \verbatim - * ( define-fun <function_def> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (define-fun <function_def>) * \endverbatim + * * @param symbol the name of the function * @param bound_vars the parameters to this function * @param sort the sort of the return value of this function @@ -3896,10 +3953,15 @@ class CVC5_EXPORT Solver /** * Define recursive function. + * * SMT-LIB: - * \verbatim - * ( define-fun-rec <function_def> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (define-fun-rec <function_def>) * \endverbatim + * * @param symbol the name of the function * @param bound_vars the parameters to this function * @param sort the sort of the return value of this function @@ -3916,10 +3978,15 @@ class CVC5_EXPORT Solver /** * Define recursive function. + * * SMT-LIB: - * \verbatim - * ( define-fun-rec <function_def> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (define-fun-rec <function_def>) * \endverbatim + * * Create parameter 'fun' with mkConst(). * @param fun the sorted function * @param bound_vars the parameters to this function @@ -3935,10 +4002,18 @@ class CVC5_EXPORT Solver /** * Define recursive functions. + * * SMT-LIB: - * \verbatim - * ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (define-funs-rec + * ( <function_decl>_1 ... <function_decl>_n ) + * ( <term>_1 ... <term>_n ) + * ) * \endverbatim + * * Create elements of parameter 'funs' with mkConst(). * @param funs the sorted functions * @param bound_vars the list of parameters to the functions @@ -3954,10 +4029,15 @@ class CVC5_EXPORT Solver /** * Echo a given string to the given output stream. + * * SMT-LIB: - * \verbatim - * ( echo <std::string> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (echo <string>) * \endverbatim + * * @param out the output stream * @param str the string to echo */ @@ -3965,27 +4045,45 @@ class CVC5_EXPORT Solver /** * Get the list of asserted formulas. + * * SMT-LIB: - * \verbatim - * ( get-assertions ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-assertions) * \endverbatim + * * @return the list of asserted formulas */ std::vector<Term> getAssertions() const; /** * Get info from the solver. - * SMT-LIB: \verbatim( get-info <info_flag> )\endverbatim + * + * SMT-LIB: + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-info <info_flag>) + * \endverbatim + * * @return the info */ std::string getInfo(const std::string& flag) const; /** * Get the value of a given option. + * * SMT-LIB: - * \verbatim - * ( get-option <keyword> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-option <keyword>) * \endverbatim + * * @param option the option for which the value is queried * @return a string representation of the option value */ @@ -4014,22 +4112,36 @@ class CVC5_EXPORT Solver /** * Get the set of unsat ("failed") assumptions. + * * SMT-LIB: - * \verbatim - * ( get-unsat-assumptions ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-unsat-assumptions) + * + * Requires to enable option + * :ref:`produce-unsat-assumptions <lbl-option-produce-unsat-assumptions>`. * \endverbatim - * Requires to enable option 'produce-unsat-assumptions'. + * * @return the set of unsat assumptions. */ std::vector<Term> getUnsatAssumptions() const; /** * Get the unsatisfiable core. + * * SMT-LIB: - * \verbatim - * ( get-unsat-core ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-unsat-core) + * + * Requires to enable option + * :ref:`produce-unsat-cores <lbl-option-produce-unsat-cores>`. * \endverbatim - * Requires to enable option 'produce-unsat-cores'. + * * @return a set of terms representing the unsatisfiable core */ std::vector<Term> getUnsatCore() const; @@ -4039,18 +4151,25 @@ class CVC5_EXPORT Solver * intended to be called immediately after any response to a checkSat. * * @return a map from (a subset of) the input assertions to a real value that - * is an estimate of how difficult each assertion was to solve. Unmentioned - * assertions can be assumed to have zero difficulty. + * is an estimate of how difficult each assertion was to solve. + * Unmentioned assertions can be assumed to have zero difficulty. */ std::map<Term, Term> getDifficulty() const; /** * Get the refutation proof + * * SMT-LIB: - * \verbatim - * ( get-proof ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-proof) + * + * Requires to enable option + * :ref:`produce-proofs <lbl-option-produce-proofs>`. * \endverbatim - * Requires to enable option 'produce-proofs'. + * * @return a string representing the proof, according to the value of * proof-format-mode. */ @@ -4058,10 +4177,15 @@ class CVC5_EXPORT Solver /** * Get the value of the given term in the current model. + * * SMT-LIB: - * \verbatim - * ( get-value ( <term> ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-value ( <term> )) * \endverbatim + * * @param term the term for which the value is queried * @return the value of the given term */ @@ -4069,10 +4193,15 @@ class CVC5_EXPORT Solver /** * Get the values of the given terms in the current model. + * * SMT-LIB: - * \verbatim - * ( get-value ( <term>+ ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-value ( <term>* )) * \endverbatim + * * @param terms the terms for which the value is queried * @return the values of the given terms */ @@ -4092,7 +4221,11 @@ class CVC5_EXPORT Solver * This returns false if the model value of free constant v was not essential * for showing the satisfiability of the last call to checkSat using the * current model. This method will only return false (for any v) if - * the model-cores option has been set. + * option + * \verbatim:rst:inline + * :ref:`model-cores <lbl-option-model-cores>` + * \endverbatim + * has been set. * * @param v The term in question * @return true if v is a model core symbol @@ -4101,11 +4234,20 @@ class CVC5_EXPORT Solver /** * Get the model + * * SMT-LIB: - * \verbatim - * ( get-model ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-model) + * + * Requires to enable option + * :ref:`produce-models <lbl-option-produce-models>`. * \endverbatim - * Requires to enable option 'produce-models'. + * + * \endverbatim + * * @param sorts The list of uninterpreted sorts that should be printed in the * model. * @param vars The list of free constants that should be printed in the @@ -4117,49 +4259,76 @@ class CVC5_EXPORT Solver /** * Do quantifier elimination. + * * SMT-LIB: - * \verbatim - * ( get-qe <q> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-qe <q>) * \endverbatim + * * Requires a logic that supports quantifier elimination. Currently, the only * logics supported by quantifier elimination is LRA and LIA. - * @param q a quantified formula of the form: - * Q x1...xn. P( x1...xn, y1...yn ) - * where P( x1...xn, y1...yn ) is a quantifier-free formula - * @return a formula ret such that, given the current set of formulas A - * asserted to this solver: - * - ( A ^ q ) and ( A ^ ret ) are equivalent - * - ret is quantifier-free formula containing only free variables in - * y1...yn. + * + * @note Quantifier Elimination is is only complete for LRA and LIA. + * + * @param q a quantified formula of the form + * @f$Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)@f$ + * where + * @f$Q\bar{x}@f$ is a set of quantified variables of the form + * @f$Q x_1...x_k@f$ and + * @f$P( x_1...x_i, y_1...y_j )@f$ is a quantifier-free formula + * @return a formula @f$\phi@f$ such that, given the current set of formulas + * @f$A@f$ asserted to this solver: + * - @f$(A \wedge q)@f$ and @f$(A \wedge \phi)@f$ are equivalent + * - @f$\phi@f$ is quantifier-free formula containing only free + * variables in @f$y_1...y_n@f$. */ Term getQuantifierElimination(const Term& q) const; /** * Do partial quantifier elimination, which can be used for incrementally * computing the result of a quantifier elimination. + * * SMT-LIB: - * \verbatim - * ( get-qe-disjunct <q> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-qe-disjunct <q>) * \endverbatim + * * Requires a logic that supports quantifier elimination. Currently, the only * logics supported by quantifier elimination is LRA and LIA. - * @param q a quantified formula of the form: - * Q x1...xn. P( x1...xn, y1...yn ) - * where P( x1...xn, y1...yn ) is a quantifier-free formula - * @return a formula ret such that, given the current set of formulas A - * asserted to this solver: - * - (A ^ q) => (A ^ ret) if Q is forall or (A ^ ret) => (A ^ q) if Q is - * exists, - * - ret is quantifier-free formula containing only free variables in - * y1...yn, - * - If Q is exists, let A^Q_n be the formula - * A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n - * where for each i=1,...n, formula ret^Q_i is the result of calling - * getQuantifierEliminationDisjunct for q with the set of assertions - * A^Q_{i-1}. Similarly, if Q is forall, then let A^Q_n be - * A ^ ret^Q_1 ^ ... ^ ret^Q_n - * where ret^Q_i is the same as above. In either case, we have - * that ret^Q_j will eventually be true or false, for some finite j. + * @param q a quantified formula of the form + * @f$Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)@f$ + * where + * @f$Q\bar{x}@f$ is a set of quantified variables of the form + * @f$Q x_1...x_k@f$ and + * @f$P( x_1...x_i, y_1...y_j )@f$ is a quantifier-free formula + * @return a formula @f$\phi@f$ such that, given the current set of formulas + * @f$A@f$ asserted to this solver: + * - @f$(A \wedge q \implies A \wedge \phi)@f$ if @f$Q@f$ is + * @f$\forall@f$, and @f$(A \wedge \phi \implies A \wedge q)@f$ if + * @f$Q@f$ is @f$\exists@f$ + * - @f$\phi@f$ is quantifier-free formula containing only free + * variables in @f$y_1...y_n@f$ + * - If @f$Q@f$ is @f$\exists@f$, let @f$(A \wedge Q_n)@f$ be the + * formula + * @f$(A \wedge \neg (\phi \wedge Q_1) \wedge ... \wedge + * \neg (\phi \wedge Q_n))@f$ + * where for each @f$i = 1...n@f$, + * formula @f$(\phi \wedge Q_i)@f$ is the result of calling + * Solver::getQuantifierEliminationDisjunct() for @f$q@f$ with the + * set of assertions @f$(A \wedge Q_{i-1})@f$. + * Similarly, if @f$Q@f$ is @f$\forall@f$, then let + * @f$(A \wedge Q_n)@f$ be + * @f$(A \wedge (\phi \wedge Q_1) \wedge ... \wedge (\phi \wedge + * Q_n))@f$ + * where @f$(\phi \wedge Q_i)@f$ is the same as above. + * In either case, we have that @f$(\phi \wedge Q_j)@f$ will + * eventually be true or false, for some finite j. */ Term getQuantifierEliminationDisjunct(const Term& q) const; @@ -4186,10 +4355,15 @@ class CVC5_EXPORT Solver /** * Declare a symbolic pool of terms with the given initial value. + * * SMT-LIB: - * \verbatim - * ( declare-pool <symbol> <sort> ( <term>* ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (declare-pool <symbol> <sort> ( <term>* )) * \endverbatim + * * @param symbol The name of the pool * @param sort The sort of the elements of the pool. * @param initValue The initial value of the pool @@ -4199,21 +4373,33 @@ class CVC5_EXPORT Solver const std::vector<Term>& initValue) const; /** * Pop (a) level(s) from the assertion stack. + * * SMT-LIB: - * \verbatim - * ( pop <numeral> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (pop <numeral>) * \endverbatim + * * @param nscopes the number of levels to pop */ void pop(uint32_t nscopes = 1) const; /** * Get an interpolant + * * SMT-LIB: - * \verbatim - * ( get-interpol <conj> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-interpol <conj>) + * + * Requires to enable option + * :ref:`produce-interpols <lbl-option-produce-interpols>`. * \endverbatim - * Requires to enable option 'produce-interpols'. + * * @param conj the conjecture term * @param output a Term I such that A->I and I->B are valid, where A is the * current set of assertions and B is given in the input by conj. @@ -4223,11 +4409,18 @@ class CVC5_EXPORT Solver /** * Get an interpolant + * * SMT-LIB: - * \verbatim - * ( get-interpol <conj> <g> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-interpol <conj> <grammar>) + * + * Requires to enable option + * :ref:`produce-interpols <lbl-option-produce-interpols>`. * \endverbatim - * Requires to enable option 'produce-interpols'. + * * @param conj the conjecture term * @param grammar the grammar for the interpolant I * @param output a Term I such that A->I and I->B are valid, where A is the @@ -4238,56 +4431,88 @@ class CVC5_EXPORT Solver /** * Get an abduct. + * * SMT-LIB: - * \verbatim - * ( get-abduct <conj> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-abduct <conj>) + * + * Requires to enable option + * :ref:`produce-abducts <lbl-option-produce-abducts>`. * \endverbatim - * Requires enabling option 'produce-abducts' + * * @param conj the conjecture term - * @param output a term C such that A^C is satisfiable, and A^~B^C is - * unsatisfiable, where A is the current set of assertions and B is - * given in the input by conj - * @return true if it gets C successfully, false otherwise + * @param output a term @f$C@f$ such that @f$(A \wedge C)@f$ is satisfiable, + * and @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where + * @f$A@f$ is the current set of assertions and @f$B@f$ is + * given in the input by ``conj``. + * @return true if it gets abduct @f$C@f$ successfully, false otherwise */ bool getAbduct(const Term& conj, Term& output) const; /** * Get an abduct. + * * SMT-LIB: - * \verbatim - * ( get-abduct <conj> <g> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-abduct <conj> <grammar>) + * + * Requires to enable option + * :ref:`produce-abducts <lbl-option-produce-abducts>`. * \endverbatim - * Requires enabling option 'produce-abducts' + * * @param conj the conjecture term - * @param grammar the grammar for the abduct C - * @param output a term C such that A^C is satisfiable, and A^~B^C is - * unsatisfiable, where A is the current set of assertions and B is - * given in the input by conj - * @return true if it gets C successfully, false otherwise + * @param grammar the grammar for the abduct @f$C@f$ + * @param output a term C such that @f$(A \wedge C)@f$ is satisfiable, and + * @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where @f$A@f$ is + * the current set of assertions and @f$B@f$ is given in the input by + * ``conj`` + * @return true if it gets abduct @f$C@f$ successfully, false otherwise */ bool getAbduct(const Term& conj, Grammar& grammar, Term& output) const; /** * Block the current model. Can be called only if immediately preceded by a * SAT or INVALID query. + * * SMT-LIB: - * \verbatim - * ( block-model ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (block-model) + * + * Requires enabling option + * :ref:`produce-models <lbl-option-produce-models>`. + * 'produce-models' and setting option + * :ref:`block-models <lbl-option-block-models>`. + * to a mode other than ``none``. * \endverbatim - * Requires enabling 'produce-models' option and setting 'block-models' option - * to a mode other than "none". */ void blockModel() const; /** * Block the current model values of (at least) the values in terms. Can be * called only if immediately preceded by a SAT or NOT_ENTAILED query. + * * SMT-LIB: - * \verbatim - * ( block-model-values ( <terms>+ ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (block-model-values ( <terms>+ )) + * + * Requires enabling option + * :ref:`produce-models <lbl-option-produce-models>`. + * 'produce-models' and setting option + * :ref:`block-models <lbl-option-block-models>`. + * to a mode other than ``none``. * \endverbatim - * Requires enabling 'produce-models' option and setting 'block-models' option - * to a mode other than "none". */ void blockModelValues(const std::vector<Term>& terms) const; @@ -4299,29 +4524,44 @@ class CVC5_EXPORT Solver /** * Push (a) level(s) to the assertion stack. + * * SMT-LIB: - * \verbatim - * ( push <numeral> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (push <numeral>) * \endverbatim + * * @param nscopes the number of levels to push */ void push(uint32_t nscopes = 1) const; /** * Remove all assertions. + * * SMT-LIB: - * \verbatim - * ( reset-assertions ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (reset-assertions) * \endverbatim + * */ void resetAssertions() const; /** * Set info. + * * SMT-LIB: - * \verbatim - * ( set-info <attribute> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (set-info <attribute>) * \endverbatim + * * @param keyword the info flag * @param value the value of the info flag */ @@ -4329,20 +4569,30 @@ class CVC5_EXPORT Solver /** * Set logic. + * * SMT-LIB: - * \verbatim - * ( set-logic <symbol> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (set-logic <symbol>) * \endverbatim + * * @param logic the logic to set */ void setLogic(const std::string& logic) const; /** * Set option. + * * SMT-LIB: - * \verbatim - * ( set-option <option> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (set-option :<option> <value>) * \endverbatim + * * @param option the option name * @param value the option value */ @@ -4361,10 +4611,15 @@ class CVC5_EXPORT Solver /** * Append \p symbol to the current list of universal variables. + * * SyGuS v2: - * \verbatim - * ( declare-var <symbol> <sort> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (declare-var <symbol> <sort>) * \endverbatim + * * @param sort the sort of the universal variable * @param symbol the name of the universal variable * @return the universal variable @@ -4385,10 +4640,15 @@ class CVC5_EXPORT Solver /** * Synthesize n-ary function. + * * SyGuS v2: - * \verbatim - * ( synth-fun <symbol> ( <boundVars>* ) <sort> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (synth-fun <symbol> ( <boundVars>* ) <sort>) * \endverbatim + * * @param symbol the name of the function * @param boundVars the parameters to this function * @param sort the sort of the return value of this function @@ -4400,10 +4660,15 @@ class CVC5_EXPORT Solver /** * Synthesize n-ary function following specified syntactic constraints. + * * SyGuS v2: - * \verbatim - * ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (synth-fun <symbol> ( <boundVars>* ) <sort> <grammar>) * \endverbatim + * * @param symbol the name of the function * @param boundVars the parameters to this function * @param sort the sort of the return value of this function @@ -4417,10 +4682,15 @@ class CVC5_EXPORT Solver /** * Synthesize invariant. + * * SyGuS v2: - * \verbatim - * ( synth-inv <symbol> ( <boundVars>* ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (synth-inv <symbol> ( <boundVars>* )) * \endverbatim + * * @param symbol the name of the invariant * @param boundVars the parameters to this invariant * @return the invariant @@ -4430,10 +4700,15 @@ class CVC5_EXPORT Solver /** * Synthesize invariant following specified syntactic constraints. + * * SyGuS v2: - * \verbatim - * ( synth-inv <symbol> ( <boundVars>* ) <g> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (synth-inv <symbol> ( <boundVars>* ) <grammar>) * \endverbatim + * * @param symbol the name of the invariant * @param boundVars the parameters to this invariant * @param grammar the syntactic constraints @@ -4445,20 +4720,30 @@ class CVC5_EXPORT Solver /** * Add a forumla to the set of Sygus constraints. + * * SyGuS v2: - * \verbatim - * ( constraint <term> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (constraint <term>) * \endverbatim + * * @param term the formula to add as a constraint */ void addSygusConstraint(const Term& term) const; /** * Add a forumla to the set of Sygus assumptions. + * * SyGuS v2: - * \verbatim - * ( assume <term> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (assume <term>) * \endverbatim + * * @param term the formula to add as an assumption */ void addSygusAssume(const Term& term) const; @@ -4466,10 +4751,15 @@ class CVC5_EXPORT Solver /** * Add a set of Sygus constraints to the current state that correspond to an * invariant synthesis problem. + * * SyGuS v2: - * \verbatim - * ( inv-constraint <inv> <pre> <trans> <post> ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (inv-constraint <inv> <pre> <trans> <post>) * \endverbatim + * * @param inv the function-to-synthesize * @param pre the pre-condition * @param trans the transition relation @@ -4481,10 +4771,15 @@ class CVC5_EXPORT Solver * Try to find a solution for the synthesis conjecture corresponding to the * current list of functions-to-synthesize, universal variables and * constraints. + * * SyGuS v2: - * \verbatim - * ( check-synth ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (check-synth) * \endverbatim + * * @return the result of the synthesis conjecture. */ Result checkSynth() const; @@ -4605,10 +4900,15 @@ class CVC5_EXPORT Solver /** * Synthesize n-ary function following specified syntactic constraints. + * * SMT-LIB: - * \verbatim - * ( synth-fun <symbol> ( <boundVars>* ) <sort> <g>? ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (synth-fun <symbol> ( <boundVars>* ) <sort> <grammar>?) * \endverbatim + * * @param symbol the name of the function * @param boundVars the parameters to this function * @param sort the sort of the return value of this function diff --git a/src/options/README.md b/src/options/README.md index c3e018215..2f89f04ee 100644 --- a/src/options/README.md +++ b/src/options/README.md @@ -26,7 +26,7 @@ Specifying Options Options can be defined within a module file with the `[[option]]` tag, the required attributes for an option are: -* `category` (string): one of `common`, `expert`, `regular`, or `undocumented` +* `category` (string): one of `common`, `regular`, `expert`, or `undocumented` * `type` (string): the C++ type of the option value, see below for more details. Optional attributes are: @@ -59,6 +59,16 @@ Optional attributes are: given) +Option categories +----------------- + +Every option has one of the following categories that influences where and how an option is visible: + +* `common`: Used for the most common options. All `common` options are shown at the very top in both the online documentation and the output of `--help` on the command line. +* `regular`: This should be used for most options. +* `expert`: This is for options that should be used with care only. A warning is shown in both the online documentation and the command line help. +* `undocumented`: Such an option is skipped entirely in both the online documentation and the command line help. This should only be used when users don't have a (reasonable) use case for this option (e.g., because it stores data that is added via another option like for `output` and `outputTagHolder`). + Option types ------------ diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 042fd6b8a..415dbf9f3 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -3,27 +3,30 @@ name = "Base" [[option]] name = "err" - category = "undocumented" + category = "regular" long = "err=erroutput" type = "ManagedErr" alias = ["diagnostic-output-channel"] predicates = ["setErrStream"] includes = ["<iostream>", "options/managed_streams.h"] + help = "Set the error (or diagnostic) output channel. Writes to stderr for \"stderr\" or \"--\", stdout for \"stdout\" or the given filename otherwise." [[option]] name = "in" - category = "undocumented" + category = "regular" long = "in=input" type = "ManagedIn" includes = ["<iostream>", "options/managed_streams.h"] + help = "Set the error (or diagnostic) output channel. Reads from stdin for \"stdin\" or \"--\" and the given filename otherwise." [[option]] name = "out" - category = "undocumented" + category = "regular" long = "out=output" type = "ManagedOut" alias = ["regular-output-channel"] includes = ["<iostream>", "options/managed_streams.h"] + help = "Set the error (or diagnostic) output channel. Writes to stdout for \"stdout\" or \"--\", stderr for \"stderr\" or the given filename otherwise." [[option]] name = "inputLanguage" diff --git a/src/options/parser_options.toml b/src/options/parser_options.toml index 6fc683368..5552a677d 100644 --- a/src/options/parser_options.toml +++ b/src/options/parser_options.toml @@ -45,10 +45,11 @@ name = "Parser" # overwrite an existing file with malicious content. [[option]] name = "filesystemAccess" - category = "undocumented" + category = "expert" long = "filesystem-access" type = "bool" default = "true" + help = "limits the file system access if set to false" [[option]] name = "forceLogicString" diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 80692055f..4021ac2aa 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1092,6 +1092,9 @@ name = "Quantifiers" [[option.mode.ENUM]] name = "enum" help = "Use optimized enumerator for actively-generated sygus enumerators." +[[option.mode.RANDOM]] + name = "random" + help = "Use basic random enumerator for actively-generated sygus enumerators." [[option.mode.VAR_AGNOSTIC]] name = "var-agnostic" help = "Use sygus solver to enumerate terms that are agnostic to variables." @@ -1100,6 +1103,16 @@ name = "Quantifiers" help = "Internally decide the best policy for each enumerator." [[option]] + name = "sygusActiveGenRandomP" + category = "regular" + long = "sygus-active-gen-random-p=P" + type = "double" + default = "0.5" + minimum = "0.0" + maximum = "1.0" + help = "the parameter of the geometric distribution used to determine the size of terms generated by --sygus-active-gen=random" + +[[option]] name = "sygusActiveGenEnumConsts" category = "regular" long = "sygus-active-gen-cfactor=N" diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 026c8f494..1e55f63d0 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -377,7 +377,7 @@ name = "SMT Layer" [[option]] name = "solveBVAsInt" - category = "undocumented" + category = "expert" long = "solve-bv-as-int=MODE" type = "SolveBVAsIntMode" default = "OFF" @@ -401,7 +401,7 @@ name = "SMT Layer" [[option]] name = "BVAndIntegerGranularity" - category = "undocumented" + category = "expert" long = "bvand-integer-granularity=N" type = "uint64_t" default = "1" @@ -409,7 +409,7 @@ name = "SMT Layer" [[option]] name = "iandMode" - category = "undocumented" + category = "expert" long = "iand-mode=mode" type = "IandMode" default = "VALUE" @@ -427,7 +427,7 @@ name = "SMT Layer" [[option]] name = "solveIntAsBV" - category = "undocumented" + category = "expert" long = "solve-int-as-bv=N" type = "uint64_t" default = "0" @@ -435,7 +435,7 @@ name = "SMT Layer" [[option]] name = "solveRealAsInt" - category = "undocumented" + category = "expert" long = "solve-real-as-int" type = "bool" default = "false" @@ -443,7 +443,7 @@ name = "SMT Layer" [[option]] name = "produceInterpols" - category = "undocumented" + category = "regular" long = "produce-interpols=MODE" type = "ProduceInterpols" default = "NONE" @@ -470,7 +470,7 @@ name = "SMT Layer" [[option]] name = "produceAbducts" - category = "undocumented" + category = "regular" long = "produce-abducts" type = "bool" default = "false" diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 05025708b..74112b286 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -209,6 +209,22 @@ name = "Strings Theory" help = "use regular expressions for eager length conflicts" [[option]] + name = "stringEagerSolver" + category = "regular" + long = "strings-eager-solver" + type = "bool" + default = "true" + help = "use the eager solver" + +[[option]] + name = "stringRegexpInclusion" + category = "regular" + long = "strings-regexp-inclusion" + type = "bool" + default = "true" + help = "use regular expression inclusion" + +[[option]] name = "seqArray" category = "expert" long = "seq-array=MODE" diff --git a/src/smt/proof_final_callback.cpp b/src/smt/proof_final_callback.cpp index 484f0dd73..4cf3a68f7 100644 --- a/src/smt/proof_final_callback.cpp +++ b/src/smt/proof_final_callback.cpp @@ -109,6 +109,12 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn, if (getInferenceId(args[0], id)) { d_annotationRuleIds << id; + // Use e.g. `--check-proofs --proof-annotate -t im-pf` to see a list of + // inference that appear in the final proof. + Trace("im-pf") << "(inference-pf " << id << " " << pn->getResult() + << ")" << std::endl; + Trace("im-pf-assert") + << "(assert " << pn->getResult() << ") ; " << id << std::endl; } } } diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index bf8798485..9b4623d37 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1839,7 +1839,6 @@ bool TheoryArithPrivate::attemptSolveInteger(Theory::Effort effortLevel, bool em << " " << effortLevel << " " << d_lastContextIntegerAttempted << " " << level - << " " << hasIntegerModel() << endl; if(d_qflraStatus == Result::UNSAT){ return false; } @@ -3372,8 +3371,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) Debug("arith") << "integer? " << " conf/split " << emmittedConflictOrSplit - << " fulleffort " << Theory::fullEffort(effortLevel) - << " hasintmodel " << hasIntegerModel() << endl; + << " fulleffort " << Theory::fullEffort(effortLevel) << endl; if(!emmittedConflictOrSplit && Theory::fullEffort(effortLevel) && !hasIntegerModel()){ Node possibleConflict = Node::null(); diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index 0694c179b..39598975b 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -260,18 +260,7 @@ bool TheoryBags::collectModelValues(TheoryModel* m, { Node key = d_state.getRepresentative(e); Node countTerm = NodeManager::currentNM()->mkNode(BAG_COUNT, e, r); - context::CDList<TNode>::const_iterator shared_it = - std::find(d_sharedTerms.begin(), d_sharedTerms.end(), countTerm); - eq::EqClassIterator it = - eq::EqClassIterator(r, d_state.getEqualityEngine()); - while (!it.isFinished() && shared_it == d_sharedTerms.end()) - { - Node bag = *(++it); - countTerm = NodeManager::currentNM()->mkNode(BAG_COUNT, e, bag); - shared_it = - std::find(d_sharedTerms.begin(), d_sharedTerms.end(), countTerm); - } - Node value = d_valuation.getModelValue(countTerm); + Node value = m->getRepresentative(countTerm); elementReps[key] = value; } Node rep = NormalForm::constructBagFromElements(tn, elementReps); @@ -289,9 +278,15 @@ Node TheoryBags::getModelValue(TNode node) { return Node::null(); } void TheoryBags::preRegisterTerm(TNode n) { - Trace("bags::TheoryBags::preRegisterTerm") << n << std::endl; + Trace("bags") << "TheoryBags::preRegisterTerm(" << n << ")" << std::endl; switch (n.getKind()) { + case kind::EQUAL: + { + // add trigger predicate for equality and membership + d_equalityEngine->addTriggerPredicate(n); + } + break; case BAG_FROM_SET: case BAG_TO_SET: case BAG_IS_SINGLETON: @@ -300,7 +295,7 @@ void TheoryBags::preRegisterTerm(TNode n) ss << "Term of kind " << n.getKind() << " is not supported yet"; throw LogicException(ss.str()); } - default: break; + default: d_equalityEngine->addTerm(n); break; } } diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 196b4f01d..93449b637 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -152,6 +152,8 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) else if (kind == MATCH) { Trace("dt-rewrite-match") << "Rewrite match: " << in << std::endl; + // ensure we've type checked + TypeNode tin = in.getType(); Node h = in[0]; std::vector<Node> cases; std::vector<Node> rets; @@ -228,8 +230,9 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) std::reverse(cases.begin(), cases.end()); std::reverse(rets.begin(), rets.end()); Node ret = rets[0]; - AlwaysAssert(cases[0].isConst() || cases.size() == dt.getNumConstructors()); - for (unsigned i = 1, ncases = cases.size(); i < ncases; i++) + // notice that due to our type checker, either there is a variable pattern + // or all constructors are present in the match. + for (size_t i = 1, ncases = cases.size(); i < ncases; i++) { ret = nm->mkNode(ITE, cases[i], rets[i], ret); } diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp index 422af1731..7ce5c0df6 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.cpp +++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp @@ -398,67 +398,64 @@ TypeNode MatchTypeRule::computeType(NodeManager* nodeManager, for (unsigned i = 1, nchildren = n.getNumChildren(); i < nchildren; i++) { Node nc = n[i]; - if (check) + Kind nck = nc.getKind(); + std::unordered_set<Node> bvs; + if (nck == kind::MATCH_BIND_CASE) { - Kind nck = nc.getKind(); - std::unordered_set<Node> bvs; - if (nck == kind::MATCH_BIND_CASE) - { - for (const Node& v : nc[0]) - { - Assert(v.getKind() == kind::BOUND_VARIABLE); - bvs.insert(v); - } - } - else if (nck != kind::MATCH_CASE) + for (const Node& v : nc[0]) { - throw TypeCheckingExceptionPrivate( - n, "expected a match case in match expression"); + Assert(v.getKind() == kind::BOUND_VARIABLE); + bvs.insert(v); } - // get the pattern type - unsigned pindex = nck == kind::MATCH_CASE ? 0 : 1; - TypeNode patType = nc[pindex].getType(); - // should be caught in the above call - if (!patType.isDatatype()) - { - throw TypeCheckingExceptionPrivate( - n, "expecting datatype pattern in match"); - } - Kind ncpk = nc[pindex].getKind(); - if (ncpk == kind::APPLY_CONSTRUCTOR) + } + else if (nck != kind::MATCH_CASE) + { + throw TypeCheckingExceptionPrivate( + n, "expected a match case in match expression"); + } + // get the pattern type + uint32_t pindex = nck == kind::MATCH_CASE ? 0 : 1; + TypeNode patType = nc[pindex].getType(); + // should be caught in the above call + if (!patType.isDatatype()) + { + throw TypeCheckingExceptionPrivate( + n, "expecting datatype pattern in match"); + } + Kind ncpk = nc[pindex].getKind(); + if (ncpk == kind::APPLY_CONSTRUCTOR) + { + for (const Node& arg : nc[pindex]) { - for (const Node& arg : nc[pindex]) + if (bvs.find(arg) == bvs.end()) { - if (bvs.find(arg) == bvs.end()) - { - throw TypeCheckingExceptionPrivate( - n, - "expecting distinct bound variable as argument to " - "constructor in pattern of match"); - } - bvs.erase(arg); + throw TypeCheckingExceptionPrivate( + n, + "expecting distinct bound variable as argument to " + "constructor in pattern of match"); } - unsigned ci = utils::indexOf(nc[pindex].getOperator()); - patIndices.insert(ci); - } - else if (ncpk == kind::BOUND_VARIABLE) - { - patHasVariable = true; - } - else - { - throw TypeCheckingExceptionPrivate( - n, "unexpected kind of term in pattern in match"); - } - const DType& pdt = patType.getDType(); - // compare datatypes instead of the types to catch parametric case, - // where the pattern has parametric type. - if (hdt.getTypeNode() != pdt.getTypeNode()) - { - std::stringstream ss; - ss << "pattern of a match case does not match the head type in match"; - throw TypeCheckingExceptionPrivate(n, ss.str()); + bvs.erase(arg); } + size_t ci = utils::indexOf(nc[pindex].getOperator()); + patIndices.insert(ci); + } + else if (ncpk == kind::BOUND_VARIABLE) + { + patHasVariable = true; + } + else + { + throw TypeCheckingExceptionPrivate( + n, "unexpected kind of term in pattern in match"); + } + const DType& pdt = patType.getDType(); + // compare datatypes instead of the types to catch parametric case, + // where the pattern has parametric type. + if (hdt.getTypeNode() != pdt.getTypeNode()) + { + std::stringstream ss; + ss << "pattern of a match case does not match the head type in match"; + throw TypeCheckingExceptionPrivate(n, ss.str()); } TypeNode currType = nc.getType(check); if (i == 1) @@ -475,13 +472,11 @@ TypeNode MatchTypeRule::computeType(NodeManager* nodeManager, } } } - if (check) + // it is mandatory to check this here to ensure the match is exhaustive + if (!patHasVariable && patIndices.size() < hdt.getNumConstructors()) { - if (!patHasVariable && patIndices.size() < hdt.getNumConstructors()) - { - throw TypeCheckingExceptionPrivate( - n, "cases for match term are not exhaustive"); - } + throw TypeCheckingExceptionPrivate( + n, "cases for match term are not exhaustive"); } return retType; } diff --git a/src/theory/quantifiers/sygus/enum_value_manager.cpp b/src/theory/quantifiers/sygus/enum_value_manager.cpp index f91127dbe..7fbe1c3cd 100644 --- a/src/theory/quantifiers/sygus/enum_value_manager.cpp +++ b/src/theory/quantifiers/sygus/enum_value_manager.cpp @@ -23,6 +23,7 @@ #include "theory/quantifiers/sygus/enum_stream_substitution.h" #include "theory/quantifiers/sygus/sygus_enumerator.h" #include "theory/quantifiers/sygus/sygus_enumerator_basic.h" +#include "theory/quantifiers/sygus/sygus_random_enumerator.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_registry.h" @@ -94,6 +95,11 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete) { d_evg.reset(new EnumValGeneratorBasic(d_tds, e.getType())); } + else if (options().quantifiers.sygusActiveGenMode + == options::SygusActiveGenMode::RANDOM) + { + d_evg.reset(new SygusRandomEnumerator(d_tds)); + } else { Assert(options().quantifiers.sygusActiveGenMode diff --git a/src/theory/quantifiers/sygus/sygus_random_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_random_enumerator.cpp new file mode 100644 index 000000000..bf051a897 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_random_enumerator.cpp @@ -0,0 +1,199 @@ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed, 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 sygus random enumerator. + */ + +#include "theory/quantifiers/sygus/sygus_random_enumerator.h" + +#include "expr/dtype_cons.h" +#include "expr/skolem_manager.h" +#include "options/quantifiers_options.h" +#include "theory/datatypes/sygus_datatype_utils.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/rewriter.h" +#include "util/random.h" + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +void SygusRandomEnumerator::initialize(Node e) +{ + d_tn = e.getType(); + Assert(d_tn.isDatatype()); + Assert(d_tn.getDType().isSygus()); + SygusTypeInfo sti; + sti.initialize(d_tds, d_tn); + std::vector<TypeNode> stns; + sti.getSubfieldTypes(stns); + // We will be using the datatype constructors a lot, so we cache them here. + for (const TypeNode& stn : stns) + { + for (const std::shared_ptr<DTypeConstructor>& cons : + stn.getDType().getConstructors()) + { + if (cons->getNumArgs() == 0) + { + d_noArgCons[stn].push_back(cons); + } + else + { + d_argCons[stn].push_back(cons); + } + } + } +} + +bool SygusRandomEnumerator::increment() +{ + Node n, bn; + do + { + // Generate the next sygus term. + n = incrementH(); + bn = d_tds->sygusToBuiltin(n); + bn = Rewriter::callExtendedRewrite(bn); + // Ensure that the builtin counterpart is unique (up to rewriting). + } while (d_cache.find(bn) != d_cache.cend()); + d_cache.insert(bn); + d_currTerm = n; + return true; +} + +Node SygusRandomEnumerator::incrementH() +{ + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); + Random& rnd = Random::getRandom(); + double p = options::sygusActiveGenRandomP(); + + Node mainSkolem = sm->mkDummySkolem("sygus_rand", d_tn); + // List of skolems with no corresponding constructor. + std::vector<Node> remainingSkolems; + remainingSkolems.push_back(mainSkolem); + // List of terms with corresponding constructors. We do not immediately + // construct sygus terms (possibly containing holes) for those skolems. + // Instead, we wait until we are done picking constructors for all skolems. We + // do so to immediately construct ground terms for all of them following their + // order in this stack. + std::vector<Node> stack; + // Constructors corresponding to each skolem. + std::unordered_map<Node, std::shared_ptr<DTypeConstructor>> skolemCons; + // Ground terms corresponding to each skolem. + std::unordered_map<Node, Node> groundTerm; + // Sub-skolems needed for skolems with constructors that take arguments. + std::unordered_map<Node, std::vector<Node>> subSkolems; + + // We stop when we get a tails or there are no more skolems to process. + while (rnd.pickWithProb(p) && !remainingSkolems.empty()) + { + // Pick a random skolem from the remaining ones and remove it from the list. + size_t r = rnd() % remainingSkolems.size(); + Node currSkolem = remainingSkolems[r]; + remainingSkolems.erase(remainingSkolems.cbegin() + r); + // Add the picked skolem to stack for later processing. + TypeNode currSkolemType = currSkolem.getType(); + // If the type current skolem is not a subfield type of `d_tn`, we replace + // it with a ground value of its type. + if (d_argCons[currSkolemType].empty() + && d_noArgCons[currSkolemType].empty()) + { + groundTerm[currSkolem] = nm->mkGroundValue(currSkolemType); + continue; + } + stack.push_back(currSkolem); + // Pick a random constructor that takes arguments for this skolem. If there + // is none, pick a random no-argument constructor. + skolemCons[currSkolem] = + d_argCons[currSkolemType].empty() + ? d_noArgCons[currSkolemType] + [rnd() % d_noArgCons[currSkolemType].size()] + : d_argCons[currSkolemType] + [rnd() % d_argCons[currSkolemType].size()]; + // Create a sub-skolem for each constructor argument and add them to the + // list of remaining skolems. + for (size_t i = 0, n = skolemCons[currSkolem]->getNumArgs(); i < n; ++i) + { + TypeNode subSkolemType = skolemCons[currSkolem]->getArgType(i); + Node subSkolem = sm->mkDummySkolem("sygus_rand", subSkolemType); + remainingSkolems.push_back(subSkolem); + subSkolems[currSkolem].push_back(subSkolem); + } + } + + // If we get a tail, we need to pick no-argument constructors for the + // remaining skolems. If all constructors take arguments, we use the ground + // value for the skolems' sygus datatype type. + for (Node skolem : remainingSkolems) + { + TypeNode skolemType = skolem.getType(); + if (d_noArgCons[skolemType].empty()) + { + groundTerm[skolem] = nm->mkGroundValue(skolemType); + } + else + { + skolemCons[skolem] = + d_noArgCons[skolemType][rnd() % d_noArgCons[skolemType].size()]; + stack.push_back(skolem); + } + } + + // Build up ground values starting from leaf skolems up to the root/main + // skolem. + while (!stack.empty()) + { + Node currSkolem = stack.back(); + stack.pop_back(); + std::vector<Node> args; + args.push_back(skolemCons[currSkolem]->getConstructor()); + for (Node subSkolem : subSkolems[currSkolem]) + { + args.push_back(groundTerm[subSkolem]); + } + // We may have already generated a sygus term equivalent to the one we are + // generating now. In that case, pick the smaller term of the two. This + // operation allows us to generate more refined terms over time. + groundTerm[currSkolem] = getMin(nm->mkNode(kind::APPLY_CONSTRUCTOR, args)); + } + + return groundTerm[mainSkolem]; +} + +Node SygusRandomEnumerator::getMin(Node n) +{ + TypeNode tn = n.getType(); + Node bn = d_tds->sygusToBuiltin(n); + bn = Rewriter::callExtendedRewrite(bn); + // Did we calculate the size of `n` before? + if (d_size.find(n) == d_size.cend()) + { + // If not, calculate its size and cache it. + d_size[n] = datatypes::utils::getSygusTermSize(n); + } + // Did we come across an equivalent term before? If so, is the equivalent term + // smaller than `n`? + if (d_minSygus[tn][bn].isNull() || d_size[n] < d_size[d_minSygus[tn][bn]]) + { + d_minSygus[tn][bn] = n; + } + else + { + n = d_minSygus[tn][bn]; + } + return n; +} + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_random_enumerator.h b/src/theory/quantifiers/sygus/sygus_random_enumerator.h new file mode 100644 index 000000000..b70fe9490 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_random_enumerator.h @@ -0,0 +1,129 @@ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed, 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. + * **************************************************************************** + * + * Random sygus enumerator class. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_RANDOM_ENUMERATOR_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_RANDOM_ENUMERATOR_H + +#include <unordered_set> + +#include "expr/node.h" +#include "expr/type_node.h" +#include "theory/quantifiers/sygus/enum_val_generator.h" + +namespace cvc5 { + +class DTypeConstructor; + +namespace theory { +namespace quantifiers { + +class TermDbSygus; + +using TypeConsMap = + std::unordered_map<TypeNode, + std::vector<std::shared_ptr<DTypeConstructor>>>; + +/** A random sygus value generator. + * + * This class is a random term generator for sygus conjectures. The sizes of the + * generated terms approximate a geometric distribution with an expected size of + * 1 / p, where p is a parameter specified by the user (defaults to 0.5). + */ +class SygusRandomEnumerator : public EnumValGenerator +{ + public: + /** Constructor. Initializes the enumerator. + * + * @param tds pointer to term database sygus. + */ + SygusRandomEnumerator(TermDbSygus* tds) : d_tds(tds){}; + + /** Initialize this class with enumerator `e`. */ + void initialize(Node e) override; + + /** Inform this generator that abstract value `v` was enumerated. */ + void addValue(Node v) override { d_cache.insert(v); } + + /** + * Get next the next random (T-rewriter-unique) value. + * + * @return true if a new value is found and loop otherwise. + */ + bool increment() override; + + /** @return the current term. */ + Node getCurrent() override { return d_currTerm; } + + private: + /** Generates a random sygus term. + * + * S ::= 0 | x | (+ S S) + * + * Assuming we are provided the above grammar, we generate random terms by + * starting with a skolem, `z0`, of the given sygus datatype type (grammar + * non-terminal). We then flip a coin to determine whether or not we should + * replace the skolem with a random constructor that takes arguments (`(+ S + * S)` above). For example, if the first 2 coin flips are heads, then we will + * replace `z0` with `(+ z1 z2)` and either `z1` or `z2` (randomly chosen) + * with `(+ z3 z4)`. So, we will end up with either `(+ (+ z3 z4) z2)` or `(+ + * z1 (+ z3 z4))`. We keep doing so until we get a tails. At which point, we + * replace all remaining skolems with random no-argument constructors (`0` and + * `x` above) and return the resulting sygus term. So, if we get a tails at + * the third flip in the previous example, then `incrementH` may return `(+ 1 + * (+ x x))`, `(+ (+ 1 1) 1)`, or any of the other 14 possible terms. + * + * \note If a skolem's datatype type does not have a no-argument constructor, + * it is replaced with a ground value using `mkGroundValue` utility. + * \note If a skolem's datatype type does not have a constructor that takes an + * argument (e.g., `S ::= 0 | 1 | x | (+ 2 y)`), it is replaced with a random + * no-argument constructor. So `incrementH` may return a term before getting a + * tails. + * + * @return a randomly generated sygus term. + */ + Node incrementH(); + + /** + * Returns smallest (in terms of size) term equivalent (up to rewriting) to + * the given sygus term. + */ + Node getMin(Node n); + + /** Pointer to term database sygus. */ + TermDbSygus* d_tds; + /** The type to enumerate. */ + TypeNode d_tn; + /** The current term. */ + Node d_currTerm; + /** Cache of no-argument constructors for each sygus datatype type. */ + TypeConsMap d_noArgCons; + /** Cache of argument constructors for each sygus datatype type. */ + TypeConsMap d_argCons; + /** Cache of builtin terms we have enumerated so far. */ + std::unordered_set<Node> d_cache; + /** Cache of smallest (in terms of size) term equivalent (up to rewriting) + * to the given sygus term, per sygus datatatype type. */ + std::unordered_map<TypeNode, std::unordered_map<Node, Node>> d_minSygus; + /** Cache of the size of a sygus term. */ + std::unordered_map<Node, unsigned> d_size; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 + +#endif // CVC5__THEORY__QUANTIFIERS__SYGUS_RANDOM_ENUMERATOR_H diff --git a/src/theory/strings/array_core_solver.cpp b/src/theory/strings/array_core_solver.cpp index 3b8fdeff4..9e3921e29 100644 --- a/src/theory/strings/array_core_solver.cpp +++ b/src/theory/strings/array_core_solver.cpp @@ -116,7 +116,6 @@ void ArrayCoreSolver::checkUpdate(const std::vector<Node>& updateTerms) Node left = nm->mkNode(SEQ_NTH, termProxy, n[1]); Node right = nm->mkNode(SEQ_NTH, n[2], nm->mkConstInt(Rational(0))); // n[2][0] - right = Rewriter::rewrite(right); Node lem = nm->mkNode(EQUAL, left, right); Trace("seq-array-debug") << "enter" << std::endl; sendInference(exp, lem, InferenceId::STRINGS_ARRAY_NTH_UPDATE); diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 2d25a0d1e..f5864bdd3 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -32,8 +32,11 @@ namespace cvc5 { namespace theory { namespace strings { -BaseSolver::BaseSolver(Env& env, SolverState& s, InferenceManager& im) - : EnvObj(env), d_state(s), d_im(im), d_congruent(context()) +BaseSolver::BaseSolver(Env& env, + SolverState& s, + InferenceManager& im, + TermRegistry& tr) + : EnvObj(env), d_state(s), d_im(im), d_termReg(tr), d_congruent(context()) { d_false = NodeManager::currentNM()->mkConst(false); d_cardSize = options().strings.stringsAlphaCard; @@ -344,7 +347,7 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti, Node c; if (isConst) { - c = utils::mkNConcat(vecc, n.getType()); + c = d_termReg.mkNConcat(vecc, n.getType()); } if (!isConst || !d_state.areEqual(n, c)) { @@ -421,7 +424,7 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti, { // The equivalence class is not entailed to be equal to a constant // and we found a better concatenation - Node nct = utils::mkNConcat(vecnc, n.getType()); + Node nct = d_termReg.mkNConcat(vecnc, n.getType()); Assert(!nct.isConst()); bei.d_bestContent = nct; bei.d_bestScore = contentSize; diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h index 96d275cd5..d4b0ebe0d 100644 --- a/src/theory/strings/base_solver.h +++ b/src/theory/strings/base_solver.h @@ -44,7 +44,7 @@ class BaseSolver : protected EnvObj using NodeSet = context::CDHashSet<Node>; public: - BaseSolver(Env& env, SolverState& s, InferenceManager& im); + BaseSolver(Env& env, SolverState& s, InferenceManager& im, TermRegistry& tr); ~BaseSolver(); //-----------------------inference steps @@ -217,6 +217,8 @@ class BaseSolver : protected EnvObj SolverState& d_state; /** The (custom) output channel of the theory of strings */ InferenceManager& d_im; + /** Reference to the term registry of theory of strings */ + TermRegistry& d_termReg; /** Commonly used constants */ Node d_emptyString; Node d_false; diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index ab214c9ce..868e855ab 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -562,7 +562,7 @@ void CoreSolver::checkNormalFormsEq() return; } NormalForm& nfe = getNormalForm(eqc); - Node nf_term = utils::mkNConcat(nfe.d_nf, stype); + Node nf_term = d_termReg.mkNConcat(nfe.d_nf, stype); std::map<Node, Node>::iterator itn = nf_to_eqc.find(nf_term); if (itn != nf_to_eqc.end()) { @@ -690,7 +690,7 @@ Node CoreSolver::getNormalString(Node x, std::vector<Node>& nf_exp) if (it != d_normal_form.end()) { NormalForm& nf = it->second; - Node ret = utils::mkNConcat(nf.d_nf, stype); + Node ret = d_termReg.mkNConcat(nf.d_nf, stype); nf_exp.insert(nf_exp.end(), nf.d_exp.begin(), nf.d_exp.end()); d_im.addToExplanation(x, nf.d_base, nf_exp); Trace("strings-debug") @@ -708,7 +708,7 @@ Node CoreSolver::getNormalString(Node x, std::vector<Node>& nf_exp) Node nc = getNormalString(x[i], nf_exp); vec_nodes.push_back(nc); } - return utils::mkNConcat(vec_nodes, stype); + return d_termReg.mkNConcat(vec_nodes, stype); } } return x; @@ -1090,7 +1090,7 @@ void CoreSolver::processNEqc(Node eqc, for (size_t i = 0, nnforms = normal_forms.size(); i < nnforms; i++) { NormalForm& nfi = normal_forms[i]; - Node ni = utils::mkNConcat(nfi.d_nf, stype); + Node ni = d_termReg.mkNConcat(nfi.d_nf, stype); if (nfCache.find(ni) == nfCache.end()) { // If the equivalence class is entailed to be constant, check @@ -1369,7 +1369,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, eqnc.push_back(nfkv[i]); } } - eqn[r] = utils::mkNConcat(eqnc, stype); + eqn[r] = d_termReg.mkNConcat(eqnc, stype); } Trace("strings-solve-debug") << "Endpoint eq check: " << eqn[0] << " " << eqn[1] << std::endl; @@ -1805,15 +1805,15 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, Trace("strings-loop") << " ... (X)= " << vecoi[index] << std::endl; Trace("strings-loop") << " ... T(Y.Z)= "; std::vector<Node> vec_t(veci.begin() + index, veci.begin() + loop_index); - Node t_yz = utils::mkNConcat(vec_t, stype); + Node t_yz = d_termReg.mkNConcat(vec_t, stype); Trace("strings-loop") << " (" << t_yz << ")" << std::endl; Trace("strings-loop") << " ... S(Z.Y)= "; std::vector<Node> vec_s(vecoi.begin() + index + 1, vecoi.end()); - Node s_zy = utils::mkNConcat(vec_s, stype); + Node s_zy = d_termReg.mkNConcat(vec_s, stype); Trace("strings-loop") << s_zy << std::endl; Trace("strings-loop") << " ... R= "; std::vector<Node> vec_r(veci.begin() + loop_index + 1, veci.end()); - Node r = utils::mkNConcat(vec_r, stype); + Node r = d_termReg.mkNConcat(vec_r, stype); Trace("strings-loop") << r << std::endl; Node emp = Word::mkEmptyWord(stype); @@ -1907,12 +1907,12 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, std::vector<Node> v2(vec_r); v2.insert(v2.begin(), y); v2.insert(v2.begin(), z); - restr = utils::mkNConcat(z, y); - cc = rewrite(s_zy.eqNode(utils::mkNConcat(v2, stype))); + restr = d_termReg.mkNConcat(z, y); + cc = rewrite(s_zy.eqNode(d_termReg.mkNConcat(v2, stype))); } else { - cc = rewrite(s_zy.eqNode(utils::mkNConcat(z, y))); + cc = rewrite(s_zy.eqNode(d_termReg.mkNConcat(z, y))); } if (cc == d_false) { @@ -1955,13 +1955,13 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, iinfo.d_skolems[LENGTH_GEQ_ONE].push_back(sk_y); Node sk_z = skc->mkSkolem("z_loop"); // t1 * ... * tn = y * z - Node conc1 = t_yz.eqNode(utils::mkNConcat(sk_y, sk_z)); + Node conc1 = t_yz.eqNode(d_termReg.mkNConcat(sk_y, sk_z)); // s1 * ... * sk = z * y * r vec_r.insert(vec_r.begin(), sk_y); vec_r.insert(vec_r.begin(), sk_z); - Node conc2 = s_zy.eqNode(utils::mkNConcat(vec_r, stype)); - Node conc3 = vecoi[index].eqNode(utils::mkNConcat(sk_y, sk_w)); - Node restr = r == emp ? s_zy : utils::mkNConcat(sk_z, sk_y); + Node conc2 = s_zy.eqNode(d_termReg.mkNConcat(vec_r, stype)); + Node conc3 = vecoi[index].eqNode(d_termReg.mkNConcat(sk_y, sk_w)); + Node restr = r == emp ? s_zy : d_termReg.mkNConcat(sk_z, sk_y); str_in_re = nm->mkNode(kind::STRING_IN_REGEXP, sk_w, @@ -2653,7 +2653,7 @@ void CoreSolver::checkLengthsEqc() { // now, check if length normalization has occurred if (ei->d_normalizedLength.get().isNull()) { - Node nf = utils::mkNConcat(nfi.d_nf, stype); + Node nf = d_termReg.mkNConcat(nfi.d_nf, stype); if (Trace.isOn("strings-process-debug")) { Trace("strings-process-debug") diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index 477533bee..a638d6009 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -21,6 +21,7 @@ #include "theory/rewriter.h" #include "theory/strings/regexp_entail.h" #include "theory/strings/theory_strings_utils.h" +#include "theory/strings/word.h" #include "util/rational.h" #include "util/string.h" @@ -173,7 +174,6 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) conc.push_back(currMem); } currEnd = nm->mkNode(PLUS, currEnd, childLengths[i]); - currEnd = Rewriter::rewrite(currEnd); } } Node res = nm->mkNode(AND, conc); @@ -560,7 +560,6 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg) Node index = bvm->mkBoundVar<ReElimStarIndexAttribute>(atom, intType); Node substr_ch = nm->mkNode(STRING_SUBSTR, x, index, nm->mkConstInt(Rational(1))); - substr_ch = Rewriter::rewrite(substr_ch); // handle the case where it is purely characters for (const Node& r : disj) { @@ -588,8 +587,6 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg) else { Node regexp_ch = nm->mkNode(STRING_IN_REGEXP, substr_ch, r); - regexp_ch = Rewriter::rewrite(regexp_ch); - Assert(regexp_ch.getKind() != STRING_IN_REGEXP); char_constraints.push_back(regexp_ch); } } @@ -617,9 +614,7 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg) Node s = r[0]; if (s.isConst()) { - Node lens = nm->mkNode(STRING_LENGTH, s); - lens = Rewriter::rewrite(lens); - Assert(lens.isConst()); + Node lens = nm->mkConstInt(Word::getLength(s)); Assert(lens.getConst<Rational>().sgn() > 0); std::vector<Node> conj; // lens is a positive constant, so it is safe to use total div/mod here. diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp index aa69f9ecf..c2ee079db 100644 --- a/src/theory/strings/regexp_entail.cpp +++ b/src/theory/strings/regexp_entail.cpp @@ -28,7 +28,7 @@ namespace cvc5 { namespace theory { namespace strings { -RegExpEntail::RegExpEntail(Rewriter* r) : d_rewriter(r), d_aent(r) +RegExpEntail::RegExpEntail(Rewriter* r) : d_aent(r) { d_zero = NodeManager::currentNM()->mkConstInt(Rational(0)); d_one = NodeManager::currentNM()->mkConstInt(Rational(1)); @@ -659,11 +659,9 @@ Node RegExpEntail::getFixedLengthForRegexp(TNode n) Kind k = n.getKind(); if (k == STRING_TO_REGEXP) { - Node ret = nm->mkNode(STRING_LENGTH, n[0]); - ret = Rewriter::rewrite(ret); - if (ret.isConst()) + if (n[0].isConst()) { - return ret; + return nm->mkConstInt(Rational(Word::getLength(n[0]))); } } else if (k == REGEXP_ALLCHAR || k == REGEXP_RANGE) @@ -690,7 +688,7 @@ Node RegExpEntail::getFixedLengthForRegexp(TNode n) } else if (k == REGEXP_CONCAT) { - NodeBuilder nb(PLUS); + Rational sum(0); for (const Node& nc : n) { Node flc = getFixedLengthForRegexp(nc); @@ -698,11 +696,10 @@ Node RegExpEntail::getFixedLengthForRegexp(TNode n) { return flc; } - nb << flc; + Assert(flc.isConst() && flc.getType().isInteger()); + sum += flc.getConst<Rational>(); } - Node ret = nb.constructNode(); - ret = Rewriter::rewrite(ret); - return ret; + return nm->mkConstInt(sum); } return Node::null(); } @@ -785,8 +782,6 @@ Node RegExpEntail::getConstantBoundLengthForRegexp(TNode n, bool isLower) const bool RegExpEntail::regExpIncludes(Node r1, Node r2) { - Assert(Rewriter::rewrite(r1) == r1); - Assert(Rewriter::rewrite(r2) == r2); if (r1 == r2) { return true; diff --git a/src/theory/strings/regexp_entail.h b/src/theory/strings/regexp_entail.h index b0511bd53..62cb5a725 100644 --- a/src/theory/strings/regexp_entail.h +++ b/src/theory/strings/regexp_entail.h @@ -146,8 +146,6 @@ class RegExpEntail * computed. Used for getConstantBoundLengthForRegexp. */ static bool getConstantBoundCache(TNode n, bool isLower, Node& c); - /** The underlying rewriter */ - Rewriter* d_rewriter; /** Arithmetic entailment module */ ArithEntail d_aent; /** Common constants */ diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 24ce64842..9a13aeab3 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -115,7 +115,7 @@ bool RegExpSolver::checkInclInter( std::vector<Node> mems2 = mr.second; Trace("regexp-process") << "Memberships(" << mr.first << ") = " << mr.second << std::endl; - if (!checkEqcInclusion(mems2)) + if (options().strings.stringRegexpInclusion && !checkEqcInclusion(mems2)) { // conflict discovered, return return true; diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 634f27294..aadca9904 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -40,6 +40,7 @@ namespace strings { SequencesRewriter::SequencesRewriter(Rewriter* r, HistogramStat<Rewrite>* statistics) : d_statistics(statistics), + d_rr(r), d_arithEntail(r), d_stringsEntail(r, d_arithEntail, *this) { @@ -135,7 +136,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) Node len0 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[0]); Node len1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]); Node len_eq = len0.eqNode(len1); - len_eq = Rewriter::rewrite(len_eq); + len_eq = d_rr->rewrite(len_eq); if (len_eq.isConst() && !len_eq.getConst<bool>()) { return returnRewrite(node, len_eq, Rewrite::EQ_LEN_DEQ); @@ -406,7 +407,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) // (= x (str.replace x "A" "B")) ---> (not (str.contains x "A")) if (x == repl[0]) { - Node eq = Rewriter::rewrite(nm->mkNode(EQUAL, repl[1], repl[2])); + Node eq = rewriteEquality(nm->mkNode(EQUAL, repl[1], repl[2])); if (eq.isConst() && !eq.getConst<bool>()) { Node ret = nm->mkNode(NOT, nm->mkNode(STRING_CONTAINS, x, repl[1])); @@ -614,9 +615,9 @@ Node SequencesRewriter::rewriteLength(Node node) } else if (nk0 == STRING_REPLACE || nk0 == STRING_REPLACE_ALL) { - Node len1 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][1])); - Node len2 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][2])); - if (len1 == len2) + Node len1 = nm->mkNode(STRING_LENGTH, node[0][1]); + Node len2 = nm->mkNode(STRING_LENGTH, node[0][2]); + if (d_arithEntail.checkEq(len1, len2)) { // len( y ) == len( z ) => len( str.replace( x, y, z ) ) ---> len( x ) Node retNode = nm->mkNode(STRING_LENGTH, node[0][0]); @@ -2555,7 +2556,7 @@ Node SequencesRewriter::rewriteIndexof(Node node) if (!node[2].isConst() || node[2].getConst<Rational>().sgn() != 0) { fstr = nm->mkNode(kind::STRING_SUBSTR, node[0], node[2], len0); - fstr = Rewriter::rewrite(fstr); + fstr = d_rr->rewrite(fstr); } Node cmp_conr = d_stringsEntail.checkContains(fstr, node[1]); @@ -2801,8 +2802,8 @@ Node SequencesRewriter::rewriteReplace(Node node) if (d_stringsEntail.checkLengthOne(node[0])) { Node empty = Word::mkEmptyWord(stype); - Node rn1 = Rewriter::rewrite( - rewriteEqualityExt(nm->mkNode(EQUAL, node[1], empty))); + Node rn1 = + d_rr->rewrite(rewriteEqualityExt(nm->mkNode(EQUAL, node[1], empty))); if (rn1 != node[1]) { std::vector<Node> emptyNodes; @@ -2827,7 +2828,7 @@ Node SequencesRewriter::rewriteReplace(Node node) // check if contains definitely does (or does not) hold Node cmp_con = nm->mkNode(kind::STRING_CONTAINS, node[0], node[1]); - Node cmp_conr = Rewriter::rewrite(cmp_con); + Node cmp_conr = d_rr->rewrite(cmp_con); if (cmp_conr.isConst()) { if (cmp_conr.getConst<bool>()) @@ -3033,8 +3034,7 @@ Node SequencesRewriter::rewriteReplace(Node node) if (d_arithEntail.check(wlen, zlen)) { // w != z - Node wEqZ = Rewriter::rewrite(nm->mkNode(kind::EQUAL, w, z)); - if (wEqZ.isConst() && !wEqZ.getConst<bool>()) + if (w != z && w.isConst() && z.isConst()) { Node ret = nm->mkNode(kind::STRING_REPLACE, nm->mkNode(kind::STRING_REPLACE, y, w, z), @@ -3346,7 +3346,7 @@ Node SequencesRewriter::rewriteReplaceReAll(Node node) // "Z" ++ y ++ "Z" ++ y TypeNode t = x.getType(); Node emp = Word::mkEmptyWord(t); - Node yp = Rewriter::rewrite( + Node yp = d_rr->rewrite( nm->mkNode(REGEXP_DIFF, y, nm->mkNode(STRING_TO_REGEXP, emp))); std::vector<Node> res; String rem = x.getConst<String>(); @@ -3524,7 +3524,7 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n) Node SequencesRewriter::lengthPreserveRewrite(Node n) { NodeManager* nm = NodeManager::currentNM(); - Node len = Rewriter::rewrite(nm->mkNode(kind::STRING_LENGTH, n)); + Node len = d_rr->rewrite(nm->mkNode(kind::STRING_LENGTH, n)); Node res = canonicalStrForSymbolicLength(len, n.getType()); return res.isNull() ? n : res; } diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h index 854e3fb81..850acfb2a 100644 --- a/src/theory/strings/sequences_rewriter.h +++ b/src/theory/strings/sequences_rewriter.h @@ -284,7 +284,7 @@ class SequencesRewriter : public TheoryRewriter * We apply certain normalizations to n', such as replacing all constants * that are not relevant to length by "A". */ - static Node lengthPreserveRewrite(Node n); + Node lengthPreserveRewrite(Node n); /** * Given a symbolic length n, returns the canonical string (of type stype) @@ -305,6 +305,11 @@ class SequencesRewriter : public TheoryRewriter Node postProcessRewrite(Node node, Node ret); /** Reference to the rewriter statistics. */ HistogramStat<Rewrite>* d_statistics; + /** + * Pointer to the rewriter. NOTE this is a cyclic dependency, and should + * be removed. + */ + Rewriter* d_rr; /** The arithmetic entailment module */ ArithEntail d_arithEntail; /** Instance of the entailment checker for strings. */ diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index 6b7fc699b..96e143244 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -77,7 +77,8 @@ TheoryModel* SolverState::getModel() { return d_valuation.getModel(); } Node SolverState::getLengthExp(Node t, std::vector<Node>& exp, Node te) { Assert(areEqual(t, te)); - Node lt = utils::mkNLength(te); + Node lt = NodeManager::currentNM()->mkNode(STRING_LENGTH, t); + lt = rewrite(lt); if (hasTerm(lt)) { // use own length if it exists, leads to shorter explanation @@ -116,7 +117,8 @@ Node SolverState::explainNonEmpty(Node s) { return s.eqNode(emp).negate(); } - Node sLen = utils::mkNLength(s); + Node sLen = NodeManager::currentNM()->mkNode(STRING_LENGTH, s); + sLen = rewrite(sLen); if (areDisequal(sLen, d_zero)) { return sLen.eqNode(d_zero).negate(); diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index d2d723276..85ec680ac 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -81,7 +81,8 @@ Node TermRegistry::eagerReduce(Node t, SkolemCache* sc, uint32_t alphaCard) if (tk == STRING_TO_CODE) { // ite( str.len(s)==1, 0 <= str.code(s) < |A|, str.code(s)=-1 ) - Node code_len = utils::mkNLength(t[0]).eqNode(nm->mkConstInt(Rational(1))); + Node len = nm->mkNode(STRING_LENGTH, t[0]); + Node code_len = len.eqNode(nm->mkConstInt(Rational(1))); Node code_eq_neg1 = t.eqNode(nm->mkConstInt(Rational(-1))); Node code_range = nm->mkNode(AND, @@ -115,7 +116,7 @@ Node TermRegistry::eagerReduce(Node t, SkolemCache* sc, uint32_t alphaCard) sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_PRE, "sc1"); Node sk2 = sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_POST, "sc2"); - lemma = t[0].eqNode(utils::mkNConcat(sk1, t[1], sk2)); + lemma = t[0].eqNode(nm->mkNode(STRING_CONCAT, sk1, t[1], sk2)); lemma = nm->mkNode(ITE, t, lemma, t[0].eqNode(t[1]).notNode()); } return lemma; @@ -669,6 +670,21 @@ void TermRegistry::removeProxyEqs(Node n, std::vector<Node>& unproc) const } } +Node TermRegistry::mkNConcat(Node n1, Node n2) const +{ + return rewrite(NodeManager::currentNM()->mkNode(STRING_CONCAT, n1, n2)); +} + +Node TermRegistry::mkNConcat(Node n1, Node n2, Node n3) const +{ + return rewrite(NodeManager::currentNM()->mkNode(STRING_CONCAT, n1, n2, n3)); +} + +Node TermRegistry::mkNConcat(const std::vector<Node>& c, TypeNode tn) const +{ + return rewrite(utils::mkConcat(c, tn)); +} + } // namespace strings } // namespace theory } // namespace cvc5 diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h index 1de5def9e..338e528fe 100644 --- a/src/theory/strings/term_registry.h +++ b/src/theory/strings/term_registry.h @@ -213,6 +213,22 @@ class TermRegistry : protected EnvObj */ void removeProxyEqs(Node n, std::vector<Node>& unproc) const; //---------------------------- end proxy variables + /** + * Returns the rewritten form of the string concatenation of n1 and n2. + */ + Node mkNConcat(Node n1, Node n2) const; + + /** + * Returns the rewritten form of the string concatenation of n1, n2 and n3. + */ + Node mkNConcat(Node n1, Node n2, Node n3) const; + + /** + * Returns the rewritten form of the concatentation from vector c of + * (string-like) type tn. + */ + Node mkNConcat(const std::vector<Node>& c, TypeNode tn) const; + private: /** Common constants */ Node d_zero; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 8b496b725..ee068fe16 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -59,13 +59,15 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) d_rewriter(env.getRewriter(), &d_statistics.d_rewrites, d_termReg.getAlphabetCardinality()), - d_eagerSolver(env, d_state, d_termReg), + d_eagerSolver(options().strings.stringEagerSolver + ? new EagerSolver(env, d_state, d_termReg) + : nullptr), d_extTheoryCb(), d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics), d_extTheory(env, d_extTheoryCb, d_im), // the checker depends on the cardinality of the alphabet d_checker(d_termReg.getAlphabetCardinality()), - d_bsolver(env, d_state, d_im), + d_bsolver(env, d_state, d_im, d_termReg), d_csolver(env, d_state, d_im, d_termReg, d_bsolver), d_esolver(env, d_state, @@ -588,7 +590,7 @@ bool TheoryStrings::collectModelInfoType( Assert(r.isConst() || processed.find(r) != processed.end()); nc.push_back(r.isConst() ? r : processed[r]); } - Node cc = utils::mkNConcat(nc, tn); + Node cc = d_termReg.mkNConcat(nc, tn); Trace("strings-model") << "*** Determined constant " << cc << " for " << rn << std::endl; processed[rn] = cc; @@ -651,7 +653,10 @@ void TheoryStrings::notifyFact(TNode atom, TNode fact, bool isInternal) { - d_eagerSolver.notifyFact(atom, polarity, fact, isInternal); + if (d_eagerSolver) + { + d_eagerSolver->notifyFact(atom, polarity, fact, isInternal); + } // process pending conflicts due to reasoning about endpoints if (!d_state.isInConflict() && d_state.hasPendingConflict()) { @@ -769,7 +774,10 @@ void TheoryStrings::eqNotifyNewClass(TNode t){ ei->d_codeTerm = t[0]; } } - d_eagerSolver.eqNotifyNewClass(t); + if (d_eagerSolver) + { + d_eagerSolver->eqNotifyNewClass(t); + } } void TheoryStrings::eqNotifyMerge(TNode t1, TNode t2) @@ -782,7 +790,10 @@ void TheoryStrings::eqNotifyMerge(TNode t1, TNode t2) // always create it if e2 was non-null EqcInfo* e1 = d_state.getOrMakeEqcInfo(t1); - d_eagerSolver.eqNotifyMerge(e1, t1, e2, t2); + if (d_eagerSolver) + { + d_eagerSolver->eqNotifyMerge(e1, t1, e2, t2); + } // add information from e2 to e1 if (!e2->d_lengthTerm.get().isNull()) @@ -1046,7 +1057,7 @@ void TheoryStrings::checkRegisterTermsNormalForms() Node lt = ei ? ei->d_lengthTerm : Node::null(); if (lt.isNull()) { - Node c = utils::mkNConcat(nfi.d_nf, eqc.getType()); + Node c = d_termReg.mkNConcat(nfi.d_nf, eqc.getType()); d_termReg.registerTerm(c, 3); } } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 21db7da0c..dd15e08ec 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -259,7 +259,7 @@ class TheoryStrings : public Theory { /** The theory rewriter for this theory. */ StringsRewriter d_rewriter; /** The eager solver */ - EagerSolver d_eagerSolver; + std::unique_ptr<EagerSolver> d_eagerSolver; /** The extended theory callback */ StringsExtfCallback d_extTheoryCb; /** The (custom) output channel of the theory of strings */ diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index 0ee2e906d..abac46d37 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -140,28 +140,6 @@ Node mkConcat(const std::vector<Node>& c, TypeNode tn) return NodeManager::currentNM()->mkNode(k, c); } -Node mkNConcat(Node n1, Node n2) -{ - return Rewriter::rewrite( - NodeManager::currentNM()->mkNode(STRING_CONCAT, n1, n2)); -} - -Node mkNConcat(Node n1, Node n2, Node n3) -{ - return Rewriter::rewrite( - NodeManager::currentNM()->mkNode(STRING_CONCAT, n1, n2, n3)); -} - -Node mkNConcat(const std::vector<Node>& c, TypeNode tn) -{ - return Rewriter::rewrite(mkConcat(c, tn)); -} - -Node mkNLength(Node t) -{ - return Rewriter::rewrite(NodeManager::currentNM()->mkNode(STRING_LENGTH, t)); -} - Node mkPrefix(Node t, Node n) { NodeManager* nm = NodeManager::currentNM(); diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h index 0cfcd64d0..f97391df8 100644 --- a/src/theory/strings/theory_strings_utils.h +++ b/src/theory/strings/theory_strings_utils.h @@ -61,27 +61,6 @@ void getConcat(Node n, std::vector<Node>& c); Node mkConcat(const std::vector<Node>& c, TypeNode tn); /** - * Returns the rewritten form of the string concatenation of n1 and n2. - */ -Node mkNConcat(Node n1, Node n2); - -/** - * Returns the rewritten form of the string concatenation of n1, n2 and n3. - */ -Node mkNConcat(Node n1, Node n2, Node n3); - -/** - * Returns the rewritten form of the concatentation from vector c of - * (string-like) type tn. - */ -Node mkNConcat(const std::vector<Node>& c, TypeNode tn); - -/** - * Returns the rewritten form of the length of string term t. - */ -Node mkNLength(Node t); - -/** * Returns (pre t n), which is (str.substr t 0 n). */ Node mkPrefix(Node t, Node n); diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index 017fc3cb4..8f8552e9c 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -193,7 +193,7 @@ class CVC5_EXPORT Rational } } - bool isIntegral() const { return getDenominator() == 1; } + bool isIntegral() const { return cln::denominator(d_value) == 1; } Integer floor() const { return Integer(cln::floor1(d_value)); } diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index b3c876533..de3fcd03d 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -286,7 +286,7 @@ class CVC5_EXPORT Rational return (*this); } - bool isIntegral() const { return getDenominator() == 1; } + bool isIntegral() const { return mpz_cmp_ui(d_value.get_den_mpz_t(), 1) == 0; } /** Returns a string representing the rational in the given base. */ std::string toString(int base = 10) const { return d_value.get_str(base); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 20722a1da..6943b7250 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1631,6 +1631,7 @@ set(regress_1_tests regress1/bags/map-lazy-lam.smt2 regress1/bags/murxla1.smt2 regress1/bags/murxla2.smt2 + regress1/bags/murxla3.smt2 regress1/bags/subbag1.smt2 regress1/bags/subbag2.smt2 regress1/bags/union_disjoint.smt2 @@ -2531,6 +2532,9 @@ set(regress_1_tests regress1/sygus/pLTL_5_trace.sy regress1/sygus/qe.sy regress1/sygus/qf_abv.smt2 + regress1/sygus/rand_const.sy + regress1/sygus/rand_p_0.sy + regress1/sygus/rand_p_1.sy regress1/sygus/real-any-const.sy regress1/sygus/real-grammar.sy regress1/sygus/rec-fun-swap.sy diff --git a/test/regress/regress1/bags/murxla3.smt2 b/test/regress/regress1/bags/murxla3.smt2 new file mode 100644 index 000000000..3bfce38b8 --- /dev/null +++ b/test/regress/regress1/bags/murxla3.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(declare-const A (Bag Bool)) +(set-info :status sat) +(declare-fun p ((Bag Bool)) Bool) +(assert (or (not (p A)) (not (p (as bag.empty (Bag Bool)))))) +(check-sat) diff --git a/test/regress/regress1/sygus/rand_const.sy b/test/regress/regress1/sygus/rand_const.sy new file mode 100644 index 000000000..e920a9cc0 --- /dev/null +++ b/test/regress/regress1/sygus/rand_const.sy @@ -0,0 +1,12 @@ +; COMMAND-LINE: --sygus-active-gen=random --sygus-out=status +; EXPECT: unsat + +(set-logic BV) + +; Ensures random enumerator correctly handles non-sygus types. + +(synth-fun f () (_ BitVec 7) + ((Start (_ BitVec 7))) + ((Start (_ BitVec 7) ((Constant (_ BitVec 7)))))) + +(check-synth) diff --git a/test/regress/regress1/sygus/rand_p_0.sy b/test/regress/regress1/sygus/rand_p_0.sy new file mode 100644 index 000000000..a7b3c9f41 --- /dev/null +++ b/test/regress/regress1/sygus/rand_p_0.sy @@ -0,0 +1,15 @@ +; COMMAND-LINE: --sygus-active-gen=random --sygus-out=status +; EXPECT: unsat + +(set-logic BV) +(set-option :sygus-active-gen-random-p 0) + +; Ensures random enumerator correctly handles cases where the coin flips to +; tails but there is no no-argument constructor to pick. + +(synth-fun f () Bool + ((Start Bool) (Const Bool)) + ((Start Bool ((not Const))) + (Const Bool (false)))) + +(check-synth) diff --git a/test/regress/regress1/sygus/rand_p_1.sy b/test/regress/regress1/sygus/rand_p_1.sy new file mode 100644 index 000000000..412e55f73 --- /dev/null +++ b/test/regress/regress1/sygus/rand_p_1.sy @@ -0,0 +1,14 @@ +; COMMAND-LINE: --sygus-active-gen=random --sygus-out=status +; EXPECT: unsat + +(set-logic BV) +(set-option :sygus-active-gen-random-p 1) + +; Ensures random enumerator correctly handles cases where the coin flips to +; heads but there is no constructor that takes arguments to pick. + +(synth-fun f () Bool + ((Start Bool)) + ((Start Bool (false)))) + +(check-synth) diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index b17054637..31034a15e 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -2777,6 +2777,40 @@ TEST_F(TestApiBlackSolver, proj_issue381) ASSERT_NO_THROW(d_solver.simplify(t187)); } + +TEST_F(TestApiBlackSolver, proj_issue382) +{ + Sort s1 = d_solver.getBooleanSort(); + Sort psort = d_solver.mkParamSort("_x1"); + DatatypeConstructorDecl ctor = d_solver.mkDatatypeConstructorDecl("_x20"); + ctor.addSelector("_x19", psort); + DatatypeDecl dtdecl = d_solver.mkDatatypeDecl("_x0", psort); + dtdecl.addConstructor(ctor); + Sort s2 = d_solver.mkDatatypeSort(dtdecl); + Sort s6 = s2.instantiate({s1}); + Term t13 = d_solver.mkVar(s6, "_x58"); + Term t18 = d_solver.mkConst(s6, "_x63"); + Term t52 = d_solver.mkVar(s6, "_x70"); + Term t53 = d_solver.mkTerm( + MATCH_BIND_CASE, d_solver.mkTerm(VARIABLE_LIST, t52), t52, t18); + Term t73 = d_solver.mkVar(s1, "_x78"); + Term t81 = + d_solver.mkTerm(MATCH_BIND_CASE, + d_solver.mkTerm(VARIABLE_LIST, t73), + d_solver.mkTerm(APPLY_CONSTRUCTOR, + s6.getDatatype() + .getConstructor("_x20") + .getInstantiatedConstructorTerm(s6), + t73), + t18); + Term t82 = d_solver.mkTerm(MATCH, {t13, t53, t53, t53, t81}); + Term t325 = d_solver.mkTerm( + APPLY_SELECTOR, + t82.getSort().getDatatype().getSelector("_x19").getSelectorTerm(), + t82); + ASSERT_NO_THROW(d_solver.simplify(t325)); +} + TEST_F(TestApiBlackSolver, proj_issue383) { d_solver.setOption("produce-models", "true"); diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp index 005e5cc3f..c468aa463 100644 --- a/test/unit/theory/sequences_rewriter_white.cpp +++ b/test/unit/theory/sequences_rewriter_white.cpp @@ -425,6 +425,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_concat) TEST_F(TestTheoryWhiteSequencesRewriter, length_preserve_rewrite) { + StringsRewriter sr(d_rewriter, nullptr); TypeNode intType = d_nodeManager->integerType(); TypeNode strType = d_nodeManager->stringType(); @@ -451,8 +452,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, length_preserve_rewrite) Node concat2 = d_nodeManager->mkNode( kind::STRING_CONCAT, {gh, x, d_nodeManager->mkNode(kind::STRING_REPLACE, x, gh, ij), ij}); - Node res_concat1 = SequencesRewriter::lengthPreserveRewrite(concat1); - Node res_concat2 = SequencesRewriter::lengthPreserveRewrite(concat2); + Node res_concat1 = sr.lengthPreserveRewrite(concat1); + Node res_concat2 = sr.lengthPreserveRewrite(concat2); ASSERT_EQ(res_concat1, res_concat2); } |