Gereon Kremer [Tue, 20 Apr 2021 19:37:18 +0000 (21:37 +0200)]
Basic setup for examples in documentation (#6383)
Aina Niemetz [Tue, 20 Apr 2021 18:58:46 +0000 (11:58 -0700)]
Add guards to disable clang-format around placeholders in templates. (#6375)
Andres Noetzli [Tue, 20 Apr 2021 18:46:14 +0000 (11:46 -0700)]
Fix `ANTLR3_COMMAND` for system ANTLR3 JAR (#6399)
ANTLR3_COMMAND was using a fixed path instead of relying on the
ANTLR3_JAR variable. If the ANTLR3 JAR was found on the system (for
example due to an existing deps folder at the root of the CVC4
folder), then the command would fail because the JAR was not at the
expected location. This commit changes the command to use the variable
and prints the location of the JAR file to make debugging easier.
Gereon Kremer [Tue, 20 Apr 2021 16:22:47 +0000 (18:22 +0200)]
Properly link Poly against GMP (#6398)
This PR fixes a linker issue with libpoly and static builds where Poly and GMP would be linked against in the wrong order.
yoni206 [Tue, 20 Apr 2021 14:33:10 +0000 (07:33 -0700)]
python API sorts: adding functions and tests (#6361)
This PR does the following:
1. removes old python sort API test
2. creates a new python sort API test, obtained by translating the (entire) cpp unit test https://github.com/CVC4/CVC4/blob/master/test/unit/api/sort_black.cpp
3. adds support for bags and datatype selectors/testers domain/codomain in the python API.
Andrew Reynolds [Mon, 19 Apr 2021 21:59:35 +0000 (16:59 -0500)]
Fully incorporate quantifiers macros into ppAssert / non-clausal simplification (#6394)
This PR removes the quantifiers macro preprocessing pass, which had several shortcomings, both in terms of performance and features.
This makes it so that quantifier macros are the (optional) implementation of TheoryQuantifiers::ppAssert.
In other words, quantifiers can now be put into "solved form", forall x. P(x) ---> P = lambda x. true.
This is part of an effort to improve proofs for preprocessing, as well as centralizing our reason about substitutions for the sake of efficiency.
Gereon Kremer [Mon, 19 Apr 2021 09:30:04 +0000 (11:30 +0200)]
Remove linking against gmp and cln in tests and parser (#6376)
Finally, we no longer need to link against GMP and CLN for the parser and the tests.
To actually achieve this, this PR also removes some dead code and unused includes from some parser files.
Gereon Kremer [Fri, 16 Apr 2021 15:12:03 +0000 (17:12 +0200)]
Fix dependencies for stats options (#6378)
A last-minute edit in a previous PR broke the handling of dependencies between the statistic options.
Andrew Reynolds [Fri, 16 Apr 2021 14:36:40 +0000 (09:36 -0500)]
Fix ONCE for post-rewrite (#6372)
Gereon Kremer [Fri, 16 Apr 2021 11:06:40 +0000 (13:06 +0200)]
Refactor cmake: auto-download and default-on dependencies (#6355)
This PR changes a few things in how dependencies are handled during configuration:
- --x-dir are removed for most dependencies, use the generic --dep-path instead
- the cmake ENABLE_AUTO_DOWNLOAD determines whether we attempt to download missing dependencies ourselves
- external projects check this option and send an error if it is OFF
- some optional dependencies are enabled by default (CaDiCaL, Poly, SymFPU)
This will essentially fail every call to ./configure.sh until the user specifies --auto-download.
Gereon Kremer [Fri, 16 Apr 2021 10:45:10 +0000 (12:45 +0200)]
Replace SExpr class by simpler conversion routines (#6363)
This PR finally removes the SExpr class. SMT-LIB compatible output is retained by using new on-the-fly conversion to s-expression strings. This finally allows us to remove includes to integer and rational from smt_engine.h.
In detail:
- a new set of toSExpr() methods is implemented that converts certain types to s-expression strings (without an intermediate class representing s-expressions)
- SmtEngine::getInfo() returns a string instead of SExpr and uses the new toSExpr methods
- SmtEngine::getStatistic() is removed
- SExpr class is removed
- d_commandVerbosity uses int instead of Integer
Mathias Preiner [Fri, 16 Apr 2021 06:55:25 +0000 (23:55 -0700)]
cmake: Build object libraries for base and context. (#6374)
cmake complains that the static base and context libraries are not
exported as install targets. Since we do not want to install these
libraries we'll build object libraries instead.
Aina Niemetz [Thu, 15 Apr 2021 21:57:53 +0000 (14:57 -0700)]
preprocessing context: Add wrapper for model substitutions. (#6370)
Previously, preprocessing passes added model substitutions without
expanding definitions for substitutions, which can be a problem.
This adds a wrapper function to take care of it properly.
Fixes #5473.
Mathias Preiner [Thu, 15 Apr 2021 21:45:54 +0000 (14:45 -0700)]
Build support library from base and context. (#6368)
This PR creates a support library from the utilities in base and context, which will be required in the parser as soon as we move the symbol table/manager to the parser.
Note: I decided to always build static libraries from base and context (and optionally enable -fPIC for shared builds) since I'm not sure if we want to have these libraries installed separately. Right now these are considered as cvc5 internal utilities that can be used in all cvc5 libraries, but not outside.
Gereon Kremer [Thu, 15 Apr 2021 21:05:44 +0000 (23:05 +0200)]
Avoid options listener for resource manager. (#6366)
This PR simplifies how the resource manager interacts with the options. Instead of using some notification mechanism, the resource manager simply retrieves the options via options::xyz(). This simplifies the options handler, the resource manager interface and the options.
When instructed to do so by the API, the SmtEngine now overwrites the respective option instead of calling out to the resource manager.
Aina Niemetz [Thu, 15 Apr 2021 20:04:55 +0000 (13:04 -0700)]
Rename occurrences of CVC4 to CVC5. (#6351)
This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.
Gereon Kremer [Thu, 15 Apr 2021 19:30:49 +0000 (21:30 +0200)]
Fix printing of stats when aborted. (#6362)
This PR improves/fixes printing of statistics when the solver has been aborted, i.e. when we use printSafe(), and a few other minor issues with the new statistics setup.
add toString() methods for TypeConstant, api::Kind to allow for automatic printing by print_safe<>()
improve kindToString() to avoid std::stringstream
fix newlines between statistics in printSafe()
make printing of histograms consistent
make --stats-all, --stats-expert and --stats-every-check automatically enable --stats (and vice versa)
Andrew Reynolds [Thu, 15 Apr 2021 19:08:00 +0000 (14:08 -0500)]
Reenable regression for minimizing instantiations (#6367)
Andrew Reynolds [Wed, 14 Apr 2021 22:10:09 +0000 (17:10 -0500)]
Fix type rule for relations join image (#6349)
The join image type rule restricted that an argument was a constant. This is a logic restriction that should not be a part of the type checker.
This is required for not throwing type checking exceptions during proof conversion to LFSC.
Gereon Kremer [Wed, 14 Apr 2021 21:52:06 +0000 (23:52 +0200)]
Improve documentation for FP rounding mode, add bibliography (#6343)
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Gereon Kremer [Wed, 14 Apr 2021 21:10:11 +0000 (23:10 +0200)]
Improve documentation of API kinds (#6341)
This PR improves the documentation of the api::Kind enum. Note that the docs for many of the enum values should still be improved. This PR merely makes sure that everything that is already there is actually output (/* vs /**) and properly rendered (missing spacing between lists, some formulas, etc).
Gereon Kremer [Wed, 14 Apr 2021 20:35:07 +0000 (22:35 +0200)]
Improve documentation for API exceptions (#6340)
Gereon Kremer [Wed, 14 Apr 2021 19:37:12 +0000 (21:37 +0200)]
Refactor / reimplement statistics (#6162)
This PR refactors how we collect statistics.
It splits the current statistic values into the values and a proxy object. The actual values now live inside the registry (making the ownership model way easier) while the proxy object are handed to whoever wants to collect a new statistic.
It also extends the C++ API to obtain and inspect the statistics.
To change the ownership, this PR needs to touch every single statistic in the whole codebase and change how it is registered.
Aina Niemetz [Wed, 14 Apr 2021 18:56:47 +0000 (11:56 -0700)]
Rename public and private headers in src/include. (#6352)
Haniel Barbosa [Wed, 14 Apr 2021 17:50:10 +0000 (14:50 -0300)]
[unsat-cores] Improving new unsat cores (#6356)
This commit adds a new option to produce unsat cores based on our proof infrastructure (whereas previously we could only do so if we were also checking unsat cores) and the corresponding changes to the default settings to account for it. Since now options::unsatCores() and options::produceProofs() are incompatible, several parts of the code where we tested if we were in "old unsat cores mode", by testing the former and the negation of the latter options, are updated accordingly.
This commit also changes how SMT engine sets things by disabling proofs in the theory engine if we are in unsat core mode.
Andrew Reynolds [Wed, 14 Apr 2021 16:49:50 +0000 (11:49 -0500)]
Add internal API methods for pool-based instantiation (#6350)
Andrew Reynolds [Wed, 14 Apr 2021 16:12:30 +0000 (11:12 -0500)]
Add interface for getting relevant assertions (#5131)
This adds an interface to TheoryEngine for getting the current set of relevant assertions if it is available.
An interface to this can further be added to the API in a future PR.
Abdalrhman Mohamed [Wed, 14 Apr 2021 14:36:58 +0000 (07:36 -0700)]
Merge equivalent sub-obligations instead of discarding them. (#6353)
This PR modifies the behavior of the reconstruction algorithm when the term to reconstruct contains two or more equivalent sub-terms, but one is easier to reconstruct than the others. Since we do not know which one is easier to reconstruct by matching, we match against all sub-terms. If a solution is found for one sub-term, we use it to solve the others.
Andrew Reynolds [Wed, 14 Apr 2021 13:58:33 +0000 (08:58 -0500)]
Warn about infeasible SyGuS conjectures (#6345)
Haniel Barbosa [Wed, 14 Apr 2021 13:31:35 +0000 (10:31 -0300)]
[proof-new] Fix explanation of literals in SAT proof manager (#6346)
Prevents exponential behavior in SAT proof generation by not reexplaining previously explained literals. Also fix a potential issue in not previously overwriting rederived resolution chains during solving.
Haniel Barbosa [Wed, 14 Apr 2021 12:54:03 +0000 (09:54 -0300)]
[proof-new] Miscellaneous improvements to dot printer (#6342)
Gereon Kremer [Wed, 14 Apr 2021 12:40:55 +0000 (14:40 +0200)]
Fix libpoly build and use new release (#6354)
This PR fixes the libpoly build: it naively removed the test/ folder from the source directory to save on cache size.
It also uses the recently published 0.1.9 release of libpoly.
Fixes #4706.
Andrew Reynolds [Tue, 13 Apr 2021 21:33:07 +0000 (16:33 -0500)]
Add pool instantiation strategy (#6308)
Adds an instantiation strategy based on user-provided pool annotations.
The next PR will connect this to quantifiers engine.
Andrew Reynolds [Tue, 13 Apr 2021 20:38:36 +0000 (15:38 -0500)]
Refactor quantifiers macros (#6348)
This does some refactoring of quantifiers macros preprocessing pass to use up-to-date utility methods, including lambdas, substitutions, methods for getting free variables.
This is work towards adding proofs for macros.
Mathias Preiner [Tue, 13 Apr 2021 20:00:29 +0000 (13:00 -0700)]
ci: Use CVC5_REGRESSION_ARGS. (#6347)
Andrew Reynolds [Tue, 13 Apr 2021 19:30:03 +0000 (14:30 -0500)]
Formalize more skolems (#6307)
This formalizes more skolems in preparation for moving Theory::expandDefinitions to Rewriter::expandDefinitions.
It also adds proof support for datatypes purification.
Aina Niemetz [Tue, 13 Apr 2021 17:19:12 +0000 (10:19 -0700)]
API docs: Add custom target to build for GH pages. (#6335)
Abdalrhman Mohamed [Tue, 13 Apr 2021 12:45:43 +0000 (05:45 -0700)]
Avoid using substitute's input cache after the method call. (#6328)
As it traverses a node, Node::substitute populates its input cache with TNodes that are not preserved by the SygusReconstruct module and maybe destroyed after the method call. This PR fixes a bug where those unsafe TNodes are referenced throughout the module by passing the method a temporary copy of the cache instead.
Abdalrhman Mohamed [Tue, 13 Apr 2021 01:51:24 +0000 (18:51 -0700)]
Fix sexpr bug with AST output language. (#6329)
When a command is invoked, its result/status may be printed depending on its current verbosity, which (for probably an outdated reason) is stored in SMTEngine. One of my previous PRs modified the SMTEngine to return the verbosity as an sexpr. The modification works correctly when the output language is SMT2, but it breaks down with the AST output language, which prints sexprs in a different way. This PR fixes this bug by making SMTEngine return options as strings instead of sexpr.
Aina Niemetz [Tue, 13 Apr 2021 01:33:55 +0000 (18:33 -0700)]
Bags: Move more implementation of type rule from header to .cpp. (#6336)
Aina Niemetz [Mon, 12 Apr 2021 23:09:43 +0000 (16:09 -0700)]
Strings: Move implementation of type rules from header to .cpp file. (#6334)
Andrew Reynolds [Mon, 12 Apr 2021 21:55:44 +0000 (16:55 -0500)]
Fix computation of whether a type is finite (#6312)
This PR generalizes TypeNode::isFinite / TypeNode::isInterpretedFinite with TypeNode::getCardinalityClass. It then uses this method to fix our computation of when a type should be treated as finite.
Fixes #4260, fixes #6100 (that benchmark now says unknown without an error).
Gereon Kremer [Mon, 12 Apr 2021 20:58:14 +0000 (22:58 +0200)]
Refactor resource manager (#6322)
This PR does another round of refactoring of the resource manager and related code.
- it moves the Resource enum out of the ResourceManager class
- it treats the resources in a generic way (storing the statistics in a vector) instead of the manual treatment we had before
- weights no longer live in the options, but in the ResourceManager and are changed accordingly in the ResourceManager constructor
- following the generic treatment of resources, it also removes all the resource-specific options --x-step in favor of a generic --rweight name=weight
- removed several unused methods from the ResourceManager
Note that we handle the Resource enum in a way that allows to easily use other enums as additional resources, for example InferenceId. The general idea is that we will at some point have sensible default weights (so that the cumulative resources somewhat simulate the solver runtime) and users (almost) never need to modify them.
Gereon Kremer [Mon, 12 Apr 2021 20:19:22 +0000 (22:19 +0200)]
Only require GMP 6.1 (#6332)
The recent refactoring of the dependencies raised the required GMP version to 6.2 for no particular reason. This PR reverts this change to only require GMP 6.1 again.
Aina Niemetz [Mon, 12 Apr 2021 19:31:43 +0000 (12:31 -0700)]
Refactor and update copyright headers. (#6316)
Andrew Reynolds [Mon, 12 Apr 2021 17:26:44 +0000 (12:26 -0500)]
Consolidate interface to prop engine (#6189)
This consolidates the interface for asserting input formulas to the PropEngine from SmtSolver.
As a consequence of this PR, this corrects one issue with the justification heuristic where skolem definitions were considered "assertions" by the justification heuristic (e.g. formulas that must be satisfied) instead of just being required for skolems in relevant literals. This was asymmetric from skolem definitions from lemmas, which were not being considered assertions. Now, skolem definitions are never assertions.
I tested this on QF_LIA SMT-LIB with decision=justification with 300 second timeout, essentially no difference in results (+6-5 all close to timeout). Also no difference on QF_S + QF_SLIA.
Andres Noetzli [Mon, 12 Apr 2021 17:15:16 +0000 (10:15 -0700)]
Fix GitHub Actions macOS build (#6331)
The build is currently failing because it tries to download an older
version of the ccache package. This commit makes sure that Homebrew is
up-to-date before trying to install packages.
Aina Niemetz [Sat, 10 Apr 2021 00:22:07 +0000 (17:22 -0700)]
Rename CVC4_ macros to CVC5_. (#6327)
Aina Niemetz [Fri, 9 Apr 2021 23:14:21 +0000 (16:14 -0700)]
Rename CVC4__ header guards to CVC5__. (#6326)
Aina Niemetz [Fri, 9 Apr 2021 22:28:18 +0000 (15:28 -0700)]
New C++ Api: Initial layout of Api documentation. (#6325)
Haniel Barbosa [Fri, 9 Apr 2021 20:30:44 +0000 (17:30 -0300)]
[proof-new] Optimizing sat proof (#6324)
For some benchmarks, checking MACRO_RESOLUTION can be up to 80% (!!!) of the running time. This commit introduces a new rule that does not perform checking. The old rule and checker are kept for ground truth. Some miscellaneous minor changes are also made in the PR.
Andrew Reynolds [Fri, 9 Apr 2021 19:21:11 +0000 (14:21 -0500)]
Add identifiers for extended function reductions (#6314)
This adds identifiers for extended function reductions, which are reasons for why an extended term no longer needs to be processed. The motivation is help understand check-model failures.
This PR adds identifiers to the ExtTheory utility. It also cleans up some unused parts of this utility. Some blocks of code changed indentation in this class.
Andrew Reynolds [Fri, 9 Apr 2021 19:11:31 +0000 (14:11 -0500)]
Add regressions for issue 6214 (#6305)
Adds 3 of the 6 benchmarks from issue 6214, the 1st and 5th benchmarks timeout.
Fixes #6214.
These benchmarks were fixed by
3c98bb2.
Andres Noetzli [Fri, 9 Apr 2021 18:01:23 +0000 (11:01 -0700)]
Learn equalities involving Boolean variables (#6323)
Previously, the circuit propagator was not learning literals of the form (= x t) where x is Boolean, since this term was not treated as a theory literal.
This commit changes that, which improves performance significantly, since it
allows the elimination of Boolean variables, which, in turn, can make the
justification heuristic much more effective.
Signed-off-by: Andres Noetzli noetzli@amazon.com
Andrew Reynolds [Fri, 9 Apr 2021 13:25:04 +0000 (08:25 -0500)]
Avoid spurious runs in run_regression.py (#6318)
The options --check-synth-sol and --check-abducts are independent from the rest of the solver. Hence, it is not necessary to run with/without them enabled in our regressions.
This saves roughly 30-40 seconds on regression regress0-2.
Andrew Reynolds [Fri, 9 Apr 2021 13:13:37 +0000 (08:13 -0500)]
Use expr miner timeout (#6321)
We currently were ignoring the option --sygus-expr-miner-timeout=N. This corrects the issue.
Gereon Kremer [Fri, 9 Apr 2021 12:41:14 +0000 (14:41 +0200)]
Add missing InferenceIds to toString (#6320)
This PR adds InferenceIds that were previously missing from the corresponding toString() method.
Andrew Reynolds [Thu, 8 Apr 2021 22:29:49 +0000 (17:29 -0500)]
Fix run_regression for cvc expected outputs (#6317)
Previously, we were not checking models / proofs / unsat cores for cvc inputs on CI.
Gereon Kremer [Thu, 8 Apr 2021 20:52:19 +0000 (22:52 +0200)]
Use newer version of update-pr-branch action. (#6315)
The CI action we use to update PRs that are ready to merge has been updated and now only considers the last review of every reviewer. It now allows to automatically update (and then merge) PRs where a reviewer first requested changes, and then accepted the PR. See adRise/update-pr-branch#11 for more details.
This PR bumps the version to the most recent one.
Andrew Reynolds [Thu, 8 Apr 2021 18:22:29 +0000 (13:22 -0500)]
Use exceptions when constructing malformed datatypes (#6303)
Fixes #5150.
Andrew Reynolds [Thu, 8 Apr 2021 14:15:31 +0000 (09:15 -0500)]
Add identifiers for sources of incompleteness (#6311)
This PR classifies all internal kinds of incompleteness as identifiers.
It makes it so TheoryEngine records an identifier when its incomplete flag is set.
The next step will be to possibly communicate this value to the user.
Andrew Reynolds [Thu, 8 Apr 2021 10:14:48 +0000 (05:14 -0500)]
Add benchmark for issue 5101 (#6301)
Fixes #5101.
Andrew Reynolds [Thu, 8 Apr 2021 10:05:43 +0000 (05:05 -0500)]
Add benchmark for issue 4400 (#6288)
Fixes #4400.
Andrew Reynolds [Thu, 8 Apr 2021 01:40:42 +0000 (20:40 -0500)]
Initial support for parametric datatypes in sygus (#6304)
Fixes #6298.
Enables parsing of par in the sygus parser, and adds support for default grammar construction.
Also fixes a bug related to single invocation for non-function types.
Aina Niemetz [Wed, 7 Apr 2021 23:12:23 +0000 (16:12 -0700)]
Remove old API header. (#6309)
Andrew Reynolds [Wed, 7 Apr 2021 22:23:40 +0000 (17:23 -0500)]
Add cardinality class definition (#6302)
This is work towards correcting our computation of whether a type is finite. Currently, arrays/functions with uninterpreted sorts as element/range types are always considered infinite. This is incorrect if finite model finding is enabled, since the interpretation of the uninterpreted sort can be one. This leads to errors during model building due to exhausted values (#4260, #6100).
This PR adds a new concept of a cardinality class, which is required for properly categorizing types with/without finite model finding.
A followup PR will replace TypeNode::isFinite with TypeNode::getCardinalityClass. Calls to TypeNode::isFinite will be replaced by calls to TheoryState::isTypeFinite, which will properly take cardinality classes into account.
Andrew Reynolds [Wed, 7 Apr 2021 22:13:14 +0000 (17:13 -0500)]
Add benchmark for 6270 (#6283)
Haniel Barbosa [Wed, 7 Apr 2021 21:17:33 +0000 (18:17 -0300)]
[proof-new] Fixing SMT post-processor's handling of assumptions (#6277)
Previously the SMT post-processor would update any assumption as long as it
had a proof for it. This can be a problem when one as assumption introduced in a
scope that should not be expanded. This commit fixes the issue by adding the
option of configuring a proof node updater to track scopes and the assumptions
they introduce, which can be used to determine the prood nodes which should be
updated. It also changes the SMT post-processor to only update assumptions that
have not been introduced in some scope.
This commit fixes an issue found by @Lachnitt during the integration of CVC4 and Isabelle.
Andrew Reynolds [Wed, 7 Apr 2021 21:03:27 +0000 (16:03 -0500)]
Add benchmark for issue 4420 (#6286)
Adds a benchmark that was previous sensitive to assertion order, fixes #4420.
Andrew Reynolds [Wed, 7 Apr 2021 20:45:39 +0000 (15:45 -0500)]
Set incomplete if not applying ho extensionality (#6281)
If the user manually disables ho-extensionality via expert option --no-uf-ho-ext, we should answer "unknown" instead of "sat" when applicable.
Fixes #4318.
Andrew Reynolds [Wed, 7 Apr 2021 20:28:47 +0000 (15:28 -0500)]
Fixes for abducts (#6279)
Fixes benchmarks 2 and 3 from #5848.
Aina Niemetz [Wed, 7 Apr 2021 20:18:53 +0000 (13:18 -0700)]
New C++ Api: Rename and move checks.h. (#6306)
Andrew Reynolds [Wed, 7 Apr 2021 19:45:45 +0000 (14:45 -0500)]
(proof-new) Proper implementation of proof node cloning (#6285)
Previously, we were traversing proof node as a tree, now we use a dag traversal.
This also makes sure that proofs work when we have a external proof conversion and we are in incremental mode. In such cases, the final proof must be cloned to ensure that we do not overwrite proof nodes, which may be reused across multiple check-sat.
Andrew Reynolds [Wed, 7 Apr 2021 19:30:58 +0000 (14:30 -0500)]
Add term pools utility (#6243)
This utility will be used to track pools for pool-based instantiation.
Aina Niemetz [Wed, 7 Apr 2021 19:15:31 +0000 (12:15 -0700)]
New C++ Api: Initial setup of Api documentation. (#6295)
This configures the initial setup for generating Api documentation with
Sphinx via Breathe and Doxygen. All fixes in the documentation of the
cvc5.h header are for the purpose of eliminating warnings. This PR does
not check for completeness of the documentation, and does not yet tweak
the documentation to be nice, beautiful and consistent, which is
postponed to future PRs.
Configure with `--docs`, and then make. This will generate a `docs`
directory in the build directory. The Sphinx documentation can be found
at `build/docs/sphinx/index.html`. Doxygen documentation is only
generated as xml under `build/docs/doxygen`.
This PR further proposes a new style for copyright headers. If this
style is approved, I will submit a PR to update the update_copyright.pl
script.
Andrew Reynolds [Wed, 7 Apr 2021 18:36:15 +0000 (13:36 -0500)]
Replace calls to NodeManager::mkSkolem with SkolemManager::mkDummySkolem (#6291)
This is in preparation for refactoring skolem creation throughout the code base to improve proofs and migrate Theory::expandDefinitions to Rewriter::expandDefinitions.
This PR also eliminates some unused code in TheoryArithPrivate.
Followup PRs will start formalizing/eliminating calls to mkDummySkolem.
Mathias Preiner [Wed, 7 Apr 2021 13:21:29 +0000 (06:21 -0700)]
cmake: Do not always regenerate cvc4kinds.{pxi,pxd}. (#6300)
Only regenerate files if dependencies changed. This avoids unnecessary
rebuilds of the Cython code.
Mathias Preiner [Tue, 6 Apr 2021 18:51:06 +0000 (11:51 -0700)]
cmake: Add helper to check if a given Python module is installed. (#6299)
Andrew Reynolds [Tue, 6 Apr 2021 17:06:46 +0000 (12:06 -0500)]
Add benchmark for issue 5942 (#6296)
Fixes #5942.
This benchmark was fixed by recent changes to ppRewrite.
Andres Noetzli [Tue, 6 Apr 2021 16:33:52 +0000 (09:33 -0700)]
Remove template argument from `NodeBuilder` (#6290)
Currently, NodeBuilder takes a single template argument: An integer
that determines the expected number of arguments. This argument is used
to determine the size of the d_inlineNvChildSpace array. This array is
used to construct nodes inline. The advantage of this is that we don't
have to allocate a NodeValue on the heap for the node under
construction until we are sure that the node is new. While templating
the array size may save some stack space (or avoid a heap allocation if
we statically know that we a fixed number of children and that number is
greater than 10), it complicates the code and leads to longer compile
times. Thus, this commit removes the template argument and moves some of
the NodeBuilder code to a source file for faster compilation.
CPU build time before change (debug build): 2429.68s
CPU build time after change (debug build): 2228.44s
Signed-off-by: Andres Noetzli noetzli@amazon.com
Andrew Reynolds [Tue, 6 Apr 2021 16:23:44 +0000 (11:23 -0500)]
Fix tptp parser for negative rational (#6297)
Andrew Reynolds [Tue, 6 Apr 2021 12:28:59 +0000 (07:28 -0500)]
Fix issue with lemma during equality engine iterator in sets (#6289)
Fixes #4370.
Mathias Preiner [Tue, 6 Apr 2021 03:58:13 +0000 (20:58 -0700)]
genkinds: Do not use relative paths to find src directory. (#6293)
Andrew Reynolds [Tue, 6 Apr 2021 03:37:46 +0000 (22:37 -0500)]
Remove stdPrintAscii option (#6280)
Fixes #4179.
Aina Niemetz [Tue, 6 Apr 2021 02:31:28 +0000 (19:31 -0700)]
New C++ Api: Rename and move headers. (#6292)
Mathias Preiner [Tue, 6 Apr 2021 01:04:11 +0000 (18:04 -0700)]
parsekinds: Remove DEFAULT_HEADER. (#6294)
DEFAULT_HEADER in src/api/parsekinds.py is essentially unused since both genkinds.py scripts pass the kinds header to the script. The current value of DEFAULT_HEADER does not work for the scripts since the working directory for genkinds.py is in src/api/{java,python}.
mudathirmahgoub [Mon, 5 Apr 2021 21:54:28 +0000 (16:54 -0500)]
Add documentation for theory_bags_type_rules.h (#6268)
Andrew Reynolds [Mon, 5 Apr 2021 20:52:20 +0000 (15:52 -0500)]
Fix spurious antecedant for symbolic regular expressions (#6284)
Fixes #6271.
This was triggered by recent fixes, this fixes solution soundness issues with symbolic regular expressions due to spuriously included antecedants, which made lemmas SAT-context dependent while being cached as user-context dependent.
Andrew Reynolds [Mon, 5 Apr 2021 20:25:37 +0000 (15:25 -0500)]
Add benchmark for issue 4412 (#6287)
Haniel Barbosa [Mon, 5 Apr 2021 18:47:40 +0000 (15:47 -0300)]
[proof-new] Registering proof checkers uniformly from the SMT solver (#6275)
Each theory has its own proof checker, responsible for checking the rules pertaining to that theory. The main proof checker uses these specialized checkers. Previously the main proof checker (of the proof node manager used across the SMT solver) was connected to these theory proof checkers during initialization of the theory. This commit adds an interface to the theories for retrieving its proof checker (analogous to how one retrieves the rewriter of a theory) which is used by a new method in the theory engine to register a theory proof checker to a given proof checker according to a theory id.
This is in preparation for the new unsat cores based on proofs.
Andrew Reynolds [Mon, 5 Apr 2021 17:17:39 +0000 (12:17 -0500)]
Enable UF when pre-skolem nested option is enabled (#6282)
Fixes #4328.
NicolaasWeideman [Mon, 5 Apr 2021 16:56:10 +0000 (09:56 -0700)]
python: Fix type casting in mkBitVector (#6261)
Fixes #6260.
Signed-off-by: Nicolaas <nweidema@usc.edu>
Andrew Reynolds [Mon, 5 Apr 2021 15:21:55 +0000 (10:21 -0500)]
Fix subtyping for sets care graph (#6278)
We were getting types for set singleton/membership in a way that was unsafe for subtyping, which was leading to incorrectly computing care graphs for sets of reals.
Fixes #5705.
Andrew Reynolds [Mon, 5 Apr 2021 14:34:18 +0000 (09:34 -0500)]
Add interface for skolem functions in SkolemManager (#6256)
This PR introduces the notion of a "skolem function" to SkolemManager, which is implemented as a simple cache of canonical skolem functions/variables.
This is a prerequisite for two things:
(1) Making progress on the LFSC proof conversion, which currently is cumbersome for skolems corresponding to regular expression unfolding.
(2) Cleaning up singletons. Having the ability make canonical skolem functions in skolem manager will enable Theory::expandDefinitions to move to TheoryRewriter::expandDefinitions. This will then enable removal of calls to SmtEngine::expandDefinitions.
This PR also makes arithmetic make use of this functionality already.
The next steps will be to clean up all raw uses of NodeManager::mkSkolem, especially for other theories that manually track allocated skolem functions.
yoni206 [Mon, 5 Apr 2021 13:30:19 +0000 (06:30 -0700)]
A proposal for python api unit tests (#6255)
This PR introduces two unit tests for the python api, translated directly from the unit tests for the cpp api.
The goal is to get feedback in order to reach some kind of a pattern/style for python API tests.
Also, i'd be happy to hear if there is any specific cpp api unit test I should translate for this initial attempt (e.g., a test that is more representative or might raise difficulties). For now i just picked the first two solver tests.
Yancheng Ou [Mon, 5 Apr 2021 13:21:40 +0000 (06:21 -0700)]
Optimizer for BitVectors (#6213)
Adds support for BitVector optimization, which is done via offline binary search. Units tests included.
Also mildly refactors the optimizer architecture.
Andrew Reynolds [Sat, 3 Apr 2021 18:21:55 +0000 (13:21 -0500)]
Disable substring component contains in strip endpoints (#6266)
Fixes the first benchmark from #6203.
Gereon Kremer [Fri, 2 Apr 2021 21:11:52 +0000 (23:11 +0200)]
Add cache for new dependencies folder. (#6265)
This PR adds caching of the new dependencies folder build/deps/ for the CI jobs and renames the old deps folder to "auxiliary told".
Note that we need to cache the entirety of build/deps/ (instead of just the install folder for the old one), otherwise cmake will try to rebuild them. Some of the external projects remove unnecessary files in their build to reduce their footprint in the cache.
Mathias Preiner [Fri, 2 Apr 2021 19:12:15 +0000 (12:12 -0700)]
cmake: Do not link against main object library. (#6269)
CMake 3.10.2 (default on Ubuntu 18.04) does not allow target_link_libraries on object libraries.
Gereon Kremer [Fri, 2 Apr 2021 18:29:27 +0000 (20:29 +0200)]
New statistics registry (#6210)
This PR adds the next part of the new statistics setup: the registry.
The new statistics registry owns the actual data and only issues proxy objects that can be used to modify the internally stored data.
Once we replace the old statistics setup, the files should be renamed from statistics_reg.* to statistics_registry.*.