| Age | Commit message (Collapse) | Author |
|---|
|
This updates all regressions that pass check-unsat-cores to enable check-unsat-cores. This includes any incremental benchmark, which was disabled in run_regression.py previously.
It adds --no-check-unsat-cores to a few corner benchmarks that were previously disabled based on --incremental.
It also reverts a change to when proofs are disabled: options like sygus-inference should not permit proofs (or unsat cores).
|
|
|
|
This PR does two things:
(1) It eliminates the ad-hoc implementation of printSynthSolutions and removes it from the API. Now, printing response to a check-synth command is done in a more standard way, using the API + symbol manager. This is analogous to recent refactoring to get-model.
(2) It updates cvc5's output in response to check-synth to be compliant with the upcoming sygus 2.1 standard. The standard has changed slightly: responses to check-synth are now closed in parentheses, mirroring the smt2 response to get-model.
It also removes the unused command GetSynthSolutionCommand.
|
|
This PR moves the option names out of the option struct (which will be removed) to free constexpr string constants.
|
|
This commit removes the remaining old proof code and the code to produce unsat cores based on it.
|
|
Previously, echo surpressed leading, trailing and escape quotes of the
string to print. However, the SMT-LIB standard states that the string is
to be printed as is, including those quote characters.
|
|
This PR adds more getter functions for api::Term to retrieve values from constant terms (and terms that the average API use might consider constant).
It also introduces std::wstring as regular representation for string constants instead of std::vector<uint32> for the SMT-LIB parser and the String class.
|
|
reflects that it is a macro, which we will eliminate
|
|
This commit changes the default unsat cores to those based on solving-under-assumptions in the SAT solver and the (new) preprocessing proofs.
The evaluation below on all the non-fp non-incremental SMT-LIB benchmarks, 120s timeout, shows the differences of the unsat cores based on the old proofs, the new ones based on SAT assumptions + preprocessing proofs, and the new ones based on SAT and preprocessing proofs. Note that the union of the last two is on par with the first.
```
status total solved sat unsat best timeout memout error uniq disagr time_cpu memory
benchmark config
AUFDTLIRA newUnsatCoresAssumps-safe/ ee 35 4 0 4 4 7 0 23 2 0 954.0 1267.5
newUnsatCoresProofs ok 35 31 0 31 25 4 0 0 0 0 894.1 1692.9
oldUnsatCores ok 35 32 0 32 30 3 0 0 1 0 799.2 1428.5
AUFLIA newUnsatCoresAssumps-safe/ ok 11 7 0 7 7 4 0 0 7 0 532.2 7604.4
newUnsatCoresProofs ok 11 4 0 4 1 6 0 0 0 0 829.0 12459.8
oldUnsatCores ok 11 4 0 4 3 6 0 0 0 0 818.2 7764.4
AUFLIRA newUnsatCoresAssumps-safe/ to 2 0 0 0 0 2 0 0 0 0 241.6 125.6
newUnsatCoresProofs ok 2 2 0 2 1 0 0 0 0 0 54.2 45.5
oldUnsatCores ok 2 2 0 2 2 0 0 0 0 0 49.4 79.7
AUFNIRA newUnsatCoresAssumps-safe/ ok 10 5 0 5 5 5 0 0 2 0 748.4 1630.0
newUnsatCoresProofs ok 10 4 0 4 0 6 0 0 0 0 850.7 2978.8
oldUnsatCores ok 10 8 0 8 5 2 0 0 1 0 502.7 2048.5
BV newUnsatCoresAssumps-safe/ ok 7 1 1 0 1 6 0 0 1 0 734.2 2065.0
newUnsatCoresProofs ok 7 6 3 3 4 1 0 0 0 0 246.7 1023.9
oldUnsatCores ok 7 6 3 3 3 1 0 0 0 0 248.6 992.0
LIA newUnsatCoresAssumps-safe/ to 1 0 0 0 0 1 0 0 0 0 120.9 47.7
newUnsatCoresProofs ok 1 1 0 1 1 0 0 0 0 0 0.3 6.5
oldUnsatCores ok 1 1 0 1 1 0 0 0 0 0 0.3 5.3
LRA newUnsatCoresAssumps-safe/ ok 5 3 0 3 3 2 0 0 3 0 450.7 260.4
newUnsatCoresProofs ok 5 2 0 2 0 3 0 0 0 0 537.8 424.5
oldUnsatCores ok 5 2 0 2 2 3 0 0 0 0 533.8 298.5
NIA newUnsatCoresAssumps-safe/ to 1 0 0 0 0 1 0 0 0 0 120.8 22.0
newUnsatCoresProofs ok 1 1 0 1 0 0 0 0 0 0 46.3 48.0
oldUnsatCores ok 1 1 0 1 1 0 0 0 0 0 43.3 40.3
QF_ABV newUnsatCoresAssumps-safe/ ok 105 70 59 11 70 35 0 0 63 0 8195.5 19363.3
newUnsatCoresProofs ok 105 34 24 10 17 71 0 0 5 0 11099.5 35756.7
oldUnsatCores ok 105 37 23 14 18 69 0 0 1 0 11198.0 26878.1
QF_ANIA newUnsatCoresAssumps-safe/ to 4 0 0 0 0 4 0 0 0 0 483.5 1631.8
newUnsatCoresProofs ok 4 4 3 1 2 0 0 0 0 0 175.1 1513.6
oldUnsatCores ok 4 4 3 1 3 0 0 0 0 0 173.8 1495.1
QF_AUFLIA newUnsatCoresAssumps-safe/ ok 35 6 1 5 6 29 0 0 3 0 3718.4 524.1
newUnsatCoresProofs ok 35 24 4 20 1 11 0 0 0 0 2357.2 36556.0
oldUnsatCores ok 35 32 5 27 29 3 0 0 5 0 1857.6 10067.7
QF_AUFNIA newUnsatCoresAssumps-safe/ ok 3 1 0 1 1 2 0 0 0 0 324.7 543.6
newUnsatCoresProofs ok 3 2 2 0 1 1 0 0 1 0 223.1 509.0
oldUnsatCores ok 3 2 1 1 1 1 0 0 0 0 268.5 484.3
QF_AX newUnsatCoresAssumps-safe/ ok 12 1 0 1 1 11 0 0 0 0 1379.2 391.3
newUnsatCoresProofs ok 12 10 0 10 0 2 0 0 0 0 528.7 7433.9
oldUnsatCores ok 12 12 0 12 11 0 0 0 1 0 343.0 2855.2
QF_BV newUnsatCoresAssumps-safe/ ok 96 56 30 26 49 39 2 0 35 0 9248.2 98058.7
newUnsatCoresProofs ok 96 37 26 11 23 52 7 0 7 0 9781.9 135924.7
oldUnsatCores ok 96 50 29 21 24 43 3 0 7 0 9155.6 107216.0
QF_IDL newUnsatCoresAssumps-safe/ ok 109 51 39 12 43 58 0 0 33 0 10427.2 50846.5
newUnsatCoresProofs ok 109 33 32 1 2 76 0 0 0 0 11692.8 108963.1
oldUnsatCores ok 109 75 55 20 64 34 0 0 26 0 10088.1 53105.6
QF_LIA newUnsatCoresAssumps-safe/ ok 306 155 111 44 138 151 0 0 119 0 25346.4 50556.0
newUnsatCoresProofs ok 306 117 95 22 49 189 0 0 0 0 27092.6 122894.9
oldUnsatCores ok 306 187 110 77 152 119 0 0 34 0 24521.0 61261.1
QF_LRA newUnsatCoresAssumps-safe/ ok 72 39 20 19 38 33 0 0 31 0 7475.3 16892.2
newUnsatCoresProofs ok 72 31 16 15 2 41 0 0 0 0 7569.3 35658.7
oldUnsatCores ok 72 41 18 23 32 31 0 0 2 0 7243.2 20593.9
QF_NIA newUnsatCoresAssumps-safe/ ok 4389 2009 1862 147 2002 903 0 0 1931 0 163975.7 280779.3
newUnsatCoresProofs ok 4389 2326 2156 170 752 792 0 0 37 0 151051.9 387779.8
oldUnsatCores ok 4389 2394 2199 195 2174 730 0 0 81 0 146419.3 259669.8
QF_NRA newUnsatCoresAssumps-safe/ ok 135 65 57 8 57 70 0 0 45 0 10195.7 24701.4
newUnsatCoresProofs ok 135 71 49 22 35 64 0 0 5 0 10825.3 32982.8
oldUnsatCores ok 135 75 54 21 51 61 0 0 9 0 10865.3 27260.9
QF_RDL newUnsatCoresAssumps-safe/ ok 7 5 1 4 5 2 0 0 1 0 564.7 958.4
newUnsatCoresProofs ok 7 1 1 0 0 6 0 0 0 0 842.0 11029.6
oldUnsatCores ok 7 6 1 5 2 1 0 0 1 0 665.8 1982.6
QF_S newUnsatCoresAssumps-safe/ ok 5 1 1 0 0 4 0 0 0 0 603.3 191.4
newUnsatCoresProofs ok 5 5 5 0 2 0 0 0 0 0 161.9 285.8
oldUnsatCores ok 5 4 4 0 3 1 0 0 0 0 225.9 219.3
QF_SLIA newUnsatCoresAssumps-safe/ ok 258 74 67 7 70 184 0 0 64 0 27245.9 20290.4
newUnsatCoresProofs ok 258 179 163 16 47 79 0 0 6 0 18996.0 33722.6
oldUnsatCores ok 258 184 162 22 149 74 0 0 9 0 18395.8 23004.3
QF_UF newUnsatCoresAssumps-safe/ ok 29 25 0 25 6 4 0 0 2 0 2362.4 7504.3
newUnsatCoresProofs ok 29 0 0 0 0 28 1 0 0 0 3508.0 124190.7
oldUnsatCores ok 29 27 0 27 23 2 0 0 4 0 1866.3 13635.1
QF_UFBV newUnsatCoresAssumps-safe/ ok 2 2 0 2 1 0 0 0 1 0 189.5 1599.3
newUnsatCoresProofs to 2 0 0 0 0 2 0 0 0 0 241.8 1818.8
oldUnsatCores ok 2 1 0 1 1 1 0 0 0 0 193.7 1500.9
QF_UFIDL newUnsatCoresAssumps-safe/ ok 9 9 0 9 7 0 0 0 4 0 697.0 1133.0
newUnsatCoresProofs to 9 0 0 0 0 9 0 0 0 0 1088.0 14652.6
oldUnsatCores ok 9 5 0 5 2 4 0 0 0 0 848.5 2079.6
QF_UFLIA newUnsatCoresAssumps-safe/ ok 1 1 0 1 0 0 0 0 0 0 117.1 76.4
newUnsatCoresProofs to 1 0 0 0 0 1 0 0 0 0 120.9 208.5
oldUnsatCores ok 1 1 0 1 1 0 0 0 0 0 110.6 127.7
QF_UFLRA newUnsatCoresAssumps-safe/ ok 7 4 1 3 0 0 3 0 0 0 266.6 55098.3
newUnsatCoresProofs mo 7 0 0 0 0 0 7 0 0 0 261.7 56000.0
oldUnsatCores ok 7 7 4 3 7 0 0 0 3 0 408.4 20933.4
QF_UFNIA newUnsatCoresAssumps-safe/ ok 48 21 19 2 21 4 0 0 20 0 592.3 880.6
newUnsatCoresProofs ok 48 27 22 5 18 4 0 0 1 0 641.4 1548.8
oldUnsatCores ok 48 26 21 5 26 7 0 0 1 0 887.5 1044.6
QF_UFNRA newUnsatCoresAssumps-safe/ ok 1 1 1 0 1 0 0 0 1 0 108.3 17.9
newUnsatCoresProofs to 1 0 0 0 0 1 0 0 0 0 120.8 19.0
oldUnsatCores to 1 0 0 0 0 1 0 0 0 0 120.8 14.7
UF newUnsatCoresAssumps-safe/ ok 21 5 0 5 5 16 0 0 5 0 2123.8 3168.7
newUnsatCoresProofs ok 21 13 0 13 6 8 0 0 0 0 1496.3 6617.8
oldUnsatCores ok 21 16 0 16 11 5 0 0 3 0 1443.3 3919.2
UFDT newUnsatCoresAssumps-safe/ ok 35 6 0 6 6 29 0 0 5 0 3777.0 4485.5
newUnsatCoresProofs ok 35 28 0 28 15 7 0 0 0 0 1416.9 4293.6
oldUnsatCores ok 35 30 0 30 26 5 0 0 1 0 1406.9 3188.5
UFDTLIA newUnsatCoresAssumps-safe/ to 4 0 0 0 0 4 0 0 0 0 483.5 1640.5
newUnsatCoresProofs ok 4 4 0 4 1 0 0 0 0 0 139.3 942.3
oldUnsatCores ok 4 4 0 4 3 0 0 0 0 0 156.4 851.8
UFDTLIRA newUnsatCoresAssumps-safe/ ok 1 1 0 1 1 0 0 0 1 0 0.0 3.1
newUnsatCoresProofs ok 1 0 0 0 0 0 0 0 0 0 0.0 3.2
oldUnsatCores ok 1 0 0 0 0 0 0 0 0 0 0.0 2.7
UFDTNIRA newUnsatCoresAssumps-safe/ ok 10 3 0 3 3 6 0 0 3 0 754.8 1386.9
newUnsatCoresProofs ok 10 7 0 7 5 3 0 0 0 0 377.0 848.8
oldUnsatCores ok 10 7 0 7 7 3 0 0 0 0 376.5 563.4
UFLIA newUnsatCoresAssumps-safe/ ok 24 8 0 8 8 16 0 0 8 0 2231.6 3179.2
newUnsatCoresProofs ok 24 14 0 14 3 10 0 0 1 0 1915.5 5131.1
oldUnsatCores ok 24 15 0 15 14 9 0 0 2 0 1857.5 3479.7
UFNIA newUnsatCoresAssumps-safe/ ok 354 183 28 155 116 133 0 0 113 0 25941.4 839089.7
newUnsatCoresProofs ok 354 107 17 90 28 107 92 0 2 0 23496.9 1020258.1
oldUnsatCores ok 354 237 19 218 233 72 0 0 66 0 19906.9 914273.0
```
|
|
This PR adds support for handling --bitblast=eager in the new bitblast solver.
|
|
This PR improves the integration of the CAD solver with the nl-ext solver in a simple way: we simply use a few of the simple linearization lemmas in combination with CAD by default, significantly improving the performance on QF_NRA.
|
|
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
|
|
This removes the expandOnly flag from expandDefinitions.
The use of expandOnly = true is equivalent to applying top-level substitutions only, which should be done explicitly via Env::getTopLevelSubstitutions. It updates the trust substitutions utility to distinguish apply vs applyTrusted for convenience for this purpose.
This also breaks several dependencies in e.g. expand definitions module.
|
|
add 3 helper functions
judge whether a node is optimizable
make strong improvement expression according to optimization objective
make weak improvement expression according to optimization objective
optChecker is now created by optimizationSolver instead of the minimize/maximize functions
Slightly refactors function signatures so that they are accepting OptimizationObjective instead of accepting target, type in separate parameters.
|
|
This is work towards eliminating singletons.
Also, TheoryModel should use the same substitution map as the preprocessor. This is work towards unifying these things, which will be done in a future PR.
|
|
for multiple objectives (#6459)
This PR is one part of multiple.
Preliminary support means currently only supports single objective.
It supports queue-ing up objectives and it always optimizes the first.
Multiple-obj optimization algorithm will be up next.
* Refactor optimization result and objective classes
* Add preliminary support for multiple objectives
* The unit tests are now comparing node values instead of node addresses
|
|
This eliminates explicit tracking of defined functions, and instead makes define-fun add to preprocessing substitutions.
In other words, the effect of:
(define-fun f X t)
is to add f -> (lambda X t) to the set of substitutions known by the preprocessor. This is essentially the same as when
(= f (lambda X t)) was an equality solved by non-clausal simplification
The motivation for this change is both uniformity and for performance, as fewer traversals of the input formula.
In this PR:
define-fun are now conceptually higher-order equalities provided to smt::Assertions. These assertions are always added as substitutions instead of being pushed to AssertionPipeline.
Top-level substitutions are moved from PreprocessingContext to Env, since they must be accessed by Assertions. Proofs for this class are enabled dynamically during SmtEngine::finishInit.
The expandDefinitions preprocessing step is replaced by apply-substs. The process assertions module no longer needs access to expand definitions.
The proof manager does not require a special case of using the define-function maps.
Define-function maps are eliminated from SmtEngine.
Further work will reorganize the relationship between the expand definitions module and the rewriter, after which global calls to SmtEngine::expandDefinitions can be cleaned up. There is also further work necessary to better integrate theory expand definitions and top-level substitutions, which will be done on a followup PR.
|
|
This PR fixes an issue with one of our nightlies.
|
|
This PR refactors how the resource manager options are used. It moves options relevant for the resource manager into its own file (making the number of smt options a bit smaller) and uses the Options object directly instead of using the old static accessors.
|
|
This PR removes two headers for exceptions from options.h, and instead pushes the includes to a couple of source files.
|
|
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.
|
|
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.
|
|
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:
|
|
One of the main motivations for this PR is to simplify our process for doing SMT-LIB wide runs.
|
|
|
|
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.
|
|
This is work towards eliminating global calls to getCurrentSmtEngine()->expandDefinition.
The next step will be to add Rewriter::expandDefinition.
|
|
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
|
|
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.
|
|
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.
|
|
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.
|
|
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
|
|
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.
|
|
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.
|
|
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.
|
|
|
|
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.
|
|
|
|
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.
|
|
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.
|
|
|
|
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.
|
|
|
|
|
|
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.
|
|
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.
|
|
Fixes benchmarks 2 and 3 from #5848.
|
|
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.
|
|
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.
|
|
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
|
