Print response to get-model using the API (#7084)

This changes our implementation of GetModelCommand so that we use the API to print the model.

It simplifies smt::Model so that this is a pretty printing utility, and not a layer on top of TheoryModel.

It adds getModel as an API method for returning the string representation of the model, analogous to our current support for getProof.

This eliminates the last call to getSmtEngine() from the command layer.

rewriter: Make registerTheoryRewriter non-static. (#7101)

More work towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.

Fixed TestTheoryWhiteBagsRewriter.map failure (#7103)

Fixed TestTheoryWhiteBagsRewriter.map failure

Fix issues with cyclic proofs due to double SYMM applications (#7083)

Our way of constructing proofs from the equality engine in very rare cases may cause cyclic proofs due to constructing double applications of SYMM, which are not recognized as assumptions in CDProof. This is due to an interplay between LazyProofChain using an underlying CDProof as its default proof generator, where the proof chain would use the proofs from the CDProof to form a cyclic proof.

This was encountered in 9 SMT-LIB benchmarks in QF_SLIA.

This makes us safer in several places related to double SYMM steps.

Make driver::totalTime a TimerStat (#7089)

This makes the `driver::totalTime` statistic a `TimerStat`. This eliminates the need to obtain the overall runtime in the driver and write it to the statistics towards the end of the runtime. This not only eliminates some code in the driver, but also gets rid of the call to `getSmtEngine()` that goes around the API.
One disclaimer: The statistics output changes from seconds as a double (i.e. `1.234`) to milliseconds (i.e. `1234ms`).

No longer use direct access to options in driver (#7094)

This PR refactors the driver to no longer directly access the Options object, but instead use Solver::getOption() or Solver::getOptionInfo().

rewriter: Make clearCaches non-static. (#7100)

This works towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.

Lazy proof reconstruction for strings theory solver (#7096)

This makes it so that we call the strings::InferProofCons::convert lazily, instead deferring to a temporary, trusted STRING_INFERENCE rule.

This decreases our average proof overhead on commonly solved instances from 64% to 58% on QF_S + QF_SLIA. It also reduces timeouts significantly, from 2010 to 1460. (Note these numbers were with a slightly extended version of this branch that includes other pending PRs for proofs).

Also fixes one subtle issue where proof reconstruction was misusing sequential substitutions (leading to warnings during proof post-processing).

bv: Remove dump=bv-rewrites. (#7099)

This is work towards eliminating calls to currentSmtEngine.
This dump mode will become obsolete with the DSL, and is thus now
removed.

Make sure modes are sorted in ModeInfo (#7097)

This PR ensures that the possible modes returned in getOptionInfo() are always sorted. Their order would depend on the python dictionary ordering, which changed with a somewhat recent python version and thereby breaks our tests.

bv-to-int-module: implementations and stubs for translating operators (#7086)

This PR introduces most of the code for the translation of terms with operators. Some methods are left as stubs for future PRs.
A unit test is added with sanity checks for all implemented operators.

Fix normal forms context-dependent simplification for strings (#7090)

This corrects an issue in our context-dependent simplification which limited the cases it was applied.

Previously, we were using a best content heuristic when it was applicable to compute the substitution, even if we were in an effort where normal forms had been computed. The latter should always be used if possible, since normal forms always have at least as much or more concrete components.

Make regular expression sort not closed enumerable (#7092)

This ensures we don't try to apply e.g. enumerative instantiation to quantified formulas over regular expressions, since no type enumerator exists for RE.

Fixes #6750.

Add API function to obtain information about a single option (#6980)

This PR adds api::Solver::getOptionInfo() that returns information about a single option, including its name, aliases, current and default value and its domain.

Add kind BAG_MAP and its type rule to bags (#6503)

This PR adds kind BAG_MAP to bags.

Further refactoring of set defaults for incompatibility methods (#7072)

This introduces standard methods for checking incompatible with models, unsat-cores, incremental, proofs.

There is one minor change in behavior in this PR.When bitblast=eager and models were enabled in combined logics, then the set defaults would change the bitblast mode to lazy. However, it would then in the same block complain that eager cannot be used in combination with incremental. After this PR, we won't complain in this case since we've already decided to change the bitblast mode to lazy.

Refactor filename handling (#7088)

This PR simplifies how we store the current input file name and handle setting and getting it.
It is now an option, that can also be set and get via setInfo() and getInfo().

Fix proof equality engine for "no-explain" premises (#7079)

There was an inconsistency between when the equality engine would explain a literal and when we would provide a proof for it. This led to rare cases where we over zealously provided a proof for a fact that should have been an assumption in the theory lemma proof.

This corrects the issue by ensuring that no-explain premises are explicitly marked via a new helper proof generator "AssumptionProofGenerator" which always supplies (ASSUME f) as the proof for f.

This corrects some proof checking errors on string benchmarks.

python docs for Datatype-related classes (#7058)

Fix quantifiers dynamic split module for parametric datatypes (#7085)

Fixes #6838.

Add Driver options (#7078)

This PR adds a new API function Solver::getDriverOptions() which is used to communicate special options that (a) can not be properly communicated via getOption() and (b) need to be available in the driver (in a type-safe manner).
As of now, this concerns the input stream and output streams.
Furthermore, this PR refactors the driver to obtain them via the driver options instead of using the (deprecated) Solver::getOptions() method.

Handle languages as strings in driver (#7074)

This PR moves the first chunk of code in the driver to use the proper options API for the language options. It is now handled as a string.

Expand definitions in sygus operators at the SMT level (#7077)

Eliminates another call to currentSmtEngine.

This PR ensures we remember the mapping between operators that are embedded in sygus datatypes during preprocessing, instead of computing this within the sygus datatypes utilities when solving.

Add n-ary match trie utility (#6909)

Towards rewrite rule reconstruction

Add missing methods to Solver API for models (#7052)

This adds the last two remaining API methods required for implementing the text output of get-model on the API side.

A followup PR will implement GetModelCommand on the API side and eliminate the (last remaining) call to getSmtEngine() from the command layer.

This PR does some minor reorganization of the model cores code to account for the new interface. It also removes a deprecated interface from TheoryModel.

Add `isNull` to cpp api tests, python api, and python api tests (#7059)

While working on API documentation for python, I noticed that isNull is not wrapped
by the python API. It is also not tested in the cpp API tests. This PR fixes both issues,
and also updates the python api tests accordingly.

Fix a subtle issues with squashing the docs-ci history (#7075)

The docs-cleanup job squashes all commits from the docs-ci repository that are older than one month. The current solution to retrieve the newest commit older than this one month erroneously relied on the commit date. As the script cherry-picks all newer commits, it should rather use the author date, though. Unfortunately, rev-list does not support filtering by author date, hence we use awk now...

Eliminate currentSmtEngine for subsolver calls (#7068)

This eliminates another occurrence of smt::currentSmtEngine by making it required to pass options + logic for all subsolver calls.

Dump models for isNotEntailed results (#7071)

This fixes a minor issue where models should be dumped for "not entailed" results. This fix was required when preparing the submission to CASC this year.

Make datatype selector expansion to its own accessible method (#7069)

This eliminates another call to currentSmtEngine.

After this, there are only two remaining calls (one for normalizing sygus grammars wrt user define-funs, and the other for Rewriter::rewrite).

Improve integration of nonlinear arithmetic into the arithmetic theory. (#6956)

The nonlinear extension used to be called only during model construction, a rather atypical place which lead to a series of subtle issues. This PR moves it into the postCheck method. To do that, a few other changes are necessary, most notably collectAssertedTerms and collectTerms are moved back from the model manager into the theory class.

int2bv: Fix conversion of signed bit-vector values. (#7061)

This commit fixes the conversion of signed bit-vector values to integers in the int-to-bv preprocessing pass.

Consolidate language types (#7065)

This PR combines the two enums InputLanguage and OutputLanguage into a single Language type. It makes sure that AST is not used as input language using a predicate whenever the option is set.

Add missing include (#7067)

This adds a missing include. Compilation fails right now, if libpoly is disabled.

Eliminate calls to currentSmtEngine (#7060)

Work towards supporting multiple solvers running in parallel.

There are now only 5 remaining internal calls to smt::currentSmtEngine.

More will be eliminated on future PRs.

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