Split higher-order term database (#7045)

This splits higher-order term database as a derived class of term database, thus separating higher-order specific things out of our core term database.

This eliminates many of the references to the deprecated option uf-ho.

This is work towards eliminating that option.

Refactor enumerator management in synth conjecture (#6942)

This moves the method SynthConjecture::getEnumeratedValue to its own class, EnumManager.

It also integrates the sygus enumerator callback into the fast enumerator.

bv-to-int: more implementations (#7051)

This PR introduces more implementations for the bv-to-int module. Once all implementations are in, this module will be called from the bv-to-int preprocessing pass, and the code there will be deleted.

Here we focus on the translation of nodes without children.
Unit tests are included.

Top-level structure for set defaults (#7047)

This breaks setDefaults into three functions that summarize the high-level behavior of setDefaults.

Uniform treatment of trusted theory inferences in proofs (#7044)

Makes it so that all theory-specific proof rules for this purpose are replaced by the generic THEORY_INFERENCE.

Miscellaneous changes from proof-new (#7042)

Fix non-deterministism in quantified datatypes expansion rewrite (#7036)

Required for properly checking proofs for quantifiers rewrites.

Purify substitutions in strings proof reconstruction (#7035)

This fixes an issue in strings proof reconstruction where sequential substitutions are used over possibly non-atomic terms like (str.replace x a b) and x simultaneously.

This leads to cases where we failed to reconstruct proofs, since a substitution x -> c, (str.replace x a b) -> d may unintentionally generate the term (str.replace c a b), after which the second substitution fails to apply.

Generalize inequality elimination in quantifiers rewriter (#7030)

This generalizes our inequality elimination technique to handle disequalities as well as inequalities.

#6999 is an example where a variable can be eliminated: if a variable x occurs only in an equality with negative required polarity, then the variable and that literal can be eliminated.

Fixes #6999.

Fix single invocation partition for higher-order (#7046)

It was not robust to cases where a function-to-synthesize occurred in a higher-order context.

Also does general clean up of the single invocation utility.

Move options parsing code to main (#7054)

This PR moves the code responsible for parsing the command line to the main folder. Note that the options themselves, and converting strings to the options proper types, calling predicates etc, stays in libcvc5. The PR also slightly refactors the options code to get rid of the assign_* functions.

Adding parameters to Datatype python API documentation (#7027)

api: Require size argument for mkBitVector. (#6998)

This removes support for creating bit-vectors from a string without a
size argument. We further also now require that the base argument is
always given (it has no default value).

Use options correctly in competition mode (#7053)

Fix competition mode by accessing options in the correct way in main functions.

Simplify model printing modes (#7049)

This removes the model printing mode options::ModelUninterpPrintMode::DtEnum which was previously used to print uninterpreted sorts as enumeration datatypes in the model. This mode was to my knowledge never used and moreover will not be easy to implement in the API.

This is work towards finalizing the API for models.

This PR also removes a file that I failed to delete in a recent PR.

Prenex quantified formulas with user annotations by default (#7048)

Our policy is now accurate to the help message on prenexUserQuant: we only prenex quantified formulas if they do not have user-provided patterns. Previously we also did not prenex any quantified formulas with any annotations.

This should avoid some more "unknown" responses on facebook benchmarks.

Also fixes a minor issue with when we print warnings about quantified formulas with no triggers.

FYI @barrettcw .

Make driver use options from the solver (#6930)

This PR removes explicit ownership of the options object from the main function and replaces it by an api::Solver object. To achieve this, it does a number of minor changes:
- api::Solver not takes a unique_ptr<Options> in its constructor
- CommandExecutor only holds a reference to (a unique ptr of) the api::Solver
- the main functions accesses options via the solver

Simplify how user-provided quantifier attributes are handled (#6963)

This makes INST_ATTRIBUTE (optionally) take multiple children, giving a way for the user to set attributes on quantified formulas, which does not require a new API command.

This is a special case of term annotations that occur as the body of a quantified formula.

If we need to extend our API to support further user-provided attributes, we should use a similar approach, e.g. a new kind ANNOTATE.

Add Term.java to the Java API (#6330)

This commit adds `Term.java`, `TermTest.java`, and `cvc5_Term.cpp` to the Java API.

More refactoring of set defaults (#7043)

A few minor changes to which options are enabled for sygus, otherwise no intended changes.

Support sygus standard command syntax set-feature (#7040)

This currently has no effect other than giving an unsupported warning.

In the future, set-feature will be implemented via the appropriate call to Solver::setOption if necessary.

Fixes #6182.

Eliminate eager model building (#7038)

Previously, we had a special case to support users who directly accessed the model object pointer in the old API.

The special case ensure that the information in the model was eagerly updated after each "sat" response, in the case that the user did not re-request a pointer to the model.

Since users no longer can access the internal model pointer (apart from GetModelCommand), this special case is no longer necessary.

This PR should make us slightly faster for incremental benchmarks where the user asks for the model on some but not all "sat" responses.

Use Env class in nonlinear extension (#7039)

This PR refactors the nonlinear extension(s) to access options only via the environment class.

Add CVC5ApiOptionException (#6992)

This PR adds the new CVC5ApiOptionException. While the driver does not (and can not) do anything special for the two existing api exceptions, it can (and should) properly inform the user about incorrect command line option usage.
The PR also removes the UnrecognizedOptionException. It is purely internal now, and immediately catched by the API wrapper. Having a separate exception for this is no longer useful.

The additional catch block in main.cpp is only temporary until option parsing has been migrated to the driver and setting the options is done properly via the API.

Make the python quickstart example run using ctest (#7023)

Add python quick start guide (#7024)

Remove `--(no-)interactive-prompt` (#7022)

This option is mostly redundant: It offers a way to access the
interactive shell without any copyright information or cvc5> prompt
being printed. However, --no-interactive offers the same experience
(except for the features offered by libedit).

Catch cases where recursive functions reference functions-to-synthesize (#6993)

We previously incorrectly allowed this, leading to problems that were unsolvable but where we would not warn the user this combination is not supported.

FYI @polgreen

Split proof final callback to its own file (#6984)

Refactor proof output for TPTP (#7029)

This eliminates the old option "inst format mode" and makes proof output for TPTP organized as an ordinary proof output format.

Start using Options via Env in arithmetic (#7032)

This PR refactors part of the arithmetic theory to use the options via the Env object.

[unsat cores] [proofs] Revert test about when to explain propagations (#7034)

Reverts a change from #7031, which changed the contract for when the proof CNF stream is handling propagations. When doing unsat cores with sat proofs (but not full proofs), theory engine will not be proof producing but the proof cnf stream still needs to connect theory lemmas with their clausified equivalents in the SAT solver.

move collectAssertedTerms back to the theory class (#7018)

This PR moves the collectAssertedTerms utility function from the model manager to the theory class. This allows to use the utility also when we are not currently building the model.

Minor fixes of policy for eliminating quantifiers (#7033)

PR #7017 fixed the policy for eliminating quantifiers but introduced
some minor issues, which this commit fixes:

the InstantiationEngine::checkOwnership() method was changed to look
for patterns in the wrong node.
the PR changed the modes of the --user-pat=MODE method but reused
one of the names. This commit fixes the name and adds a check in the
options script.
fixing the policy caused cvc5 to answer unsat instead of the
expected unknown for regress0/use_approx/bug812_approx.smt2. The
commit updates the expected result.

Make TheoryProxy use Env, simplify initialization of PropEngine (#7031)

This simplifies our management of how/when proofs are enabled in the PropEngine.

Replace `Maybe` with `std::optional` (#7005)

Because we are now using C++17, we can get rid of Maybe and instead
use std::optional, which offers the same functionality.

Make SmtEngineState use Env (#7028)

Also moves d_filename to Env.

Refactoring theory-specific variable elimination in quantifiers rewriter (#7026)

No behavior changes in this PR, just code reorganization.

Fix policy for eliminating quantified formulas (#7017)

This also consolidates the option strictTriggers into userPatMode.

Fixes #6996.

Make theory BV use central eq engine when option is enabled (#7025)

Cosmetic improvements to theory datatypes (#7020)

Mainly just indentation / formatting changes. In preparation for playing around with heuristics to datatypes theory motivated by Facebook benchmarks.

Improve conversion to skolems in expression miner (#7019)

Work towards a new expression miner for caching satisfiability queries.

Initial refactoring of set defaults (#7021)

This commit starts to carve out better control flow structure in setDefaults.

It makes setDefaults contained in a class, and moves a few blocks of code to their own functions.

This class also makes options manager obsolete, it is deleted in this PR.

There should be no behavior change in this PR.

Push Env class into TheoryState (#7012)

This PR is a follow-up to #7011, making the Env object available in the TheoryState base class.

Use InferenceManager in ExtTheory (#7006)

This PR refactors the ExtTheory class to use a given inference manager instead of a given output channel.

Make Theory class use Env (#7011)

This PR changes the Theory base class and the constructors of all theories to use the Env class to access contexts, logic information and the proof node manager.

[Strings] Make fact detection more robust (#7007)

Currently, our check for whether an inference is a fact or a lemma
involves checking whether the kind of the conclusion is a conjunction or
a disjunction. However, this does not take into account inferences of
other kinds such as ites, which is a problem because they require a
decision from the SAT solver. This commit changes the condition to check
the theory of the conclusion. If the conclusion belongs to the theory of
strings, it considers it as a fact.

Add check for static libraries when compiling CryptoMiniSat #7010 (#7014)

This commit adds a check for CryptoMiniSat's static dependencies when configuring CryptoMiniSat. It changes a build-time failure into a configure-time failure.

`find_library` in CMake > 3.18 supports `REQUIRED`; as `cvc5` targets 3.10, I've implemented a check for what `find_library` returns.

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>

Correct copyright print for GLPK (#7015)

In `master`, starting `cvc5` interactively will give you:

```
  glpk-cut-log -  a modified version of GPLK, the GNU Linear Programming Kit
  See http://github.com/timothy-king/glpk-cut-log for copyrightinformation
```

Notice: there's a double-space after the dash following the library name, and there's no space between "copyrightinformation".

This commit corrects this print such that it gives:

```
  glpk-cut-log - a modified version of GPLK, the GNU Linear Programming Kit
  See http://github.com/timothy-king/glpk-cut-log for copyright information
```

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>

Refactor setDefaults to use an options object (#6994)

This commit refactors the `setDefaults` method to accept an `Options` object as argument instead of using the current (static) `Options` object.

Disable external initialization of `thread_local` variables (#7004)

This commit adds `-fno-extern-tls-init` to the list of compiler flags to
tell the compiler that it can assume that there is no dynamic
initialization of thread-local variables in non-defining translation
units. This option should result in better performance and works around
crashing issues with our Windows build.

Simplify generation of option module code. (#6995)

This commit simplifies both the code that generates the option modules and the generated code itself. It removes placeholders in the templates that are no longer used, gets rid of the option holder types (and replaces them by simple inline functions) and does some clean up on the related code in the `mkoptions.py` script.

Create grouping of tests that exercise '--use-approx' (#6958)

Currently, it seems that `cvc5` has no tests that get anywhere near close to exercising the code in `approx_simplex`, which means that the GLPK integration is effectively untested in CI:

* https://cvc4.cs.stanford.edu/downloads/builds/coverage/cvc5-2021-08-02/index.src_theory_arith_approx_simplex.cpp.html

(which is at 2.8% at the time of writing!)

Indeed, if you run the whole of `ctest`, none of the code near GLPK is exercised; and, worse, there are *no* regression tests that use `--use-approx`!

This commit adds a selection of simple tests that have been derived (using `cvc5`'s existing regression suite and ddSMT) to reach code inside of `approx_simplex`; namely:

- `solveRelaxation`, and
- `solveMIP`

This is (hopefully) an initial start that will allow us to grow more regression tests exercising GLPK (e.g., following the same process of reduction, but using the SMTLIB benchmarks vs. only `cvc5`'s regression suite).

The folder structure has been named such that I can do `ctest -R "use_approx"` to run only the tests that (should) reach GLPK.

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>

Support older CMake versions (#7003)

Fixes #7001. Commit c8bc488 introduced the use
of list(PREPEND ...) which was only introduced in version 3.15. We require
CMake 3.9 or later and this commit makes our build system compatible with older
CMake versions again. It also changes our CI to have two builds with Ubuntu
18.04 and two builds with Ubuntu 20.04 to better cover different versions of
build tools (including CMake 3.10).

Merge options cmake into general cmake file (#6989)

This PR removes options/CMakeLists.txt and merges its contents into src/CMakeLists.txt and does some generalization in the mkoptions.py script. This prepares the whole setup so that we can also generate options code in other directories than options/ easily in the future: parts of the options code will be moved to the main folder.

Clear options manager (#6991)

This PR moves the remaining responsibilities from the options manager into option predicates. They belong there anyway, given that this code shall be executed immediately when an option is set. This also allows to remove the infrastructure for an options listener.

Normalize val in BitVector(val_str, base)  (#6955)

Fixes cpp API's mkBitVector(val_str, base) constructor.

Generalize term canonizer for type classes (#6895)

Initial work towards rewrite rule reconstruction.

[Unit Tests] Add missing include (#6990)

For some configurations, the unit test `solver_black` was unable to find
the correct variant `std::find()`. This commit adds an explicit include
of `<algorithm>`, which declares the `std::find()` as required by the
unit test.

Fix policy for rewriting string equalities (#6916)

This PR simplifies our rewriter for string equalities. We do not try to rewrite equalities to true/false by default.

This prevents cases where lemmas may contain vacuous premises that rewrite to false, hence making a lemma rewrite to true.

This PR reorganizes the interplay between the rewrite and the post-processing of rewrites via extended equality rewriting.

Fixes #6913. Also adds benchmarks from #6101 which appear related but were fixed in previous commits, thus fixes #6101 as well.

No longer call solver constructor with an options object. (#6985)

This PR removes calls to the Solver constructor with an Options object, and instead uses the setOption() method.

Consolidate solver resets (#6986)

This PR consolidates the two different reset implementations into a single function.

Proper printing of proofs in the internal calculus (#6975)

Fix policy for merging subproofs (#6981)

This makes it so that we replace subproof A with subproof B if A and B prove the same thing, and B contains no assumptions. This is independent of the scope that A and B are in.

The previous policy replaced subproof A with subproof B if A and B prove the same thing and were in the same scope. This is not safe if A occurs in multiple scopes, where free assumptions can escape.

The new policy is more effective and safer than the previous one.

[proof] [dot] Fix comments on dot printer (#6983)

This PR fixes the escaped characters in the dot printer. The output is now a valid DOT.

Signed-off-by: Diego Della Rocca de Camargos diegodellarocc@gmail.com

Add inference ids for remainder of sygus solver (#6977)

Now, all inferences throughout cvc5 in our regression are properly marked with an InferenceId.

This PR includes minor simplifications to the interface for sygus modules. In particular it changes the behavior to send inferences via the inference manager instead of passing them around as a vector.

Improve error messages for UF catching higher-order (#6982)

Addresses #6979.

syqi: Add debug information for dumping instantiations. (#6978)

Adds the datatype values as debug information for dumping instantiations produced by --sygus-inst.

Add optional debug information for dumping instantiations (#6950)

This complete the implementation of dump-instantiations-debug.

With this option, we can print the source of instantiations. For example:

$ cvc5 regress1/quantifiers/dump-inst-proof.smt2 --dump-instantiations-debug --produce-proofs
unsat
(instantiations (forall ((x Int)) (or (P x) (Q x)))
  (! ( 2 ) :source QUANTIFIERS_INST_E_MATCHING_SIMPLE ((not (= (P x) true))))
)
(instantiations (forall ((x Int)) (or (not (S x)) (not (Q x))))
  (! ( 2 ) :source QUANTIFIERS_INST_E_MATCHING_SIMPLE ((not (= (S x) false))))
)

Update bug_report.md

Add containsAssumption proof utility (#6953)

Work towards making our policy for subproof merging safer.

Refactor managed streams (#6934)

This PR introduces a new ManagedStream class that replaces the previous ManagedOstream. It allows to directly store the (wrapped) stream objects in the options. Handling the stream options is moved from the options manager to option predicates and the different options for input and output streams are combined into a single one.
Some associated utilities (open_ostream.h and update_ostream.h) are now obsolete and thus removed.

Add API function to get list of option names (#6971)

This PR adds a new API function api::Solver::getOptionNames() that exposes a list of all option names as strings. This PR will be followed by another that adds a method to further inspect a particular option by name, and thereby allows to inspect the solver options in a sensible way.

Replace numeric predicates by explicit minimum and maximum (#6976)

This PR replaces some option predicates by explicit minimum and maximum values. This allows us to export information about an options domain/range in the future.

Add missing inference identifiers (#6962)

The only remaining unknown inferences covered by our regressions are from the sygus solver, will address in later PR.

[proof] Add getProof to API and use it in GetProofCommand (#6974)

Also adds a call to get proof in a unit test.

Add IEEE-BV-to-FP to external-to-internal mapping in C++ API (#6951)

Without this, you can't make terms with that kind.

Remove dependencies on smt engine in smt solver (#6965)

This is work towards eliminating circular dependencies on SmtEngine.

This simplifies several interfaces and makes it so that SmtSolver does not take a pointer to its parent SmtEngine.

It is also work towards eliminating the output manager, which is now subsumed by Env.

Use int64_t, uint64_t or double for all numeric options. (#6970)

This PR further simplifies the option setup by only using int64_t or uint64_t for integer options.

Refactor shared solver to use theory builtin inference manager (#6960)

This ensures that e.g. COMBINATION_SPLIT shows up under theory::builtin::inferencesLemmas, and -t im. It also removes outdated interfaces from OutputChannel, and makes the feature TheoryEngine::ensureLemmaAtoms more modular, which was required for making these interfaces more consistent.

It also ensures that TheoryBuiltin has an inference manager, which will simplify special casing in #6956.

Remove "inUnsatCore" flag throughout (#6964)

The internal solver no longer cares about what assertions are named / are in the unsat core.

This simplifies the code so that the (now unused) `inUnsatCore` flag is removed from all interfaces.

This eliminates another external use of `getSmtEngine`.

Properly honor --stats-all and --stats-expert when printing statistics (#6967)

This PR fixes an issue that was introduced with fda4613 where printing the statistics would only show non-defaulted and non-expert options.

Add 'REQUIRES: poly' to regression. (#6966)

This regression times out without libpoly.

bv: Enable equality engine for bitblast-internal. (#6961)

Perform statistics printing via the API (#6952)

This PR changes how the command executor prints the statistics by moving stuff around a bit, eventually using only proper API methods of api::Solver. This PR also removes the smt_engine.h include from command_executor.cpp.

Allow changing certain options while solving (#6945)

This PR allows changing some select options ever after the smt engine has been fully initialized, following the SMT-LIB standard (section 4.1.7).

Simplify smt2 printer (#6954)

The common case of printing function applications is to print the kind in smt2 format, this makes this the default case and removes spurious cases. It also makes a few minor fixes.

Integrate installation instructions into documentation (#6814)

This PR migrates the current INSTALL.md to an rst file and then includes it in the documentation. It also does some minor improvements to this file, in particular it now mentions --dep-path

quickstart: Add python example to docs. (#6949)

[proofs] Set BV solver to better proof-producing one when proofs on (#6903)

Since the internal bitblaster can be way slower, the regressions that would have slow runs when --check-proofs is passed now have the command line that forces the use of the default bitblaster.

Python quick start example (#6939)

This is a translation of quickstart.cpp to python.

Integrate central equality engine approach into theory engine, add option and regressions (#6943)

This commit makes TheoryEngine take into account whether theories are using the central equality engine.

With this commit, the central equality engine can now be optionally enabled via `--ee-mode=central`.

Minor updates to shared terms database for central equality engine (#6929)

Includes proper set up of the proof equality engine it uses (which may be shared over multiple theories). Also makes its assertEquality method robust to non-equality atoms.

Fixes for building python wheels on manylinux2014 (#6947)

This PR makes several fixes to the wheel building infrastructure for manylinux2014.

don't statically link to Python (see: this section of PEP-513)
use standard 'build' directory. I noticed that the wheel infrastructure uses directory 'build' to prepare the wheel anyway, so it doesn't make a lot of sense for us to use a separate working directory. I tried changing the name of the build directory in setuptools by setting member variables in initialize_options but that didn't seem to work and I decided it wasn't worth the effort. The wheel should be built in a clean environment anyway, i.e., docker.
find the correct include directory and python library paths for building on manylinux2014 using skbuild. manylinux2014 has several versions of python installed in /opt/python. The CMake infrastructure can't find the necessary information (plus the libraries are deleted from the docker image to save space -- the library is just set to a generic libpython<version>.a). Instead, this PR would manually set them via CMake options.
to allow setting the python information, I extended the configure.sh script to allow directly setting CMake options. There are definitely other options here if you'd rather not change configure.sh. My reasoning was that it could be useful in other situations and I just marked it as an advanced feature. Another approach would be to use skbuild directly in the CMake infrastructure. I didn't like that solution because it would make the CMakeLists.txt more complicated and it wouldn't follow the standard CMake/Cython/Python approach which means we won't benefit from future improvements to that CMake infrastructure. Plus, this issue should only come up on systems with non-standard installations of Python, such as manylinux. This approach (setting CMake options) is basically what scikit-build does automatically if we had used that infrastructure directly.

Minor changes to arrays in preparation for central equality engine (#6917)

Makes arrays more robust to the order in which terms can be added to the equality engine vs. when they are preregistered.

We should probably performance test this.

FYI @barrettcw

Only use libedit on tty inputs (#6946)

This PR improves the check when we use libedit: only when the input is an interactive terminal.
This is motivated by a change to the unit test for the interactive mode that now properly redirects standard input (and output).

Print link to docs preview (#6922)

This commit adds a message to the `docs` target with a link to a preview
of the documentation, e.g.:

```
Preview docs in browser: file://localhost/home/noetzli/repos/cvc5_win/build-docs/docs/sphinx/index.html
```

Make extended rewriter methods const (#6948)

bv: Refactor getEqualityStatus and use for both bitblasting solvers. (#6933)

This commit refactors the getEqualityStatus handling for bitblast and bitblast-internal.

proof: Add eqrange expansion rule. (#6936)

Adds proof support for the eqrange operator.

Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>