| Age | Commit message (Collapse) | Author |
|---|
|
solver. Minor additions to datatypes and qcf.
|
|
|
|
|
|
Disable ITE terms in quant conflict find.
|
|
|
|
reductions in quantifiers engine.
|
|
fixes in quantifiers related to subtypes/parametric sorts. Make macros trace dependencies for get-unsat-core. Add regressions.
|
|
|
|
preprocessing, implement get-qe-disjunct.
|
|
rewriter.
|
|
|
|
|
|
records, replace with datatypes throughout, update cvc printer for tuples/records. Minor changes to API for records and tuples.
|
|
incomplete for fmc.
|
|
|
|
|
|
to quantifier instantiations.
|
|
enumerator and codatatype rewriter, further simplify fmc.
|
|
The explanation for a != b is now:
1. a == find(a)
2. ( find(a) == find(b) ) == false
3. find(b) == b
This simplifies the creation of transitivity proofs for disequalities.
|
|
for selectors applied to codatatype values.
|
|
|
|
variables known to be don't-cares.
|
|
Breaking an edge between the sat solver and command.h.
|
|
type.h.
|
|
process.
|
|
|
|
be compiled.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- 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}.
|
|
|
|
values. Add regression.
|
|
|
|
|
|
uninterpreted sorts. Modify TheoryModelBuilder. Fix bug in fmf-empty-sorts.
|
|
respect cardinality bounds on when finite model finding is enabled.
|
|
datatypes model generation for UFinite datatypes when FMF.
|
|
Listeners for reporting hard and soft resource out() events.
|
|
- 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.
|
|
|
|
|
|
|
