summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Collapse)Author
2017-09-24CID 1362907: Initializing d_smtEngine to nullptr. (#1134)Tim King
2017-09-19Fix issue #1074, improve non-fatal error handling (#1075)Andres Noetzli
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.
2017-09-14Simplifying the throw specifier of SmtEngine::checkSat and related calls to ↵Tim King
CVC4::Exception. (#1085)
2017-09-13Floating point symfpu support (#1093)Martin
Changes needed for the bit-blasting floating-point solver which are outside of it's area and / or applicable independently.
2017-09-10Ensure that expand definitions is called on all non-variable expressi… (#1070)Andrew Reynolds
* 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
2017-08-30Use thread_local instead of compiler extensions (#210)Andres Noetzli
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.
2017-08-25Move LFSC checker out of the CVC repository. (#222)Aina Niemetz
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).
2017-08-23Fix typosAndres Noetzli
2017-08-14Move function defns from smt_engine_scope.h to cpp (#216)Andres Noetzli
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.
2017-08-14Build and test suite fixes for Windows (#186)Mark Laws
- Build fixes for Windows - Make proof checking tempfile handling portable - Test suite fixes for Windows
2017-08-07Make quantifier elimination more robust to preprocessing.ajreynol
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
* 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.
2017-07-19Removing the unused CDAttribute. This makes CDHashMap::obliterate unused. ↵Tim King
Removing it as well.
2017-07-12Make type rules more strict for operators whose type rules involve subtypes. ↵ajreynol
Disable support for subrange and predicate subtypes (which were only partially supported previously).
2017-07-10Do not exit when value/model/unsat-core/proof is requested at wrong time, ↵ajreynol
for bug 831.
2017-07-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ↵ajreynol
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.
2017-07-07Update copyright headers.Mathias Preiner
2017-05-31Fix model construction for BV with cbqi. Minor change to defaults.ajreynol
2017-05-31Minor change to defaults, update smt comp script, minor changes to options ↵ajreynol
in regressions.
2017-05-15Fix bug 806. Minor fixes to remove term formula pass.ajreynol
2017-05-12Make signal handlers saferAndres Notzli
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
2017-05-05Do not eliminate extended arithmetic symbols when finite model finding is ↵ajreynol
on, add regression.
2017-05-04fixing bug 790: track dependencies when the unsatCores() option is onguykatzz
2017-04-21Move assertion out of loop for better performanceAndres Noetzli
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
2017-04-20Minor fixes.ajreynol
2017-04-14Fix for fmf-fun when the option is set by user command.ajreynol
2017-04-12Add nullary operator metakind.ajreynol
2017-04-07Change option names for nl.ajreynol
2017-04-03Merge pull request #141 from 4tXJ7f/remove_defClark Barrett
Remove decl. of getStatisticsRegistry(SmtEngine*)
2017-04-02Adding a model based axiom instantiation scheme for multiplication. Merge ↵Tim King
commit for nlAlgMaster.
2017-03-31Remove decl. of getStatisticsRegistry(SmtEngine*)Andres Notzli
Commit f4ef7af0a2295691f281ee1604dfeb4082fe229c removed the definition of getStatisticsRegistry(SmtEngine*) but not the declaration.
2017-03-30[Coverity] Remove throw qualifiers in src/smtremove_throwAndres Notzli
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
2017-03-28Fix bug 787.ajreynol
2017-03-24Refactor model building for quantifiers to be a single pass, simplification. ↵ajreynol
Modify datatypes collect model info to include dt equivalence classes. Further work on sygus. Other minor fixes.
2017-03-23Fixing warning message.Clark Barrett
2017-03-23support incremental unsat coresguykatzz
2017-03-16Minor fixes, always expand applications of lambdas at preprocess.ajreynol
2017-03-16Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for ↵ajreynol
mkGroundTerm for parametric datatypes. Minor change to run_regression to allow regressions to override input language. Minor refactoring to Cvc.g.
2017-03-06Adding support for bool-to-bvClark Barrett
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.
2017-03-02Minor cleanup and reorganization related to last commit.ajreynol
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵ajreynol
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
2017-01-13Fix call to SExpr constructor for greater portability.Clark Barrett
2016-12-16Fix dependency tracing for fewerPreprocessingHolesAndres Notzli
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.
2016-12-07Fix boolean term conversion for INST_ATTRIBUTE, fixes bug 764.ajreynol
2016-12-07Merge branch 'master' of https://github.com/CVC4/CVC4guykatzz
2016-12-07Turned off nonClausalSimplify when using fewerPreprocessingHoles.guykatzz
It was turned off for unsatCores, and fewerPreprocessingHoles using the same infrastructure.
2016-12-07Refactoring, generalization of bounded inference module. Simplification of ↵ajreynol
rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions.
2016-12-05Added "dump=raw-benchmark" option for dumping all user commands exactly as ↵Clark Barrett
received.
2016-12-02Bug fixes and refactoring of parametric datatypes, add some regressions.ajreynol
2016-11-21Refactoring related to track instantiation option.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback