summaryrefslogtreecommitdiff
path: root/src/options
AgeCommit message (Collapse)Author
2016-07-20Print only instantiations that are in the unsat core when --proof is ↵ajreynol
enabled. Add option to minimize sygus solutions based on unsat core (disabled by default).
2016-07-19Add infrastructure for tracking instantiation lemmas (for proofs, and ↵ajreynol
minimization of --dump-instantiations, qe and synthesis solutions). Eliminate quantified arithmetic variables that only have lower/upper bounds. Cleanup strings preprocess, minor fix for str.replace semantics. Reorder cegqi before fmf. Minor cleanup.
2016-07-16Refactor strings extf evaluation info. Ensure strings eager preprocess ↵ajreynol
eliminates all extf symbols during ppRewrite. Add options stringGuessModel and stringUfReduct. Minor optimizations.
2016-07-06Add comment field for model, resolves hack for printing sep logic models.ajreynol
2016-07-05Add option --trigger-active-sel. Recognize simple triggers with polarity. Do ↵ajreynol
not drop patterns from merged prenex (fixes bug 743).
2016-06-23Fixed some warnings, fixed bug in cdhashmap that was crashing cdmap_black,Clark Barrett
re-enabled cdmap_black.
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-06-08Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-06-08LFSC letification is true by defaultGuy
2016-06-08Support for printing a global let map in LFSC proofs.Guy
Added a flag to enable/disbale this feature (enabled by default). Also, added some infrastructure for proving rewrite rules.
2016-06-06Merge pull request #85 from CVC4/master_for_proof_mergeguykatzz
Merge from proof branch
2016-06-03Remove NodeListMap from datatypes and equality inference. Add option ↵ajreynol
--dt-blast-splits.
2016-06-01Merge from proof branchGuy
2016-06-01Revert "Merging proof branch"Guy
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
2016-06-01Merging proof branchGuy
2016-05-24Merged cryptominisat from experimental branch.Liana Hadarean
2016-05-24Improvements to symmetry breaking in sygus search. Minor fix for getting ↵ajreynol
instantiations of non-registered quantifiers in sygus.
2016-05-18Refactor modes for sygus+single invocation. Add option --inst-rlv-cond. ↵ajreynol
Minor fixes for inst max level.
2016-05-16Enable --sygus-direct-eval by default, limit to terms that do not induce ↵ajreynol
Boolean structure. Minor fixes for bitvectors: rewrite SDIV to total operators when options::bitvectorDivByZeroConst is true, fix collectModelInfo when fullModel=false. Lift ITEs in sygus search. Fix sygus initialization related to cbqi.
2016-05-15Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. ↵ajreynol
Enable e-matching when --strings-exp is enabled.
2016-05-12Add casc scripts. Improvements to qcf related to nested quantifiers and ↵ajreynol
variable ordering.
2016-05-10Add smt comp 2016 scripts. Fix for --relevant-triggers. Add minor ↵ajreynol
optimizations to sygus and qcf.
2016-05-05Compute term indices lazily in TermDb. Optimization for qcf to recognize ↵ajreynol
irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges. Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs.
2016-04-28More work on inst propagate. Optimization for qcf to check instances ↵ajreynol
eagerly. Improvements to equality query for disequalities.
2016-04-14Add option --snorm-infer-eq to infer equalities based on normalization in ↵ajreynol
ArithCongruenceManager at standard effort (disabled by default).
2016-04-13Handle parametric datatypes with --quant-ind. Minor updates.ajreynol
2016-04-12Optimizations for QCF to check relevant domain of variable argument ↵ajreynol
positions eagerly, global ordering mechanism for quantified formulas within check. Refactoring of term database.
2016-04-09cardinality operation for finite sets (based on my thesis / ijcar16 paper)Kshitij Bansal
Some further cleanup/fixes pending This is squash of 39 commits (kbansal/card branch + cleanup): * add card operator * local reasoning * towards graph building * first implementation * close cardinality terms * model building * more * more * more * Add aggressive sets rewriting. * Recursively aggressive rewrite sets. * Fix * incomplete card2 implementation * ... * Avoid using auto in sets. * fix merge * more * ... * more * ... * Fixed for loops * Slight modification to computeRelevantTerms * more * .. * more * ... * mv empty set lemma generation to later point * more options/reordering * debug related * more trace * ... * fix merge_nodes, models * rm warnigns * fix compile errors * warning * bug fixes/cleanup * mroe fixes * cleanup * ...
2016-04-09Minor refactoring of entailment tests and quantifiers util. Initial draft of ↵ajreynol
instantiation propagator.
2016-04-04New options for trigger selection, add option --strict-triggers. Do not ↵ajreynol
infer alpha equivalence for quantifiers with annotations, limit rewrite operations when triggers are trusted.
2016-04-03Updating the copyright headers and scripts.Tim King
2016-04-01Improvements to equality inference module: add missing cases for solvable ↵ajreynol
variables, do not infer equalities that are derivable by transitivity of other inferred equalities, refactor solved vars/eqc into one, option to track explanations. Handle case when equality inference in quantifiers can derive purely arithmetic ground conflicts at full effort.
2016-03-31Improvements to trigger selection, min triggers by default. Optimizations ↵ajreynol
for E-matching. Minor work to equality infer.
2016-03-30Updates to E-matching to avoid entailed instantiations earlier. Minor ↵ajreynol
updates to datatypes lemmas, other minor changes.
2016-03-23squash-merge from proof branchGuy
2016-03-23Fixed help for tear-down-incremental optionClark Barrett
2016-03-21New version of the recursive options parsing strategy.Tim King
2016-03-12Add options related to interleaving quantifiers and theory combination, ↵ajreynol
changes default behavior.
2016-03-10Faster conditional rewriting for and/or beneath quantifiers. Improvements to ↵ajreynol
sort inference, related to constants. Add several quantifiers options, minor refactoring.
2016-03-01Shorter explanations for strings based on tracking which parts of normal ↵ajreynol
forms are dependent upon which equalities. Add anti-skolemization module to quantifiers. Disable rewriting of non-clashing equalities between same constructors.
2016-02-29Minor options to datatypes.ajreynol
2016-02-26Refactoring of inferences in strings. Add several options.ajreynol
2016-02-25Minor improvement to partial qe. Add options for representative selection in ↵ajreynol
FMF.
2016-02-24Add entailment checks between length terms to reduce splitting in strings ↵ajreynol
solver. Minor additions to datatypes and qcf.
2016-02-18Implement dynamic splitting for quantified formulas. Minor refactoring of ↵ajreynol
reductions in quantifiers engine.
2016-02-05Add two optimizations for datatypes, currently disabled. Bug fix rewriter ↵ajreynol
for selectors applied to codatatype values.
2016-02-03Added --omit-dont-cares option which doesn't print model values forClark Barrett
variables known to be don't-cares.
2016-02-01Making the references to std more explicit in didyoumean.cpp.Tim King
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback