summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2020-02-26Basic support for regular expression complement (#3437)Andrew Reynolds
2020-02-26Use default consts when not using any const during grammar normalization (#3807)Andrew Reynolds
2020-02-26Fix node arity issue in reduction of int2bv (#3777)Andrew Reynolds
2020-02-26Move equivalence class info to its own file in strings (#3799)Andrew Reynolds
2020-02-26Support for witnessing choice in models (#3781)Andrew Reynolds
2020-02-26Remove portfolio leftovers (#3821)Andres Noetzli
2020-02-25remove redundant includes (#3815)yoni206
2020-02-24Fixes for quantifiers documentation (#3811)Andrew Reynolds
2020-02-24Utilities for words (#3797)Andrew Reynolds
2020-02-24Make lambda rewriter more robust (#3806)Andres Noetzli
2020-02-22Minor refactoring of equality notifications (#3798)Andrew Reynolds
2020-02-22 Move check memberships to reg exp solver (#3793)Andrew Reynolds
2020-02-21Move cardinality inference scheme to base solver in strings (#3792)Andrew Reynolds
2020-02-21Dump boolean propagations and conflicts for decision tree org-mode viewer (#3...makaimann
2020-02-21Split extended functions solver in strings (#3768)Andrew Reynolds
2020-02-20Remove front-end support for Chain (#3767)Andrew Reynolds
2020-02-20Minor removals (#3786)Andrew Reynolds
2020-02-19resource manager: Add statistic for every resource. (#3772)Mathias Preiner
2020-02-19Fix symmetry breaking for multiple sygus types (#3775)Andrew Reynolds
2020-02-19Delay enumerative instantiation if theory engine does not need check (#3774)Andrew Reynolds
2020-02-18Fix approximate bounds for transcendental functions whose model values rewrit...Andrew Reynolds
2020-02-17Option to limit the number of rounds of enumerative instantiation (#3760)Andrew Reynolds
2020-02-17 Fix soundness bug in reduction of integer div/mod (#3766)Andrew Reynolds
2020-02-16Fix simple issue with cache (#3762)Andrew Reynolds
2020-02-16Activate reverse variant of F-Split inference (#3745)Andres Noetzli
2020-02-15Disable regression (#3761)Andrew Reynolds
2020-02-15Move proxy variables to InferenceManager in strings (#3758)Andrew Reynolds
2020-02-14Remove quantifiers rewrite rules infrastructure (#3754)Andrew Reynolds
2020-02-12Ensure ext rewrites for associative ops dont throw assertions for kind aritie...Andrew Reynolds
2020-02-11Fix non-linear equality solving that involves mixed real/integer arithmetic (...Andrew Reynolds
2020-02-11Fix term simplification based on entailment in quantifiers rewriter (#3746)Andrew Reynolds
2020-02-11Remove `--strings-binary-csp` option (#3743)Andres Noetzli
2020-02-10Refactor `CoreSolver::processSimpleNEq()` (#3736)Andres Noetzli
2020-02-10Use example evaluation cache instead of sygus PBE (#3733)Andrew Reynolds
2020-02-07Split strings finite model finding strategy (#3727)Andrew Reynolds
2020-02-07Split core solver from the theory of strings (#3713)Andrew Reynolds
2020-02-07Interface for example evaluation cache utilities (#3726)Andrew Reynolds
2020-02-07Univeset Cardinality constraints for infinite types (#3712)mudathirmahgoub
2020-02-07Statistics for fast enumerator (#3699)Andrew Reynolds
2020-02-07Example evaluation cache utility (#3698)Andrew Reynolds
2020-02-06Fix exact sqrt (#3721)Andrew Reynolds
2020-02-06Generalize containsQuantifiers to hasClosure (#3722)Andrew Reynolds
2020-02-04Articulate proof-related debug statements in arith (#3700)Alex Ozdemir
2020-02-04--fp-exp: Better warning message. (#3709)Aina Niemetz
2020-02-04Split base solver from the theory of strings (#3680)Andrew Reynolds
2020-02-04Revert semantic change from refactoring (#3711)Andres Noetzli
2020-02-03Fix corner case - might need to REWRITE_AGAIN (#3706)Clark Barrett
2020-02-03Fix cardinality of uninterpreted types when univset is not used (#3663)mudathirmahgoub
2020-02-03Split on model values when repaired model from non-linear is inconsisent (#3668)Andrew Reynolds
2020-02-03Fix invariant template inference for trivially infeasible conjecture (#3693)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback