Age | Commit message (Collapse) | Author |
|
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
|
|
|
|
|
|
|
|
This PR adds optional rewriting to the SubstitutionMap class. Before, only the new TrustSubstitutionMap added optional rewriting, leading to unexpected inconsistencies between the two. In particular, cases exist where the substitution and the rewriting cancel each other (see #5943).
This PR moves the optional rewriting from TrustSubstitutionMap into SubstitutionMap. While the former enables it by default, it is disabled by default for the latter and thus does not change current behavior.
We now use this new option in an assertion in the non-clausal simplification.
Fixes #5943.
|
|
|
|
This class is an important utility in preprocessing, which we are adding proof support for. This simplifies the interface of this class with regards to unused interfaces for clarity.
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
|
|
Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally.
Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Some new functionality in substitutions.h/cpp
|
|
This reverts commit 9775bced75843c6f01e9524c2d0e7021535e3ec0.
|
|
for faster compilation
|
|
|
|
|
|
|
|
just the header comments at the top, though. Don't update to this rev if
you don't have time for a complete rebuild, and exclude this rev if you
want to see what's new across a range of commits.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
Also fix bug 421 relating to incrementality and models.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
To enable, use --check-models. Turning on the option can be done in debug or optimized builds, regardless of whether normal assertions are on or not. This is to allow us to check the generated models in long-running queries, and might be useful to end users as a double-check too.
By default, --check-models is quiet (no output unless it detects a problem). That allows regression runs to pass unless there are problems:
make regress CVC4_REGRESSION_ARGS=--check-models
To see it work, use -v in addition to --check-models.
There may still be bugs in the feature itself, but already I've found some apparent model-generation bugs (and discussed with Andy) from this feature, so it seems useful in its current state.
--check-models turns on what SMT-LIBv2 calls "interactive mode" (which keeps the list of user assertions around), and also implies --produce-models. This version does NOT require incremental-mode, which one design did (the one mentioned in yesterday's meeting).
Also:
* TheoryUF::collectModelInfo() now generates UninterpretedConstants (rather than non-constants)
* The UF rewriter now reduces (APPLY_UF (LAMBDA...) args...), and treats uninterpreted constants correctly (e.g. uc_U_1 != uc_U_2)
* The SubstitutionMap now supports substitutions of operators for paramaterized kinds (e.g., function symbols)
|
|
simplification for some benchmarks
|
|
non-SAT-solver) uses of std::cout to the Message stream, and all uses of std::cerr to the Warning stream.
|
|
|
|
|
|
|
|
the unconstrained examples in QF_AUFBV/brummayerbiere3 - should also help
generally on at least BV and maybe others.
Off by default for now - results are mixed and it's hard to evaluate with so
many existing assertion failures and segfaults - will re-evaluate once those
are fixed
|
|
support incrementality.
Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.
Expected performance change negligible; slightly better on memory:
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!
|
|
|
|
|
|
and model gen also.
I also expect this commit to fix bug #273.
No performance change is expected on regressions with this commit, see
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
|
|
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
|
|
infrastructure, and takes care not to affect CVC4's performance on LRA
benchmarks.
|
|
|