Aina Niemetz [Tue, 27 Apr 2021 03:33:03 +0000 (20:33 -0700)]
Bool: Move implementation of type rules to cpp. (#6420)
Gereon Kremer [Mon, 26 Apr 2021 20:48:40 +0000 (22:48 +0200)]
Generate docs conf.py by cmake (#6441)
This PR makes cmake generate the sphinx configuration file. This will simplify dynamically modifying this file in the future, for example to add custom paths within the build directory (for the python API).
Gereon Kremer [Mon, 26 Apr 2021 20:16:27 +0000 (22:16 +0200)]
Protect int stats methods (#6442)
This PR protects two methods of the IntStat class in case statistics are disabled.
Gereon Kremer [Mon, 26 Apr 2021 19:43:15 +0000 (21:43 +0200)]
First part of options refactoring (#6428)
This PR does a first round of refactoring and gets rid of a significant portion of generated code. In particular
- it removes options::optionName.wasSetByUser() (we still have Options::wasSetByUser())
- it removes options::optionName.set() (we still have Options::set())
- it removes options::optionName.getName() in favor of options::optionName.name
- it removes the specializations of Options::assign() and Options::assignBool() from the headers
- it eliminates runHandlerAndPredicates() and runBoolPredicates()
The removed methods are only used in few places with are changed to using Options::current().X() instead.
In the future, we also want to get rid of options::optionName() and use Options::operator[]() instead, and furthermore not use Options::current() but use the options from the Env object. This PR already adds Env::getOption() as a shorthand for Env::getOptions()[...] and uses it as a proof of concept within SmtEngine.
Andrew Reynolds [Mon, 26 Apr 2021 18:58:53 +0000 (13:58 -0500)]
Fix theoryOf for Boolean equalities (#6444)
Required for fixing a bug in CNF stream's ensureLiteral, which was crashing when combined with unsat-cores-mode=assumptions.
With this PR, we assign a formula like (= (= x y) (= z w)) to have theoryOf THEORY_BOOL. Previously, it mistaken was assigned THEORY_UF if e.g. x,y z, w were terms whose type was an uninterpreted sort.
We should retest unsat-cores-mode=assumptions after this PR is merged.
Diego Della Rocca de Camargos [Mon, 26 Apr 2021 17:36:55 +0000 (14:36 -0300)]
New design in DOT representation, nodes colored based on visions(basic and propositional) (#6423)
Conclusion and rule are placed on the same node (records nodes in the dot format).
Nodes are colored based on the view they will belong to.
Signed-off-by: Diego Della Rocca de Camargos diegodellarocc@gmail.com
Andrew Reynolds [Mon, 26 Apr 2021 15:13:50 +0000 (10:13 -0500)]
Ensure dependency is tracked for all substitutions (#6438)
This ensures that dependencies are tracked for all inferred substitutions, even if a trusted step is added.
This is required to ensure unsat cores are sound when we use e.g. non-clausal simplification + unsat cores.
Andrew Reynolds [Mon, 26 Apr 2021 14:57:36 +0000 (09:57 -0500)]
Enable print-inst-full by default (#6435)
This makes dump-instantiations print instantiations for all quantified formulas by default, regardless of whether they had an associated identifier.
Haniel Barbosa [Mon, 26 Apr 2021 14:46:56 +0000 (11:46 -0300)]
Fix assertions in SAT solver (#6443)
Due to our recent changes in the unsat core infrastructure we were doing a couple assertions wrong during conflict analysis. This commit fixes them.
Andrew Reynolds [Mon, 26 Apr 2021 07:34:14 +0000 (02:34 -0500)]
Do not process looping word equations over sequences (#6434)
Andrew Reynolds [Sun, 25 Apr 2021 20:05:15 +0000 (15:05 -0500)]
Use fast enumeration by default for Boolean predicate synthesis (#6440)
This updates the policy of when to apply smart enumeration: we do so if the grammar has ITE or admits Boolean connective terms. Previously, we applied smart enumeration for ITE and all Boolean grammars. However, this is misguided since e.g. partial evaluation unfolding has no opportunity to be effective if the enumerated terms are only Boolean literals.
This significantly improves run time on a challenge benchmark from @makaimann.
Andrew Reynolds [Sun, 25 Apr 2021 19:56:01 +0000 (14:56 -0500)]
More check models (#6439)
Andrew Reynolds [Sat, 24 Apr 2021 01:45:01 +0000 (20:45 -0500)]
Improve getValue for non-evaluated operators (#6436)
This makes it so that we attempt evaluation + rewriting on applications of operators that do not always evaluate, and return constants in case the evaluation was successful.
This fixes warnings for check-models on 43 of our regressions, and also uncovered one regression where our model was wrong but check-models silently succeeded. I've opened CVC4/cvc4-projects#276 for fixing the latter.
Mathias Preiner [Sat, 24 Apr 2021 00:57:35 +0000 (17:57 -0700)]
Add assumption-based unsat cores. (#6427)
This PR adds an assumption-based unsat cores option. If enabled it will
disable proof logging in the SAT solver and adds input assertions as
assumptions to the SAT solver. When an unsat core is requested we
extract the unsat core in terms of the unsat assumption in the SAT
solver. Assumption-based unsat cores use the proof infrastructure to map
the input assumptions back to the original assertions.
Gereon Kremer [Fri, 23 Apr 2021 21:50:02 +0000 (23:50 +0200)]
Add missing dependency for CaDiCaL (#6431)
This PR adds the dependency of the CaDiCaL cmake target on the external project CaDiCaL-EP if it is not found in the system.
Andrew Reynolds [Fri, 23 Apr 2021 20:44:39 +0000 (15:44 -0500)]
(proof-new) Proofs for sets purification lemmas (#6416)
This adds proofs for sets purification lemmas, which are of the form (= t (skolem t)) and (member t (skolem (singleton t))). Each can be trivially justified in the internal calculus by MACRO_SR_PRED_INTRO.
Andrew Reynolds [Fri, 23 Apr 2021 18:31:37 +0000 (13:31 -0500)]
Add new substitution apply methods fixpoint, sequential, simultaneous (#6429)
This adds various methods for applying substitution as an options to MACRO_SR_* rules. It extends the proof checker and the proof post processor to eliminate based on these types.
It updates the trust substitutions utility used by non-clausal simplification to use fixed-point semantics for substitution, which is highly important for efficiency.
As a result of this PR, we are orders of magnitude faster for checking proofs for problems where non-clausal substitution infers many substitutions. It also makes our regressions noticeably faster:
Gereon Kremer [Fri, 23 Apr 2021 13:46:52 +0000 (15:46 +0200)]
Make sure a ReferenceStat is set to values of the correct type (#6430)
This PR fixes a very subtle issue with setting the values a ReferenceStat refers to.
ReferenceStat::set() would take a variable by const& and then store the pointer to it. When giving it a different, but implicitly convertible, type, the pointer would assume the wrong type and consequently read incorrect values from it.
This PR makes set() a template function that explicitly checks that the given type is the correct one.
As we can only export int64_t to the API, this forces users of ReferenceStat to use int64_t stats.
Andrew Reynolds [Fri, 23 Apr 2021 02:18:13 +0000 (21:18 -0500)]
Enable strings exp by default for strings specific logics (#6424)
One of the main motivations for this PR is to simplify our process for doing SMT-LIB wide runs.
Aina Niemetz [Fri, 23 Apr 2021 01:19:05 +0000 (18:19 -0700)]
BV: Add proof logging for bit-blasting. (#6373)
Andrew Reynolds [Fri, 23 Apr 2021 00:06:10 +0000 (19:06 -0500)]
Move implementation of UF rewriter to cpp (#6393)
Andrew Reynolds [Thu, 22 Apr 2021 22:53:15 +0000 (17:53 -0500)]
Make trust substitution map generate proofs lazily (#6379)
This is work towards addressing a bottleneck when generating proofs for substitutions from non-clausal simplification.
This makes the proof generation in trust substitution map lazy.
Further work is required to allow an alternative fixpoint semantics for substitutions in the proof checker instead of the current sequential one.
Andrew Reynolds [Thu, 22 Apr 2021 22:36:02 +0000 (17:36 -0500)]
Minor improvements to substitutions (#6380)
In preparation for using this class as part of our proof checker.
This removes an option that was previously used as a hack to try to make check-models work for quantifiers. It also makes supplying a context optional.
Andrew Reynolds [Thu, 22 Apr 2021 21:03:08 +0000 (16:03 -0500)]
Minor changes to unsat core default setting (#6425)
Mathias Preiner [Thu, 22 Apr 2021 20:22:36 +0000 (13:22 -0700)]
cmake: Do not require --auto-download for already downloaded dependencies. (#6417)
This will look for already downloaded dependencies in the build
directory and therefore will not require --auto-download if the
dependencies were already downloaded in a previous build.
Gereon Kremer [Thu, 22 Apr 2021 19:55:41 +0000 (21:55 +0200)]
Update INSTALL.md (#6412)
This PR updates our build and installation instructions in INSTALL.md after we have changed how we handle dependencies.
Thanks @polgreen / #6391.
Gereon Kremer [Thu, 22 Apr 2021 19:38:57 +0000 (21:38 +0200)]
Add API documentation for statistics (#6364)
This PR adds documentation for api::Statistics and api::Stat, as well as further explanations in sphinx.
It also adds a custom css to our sphinx theme that slightly changes how inline code blocks look.
Gereon Kremer [Thu, 22 Apr 2021 19:27:54 +0000 (21:27 +0200)]
Remove unused stuff from options setup (#6422)
This PR removes some old stuff from our options setup that has not been used in a long time.
Most prominently, this includes the man pages that were still generated, and the alias and links options, which no longer worked anyway.
Andrew Reynolds [Thu, 22 Apr 2021 19:12:23 +0000 (14:12 -0500)]
Reorganizing use of skolem definition manager in prop engine (#6415)
Towards setting up the proper callbacks into the new justification heuristic.
Moves ownership of skolem definition manager from TheoryProxy to PropEngine.
Aina Niemetz [Thu, 22 Apr 2021 17:46:04 +0000 (10:46 -0700)]
api docs: Rename doxygen output directory. (#6426)
Aina Niemetz [Thu, 22 Apr 2021 17:20:36 +0000 (10:20 -0700)]
api docs: Remove file reintroduced in past merge. (#6426)
Andrew Reynolds [Thu, 22 Apr 2021 15:02:05 +0000 (10:02 -0500)]
Fix models for sygus-inference, bv2int, real2int (#6421)
In each case, previously we were generating a define-fun, what we needed was to do a model substitution.
This actually meant that check-models was giving false positives. The model was incorrect but check-models succeeded due to its use of expand definitions.
Haniel Barbosa [Thu, 22 Apr 2021 14:33:38 +0000 (11:33 -0300)]
Reconciling proofs and unsat cores (#6405)
This commit changes how defaults are set and how the SMT solver is initialized so that proofs can be used fully with (new) unsat cores. Three modes of unsat cores are established now:
the upcoming assumption-based cores, which are incompatible with producing proofs (but enable proofs for preprocessing)
cores based on the SAT proof, which are incompatible with producing proofs (but enable proofs for preprocessing and the SAT solver)
cores based on the full proof, which are unrestricted
All the modes activate proofs but lead to errors if the user requires proofs but is not in the full proofs mode for cores.
Andres Noetzli [Thu, 22 Apr 2021 03:25:57 +0000 (20:25 -0700)]
Allow in-place construction of `CDList` items (#6409)
This commit adds CDList::emplace_back(), which allows users to create
elements in CDList in-place (as opposed to copying the items using
CDList::push_back(). This allows CDList to be used with
std::unique_ptrs, which do not allow copying. Using
CDList::emplace_back() could also be more efficient in certain cases.
Andrew Reynolds [Thu, 22 Apr 2021 02:42:08 +0000 (21:42 -0500)]
Move expand definition from Theory to TheoryRewriter (#6408)
This is work towards eliminating global calls to getCurrentSmtEngine()->expandDefinition.
The next step will be to add Rewriter::expandDefinition.
Aina Niemetz [Wed, 21 Apr 2021 22:57:49 +0000 (15:57 -0700)]
Arithmetic: Move implementation of type rules to cpp. (#6419)
Aina Niemetz [Wed, 21 Apr 2021 22:48:38 +0000 (15:48 -0700)]
UF: Move implementation of type rules to cpp. (#6403)
Gereon Kremer [Wed, 21 Apr 2021 21:59:07 +0000 (23:59 +0200)]
Add explicit dependencies for base lib (#6410)
This PR adds missing cmake dependencies for the base library. This makes sure that Debug_tags.h and Trace_tags.h are already present when we start compiling.
Gereon Kremer [Wed, 21 Apr 2021 19:33:21 +0000 (21:33 +0200)]
Pass GMP to libpoly (#6411)
This PR makes sure that our build of libpoly works on systems without GMP: by passing the paths to GMP we use ourselves to libpoly, we make sure libpoly always has a suitable version of GMP.
Also, we make libpoly somewhat faster to build by disabling tests.
Aina Niemetz [Wed, 21 Apr 2021 18:54:32 +0000 (11:54 -0700)]
Datatypes: Move implementation of type rules to cpp. (#6418)
Mathias Preiner [Wed, 21 Apr 2021 17:21:34 +0000 (10:21 -0700)]
Goodbye CVC4, hello cvc5! (#6371)
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
Mathias Preiner [Wed, 21 Apr 2021 12:52:27 +0000 (05:52 -0700)]
cmake: Add optional module name argument for check_python_module helper. (#6406)
Addtionally adds checks for required documentation modules.
Aina Niemetz [Wed, 21 Apr 2021 12:27:16 +0000 (05:27 -0700)]
Sets: Move implementation of type rules to cpp. (#6401)
Aina Niemetz [Wed, 21 Apr 2021 03:15:43 +0000 (20:15 -0700)]
Arrays: Move implementation of type rules to cpp. (#6407)
Andrew Reynolds [Wed, 21 Apr 2021 03:02:31 +0000 (22:02 -0500)]
Add unit test for abduction (#6400)
Andrew Reynolds [Wed, 21 Apr 2021 02:34:35 +0000 (21:34 -0500)]
Add basic utilities for new implementation of justification heuristic (#6333)
This sets up the core utilities for the new implementation of justification heuristic
mudathirmahgoub [Wed, 21 Apr 2021 01:57:56 +0000 (20:57 -0500)]
Add getNumIndices to Op (#6386)
Add getNumIndices to Op
Andrew Reynolds [Tue, 20 Apr 2021 23:53:56 +0000 (18:53 -0500)]
Split FP expand definitions to own module (#6392)
This moves the code for expanding definitions in floating point to its own module, which lives in the rewriter.
This is work towards moving Theory::expandDefinitions to Rewriter::expandDefinitions.
The code was only moved, not modified in this PR.
Aina Niemetz [Tue, 20 Apr 2021 23:06:11 +0000 (16:06 -0700)]
BV: Move implementation of type rules from header to .cpp. (#6360)
Aina Niemetz [Tue, 20 Apr 2021 22:55:56 +0000 (15:55 -0700)]
Sep: Move implementation of type rules to cpp. (#6402)
Aina Niemetz [Tue, 20 Apr 2021 22:33:39 +0000 (15:33 -0700)]
Quantifiers: Move implementation of type rules to cpp. (#6404)
Gereon Kremer [Tue, 20 Apr 2021 22:10:17 +0000 (00:10 +0200)]
Add InferenceId as resources (#6339)
This PR extends the resource manager to consider theory::InferenceId a resource we can spend. This should give us a robust way to have the resource limiting cover a lot of theory reasoning. To make use of this, TheoryInferenceManager now spends these resources.
Also, it makes the ResourceManager properly use the options from the Env class.
Andrew Reynolds [Tue, 20 Apr 2021 21:40:12 +0000 (16:40 -0500)]
Add instantiation pool feature to the API (#6358)
This adds the command declare-pool to the public API. It also adds parsing support for this feature, lifts the internal kinds to public kinds, adds an example regression, and a unit test for the new declare-pool solver method.
Gereon Kremer [Tue, 20 Apr 2021 21:10:38 +0000 (23:10 +0200)]
Split C++ API docs from general docs (#6365)
Aina Niemetz [Tue, 20 Apr 2021 20:25:10 +0000 (13:25 -0700)]
Remove support for CVC3 language. (#6369)
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)