Implement alpha equivalence proofs (#7066)

This is a modified version of #6137 which accounts for extended rewriting between quantified formulas that are considered alpha equivalent.

It also generalizes the proof rule ALPHA_EQUIV. Notice that if we were to make this rule more pedantic, we would check for variable shadowing during substitution, although this is not currently done.

Make cegqi subsolvers EnvObj (#7205)

Makes a few places do multiplication for Rational directly instead of invoking the rewriter.

Remove CVC language support (#7219)

This commit removes the support for the CVC language and converts all *.cvc regression tests to SMT-LIBv2.

Towards standard usage of evaluator (#7189)

This makes the evaluator accessible via EnvObj through the Rewriter. It furthermore removes Rewriter::rewrite from inside the evaluator itself.

Construction of Evaluator utilities is now discouraged.

The include dependencies were cleaned slightly in this PR, leading to more precise includes throughout.

This is work towards having a configurable cardinality for strings, as well as eliminating SmtEngineScope.

Fix solver_black unit test (#7233)

In file `test/unit/api/solver_black.cpp` line 1499,
`for (const std::pair<Term, Term>& t : dmap)` is not the correct way of iterating through the element pairs,
it should be `for (const std::pair<const Term, Term>& t : dmap)` as the keys are immutable.
This triggers a warning on LLVM clang 12.0.1 (not AppleClang) on macOS.

Add extensionality option for strings disequalities (#7229)

Towards the strings array solver.

Extensionality for disequalities is disabled by default, but will be used when the strings array solver is enabled.

arrays: Use EnvObj::rewrite and EnvObj::options. (#7217)

This does not yet clean up the usage of Rewriter::rewrite in the arrays
type enumerator yet. Will be cleaned up in a follow-up PR.

arrays: Move type enumerator implementation to .cpp. (#7216)

This further cleans up the class declaration in the header to comply
with code style guidelines.

Eliminate arithmetic proof macros (#7226)

This PR eliminates some macros for arithmetic proofs, that only slightly simplified access to the produce-proofs option. Now that static access is deprecated, these checks needed to be implemented differently anyway.

Minimal fixing version for tuple update parsing (#7228)

This takes the essential changes from #7218 so that the current ANTLR issues are avoided.

[Proofs] Alethe: Translate ASSUME rule (#7213)

Implementation of the translation of ASSUME rules into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

[proofs] Alethe: Implementation of AletheProofPostprocessCallback (#7212)

Implementation of addAletheStep and addAletheStepFromOr. Added stub for AletheProofPostprocessCallback update function that will be populated by subsequent PRs.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

README: Fix link to INSTALL.rst. (#7222)

Fix handling of conversions between FP and reals (#7149)

Fixes #7056. Currently, we introduce a UF for conversions between FP
numbers and reals. This is done as part of `ppRewrite()`. The problem is
that terms sent to `ppRewrite()` are not fully preprocessed yet and the
FP theory solver was storing terms that were not fully preprocessed in a
map for later lookup. For the issue at hand, the conversion term
contained an `ite`, which was later removed. As a result, the theory
solver did not consider the term to be relevant when refining
abstractions. This commit changes the handling of conversion functions
to instead adding purification lemmas for conversion terms when they are
registered. The purification lemmas are needed, because otherwise, we
can't retrieve the model values for the term without the rewriter
interferring.

Start python API Solver documentation (#7064)

[proofs] Alethe: adds a node converter

Currently the only transformation it applies is removing attributes from quantifiers. Others may be added later.

Add the LFSC proof post-processor (#7134)

Includes the necessary conversions to LFSC for the core rules of the internal calculus.

TheoryModel: Use EnvObj::rewrite instead of Rewriter::rewrite. (#7215)

Optionally enable interprocedural optimization (#7209)

This commit adds support for enabling interprocedural optimization. The
option is enabled by default for --best builds and cuts down our
executable size from about 33M to 20M.

Add anchors to cmdline options (#7210)

This PR adds anchors to the auto-generates command line option documentation. This allows to link to specific options from other parts of the documentation.

Fix printer for datatype udpater (#7208)

Refactor tag suggestion mechanism (#7199)

This refactors the internal tag suggestion mechanism to no longer rely on C-style char arrays, but use a C++ vector of strings instead.

Use a single `NodeManager` per thread (#7204)

This changes cvc5 to use a single `NodeManager` per thread (using
`thread_local`). We have decided that this is more convenient because
nodes between solvers in the same thread could be exchanged and that
there isn't really an advantage of having multiple `NodeManager`s per
thread.

One wrinkle of this change is that `NodeManager::init()` must be called
explicitly before the `NodeManager` can be used. This code can currently
not be moved to the constructor of `NodeManager` because the code
indirectly calls `NodeManager::currentNM()`, which leads to a loop
because the `NodeManager` is created in `NodeManager::currentNM()`.
Further refactoring is required to get rid of this restriction.

[proofs] Alethe: Added Proof Postprocessor to alethe_proof_processor (#7202)

Added proof postprocessor class to alethe_proof_processor header file.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

[proofs] Alethe: Added Final Callback Function to alethe_proof_processor (#7200)

Added final callback class to alethe_proof_processor header file.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

Replace write access to options by a local variable (#7207)

This PR replaces a write to the options object by a local variable in the simplex procedure base class. The write was used to temporarily lower a limit for a single simplex call.

Minor cleanup related to EnvObj (#7206)

This PR does a bit of cleanup in the nonlinear arithmetic code related to the usage of EnvObj.

Fix relevant domain for parametric operators (#7198)

Fixes #6531.

This issue also occurs when using `--full-saturate-quant` on facebook benchmarks that combine multiple sequence types.

It does some cleanup on relevant domain in the process.

[proofs] Alethe: Added Callback Function to alethe_proof_processor (#7186)

Added alethe_proof_processor header file and introduced callback class.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

Minor changes to E-matching utilities (#7062)

remove options that are no longer used (#7197)

This PR removes a handful of options that are no longer used anywhere.

[proof] Added printer for proof rule names (#7185)

Implementation file for Alethe proof rules.

[proof] Alethe proof rules (#7180)

Adds header for Alethe proof rules

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

Eliminate global access to options:: from quantifiers rewriter (#7192)

Add get-difficulty to the API (#7194)

Adds smt2 parsing, printing and API support for get-difficulty. Adds unit tests.

Final cleanup (#7193)

This PR does some final cleanup on the options generation code.

Make `-o raw-benchmark` work with `--parse-only` (#7195)

Before, cvc5 was returning with --parse-only before the code could
reach the code responsible for dumping the raw benchmark. This moves the
check for --parse-only to the appropriate place and updates the
run_regression.py script to use --parse-only.

Support sygus version 2.1 command assume (#7081)

Adds support for global assumptions in sygus files.

Also guards against cases of declare-const, which should be prohibited in sygus.

Utilities in preparation for print benchmark utility (#7190)

This adds a few utilities in preparation for the print benchmark utility, which will replace our own dumping infrastructure.

Add proof manager method to translate difficulty map (#7159)

This method will be called from SmtEngine in the implementation for (get-difficulty).

Refactor code generation for option modules (#7182)

This PR refactors the code generation for options/<module>_options.(h|cpp).

Turn sphinx generation into a function (#7181)

This PR refactors the generation of the command line help for sphinx to a function, just like all the other code generation methods.

bv: Unify bit-blasting code for udiv and urem. (#7188)

This refactor additionally removes the caching for urem/udiv cases when
bit-blasting udiv/urem and eliminates the only rewrite() calls in the
bit-blaster. Caching is not required since repeated calls to udiv/urem
with the same arguments will produce the same circuit. Further, the rewrite()
calls during bit-blasting would further complicate the recording of
bit-blasting proofs and hence is removed.

proofs: Properly track pre- and post-rewrites in bbAtom(). (#7147)

This commit refactors the proof bit-blaster to properly track the pre- and post-rewrites in bbAtom(). The individual bit-blast steps are recorded in a term conversion proof generator. The overall bit-blast proof is stored in a BitblastProofGenerator, which tracks the pre- and post-rewrite and includes the bit-blast proof of the TCPG.

Reimplement `--dump=raw-benchmark` as `-o raw-benchmark` (#7191)

Printing the original benchmark is simple, as it is exactly the commands we execute.

This removes the previous code from SmtEngine, which is currently broken.

Remove context getters from `TheoryState` (#7174)

This removes TheoryState::getSatContext() and
TheoryState::getUserContext().

Connect difficulty manager to TheoryEngine (#7161)

This also introduces the produceDifficulty option which is analogous to produceUnsatCores.

It requires another unsat cores mode PP_ONLY, indicating that we are only tracking proofs of preprocessing. This option should perhaps be renamed to proofMode instead of unsatCoresMode, since its use is more general than for unsat cores. This will be addressed in a future refactoring.

Add Solver::isOutputOn() (#7187)

This PR adds a new api::Solver::isOutputOn() method, including unit tests for both isOutputOn() and getOutput().

FP: Rename FpConverter to FpWordBlaster. (#7170)

Refactor generation code for getInfo() (#7176)

This PR refactors the code generation for options::getInfo()

Add main options to cmake (#7178)

This PR adds main/options.cpp to cmake. Also, it removes the old (now obsolete and unused) options script.

Reorder code (#7175)

This PR reorders some options generation code that is out of order after some merges.

Refactor options parsing (#7143)

This PR refactors the code for options parsing.

Use StatisticsRegistry from Env (#7166)

This commit better integrates the StatisticsRegistry with the environment. It makes the registry an `EnvObj` itself and adds a getter to `EnvObj` to get the registry. It also refactors parts of cvc5 to use this new mechanism to obtain the registry instead of using the (global, static) `smtStatisticsRegistry()` function.

checkModel: Extend documentation. (#7177)

Add comment that partial operators are one reason that the current
assertion cannot be checked.

bv: Move IsPowerOfTwo rule to preprocessing pass and use EnvObj. (#7179)

IsPowerOfTwo rule is specific to the BvIntroPow2 preprocessing pass and should not be a general bit-vector rewrite rule.

Add casc 28 scripts (#7070)

FP: Enable caching in the theory inference manager. (#7168)

bv: Use EnvObj::rewrite() and EnvObj::options() in NodeBitblaster. (#7172)

This PR is based on #7171

FP: Use EnvObj::rewrite() and options() in theory_fp. (#7169)

FP: Do not send trivial lemmas. (#7167)

Fixes #7002.

Add Op.java to the java API (#6387)

This commit adds Op.java OpTest.java and cvc5_Op.cpp to the java api.

Use C++17 attributes (#7154)

Currently, we are using non-standard attributes. With C++17, all the
attributes that we use regularly are now standardized. This commit
replaces the compiler-specific attributes with standard ones.

More refactoring of set defaults (#7160)

This moves a large portion of the `finalizeLogic` method to more appropriate places.

It also fixes an issue : `opts.datatypes.dtSharedSelectorsWasSetByUser` was checked with wrong polarity, making a previous commit not effective.

bv: Use EnvObj::rewrite() and EnvObj::options() in BvSolver. (#7171)

Refactor command-line help (#7157)

This PR refactors how we generate the command-line help message.

Use EnvObj-based options in preprocessing (#7165)

This PR is the first step in replacing options access via options::foo() to using the environment (via EnvObj and options().module.foo). It replaces all such options accesses in the preprocessing passes.

pp passes: Use EnvObj::rewrite() instead of Rewriter::rewrite(). (#7164)

Remove `TheoryState::getEnv()` (#7163)

Add Solver::getOutput() (#7162)

Allow access to the Output() macro via the API.

Add difficulty manager (#7151)

Towards supporting a (get-difficulty) command.

This tracks an estimate of the difficulty of preprocessed assertions during solving. It will be connected to TheoryEngine (via RelevanceManager) in a followup PR.

Add difficulty post-processor (#7150)

This is work towards supporting a (get-difficulty) command.

This is a helper class for transforming the difficulty of preprocessed assertions to difficulty of the input assertions.

Disable shared selectors for quantified logics without SyGuS (#7156)

The use of shared selectors may have fairly negative effects when combined with E-matching. The issue is that it allows too many things to match. When shared selectors are disabled, a selector trigger like s(x) will only match terms that access the field of the constructor associated with s. When we use shared selectors, s(x) is converted to e.g. shared_selector_D_Int_1(x), which in turn matches applications of selectors of the same type over any constructor.

This PR disables shared selectors when quantifiers are present and SyGuS is not used.
It also disables shared selectors in single invocation subcalls, thus fixes #3109.
It further makes a minor fix to the datatypes rewriter to ensure that rewritten form does not depend on options.

Remove `TheoryState::options()` (#7148)

This commit removes TheoryState::options() by changing more classes to
EnvObjs.

Remove deprecated SyGuS method evaluateWithUnfolding (#7155)

This was a predecessor to the evaluator and TermDbSygus::rewriteNode that is no longer necessary.

This refactors the code so that evaluateWithUnfolding is replaced by rewriteNode as necessary throughout the SyGuS solver.

Note that in a few places, the extended rewriter was being used where TermDbSygus::rewriteNode (which also evaluates recursive function definitions) should have been used.

Add Lfsc print channel utilities (#7123)

These are utilities used for two-pass printing of LFSC proofs.

Improve pre-skolemization, move quantifiers preprocess to own file (#7153)

This also heavily refactors the preskolemization method (now in QuantifiersPreprocess), in preparation for it being enabled by default. This method previously was doing a tree traversal, it now maintains a visited cache.

It makes minor cleanup to the dependencies of this method.

Refactor options::set() (#7138)

This PR refactors the code generation and the generate code for options::set().

Work on comments (#7139)

This PR fixes / improves the comments in the options scripts.

A couple of minor cleanups (#7141)

This PR does a couple of minor cleanups related to options.

Refactor code generation for options.h/.cpp (#7126)

This PR refactors the options code generation for the options/options.h/.cpp files.

Towards standard usage of ExtendedRewriter (#7145)

This PR:

Adds extendedRewrite to EnvObj and Rewriter.
Eliminates static calls to Rewriter::rewrite from within the extended rewriter. Instead, the use of extended rewriter is always through Rewriter, which passes itself to the ExtendedRewriter.
Make most uses of extended rewriter non-static. I've added a placeholder method Rewriter::callExtendedRewrite for places in the code that call the extended rewriter are currently difficult to eliminate.

Add option for using bound inference for relevant assertions (#7152)

The method for discarding assertions based on bound inference is quite expensive (40% of runtime) for some benchmarks with quantified formulas from Facebook. This adds an option to disable this, which is done by default for quantified logics.

Add LFSC side condition conversion utility for list variables (#7131)

Required for automatic generation of side conditions from DSL rewrite rules.

Add Datatype.java to the Java API (#6389)

This commit adds Datatype.java DatatypeTest.java and cvc5_Datatype.cpp to the java api.

Add DatatypeConstructor.java, DatatypeConstructorDecl.java, DatatypeDecl.java, DatatypeSelector.java (#6390)

Add DatatypeConstructor.java, DatatypeConstructorDecl.java, DatatypeDecl.java, DatatypeSelector.java and their corresponding c++ files

Use rewriteViaMethod instead of accessing builtin proof checker (#7146)

Refactoring of proof manager initialization (#7073)

No longer takes a backwards reference to SmtEngine.

Also takes minor changes to proof post-processor from proof-new.

Use `EnvObj` methods instead of `Theory` methods (#7144)

This removes the methods `getEnv()`, `options()`, `getSatContext()`, and
`getUserContext()` from the `Theory` class because they are now part of
`EnvObj`. Additionally, this commit converts the inference managers to
`EnvObj` because of there were some calls to retrieve the contexts from
`Theory` in those classes.

sygus: Eliminate calls to Rewriter::rewrite. (#7142)

This derives sygus unification utility objects from EnvObj where
necessary. There's one remaining occurrence of Rewriter::rewrite in
sygus_unif_rl.cpp, which is a bit tricky to address and thus subject to
a future PR.

Refactoring and fixes of set defaults for quantifiers (#7120)

This PR further refactors set defaults for incompatibility issues related to quantifiers.

It adds a new restriction that was discovered recently: --nl-rlv should not be used in quantified logics. Some regressions are modified that are impacted by this restriction.

Also does minor rearrangements to the order in which default options are set.

EnvObj: Add options(), context(), userContext(). (#7137)

This further renames EnvObj::getLogicInfo to EnvObj::logicInfo.

Avoiding duplicate search in maps (#7055)

This commit identifies a couple of scenarios where an operation required
2 searches into a map/hashmap and replaces them with a single search.
This also makes the code shorter.

Signed-off-by: Mikolas Janota <mikolas.janota@gmail.com>

sygus: Make more classes derive from EnvObj. (#7140)

Refactor option sanitizations (#7129)

This PR refactors the code that performs sanity checks on the parsed option data.

Standardize Rewriter::rewriteViaMethod call (#7119)

This moves the standard method for rewrites in proofs from TheoryBuiltinProofRuleChecker to Rewriter.  The motivation for this change is to make various kinds of rewrite methods (standard rewrite, extended rewrite, extended equality rewrite, evaluate) accessible throughout the code in a standard way.  After this PR, it is possible to know variants of the REWRITE proof rule application by having access to the rewriter, instead of having to get the builtin proof rule checker.  Note that TheoryBuiltinProofRuleChecker::applyRewrite *cannot* be static since access to the rewriter is not longer permitted to be static.

It also removes some unused infrastructure from Rewriter.

Followup PRs will remove applyRewrite for TheoryBuiltinProofRuleChecker in favor of calling the rewriter directly.

Check that alternate is only set for bool (#7125)

This PR slightly changes how the alternate option property is handled and explicitly checks that alternate is only set for bool options.

Refactor options::get() and options::getNames() (#7135)

This PR refactors the code generation and the generated code for options::get() and options::getNames().

Make quantifier module classes derive from EnvObj (#7132)

sygus: Make CeSingleInv derive from EnvObj. (#7136)

This further reorders the header according to the code style guidelines.