cvc5.git
3 years agoSome cleanup in `mkoptions.py` (#6667)
Gereon Kremer [Fri, 4 Jun 2021 00:14:27 +0000 (02:14 +0200)]
Some cleanup in `mkoptions.py` (#6667)

This PR does some general cleanup in the mkoptions.py script: removal of obsolete code and some fixes to the comments.

3 years agodocs: Migrate datatypes theory reference. (#6662)
Aina Niemetz [Fri, 4 Jun 2021 00:07:05 +0000 (17:07 -0700)]
docs: Migrate datatypes theory reference. (#6662)

This migrates https://cvc4.github.io/datatypes.

3 years agoAdding unit tests for the datatypes python API (#6658)
yoni206 [Thu, 3 Jun 2021 23:57:29 +0000 (16:57 -0700)]
Adding unit tests for the datatypes python API (#6658)

This commit adds unit tests that are translated from `datatype_api_black.cpp`. One API function is also added to the python API.
This is the last part of the python api unit tests for datatypes.

Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
3 years agoSimplify automatic set-logic in smt2 parser (#6678)
Andrew Reynolds [Thu, 3 Jun 2021 22:49:32 +0000 (17:49 -0500)]
Simplify automatic set-logic in smt2 parser (#6678)

This simplifies the smt2 parser so that automatically setting the logic is done directly instead of being buffered as a command.

This prevents spurious errors for features that require (A) checking the logic is set and (B) fully intialize the underlying SMT engine.  `declare-pool` is an example of an smt2 command where the user will get an error (instead of a warning) when set-logic is not used due to setting the logic, after fully initing SMT engine and then executing the buffered set-logic command.

Note this should also make dump=raw-benchmark more accurate (no set-logic is included when dumping benchmarks with no set-logic command).

3 years ago[GitHub Actions] Make caching of dependencies depend on image version (#6677)
Andres Noetzli [Thu, 3 Jun 2021 22:26:52 +0000 (15:26 -0700)]
[GitHub Actions] Make caching of dependencies depend on image version (#6677)

Our Clang builds started to fail to link when the environment changed. This commit changes our CI to only use cached dependencies if the build environment has not changed.

3 years agoRenaming pow2 to p2 in regression tests (#6675)
yoni206 [Thu, 3 Jun 2021 14:39:55 +0000 (07:39 -0700)]
Renaming pow2 to p2 in regression tests (#6675)

We plan to add a unary pow2 operator to cvc5, that is obtained from the binary operator pow by fixing the first argument to 2.
An initial working branch is here: https://github.com/yoni206/cvc5/tree/pow2

This PR does the first step, which is to rename some uninterpreted symbols in regression tests from pow2 to p2, to avoid clashing with the new operator.

3 years agoRemove references to `bv-div-zero-const` in docs (#6672)
Andres Noetzli [Wed, 2 Jun 2021 21:37:48 +0000 (14:37 -0700)]
Remove references to `bv-div-zero-const` in docs (#6672)

The bv-div-zero-const option has been removed and is now always
enabled, so this commit updates the documentation of the kinds to
reflect that. It also makes the language to describe the special cases a
bit more uniform.

3 years agoFixes for printing define-fun-rec (#6673)
Andrew Reynolds [Wed, 2 Jun 2021 21:16:40 +0000 (16:16 -0500)]
Fixes for printing define-fun-rec (#6673)

3 years agoRemove option to ignore negative memberships (#6665)
Andres Noetzli [Wed, 2 Jun 2021 19:41:14 +0000 (12:41 -0700)]
Remove option to ignore negative memberships (#6665)

Fixes #6661. The option `--strings-inm` could be used to ignore negative
membership constraints. However, this option made the string solver
model-unsound or produced incorrect models if the user provided a
benchmark that actually contained negative membership constraints. The
solver did not check for negative membership constraints and did not
warn the user about them. Because the option is not really being used,
this commit removes it.

3 years agoAdding getters to the python API and testing them (#6652)
yoni206 [Wed, 2 Jun 2021 19:30:46 +0000 (12:30 -0700)]
Adding getters to the python API and testing them (#6652)

This PR adds missing API functions from the cpp Term API to the python API.
Corresponding tests are translated from term_black.cpp.

3 years agoRemove redundant logic ALL_SUPPORTED. (#6664)
Aina Niemetz [Wed, 2 Jun 2021 17:16:26 +0000 (10:16 -0700)]
Remove redundant logic ALL_SUPPORTED. (#6664)

3 years agoMove `toPythonObj` tests to the new API unit test directory (#6656)
yoni206 [Wed, 2 Jun 2021 16:47:09 +0000 (09:47 -0700)]
Move `toPythonObj` tests to the new API unit test directory (#6656)

This is the last test file that we move from the old directory to the new one, and so the old directory is deleted.

3 years agoUse proper variable name (#6670)
Gereon Kremer [Wed, 2 Jun 2021 16:01:08 +0000 (18:01 +0200)]
Use proper variable name (#6670)

This PR fixes the driver which used an incorrect variable name in competition mode.

3 years agoFix unsat core proofs (#6655)
Andrew Reynolds [Wed, 2 Jun 2021 15:28:36 +0000 (10:28 -0500)]
Fix unsat core proofs (#6655)

Fixes cases of satisfiable unsat cores when proofs are enabled.

Unfortunately, this bug was also preventing us from doing the final scope check for all proof checking. As this was not being tested, this PR uncovers that proof checking is now failing on 6 regressions. I'm disabling proof checking here and will address these issues on later PRs.

3 years agoMake `STRINGS_CTN_DECOMPOSE` an explicit conflict (#6663)
Andres Noetzli [Wed, 2 Jun 2021 13:50:51 +0000 (06:50 -0700)]
Make `STRINGS_CTN_DECOMPOSE` an explicit conflict  (#6663)

Fixes #6643. The STRINGS_CTN_DECOMPOSE inference is always a conflict
but we sometimes sent it as an inference. To make sure that the
inference manager actually recognizes the inference as a conflict, this
commit ensures that the conclusion is always false and modifies the
explanation accordingly.

3 years agoRemove `Options::operator[]` (#6649)
Gereon Kremer [Wed, 2 Jun 2021 13:21:22 +0000 (15:21 +0200)]
Remove `Options::operator[]` (#6649)

This PR removes the next heavily specialized template function Options::operator[] in favor of direct access to the option data.

3 years agoMove public wrapper functions out of options class (#6600)
Gereon Kremer [Wed, 2 Jun 2021 12:11:05 +0000 (14:11 +0200)]
Move public wrapper functions out of options class (#6600)

This PR moves options wrapper functions out of the Options class. These wrapper functions are meant to be called by "external" code that should not access the options modules. This PR thereby significantly reduces the interface of the Options class.

3 years agoFix issues with double negation in circuit propagator (#6669)
Gereon Kremer [Wed, 2 Jun 2021 11:55:40 +0000 (13:55 +0200)]
Fix issues with double negation in circuit propagator (#6669)

This PR fixes a subtle issue with double negations when producing proofs in the circuit propagator.
Adds the test case as a new regression, as well as some similar instances.
Fixes cvc5/cvc5-projects#277.

3 years agoFix issues when poly is disabled (#6668)
Gereon Kremer [Wed, 2 Jun 2021 10:11:13 +0000 (12:11 +0200)]
Fix issues when poly is disabled (#6668)

Recent changes introduced issues when libpoly is disabled.

3 years agoMake `Options::assign()` specializations free functions (#6648)
Gereon Kremer [Wed, 2 Jun 2021 06:55:24 +0000 (08:55 +0200)]
Make `Options::assign()` specializations free functions (#6648)

This PR removes the next two heavily specialized template functions. Both Options::assign() and Options::assignBool() are only used within options.cpp now and there is thus no reason to keep them in the public interface. Furthermore, we can just make them properly named functions instead of template functions.

3 years agoDo manual squash cleanup for docs (#6646)
Gereon Kremer [Wed, 2 Jun 2021 06:29:02 +0000 (08:29 +0200)]
Do manual squash cleanup for docs (#6646)

This PR abandons the attempt to do the cleanup in a single rebase command, and instead squashes the old commits manually. The current solution does not handle conflicts properly. The new approach (which seems to be more robust) proceeds as follows (to squash $first..$last):

- checkout $last
- soft reset to $first (checkout $first, but keep changes in working copy)
- commit to squashed commit
- cherry-pick $last..HEAD from main branch

3 years agodocs: Migrate input languages page. (#6659)
Aina Niemetz [Wed, 2 Jun 2021 00:21:56 +0000 (17:21 -0700)]
docs: Migrate input languages page. (#6659)

This migrates page https://cvc4.github.io/input-languages.

3 years agodocs: Restructure index page, fix style issue. (#6657)
Aina Niemetz [Wed, 2 Jun 2021 00:05:52 +0000 (17:05 -0700)]
docs: Restructure index page, fix style issue. (#6657)

3 years agoSome additions to the datatypes python API (#6640)
yoni206 [Tue, 1 Jun 2021 21:24:43 +0000 (14:24 -0700)]
Some additions to the datatypes python API (#6640)

This commit makes the following additions, in order to sync the python API with the cpp API.

1. adding `getName` functions to datatypes related classes
2. allowing `mkDatatypeSorts` with 1 or 2 arguments (previously allowed only 2).
3. In case there is a second argument to `mkDatatypeSorts`, we make sure it is a set.
4. Corresponding changes to the tests.

3 years agoUse top-level substitutions in ITE simp (#6651)
Andrew Reynolds [Tue, 1 Jun 2021 18:58:49 +0000 (13:58 -0500)]
Use top-level substitutions in ITE simp (#6651)

With this PR, we use the central top-level substitutions instance in the ITE simplification preprocessing pass. Previously the ITE simplification pass maintained its own copy of the substitutions.

Since the top-level substitutions now are the authority on models, this led to model failures after this change: ac8cf53#diff-30677c5a1752b1d0e83ef25fd2cfb8949576ea42cf7821fe0ac00ebbd0122f8aL276.
This PR corrects the issue.

This is required for SMT-COMP.

3 years agoDisable timeout regressions (#6650)
Andrew Reynolds [Tue, 1 Jun 2021 14:59:41 +0000 (09:59 -0500)]
Disable timeout regressions (#6650)

Disables two regressions that have been timing out causing nightlies to fail.

3 years agoFP value support in python API (#6644)
yoni206 [Tue, 1 Jun 2021 09:40:54 +0000 (02:40 -0700)]
FP value support in python API (#6644)

This PR adds new is* functions from the cpp API to the python API.
In particular, it adds getFloatingPointValue() function from the cpp API.
A test (translated from term_black.cpp) is added.

getFloatingPointValue() returns a tuple, and so this requires importing an instance of tuples into cython.

3 years agoRemove Options::ref() (#6647)
Gereon Kremer [Mon, 31 May 2021 14:05:39 +0000 (16:05 +0200)]
Remove Options::ref() (#6647)

This PR gets rid of the templated Options::ref() method (and all its specializations for every option).

3 years agoRemove invalid options from run scripts (#6645)
Andres Noetzli [Mon, 31 May 2021 04:13:37 +0000 (21:13 -0700)]
Remove invalid options from run scripts (#6645)

This commit removes some of the options in the run scripts that are not
supported anymore: `--bv-div-zero-const` and `--rewrite-divk`. Both of
those options are effectively enabled by default in cvc5.

3 years agoUpdate `toPythonObj` to use new getters -- part 1 (#6623)
yoni206 [Mon, 31 May 2021 00:56:14 +0000 (17:56 -0700)]
Update `toPythonObj` to use new getters -- part 1 (#6623)

Following #6496 , this PR adds new getters to the python API, as well as tests for them. This makes toPythonObj simpler.

A future PR will add more getters to the python API.

Co-authored-by: Gereon Kremer nafur42@gmail.com
3 years agoCompute model values for nested sequences in order (#6631)
Andres Noetzli [Mon, 31 May 2021 00:35:08 +0000 (17:35 -0700)]
Compute model values for nested sequences in order (#6631)

Fixes #6337 (the other benchmarks in this issue are either solved
correctly or time out after the changes in #6615) and fixes #5665.

While computing the model for a nested equivalence class containing
seq.unit, we were looking up the representative of the argument in
(seq.unit (seq.unit j)) and the representative was simpliy (seq.unit j). However, we had assigned (seq.unit 0) to (seq.unit j) earlier.
A second equivalence class of type (Seq (Seq Int)) and length 1 was
later assigned (seq.unit (seq.unit 0)) and we didn't detect that
(seq.unit (seq.unit j)) and (seq.unit (seq.unit 0)) have the same
value. This was incorrect because we do not allow assigning the same
value to different equivalence classes. In this case, it led to one of
the assertions being false.

This commit fixes the issues in two ways: it ensures that types are
processed in ascending order of nesting (e.g., (Seq Int) terms are
processed before (Seq (Seq Int)) terms) and it changes the procedure
to look up the representative in the model instead of the theory state
to take into account the model values assigned to the elements of
sequences.

cc @yoni206

3 years agoRemove `Options::set()` method (#6556)
Gereon Kremer [Sat, 29 May 2021 07:09:34 +0000 (09:09 +0200)]
Remove `Options::set()` method (#6556)

This PR gets rid of the Options::set() method, replacing it by direct access to the options data.
This method was only used internally and did nothing except for resolving the options data from the option tag type via template specializations (via ref()), which is no longer necessary.

3 years ago(Optimization) remove popObjective, add resetObjectives, rename pushObjective =>...
Ouyancheng [Fri, 28 May 2021 21:00:16 +0000 (14:00 -0700)]
(Optimization) remove popObjective, add resetObjectives, rename pushObjective => addObjective (#6634)

In order for OptimizationSolver to support pushing & popping,
we could remove popObjective because it might be difficult to handle cases like:

optSlv->pushObjective(...);
optSlv->push();
optSlv->popObjective();
optSlv->pop();
In this case we need to add back the popped objective...
If push/pop is supported, pop does not bring back objectives if you resetObjective
but it will revert the objs you add.
just like assertFormula and resetAssertions.

3 years agoPython API: bugfix + translating tests from cpp unit tests (#6559)
yoni206 [Fri, 28 May 2021 20:28:56 +0000 (13:28 -0700)]
Python API: bugfix + translating tests from cpp unit tests (#6559)

This PR fixes an issue in the python API for datatypes, and also introduces tests translated from https://github.com/cvc5/cvc5/blob/master/test/unit/api/datatype_api_black.cpp

The next PR will translate more tests and will also introduce missing functions in the python API for datatypes.

3 years agoAdd non-templated method to set option defaults (#6540)
Gereon Kremer [Fri, 28 May 2021 19:46:54 +0000 (21:46 +0200)]
Add non-templated method to set option defaults (#6540)

This PR replaces the templated Options::setDefault() methods by new non-templated free functions options::{module}::setDefault{option}().
These methods should be used instead of the common if (!set by user) { set option value } pattern.

3 years agoDisable `--jh-rlv-order` for slow regressions (#6633)
Andres Noetzli [Fri, 28 May 2021 14:10:15 +0000 (07:10 -0700)]
Disable `--jh-rlv-order` for slow regressions (#6633)

This commit adds --no-jh-rlv-order to two string regressions that take
over 2 minutes to run in debug after #6613, which increases the overall
regression runtime significantly.

3 years ago`STRINGS_CTN_DECOMPOSE`: Avoid multiple conflicts (#6632)
Andres Noetzli [Fri, 28 May 2021 03:28:20 +0000 (20:28 -0700)]
`STRINGS_CTN_DECOMPOSE`: Avoid multiple conflicts (#6632)

Fixes #5508. `STRINGS_CTN_DECOMPOSE` could be triggered multiple times
by the same term, which resulted in an assertion failure. This commit
returns immediately after the first conflict to avoid the assertion
failure.

3 years agoFix regular expression aggressive elim (#6627)
Andrew Reynolds [Thu, 27 May 2021 23:22:28 +0000 (18:22 -0500)]
Fix regular expression aggressive elim (#6627)

Fixes #6620, fixes #6622. Fixes cvc5/cvc5-projects#254.

The benchmarks from the 2 issues timeout, a regression is added for the projects issue.

3 years agoFix `str.replace_re` and `str.replace_re_all` (#6615)
Andres Noetzli [Thu, 27 May 2021 22:42:10 +0000 (15:42 -0700)]
Fix `str.replace_re` and `str.replace_re_all` (#6615)

Fixes #6057. The reductions of `str.replace_re` and `str.replace_re_all`
were not correctly enforcing that the operations replace the _first_
occurrence of some regular expression in a string. This commit fixes the
issue by introducing a new operator `str.indexof_re(s, r, n)`, which,
analoguously to `str.indexof`, returns the index of the first match of
the regular expression `r` in `s`. The commit adds basic rewrites for
evaluating the operator as well as its reduction. Additionally, it
converts the reductions of `str.replace_re` and `str.replace_re_all` to
use that new operator. This simplifies the reductions of the two
operators and ensures that the semantics are consistent between the two.

3 years agoAdd Lexicographic + Pareto Optimizations (#6626)
Ouyancheng [Thu, 27 May 2021 22:02:48 +0000 (15:02 -0700)]
Add Lexicographic + Pareto Optimizations (#6626)

Lexicographic optimizations: Optimize the objectives one-by-one, in the order they are pushed.
Pareto optimizations: Optimize the objectives to the extend that further optimization on any objective will worsen the other objective.
Units tests are of course added.

Lexicographic optimization is using iterative implementation, pretty similar to the naive box optimization.

3 years agoUpdate proof namespaces (#6614)
Andrew Reynolds [Thu, 27 May 2021 21:28:58 +0000 (16:28 -0500)]
Update proof namespaces (#6614)

This removes namespace theory from proof utilities, and moves MethodId to its own file in src/proof/.

3 years agoFix CEGQI for datatypes with Boolean subfields (#6630)
Andrew Reynolds [Thu, 27 May 2021 21:18:28 +0000 (16:18 -0500)]
Fix CEGQI for datatypes with Boolean subfields (#6630)

Fixes a solution soundness issue caused by allowing ineligible terms of kind BOOLEAN_TERM_VARIABLE to appear in instantiations.

This also corrects the expected solution on a benchmark that had an incorrect status.

Fixes #6603.

3 years agoFix spurious assertion for trivial abduction (#6629)
Andrew Reynolds [Thu, 27 May 2021 20:02:43 +0000 (15:02 -0500)]
Fix spurious assertion for trivial abduction (#6629)

Fixes 2nd benchmark from #6605.

3 years agoFP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD. (#6628)
Aina Niemetz [Thu, 27 May 2021 19:08:24 +0000 (12:08 -0700)]
FP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD. (#6628)

This is to make it consistent with the name of the SMT-LIB operator
(fp.add).

3 years agoReturn `REWRITE_AGAIN` after rewriting bvcomp (#6624)
Andres Noetzli [Thu, 27 May 2021 17:11:57 +0000 (10:11 -0700)]
Return `REWRITE_AGAIN` after rewriting bvcomp (#6624)

This commit fixes an assertion failure in the rewriter on some of the
SMT-LIB QF_ABVFP benchmarks (the regression in this commit is the
minified version of
`non_incremental/QF_ABVFP/20170428-Liew-KLEE/imperial_gsl_benchmarks_statistics_klee.x86_64/query.14.smt2`).
The problem was that after applying the `BvComp` rewrite, the bit-vector
rewriter was returning `REWRITE_DONE` instead of `REWRITE_AGAIN`. The
rewrite simplifies expressions of the form `bvcomp(t, c)` where `c` is a
constant of bit-width 1. If `c` is zero, then the rewrite returns
`bvnot(t)`. This node can potentially be rewritten further, e.g., if `t`
is `bvnot(x)`. This commit fixes the response and adds the corresponding
tests.

3 years agoAdd support for Box optimization (#6599)
Ouyancheng [Thu, 27 May 2021 07:53:58 +0000 (00:53 -0700)]
Add support for Box optimization (#6599)

Add support for box optimization -- independently optimize each goal as if the other goals do not exist.
Single minimize() / maximize() now maintains the pushed / popped context.
Of course unit tests are here as well.

3 years agoAvoid uploading docs if they did not change (#6621)
Gereon Kremer [Thu, 27 May 2021 07:38:12 +0000 (09:38 +0200)]
Avoid uploading docs if they did not change (#6621)

Fixes an oversight from #6601.

3 years agoEnable new justification heuristic by default (#6613)
Andrew Reynolds [Thu, 27 May 2021 06:44:55 +0000 (01:44 -0500)]
Enable new justification heuristic by default (#6613)

This enables the new implementation of justification heuristic by default.

Fixes #5454, fixes #5785. Fixes wishues 114, 115, 149, 160.

3 years agoUse references instead of getter functions (#6597)
Gereon Kremer [Wed, 26 May 2021 20:30:19 +0000 (22:30 +0200)]
Use references instead of getter functions (#6597)

This PR follows a suggestions of @ajreynol to use public references instead of getter functions to access the individual option modules.

3 years ago More precise includes of `Node` constants (#6617)
Andres Noetzli [Wed, 26 May 2021 14:30:17 +0000 (07:30 -0700)]
 More precise includes of `Node` constants (#6617)

We store constants, e.g., BitVector and Rational, in our node infrastructure. As a result, we were indirectly including some headers in almost all files, e.g., the GMP headers. This commit changes that by forward-declaring the classes for the constants. As a result, we have to include headers like util/rational.h explicitly when we use Rational but it saves about 3 minutes in compile time (CPU time).

The commit changes RoundingMode from an enum to an enum class such that it can be forward declared.

3 years agoAdd more examples to the documentation (#6569)
Gereon Kremer [Wed, 26 May 2021 06:30:45 +0000 (08:30 +0200)]
Add more examples to the documentation (#6569)

This PR adds (most of) the existing examples to the documentation, and does some other minor updates on the documentation. Some details:
- for consistency, all cpp examples are moved from examples/api to examples/api/cpp
- add capabilities for SMT-LIB examples, and two simple smt2 examples
- more docs/examples/*.rst files
- two new documentation categories: installation (how to obtain, compile and install cvc5) and binary (about the cvc5 binary)

3 years agoEnsure proper types in unit tests (#6598)
Gereon Kremer [Wed, 26 May 2021 06:20:03 +0000 (08:20 +0200)]
Ensure proper types in unit tests (#6598)

This PR fixes a type mixup (the usual long vs long long mixup on macos systems) in the unit tests for the new api::Term getters.
Fixes #6594.

3 years agoReduce size of sphinx-gh output (#6601)
Gereon Kremer [Wed, 26 May 2021 06:10:51 +0000 (08:10 +0200)]
Reduce size of sphinx-gh output (#6601)

This PR reduces the disk size of the docs generated by make sphinx-gh.
Apart from reformatting the cmake source, we now not only remove the _sources folder, but also .doctrees (essentially the sphinx cache) and _static/fonts/ (the fonts that are actually used live in _static/css/fonts).
In combination, this now reduces the disk size from about 20MB (sphinx) to less than 6MB (sphinx-gh).
Furthermore this PR only uploads the generated documentation if it differs from whatever we currently have for master.
This is relevant to make the docs-ci repository smaller (which already has more than 5GB...)

3 years agoapi docs: Fix and tweak style for home and top links. (#6618)
Aina Niemetz [Tue, 25 May 2021 21:05:40 +0000 (14:05 -0700)]
api docs: Fix and tweak style for home and top links. (#6618)

3 years agoReplace deprecated calls to `std::allocator` (#6606)
Andres Noetzli [Tue, 25 May 2021 13:51:56 +0000 (06:51 -0700)]
Replace deprecated calls to `std::allocator` (#6606)

Fixes #6453. This commit replaces all calls to std::allocator with calls to
std::allocator_traits. Strictly speaking, allocate() and deallocate() are
not deprecated but the commit replaces them for uniformity.

3 years ago[Unit tests] Fix path of Java bindings (#6616)
Andres Noetzli [Tue, 25 May 2021 03:21:16 +0000 (20:21 -0700)]
[Unit tests] Fix path of Java bindings (#6616)

Currently, when configuring cvc5 with Java bindings, CMake complains
about `get_filename_component(CVC5_JNI_PATH ${CVC5_JAR_PATH} DIRECTORY)`
not using the correct number of arguments in the Java unit tests. The
issue is that `${CVC5_JAR_PATH}` is empty. The value of
`${CVC5_JAR_PATH}` was computed in the Java API bindings but then not
shared with the rest of the build system. Because `${CVC5_JAR_PATH}` is
not used anywhere else, this commit moves the computation of
`${CVC5_JAR_PATH}` to the unit tests. The commit also ensures that the
API subdirectories are processed before the test subdirectories.

3 years agoFix non-fixed length case in re-elim (#6612)
Andrew Reynolds [Mon, 24 May 2021 23:59:28 +0000 (18:59 -0500)]
Fix non-fixed length case in re-elim (#6612)

Fixes followup issues from #6604.

3 years agoImplementation of the new justification heuristic (#6465)
Andrew Reynolds [Mon, 24 May 2021 19:32:48 +0000 (14:32 -0500)]
Implementation of the new justification heuristic (#6465)

This adds the new implementation of the justification heuristic. It does not enable this strategy yet.

A followup PR will activate this strategy within DecisionEngine.

3 years agoMove proof utilities to src/proof/ (#6611)
Andrew Reynolds [Mon, 24 May 2021 18:51:09 +0000 (13:51 -0500)]
Move proof utilities to src/proof/ (#6611)

This moves all generic proof utilites from src/expr/ and src/theory/ to src/proof/.

It also changes the include for term conversion proof generator to conv_proof_generator in preparation to rename this utility on a followup PR (to avoid confusion with the use of "Term").

3 years agoFix re-elim length requirement for symbolic RE memberships (#6609)
Andrew Reynolds [Mon, 24 May 2021 16:15:12 +0000 (11:15 -0500)]
Fix re-elim length requirement for symbolic RE memberships (#6609)

Fixes #6604.

Previously, re-elim was solution unsound for cases where the LHS and a component of the RHS were both empty. This ensures a length requirement is given for the LHS to ensure proper containment.

3 years agoFix instance of no rewrite in extended rewriter (#6610)
Andrew Reynolds [Mon, 24 May 2021 15:55:17 +0000 (10:55 -0500)]
Fix instance of no rewrite in extended rewriter (#6610)

Fixes #6545.

An assertion failure was being raised indicating that we were reporting a rewrite that was not changing the original term.

3 years agoBetter formalization of regular expression unfolding skolems (#6602)
Andrew Reynolds [Mon, 24 May 2021 14:39:56 +0000 (09:39 -0500)]
Better formalization of regular expression unfolding skolems (#6602)

This replaces our previous formalization of RE unfolding skolems with a more explicit one that is amenable to external proof conversion. It adds a few associated utility methods to SkolemManager required for LFSC proof conversion for RE_UNFOLD_POS.

It also changes the order of equalities in the RE_UNFOLD_POS rule, which simplifies LFSC proof checking.

3 years agoFix tests of unsat cores (#6593)
Andrew Reynolds [Fri, 21 May 2021 21:46:48 +0000 (16:46 -0500)]
Fix tests of unsat cores (#6593)

This updates all regressions that pass check-unsat-cores to enable check-unsat-cores. This includes any incremental benchmark, which was disabled in run_regression.py previously.

It adds --no-check-unsat-cores to a few corner benchmarks that were previously disabled based on --incremental.

It also reverts a change to when proofs are disabled: options like sygus-inference should not permit proofs (or unsat cores).

3 years agoFix and refactor relevant domain (#6528)
Andrew Reynolds [Fri, 21 May 2021 21:27:19 +0000 (16:27 -0500)]
Fix and refactor relevant domain (#6528)

In a handcrafted case, one can make the body of quantified formula another quantified formula when special attributes are used. The relevant domain utility was not robust to this case, leading to instantiations with free variables.

This fixes the issue and also updates its style to use a term context stack, which also avoids a tree traversal of the bodies of quantified formulas in this utility.

Fixes #6476. The benchmark from that issue now times out.

3 years agoFormalize shared selectors as skolem functions (#6591)
Andrew Reynolds [Fri, 21 May 2021 21:07:50 +0000 (16:07 -0500)]
Formalize shared selectors as skolem functions (#6591)

This is work towards properly printing shared selectors in external proofs.

3 years agoMinor simplification to boolean proof checker (#6590)
Andrew Reynolds [Fri, 21 May 2021 20:48:39 +0000 (15:48 -0500)]
Minor simplification to boolean proof checker (#6590)

3 years ago(proof-new) Minor documentation sync (#6592)
Andrew Reynolds [Fri, 21 May 2021 20:16:20 +0000 (15:16 -0500)]
(proof-new) Minor documentation sync (#6592)

3 years agoAdd utility to get all types occurring in a term (#6588)
Andrew Reynolds [Fri, 21 May 2021 18:04:49 +0000 (13:04 -0500)]
Add utility to get all types occurring in a term (#6588)

Required for external proof conversions.

3 years agoUpdate to sygus standard output for check-synth responses (#6521)
Andrew Reynolds [Fri, 21 May 2021 17:15:28 +0000 (12:15 -0500)]
Update to sygus standard output for check-synth responses (#6521)

This PR does two things:
(1) It eliminates the ad-hoc implementation of printSynthSolutions and removes it from the API. Now, printing response to a check-synth command is done in a more standard way, using the API + symbol manager. This is analogous to recent refactoring to get-model.
(2) It updates cvc5's output in response to check-synth to be compliant with the upcoming sygus 2.1 standard. The standard has changed slightly: responses to check-synth are now closed in parentheses, mirroring the smt2 response to get-model.

It also removes the unused command GetSynthSolutionCommand.

3 years agoSupport braced-init-lists with `mkNode()` (#6580)
Andres Noetzli [Fri, 21 May 2021 16:05:45 +0000 (09:05 -0700)]
Support braced-init-lists with `mkNode()` (#6580)

This commit adds support for braced-init-lists in calls to `mkNode()`,
e.g., `mkNode(REGEXP_EMPTY, {})`. Previously, such a call would result
in a node of kind `REGEXP_EMPTY` with a single null node as a child
because the compiler chose the `mkNode(Kind kind, TNode child1)` variant
and converted `{}` to a node using the default constructor. This commit
adds an overload of `mkNode()` that takes an `initializer_list<TNode>`
to allow this use case. It also adds a `mkNode()` overload with zero children
for convenience and removes the 4- and 5-children variants because they
saw little use. Finally, it makes the default constructor of `NodeTemplate`
explicit to avoid accidental conversions.

3 years agoapi docs: Tweak and fix style. (#6582)
Aina Niemetz [Fri, 21 May 2021 10:19:10 +0000 (03:19 -0700)]
api docs: Tweak and fix style. (#6582)

This fixes the style for narrow layouts. It further fixes and improves
the style for the menu.

3 years agoapi docs: Update copyright. (#6596)
Aina Niemetz [Fri, 21 May 2021 08:02:57 +0000 (01:02 -0700)]
api docs: Update copyright. (#6596)

3 years agoUse scikit-build CMake files for pycvc5 (#6543)
makaimann [Fri, 21 May 2021 04:20:30 +0000 (00:20 -0400)]
Use scikit-build CMake files for pycvc5 (#6543)

This PR removes copied CMake files for the pycvc5 Cython target, and instead adds a dependency on scikit-build (where those CMake files originated anyway). This keeps us up to date with fixes. Furthermore, the PR switches from distutils to the more modern setuptools. This does add another dependency but it's a fairly reasonable one. setuptools is not part of the base Python distribution, but my understanding is that it is now the de facto standard, and most package managers install it automatically with Python. The main motivation for switching is in preparation for building wheels.

This PR is a piece of this old one (#5657) which I am closing and splitting up.

3 years agoMove option names out of struct (#6554)
Gereon Kremer [Fri, 21 May 2021 03:22:40 +0000 (05:22 +0200)]
Move option names out of struct (#6554)

This PR moves the option names out of the option struct (which will be removed) to free constexpr string constants.

3 years agoBV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)
Aina Niemetz [Fri, 21 May 2021 00:41:50 +0000 (17:41 -0700)]
BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)

3 years agoUpdate version of CaDiCaL. (#6583)
Mathias Preiner [Thu, 20 May 2021 22:53:02 +0000 (15:53 -0700)]
Update version of CaDiCaL. (#6583)

3 years agoDisable unit testing for clang builds. (#6595)
Aina Niemetz [Thu, 20 May 2021 22:26:49 +0000 (15:26 -0700)]
Disable unit testing for clang builds. (#6595)

We currently have issues with clang 11 failing for white unit tests.
This disables unit tests for clang builds.

3 years agoProperly initialize. (#6586)
Gereon Kremer [Thu, 20 May 2021 18:50:50 +0000 (20:50 +0200)]
Properly initialize. (#6586)

This PR fixes a missing initialization that lead to a valgrind warning.

3 years agoRemove old unsat cores (#6581)
Haniel Barbosa [Thu, 20 May 2021 18:29:32 +0000 (15:29 -0300)]
Remove old unsat cores (#6581)

This commit removes the remaining old proof code and the code to produce unsat cores based on it.

3 years agoUse most recent version of libpoly (#6587)
Gereon Kremer [Thu, 20 May 2021 17:55:35 +0000 (19:55 +0200)]
Use most recent version of libpoly (#6587)

This PR updates to the most recent version of libpoly which fixes some memory leaks.

3 years agoAvoid using printSynthSolution in the python API and examples (#6564)
yoni206 [Thu, 20 May 2021 15:29:27 +0000 (08:29 -0700)]
Avoid using printSynthSolution in the python API and examples (#6564)

The function printSynthSolution declared here is going to be removed in #6521.

This PR removes it from the python API.
Following #6530, this PR also replaces its usages in the examples by a utility function.
For this, we also add support for getSynthSolutions in the python API.

3 years agoMinor improvements to the API (#6585)
Gereon Kremer [Thu, 20 May 2021 14:29:17 +0000 (16:29 +0200)]
Minor improvements to the API (#6585)

This PR does some minor improvements to the API:
- remove getConstSequenceElements(), use getSequenceValue() instead
- improve documentation for Term

3 years agoFix echo printing. (#6573)
Aina Niemetz [Thu, 20 May 2021 02:54:52 +0000 (19:54 -0700)]
Fix echo printing. (#6573)

Previously, echo surpressed leading, trailing and escape quotes of the
string to print. However, the SMT-LIB standard states that the string is
to be printed as is, including those quote characters.

3 years agoAdd more getters for api::Term (#6496)
Gereon Kremer [Thu, 20 May 2021 02:08:56 +0000 (04:08 +0200)]
Add more getters for api::Term (#6496)

This PR adds more getter functions for api::Term to retrieve values from constant terms (and terms that the average API use might consider constant).
It also introduces std::wstring as regular representation for string constants instead of std::vector<uint32> for the SMT-LIB parser and the String class.

3 years agoExpand arith's farkas lemma rule as a macro (#6577)
Alex Ozdemir [Thu, 20 May 2021 01:16:12 +0000 (18:16 -0700)]
Expand arith's farkas lemma rule as a macro (#6577)

reflects that it is a macro, which we will eliminate

3 years agoRemove unused methods from `NodeManager` (#6578)
Andres Noetzli [Wed, 19 May 2021 23:40:59 +0000 (16:40 -0700)]
Remove unused methods from `NodeManager` (#6578)

3 years agoCorrectly handle negated assertions for assumption-based unsat cores. (#6579)
Mathias Preiner [Wed, 19 May 2021 23:32:25 +0000 (16:32 -0700)]
Correctly handle negated assertions for assumption-based unsat cores. (#6579)

3 years agoPass empty vector when constructing re empty, fixes rewrite (#6576)
Andrew Reynolds [Wed, 19 May 2021 22:50:43 +0000 (17:50 -0500)]
Pass empty vector when constructing re empty, fixes rewrite (#6576)

Fixes #6567.

3 years agoAdding python API test part 4 (#6553)
Ying Sheng [Wed, 19 May 2021 22:15:45 +0000 (15:15 -0700)]
Adding python API test part 4 (#6553)

This commit (follow #6552) adds more unit tests for python API.
Subsequent commits will include additional missing functions and unit tests.

3 years agoMake output list of `mkoptions.py` more accurate (#6572)
Andres Noetzli [Wed, 19 May 2021 21:53:27 +0000 (14:53 -0700)]
Make output list of `mkoptions.py` more accurate (#6572)

After commit 6dc5b74, cvc5 was always
being almost completely rebuilt, even if there hadn't been any changes
if cvc5 was configured not to produce documentation (the default).
This was because mkoptions.py only produces the
options_generated.rst file when documentation is enabled. However, it
was unconditionally declared to be an output of the script in
CMakeLists.txt. As a result, the options (and thus most of the code
base) were rebuilt every time because the file was missing in builds
without documentation. This commit modifies the output list depending on
the configuration.

3 years agoMake strings emp inference an unhandled inference for proofs (#6575)
Andrew Reynolds [Wed, 19 May 2021 21:33:06 +0000 (16:33 -0500)]
Make strings emp inference an unhandled inference for proofs (#6575)

The strings inference id STRINGS_INFER_EMP is a rare inference that currently leads to a segfault when proof reconstruction is tried for it. This PR makes it unhandled.

This was caught by a new regression on the soon-to-be-merged jh-new branch.

3 years agoAdding regressions that failed on old unsat cores (#6574)
Haniel Barbosa [Wed, 19 May 2021 21:05:07 +0000 (18:05 -0300)]
Adding regressions that failed on old unsat cores (#6574)

We can thus close #3455, #3651, #4925, #5079, #5238, #5902, #5908, and #5604.

3 years agoChange the default unsat cores (#6571)
Haniel Barbosa [Wed, 19 May 2021 20:25:18 +0000 (17:25 -0300)]
Change the default unsat cores (#6571)

This commit changes the default unsat cores to those based on solving-under-assumptions in the SAT solver and the (new) preprocessing proofs.

The evaluation below on all the non-fp non-incremental SMT-LIB benchmarks, 120s timeout, shows the differences of the unsat cores based on the old proofs, the new ones based on SAT assumptions + preprocessing proofs, and the new ones based on SAT and preprocessing proofs. Note that the union of the last two is on par with the first.

```
                                      status  total  solved   sat  unsat  best  timeout  memout  error  uniq  disagr  time_cpu    memory
benchmark config
AUFDTLIRA newUnsatCoresAssumps-safe/     ee     35       4     0      4     4        7       0     23     2       0     954.0    1267.5
          newUnsatCoresProofs            ok     35      31     0     31    25        4       0      0     0       0     894.1    1692.9
          oldUnsatCores                  ok     35      32     0     32    30        3       0      0     1       0     799.2    1428.5
AUFLIA    newUnsatCoresAssumps-safe/     ok     11       7     0      7     7        4       0      0     7       0     532.2    7604.4
          newUnsatCoresProofs            ok     11       4     0      4     1        6       0      0     0       0     829.0   12459.8
          oldUnsatCores                  ok     11       4     0      4     3        6       0      0     0       0     818.2    7764.4
AUFLIRA   newUnsatCoresAssumps-safe/     to      2       0     0      0     0        2       0      0     0       0     241.6     125.6
          newUnsatCoresProofs            ok      2       2     0      2     1        0       0      0     0       0      54.2      45.5
          oldUnsatCores                  ok      2       2     0      2     2        0       0      0     0       0      49.4      79.7
AUFNIRA   newUnsatCoresAssumps-safe/     ok     10       5     0      5     5        5       0      0     2       0     748.4    1630.0
          newUnsatCoresProofs            ok     10       4     0      4     0        6       0      0     0       0     850.7    2978.8
          oldUnsatCores                  ok     10       8     0      8     5        2       0      0     1       0     502.7    2048.5
BV        newUnsatCoresAssumps-safe/     ok      7       1     1      0     1        6       0      0     1       0     734.2    2065.0
          newUnsatCoresProofs            ok      7       6     3      3     4        1       0      0     0       0     246.7    1023.9
          oldUnsatCores                  ok      7       6     3      3     3        1       0      0     0       0     248.6     992.0
LIA       newUnsatCoresAssumps-safe/     to      1       0     0      0     0        1       0      0     0       0     120.9      47.7
          newUnsatCoresProofs            ok      1       1     0      1     1        0       0      0     0       0       0.3       6.5
          oldUnsatCores                  ok      1       1     0      1     1        0       0      0     0       0       0.3       5.3
LRA       newUnsatCoresAssumps-safe/     ok      5       3     0      3     3        2       0      0     3       0     450.7     260.4
          newUnsatCoresProofs            ok      5       2     0      2     0        3       0      0     0       0     537.8     424.5
          oldUnsatCores                  ok      5       2     0      2     2        3       0      0     0       0     533.8     298.5
NIA       newUnsatCoresAssumps-safe/     to      1       0     0      0     0        1       0      0     0       0     120.8      22.0
          newUnsatCoresProofs            ok      1       1     0      1     0        0       0      0     0       0      46.3      48.0
          oldUnsatCores                  ok      1       1     0      1     1        0       0      0     0       0      43.3      40.3
QF_ABV    newUnsatCoresAssumps-safe/     ok    105      70    59     11    70       35       0      0    63       0    8195.5   19363.3
          newUnsatCoresProofs            ok    105      34    24     10    17       71       0      0     5       0   11099.5   35756.7
          oldUnsatCores                  ok    105      37    23     14    18       69       0      0     1       0   11198.0   26878.1
QF_ANIA   newUnsatCoresAssumps-safe/     to      4       0     0      0     0        4       0      0     0       0     483.5    1631.8
          newUnsatCoresProofs            ok      4       4     3      1     2        0       0      0     0       0     175.1    1513.6
          oldUnsatCores                  ok      4       4     3      1     3        0       0      0     0       0     173.8    1495.1
QF_AUFLIA newUnsatCoresAssumps-safe/     ok     35       6     1      5     6       29       0      0     3       0    3718.4     524.1
          newUnsatCoresProofs            ok     35      24     4     20     1       11       0      0     0       0    2357.2   36556.0
          oldUnsatCores                  ok     35      32     5     27    29        3       0      0     5       0    1857.6   10067.7
QF_AUFNIA newUnsatCoresAssumps-safe/     ok      3       1     0      1     1        2       0      0     0       0     324.7     543.6
          newUnsatCoresProofs            ok      3       2     2      0     1        1       0      0     1       0     223.1     509.0
          oldUnsatCores                  ok      3       2     1      1     1        1       0      0     0       0     268.5     484.3
QF_AX     newUnsatCoresAssumps-safe/     ok     12       1     0      1     1       11       0      0     0       0    1379.2     391.3
          newUnsatCoresProofs            ok     12      10     0     10     0        2       0      0     0       0     528.7    7433.9
          oldUnsatCores                  ok     12      12     0     12    11        0       0      0     1       0     343.0    2855.2
QF_BV     newUnsatCoresAssumps-safe/     ok     96      56    30     26    49       39       2      0    35       0    9248.2   98058.7
          newUnsatCoresProofs            ok     96      37    26     11    23       52       7      0     7       0    9781.9  135924.7
          oldUnsatCores                  ok     96      50    29     21    24       43       3      0     7       0    9155.6  107216.0
QF_IDL    newUnsatCoresAssumps-safe/     ok    109      51    39     12    43       58       0      0    33       0   10427.2   50846.5
          newUnsatCoresProofs            ok    109      33    32      1     2       76       0      0     0       0   11692.8  108963.1
          oldUnsatCores                  ok    109      75    55     20    64       34       0      0    26       0   10088.1   53105.6
QF_LIA    newUnsatCoresAssumps-safe/     ok    306     155   111     44   138      151       0      0   119       0   25346.4   50556.0
          newUnsatCoresProofs            ok    306     117    95     22    49      189       0      0     0       0   27092.6  122894.9
          oldUnsatCores                  ok    306     187   110     77   152      119       0      0    34       0   24521.0   61261.1
QF_LRA    newUnsatCoresAssumps-safe/     ok     72      39    20     19    38       33       0      0    31       0    7475.3   16892.2
          newUnsatCoresProofs            ok     72      31    16     15     2       41       0      0     0       0    7569.3   35658.7
          oldUnsatCores                  ok     72      41    18     23    32       31       0      0     2       0    7243.2   20593.9
QF_NIA    newUnsatCoresAssumps-safe/     ok   4389    2009  1862    147  2002      903       0      0  1931       0  163975.7  280779.3
          newUnsatCoresProofs            ok   4389    2326  2156    170   752      792       0      0    37       0  151051.9  387779.8
          oldUnsatCores                  ok   4389    2394  2199    195  2174      730       0      0    81       0  146419.3  259669.8
QF_NRA    newUnsatCoresAssumps-safe/     ok    135      65    57      8    57       70       0      0    45       0   10195.7   24701.4
          newUnsatCoresProofs            ok    135      71    49     22    35       64       0      0     5       0   10825.3   32982.8
          oldUnsatCores                  ok    135      75    54     21    51       61       0      0     9       0   10865.3   27260.9
QF_RDL    newUnsatCoresAssumps-safe/     ok      7       5     1      4     5        2       0      0     1       0     564.7     958.4
          newUnsatCoresProofs            ok      7       1     1      0     0        6       0      0     0       0     842.0   11029.6
          oldUnsatCores                  ok      7       6     1      5     2        1       0      0     1       0     665.8    1982.6
QF_S      newUnsatCoresAssumps-safe/     ok      5       1     1      0     0        4       0      0     0       0     603.3     191.4
          newUnsatCoresProofs            ok      5       5     5      0     2        0       0      0     0       0     161.9     285.8
          oldUnsatCores                  ok      5       4     4      0     3        1       0      0     0       0     225.9     219.3
QF_SLIA   newUnsatCoresAssumps-safe/     ok    258      74    67      7    70      184       0      0    64       0   27245.9   20290.4
          newUnsatCoresProofs            ok    258     179   163     16    47       79       0      0     6       0   18996.0   33722.6
          oldUnsatCores                  ok    258     184   162     22   149       74       0      0     9       0   18395.8   23004.3
QF_UF     newUnsatCoresAssumps-safe/     ok     29      25     0     25     6        4       0      0     2       0    2362.4    7504.3
          newUnsatCoresProofs            ok     29       0     0      0     0       28       1      0     0       0    3508.0  124190.7
          oldUnsatCores                  ok     29      27     0     27    23        2       0      0     4       0    1866.3   13635.1
QF_UFBV   newUnsatCoresAssumps-safe/     ok      2       2     0      2     1        0       0      0     1       0     189.5    1599.3
          newUnsatCoresProofs            to      2       0     0      0     0        2       0      0     0       0     241.8    1818.8
          oldUnsatCores                  ok      2       1     0      1     1        1       0      0     0       0     193.7    1500.9
QF_UFIDL  newUnsatCoresAssumps-safe/     ok      9       9     0      9     7        0       0      0     4       0     697.0    1133.0
          newUnsatCoresProofs            to      9       0     0      0     0        9       0      0     0       0    1088.0   14652.6
          oldUnsatCores                  ok      9       5     0      5     2        4       0      0     0       0     848.5    2079.6
QF_UFLIA  newUnsatCoresAssumps-safe/     ok      1       1     0      1     0        0       0      0     0       0     117.1      76.4
          newUnsatCoresProofs            to      1       0     0      0     0        1       0      0     0       0     120.9     208.5
          oldUnsatCores                  ok      1       1     0      1     1        0       0      0     0       0     110.6     127.7
QF_UFLRA  newUnsatCoresAssumps-safe/     ok      7       4     1      3     0        0       3      0     0       0     266.6   55098.3
          newUnsatCoresProofs            mo      7       0     0      0     0        0       7      0     0       0     261.7   56000.0
          oldUnsatCores                  ok      7       7     4      3     7        0       0      0     3       0     408.4   20933.4
QF_UFNIA  newUnsatCoresAssumps-safe/     ok     48      21    19      2    21        4       0      0    20       0     592.3     880.6
          newUnsatCoresProofs            ok     48      27    22      5    18        4       0      0     1       0     641.4    1548.8
          oldUnsatCores                  ok     48      26    21      5    26        7       0      0     1       0     887.5    1044.6
QF_UFNRA  newUnsatCoresAssumps-safe/     ok      1       1     1      0     1        0       0      0     1       0     108.3      17.9
          newUnsatCoresProofs            to      1       0     0      0     0        1       0      0     0       0     120.8      19.0
          oldUnsatCores                  to      1       0     0      0     0        1       0      0     0       0     120.8      14.7
UF        newUnsatCoresAssumps-safe/     ok     21       5     0      5     5       16       0      0     5       0    2123.8    3168.7
          newUnsatCoresProofs            ok     21      13     0     13     6        8       0      0     0       0    1496.3    6617.8
          oldUnsatCores                  ok     21      16     0     16    11        5       0      0     3       0    1443.3    3919.2
UFDT      newUnsatCoresAssumps-safe/     ok     35       6     0      6     6       29       0      0     5       0    3777.0    4485.5
          newUnsatCoresProofs            ok     35      28     0     28    15        7       0      0     0       0    1416.9    4293.6
          oldUnsatCores                  ok     35      30     0     30    26        5       0      0     1       0    1406.9    3188.5
UFDTLIA   newUnsatCoresAssumps-safe/     to      4       0     0      0     0        4       0      0     0       0     483.5    1640.5
          newUnsatCoresProofs            ok      4       4     0      4     1        0       0      0     0       0     139.3     942.3
          oldUnsatCores                  ok      4       4     0      4     3        0       0      0     0       0     156.4     851.8
UFDTLIRA  newUnsatCoresAssumps-safe/     ok      1       1     0      1     1        0       0      0     1       0       0.0       3.1
          newUnsatCoresProofs            ok      1       0     0      0     0        0       0      0     0       0       0.0       3.2
          oldUnsatCores                  ok      1       0     0      0     0        0       0      0     0       0       0.0       2.7
UFDTNIRA  newUnsatCoresAssumps-safe/     ok     10       3     0      3     3        6       0      0     3       0     754.8    1386.9
          newUnsatCoresProofs            ok     10       7     0      7     5        3       0      0     0       0     377.0     848.8
          oldUnsatCores                  ok     10       7     0      7     7        3       0      0     0       0     376.5     563.4
UFLIA     newUnsatCoresAssumps-safe/     ok     24       8     0      8     8       16       0      0     8       0    2231.6    3179.2
          newUnsatCoresProofs            ok     24      14     0     14     3       10       0      0     1       0    1915.5    5131.1
          oldUnsatCores                  ok     24      15     0     15    14        9       0      0     2       0    1857.5    3479.7
UFNIA     newUnsatCoresAssumps-safe/     ok    354     183    28    155   116      133       0      0   113       0   25941.4  839089.7
          newUnsatCoresProofs            ok    354     107    17     90    28      107      92      0     2       0   23496.9 1020258.1
          oldUnsatCores                  ok    354     237    19    218   233       72       0      0    66       0   19906.9  914273.0
```

3 years agoAdding python API test part 3 (#6552)
Ying Sheng [Wed, 19 May 2021 20:08:54 +0000 (13:08 -0700)]
Adding python API test part 3 (#6552)

This commit (follow #6551) adds more unit tests for python API.
Subsequent commits will include additional missing functions and unit tests.

3 years agoFix strings rewriter for non-standard re range (#6570)
Andrew Reynolds [Wed, 19 May 2021 19:42:21 +0000 (14:42 -0500)]
Fix strings rewriter for non-standard re range (#6570)

Fixes #6561.

Previously we missed a case where a rewrite fired for (re.range x x) where x is not a character.

3 years agoAdd more missing inference ids (#6313)
Andrew Reynolds [Wed, 19 May 2021 18:39:59 +0000 (13:39 -0500)]
Add more missing inference ids (#6313)

This also makes the relations solver use the inference manager in the standard way.

3 years agobv: Add support for --bitblast=eager. (#6516)
Mathias Preiner [Wed, 19 May 2021 17:21:42 +0000 (10:21 -0700)]
bv: Add support for --bitblast=eager. (#6516)

This PR adds support for handling --bitblast=eager in the new bitblast solver.

3 years agoFix positive contains indexof rewrites for empty string second argument (#6566)
Andrew Reynolds [Wed, 19 May 2021 17:12:28 +0000 (12:12 -0500)]
Fix positive contains indexof rewrites for empty string second argument (#6566)

Fixes #6560.

3 years agoRemove accidental print (#6568)
Gereon Kremer [Wed, 19 May 2021 14:00:10 +0000 (16:00 +0200)]
Remove accidental print (#6568)

3 years agoGenerate command line options for sphinx docs (#6555)
Gereon Kremer [Wed, 19 May 2021 05:55:53 +0000 (07:55 +0200)]
Generate command line options for sphinx docs (#6555)

This PR adds documentation about the command line options to the sphinx documentation. It is mostly a reformatted version of what --help would print.