summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2018-10-09Merge branch 'master' into miscWarnsAndres Noetzli
2018-10-09address commentsAndres Noetzli
2018-10-09 Support for basic actively-generated enumerators (#2606)Andrew Reynolds
2018-10-09Random: support URNG interface (#2595)Aina Niemetz
2018-10-09Allow multiple synthesis conjectures. (#2593)Andrew Reynolds
2018-10-08BV instantiator: Factor out util functions. (#2604)Aina Niemetz
2018-10-08 BV inverter: Factor out util functions. (#2603)Aina Niemetz
2018-10-08 Fix string register extended terms (#2597)Andrew Reynolds
2018-10-08Fix compiler warningsAndres Noetzli
2018-10-08 Disable extended rewriter when applicable with var agnostic enumeration (#2594)Andrew Reynolds
2018-10-05Fix unif trace (#2550)Haniel Barbosa
2018-10-05 Fix cache for sygus post-condition inference (#2592)Andrew Reynolds
2018-10-05Update default options for sygus (#2586)Andrew Reynolds
2018-10-04Fix rewrite rule filtering. (#2591)Andrew Reynolds
2018-10-04Infrastructure for string length entailments via approximations (#2514)Andrew Reynolds
2018-10-04Fix end constraint for regexp elimination (#2571)Andrew Reynolds
2018-10-04Clean remaining references to getNextDecisionRequest and simplify (#2500)Andrew Reynolds
2018-10-03Fix compiler warnings. (#2585)Aina Niemetz
2018-10-03Add actively generated sygus enumerators (#2552)Andrew Reynolds
2018-10-03Make CegisUnif with condition independent robust to var agnostic (#2565)Haniel Barbosa
2018-10-03Fix stale op list in sets (#2572)Andrew Reynolds
2018-10-03Eliminate partial operators within lambdas during grammar normalization (#2570)Andrew Reynolds
2018-10-01init scalar class members (coverity issues 1473720 and 1473721) (#2554)Haniel Barbosa
2018-10-01Fix compiler warnings. (#2555)Aina Niemetz
2018-09-30Add rewrite for solving stoi (#2532)Andrew Reynolds
2018-09-29Stream concrete values for variable agnostic enumerators (#2526)Haniel Barbosa
2018-09-28Rewrites for (= "" _) and (= (str.replace _) _) (#2546)Andres Noetzli
2018-09-27Remove assertion. (#2549)Andrew Reynolds
2018-09-27Infrastructure for using active enumerators in sygus modules (#2547)Andrew Reynolds
2018-09-27Incorporate all unification enumerators into getTermList. (#2541)Andrew Reynolds
2018-09-27Fix Taylor overapproximation for large exponentials (#2538)Andrew Reynolds
2018-09-26 Fix homogeneous string constant rewrite (#2545)Andrew Reynolds
2018-09-26Symmetry breaking for variable agnostic enumerators (#2527)Andrew Reynolds
2018-09-25Eagerly ensure literal on active guards for sygus enumerators (#2531)Andrew Reynolds
2018-09-25Fix warnings uncovered by cmake build (#2521)Andrew Reynolds
2018-09-24Fix quantifiers selector over store rewrite (#2510)Andrew Reynolds
2018-09-24Allow partial models for multiple sygus enumerators (#2499)Andrew Reynolds
2018-09-24Infrastructure for variable agnostic sygus enumerators (#2511)Andrew Reynolds
2018-09-24 Improve non-linear check model error handling (#2497)Andrew Reynolds
2018-09-24Refactor strings equality rewriting (#2513)Andrew Reynolds
2018-09-24cmake: Fix dependencies for code generation. (#2524)Mathias Preiner
2018-09-24cmake: Fix theory order #2. (#2522)Mathias Preiner
2018-09-24Unify rewrites related to (str.contains x y) --> (= x y) (#2512)Andres Noetzli
2018-09-24cmake: Fix theory order. (#2518)Mathias Preiner
2018-09-22cmake: Only build libcvc4 and libcvc4parser as libraries.Mathias Preiner
2018-09-22cmake: Remove unused CMakeLists.txtMathias Preiner
2018-09-22cmake: Working build infrastructure.Mathias Preiner
2018-09-22cmake: .cpp generation done, .h generation not yet completeAina Niemetz
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-09-19Decision strategy: incorporate arrays. (#2495)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback