summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-10-02Added internal support for constant arrays.Clark Barrett
2014-10-02Merge branch '1.4.x'.Morgan Deters
2014-10-02Added option for developer use onlyClark Barrett
2014-10-02More model-based combination for arraysClark Barrett
2014-10-02Better getEqualityStatus for arrays, smarter combination of theoriesClark Barrett
2014-10-02Fix comment in SmtEngine.Morgan Deters
2014-10-02Merge pull request #54 from kbansal/bugfix_setssegfaultMorgan Deters
fix getModelValue(<non-preregistered term>)
2014-10-02fix getModelValue(<non-preregistered term>)Kshitij Bansal
2014-10-02Fix for an array-of-record model generation assert-fail (assert was too strong).Morgan Deters
2014-10-01Option for more aggressive merging in UEE.ajreynol
2014-09-30Merge branch '1.4.x'Morgan Deters
2014-09-30Fix improper #inclusion of private header outside library.Morgan Deters
2014-09-30Fix a command-replay bug in tear-down-incremental mode. Thanks to Christoph ↵Morgan Deters
Sticksel for the report.
2014-09-30Proofs- and cores-related segfault fixes (mainly a usability issue), thanks ↵Morgan Deters
Christoph Sticksel for reporting these.
2014-09-29Add option for aggressive model filtering in conjecture generator (enumerate ↵ajreynol
ground terms).
2014-09-27Merge branch '1.4.x'Morgan Deters
2014-09-27Fix infinite loop in --bitblast-aig/--bv-aig-simp options.Morgan Deters
2014-09-26Merge branch '1.4.x'Morgan Deters
2014-09-26Fix bv options doc.Morgan Deters
2014-09-26Fix some configuration-related oddness.Morgan Deters
2014-09-26Clarify some licensing-related things.Morgan Deters
2014-09-26Finer-grained resource-limiting in quantifiers.Morgan Deters
2014-09-26Fix AIG bitblaster for unsat cores.Morgan Deters
2014-09-25fix unit test for new fair datatype enumerationMorgan Deters
2014-09-25Fair datatype enumeration.ajreynol
2014-09-24Fix infinite loop in datatypes enumerator. Minor work on conjecture generator.ajreynol
2014-09-24Refactor option for uf+cardinality constraints solver.ajreynol
2014-09-24Partial support for codatatype models.ajreynol
2014-09-23Support :no-pattern.ajreynol
2014-09-23Do not throw error when codatatype is not well-founded. Add option for ↵ajreynol
disabling codatatype reasoning. Minor cleanup.
2014-09-18Resource spending support in theories (and especially in quantifiers).Morgan Deters
2014-09-18cvc4terminate infinite loop fixKshitij Bansal
2014-09-18cvc4terminate infinite loop fixKshitij Bansal
2014-09-17Merge branch '1.4.x' while ignoring commit 8d5eb49.Kshitij Bansal
2014-09-17Fix fix. There are no unsat cores in 1.4Kshitij Bansal
2014-09-17Merge branch '1.4.x'Kshitij Bansal
2014-09-17Fix (push) and (pop). Thanks to Christoph Sticksel for the bug report.Kshitij Bansal
2014-09-17Fix soundness bug for quantifier macros involving Int/Real.ajreynol
2014-09-17Refactor entailment filtering for conjecture generator. Other minor cleanup.ajreynol
2014-09-17More refactoring of conjecture generation. Term generation into own class.ajreynol
2014-09-16Bug fix variable triggers with --inst-max-level : use term in EQC with ↵ajreynol
minimal instantiation level.
2014-09-16Refactoring of conjecture generator. Determine subgoals are non-canonical ↵ajreynol
based on ground equalities. Add filtering options to options file.
2014-09-09Fix bug for variable term triggers within multi-triggers.ajreynol
2014-09-09Accept user-provided triggers with variable terms. Flush lemmas before ↵ajreynol
quantifiers check. Minor fix for conjecture generation.
2014-09-04Update command_executor_portfolio.cppKshitij Bansal
2014-09-03Merge remote-tracking branch 'origin/master'Kshitij Bansal
2014-09-03check() optimizationKshitij Bansal
Details of testing here: http://church.cims.nyu.edu/wiki/User:Kshitij/theorycheckoptimization
2014-09-03Implement and enable --dt-var-exp-quant, cleanup trace messages, minor ↵ajreynol
changes for relevant term filtering.
2014-09-03Work on conjecture generator : do not generalize subterms with concrete ↵ajreynol
values, filter conjectures with ground substitutions whose equality is unknown, simplify generalization depth calculation. Print --dump-instantiations on sat/unknown.
2014-08-29Set instantiation level on skolemized bodies of quantifiers. Rename ↵ajreynol
inst-level attribute to quant-inst-max-level
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback