summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2014-10-06Fix a resource limiting issue where interruption didn't occur promptly. Than...Morgan Deters
2014-10-06Some minor cleanup.Morgan Deters
2014-10-06Merge branch '1.4.x'Morgan Deters
2014-10-06fix for bug586Kshitij Bansal
2014-10-02Added internal support for constant arrays.Clark Barrett
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 getModelValue(<non-preregistered term>)Kshitij Bansal
2014-10-01Option for more aggressive merging in UEE.ajreynol
2014-09-30Proofs- and cores-related segfault fixes (mainly a usability issue), thanks C...Morgan Deters
2014-09-29Add option for aggressive model filtering in conjecture generator (enumerate ...ajreynol
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-26Finer-grained resource-limiting in quantifiers.Morgan Deters
2014-09-26Fix AIG bitblaster for unsat cores.Morgan 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 disab...ajreynol
2014-09-18Resource spending support in theories (and especially in quantifiers).Morgan Deters
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 minima...ajreynol
2014-09-16Refactoring of conjecture generator. Determine subgoals are non-canonical ba...ajreynol
2014-09-09Fix bug for variable term triggers within multi-triggers.ajreynol
2014-09-09Accept user-provided triggers with variable terms. Flush lemmas before quant...ajreynol
2014-09-03Merge remote-tracking branch 'origin/master'Kshitij Bansal
2014-09-03check() optimizationKshitij Bansal
2014-09-03Implement and enable --dt-var-exp-quant, cleanup trace messages, minor change...ajreynol
2014-09-03Work on conjecture generator : do not generalize subterms with concrete value...ajreynol
2014-08-29Set instantiation level on skolemized bodies of quantifiers. Rename inst-lev...ajreynol
2014-08-29Do not use pure theory terms as single triggers. Minor cleanup.ajreynol
2014-08-28fixing bug580 caused by bad bv inequality explanationlianah
2014-08-28fixing bug580 caused by bad bv inequality explanationlianah
2014-08-27Fix assertion in rep_set.cpp, avoid full check in datatypes when in conflict.ajreynol
2014-08-26Bug fixes for --purify-triggers, --dt-force-assignment.ajreynol
2014-08-25New option --purify-triggers. Refactoring of InstMatchGenerator.ajreynol
2014-08-24remove some debugging codeKshitij Bansal
2014-08-24improvements to sets sharingKshitij Bansal
2014-08-22Unsat core infrastruture and API (SMT-LIB compliance to come).Morgan Deters
2014-08-21Avoid doing work in quantifiers engine when no quantifiers are asserted.ajreynol
2014-08-21Fix --inst-max-level for strategies that use arbitrary representative terms.ajreynol
2014-08-20Add option for inductive strengthening based on well-founded induction for in...ajreynol
2014-08-18Making getEqualityStatus more powerful for bit-vector theory.lianah
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback