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

No behavior changes in this PR, just code reorganization.

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

This also consolidates the option strictTriggers into userPatMode.

Fixes #6996.

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

3 years agoCosmetic improvements to theory datatypes (#7020)
Andrew Reynolds [Tue, 17 Aug 2021 05:44:20 +0000 (00:44 -0500)]
Cosmetic improvements to theory datatypes (#7020)

Mainly just indentation / formatting changes. In preparation for playing around with heuristics to datatypes theory motivated by Facebook benchmarks.

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

Work towards a new expression miner for caching satisfiability queries.

3 years agoInitial refactoring of set defaults (#7021)
Andrew Reynolds [Tue, 17 Aug 2021 01:57:40 +0000 (20:57 -0500)]
Initial refactoring of set defaults (#7021)

This commit starts to carve out better control flow structure in setDefaults.

It makes setDefaults contained in a class, and moves a few blocks of code to their own functions.

This class also makes options manager obsolete, it is deleted in this PR.

There should be no behavior change in this PR.

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

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

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

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

3 years agoMake Theory class use Env (#7011)
Gereon Kremer [Mon, 16 Aug 2021 14:20:22 +0000 (07:20 -0700)]
Make Theory class use Env (#7011)

This PR changes the Theory base class and the constructors of all theories to use the Env class to access contexts, logic information and the proof node manager.

3 years ago[Strings] Make fact detection more robust (#7007)
Andres Noetzli [Mon, 16 Aug 2021 13:58:43 +0000 (06:58 -0700)]
[Strings] Make fact detection more robust (#7007)

Currently, our check for whether an inference is a fact or a lemma
involves checking whether the kind of the conclusion is a conjunction or
a disjunction. However, this does not take into account inferences of
other kinds such as ites, which is a problem because they require a
decision from the SAT solver. This commit changes the condition to check
the theory of the conclusion. If the conclusion belongs to the theory of
strings, it considers it as a fact.

3 years agoAdd check for static libraries when compiling CryptoMiniSat #7010 (#7014)
Andrew V. Jones [Mon, 16 Aug 2021 05:31:23 +0000 (06:31 +0100)]
Add check for static libraries when compiling CryptoMiniSat #7010 (#7014)

This commit adds a check for CryptoMiniSat's static dependencies when configuring CryptoMiniSat. It changes a build-time failure into a configure-time failure.

`find_library` in CMake > 3.18 supports `REQUIRED`; as `cvc5` targets 3.10, I've implemented a check for what `find_library` returns.

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
3 years agoCorrect copyright print for GLPK (#7015)
Andrew V. Jones [Mon, 16 Aug 2021 03:24:25 +0000 (04:24 +0100)]
Correct copyright print for GLPK (#7015)

In `master`, starting `cvc5` interactively will give you:

```
  glpk-cut-log -  a modified version of GPLK, the GNU Linear Programming Kit
  See http://github.com/timothy-king/glpk-cut-log for copyrightinformation
```

Notice: there's a double-space after the dash following the library name, and there's no space between "copyrightinformation".

This commit corrects this print such that it gives:

```
  glpk-cut-log - a modified version of GPLK, the GNU Linear Programming Kit
  See http://github.com/timothy-king/glpk-cut-log for copyright information
```

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
3 years agoRefactor setDefaults to use an options object (#6994)
Gereon Kremer [Fri, 13 Aug 2021 00:12:19 +0000 (17:12 -0700)]
Refactor setDefaults to use an options object (#6994)

This commit refactors the `setDefaults` method to accept an `Options` object as argument instead of using the current (static) `Options` object.

3 years agoDisable external initialization of `thread_local` variables (#7004)
Andres Noetzli [Tue, 10 Aug 2021 20:04:21 +0000 (13:04 -0700)]
Disable external initialization of `thread_local` variables (#7004)

This commit adds `-fno-extern-tls-init` to the list of compiler flags to
tell the compiler that it can assume that there is no dynamic
initialization of thread-local variables in non-defining translation
units. This option should result in better performance and works around
crashing issues with our Windows build.

3 years agoSimplify generation of option module code. (#6995)
Gereon Kremer [Tue, 10 Aug 2021 00:09:24 +0000 (17:09 -0700)]
Simplify generation of option module code. (#6995)

This commit simplifies both the code that generates the option modules and the generated code itself. It removes placeholders in the templates that are no longer used, gets rid of the option holder types (and replaces them by simple inline functions) and does some clean up on the related code in the `mkoptions.py` script.

3 years agoCreate grouping of tests that exercise '--use-approx' (#6958)
Andrew V. Jones [Mon, 9 Aug 2021 18:01:37 +0000 (19:01 +0100)]
Create grouping of tests that exercise '--use-approx' (#6958)

Currently, it seems that `cvc5` has no tests that get anywhere near close to exercising the code in `approx_simplex`, which means that the GLPK integration is effectively untested in CI:

* https://cvc4.cs.stanford.edu/downloads/builds/coverage/cvc5-2021-08-02/index.src_theory_arith_approx_simplex.cpp.html

(which is at 2.8% at the time of writing!)

Indeed, if you run the whole of `ctest`, none of the code near GLPK is exercised; and, worse, there are *no* regression tests that use `--use-approx`!

This commit adds a selection of simple tests that have been derived (using `cvc5`'s existing regression suite and ddSMT) to reach code inside of `approx_simplex`; namely:

- `solveRelaxation`, and
- `solveMIP`

This is (hopefully) an initial start that will allow us to grow more regression tests exercising GLPK (e.g., following the same process of reduction, but using the SMTLIB benchmarks vs. only `cvc5`'s regression suite).

The folder structure has been named such that I can do `ctest -R "use_approx"` to run only the tests that (should) reach GLPK.

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
3 years agoSupport older CMake versions (#7003)
Andres Noetzli [Mon, 9 Aug 2021 15:13:39 +0000 (08:13 -0700)]
Support older CMake versions (#7003)

Fixes #7001. Commit c8bc488 introduced the use
of list(PREPEND ...) which was only introduced in version 3.15. We require
CMake 3.9 or later and this commit makes our build system compatible with older
CMake versions again. It also changes our CI to have two builds with Ubuntu
18.04 and two builds with Ubuntu 20.04 to better cover different versions of
build tools (including CMake 3.10).

3 years agoMerge options cmake into general cmake file (#6989)
Gereon Kremer [Fri, 6 Aug 2021 18:55:18 +0000 (11:55 -0700)]
Merge options cmake into general cmake file (#6989)

This PR removes options/CMakeLists.txt and merges its contents into src/CMakeLists.txt and does some generalization in the mkoptions.py script. This prepares the whole setup so that we can also generate options code in other directories than options/ easily in the future: parts of the options code will be moved to the main folder.

3 years agoClear options manager (#6991)
Gereon Kremer [Fri, 6 Aug 2021 01:18:49 +0000 (18:18 -0700)]
Clear options manager (#6991)

This PR moves the remaining responsibilities from the options manager into option predicates. They belong there anyway, given that this code shall be executed immediately when an option is set. This also allows to remove the infrastructure for an options listener.

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

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

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

Initial work towards rewrite rule reconstruction.

3 years ago[Unit Tests] Add missing include (#6990)
Andres Noetzli [Thu, 5 Aug 2021 20:13:56 +0000 (13:13 -0700)]
[Unit Tests] Add missing include (#6990)

For some configurations, the unit test `solver_black` was unable to find
the correct variant `std::find()`. This commit adds an explicit include
of `<algorithm>`, which declares the `std::find()` as required by the
unit test.

3 years agoFix policy for rewriting string equalities (#6916)
Andrew Reynolds [Thu, 5 Aug 2021 15:21:48 +0000 (10:21 -0500)]
Fix policy for rewriting string equalities (#6916)

This PR simplifies our rewriter for string equalities. We do not try to rewrite equalities to true/false by default.

This prevents cases where lemmas may contain vacuous premises that rewrite to false, hence making a lemma rewrite to true.

This PR reorganizes the interplay between the rewrite and the post-processing of rewrites via extended equality rewriting.

Fixes #6913. Also adds benchmarks from #6101 which appear related but were fixed in previous commits, thus fixes #6101 as well.

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

This PR removes calls to the Solver constructor with an Options object, and instead uses the setOption() method.

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

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

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

3 years agoFix policy for merging subproofs (#6981)
Andrew Reynolds [Wed, 4 Aug 2021 22:11:08 +0000 (17:11 -0500)]
Fix policy for merging subproofs (#6981)

This makes it so that we replace subproof A with subproof B if A and B prove the same thing, and B contains no assumptions. This is independent of the scope that A and B are in.

The previous policy replaced subproof A with subproof B if A and B prove the same thing and were in the same scope. This is not safe if A occurs in multiple scopes, where free assumptions can escape.

The new policy is more effective and safer than the previous one.

3 years ago[proof] [dot] Fix comments on dot printer (#6983)
Diego Della Rocca de Camargos [Wed, 4 Aug 2021 21:45:29 +0000 (18:45 -0300)]
[proof] [dot] Fix comments on dot printer (#6983)

This PR fixes the escaped characters in the dot printer. The output is now a valid DOT.

Signed-off-by: Diego Della Rocca de Camargos diegodellarocc@gmail.com
3 years agoAdd inference ids for remainder of sygus solver (#6977)
Andrew Reynolds [Wed, 4 Aug 2021 20:25:37 +0000 (15:25 -0500)]
Add inference ids for remainder of sygus solver (#6977)

Now, all inferences throughout cvc5 in our regression are properly marked with an InferenceId.

This PR includes minor simplifications to the interface for sygus modules. In particular it changes the behavior to send inferences via the inference manager instead of passing them around as a vector.

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

Addresses #6979.

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

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

3 years agoAdd optional debug information for dumping instantiations (#6950)
Andrew Reynolds [Wed, 4 Aug 2021 19:19:51 +0000 (14:19 -0500)]
Add optional debug information for dumping instantiations (#6950)

This complete the implementation of dump-instantiations-debug.

With this option, we can print the source of instantiations. For example:

$ cvc5 regress1/quantifiers/dump-inst-proof.smt2 --dump-instantiations-debug --produce-proofs
unsat
(instantiations (forall ((x Int)) (or (P x) (Q x)))
  (! ( 2 ) :source QUANTIFIERS_INST_E_MATCHING_SIMPLE ((not (= (P x) true))))
)
(instantiations (forall ((x Int)) (or (not (S x)) (not (Q x))))
  (! ( 2 ) :source QUANTIFIERS_INST_E_MATCHING_SIMPLE ((not (= (S x) false))))
)

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

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

Work towards making our policy for subproof merging safer.

3 years agoRefactor managed streams (#6934)
Gereon Kremer [Wed, 4 Aug 2021 18:35:41 +0000 (11:35 -0700)]
Refactor managed streams (#6934)

This PR introduces a new ManagedStream class that replaces the previous ManagedOstream. It allows to directly store the (wrapped) stream objects in the options. Handling the stream options is moved from the options manager to option predicates and the different options for input and output streams are combined into a single one.
Some associated utilities (open_ostream.h and update_ostream.h) are now obsolete and thus removed.

3 years agoAdd API function to get list of option names (#6971)
Gereon Kremer [Wed, 4 Aug 2021 18:17:42 +0000 (11:17 -0700)]
Add API function to get list of option names (#6971)

This PR adds a new API function api::Solver::getOptionNames() that exposes a list of all option names as strings. This PR will be followed by another that adds a method to further inspect a particular option by name, and thereby allows to inspect the solver options in a sensible way.

3 years agoReplace numeric predicates by explicit minimum and maximum (#6976)
Gereon Kremer [Wed, 4 Aug 2021 17:49:26 +0000 (10:49 -0700)]
Replace numeric predicates by explicit minimum and maximum (#6976)

This PR replaces some option predicates by explicit minimum and maximum values. This allows us to export information about an options domain/range in the future.

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

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

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

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

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

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

3 years agoRemove dependencies on smt engine in smt solver (#6965)
Andrew Reynolds [Wed, 4 Aug 2021 01:15:43 +0000 (20:15 -0500)]
Remove dependencies on smt engine in smt solver (#6965)

This is work towards eliminating circular dependencies on SmtEngine.

This simplifies several interfaces and makes it so that SmtSolver does not take a pointer to its parent SmtEngine.

It is also work towards eliminating the output manager, which is now subsumed by Env.

3 years agoUse int64_t, uint64_t or double for all numeric options. (#6970)
Gereon Kremer [Tue, 3 Aug 2021 21:44:35 +0000 (14:44 -0700)]
Use int64_t, uint64_t or double for all numeric options. (#6970)

This PR further simplifies the option setup by only using int64_t or uint64_t for integer options.

3 years agoRefactor shared solver to use theory builtin inference manager (#6960)
Andrew Reynolds [Tue, 3 Aug 2021 16:50:51 +0000 (11:50 -0500)]
Refactor shared solver to use theory builtin inference manager (#6960)

This ensures that e.g. COMBINATION_SPLIT shows up under theory::builtin::inferencesLemmas, and -t im. It also removes outdated interfaces from OutputChannel, and makes the feature TheoryEngine::ensureLemmaAtoms more modular, which was required for making these interfaces more consistent.

It also ensures that TheoryBuiltin has an inference manager, which will simplify special casing in #6956.

3 years agoRemove "inUnsatCore" flag throughout (#6964)
Andrew Reynolds [Tue, 3 Aug 2021 01:21:04 +0000 (20:21 -0500)]
Remove "inUnsatCore" flag throughout (#6964)

The internal solver no longer cares about what assertions are named / are in the unsat core.

This simplifies the code so that the (now unused) `inUnsatCore` flag is removed from all interfaces.

This eliminates another external use of `getSmtEngine`.

3 years agoProperly honor --stats-all and --stats-expert when printing statistics (#6967)
Gereon Kremer [Tue, 3 Aug 2021 00:05:54 +0000 (17:05 -0700)]
Properly honor --stats-all and --stats-expert when printing statistics (#6967)

This PR fixes an issue that was introduced with fda4613 where printing the statistics would only show non-defaulted and non-expert options.

3 years agoAdd 'REQUIRES: poly' to regression. (#6966)
Aina Niemetz [Mon, 2 Aug 2021 23:28:53 +0000 (16:28 -0700)]
Add 'REQUIRES: poly' to regression. (#6966)

This regression times out without libpoly.

3 years agobv: Enable equality engine for bitblast-internal. (#6961)
Mathias Preiner [Mon, 2 Aug 2021 21:33:34 +0000 (14:33 -0700)]
bv: Enable equality engine for bitblast-internal. (#6961)

3 years agoPerform statistics printing via the API (#6952)
Gereon Kremer [Sat, 31 Jul 2021 01:21:36 +0000 (18:21 -0700)]
Perform statistics printing via the API (#6952)

This PR changes how the command executor prints the statistics by moving stuff around a bit, eventually using only proper API methods of api::Solver. This PR also removes the smt_engine.h include from command_executor.cpp.

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.