summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.h
AgeCommit message (Collapse)Author
2019-11-13Distinguish unknown status for model printing (#3454)Andrew Reynolds
2019-11-04Make getSynthSolution return a Bool (#3306)Andrew Reynolds
2019-09-04Towards incremental SyGuS in SMT engine (#3195)Andrew Reynolds
2019-08-19New C++ API: Add checks for Solver::checkValid and ↵Aina Niemetz
Solver::checkValidAssuming. (#3197)
2019-08-14Call separate SMT engine for single invocation sygus (#3151)Andrew Reynolds
2019-08-13SmtEngine: Reorganize class according to guidelines, some cleanup. (#3183)Aina Niemetz
2019-08-13 Track sygus variable to term relationship via attribute (#3182)Andrew Reynolds
2019-08-13Implement check abduct feature (#3152)Andrew Reynolds
2019-08-07New C++ API: Add checks and tests for push/pop. (#3121)Aina Niemetz
2019-08-02Flip the polarity of the argument of get-abduct (#3153)Andrew Reynolds
2019-07-30 Track solver execution mode (#3132)Andrew Reynolds
2019-07-29Model blocker feature (#3112)Andrew Reynolds
2019-07-29Support get-abduct smt2 command (#3122)Andrew Reynolds
2019-06-04Add check that result matches benchmark status (#3028)Andres Noetzli
This commit adds a check to make sure that the result of a `(check-sat)` call matches the expected result set via `(set-info :status ...)`. In doing so, it also fixes an issue where CVC4 would crash if asked for the unsat core after setting the status to `unsat` but before calling `(check-sat)` (see regression for concrete example). This happened because CVC4 was storing the expected result and the computed result both in the same variable (the expected result wasn't really being used though). This commit keeps track of the expected result and the computed result in separate variables to fix that issue.
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
Fixes 2887.
2019-03-26Update copyright headers.Aina Niemetz
2019-03-19Sygus abduction feature (#2744)Andrew Reynolds
2019-01-11New C++ API: Add unit tests for setInfo, setLogic, setOption. (#2782)Aina Niemetz
2018-10-18Introducing internal commands for SyGuS commands (#2627)Haniel Barbosa
2018-08-23Makes the filename be set in the SMT engine by default (#2366)Haniel Barbosa
2018-08-15Fix dumping of get-unsat-assumptions (#2302)Andres Noetzli
When dumping a `get-unsat-assumptions` command, CVC4 was instead dumping two `get-unsat-cores` commands. This commit splits `SmtEngine::getUnsatCores()` into a part that does the dumping and an internal part that actually gets the unsat core without dumping. `SmtEngine::getUnsatAssumptions()` now calls the internal version to avoid the redundant dumping of a `get-unsat-cores` command and changes the command that gets dumped in `SmtEngine::getUnsatAssumptions()`.
2018-08-07Delete functions instead of using CVC4_UNDEFINED (#1794)Andres Noetzli
C++11 supports explicitly deleting functions that should not be used (explictly or implictly), e.g. copy or assignment constructors. We were previously using the CVC4_UNDEFINED macro that used a compiler-specific attribute. The C++11 feature should be more portable.
2018-07-31Improvements and tests for the API around separation logic (#2229)ayveejay
- Introduces a system that validating that, when not using THEORY_SEP, that it is not possible to obtain the separation logic heap/nil (validate_exception()) - Introduces a system test demonstrating how to use the separation logic theory, and then how to use the "getters" to obtain and interrogate the heap/nil expressions (validate_getters()) - Refactors the original getters to avoid duplicate code - Add a check as part of the getters to ensure that THEORY_SEP is in use
2018-07-24Adding API access methods to get heap/nil expressions when using separation ↵ayveejay
logic (#2194)
2018-05-22Make sygus infer find function definitions (#1951)Andrew Reynolds
2018-03-13SmtEngine::getModel() is now public. (#1665)Aina Niemetz
2018-03-09Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653)Aina Niemetz
2018-03-05Add support for check-sat-assuming. (#1637)Aina Niemetz
This adds support for check-sat-assuming. It further adds support for SmtEngine::query() over a vector of Expressions, e.g., smtEngine->query({a, b}); checks the validity (of the current input formula) under assumption (not (or a b)).
2018-03-02Fixed comments in smt_engine.h.Aina Niemetz
2018-02-28SmtEngine::getAssignment now returns a vector of assignments. (#1628)Aina Niemetz
2018-02-02Option to check solutions produced by SyGuS solver (#1553)Haniel Barbosa
2018-01-24Commenting out throw specifiers on SmtEngine. These can later be refined ↵Tim King
into better documentation. (#1512)
2018-01-03Global negate (#1466)Andrew Reynolds
2017-12-10Add new infrastructure for preprocessing passes (#1053)justinxu421
This commit adds new infrastructure for preprocessing passes. It is preparation only, it does not change how the current preprocessing passes work (this will be done in future commits).
2017-12-06Add command for define-fun-rec and add to API (#1412)Andrew Reynolds
2017-11-15Adding garbage collection for Proof objects. (#1294)Tim King
2017-11-07Allow FORALL in quantifier elimination command (#1322)Andrew Reynolds
* Allow FORALL passed as an argument to get-qe. * Document * Format * Minor
2017-10-11Move unsat core names to smt engine (#1192)Andrew Reynolds
* Move unsat core names to SmtEnginePrivate. Adds a SetExpressionNameCommand to do this. Removes the names field from GetUnsatCoreCommand. * Comment * Pass expression names by reference. * Update throw specifiers. * Minor * Switch expression names to CDMap, simplify interface for printing unsat core names. * Revert throw specifier change. * Minor simplifcations
2017-09-14Simplifying the throw specifier of SmtEngine::checkSat and related calls to ↵Tim King
CVC4::Exception. (#1085)
2017-07-19Removing the unused CDAttribute. This makes CDHashMap::obliterate unused. ↵Tim King
Removing it as well.
2017-07-07Update copyright headers.Mathias Preiner
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-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
2016-11-04Fix a few more minor memory leaks.ajreynol
2016-10-28Add get instantiations utilities to API.ajreynol
2016-04-20update from the masterPaulMeng
2016-01-28Adding listeners to Options.Tim King
- Options -- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options. -- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners. -- Added functions to Options for registering listeners of the notify calls. -- Changed a number of options to use the new listener infrastructure. -- Fixed a number of warnings in options. -- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure. -- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}. - Theories -- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options. - Ostream Handling: -- Added new functionality that generalized how ostreams are opened, options/open_stream.h. -- Simplified the memory management for different ostreams, smt/managed_ostreams.h. -- Had the SmtEnginePrivate manage the memory for the ostreams set by options. -- Simplified how the setting of ostreams are updated, smt/update_ostream.h. - Configuration and Tags: -- Configuration can now be used during predicates and handlers for options. -- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/. -- Moved {Debug,Trace}_tags.* from being generated in options/ into base/. - cvc4_private.h -- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's. -- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations. -- Made lib/lib/clock_gettime.h a cvc4_private_library.h header. - Antlr -- Fixed antlr and cvc4 macro definition conflicts that caused warnings. - SmtGlobals -- Refactored replayStream and replayLog out of SmtGlobals. -- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.
2016-01-08Removing StatisticsRegistry's static functions current() and registerStat().Tim King
- The functionality the get the StatisticsRegistry attached to the SmtEngine was previously through StatisticsRegistry::current(). This is the dominant StatisticsRegistry in the code. (There is another StatisticsRegistry attached to the NodeManager.) Having this be a static function on StatisticsRegistry requires the use of an SmtEngine in the wrong compilation unit. - Usages of StatisticsRegistry::current() that were visible in prop/{bvminisat,minisat} has been removed. A pointer to the relevant StatisticsRegistry should be passed instead into the constructor. - The function StatisticsRegistry::current() has been replaced by SmtScope::currentStatisticsRegistry(). SmtScope is in the libcvc4 package, where SmtEngine is available in the compilation unit. - The function smtStatisticsRegistry() is a synonym for SmtScope::currentStatisticsRegistry() in smt/smt_statistics_registry.h. This header has fewer include dependencies than the one for SmtScope. - Correspondingly, the static functions StatisticsRegistry::{registerStat, unregisterStat} have been removed. One should instead use smtStatisticsRegistry()->{registerStat,unregisterStat} instead. - The KEEP_STATISTIC macro has been moved into smt/smt_statistics_registry.h. - Documents the reason StatisticsRegistry is CVC4_PUBLIC. This lets me remove the warning I added. - Removing most operators for timespec from statistics_registry.h file. These a bit error prone in clang. - Most of the really confusing ifdef's in util/statistics_registry.h are gone.
2016-01-05Moving sexpr.{cpp,h,i} from expr/ back into util/.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback