cvc5.git
3 years agoAllow changing certain options while solving (#6945)
Gereon Kremer [Fri, 30 Jul 2021 17:23:44 +0000 (10:23 -0700)]
Allow changing certain options while solving (#6945)

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

3 years agoSimplify smt2 printer (#6954)
Andrew Reynolds [Fri, 30 Jul 2021 17:13:07 +0000 (12:13 -0500)]
Simplify smt2 printer (#6954)

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

3 years agoIntegrate installation instructions into documentation (#6814)
Gereon Kremer [Thu, 29 Jul 2021 19:40:00 +0000 (12:40 -0700)]
Integrate installation instructions into documentation (#6814)

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

3 years agoquickstart: Add python example to docs. (#6949)
Aina Niemetz [Thu, 29 Jul 2021 17:45:25 +0000 (10:45 -0700)]
quickstart: Add python example to docs. (#6949)

3 years ago[proofs] Set BV solver to better proof-producing one when proofs on (#6903)
Haniel Barbosa [Thu, 29 Jul 2021 17:22:10 +0000 (14:22 -0300)]
[proofs] Set BV solver to better proof-producing one when proofs on (#6903)

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

3 years agoPython quick start example (#6939)
yoni206 [Thu, 29 Jul 2021 16:43:30 +0000 (09:43 -0700)]
Python quick start example (#6939)

This is a translation of quickstart.cpp to python.

3 years agoIntegrate central equality engine approach into theory engine, add option and regress...
Andrew Reynolds [Thu, 29 Jul 2021 16:11:05 +0000 (11:11 -0500)]
Integrate central equality engine approach into theory engine, add option and regressions (#6943)

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

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

3 years agoMinor updates to shared terms database for central equality engine (#6929)
Andrew Reynolds [Thu, 29 Jul 2021 15:53:48 +0000 (10:53 -0500)]
Minor updates to shared terms database for central equality engine (#6929)

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

3 years agoFixes for building python wheels on manylinux2014 (#6947)
makaimann [Wed, 28 Jul 2021 22:13:43 +0000 (18:13 -0400)]
Fixes for building python wheels on manylinux2014 (#6947)

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

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

3 years agoMinor changes to arrays in preparation for central equality engine (#6917)
Andrew Reynolds [Wed, 28 Jul 2021 21:50:08 +0000 (16:50 -0500)]
Minor changes to arrays in preparation for central equality engine (#6917)

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

We should probably performance test this.

FYI @barrettcw

3 years agoOnly use libedit on tty inputs (#6946)
Gereon Kremer [Wed, 28 Jul 2021 21:41:22 +0000 (14:41 -0700)]
Only use libedit on tty inputs (#6946)

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

3 years agoPrint link to docs preview (#6922)
Andres Noetzli [Wed, 28 Jul 2021 21:28:25 +0000 (14:28 -0700)]
Print link to docs preview (#6922)

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

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

3 years agoMake extended rewriter methods const (#6948)
Andrew Reynolds [Wed, 28 Jul 2021 21:00:49 +0000 (16:00 -0500)]
Make extended rewriter methods const (#6948)

3 years agobv: Refactor getEqualityStatus and use for both bitblasting solvers. (#6933)
Mathias Preiner [Tue, 27 Jul 2021 20:23:32 +0000 (13:23 -0700)]
bv: Refactor getEqualityStatus and use for both bitblasting solvers. (#6933)

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

3 years agoproof: Add eqrange expansion rule. (#6936)
Mathias Preiner [Tue, 27 Jul 2021 19:39:53 +0000 (12:39 -0700)]
proof: Add eqrange expansion rule. (#6936)

Adds proof support for the eqrange operator.

Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
3 years agoTrack instantiation reasons in proofs (#6935)
Andrew Reynolds [Tue, 27 Jul 2021 17:24:17 +0000 (12:24 -0500)]
Track instantiation reasons in proofs (#6935)

This adds optional arguments to INSTANTIATE steps in proofs to track fine-grained reasons for relevant instantiations.

Also simplifies an old argument modEq which was unused.

FYI @MikolasJanota

3 years agoAdd basic LFSC utilities (#6879)
Andrew Reynolds [Tue, 27 Jul 2021 15:30:31 +0000 (10:30 -0500)]
Add basic LFSC utilities (#6879)

Adds basic utilities in preparation for the LFSC proof conversion.

Depends on #6881, review that first.

3 years agoMove enum value generator to own file (#6941)
Andrew Reynolds [Tue, 27 Jul 2021 14:51:02 +0000 (09:51 -0500)]
Move enum value generator to own file (#6941)

Work towards integrating the enumerator callback into the fast enumerator.

3 years agoMinor fix for term database + central equality engine (#6928)
Andrew Reynolds [Tue, 27 Jul 2021 14:24:20 +0000 (09:24 -0500)]
Minor fix for term database + central equality engine (#6928)

Previously we provided a bogus (self) explanation in a rare case of setting up the term database for higher order. This is incompatible with cases where central equality engine = master equality engine.

3 years agoRevert change to regression (#6940)
Andrew Reynolds [Tue, 27 Jul 2021 14:06:33 +0000 (09:06 -0500)]
Revert change to regression (#6940)

Although it works on most machines, it times out in the nightly builds.

3 years agoMake all dependencies in the fast enumerator optional (#6918)
Andrew Reynolds [Tue, 27 Jul 2021 13:50:38 +0000 (08:50 -0500)]
Make all dependencies in the fast enumerator optional (#6918)

This allows one to use a fast enumerator without having access to sygus term database, statistics, etc.

3 years agoAdd print expression utility (#6880)
Andrew Reynolds [Tue, 27 Jul 2021 13:33:23 +0000 (08:33 -0500)]
Add print expression utility (#6880)

This will be used in the LFSC printer. It may be of general use to other proof printers.

3 years agoAdd regression for fixed `str.indexof_re` issue (#6938)
Andres Noetzli [Tue, 27 Jul 2021 11:57:02 +0000 (04:57 -0700)]
Add regression for fixed `str.indexof_re` issue (#6938)

Fixes #6639. The issue cannot be reproduced on current master and git bisect suggests that commit adf497a
fixed the issue.

3 years agoMinor changes from proof-new (#6937)
Andrew Reynolds [Tue, 27 Jul 2021 06:36:18 +0000 (01:36 -0500)]
Minor changes from proof-new (#6937)

Note the change to the unit test makes it so the test is not dependent on Node ID order.

3 years agoMiscellaneous fixes from proof-new (#6914)
Andrew Reynolds [Tue, 27 Jul 2021 01:52:15 +0000 (20:52 -0500)]
Miscellaneous fixes from proof-new (#6914)

3 years agoAdd proof letify utility (#6881)
Andrew Reynolds [Tue, 27 Jul 2021 01:31:21 +0000 (20:31 -0500)]
Add proof letify utility (#6881)

Towards support for external proof conversions.

3 years agoFix eq proof conversion for constant merged parameterized ops (#6926)
Andrew Reynolds [Tue, 27 Jul 2021 01:21:20 +0000 (20:21 -0500)]
Fix eq proof conversion for constant merged parameterized ops (#6926)

This issue arises when using the central equality engine on several regressions.

3 years agoDefault equality proofs for bags and separation logic (#6932)
Andrew Reynolds [Tue, 27 Jul 2021 00:48:03 +0000 (19:48 -0500)]
Default equality proofs for bags and separation logic (#6932)

This is the last 2 remaining theories not to use the default handling of equality proofs.

In preparation for proofs in central equality engine.

3 years agoAdd sygus enumerator callback (#6923)
Andrew Reynolds [Tue, 27 Jul 2021 00:20:40 +0000 (19:20 -0500)]
Add sygus enumerator callback (#6923)

This class will make the uses of the fast enumerator customizable.

3 years agoMove public options functions to separate file (#6671)
Gereon Kremer [Mon, 26 Jul 2021 23:42:20 +0000 (16:42 -0700)]
Move public options functions to separate file (#6671)

This PR moves the remaining special purpose functions out of the Options class. This set of functions is only used to implement API functions in the smt engine (getting and setting options by string), and by the main driver for parsing and printing usage information.

3 years agoEnable default equality proofs for sets (#6931)
Andrew Reynolds [Mon, 26 Jul 2021 21:03:48 +0000 (16:03 -0500)]
Enable default equality proofs for sets (#6931)

This enables default support for equality proofs in the theory of sets.

This is in preparation for proofs in the central equality engine, which requires that all active theories that use the central equality engine at least support the default interaction with the equality engine.

3 years agoMore updates to arithmetic in preparation for central equality engine (#6927)
Andrew Reynolds [Mon, 26 Jul 2021 18:26:55 +0000 (13:26 -0500)]
More updates to arithmetic in preparation for central equality engine (#6927)

Makes arithEqSolver more robust to propagations from multiple sources, changes the default relationship to congruence manager based on preliminary results on SMT-LIB.

3 years agoChanges to datatypes in preparation for central equality engine (#6901)
Andrew Reynolds [Sun, 25 Jul 2021 16:04:00 +0000 (11:04 -0500)]
Changes to datatypes in preparation for central equality engine (#6901)

This adds changes from the centralEeDev branch for datatypes.

The changes in behavior are that the inference manager clears its pending inferences when the state is in conflict, and preCheck processes pending facts immediately (which may have been enqueued prior to the call to check via ee merges). These are required to make datatypes robust to the order in which check / merge / backtracks can occur.

3 years agoRefactor equality engine setup for arithmetic congruence manager (#6902)
Andrew Reynolds [Sun, 25 Jul 2021 14:54:28 +0000 (09:54 -0500)]
Refactor equality engine setup for arithmetic congruence manager (#6902)

Allows congruence manager to use its own (non-official) equality engine if both it and the arithmetic equality solver are enabled.

3 years agoFix CLN build (#6920)
Andres Noetzli [Sat, 24 Jul 2021 00:06:51 +0000 (17:06 -0700)]
Fix CLN build (#6920)

Currently, the CLN `CONFIGURE_COMMAND` chains multiple commands using
`&&` but this does not seem to work with CMake 3.20.4 and CMake 3.19.7
and is also not the recommended way of doing it. The commit fixes the
issue by using additional `COMMAND`s and also switches to using the
CMake's `chdir` instead of `cd`.

3 years agoConfiguration: Indicate dependencies being built (#6921)
Andres Noetzli [Fri, 23 Jul 2021 20:57:42 +0000 (13:57 -0700)]
Configuration: Indicate dependencies being built (#6921)

This commit changes the output of our configuration to show which
dependencies are being built as part of the cvc5 build. For example:

```
ABC                       : off
CryptoMiniSat             : off
GLPK                      : off
Kissat                    : off
LibPoly                   : on (local)
CoCoALib                  : off

Build libcvc5 only        : off
MP library                : gmp (system)
Editline                  : off
```

Indicates that `LibPoly` was not found in the system and is thus built
as part of the cvc5 build and GMP was found in the system.

3 years agoFix CoCoA build for newer compilers (#6919)
Andres Noetzli [Fri, 23 Jul 2021 20:47:16 +0000 (13:47 -0700)]
Fix CoCoA build for newer compilers (#6919)

Newer compilers, such as GCC 11, default to C++17. CoCoA does not
compile with C++17 and its check for the C++ version used by the
compiler does not take into account newer C++ versions. As a result,
building CoCoA using `--auto-download` fails with GCC 11. This commit
adds a patch that makes the test in CoCoA take into account compilers
that default to C++17 or newer.

3 years agoFP: Add option to word-blast more lazily. (#6904)
Aina Niemetz [Fri, 23 Jul 2021 17:51:22 +0000 (10:51 -0700)]
FP: Add option to word-blast more lazily. (#6904)

When enabled, this does not word-blast when registering term but at preNotifyFact (= more lazily) instead.
This is enabled via option --fp-lazy-wb.

3 years agoSimplify computation of relevant terms in datatypes (#6885)
Andrew Reynolds [Thu, 22 Jul 2021 16:57:46 +0000 (11:57 -0500)]
Simplify computation of relevant terms in datatypes (#6885)

This makes it so that we do not consider non-singleton equivalence classes of DT for non-datatype terms to be relevant. This impacts how model construction is done for datatypes.

It's not clear why this method considered such terms to be relevant, I believe this was done to mask a previous bug; regressions now pass when this method is simplified.

Doing this is definitely wrong when using central equality engine, hence the motivation for this simplification.

3 years agoAdd the central equality engine manager (#6893)
Andrew Reynolds [Thu, 22 Jul 2021 14:23:35 +0000 (09:23 -0500)]
Add the central equality engine manager (#6893)

This class is responsible for setting up the central equality engine. It relies on a new static method Theory::usesCentralEqualityEngine, which will be refined in followup PRs.

This PR does not change the behavior, it only adds the class.

Further PRs will connect this class to CombinationEngine, make it optionally enabled, and make the remaining changes to TheoryEngine to make it compatible.

3 years agoMiscellaneous changes in preparation for central equality engine (#6900)
Andrew Reynolds [Thu, 22 Jul 2021 13:59:17 +0000 (08:59 -0500)]
Miscellaneous changes in preparation for central equality engine (#6900)

3 years agoAdd support for minimal unsat cores (#4605)
Andres Noetzli [Thu, 22 Jul 2021 07:50:02 +0000 (00:50 -0700)]
Add support for minimal unsat cores (#4605)

This commit adds support for computing minimal unsat cores. The
algorithm implemented in this commit is just a trivial deletion-based
algorithm that tries to remove each assertion in the unsat core
individually.

3 years agoPreparation for carry the rewrite rule database in the proof checker (#6915)
Andrew Reynolds [Thu, 22 Jul 2021 07:22:02 +0000 (02:22 -0500)]
Preparation for carry the rewrite rule database in the proof checker (#6915)

3 years agoAdd std::vector<Term> Op:: getIndices() and operator[] for Op (#6397)
mudathirmahgoub [Thu, 22 Jul 2021 07:10:39 +0000 (02:10 -0500)]
Add std::vector<Term> Op:: getIndices() and operator[] for Op (#6397)

3 years ago[AUTHORS] Add CVC4 as part of CVC series (#6907)
Haniel Barbosa [Tue, 20 Jul 2021 17:36:41 +0000 (14:36 -0300)]
[AUTHORS] Add CVC4 as part of CVC series (#6907)

3 years agoANTLR3: Install into `CMAKE_INSTALL_LIBDIR` (#6912)
Andres Noetzli [Tue, 20 Jul 2021 16:11:15 +0000 (09:11 -0700)]
ANTLR3: Install into `CMAKE_INSTALL_LIBDIR` (#6912)

On some platforms, autotools installs ANTLR3's libraries into lib but
CMAKE_INSTALL_LIBDIR is set to lib64 (e.g., Fedora 33). This commit
sets --libdir to force autotools to install the library into the
directory specified by CMAKE_INSTALL_LIBDIR.

3 years ago'CryptoMiniSat_LIBRARIES' should respect lib/lib64 (#6905)
Andrew V. Jones [Mon, 19 Jul 2021 07:06:53 +0000 (08:06 +0100)]
'CryptoMiniSat_LIBRARIES' should respect lib/lib64 (#6905)

On 64-bit openSUSE (and maybe other distributions), the default install directory for static libraries is `lib64` *not* `lib`. This has an impact on cvc5 when it is automatically building CMS (e.g., with `./configure.sh --cryptominisat --auto-download`): CMS adheres to the default value of `CMAKE_INSTALL_LIBDIR` to work out where to install the library files (so `lib64` on openSUSE), which fails when cvc5 tries to find these in `lib`.

Without this change, the build fails as follows:

```
<snip>
src/CMakeFiles/cvc5.dir/theory/type_enumerator.cpp.o  -Wl,-rpath,::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::  deps/lib/libcadical.a  deps/lib/libcryptominisat5.a  ../deps/install/lib64/libglpk.a  deps/lib/libpicpolyxx.a  /usr/lib64/libgmp.so  deps/lib/libpicpoly.a  /usr/lib64/libgmp.so && :
/usr/lib64/gcc/x86_64-suse-linux/11/../../../../x86_64-suse-linux/bin/ld: cannot find deps/lib/libcryptominisat5.a: No such file or directory
collect2: error: ld returned 1 exit status
ninja: build stopped: subcommand failed.
```

and where:

```
avj@platypus ~/clones/cvc5/master/build$ find . -iname "libcryptominisat5.a"
./deps/src/CryptoMiniSat-EP-build/lib/libcryptominisat5.a
./deps/lib64/libcryptominisat5.a
```

(notice: `lib64` in the second path!)

This commit fixes this discrepancy to ensure that cvc5 checks for CMS on `CMAKE_INSTALL_LIBDIR` as well.

**Note**: `CMAKE_INSTALL_LIBDIR` comes from `GNUInstallDirs`, and this is `include`'d in cvc5's top-level `CMakeLists.txt`

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
3 years ago'ANTLR3_RUNTIME' should respect lib/lib64 (#6906)
Andrew V. Jones [Mon, 19 Jul 2021 06:55:35 +0000 (07:55 +0100)]
'ANTLR3_RUNTIME' should respect lib/lib64 (#6906)

On 64-bit openSUSE (and maybe other distributions), the default install directory for static libraries is `lib64` *not* `lib`. This has an impact on cvc5 when it is automatically building ANTLR3: ANTLR3 follows the system-wide default of `lib64`, which fails when cvc5 tries to find these in `lib`.

Without this change, the build fails as follows:

```
<snip>
src/parser/CMakeFiles/cvc5parser.dir/smt2/Smt2Parser.c.o  -Wl,-rpath,/home/avj/clones/cvc5/lib64_cms/build/src::::::::::::::::::::::::  src/libcvc5.so.1  deps/lib/libantlr3c.a && :
/usr/lib64/gcc/x86_64-suse-linux/11/../../../../x86_64-suse-linux/bin/ld: cannot find deps/lib/libantlr3c.a: No such file or directory
collect2: error: ld returned 1 exit status
ninja: build stopped: subcommand failed.
```

and where:

```
avj@platypus ~/clones/cvc5/lib64_cms/build$ find . -iname "libantlr3c.a"
./deps/src/ANTLR3-EP-runtime/.libs/libantlr3c.a
./deps/lib64/libantlr3c.a
```

(notice: `lib64` in the second path!)

This commit fixes this discrepancy to ensure that cvc5 checks for ANTLR3 on `CMAKE_INSTALL_LIBDIR`, which matches that `autotools` will use.

**Note**: `CMAKE_INSTALL_LIBDIR` comes from `GNUInstallDirs`, and this is `include`'d in cvc5's top-level `CMakeLists.txt`

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
3 years agoAdd n-ary term utilities (#6896)
Andrew Reynolds [Sun, 18 Jul 2021 19:29:13 +0000 (14:29 -0500)]
Add n-ary term utilities (#6896)

Initial work towards rewrite rule reconstruction

3 years agoDo not exhaustive instantiation when FMF is disabled (#6899)
Andrew Reynolds [Fri, 16 Jul 2021 17:04:39 +0000 (12:04 -0500)]
Do not exhaustive instantiation when FMF is disabled (#6899)

This makes FMF not handle quantified formulas when FMF options are disabled, apart from those marked internal.

This is required for combinations of sequences + quantified formulas.

3 years ago[Unit Tests] Avoid linking against external libs (#6898)
Andres Noetzli [Fri, 16 Jul 2021 16:28:30 +0000 (09:28 -0700)]
[Unit Tests] Avoid linking against external libs (#6898)

Fixes #6866. The `theory_airth_cad_white` unit test has been failing on
some platforms (e.g., macOS) due to statically linking libpoly in
libcvc5 and then separately linking it in the unit tests. This resulted
in issues with `static` variables. This commit fixes the issue by
avoiding linking libpoly in the unit tests and instead relying solely on
libcvc5.

Co-authored-by: Ouyancheng <1024842937@qq.com>
3 years ago[Unit Tests] Reenable `top_scope_context_obj` (#6892)
Andres Noetzli [Fri, 16 Jul 2021 03:11:24 +0000 (20:11 -0700)]
[Unit Tests] Reenable `top_scope_context_obj` (#6892)

Fixes #6047. The test was disabled because ASan found a use-after-free
due to an object allocated in the top scope being destroyed after the
scope (see #2607 for a detailed explanation). At first, the plan was to
add support for this use case. However, we have decided that we
currently don't need support for this feature and added a guard against
it (#6082). This commit reenables the test but changes it to destroy the
object allocated in the top level scope before the corresponding level
is popped. It additionally adds a test of the guard from #6082.

3 years agoFix context for proofs of instantiations (#6890)
Andrew Reynolds [Thu, 15 Jul 2021 18:45:12 +0000 (13:45 -0500)]
Fix context for proofs of instantiations (#6890)

Caught by a regression on proof-new, where an instantiation was the symmetric equality of an instantiation on a previous call to check-sat. Proofs of instantiation should be user-context dependent.

3 years agoDistinguish quantifiers preprocess as its own proof rule (#6897)
Andrew Reynolds [Thu, 15 Jul 2021 17:56:05 +0000 (12:56 -0500)]
Distinguish quantifiers preprocess as its own proof rule (#6897)

3 years agoConnect the equality solver to theory arith (#6894)
Andrew Reynolds [Thu, 15 Jul 2021 15:53:05 +0000 (10:53 -0500)]
Connect the equality solver to theory arith (#6894)

--arith-eq-solver is a new option to enable the equality solver in arithmetic, disabled by default.

This PR connects the equality solver to TheoryArith when this option is enabled.

This is in preparation for the central equality engine.

3 years agoArithmetic equality solver (#6876)
Andrew Reynolds [Thu, 15 Jul 2021 13:25:28 +0000 (08:25 -0500)]
Arithmetic equality solver (#6876)

This is work towards the central equality engine. This adds a module of arithmetic that uses the equality engine in the default way.

This class will be incorporated into theory_arith.cpp. It will be the replacement for CongruenceManager when we use the central equality engine architecture.

3 years agoMove master equality engine notification to own file (#6877)
Andrew Reynolds [Thu, 15 Jul 2021 05:20:11 +0000 (00:20 -0500)]
Move master equality engine notification to own file (#6877)

Preparation for central equality engine.

3 years agoAdd node converter utility (#6878)
Andrew Reynolds [Thu, 15 Jul 2021 04:25:36 +0000 (23:25 -0500)]
Add node converter utility (#6878)

Adds a utility for converting nodes. This is the first step towards the LFSC proof conversion.

3 years agobv: Disable bv-assert-input if proofs are enabled. (#6886)
Mathias Preiner [Thu, 15 Jul 2021 02:39:00 +0000 (19:39 -0700)]
bv: Disable bv-assert-input if proofs are enabled. (#6886)

3 years agobv: Rename BBSimple to NodeBitblaster. (#6891)
Mathias Preiner [Thu, 15 Jul 2021 02:19:12 +0000 (19:19 -0700)]
bv: Rename BBSimple to NodeBitblaster. (#6891)

3 years agobv: Rename lazy solver to layered solver. (#6889)
Mathias Preiner [Thu, 15 Jul 2021 01:54:33 +0000 (18:54 -0700)]
bv: Rename lazy solver to layered solver. (#6889)

3 years agobv: Rename simple solver to bitblast-internal. (#6888)
Mathias Preiner [Thu, 15 Jul 2021 01:27:33 +0000 (18:27 -0700)]
bv: Rename simple solver to bitblast-internal. (#6888)

3 years ago[proof] Fix open proof issues in SAT proof (#6887)
Haniel Barbosa [Wed, 14 Jul 2021 23:02:30 +0000 (20:02 -0300)]
[proof] Fix open proof issues in SAT proof (#6887)

Commit d1eee40cc (PR #6346), in a foolish attempt to prevent speculated issues, introduced an overwriting policy to addition of resolution chains during SAT solving at the SAT proof manager. First, this is nonsensical because the lazy proof chain is context-dependent and at the same level other ways of proving that clause are simply redundant and therefore should be ignored. Second, and catastrophically, this policy, for reasons beyond me, can lead to open SAT proofs when the same clause is rederived at the same level.

So this commit simply reverts the change and adds an optimization that when the clause would be rederived at the same level we do nothing and leave the method.

3 years agoAdd option that exercises the previously buggy behavior (#6884)
Haniel Barbosa [Wed, 14 Jul 2021 22:29:50 +0000 (19:29 -0300)]
Add option that exercises the previously buggy behavior (#6884)

3 years agoGeneralize congruence handling for HO in eq proofs (#6883)
Haniel Barbosa [Wed, 14 Jul 2021 21:35:21 +0000 (18:35 -0300)]
Generalize congruence handling for HO in eq proofs (#6883)

Previously we were not considering proofs for HO equalities (i.e., between operators) that were transitivity chains. This commit generalizes the elaboration procedure in eq_proof to do so.

3 years agoFix for context on input proof generator (#6873)
Andrew Reynolds [Wed, 14 Jul 2021 21:15:28 +0000 (16:15 -0500)]
Fix for context on input proof generator (#6873)

The preprocess proof generator uses a dummy CDProof to mark input assertions that do not need justification. This CDProof should be user-context dependent to avoid rare cases where an input assertion was the symmetric equality of another, it was previously context independent.

This also refactors the debugging traces in this class.

3 years agoMove synthesis verification check to own file (#6882)
Andrew Reynolds [Wed, 14 Jul 2021 20:42:40 +0000 (15:42 -0500)]
Move synthesis verification check to own file (#6882)

In preparation for more extensions to this aspect of the synthesis solver.

3 years agoRefactor setup of proof equality engine for central EE (#6831)
Andrew Reynolds [Wed, 14 Jul 2021 14:15:25 +0000 (09:15 -0500)]
Refactor setup of proof equality engine for central EE (#6831)

Users of an equality engine should each use the same proof equality engine that wraps it. This ensures that theory inference managers do so, by tracking the official proof equality engine for an equality engine in theory inference manager.

This is in preparation for (proper equality proofs for) central equality engine.

It also adds some debugging code that is highly useful for debugging issues related to when equalities are processed in theory inference manager.

3 years agoFix models for sequences of infinite element type (#6870)
Andrew Reynolds [Wed, 14 Jul 2021 13:43:25 +0000 (08:43 -0500)]
Fix models for sequences of infinite element type (#6870)

This fixes our model construction for sequences of infinite element type.

We were relying on getModelValue in our model construction which is incorrect since it assumes that the element type's theory can provide concrete values during model generation time. This makes the sequence model construction more robust by generalizing how model values are assigned: we use skeletons instead of concrete values when the element type is infinite.

This fixes some open model generation issues with Facebook benchmarks.

3 years agoClean up option usage in command executor (#6844)
Gereon Kremer [Wed, 14 Jul 2021 07:40:30 +0000 (09:40 +0200)]
Clean up option usage in command executor (#6844)

This PR makes the CommandExecutor class use the options object from its SmtEngine instead of the driver one. This makes sure that options that are set via (set-option ...) are in effect for the CommandExecutor. It still stores the driver options, though, as they are used for resets.
The PR also does some minor cleanups along the way (remove unused pOptions, make things const).
Fixes #2376.

3 years agoAdd missing space for check macro error messages. (#6875)
Mathias Preiner [Wed, 14 Jul 2021 06:57:13 +0000 (23:57 -0700)]
Add missing space for check macro error messages. (#6875)

3 years agobv: Add missing BV_EAGER_ATOM proof rule. (#6874)
Mathias Preiner [Wed, 14 Jul 2021 03:09:07 +0000 (20:09 -0700)]
bv: Add missing BV_EAGER_ATOM proof rule. (#6874)

Fixes an issue with --proof-eager-checking and --bitblast=eager.

3 years agobv: Simplify BV_BITBLAST_* proof rules. (#6871)
Mathias Preiner [Tue, 13 Jul 2021 19:02:37 +0000 (12:02 -0700)]
bv: Simplify BV_BITBLAST_* proof rules. (#6871)

Introduces BV_BITBLAST_STEP rule, which replaces BV_BITBLAST_X rules.

3 years ago[rewriter] Add rewrite to order IFF (equality for Booleans) (#6872)
Haniel Barbosa [Tue, 13 Jul 2021 18:38:23 +0000 (15:38 -0300)]
[rewriter] Add rewrite to order IFF (equality for Booleans) (#6872)

Not doing this rewrite for Booleans is probably an artifact of the old IFF kind being removed. This rewrite is important to simplify the generation of proofs for the SAT solver, as clarified in the new comment in the SAT proof manager.

3 years agobv: Do not rewrite below BV leafs in BBProof's TConvProofGenerator. (#6869)
Mathias Preiner [Tue, 13 Jul 2021 16:11:33 +0000 (09:11 -0700)]
bv: Do not rewrite below BV leafs in BBProof's TConvProofGenerator. (#6869)

Introduces a TermContext class that can be used to skip rewrites below theory leafs. Fixes issues related to bit-vector leafs begin incorrectly rewritten.

3 years agoAdd branch and bound lemma if linear arithmetic generates a non-integer assignment...
Andrew Reynolds [Tue, 13 Jul 2021 07:12:46 +0000 (02:12 -0500)]
Add branch and bound lemma if linear arithmetic generates a non-integer assignment (#6868)

This double checks that TheoryArithPrivate generates a model that does not assign real values to integer variables.

This is done outside of TheoryArithPrivate intentionally, so that it can be checked independently.

This code should very rarely be applied but would have caught the incorrect model which led to wrong results in the UFNIA division of smtcomp 2021.

3 years agobv: Expand bitblast proof steps in the proof post processor. (#6867)
Mathias Preiner [Tue, 13 Jul 2021 02:33:08 +0000 (19:33 -0700)]
bv: Expand bitblast proof steps in the proof post processor. (#6867)

This commit changes BV proof logging to record coarse-grained bit-blast steps during solving and expanding these steps on-demand in the proof post processor.

3 years agoAdd branch and bound (#6865)
Andrew Reynolds [Mon, 12 Jul 2021 20:59:25 +0000 (15:59 -0500)]
Add branch and bound (#6865)

This PR moves https://github.com/cvc5/cvc5/blob/master/src/theory/arith/theory_arith_private.cpp#L3451 to its own module.

The next PR will connect this module to theory_arith / theory_arith_private.

Towards ensuring type constraints are met for linear arithmetic models.

3 years agoFix for learned rewrite pass, add regression (#6850)
Andrew Reynolds [Mon, 12 Jul 2021 19:18:17 +0000 (14:18 -0500)]
Fix for learned rewrite pass, add regression (#6850)

Fixes #4791.

3 years agoFix ANTLR build on CMake <3.11 (#6864)
Andres Noetzli [Mon, 12 Jul 2021 19:05:14 +0000 (12:05 -0700)]
Fix ANTLR build on CMake <3.11 (#6864)

With CMake 3.11 and later, `<DOWNLOAD_DIR>` is substituted in
`ExternalProject_Add` but not in older versions [0]. To maintain
compatibility with older versions of CMake, this commit changes
`ExternalProject_Add` to use `<DOWNLOADED_FILE>` instead, which is both
nicer and substituted in older versions of CMake.

[0] https://cmake.org/cmake/help/latest/release/3.11.html#modules

3 years agoAdd arithmetic preprocess rewrite equality module (#6860)
Andrew Reynolds [Mon, 12 Jul 2021 18:55:13 +0000 (13:55 -0500)]
Add arithmetic preprocess rewrite equality module (#6860)

This is the first part of a refactoring which will ensure that the linear arithmetic solver does not violate integer type constraints in its model.

This PR moves the method https://github.com/ajreynol/CVC4/blob/master/src/theory/arith/theory_arith.cpp#L129 to its own module / file.

3 years agoAdd trace for combination splits (#6862)
Andrew Reynolds [Mon, 12 Jul 2021 18:15:48 +0000 (13:15 -0500)]
Add trace for combination splits (#6862)

Followup PRs will unify these with the lemmas / stats infrastructure in theory inference manager.

3 years agoUse default visibility for `cvc5::Exception` (#6856)
Andres Noetzli [Mon, 12 Jul 2021 17:31:58 +0000 (10:31 -0700)]
Use default visibility for `cvc5::Exception` (#6856)

Currently, `cvc5::Exception` does not have default visibility, which can
cause cvc5 to terminate when trying to catch it in `main.cpp`.
Presumably, this is because the necessary typeinfo is missing [0]. Due
to this issue, production builds for M1 on macOS crashed when parser
exceptions were thrown. The commit changes the visibility of the
exception.

[0] https://gcc.gnu.org/wiki/Visibility,
    "Problems with C++ exceptions (please read!)"

3 years agoImprovements to debug check model (#6861)
Andrew Reynolds [Mon, 12 Jul 2021 17:20:57 +0000 (12:20 -0500)]
Improvements to debug check model (#6861)

This makes it so that debug-check-models applies in production mode, not just in debug mode. It also verifies that type constraints are met.

3 years agotest also with default cores (#6858)
Haniel Barbosa [Fri, 9 Jul 2021 19:25:44 +0000 (16:25 -0300)]
test also with default cores (#6858)

Have unsat cores regression tested also with default mode.

3 years agoMake regression test `issue4971-0` more robust (#6857)
Andres Noetzli [Fri, 9 Jul 2021 19:15:51 +0000 (12:15 -0700)]
Make regression test `issue4971-0` more robust (#6857)

When compiling and running cvc5 on macOS with an M1 CPU, the regression
test regress0/cores/issue4971-0.smt2 returned unsat instead of the
expected unknown for the first (check-sat) command. This commit
makes the regression more robust by adding --cegqi-full and expecting
unsat.

3 years agoUse newer config.sub to fix build on Apple M1 (#6854)
Andres Noetzli [Fri, 9 Jul 2021 18:24:05 +0000 (11:24 -0700)]
Use newer config.sub to fix build on Apple M1 (#6854)

When building cvc5 on macOS for M1 natively, ANTLR's version of
`config.sub` does not recognize `aarch64-apple-darwin20.5.0`. This
commit fixes that issue by downloading the latest version of
`config.sub` (similar to what we are already doing for `config.guess`).
The commit also updates the URLs for `config.guess` and `config.sub` to
the URLs recommended in the files themselves. The commit also does some
minor cleanup/simplifications of the commands for building ANTLR.

3 years agoFix sets cardinality inference involving equivalent parents (#6855)
Andrew Reynolds [Fri, 9 Jul 2021 17:24:50 +0000 (12:24 -0500)]
Fix sets cardinality inference involving equivalent parents (#6855)

This fixes an unsoundness issue in the sets + cardinality solver.

One rule of this solver applies in sets when two parents of a child of a cardinality graph are equal, in which case we know that child or one of its siblings must be equal to the opposite parent. For example, this rule tells us that:

if T = (union T S), then (intersect T S) = S.

The explanation of this rule could consider the representative term of one the parents instead of the term itself say (union T S) is representative T, giving the unsound inference: if (union T S) = (union T S), then (intersect T S) = S. This ensures we use the original terms.

This PR also does some minor cleanup.

3 years agoImplement stop-only for new justification heuristic (#6847)
Andrew Reynolds [Fri, 9 Jul 2021 16:50:51 +0000 (11:50 -0500)]
Implement stop-only for new justification heuristic (#6847)

This also refactors decision engine so that we use inheritance instead of a dummy flag + members to determine which implementation to use.

3 years agoDisable ordering heuristic for justification by default (#6848)
Andrew Reynolds [Thu, 8 Jul 2021 21:16:25 +0000 (16:16 -0500)]
Disable ordering heuristic for justification by default (#6848)

3 years agoAdd script to build wheel for pycvc5 (#6839)
makaimann [Thu, 8 Jul 2021 16:24:54 +0000 (12:24 -0400)]
Add script to build wheel for pycvc5 (#6839)

This PR adds a script for building a wheel distribution for pycvc5. It automatically reads the top-level CMakeLists.txt to obtain the current version number, and then runs the standard setup from setuptools with an extension command class that configures and builds cvc5 with Python bindings. This wheel file is sufficient for uploading to Pypi. Although, note that we need to build for different operating systems and different Python versions because of the extension modules.

Note: another option is to use the scikit-build instead of doing the configuring and building manually. However, I ran into some issues when the setup.py file was not at the top-level. Because we prefer to have it hidden in a sub-folder, I took the manual route for now. In the future, we could consider changing this.

3 years ago[proof] [dot] Print let map (of terms in proof) as part of dot proof (#6853)
Haniel Barbosa [Thu, 8 Jul 2021 13:44:05 +0000 (10:44 -0300)]
[proof] [dot] Print let map (of terms in proof) as part of dot proof (#6853)

The let map is printed as JSON-like dictionary via a comment of the dot output.

3 years ago[unsat cores] Adding regressions from #4971 (#6852)
Haniel Barbosa [Wed, 7 Jul 2021 20:53:20 +0000 (17:53 -0300)]
[unsat cores] Adding regressions from #4971 (#6852)

Adds remaining regressions from issue #4791, which we can handle with the different new unsat-core modes. Note that issue4971-1.smt2 requires the sat-proof mode for unsat cores.

3 years agopow2: Update NEWS. (#6851)
Aina Niemetz [Wed, 7 Jul 2021 19:46:59 +0000 (12:46 -0700)]
pow2: Update NEWS. (#6851)

3 years agoRename operator pow2 to int.pow2. (#6849)
Aina Niemetz [Wed, 7 Jul 2021 18:36:15 +0000 (11:36 -0700)]
Rename operator pow2 to int.pow2. (#6849)

This name is the name of the symbol we parse. Internally, we still call
it POW2. This is a fix for the problem that `pow2` may clash (and
already does clash on SMT-LIB benchmarks) with user-defined symbols.

3 years agoFix regressions for competition build (#6846)
Andrew Reynolds [Wed, 7 Jul 2021 16:08:24 +0000 (11:08 -0500)]
Fix regressions for competition build (#6846)

Fixes one of the issues in the nightlies.

3 years agoStandard output for trigger selection (#6841)
Andrew Reynolds [Wed, 7 Jul 2021 15:44:01 +0000 (10:44 -0500)]
Standard output for trigger selection (#6841)

Fixes #6259.

3 years agoIntegrate Lazard into CAD module (#6812)
Gereon Kremer [Tue, 6 Jul 2021 23:01:13 +0000 (01:01 +0200)]
Integrate Lazard into CAD module (#6812)

This PR adds two new command line options that govern how the CAD module does projection and lifting, allowing to use the new Lazard evaluation. By default, we use McCallum with regular lifting which does not require CoCoA.
Additionally, this PR adds a bunch of unit tests for the CAD module.

3 years agoIntegrate learned rewrite preprocessing pass (#6840)
Andrew Reynolds [Tue, 6 Jul 2021 22:44:09 +0000 (17:44 -0500)]
Integrate learned rewrite preprocessing pass (#6840)

This adds the learned rewrite preprocessing pass, which rewrites the input formula based on (typically theory specific) reasoning about learned literals. The main motivation is for preprocessing ints division/modulus based on bounds.

3 years agoAdd implementation of learned rewrite pass (#6843)
Andrew Reynolds [Tue, 6 Jul 2021 20:00:38 +0000 (15:00 -0500)]
Add implementation of learned rewrite pass (#6843)