projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Add substr, contains and equality rewrites (#2665)
[cvc5.git] / src / theory /
2018-10-20 Andres NoetzliAdd substr, contains and equality rewrites (#2665) tree | commitdiff
2018-10-20 Aina NiemetzBV rewrites (mined): Rule 35: ConcatPullUp with special... tree | commitdiff
2018-10-20 Aina NiemetzBV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_X... tree | commitdiff
2018-10-20 Andrew ReynoldsSygus streaming non-implied predicates (#2660) tree | commitdiff
2018-10-19 Mathias PreinerRemove autotools build system. (#2639) tree | commitdiff
2018-10-19 Andres NoetzliAdd helper to detect length one string terms (#2654) tree | commitdiff
2018-10-19 Andrew ReynoldsNon-implied mode for model cores (#2653) tree | commitdiff
2018-10-18 Andrew ReynoldsNon-contributing find replace rewrite (#2652) tree | commitdiff
2018-10-18 Andrew ReynoldsImprove reduction for str.to.int (#2636) tree | commitdiff
2018-10-18 Andrew ReynoldsConstant length regular expression elimination (#2646) tree | commitdiff
2018-10-18 Andrew ReynoldsSygus query generator (#2465) tree | commitdiff
2018-10-17 Andrew Reynolds Fix context-dependent for positive contains reduction... tree | commitdiff
2018-10-17 Aina NiemetzBV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_O... tree | commitdiff
2018-10-16 Aina NiemetzBV rewrites (mined): Rule 35: Generalized ConcatPullUp... tree | commitdiff
2018-10-16 Aina NiemetzBV rewrites (mined): Rule 35: Generalized ConcatPullUp... tree | commitdiff
2018-10-16 Aina NiemetzBV rewrites (mined): Rule 35: Generalized ConcatPullUp... tree | commitdiff
2018-10-16 Aina NiemetzBV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_A... tree | commitdiff
2018-10-16 Andrew ReynoldsImprove strings reductions including skolem caching... tree | commitdiff
2018-10-16 Andrew ReynoldsImprove reduction for int.to.str (#2629) tree | commitdiff
2018-10-16 Haniel BarbosaOption for shuffling condition pool in CegisUnif (... tree | commitdiff
2018-10-15 Andres NoetzliAdd more (str.replace x y z) rewrites (#2628) tree | commitdiff
2018-10-13 Andres NoetzliReset input language for ExprMiner subsolver (#2624) tree | commitdiff
2018-10-12 Andrew ReynoldsImprovements to rewrite rules from inputs (#2625) tree | commitdiff
2018-10-12 Andres Noetzli Add rewrites for str.replace in str.contains (#2623) tree | commitdiff
2018-10-12 Andrew Reynolds Fix heuristic for string length approximation (#2622) tree | commitdiff
2018-10-11 Andres NoetzliImprove reasoning about empty strings in rewriter ... tree | commitdiff
2018-10-11 Andrew Reynolds Fix partial operator elimination in sygus grammar... tree | commitdiff
2018-10-11 Andrew Reynolds Fix string ext inference for rewrites that introduce... tree | commitdiff
2018-10-11 Andres NoetzliFix compiler warnings (#2602) tree | commitdiff
2018-10-11 Andrew ReynoldsSynthesize rewrite rules from inputs (#2608) tree | commitdiff
2018-10-10 Andrew ReynoldsFix cegis so that evaluation unfolding is not interleav... tree | commitdiff
2018-10-10 Andrew ReynoldsOptimize regular expression elimination (#2612) tree | commitdiff
2018-10-10 Andres NoetzliAdd length-based rewrites for (str.substr _ _ _) (... tree | commitdiff
2018-10-09 Andrew Reynolds Support for basic actively-generated enumerators ... tree | commitdiff
2018-10-09 Aina NiemetzRandom: support URNG interface (#2595) tree | commitdiff
2018-10-09 Andrew ReynoldsAllow multiple synthesis conjectures. (#2593) tree | commitdiff
2018-10-09 Aina NiemetzBV instantiator: Factor out util functions. (#2604) tree | commitdiff
2018-10-09 Aina Niemetz BV inverter: Factor out util functions. (#2603) tree | commitdiff
2018-10-09 Andrew Reynolds Fix string register extended terms (#2597) tree | commitdiff
2018-10-08 Andrew Reynolds Disable extended rewriter when applicable with var... tree | commitdiff
2018-10-05 Haniel BarbosaFix unif trace (#2550) tree | commitdiff
2018-10-05 Andrew Reynolds Fix cache for sygus post-condition inference (#2592) tree | commitdiff
2018-10-05 Andrew ReynoldsUpdate default options for sygus (#2586) tree | commitdiff
2018-10-05 Andrew ReynoldsFix rewrite rule filtering. (#2591) tree | commitdiff
2018-10-04 Andrew ReynoldsInfrastructure for string length entailments via approx... tree | commitdiff
2018-10-04 Andrew ReynoldsFix end constraint for regexp elimination (#2571) tree | commitdiff
2018-10-04 Andrew ReynoldsClean remaining references to getNextDecisionRequest... tree | commitdiff
2018-10-04 Aina NiemetzFix compiler warnings. (#2585) tree | commitdiff
2018-10-03 Andrew ReynoldsAdd actively generated sygus enumerators (#2552) tree | commitdiff
2018-10-03 Haniel BarbosaMake CegisUnif with condition independent robust to... tree | commitdiff
2018-10-03 Andrew ReynoldsFix stale op list in sets (#2572) tree | commitdiff
2018-10-03 Andrew ReynoldsEliminate partial operators within lambdas during gramm... tree | commitdiff
2018-10-01 Haniel Barbosainit scalar class members (coverity issues 1473720... tree | commitdiff
2018-10-01 Aina NiemetzFix compiler warnings. (#2555) tree | commitdiff
2018-09-30 Andrew ReynoldsAdd rewrite for solving stoi (#2532) tree | commitdiff
2018-09-29 Haniel BarbosaStream concrete values for variable agnostic enumerator... tree | commitdiff
2018-09-28 Andres NoetzliRewrites for (= "" _) and (= (str.replace _) _) (#2546) tree | commitdiff
2018-09-27 Andrew ReynoldsRemove assertion. (#2549) tree | commitdiff
2018-09-27 Andrew ReynoldsInfrastructure for using active enumerators in sygus... tree | commitdiff
2018-09-27 Andrew ReynoldsIncorporate all unification enumerators into getTermLis... tree | commitdiff
2018-09-27 Andrew ReynoldsFix Taylor overapproximation for large exponentials... tree | commitdiff
2018-09-27 Andrew Reynolds Fix homogeneous string constant rewrite (#2545) tree | commitdiff
2018-09-26 Andrew ReynoldsSymmetry breaking for variable agnostic enumerators... tree | commitdiff
2018-09-26 Andrew ReynoldsEagerly ensure literal on active guards for sygus enume... tree | commitdiff
2018-09-25 Andrew ReynoldsFix warnings uncovered by cmake build (#2521) tree | commitdiff
2018-09-25 Andrew ReynoldsFix quantifiers selector over store rewrite (#2510) tree | commitdiff
2018-09-25 Andrew ReynoldsAllow partial models for multiple sygus enumerators... tree | commitdiff
2018-09-25 Andrew ReynoldsInfrastructure for variable agnostic sygus enumerators... tree | commitdiff
2018-09-25 Andrew Reynolds Improve non-linear check model error handling (#2497) tree | commitdiff
2018-09-25 Andrew ReynoldsRefactor strings equality rewriting (#2513) tree | commitdiff
2018-09-25 Mathias Preinercmake: Fix dependencies for code generation. (#2524) tree | commitdiff
2018-09-24 Mathias Preinercmake: Fix theory order #2. (#2522) tree | commitdiff
2018-09-24 Andres NoetzliUnify rewrites related to (str.contains x y) --> (... tree | commitdiff
2018-09-24 Mathias Preinercmake: Fix theory order. (#2518) tree | commitdiff
2018-09-22 Mathias Preinercmake: Only build libcvc4 and libcvc4parser as libraries. tree | commitdiff
2018-09-22 Mathias Preinercmake: Remove unused CMakeLists.txt tree | commitdiff
2018-09-22 Mathias Preinercmake: Working build infrastructure. tree | commitdiff
2018-09-22 Aina Niemetzcmake: .cpp generation done, .h generation not yet... tree | commitdiff
2018-09-22 Aina Niemetzcmake: Added initial build infrastructure. tree | commitdiff
2018-09-19 Andrew ReynoldsDecision strategy: incorporate arrays. (#2495) tree | commitdiff
2018-09-19 Andres NoetzliAdd rewrites for str.contains + str.replace/substr... tree | commitdiff
2018-09-19 Andrew ReynoldsDecision strategy: incorporate separation logic. (... tree | commitdiff
2018-09-19 Andrew ReynoldsAdd two rewrites for string contains character (#2492) tree | commitdiff
2018-09-19 Andrew Reynolds Refactor strings extended functions inferences (#2480) tree | commitdiff
2018-09-18 Andres NoetzliFix issue with str.idof in evaluator (#2493) tree | commitdiff
2018-09-18 Andrew ReynoldsDecision strategy: incorporate strings fmf. (#2485) tree | commitdiff
2018-09-18 Andrew ReynoldsMore aggressive caching of string skolems. (#2491) tree | commitdiff
2018-09-18 Andrew ReynoldsMove and rename sygus solver classes (#2488) tree | commitdiff
2018-09-18 Andrew ReynoldsClean remaining references to getNextDecisionRequest... tree | commitdiff
2018-09-18 Andrew ReynoldsImprovements and fixes for symmetry detection and break... tree | commitdiff
2018-09-17 Andrew ReynoldsMove inst_strategy_cbqi to inst_strategy_cegqi (#2477) tree | commitdiff
2018-09-17 Andrew ReynoldsDecision strategy: incorporate cegis unif (#2482) tree | commitdiff
2018-09-17 Andrew Reynolds Decision strategy: incorporate bounded integers (... tree | commitdiff
2018-09-17 Andrew ReynoldsDecision strategy: incorporate datatypes sygus solver... tree | commitdiff
2018-09-17 Andrew ReynoldsMore aggressive skolem caching for strings, document... tree | commitdiff
2018-09-17 Andrew ReynoldsMake strings model construction robust to lengths that... tree | commitdiff
2018-09-17 Andrew ReynoldsDecision strategy: incorporate UF with cardinality... tree | commitdiff
2018-09-17 Andrew ReynoldsDecision strategy: incorporate sygus feasible and sygus... tree | commitdiff
2018-09-15 Andres NoetzliRefactor how assertions are added to decision engine... tree | commitdiff
2018-09-14 Andrew ReynoldsAdd Skolem cache for strings, refactor length registrat... tree | commitdiff
next