From 942b1c357a2a635bedcda8e01ce4f934c8a5a2e9 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 14 Dec 2021 12:02:37 -0800 Subject: Add switches to toggle eager and inclusion solvers (#7784) --- src/options/strings_options.toml | 16 ++++++++++++++++ src/theory/strings/regexp_solver.cpp | 2 +- src/theory/strings/theory_strings.cpp | 19 +++++++++++++++---- src/theory/strings/theory_strings.h | 2 +- 4 files changed, 33 insertions(+), 6 deletions(-) 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 @@ -208,6 +208,22 @@ name = "Strings Theory" default = "false" 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" 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 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/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 8b496b725..25db8d190 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -59,7 +59,9 @@ 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), @@ -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()) 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 d_eagerSolver; /** The extended theory callback */ StringsExtfCallback d_extTheoryCb; /** The (custom) output channel of the theory of strings */ -- cgit v1.2.3 From 1bf45579ff7a4af921bb3db159e371623a4bfd63 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 14 Dec 2021 12:40:06 -0800 Subject: Fix issues with tracing builds (#7809) This PR fixes two issues that were revealed when analyzing decreased performance on trace-enabled builds. hasIntegerModel() turns out to be a rather expensive method and should thus not be called in a Trace output. Furthermore, the implementation of Rational::isIntegral() was generally bad because it used getDenominator() (which returns a copy of the denominator as an Integer) instead of directly checking the underlying denominator with equality for zero. --- src/theory/arith/theory_arith_private.cpp | 4 +--- src/util/rational_cln_imp.h | 2 +- src/util/rational_gmp_imp.h | 2 +- 3 files changed, 3 insertions(+), 5 deletions(-) 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/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); } -- cgit v1.2.3 From 9ef7cc3520344901a704bda018cd1783ebc18d06 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 14 Dec 2021 13:14:48 -0800 Subject: Make some undocumented options regular/expert (#7805) We have some options that are currently "undocumented" for no good reason. This PR makes them regular or expert options. --- src/options/README.md | 12 +++++++++++- src/options/base_options.toml | 9 ++++++--- src/options/parser_options.toml | 3 ++- src/options/smt_options.toml | 14 +++++++------- 4 files changed, 26 insertions(+), 12 deletions(-) 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 = ["", "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 = ["", "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 = ["", "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/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" -- cgit v1.2.3 From bbbe2f3ebbd7175930054cca12c3e5e32cd0cbd9 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Tue, 14 Dec 2021 16:03:36 -0600 Subject: Add a random Sygus enumerator. (#7782) This PR adds a Sygus enumerator that generates random terms from a grammar. The size of the terms generated by the enumerator approximates a geometric distribution and can be configured with an option. --- src/CMakeLists.txt | 6 +- src/options/quantifiers_options.toml | 13 ++ .../quantifiers/sygus/enum_value_manager.cpp | 6 + .../quantifiers/sygus/sygus_random_enumerator.cpp | 199 +++++++++++++++++++++ .../quantifiers/sygus/sygus_random_enumerator.h | 129 +++++++++++++ test/regress/CMakeLists.txt | 3 + test/regress/regress1/sygus/rand_const.sy | 12 ++ test/regress/regress1/sygus/rand_p_0.sy | 15 ++ test/regress/regress1/sygus/rand_p_1.sy | 14 ++ 9 files changed, 395 insertions(+), 2 deletions(-) create mode 100644 src/theory/quantifiers/sygus/sygus_random_enumerator.cpp create mode 100644 src/theory/quantifiers/sygus/sygus_random_enumerator.h create mode 100644 test/regress/regress1/sygus/rand_const.sy create mode 100644 test/regress/regress1/sygus/rand_p_0.sy create mode 100644 test/regress/regress1/sygus/rand_p_1.sy 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/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." @@ -1099,6 +1102,16 @@ name = "Quantifiers" name = "auto" 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" 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 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& 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 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 stack; + // Constructors corresponding to each skolem. + std::unordered_map> skolemCons; + // Ground terms corresponding to each skolem. + std::unordered_map groundTerm; + // Sub-skolems needed for skolems with constructors that take arguments. + std::unordered_map> 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 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 + +#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>>; + +/** 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 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> d_minSygus; + /** Cache of the size of a sygus term. */ + std::unordered_map d_size; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 + +#endif // CVC5__THEORY__QUANTIFIERS__SYGUS_RANDOM_ENUMERATOR_H diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 20722a1da..ffff25520 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2531,6 +2531,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/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) -- cgit v1.2.3 From 42ea81197ca20d3fed29c2d461176dfec5270a27 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Tue, 14 Dec 2021 17:09:25 -0600 Subject: Fix cvc5-projects issue 358 (#7804) This PR fixes issue cvc5/cvc5-projects#358 which is caused by unregistered terms in the equality engine of bags --- src/theory/bags/theory_bags.cpp | 23 +++++++++-------------- test/regress/CMakeLists.txt | 1 + test/regress/regress1/bags/murxla3.smt2 | 6 ++++++ 3 files changed, 16 insertions(+), 14 deletions(-) create mode 100644 test/regress/regress1/bags/murxla3.smt2 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::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/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ffff25520..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 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) -- cgit v1.2.3 From 7a3273b3047120a0c69bbc040166895f69a3b2e2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 14 Dec 2021 17:26:46 -0600 Subject: Eliminate static calls to rewrite in strings (#7803) --- src/theory/strings/array_core_solver.cpp | 1 - src/theory/strings/base_solver.cpp | 11 +++++---- src/theory/strings/base_solver.h | 4 +++- src/theory/strings/core_solver.cpp | 32 +++++++++++++-------------- src/theory/strings/regexp_elim.cpp | 9 ++------ src/theory/strings/regexp_entail.cpp | 19 ++++++---------- src/theory/strings/regexp_entail.h | 2 -- src/theory/strings/sequences_rewriter.cpp | 26 +++++++++++----------- src/theory/strings/sequences_rewriter.h | 7 +++++- src/theory/strings/solver_state.cpp | 6 +++-- src/theory/strings/term_registry.cpp | 20 +++++++++++++++-- src/theory/strings/term_registry.h | 16 ++++++++++++++ src/theory/strings/theory_strings.cpp | 6 ++--- src/theory/strings/theory_strings_utils.cpp | 22 ------------------ src/theory/strings/theory_strings_utils.h | 21 ------------------ test/unit/theory/sequences_rewriter_white.cpp | 5 +++-- 16 files changed, 98 insertions(+), 109 deletions(-) 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& 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; 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::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& 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& 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 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 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 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 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(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().sgn() > 0); std::vector 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(); } - 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/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 1ccb67490..11cc52ad4 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* 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()) { 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()) { 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().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 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()) @@ -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()) + 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 res; String rem = x.getConst(); @@ -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* 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& 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& 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& 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& 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& 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 25db8d190..ee068fe16 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -67,7 +67,7 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) 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, @@ -590,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; @@ -1057,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_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& 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& 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 @@ -60,27 +60,6 @@ void getConcat(Node n, std::vector& c); */ Node mkConcat(const std::vector& 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& 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). */ 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); } -- cgit v1.2.3 From 5c82e1dd02c304dd34c72ffcc966840e8b3005ff Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 15 Dec 2021 09:15:26 -0600 Subject: Add trace to see inferences in final proof (#7813) Adds -t im-pf to see which inferences occur in the final proof. Must be used with proofs and --proof-annotate. --- src/smt/proof_final_callback.cpp | 6 ++++++ 1 file changed, 6 insertions(+) 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 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; } } } -- cgit v1.2.3 From eb3b04319a26e3573dd2ba520f12432ce2d797b3 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 15 Dec 2021 15:09:51 -0800 Subject: api: Fix smt-lib code blocks and math in C++ docs. (#7795) --- docs/api/java/java.rst | 4 +- docs/api/python/z3compat/boolean.rst | 12 +- docs/ext/smtliblexer.py | 16 +- src/api/cpp/cvc5.h | 602 ++++++++++++++++++++++++++--------- 4 files changed, 468 insertions(+), 166 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 `_ -^^^^^^^^^^^^^^^ +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ * class `Datatype `_ * class `DatatypeConstructor `_ 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/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 ) - * ( declare-fun ( ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (declare-const ) + * (declare-fun () ) * \endverbatim * * @param sort the sort of the constant @@ -3779,30 +3796,45 @@ class CVC5_EXPORT Solver /** * Assert a formula. + * * SMT-LIB: - * \verbatim - * ( assert ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (assert ) * \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 ( ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (check-sat-assuming ( )) * \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 ( + ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (check-sat-assuming ( + )) * \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 ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (declare-datatype ) * \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 ( * ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (declare-fun ( * ) ) * \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 ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (declare-sort ) * \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 ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (define-fun ) * \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 ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (define-fun-rec ) * \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 ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (define-fun-rec ) * \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 ( ^{n+1} ) ( ^{n+1} ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (define-funs-rec + * ( _1 ... _n ) + * ( _1 ... _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 ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (echo ) * \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 getAssertions() const; /** * Get info from the solver. - * SMT-LIB: \verbatim( get-info )\endverbatim + * + * SMT-LIB: + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-info ) + * \endverbatim + * * @return the info */ std::string getInfo(const std::string& flag) const; /** * Get the value of a given option. + * * SMT-LIB: - * \verbatim - * ( get-option ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-option ) * \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 `. * \endverbatim - * Requires to enable option 'produce-unsat-assumptions'. + * * @return the set of unsat assumptions. */ std::vector 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 `. * \endverbatim - * Requires to enable option 'produce-unsat-cores'. + * * @return a set of terms representing the unsatisfiable core */ std::vector 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 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 `. * \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 ( ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-value ( )) * \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 ( + ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-value ( * )) * \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 ` + * \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 `. * \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 ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-qe ) * \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 ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-qe-disjunct ) * \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 ( * ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (declare-pool ( * )) * \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& initValue) const; /** * Pop (a) level(s) from the assertion stack. + * * SMT-LIB: - * \verbatim - * ( pop ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (pop ) * \endverbatim + * * @param nscopes the number of levels to pop */ void pop(uint32_t nscopes = 1) const; /** * Get an interpolant + * * SMT-LIB: - * \verbatim - * ( get-interpol ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-interpol ) + * + * Requires to enable option + * :ref:`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 ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-interpol ) + * + * Requires to enable option + * :ref:`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 ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-abduct ) + * + * Requires to enable option + * :ref:`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 ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-abduct ) + * + * Requires to enable option + * :ref:`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 `. + * 'produce-models' and setting option + * :ref:`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 ( + ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (block-model-values ( + )) + * + * Requires enabling option + * :ref:`produce-models `. + * 'produce-models' and setting option + * :ref:`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& terms) const; @@ -4299,29 +4524,44 @@ class CVC5_EXPORT Solver /** * Push (a) level(s) to the assertion stack. + * * SMT-LIB: - * \verbatim - * ( push ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (push ) * \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 ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (set-info ) * \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 ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (set-logic ) * \endverbatim + * * @param logic the logic to set */ void setLogic(const std::string& logic) const; /** * Set option. + * * SMT-LIB: - * \verbatim - * ( set-option