cvc5.git
3 years agoAdd API function to obtain information about a single option (#6980)
Gereon Kremer [Mon, 30 Aug 2021 23:55:58 +0000 (16:55 -0700)]
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.

3 years agoAdd kind BAG_MAP and its type rule to bags (#6503)
mudathirmahgoub [Mon, 30 Aug 2021 23:26:43 +0000 (18:26 -0500)]
Add kind BAG_MAP and its type rule to bags (#6503)

This PR adds kind BAG_MAP to bags.

3 years agoFurther refactoring of set defaults for incompatibility methods (#7072)
Andrew Reynolds [Mon, 30 Aug 2021 22:36:15 +0000 (17:36 -0500)]
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.

3 years agoRefactor filename handling (#7088)
Gereon Kremer [Mon, 30 Aug 2021 21:23:29 +0000 (14:23 -0700)]
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().

3 years agoFix proof equality engine for "no-explain" premises (#7079)
Andrew Reynolds [Mon, 30 Aug 2021 20:44:32 +0000 (15:44 -0500)]
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.

3 years agopython docs for Datatype-related classes (#7058)
yoni206 [Mon, 30 Aug 2021 19:32:24 +0000 (22:32 +0300)]
python docs for Datatype-related classes (#7058)

3 years agoFix quantifiers dynamic split module for parametric datatypes (#7085)
Andrew Reynolds [Mon, 30 Aug 2021 19:10:27 +0000 (14:10 -0500)]
Fix quantifiers dynamic split module for parametric datatypes (#7085)

Fixes #6838.

3 years agoAdd Driver options (#7078)
Gereon Kremer [Fri, 27 Aug 2021 18:51:02 +0000 (11:51 -0700)]
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.

3 years agoHandle languages as strings in driver (#7074)
Gereon Kremer [Fri, 27 Aug 2021 18:23:15 +0000 (11:23 -0700)]
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.

3 years agoExpand definitions in sygus operators at the SMT level (#7077)
Andrew Reynolds [Fri, 27 Aug 2021 18:03:41 +0000 (13:03 -0500)]
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.

3 years agoAdd n-ary match trie utility (#6909)
Andrew Reynolds [Fri, 27 Aug 2021 17:28:31 +0000 (12:28 -0500)]
Add n-ary match trie utility (#6909)

Towards rewrite rule reconstruction

3 years agoAdd missing methods to Solver API for models (#7052)
Andrew Reynolds [Fri, 27 Aug 2021 15:36:27 +0000 (10:36 -0500)]
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.

3 years agoAdd `isNull` to cpp api tests, python api, and python api tests (#7059)
yoni206 [Fri, 27 Aug 2021 00:34:12 +0000 (03:34 +0300)]
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.

3 years agoFix a subtle issues with squashing the docs-ci history (#7075)
Gereon Kremer [Thu, 26 Aug 2021 21:03:05 +0000 (14:03 -0700)]
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...

3 years agoEliminate currentSmtEngine for subsolver calls (#7068)
Andrew Reynolds [Thu, 26 Aug 2021 16:55:59 +0000 (11:55 -0500)]
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.

3 years agoDump models for isNotEntailed results (#7071)
Andrew Reynolds [Thu, 26 Aug 2021 16:32:09 +0000 (11:32 -0500)]
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.

3 years agoMake datatype selector expansion to its own accessible method (#7069)
Andrew Reynolds [Thu, 26 Aug 2021 16:20:43 +0000 (11:20 -0500)]
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).

3 years agoImprove integration of nonlinear arithmetic into the arithmetic theory. (#6956)
Gereon Kremer [Thu, 26 Aug 2021 14:19:56 +0000 (07:19 -0700)]
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.

3 years agoint2bv: Fix conversion of signed bit-vector values. (#7061)
Mathias Preiner [Thu, 26 Aug 2021 00:50:53 +0000 (17:50 -0700)]
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.

3 years agoConsolidate language types (#7065)
Gereon Kremer [Thu, 26 Aug 2021 00:19:41 +0000 (17:19 -0700)]
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.

3 years agoAdd missing include (#7067)
Gereon Kremer [Wed, 25 Aug 2021 18:01:26 +0000 (11:01 -0700)]
Add missing include (#7067)

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

3 years agoEliminate calls to currentSmtEngine (#7060)
Andrew Reynolds [Wed, 25 Aug 2021 16:27:03 +0000 (11:27 -0500)]
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.

3 years agoSplit higher-order term database (#7045)
Andrew Reynolds [Tue, 24 Aug 2021 20:54:31 +0000 (15:54 -0500)]
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.

3 years agoRefactor enumerator management in synth conjecture (#6942)
Andrew Reynolds [Tue, 24 Aug 2021 17:26:35 +0000 (12:26 -0500)]
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.

3 years agobv-to-int: more implementations (#7051)
yoni206 [Tue, 24 Aug 2021 01:20:56 +0000 (04:20 +0300)]
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.

3 years agoTop-level structure for set defaults (#7047)
Andrew Reynolds [Tue, 24 Aug 2021 01:09:31 +0000 (20:09 -0500)]
Top-level structure for set defaults (#7047)

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

3 years agoUniform treatment of trusted theory inferences in proofs (#7044)
Andrew Reynolds [Tue, 24 Aug 2021 00:33:18 +0000 (19:33 -0500)]
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.

3 years agoMiscellaneous changes from proof-new (#7042)
Andrew Reynolds [Tue, 24 Aug 2021 00:00:16 +0000 (19:00 -0500)]
Miscellaneous changes from proof-new (#7042)

3 years agoFix non-deterministism in quantified datatypes expansion rewrite (#7036)
Andrew Reynolds [Mon, 23 Aug 2021 22:15:41 +0000 (17:15 -0500)]
Fix non-deterministism in quantified datatypes expansion rewrite (#7036)

Required for properly checking proofs for quantifiers rewrites.

3 years agoPurify substitutions in strings proof reconstruction (#7035)
Andrew Reynolds [Mon, 23 Aug 2021 21:57:13 +0000 (16:57 -0500)]
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.

3 years agoGeneralize inequality elimination in quantifiers rewriter (#7030)
Andrew Reynolds [Mon, 23 Aug 2021 21:42:14 +0000 (16:42 -0500)]
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.

3 years agoFix single invocation partition for higher-order (#7046)
Andrew Reynolds [Mon, 23 Aug 2021 20:45:38 +0000 (15:45 -0500)]
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.

3 years agoMove options parsing code to main (#7054)
Gereon Kremer [Mon, 23 Aug 2021 19:11:13 +0000 (12:11 -0700)]
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.

3 years agoAdding parameters to Datatype python API documentation (#7027)
yoni206 [Mon, 23 Aug 2021 17:01:39 +0000 (20:01 +0300)]
Adding parameters to Datatype python API documentation (#7027)

3 years agoapi: Require size argument for mkBitVector. (#6998)
Aina Niemetz [Mon, 23 Aug 2021 16:50:06 +0000 (09:50 -0700)]
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).

3 years agoUse options correctly in competition mode (#7053)
Gereon Kremer [Mon, 23 Aug 2021 15:37:47 +0000 (08:37 -0700)]
Use options correctly in competition mode (#7053)

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

3 years agoSimplify model printing modes (#7049)
Andrew Reynolds [Sun, 22 Aug 2021 20:03:08 +0000 (15:03 -0500)]
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.

3 years agoPrenex quantified formulas with user annotations by default (#7048)
Andrew Reynolds [Sun, 22 Aug 2021 19:37:50 +0000 (14:37 -0500)]
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 .

3 years agoMake driver use options from the solver (#6930)
Gereon Kremer [Fri, 20 Aug 2021 21:47:04 +0000 (14:47 -0700)]
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

3 years agoSimplify how user-provided quantifier attributes are handled (#6963)
Andrew Reynolds [Fri, 20 Aug 2021 21:08:52 +0000 (16:08 -0500)]
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.

3 years agoAdd Term.java to the Java API (#6330)
mudathirmahgoub [Fri, 20 Aug 2021 19:30:29 +0000 (14:30 -0500)]
Add Term.java to the Java API (#6330)

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

3 years agoMore refactoring of set defaults (#7043)
Andrew Reynolds [Fri, 20 Aug 2021 19:19:30 +0000 (14:19 -0500)]
More refactoring of set defaults (#7043)

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

3 years agoSupport sygus standard command syntax set-feature (#7040)
Andrew Reynolds [Fri, 20 Aug 2021 02:34:45 +0000 (21:34 -0500)]
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.

3 years agoEliminate eager model building (#7038)
Andrew Reynolds [Fri, 20 Aug 2021 01:51:33 +0000 (20:51 -0500)]
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.

3 years agoUse Env class in nonlinear extension (#7039)
Gereon Kremer [Fri, 20 Aug 2021 01:30:31 +0000 (18:30 -0700)]
Use Env class in nonlinear extension (#7039)

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

3 years agoAdd CVC5ApiOptionException (#6992)
Gereon Kremer [Fri, 20 Aug 2021 00:31:58 +0000 (17:31 -0700)]
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.

3 years agoMake the python quickstart example run using ctest (#7023)
yoni206 [Thu, 19 Aug 2021 23:43:13 +0000 (02:43 +0300)]
Make the python quickstart example run using ctest (#7023)

3 years agoAdd python quick start guide (#7024)
yoni206 [Thu, 19 Aug 2021 23:32:57 +0000 (02:32 +0300)]
Add python quick start guide (#7024)

3 years agoRemove `--(no-)interactive-prompt` (#7022)
Andres Noetzli [Thu, 19 Aug 2021 23:03:13 +0000 (16:03 -0700)]
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).

3 years agoCatch cases where recursive functions reference functions-to-synthesize (#6993)
Andrew Reynolds [Thu, 19 Aug 2021 22:40:05 +0000 (17:40 -0500)]
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

3 years agoSplit proof final callback to its own file (#6984)
Andrew Reynolds [Thu, 19 Aug 2021 18:48:42 +0000 (13:48 -0500)]
Split proof final callback to its own file (#6984)

3 years agoRefactor proof output for TPTP (#7029)
Andrew Reynolds [Thu, 19 Aug 2021 18:32:50 +0000 (13:32 -0500)]
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.

3 years agoStart using Options via Env in arithmetic (#7032)
Gereon Kremer [Thu, 19 Aug 2021 17:29:17 +0000 (10:29 -0700)]
Start using Options via Env in arithmetic (#7032)

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

3 years ago[unsat cores] [proofs] Revert test about when to explain propagations (#7034)
Haniel Barbosa [Thu, 19 Aug 2021 14:06:23 +0000 (11:06 -0300)]
[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.

3 years agomove collectAssertedTerms back to the theory class (#7018)
Gereon Kremer [Wed, 18 Aug 2021 23:20:30 +0000 (16:20 -0700)]
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.

3 years agoMinor fixes of policy for eliminating quantifiers (#7033)
Andres Noetzli [Wed, 18 Aug 2021 21:06:52 +0000 (14:06 -0700)]
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.

3 years agoMake TheoryProxy use Env, simplify initialization of PropEngine (#7031)
Andrew Reynolds [Wed, 18 Aug 2021 20:13:21 +0000 (15:13 -0500)]
Make TheoryProxy use Env, simplify initialization of PropEngine (#7031)

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

3 years agoReplace `Maybe` with `std::optional` (#7005)
Andres Noetzli [Tue, 17 Aug 2021 18:18:16 +0000 (11:18 -0700)]
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.

3 years agoMake SmtEngineState use Env (#7028)
Andrew Reynolds [Tue, 17 Aug 2021 17:52:15 +0000 (12:52 -0500)]
Make SmtEngineState use Env (#7028)

Also moves d_filename to Env.

3 years agoRefactoring theory-specific variable elimination in quantifiers rewriter (#7026)
Andrew Reynolds [Tue, 17 Aug 2021 17:31:35 +0000 (12:31 -0500)]
Refactoring theory-specific variable elimination in quantifiers rewriter (#7026)

No behavior changes in this PR, just code reorganization.

3 years agoFix policy for eliminating quantified formulas (#7017)
Andrew Reynolds [Tue, 17 Aug 2021 17:07:00 +0000 (12:07 -0500)]
Fix policy for eliminating quantified formulas (#7017)

This also consolidates the option strictTriggers into userPatMode.

Fixes #6996.

3 years agoMake theory BV use central eq engine when option is enabled (#7025)
Andrew Reynolds [Tue, 17 Aug 2021 14:45:23 +0000 (09:45 -0500)]
Make theory BV use central eq engine when option is enabled (#7025)

3 years agoCosmetic improvements to theory datatypes (#7020)
Andrew Reynolds [Tue, 17 Aug 2021 05:44:20 +0000 (00:44 -0500)]
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.

3 years agoImprove conversion to skolems in expression miner (#7019)
Andrew Reynolds [Tue, 17 Aug 2021 05:24:39 +0000 (00:24 -0500)]
Improve conversion to skolems in expression miner (#7019)

Work towards a new expression miner for caching satisfiability queries.

3 years agoInitial refactoring of set defaults (#7021)
Andrew Reynolds [Tue, 17 Aug 2021 01:57:40 +0000 (20:57 -0500)]
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.

3 years agoPush Env class into TheoryState (#7012)
Gereon Kremer [Tue, 17 Aug 2021 00:20:27 +0000 (17:20 -0700)]
Push Env class into TheoryState (#7012)

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

3 years agoUse InferenceManager in ExtTheory (#7006)
Gereon Kremer [Mon, 16 Aug 2021 16:11:18 +0000 (09:11 -0700)]
Use InferenceManager in ExtTheory (#7006)

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

3 years agoMake Theory class use Env (#7011)
Gereon Kremer [Mon, 16 Aug 2021 14:20:22 +0000 (07:20 -0700)]
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.

3 years ago[Strings] Make fact detection more robust (#7007)
Andres Noetzli [Mon, 16 Aug 2021 13:58:43 +0000 (06:58 -0700)]
[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.

3 years agoAdd check for static libraries when compiling CryptoMiniSat #7010 (#7014)
Andrew V. Jones [Mon, 16 Aug 2021 05:31:23 +0000 (06:31 +0100)]
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>
3 years agoCorrect copyright print for GLPK (#7015)
Andrew V. Jones [Mon, 16 Aug 2021 03:24:25 +0000 (04:24 +0100)]
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>
3 years agoRefactor setDefaults to use an options object (#6994)
Gereon Kremer [Fri, 13 Aug 2021 00:12:19 +0000 (17:12 -0700)]
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.

3 years agoDisable external initialization of `thread_local` variables (#7004)
Andres Noetzli [Tue, 10 Aug 2021 20:04:21 +0000 (13:04 -0700)]
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.

3 years agoSimplify generation of option module code. (#6995)
Gereon Kremer [Tue, 10 Aug 2021 00:09:24 +0000 (17:09 -0700)]
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.

3 years agoCreate grouping of tests that exercise '--use-approx' (#6958)
Andrew V. Jones [Mon, 9 Aug 2021 18:01:37 +0000 (19:01 +0100)]
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>
3 years agoSupport older CMake versions (#7003)
Andres Noetzli [Mon, 9 Aug 2021 15:13:39 +0000 (08:13 -0700)]
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).

3 years agoMerge options cmake into general cmake file (#6989)
Gereon Kremer [Fri, 6 Aug 2021 18:55:18 +0000 (11:55 -0700)]
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.

3 years agoClear options manager (#6991)
Gereon Kremer [Fri, 6 Aug 2021 01:18:49 +0000 (18:18 -0700)]
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.

3 years agoNormalize val in BitVector(val_str, base) (#6955)
Alex Ozdemir [Thu, 5 Aug 2021 21:15:02 +0000 (14:15 -0700)]
Normalize val in BitVector(val_str, base)  (#6955)

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

3 years agoGeneralize term canonizer for type classes (#6895)
Andrew Reynolds [Thu, 5 Aug 2021 20:41:52 +0000 (15:41 -0500)]
Generalize term canonizer for type classes (#6895)

Initial work towards rewrite rule reconstruction.

3 years ago[Unit Tests] Add missing include (#6990)
Andres Noetzli [Thu, 5 Aug 2021 20:13:56 +0000 (13:13 -0700)]
[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.

3 years agoFix policy for rewriting string equalities (#6916)
Andrew Reynolds [Thu, 5 Aug 2021 15:21:48 +0000 (10:21 -0500)]
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.

3 years agoNo longer call solver constructor with an options object. (#6985)
Gereon Kremer [Thu, 5 Aug 2021 00:29:11 +0000 (17:29 -0700)]
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.

3 years agoConsolidate solver resets (#6986)
Gereon Kremer [Wed, 4 Aug 2021 23:46:49 +0000 (16:46 -0700)]
Consolidate solver resets (#6986)

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

3 years agoProper printing of proofs in the internal calculus (#6975)
Andrew Reynolds [Wed, 4 Aug 2021 22:28:55 +0000 (17:28 -0500)]
Proper printing of proofs in the internal calculus (#6975)

3 years agoFix policy for merging subproofs (#6981)
Andrew Reynolds [Wed, 4 Aug 2021 22:11:08 +0000 (17:11 -0500)]
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.

3 years ago[proof] [dot] Fix comments on dot printer (#6983)
Diego Della Rocca de Camargos [Wed, 4 Aug 2021 21:45:29 +0000 (18:45 -0300)]
[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
3 years agoAdd inference ids for remainder of sygus solver (#6977)
Andrew Reynolds [Wed, 4 Aug 2021 20:25:37 +0000 (15:25 -0500)]
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.

3 years agoImprove error messages for UF catching higher-order (#6982)
Haniel Barbosa [Wed, 4 Aug 2021 20:08:06 +0000 (17:08 -0300)]
Improve error messages for UF catching higher-order (#6982)

Addresses #6979.

3 years agosyqi: Add debug information for dumping instantiations. (#6978)
Mathias Preiner [Wed, 4 Aug 2021 19:38:24 +0000 (12:38 -0700)]
syqi: Add debug information for dumping instantiations. (#6978)

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

3 years agoAdd optional debug information for dumping instantiations (#6950)
Andrew Reynolds [Wed, 4 Aug 2021 19:19:51 +0000 (14:19 -0500)]
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))))
)

3 years agoUpdate bug_report.md
Aina Niemetz [Wed, 4 Aug 2021 19:01:08 +0000 (12:01 -0700)]
Update bug_report.md

3 years agoAdd containsAssumption proof utility (#6953)
Andrew Reynolds [Wed, 4 Aug 2021 18:58:14 +0000 (13:58 -0500)]
Add containsAssumption proof utility (#6953)

Work towards making our policy for subproof merging safer.

3 years agoRefactor managed streams (#6934)
Gereon Kremer [Wed, 4 Aug 2021 18:35:41 +0000 (11:35 -0700)]
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.

3 years agoAdd API function to get list of option names (#6971)
Gereon Kremer [Wed, 4 Aug 2021 18:17:42 +0000 (11:17 -0700)]
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.

3 years agoReplace numeric predicates by explicit minimum and maximum (#6976)
Gereon Kremer [Wed, 4 Aug 2021 17:49:26 +0000 (10:49 -0700)]
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.

3 years agoAdd missing inference identifiers (#6962)
Andrew Reynolds [Wed, 4 Aug 2021 16:32:48 +0000 (11:32 -0500)]
Add missing inference identifiers (#6962)

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

3 years ago[proof] Add getProof to API and use it in GetProofCommand (#6974)
Haniel Barbosa [Wed, 4 Aug 2021 15:28:12 +0000 (12:28 -0300)]
[proof] Add getProof to API and use it in GetProofCommand (#6974)

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

3 years agoAdd IEEE-BV-to-FP to external-to-internal mapping in C++ API (#6951)
Alex Ozdemir [Wed, 4 Aug 2021 01:41:04 +0000 (18:41 -0700)]
Add IEEE-BV-to-FP to external-to-internal mapping in C++ API (#6951)

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

3 years agoRemove dependencies on smt engine in smt solver (#6965)
Andrew Reynolds [Wed, 4 Aug 2021 01:15:43 +0000 (20:15 -0500)]
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.