summaryrefslogtreecommitdiff
path: root/src/theory/uf/theory_uf.h
AgeCommit message (Collapse)Author
2018-09-17Decision strategy: incorporate UF with cardinality constraints (#2476)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-04-10Properly implement function extensionality based on cardinality (#1765)Andrew Reynolds
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
Adds missing override keywords.
2018-02-06Resolving warnings from -Winconsistent-missing-override on clang. (#1563)Tim King
2017-12-08Make collect model info return a Bool (#1421)Andrew Reynolds
2017-09-20Extend quantifier-free UF solver to higher-order. This includes an ex… (#1100)Andrew Reynolds
* Extend quantifier-free UF solver to higher-order. This includes an extensionality inference, and lazy conversion from APPLY_UF to HO_APPLY terms.Implements collectModelInfo and theory combination for HO_APPLY terms. * Update comments, minor changes to functions. Update APPLY_UF skolem to be user-context dependent. * Remove unused NodeList
2017-07-07Update copyright headers.Mathias Preiner
2017-04-04Simplify Theory::collectModelInfo interface to not take deprecated fullModel ↵ajreynol
argument.
2017-03-21Improve computeCareGraph functions to check shared term equality status once ↵ajreynol
per equivalence class pair.
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.
2016-11-03Add priorities to getNextDecision. Properly handle case for finite types + ↵ajreynol
unbounded heaps in sep logic. Fix another simple memory leak in sygus.
2016-05-26Use term indexing in TheoryUF::computeCareGraph. Do not reject model value ↵ajreynol
instantiations in cbqi+BV. Use dag in alpha equivalence check. Fix simple memory leak in fmf.
2016-05-20Improvements to theory combination + strings: do not return trivial care ↵ajreynol
graph, split on length terms for disequal strings. Term indexing for TheoryDatatypes::computeCareGraph. Minor fix in quantifiers rewriter for entailed conditions, strings cardinality.
2016-04-03Updating the copyright headers and scripts.Tim King
2016-03-23squash-merge from proof branchGuy
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-26Merged bit-vector and uf proof branch.Liana Hadarean
2016-01-05Add SmtGlobals ClassTim King
- The options replayStream, lemmaInputChannel, lemmaOutputChannel have been removed due to their datatypes. These datatypes were previously pointers to types that were not usable from the options/ library. - The option replayLog has been removed due to inconsistent memory management. - SmtGlobals is a class that wraps a pointer to each of these removed options. These can each be set independently. - There is a single SmtGlobals per SmtEngine with the lifetime of the SmtEngine. - A pointer to this is freely given to the user of an SmtEngine to parameterize the solver after construction. - Selected classes have been given a copy of this pointer in their constructors. - Removed the dependence on Node from Result. Moving Result back into util/.
2015-10-26Promote InstStrategyCbqi to quantifier module. Cleanup unused code.ajreynol
2014-07-01Update copyrights.Morgan Deters
2014-04-29Fix compiler warning re: TheoryUF destructor.Morgan Deters
2014-04-29Mostly resolves bug #561 memory leaks, and more.Morgan Deters
2014-01-22Delay QuantifiersEngine and UF strong solver initialization until after ↵Morgan Deters
final options/logic are set.
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-02-24added option --model-u-dt-enum for outputting uninterpreted sorts as ↵Andrew Reynolds
datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts
2012-12-01remove instantiator frameworkMorgan Deters
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-26Adding support for a master equality engine. Each theory gets the master ↵Dejan Jovanović
equality engine through the setMasterEqualityEngine method. This is a read-only equality engine, so nothing should be added to it directly. Instead each equality engine that is of interest should have the master equality engine attached to it. To set when to use the master equality engine see TheoryEngine::finishInit().
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
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.)
2012-08-31merge from fmf-devel branch. more updates to models: now with ↵Andrew Reynolds
collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models
2012-07-12merged fmf-devel branch, includes support for SMT2 command get-value and ↵Andrew Reynolds
(extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.
2012-07-06Added virtual destructor to PpRewrite.Tim King
2012-06-11Merge from quantifiers2-trunkmerge branch.Morgan Deters
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure. Adds theory instantiators to many theories. Adds the UF strong solver.
2012-06-10fixes for bug347Dejan Jovanović
it was an issue with constants being merged, which influenced explanations of disequalities. when constants are attempted to be merged, equality engine now enters conflict mode immediately
2012-06-06Changes to the combination mechanism, lots of details. Not done yet, there ↵Dejan Jovanović
are still the AUFBV wrong results, but it seems better. http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5
2012-05-21Updating equality manager to handle tagged trigger terms. Notifications are ↵Dejan Jovanović
pushed out for relationships between terms tagged with the same tag. No performance impact.
2012-05-09* simplifying equality engine interfaceDejan Jovanović
* notifications are now through the interface subclass instead of a template * notifications include constants being merged * changed contextNotifyObj::notify to contextNotifyObj::contextNotifyPop so it's more descriptive and doesn't clutter methods when subclassed * sat solver now has explicit methods to make true and false constants * 0-level literals are removed from explanations of propagations
2012-05-03Some cleanup starting off from trying to understand the sharing code. ↵Dejan Jovanović
Changes include * fixed term visitor from the bvprop branch * removed all the warnings from builds -- warnings are there to be noted *NOT* to be used as scribbles * moved the LogicInfo into the theory constructor
2012-03-22some improvements to the sharing mechanism/interfaceDejan Jovanović
2012-03-02CDMap -> CDHashMapDejan Jovanović
CDSet -> CDHashSet
2012-02-24Theory interface changes:Dejan Jovanović
solve -> ppAsert staticLearning -> ppStaticLearn preprocess -> ppRewrite SolveStatus -> PPAssertStatus (SOLVE_* -> PP_ASSERT_*) via Eclipse refactoring magic.
2011-11-30fix linking errors on oneiricMorgan Deters
2011-10-17Sharing workDejan Jovanović
2011-09-29Some base infrastructure for user push/pop; a few bugfixes to user push/pop ↵Morgan Deters
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
2011-09-15additional stuff for sharing, Dejan Jovanović
2011-09-07fixes for uf/equality engine from the quantifiers branch. mainly ↵Dejan Jovanović
backtracking issues.
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
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.
2011-07-11adding disequality propagationDejan Jovanović
relevant comparison http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2602&reference_id=2590&p=5
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback