Age | Commit message (Collapse) | Author |
|
|
|
Commit 54d24c786d6a843cc72dfb5e377603349ea5e420 was
changing CVC4 to handle certain non-fatal errors
(such as calling get-unsat-core without a proceding
unsat check-sat command) without terminating the
solver. In the case of get-unsat-cores, the changes
lead to the solver crashing because it was trying to
print an unsat core initialized with the default
constructor, so the member variable d_smt was NULL,
which lead to a dereference of a null pointer.
One of the issues of the way non-fatal errors were
handled was that the error reporting was done in the
invoke() method of the command instead of the
printResult() method, which lead to the error
described above and other issues such as a call to
get-value printing a value after reporting an error.
This commit aims to improve the design by adding a
RecoverableModalException for errors that the solver
can recover from and CommandRecoverableFailure to
communicate that a command failed in a way that does
not prohibit the solver from continuing to execute.
The exception RecoverableModalException is thrown by
the SMTEngine and the commands catch it and turn it
into a CommandRecoverableFailure. The commit changes
all error conditions from the commit above and adds a
regression test for them.
|
|
CVC4::Exception. (#1085)
|
|
Changes needed for the bit-blasting floating-point solver which are outside of it's area and / or applicable independently.
|
|
* Ensure that expand definitions is called on all non-variable expressions. In particular, it is necessary that the sets theory is notified when a set universe term occurs in the input to ensure options are set correctly. The commit moves this check from within check() to expandDefinitions(), and also adds the check for join image which relies on universe set. This fixes a bug reported by Arjun. Add and update regressions.
* Add comments concerning expandDefinitions
* Expand comment, move to .h
|
|
C++11 introduced the thread_local keyword, so we don't need to use
non-standard extensions or our custom pthread extension anymore.
The behavior was previously introduced as a workaround in commit
753a072c542c1c254d7c6adbf10e091ba585ede5. This commit
introduces the macro CVC4_THREAD_LOCAL that can be used to
declare variables as thread local. For Swig, this macro is defined to
be empty.
|
|
LFSC now lives outside of the CVC4 repository and is not part of the CVC4 distribution
anymore. As a consequence, we
+ Add --with-lfsc and --with-lfsc-directory as configure options.
In the case where CVC4 has not been built with integrated LFSC, all code that interacts with
LFSC is disabled.
+ Disable proof checking if CVC4_USE_LFSC is not defined.
Configuring the build with --check-proofs but without --with-lfsc results in an error.
+ Do not call LFSC's cleanup function (but we should in the future).
LFSC checker segfaults during cleanup on regression testcase regress0/bv/core/bitvec7.smt.
Disabled call to lfscc_cleanup until the problem in lfscc is fixed.
+ Disable building with LFSC for the distcheck travis build since it is not part of the distribution
anymore. Further, make distcheck with LFSC would require to call contrib/get-lfsc-checker
before calling make check on the temp build (the build of the unpacked distribution tar ball).
|
|
|
|
Additionally, this commit removes unnecessary includes, adds includes to
smt_engine.h in files that require it and removes s_smtEngine_current from
smt_engine_scope.h.
|
|
- Build fixes for Windows
- Make proof checking tempfile handling portable
- Test suite fixes for Windows
|
|
|
|
* Replacing __gnu_cxx::hash_map with std::unordered_map.
* Replacing __gnu_cxx::hash_set with std::unordered_set.
* Replacing __gnu_cxx::hash with std::hash.
* Adding missing includes.
|
|
Removing it as well.
|
|
Disable support for subrange and predicate subtypes (which were only partially supported previously).
|
|
for bug 831.
|
|
decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.
|
|
|
|
|
|
in regressions.
|
|
|
|
As reported in bug 769, the signal handlers currently use unsafe
functions such as dynamic memory allocations and fprintf. This commit
fixes the issue by introducing functions for printing statistics in
signal handlers (functions with the `safe` prefix). It also avoids
copying statistics, which further avoids dynamic memory allocation. The
safe printing of statistics has some limitations (it does not support
SExprStats or printing CVC4::Result), which should not matter much in
practice. Printing statistics in a non-signal handler is not affected by
these changes as that uses a separate code path (the functions without
the `safe` prefix).
Additional changes:
- Remove ListStat as it is not used anywhere
- Add unit test for safe printing statistics
|
|
on, add regression.
|
|
|
|
This is related to bug 508. The debug build was taking much longer than the
production build to compute the result. The issue was an assertion in a loop in
nonClausalSimplify(). By moving the assertion outside of the loop, the debug
build is now roughly an order of magnitude slower than the production build
(instead of two orders of magnitude), which seems to be roughly in line with
the difference for other benchmarks:
Debug version before change:
- Bug (minified version): 1065.6s
- regress3/friedman_n6_i4.smt: 6.9s
- regress2/uflia-error0.smt2: 6.3s
- regress2/fuzz_2.smt: 2.3s
Debug version after change:
- Bug (minified version): 131.4s
- regress3/friedman_n6_i4.smt: 6.7s
- regress2/uflia-error0.smt2: 6.2s
- regress2/fuzz_2.smt: 1.9s
Production version:
- Bug (minified version): 18.8s
- regress3/friedman_n6_i4.smt: 0.8s
- regress2/uflia-error0.smt2: 0.8s
- regress2/fuzz_2.smt: 0.2s
|
|
|
|
|
|
|
|
|
|
Remove decl. of getStatisticsRegistry(SmtEngine*)
|
|
commit for nlAlgMaster.
|
|
Commit f4ef7af0a2295691f281ee1604dfeb4082fe229c removed the definition
of getStatisticsRegistry(SmtEngine*) but not the declaration.
|
|
Addresses coverity issues:
1172167
1172174
1172176
1172183
1172185
1172186
1172188
1172189
1172191
1172192
1172193
1172194
1172197
1172197
1172198
1172434
1172437
1172438
1172443
1172445
1172446
1172447
1172448
1362695
1362700
1362717
1362736
1362768
1362786
1362811
1379599
1421404
1421405
1421406
1421407
1421408
1421409
1421410
1421411
1421412
1421413
|
|
|
|
Modify datatypes collect model info to include dt equivalence classes. Further work on sygus. Other minor fixes.
|
|
|
|
|
|
|
|
mkGroundTerm for parametric datatypes. Minor change to run_regression to allow regressions to override input language. Minor refactoring to Cvc.g.
|
|
Squashed commit of the following:
commit 5197a663eb262afbeb7740f53b5bd27479dccea0
Author: Clark Barrett <barrett@cs.stanford.edu>
Date: Mon Mar 6 00:16:16 2017 -0800
Remove IFF case
commit 2119b25a30ed42eca54f632e7232c9f76ae5755a
Author: guykatzz <katz911@gmail.com>
Date: Mon Feb 20 12:37:06 2017 -0800
proof support for bvcomp
commit d8c0c0d2c9c92ce06a5033ec0f3f85ea7bda1a22
Author: Clark Barrett <barrett@cs.stanford.edu>
Date: Fri Feb 17 21:09:04 2017 -0800
Added missing cases to operator<< for bv rewrite rules.
commit 0ed797c31d0e66cadc35b2397716c841d1aff270
Author: Clark Barrett <barrett@cs.stanford.edu>
Date: Fri Feb 17 11:43:51 2017 -0800
Added rewrite rules for new bitvector kinds.
commit 3b23dffb317de5559f8a95118fef633f711c114a
Author: Clark Barrett <barrett@cs.stanford.edu>
Date: Mon Feb 13 14:41:49 2017 -0800
First draft of bool-to-bv pass.
|
|
|
|
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
|
|
|
|
Previously, dependency tracing in `ite_removal.cpp` was only done with
the `unsatCores` option but `fewerPreprocessingHoles` requires
dependencies, too. This lead to errors during proof construction when
`fewerPreprocessingHoles` was active. This commit fixes the condition
and includes a test case that previously failed. Additionally, it fixes
a similar issue in the theory engine.
NOTE: this commit might not fix all instances of this problem.
`smt_engine.cpp` turns certain flags off with `unsatCores`.
Compatibility between those flags and `fewerPreprocessingHoles` needs to
be checked separately.
|
|
|
|
|
|
It was turned off for unsatCores, and fewerPreprocessingHoles using the same infrastructure.
|
|
rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions.
|
|
received.
|
|
|
|
|