cvc5.git
3 years agoRefactor regressions script (#7249)
Andres Noetzli [Thu, 21 Oct 2021 15:34:26 +0000 (08:34 -0700)]
Refactor regressions script (#7249)

This makes the regression script more modular by refactoring all the
different checks into separate classes, which makes it easier to add
additional tests and to run only a subset of the tests.

3 years agoMake cardinality constraint a nullary operator (#7333)
Andrew Reynolds [Thu, 21 Oct 2021 14:11:57 +0000 (09:11 -0500)]
Make cardinality constraint a nullary operator (#7333)

This makes cardinality constraints nullary operators. This eliminates hacks for supporting these previously.

It also removes an unimplemented kind CARDINALITY_VALUE.

Notice that the parser and printer now do not use a common syntax for cardinality constraints, this will be resolved on followup PRs.

3 years agoWorking on windows builds (#7381)
Gereon Kremer [Thu, 21 Oct 2021 12:31:59 +0000 (05:31 -0700)]
Working on windows builds (#7381)

This makes a push to fix our windows nightly builds. It does a couple of things:
- remove `CVC5_WINDOWS_BUILD` and check `CMAKE_SYSTEM_NAME` instead
- use `CMAKE_SHARED_LIBRARY_SUFFIX` instead of `so`
- properly set `IMPORTED_IMPLIB` on imported shared libraries
- fix the GMP build, where the header is different for shared and static builds
- fix the find&sed patching for libpoly
- add `CVC5_EXPORT` to nested types in the API
- remove `CVC5_EXPORT` from enums
- add `-Dcvc5_obj_EXPORTS` to actually enable exports
- Fix how template function `safe_print` is exported.

3 years agoAdd setup to generate graphs for cmake target dependencies (#7383)
Gereon Kremer [Thu, 21 Oct 2021 12:10:20 +0000 (05:10 -0700)]
Add setup to generate graphs for cmake target dependencies (#7383)

This adds the target `target-graphs` that generated graphs of cmake dependencies based on `cmake --graphviz`. It is a nice to tool to debug the cmake setup in some cases.

3 years agoEnable and fix dump test (#7387)
Andres Noetzli [Thu, 21 Oct 2021 01:31:52 +0000 (18:31 -0700)]
Enable and fix dump test (#7387)

Fixes #1649. The test was not enabled before and was still expecting
CVC-style output.

3 years agoFix (#7437)
Gereon Kremer [Thu, 21 Oct 2021 01:22:55 +0000 (18:22 -0700)]
Fix (#7437)

This PR reintroduces support for the (deprecated) option interactive-mode. It was erroneously removed in #7295.

Fixes #7379.

3 years agoEnable some previously failing regressions (#7434)
Andrew Reynolds [Wed, 20 Oct 2021 23:56:25 +0000 (18:56 -0500)]
Enable some previously failing regressions (#7434)

3 years agoFix docs upload (again) (#7435)
Gereon Kremer [Wed, 20 Oct 2021 23:45:48 +0000 (16:45 -0700)]
Fix docs upload (again) (#7435)

This is a follow-up to #7420. This time, I tested the modified code with every combination of values...

3 years agoapi: Add Solver::mkSepEmp(). (#7432)
Aina Niemetz [Wed, 20 Oct 2021 23:12:55 +0000 (16:12 -0700)]
api: Add Solver::mkSepEmp(). (#7432)

@alex-ozdemir

3 years agoapi: Improve documentation for special cases with nullary ops. (#7433)
Aina Niemetz [Wed, 20 Oct 2021 22:56:40 +0000 (15:56 -0700)]
api: Improve documentation for special cases with nullary ops. (#7433)

Fixes #7430.

3 years agoMove variadic trie utility to its own file (#7410)
Andrew Reynolds [Wed, 20 Oct 2021 22:39:12 +0000 (17:39 -0500)]
Move variadic trie utility to its own file (#7410)

Work towards a new internal fuzzing technique.

The new fuzzing technique leverages elements of the IJCAR 2020 paper on abduction, this moves https://github.com/cvc5/cvc5/blob/master/src/theory/quantifiers/sygus/cegis_core_connective.h#L44 to its own file. A followup PR will break this and further utility methods out of this file.

3 years agoAdd regressions for fixed issues (#7421)
Andrew Reynolds [Wed, 20 Oct 2021 22:28:52 +0000 (17:28 -0500)]
Add regressions for fixed issues (#7421)

Fixes #5288, fixes (the 3rd benchmark on) #5741, fixes #6184, fixes #5735, which do not trigger on master.

3 years agoAdd `isNull` and `isUpdater` to `Sort` class of python API (#7423)
yoni206 [Wed, 20 Oct 2021 22:18:33 +0000 (01:18 +0300)]
Add `isNull` and `isUpdater` to `Sort` class of python API  (#7423)

This adds two missing functions to the python API, along with tests for them. It also adds a missing test for the cpp API.

3 years agoThrow exception if checking model with separation logic heap (#7422)
Andrew Reynolds [Wed, 20 Oct 2021 22:09:07 +0000 (17:09 -0500)]
Throw exception if checking model with separation logic heap (#7422)

Fixes #5515.

It is currently not possible to check-model with separation logic. Checking models requires either additional bookkeeping (heap per formula position) or otherwise is expensive to check.

This makes us give a recoverable exception.

3 years agoCheck for higher-order variables in TheoryUF::ppRewrite (#7408)
Andrew Reynolds [Wed, 20 Oct 2021 22:01:01 +0000 (17:01 -0500)]
Check for higher-order variables in TheoryUF::ppRewrite (#7408)

Fixes #7000. That sequence of API calls now throws a logic exception.

3 years agoFix inadvertent failure of workflow step (#7420)
Gereon Kremer [Wed, 20 Oct 2021 21:42:16 +0000 (14:42 -0700)]
Fix inadvertent failure of workflow step (#7420)

This fixes an issue introduced with #7352: jobs fail immediately if any command has a non-zero exit code. The way we obtained the exit code of the `diff` command was incompatible with this policy, which is why we currently never upload any docs to `docs-ci`.

3 years agoEliminate last static calls to rewriter from smt layer (#7355)
Andrew Reynolds [Wed, 20 Oct 2021 21:07:09 +0000 (16:07 -0500)]
Eliminate last static calls to rewriter from smt layer (#7355)

3 years agoMake SyGuS solver robust to non-closed enumerable sorts (#7417)
Andrew Reynolds [Wed, 20 Oct 2021 20:47:06 +0000 (15:47 -0500)]
Make SyGuS solver robust to non-closed enumerable sorts (#7417)

This makes the SyGuS solver robust to variables that are not closed enumerable, e.g. arrays of uninterpreted sorts.

It corrects an issue in array's mkGroundTerm issue which would allow constants to enter into constraints for SyGuS problems with arrays. This method does not cause further issues currently since quantifiers is guarded in several places to ensure array constants are not constructed via this method.

It also makes it so that we don't add explicit CEGIS refinement lemmas unless evaluation unfolding is enabled and the counterexamples are from closed enumerable types; there is no reason to add these unless we are combining with evaluation unfolding.

This addresses several of the issues raised in #6605.

3 years agoDo not construct instantiation for checking propagating instantiations spurious ...
Andrew Reynolds [Wed, 20 Oct 2021 20:34:33 +0000 (15:34 -0500)]
Do not construct instantiation for checking propagating instantiations spurious (#7390)

This makes the check for when an instantiation is "propagating" faster by not constructing the substitution + rewriting of the entire formula, and instead threading the substitution through the entailment check utility's evaluateTerm utility.

On a handful of challenge Facebook benchmarks, we go 35 seconds -> 18 seconds with this change.

This also eliminates the argument exp to the evaluateTerm method, which is no longer used, and eliminates hasSubs from several methods, which is redundant.

3 years agoCheck whether abduct option is enabled (#7418)
Andrew Reynolds [Wed, 20 Oct 2021 19:48:11 +0000 (14:48 -0500)]
Check whether abduct option is enabled (#7418)

This addresses one of the issues related to #6605.

3 years agoapi: Rename get(BV|FP)*Size functions for consistency. (#7428)
Aina Niemetz [Wed, 20 Oct 2021 19:14:59 +0000 (12:14 -0700)]
api: Rename get(BV|FP)*Size functions for consistency. (#7428)

3 years ago[proofs] Alethe: Documentation on Translation (#7394)
Lachnitt [Wed, 20 Oct 2021 18:50:38 +0000 (11:50 -0700)]
[proofs] Alethe: Documentation on Translation (#7394)

Provides background on the translation into the Alethe calculus that is common to all rules.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
3 years agoAdd LFSC signature for n-ary programs (#7360)
Andrew Reynolds [Wed, 20 Oct 2021 17:27:33 +0000 (12:27 -0500)]
Add LFSC signature for n-ary programs (#7360)

This is the last utility signature. Theory signatures will be added afterwards.

3 years agoUse codatatype bound variables for codatatype values (#7425)
Andrew Reynolds [Wed, 20 Oct 2021 16:49:53 +0000 (11:49 -0500)]
Use codatatype bound variables for codatatype values (#7425)

Previously, we had conflated codatatype bound variables and uninterpreted constants (as they have the same functionality). However, we should separate these concepts so we can ensure that uninterpreted constants are only used for uninterpreted sorts.

3 years agoReimplement support for relational triggers (#7063)
Andrew Reynolds [Wed, 20 Oct 2021 16:14:50 +0000 (11:14 -0500)]
Reimplement support for relational triggers (#7063)

This makes relational triggers its own kind of instantiation match generator. Future PRs will delete the code interleaved in the core InstMatchGenerator class for handling relational triggers.

This PR also fixes two issues related to how trigger techniques are combined:
(1) instantiation match generators that are generated as part of multi-triggers now are properly specialized (using getInstMatchGenerator),
(2) there was a bug with auto-generated triggers: when the first auto-generated trigger was generated that was already a user trigger, then we would ignore all other auto-generated triggers.

This is work towards finding a solution for the choice.move.hard Facebook benchmark, where relational-triggers appear to be a possible solution.

3 years agoDo not make assumption about model for Boolean variables in FMF (#7407)
Andrew Reynolds [Wed, 20 Oct 2021 14:34:10 +0000 (09:34 -0500)]
Do not make assumption about model for Boolean variables in FMF (#7407)

Fixes cases where models can be wrong for FMF with Boolean variables in the bodies of quantified formulas.

Fixes #6744, all benchmarks on that issue are fixed. This PR adds 2 of the regressions from that issue.

3 years agoCorrectly parse uninterpreted constant values in get-value (#7393)
Andrew Reynolds [Wed, 20 Oct 2021 11:57:44 +0000 (06:57 -0500)]
Correctly parse uninterpreted constant values in get-value (#7393)

SMT-LIB indicates that abstract values can appear in terms as arguments to `get-value`.  This is not currently the case, as pointed out by #6908.

This updates our parser so that bindings are added to the symbol table for all uninterpreted constants in the model whenever we parse a `get-value` term.

Fixes #6908.

3 years agoAvoid escaping `double-quotes` twice. (#7409)
Abdalrhman Mohamed [Wed, 20 Oct 2021 01:11:53 +0000 (20:11 -0500)]
Avoid escaping `double-quotes` twice. (#7409)

With -o raw-benchmark, The command:

(echo """")
was printed as

(echo """""""")
because we run the quote-escaping procedure twice on it. This PR fixes the issue by ensuring that we only run it once.

3 years agoMake proofs of rewrites robust to use in internal subsolvers (#7411)
Andrew Reynolds [Wed, 20 Oct 2021 00:35:14 +0000 (19:35 -0500)]
Make proofs of rewrites robust to use in internal subsolvers (#7411)

We are currently using an attribute to mark "rewritten with proofs". This is incorrect as attributes are global, but proofs of rewrites are local to the solver instance.

This enables applications of proofs within internal subsolvers, and is required for a new internal fuzzing technique.

3 years agoAdd basic regular expression type enumerator (#7416)
Andrew Reynolds [Wed, 20 Oct 2021 00:24:32 +0000 (19:24 -0500)]
Add basic regular expression type enumerator (#7416)

The lack of a type enumerator for regular expressions makes certain things impossible e.g. sygus-based sampling for RE queries.

It is trivial to support a basic RE enumerator that takes singleton languages of strings. This commit adds this utility as the type enumerator for RE.

3 years agoFix expected conclusion for EQ_RESOLVE when expanding MACRO_SR_PRED_TRANSFORM (#7412)
Andrew Reynolds [Tue, 19 Oct 2021 23:53:56 +0000 (18:53 -0500)]
Fix expected conclusion for EQ_RESOLVE when expanding MACRO_SR_PRED_TRANSFORM (#7412)

Fixes a proof checking failure during post-processing.

Fixes a rare case where the RHS of equality resolve step requires a symmetry step.

3 years agoSupport sequences of fixed finite cardinality (#7371)
Andrew Reynolds [Tue, 19 Oct 2021 23:01:11 +0000 (18:01 -0500)]
Support sequences of fixed finite cardinality (#7371)

The only open case is dynamic cardinality types (e.g. uninterpreted sorts when FMF is enabled).

3 years agoFix issue related to sanity checking integer models (#7363)
Andrew Reynolds [Tue, 19 Oct 2021 20:35:13 +0000 (15:35 -0500)]
Fix issue related to sanity checking integer models (#7363)

We now insist that we sanity check integer models in linear logics. Previously, we could trigger an assertion failure in Minisat if a user asked for a model in a state where the linear solver had assigned a real value to an integer variable, as we would be sending a lemma during collectModelValues in a state where we had already terminated with "sat".

This also changes an assertion to warning, to allow the regression to pass.

Fixes #6774 (This PR fixes a followup issue after the original bad model reported there was fixed by sanity checks).

As the assertion failure is downgraded to a warning, fixes #6988, fixes #7252.

3 years agoRemove setDefaults methods (#7413)
Gereon Kremer [Tue, 19 Oct 2021 19:33:25 +0000 (12:33 -0700)]
Remove setDefaults methods (#7413)

This PR removes some auto-generated utility methods to set an option if it has not been set by the user. It was once added as we thought it might be useful, but we do not actually use it.

3 years agoAdd regression for fixed issue (#7395)
Andrew Reynolds [Mon, 18 Oct 2021 22:59:38 +0000 (17:59 -0500)]
Add regression for fixed issue (#7395)

Fixes #6653.

The third benchmark on that issue is no longer an issue, this adds it as a regression, which is the last open benchmark on the referenced issue.

3 years agoMove check for experimental arrays features to `theory_arrays.cpp`. (#7391)
Abdalrhman Mohamed [Mon, 18 Oct 2021 22:50:04 +0000 (17:50 -0500)]
Move check for experimental arrays features to `theory_arrays.cpp`. (#7391)

Check for experimental array features was done at the parser module, which meant that users of the API could use them without calling Solver::setOption("arrays-exp"). This PR fixes that by moving the check to the internal theory module.

3 years agoUpdate SMT-COMP script (#7389)
Andres Noetzli [Mon, 18 Oct 2021 14:50:50 +0000 (07:50 -0700)]
Update SMT-COMP script (#7389)

PR #6848 disabled relevancy order by default, but for QF_NIA, it helps
us solve significantly more benchmarks (17525 vs. 16889 with a 20 minute
timeout using the updated SMT-COMP script). This also updates the
options for `QF_AUFBV` and `QF_ALIA` to use `--decision=stoponly`,
following the name change of the option.

3 years agoPython api documentation: Op, Grammar, Result, Enums (#7095)
yoni206 [Fri, 15 Oct 2021 23:09:02 +0000 (02:09 +0300)]
Python api documentation: Op, Grammar, Result, Enums (#7095)

This PR adds documentation to the python class Op, Grammar, Result, and for API enums.
Additionally, documentation for isNull functions in the datatype classes is added for the python API, and a small change in the cpp API documentation is introduced.

3 years agoAdd more regressions for fixed issues (#7382)
Andrew Reynolds [Fri, 15 Oct 2021 22:57:00 +0000 (17:57 -0500)]
Add more regressions for fixed issues (#7382)

Fixes #6535, Fixes #6475, Fixes #5660, Fixes #6607, Fixes #6638, Fixes #6642, Fixes #6775.

3 years agoHave docs_upload properly upload tags. (#7352)
Gereon Kremer [Fri, 15 Oct 2021 20:54:06 +0000 (13:54 -0700)]
Have docs_upload properly upload tags. (#7352)

This PR improves our docs-ci mechanism to properly upload documentation for tags.

3 years agoFix bad cast in the python API (#7359)
Alex Ozdemir [Fri, 15 Oct 2021 20:45:03 +0000 (13:45 -0700)]
Fix bad cast in the python API (#7359)

3 years agoFix issues related to proofs of lemmas with duplicate conclusions in strings (#7366)
Andrew Reynolds [Fri, 15 Oct 2021 12:24:28 +0000 (07:24 -0500)]
Fix issues related to proofs of lemmas with duplicate conclusions in strings (#7366)

This makes string proof construction more robust by maintaining two separate proof inference constructors, one for facts and one for lemmas/conflicts. This avoids issues where 2 lemmas with the same conclusion (but possibly different explanations) are added in the same call to check.

This fixes one of the two issues related to proofs for #6973.

3 years agoAdd regressions for fixed issues (#7369)
Andrew Reynolds [Thu, 14 Oct 2021 23:54:28 +0000 (18:54 -0500)]
Add regressions for fixed issues (#7369)

Fixes #4393. Fixes #3966.

These issues do not occur on current master.

3 years agoFix (get-info :authors) (#7373)
Gereon Kremer [Thu, 14 Oct 2021 23:38:21 +0000 (16:38 -0700)]
Fix (get-info :authors) (#7373)

This PR fixes calling (get-info :authors). It used to (try to) print the whole about() information, but failed to do so because the string needed to be turned into an s-expression. However, about() is not properly escaped.
We now simply print the cvc5 authors.
It also fixes isValidGetInfoFlag() which was missing filename.

Fixes #7362.

3 years agoImprove ManagedStreams (#7367)
Gereon Kremer [Thu, 14 Oct 2021 22:16:58 +0000 (15:16 -0700)]
Improve ManagedStreams (#7367)

This PR addresses #7361, but also a more general issue about regular-output-channel being able to hold stderr and diagnostic-output-channel being able to hold stdout.
It therefore changes how non-owned streams are stored: beforehand, an explicit stream would always be owned by the ManagedStream (through a std::shared_ptr) and a nullptr implicitly stood for stdout, stderr or stdin. Now we explicitly hold a pointer to a non-owned stream for these special values.

Fixes #7361.

3 years agoAdd regression for fixed issue (#7365)
Andrew Reynolds [Thu, 14 Oct 2021 21:12:09 +0000 (16:12 -0500)]
Add regression for fixed issue (#7365)

Fixes #6845.

This issue does not occur in current master.

3 years agoImprove parser for tuple select (#7364)
Andrew Reynolds [Thu, 14 Oct 2021 20:32:37 +0000 (15:32 -0500)]
Improve parser for tuple select (#7364)

3 years agoSplit entailment check from term database (#7342)
Andrew Reynolds [Thu, 14 Oct 2021 19:15:29 +0000 (14:15 -0500)]
Split entailment check from term database (#7342)

Towards addressing some bottlenecks on Facebook benchmarks.

3 years agoAlso test older cmake versions (#7347)
Gereon Kremer [Thu, 14 Oct 2021 18:50:13 +0000 (11:50 -0700)]
Also test older cmake versions (#7347)

This PR generally improves the new CI job to test different cmake versions. It extends the tested versions back to 3.8 and also sets the minimum required version (cmake_minimum_required) to the version that is tested. This allows to check compatibility with changing cmake policies.
It also modifies the run-tests action to get the regression options from explicit inputs instead of the build matrix. As the cmake job had no build matrix, it used to build regress3-4 as well.

3 years agoFix quantifiers variable elimination for parametric datatypes (#7358)
Andrew Reynolds [Thu, 14 Oct 2021 16:14:02 +0000 (11:14 -0500)]
Fix quantifiers variable elimination for parametric datatypes (#7358)

Fixes #7353.

3 years agoFix GLPK linking (#7357)
Gereon Kremer [Thu, 14 Oct 2021 15:50:36 +0000 (08:50 -0700)]
Fix GLPK linking (#7357)

While #7341 added cmake-3.9 compatible linking for GLPK, it did not actually remove the line that triggers the error on older cmake versions. This commit does.

3 years agoAdd core LFSC signatures (#7289)
Andrew Reynolds [Thu, 14 Oct 2021 13:33:04 +0000 (08:33 -0500)]
Add core LFSC signatures (#7289)

These files define how terms and sorts are represented. It also adds basic utilities used throughout.

3 years agoEliminate uses of rewrite from datatypes theory (#7354)
Andrew Reynolds [Wed, 13 Oct 2021 15:22:03 +0000 (10:22 -0500)]
Eliminate uses of rewrite from datatypes theory (#7354)

Also simplifies slightly how rewritten forms of operators in sygus grammars are obtained.

3 years agoMake (proof) equality engine use Env (#7336)
Andrew Reynolds [Wed, 13 Oct 2021 04:38:46 +0000 (23:38 -0500)]
Make (proof) equality engine use Env (#7336)

3 years agoSimplify refinement in sygus solver (#7343)
Andrew Reynolds [Tue, 12 Oct 2021 22:50:53 +0000 (17:50 -0500)]
Simplify refinement in sygus solver (#7343)

This tightens the interface of the sygus solver, which was a product of not using subsolver calls in the original design.

3 years agoEliminate calls to currentResourceManager (#7350)
Andrew Reynolds [Tue, 12 Oct 2021 21:09:12 +0000 (16:09 -0500)]
Eliminate calls to currentResourceManager (#7350)

The remaining calls to smt::currentResourceManager are in the bitblasters, which should probably update to Env. FYI @mpreiner .

3 years agocmake: Fix git info if build directory is outside of source tree. (#7351)
Mathias Preiner [Tue, 12 Oct 2021 20:57:41 +0000 (13:57 -0700)]
cmake: Fix git info if build directory is outside of source tree. (#7351)

3 years agoClean up occurrences of SmtEngine in comments. (#7349)
Aina Niemetz [Tue, 12 Oct 2021 18:31:57 +0000 (11:31 -0700)]
Clean up occurrences of SmtEngine in comments. (#7349)

3 years agoGet rid of unused member d_smtStats in ExpandDefs. (#7346)
Aina Niemetz [Tue, 12 Oct 2021 18:09:22 +0000 (11:09 -0700)]
Get rid of unused member d_smtStats in ExpandDefs. (#7346)

This further renames d_smtStats to d_slvStats in ProcessAssertions.

3 years agoRename SmtEngineState to SolverEngineState. (#7344)
Aina Niemetz [Tue, 12 Oct 2021 17:53:03 +0000 (10:53 -0700)]
Rename SmtEngineState to SolverEngineState. (#7344)

3 years agoFix glpk, add antlr.so (#7341)
Gereon Kremer [Tue, 12 Oct 2021 16:37:51 +0000 (09:37 -0700)]
Fix glpk, add antlr.so (#7341)

This PR makes the cmake integration of GLPK compatible with cmake 3.9.
Also, it adds a missing BUILD_BYPRODUCT for antlr.

3 years agoProvide a non-traversal interface to term formula removal (#7328)
Andrew Reynolds [Tue, 12 Oct 2021 16:24:40 +0000 (11:24 -0500)]
Provide a non-traversal interface to term formula removal (#7328)

Towards making theory preprocessing a single pass.

3 years agoMinor cleaning of instantiation utilities (#7334)
Andrew Reynolds [Tue, 12 Oct 2021 15:29:38 +0000 (10:29 -0500)]
Minor cleaning of instantiation utilities (#7334)

Also fixes a bug in the quantifiers macro utility which did not compute the instantiation constant body of a quantified formula properly.

This is work towards a major refactoring of conflict-based instantiation / entailment checks.

3 years agoSimplify skolemization in sygus solver (#7331)
Andrew Reynolds [Tue, 12 Oct 2021 14:03:29 +0000 (09:03 -0500)]
Simplify skolemization in sygus solver (#7331)

The core sygus solver predates the use of subsolvers. When doing verification checks in the CEGIS loop, we previously added unique lemmas to the main solver with fresh skolem variables. We now call subsolvers only, meaning that the set of skolem variables used in verification calls can be fixed.

3 years agofix deprecation of std::iterator (#7332)
Ouyancheng [Tue, 12 Oct 2021 09:44:50 +0000 (02:44 -0700)]
fix deprecation of std::iterator (#7332)

When compiling cvc5 with clang-13, it will emit lots of warnings of usages of `std::iterator` as it's deprecated since C++17.
The recommended implementation of iterators is to manually define the following five types:
```
template< class Iter >
struct iterator_traits;

difference_type         Iter::difference_type
value_type         Iter::value_type
pointer                 Iter::pointer
reference         Iter::reference
iterator_category Iter::iterator_category

```
And the iterator-related types could be accessed by for example `typename std::iterator_traits<Iter>::value_type value`.

This pull request performs the fix, and the program is semantically equivalent before and after the fix.

References:
https://en.cppreference.com/w/cpp/iterator/iterator_traits
https://en.cppreference.com/w/cpp/iterator/iterator

3 years agoStart post-release for 0.0.2
Mathias Preiner [Mon, 11 Oct 2021 23:54:34 +0000 (16:54 -0700)]
Start post-release for 0.0.2

3 years agoBump version to 0.0.2
Mathias Preiner [Mon, 11 Oct 2021 23:54:34 +0000 (16:54 -0700)]
Bump version to 0.0.2

3 years agoFix release action.
Mathias Preiner [Mon, 11 Oct 2021 23:53:17 +0000 (16:53 -0700)]
Fix release action.

3 years agoRename SmtEngineStatistics to SolverEngineStatistics. (#7339)
Aina Niemetz [Mon, 11 Oct 2021 23:21:32 +0000 (16:21 -0700)]
Rename SmtEngineStatistics to SolverEngineStatistics. (#7339)

3 years agoStart post-release for 0.0.1
Mathias Preiner [Mon, 11 Oct 2021 22:45:50 +0000 (15:45 -0700)]
Start post-release for 0.0.1

3 years agoBump version to 0.0.1
Mathias Preiner [Mon, 11 Oct 2021 22:45:50 +0000 (15:45 -0700)]
Bump version to 0.0.1

3 years agoAntlr: runtime -> libraries (#7338)
Gereon Kremer [Mon, 11 Oct 2021 20:54:30 +0000 (13:54 -0700)]
Antlr: runtime -> libraries (#7338)

For static builds, there was a mixup of variable naming in FindANTLR3 (RUNTIME vs LIBRARIES).

3 years agoRename SmtScope to SolverEngineScope. (#7284)
Aina Niemetz [Mon, 11 Oct 2021 19:13:46 +0000 (12:13 -0700)]
Rename SmtScope to SolverEngineScope. (#7284)

3 years agoRevert #7257 (#7337)
Gereon Kremer [Mon, 11 Oct 2021 17:48:09 +0000 (10:48 -0700)]
Revert #7257 (#7337)

This PR reverts #7257 and restores compatibility with ancient glibc versions.

3 years agoAdd CI workflow to test different cmake versions (#7254)
Gereon Kremer [Mon, 11 Oct 2021 16:31:21 +0000 (09:31 -0700)]
Add CI workflow to test different cmake versions (#7254)

This refactors the CI setup by moving parts of the CI workflow into new composite actions. This allows to reuse this parts in a new workflow that tests against many different cmake versions. It is mostly useful after modifying our cmake setup to check compatibility with older cmake versions.
The workflow is not triggered automatically, but can be started manually.

3 years agoConnect the LFSC printer (#7323)
Andrew Reynolds [Mon, 11 Oct 2021 14:28:51 +0000 (09:28 -0500)]
Connect the LFSC printer (#7323)

This adds the option --proof-format=lfsc.

It adds an initial regression to test the LFSC printer. This will be followed up with a more comprehensive plan for regression tests.

3 years agoAdd cardinality constraint utilities (#7286)
Andrew Reynolds [Mon, 11 Oct 2021 08:20:19 +0000 (03:20 -0500)]
Add cardinality constraint utilities (#7286)

This class will be used to replace the `fmf.card` operator with a 0-ary indexed parameterized nullary predicate for representing cardinality constraints for UF.

This is in preparation for eliminating hacks in the core of theory combination for e.g. not considering the dummy arguments of cardinality constraints to be shared terms.

3 years agoRestore compatibility with cmake 3.9 (#7329)
Gereon Kremer [Mon, 11 Oct 2021 06:26:49 +0000 (23:26 -0700)]
Restore compatibility with cmake 3.9 (#7329)

This goes back to the new cmake setup and makes it compatible again with cmake 3.9.
It mostly means we can not link object libraries and also not link other libraries to object libraries.

I've tested these changes within docker on `ubuntu:18-04` with a manually installed `cmake-3.9.6`.

3 years agoRemove static accesses to options where EnvObj is used (#7330)
Gereon Kremer [Sat, 9 Oct 2021 15:19:15 +0000 (08:19 -0700)]
Remove static accesses to options where EnvObj is used (#7330)

This PR removes a bunch of static accesses in places where EnvObj is used now, and we can thus use options().

3 years agoMake skolem definition manager robust to function skolems (#7327)
Andrew Reynolds [Fri, 8 Oct 2021 20:32:24 +0000 (15:32 -0500)]
Make skolem definition manager robust to function skolems (#7327)

This led to a model soundness issue in a development branch that reorganizes theory preprocessing.

This ensures that skolem definition manager looks for skolems that appear in operators.

This is important for inputs like:
(declare-fun h (Int) Int)
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(assert (= h (ite A f g)))
(assert (= (h 0) ...)))

3 years agoAdd argument to distinguish lemmas and input assertions (#7326)
Andrew Reynolds [Fri, 8 Oct 2021 20:23:15 +0000 (15:23 -0500)]
Add argument to distinguish lemmas and input assertions (#7326)

Work towards virtual clause deletion, where lemmas will be SAT-context dependent.

This adds an argument to the decision engine so it can distinguish lemmas from input assertions.

3 years agoA few more miscellaneous uses of EnvObj (#7325)
Andrew Reynolds [Fri, 8 Oct 2021 16:36:55 +0000 (11:36 -0500)]
A few more miscellaneous uses of EnvObj (#7325)

3 years agoIgnore zip files for docs upload diff (#7322)
Gereon Kremer [Fri, 8 Oct 2021 11:02:51 +0000 (04:02 -0700)]
Ignore zip files for docs upload diff (#7322)

This fixes the diff mechanism to detect whether the current PR changes the documentation. It ignores zip files now, i.e. the javadoc search index files.

3 years agoAttach the static binaries to a release (#7324)
Gereon Kremer [Fri, 8 Oct 2021 10:46:47 +0000 (03:46 -0700)]
Attach the static binaries to a release (#7324)

This adds another step to our CI pipeline that uploads the binary build by some of the jobs to a release.

3 years agoMove preprocessor to smt solver (#7321)
Andrew Reynolds [Thu, 7 Oct 2021 20:10:26 +0000 (15:10 -0500)]
Move preprocessor to smt solver (#7321)

This breaks the circular dependency of preprocessing pass context of solver engine.

It also moves the preprocessor to be owned by SMT solver, instead of Solver engine.

It also changes the behavior of reset assertions: now, the preprocessing pass context is reset, whereas previously it was not. I believe this is the right behavior, as it eliminates stale data (e.g. learned literals, symbols in assertion cache).

3 years agoAdd a binary / SMT-LIB quickstart (#7315)
Gereon Kremer [Thu, 7 Oct 2021 18:26:31 +0000 (11:26 -0700)]
Add a binary / SMT-LIB quickstart (#7315)

This PR adds a binary/SMT-LIBv2 quickstart example, based on the cpp quickstart example.

3 years agoFinish the LFSC printer (#7285)
Andrew Reynolds [Thu, 7 Oct 2021 17:45:50 +0000 (12:45 -0500)]
Finish the LFSC printer (#7285)

This adds the remaining implementation of the LFSC printer.

It also corrects a bug introduced during merging the last PR.

The printer will be connected to the proof manager in a follow up PR. It will also be extended with support for DSL proof rule printing when the infrastructure is added.

3 years agoUse skolem lemma in prop layer interfaces (#7320)
Andrew Reynolds [Thu, 7 Oct 2021 16:49:41 +0000 (11:49 -0500)]
Use skolem lemma in prop layer interfaces (#7320)

3 years agoAdd new versioning scheme (#7253)
Gereon Kremer [Thu, 7 Oct 2021 14:51:09 +0000 (07:51 -0700)]
Add new versioning scheme (#7253)

This introduces a new versioning mechanism that allows for better automation.

3 years agoMake the cardinality of the alphabet of strings configurable (#7298)
Andrew Reynolds [Thu, 7 Oct 2021 12:18:08 +0000 (07:18 -0500)]
Make the cardinality of the alphabet of strings configurable (#7298)

This adds an option to change the cardinality of the alphabet of strings. The alphabet of strings is always a prefix of the interval of unicode code points in the string standard.

3 years agoAdd missing functions in Term.java (#7297)
mudathirmahgoub [Thu, 7 Oct 2021 11:29:28 +0000 (06:29 -0500)]
Add missing functions in Term.java (#7297)

This adds recent API functions that were added to terms.
It also uses BigInteger now for integer terms.

3 years agoFix/Improve static and shared builds with CLN or Poly (#7306)
Gereon Kremer [Thu, 7 Oct 2021 10:59:50 +0000 (03:59 -0700)]
Fix/Improve static and shared builds with CLN or Poly (#7306)

We already created two dependency targets `GMP_SHARED` and `GMP_STATIC`, as we could not use `libgmp.a` for shared linking (as it is built without `-fPIC`). This PR fixes our handling of CLN and Poly: they would always link with `GMP_STATIC`, leading to having both `GMP_SHARED` and `GMP_STATIC` in the linker command line in certain situations. We now also have `*_SHARED` and `*_STATIC` for both CLN and Poly.

3 years agoMiscellaneous fixes from proof-new (#7313)
Andrew Reynolds [Thu, 7 Oct 2021 09:53:59 +0000 (04:53 -0500)]
Miscellaneous fixes from proof-new (#7313)

Includes a few fixes for strings and datatypes theory lemma proofs.

3 years agoFast exit for string extended equality rewriter (#7312)
Andrew Reynolds [Thu, 7 Oct 2021 09:41:01 +0000 (04:41 -0500)]
Fast exit for string extended equality rewriter (#7312)

In benchmarks with many string equalities between variables and constants, a significant portion of the run time is spent on extended equality rewriting. This adds a fast exit when the equality is between variable/constants only.

3 years agoReplace doubles by rationals in C++ quickstart (#7317)
Gereon Kremer [Thu, 7 Oct 2021 03:03:17 +0000 (20:03 -0700)]
Replace doubles by rationals in C++ quickstart (#7317)

This PR removes the conversion of rationals to double in favour of properly handling them as rationals (as pairs of integers) in the C++ quickstart example.

3 years agoEliminate more circular dependencies on solver engine (#7311)
Andrew Reynolds [Thu, 7 Oct 2021 01:16:20 +0000 (20:16 -0500)]
Eliminate more circular dependencies on solver engine (#7311)

This is work towards replacing our old dump infrastructure. This PR also does some initial reorganization towards printing assertions using the print benchmark utility.

3 years agoChange behaviour of Term::getRealValue() (#7316)
Gereon Kremer [Thu, 7 Oct 2021 00:37:08 +0000 (17:37 -0700)]
Change behaviour of Term::getRealValue() (#7316)

This PR modifies the API function Term::getRealValue() to always return a fraction. Beforehand, it would return rationals in fractional notation (15/2) and integers in decimal notation (2.0).

3 years agoChange semantics of dumpUnsatCoresFull (#7314)
Gereon Kremer [Wed, 6 Oct 2021 23:12:46 +0000 (16:12 -0700)]
Change semantics of dumpUnsatCoresFull (#7314)

This PR changes --dump-unsat-cores-full to --print-unsat-cores-full.
It also makes it so that solely having --dump-unsat-cores-full no longer automatically prints unsat cores.

3 years agoRefactor skolem definitions notifications for the decision engine (#7310)
Andrew Reynolds [Wed, 6 Oct 2021 16:45:13 +0000 (11:45 -0500)]
Refactor skolem definitions notifications for the decision engine (#7310)

These changes are taken from the SAT relevancy branch. This does not change the behavior of the current code, it breaks the dependency of decision engine on the skolem definition manager and makes the latter solely managed by TheoryProxy.

This is in preparation for virtual clause deletion.

3 years agoEnable static builds in CI (#7281)
Gereon Kremer [Wed, 6 Oct 2021 16:27:33 +0000 (09:27 -0700)]
Enable static builds in CI (#7281)

This PR modifies our CI builds to have two static production builds. These binaries will be used as release artifacts later.