git.libre-soc.org Git - cvc5.git/search

2020-01-30	Andrew Reynolds	Eliminate spurious postprocessing step for single invocation...	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	Ensure literals in FMF decision strategies are in the...	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	Weaken assertion for models with approximations (#3667)	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	Move disequality list to solver state in strings (...	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	Example minimize evaluation utility. (#3671)	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	External cache argument for evaluator (#3672)	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	Do not debug check model for models with approximations...	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	Modularize more steps in the strings strategy (#3676)	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	Minor updates to string utilities (#3675)	commit \| commitdiff \| tree
2020-01-29	Andrew Reynolds	Fix isLeq function in String utility (#3659)	commit \| commitdiff \| tree
2020-01-28	Andrew Reynolds	Do not insist on bound values being constant in arithmetic...	commit \| commitdiff \| tree
2020-01-28	Andrew Reynolds	Avoid PLUS with one child for bv2nat elimination (...	commit \| commitdiff \| tree
2020-01-23	Andrew Reynolds	Fix trivial solve method for single invocation (#3650)	commit \| commitdiff \| tree
2020-01-22	Andrew Reynolds	Fix subtyping for instantiations where internal representati...	commit \| commitdiff \| tree
2020-01-22	Andrew Reynolds	Fix substitution in nl solver (#3638)	commit \| commitdiff \| tree
2020-01-22	Andrew Reynolds	Fix single invocation partition for non-function non...	commit \| commitdiff \| tree
2020-01-22	Andrew Reynolds	Fix check for subtypes in sygus PBE (#3640)	commit \| commitdiff \| tree
2020-01-22	Andrew Reynolds	Fix parameteric sorts involving Booleans in sygus default...	commit \| commitdiff \| tree
2020-01-17	Andrew Reynolds	Use axioms when checking goal entailment for abduction...	commit \| commitdiff \| tree
2020-01-14	Andrew Reynolds	Generalize example-based sym breaking to conjectures...	commit \| commitdiff \| tree
2020-01-10	Andrew Reynolds	Fix side condition check in sygus core connective ...	commit \| commitdiff \| tree
2020-01-10	Andrew Reynolds	Track trivial cases in transition inference (#3598)	commit \| commitdiff \| tree
2020-01-08	Andrew Reynolds	Fix backtracking issue in sygus fast enumerator (#3593)	commit \| commitdiff \| tree
2020-01-07	Andrew Reynolds	Fix unary minus parse check (#3594)	commit \| commitdiff \| tree
2020-01-07	Andrew Reynolds	Update any-constant and normalization policies for...	commit \| commitdiff \| tree
2020-01-04	Andrew Reynolds	Fix finiteness check for bounded fmf (#3589)	commit \| commitdiff \| tree
2019-12-23	Andrew Reynolds	Initial support for string reverse (#3581)	commit \| commitdiff \| tree
2019-12-18	Andrew Reynolds	Increment Taylor degree for tangent and secant plane...	commit \| commitdiff \| tree
2019-12-17	Andrew Reynolds	Fix spurious parse error for rational real array constants...	commit \| commitdiff \| tree
2019-12-16	Andrew Reynolds	Use the evaluator utility in the function definition...	commit \| commitdiff \| tree
2019-12-16	Andrew Reynolds	Extend model construction with assignment exclusion...	commit \| commitdiff \| tree
2019-12-16	Andrew Reynolds	Move Datatype management to ExprManager (#3568)	commit \| commitdiff \| tree
2019-12-16	Andrew Reynolds	Fix evaluator for non-evaluatable nodes (#3575)	commit \| commitdiff \| tree
2019-12-16	Andrew Reynolds	Revert evaluate as node. (#3574)	commit \| commitdiff \| tree
2019-12-16	Andrew Reynolds	Minor improvement to evaluator (#3570)	commit \| commitdiff \| tree
2019-12-15	Andrew Reynolds	Simple optimizations for the core rewriter (#3569)	commit \| commitdiff \| tree
2019-12-13	Andrew Reynolds	Eliminate Expr-level calls in TypeNode (#3562)	commit \| commitdiff \| tree
2019-12-13	Andrew Reynolds	Add support for set comprehension (#3312)	commit \| commitdiff \| tree
2019-12-13	Andrew Reynolds	Disable check-synth-sol in regression with recursive...	commit \| commitdiff \| tree
2019-12-12	Andrew Reynolds	Make CEGIS sampling robust to non-vanilla CEGIS (#3559)	commit \| commitdiff \| tree
2019-12-12	Andrew Reynolds	Use the node-level datatypes API (#3556)	commit \| commitdiff \| tree
2019-12-12	Andrew Reynolds	Fixes for regressions (#3557)	commit \| commitdiff \| tree
2019-12-12	Andrew Reynolds	Fix CEGIS refinement for recursive functions evaluation...	commit \| commitdiff \| tree
2019-12-12	Andrew Reynolds	Activate node-level datatype API (#3540)	commit \| commitdiff \| tree
2019-12-11	Andrew Reynolds	Do not substitute beneath arithmetic terms in the non...	commit \| commitdiff \| tree
2019-12-11	Andrew Reynolds	Support symbolic unfolding in UNIF+PI (#3553)	commit \| commitdiff \| tree
2019-12-10	Andrew Reynolds	Incorporate rewriting on demand in the evaluator (...	commit \| commitdiff \| tree
2019-12-10	Andrew Reynolds	Allow unsat cores with sygus inference (#3550)	commit \| commitdiff \| tree
2019-12-09	Andrew Reynolds	Disable sygus inference when combined with incremental...	commit \| commitdiff \| tree
2019-12-09	Andrew Reynolds	Fix case of uninterpreted constant instantiation in...	commit \| commitdiff \| tree
2019-12-06	Andrew Reynolds	Throw exception instead of warning for approximate...	commit \| commitdiff \| tree
2019-12-06	Andrew Reynolds	Optimize the rewriter for DT_SYGUS_EVAL (#3529)	commit \| commitdiff \| tree
2019-12-06	Andrew Reynolds	New algorithm for interpolation and abduction based...	commit \| commitdiff \| tree
2019-12-06	Andrew Reynolds	Add ExprManager as argument to Datatype (#3535)	commit \| commitdiff \| tree
2019-12-06	Andrew Reynolds	Introduce the Node-level Datatypes API (#3462)	commit \| commitdiff \| tree
2019-12-05	Andrew Reynolds	Make nonlinear solver intercept model assignments from...	commit \| commitdiff \| tree
2019-12-05	Andrew Reynolds	Refactor mode options for Unif+PI (#3531)	commit \| commitdiff \| tree
2019-12-05	Andrew Reynolds	Fix the subtyping relation for functions (#3494)	commit \| commitdiff \| tree
2019-12-04	Andrew Reynolds	New grammar construction modes for SyGuS (#3486)	commit \| commitdiff \| tree
2019-12-04	Andrew Reynolds	Fix (#3530)	commit \| commitdiff \| tree
2019-12-04	Andrew Reynolds	Fixes for SyGuS PBE + templated string concatenations...	commit \| commitdiff \| tree
2019-12-04	Andrew Reynolds	Fix single invocation solution construction for multiple...	commit \| commitdiff \| tree
2019-12-03	Andrew Reynolds	Improve flexibility of lemma output in non-linear solver...	commit \| commitdiff \| tree
2019-12-02	Andrew Reynolds	Update ownership policy for dynamic quantifiers splitting...	commit \| commitdiff \| tree
2019-12-02	Andrew Reynolds	Fix case of higher-order + sygus inference (#3509)	commit \| commitdiff \| tree
2019-12-02	Andrew Reynolds	Ensure quantifiers options are set with --no-strings...	commit \| commitdiff \| tree
2019-11-30	Andrew Reynolds	Fix fast SyGuS enumeration for interpreted constants...	commit \| commitdiff \| tree
2019-11-29	Andrew Reynolds	Check free variables in assertions when using SyGuS...	commit \| commitdiff \| tree
2019-11-27	Andrew Reynolds	Fix sygus inference for choice functions introduced...	commit \| commitdiff \| tree
2019-11-27	Andrew Reynolds	Fix indexof range lemma (#3499)	commit \| commitdiff \| tree
2019-11-25	Andrew Reynolds	Better front-end type checking for SyGuS (#3496)	commit \| commitdiff \| tree
2019-11-22	Andrew Reynolds	Minor refactoring of compute model value for nl (#3489)	commit \| commitdiff \| tree
2019-11-21	Andrew Reynolds	Evaluation unfolding for symbolic SyGuS constructors...	commit \| commitdiff \| tree
2019-11-18	Andrew Reynolds	Use standard sygus interface for abduction and rewrite...	commit \| commitdiff \| tree
2019-11-18	Andrew Reynolds	Improve interface for sygus datatype, fix utilities...	commit \| commitdiff \| tree
2019-11-18	Andrew Reynolds	Updates to the unit tests, api, and examples for datatypes...	commit \| commitdiff \| tree
2019-11-16	Andrew Reynolds	Use standard interface for sygus default grammar constructio...	commit \| commitdiff \| tree
2019-11-15	Andrew Reynolds	Introduce SyGuS datatype API (#3465)	commit \| commitdiff \| tree
2019-11-15	Andrew Reynolds	Fix wrong kind in sygus version 1 parser (#3463)	commit \| commitdiff \| tree
2019-11-13	Andrew Reynolds	Distinguish unknown status for model printing (#3454)	commit \| commitdiff \| tree
2019-11-13	Andrew Reynolds	Refactor non-linear extension for model-based refinement...	commit \| commitdiff \| tree
2019-11-11	Andrew Reynolds	Add missing utilities for Node-level Datatype API ...	commit \| commitdiff \| tree
2019-11-11	Andrew Reynolds	Eliminate remaining references to type/expr in datatype...	commit \| commitdiff \| tree
2019-11-10	Andrew Reynolds	Fix bugs related to sygus higher-order + recursive...	commit \| commitdiff \| tree
2019-11-09	Andrew Reynolds	Fixes in relations related to datatypes not passed...	commit \| commitdiff \| tree
2019-11-06	Andrew Reynolds	Move more string utility functions (#3398)	commit \| commitdiff \| tree
2019-11-06	Andrew Reynolds	Migrate more datatype methods to the Node level (#3443)	commit \| commitdiff \| tree
2019-11-06	Andrew Reynolds	Support for SyGuS PBE + recursive functions (#3433)	commit \| commitdiff \| tree
2019-11-05	Andrew Reynolds	Separate model object in non-linear extension (#3426)	commit \| commitdiff \| tree
2019-11-05	Andrew Reynolds	Refactor type matcher utility (#3439)	commit \| commitdiff \| tree
2019-11-04	Andrew Reynolds	Make check synth solution robust to auxiliary assertions...	commit \| commitdiff \| tree
2019-11-04	Andrew Reynolds	Fix ho extensionality in collect model info (#3435)	commit \| commitdiff \| tree
2019-11-04	Andrew Reynolds	Avoid non-well-founded sygus grammars (#3434)	commit \| commitdiff \| tree
2019-11-04	Andrew Reynolds	Make getSynthSolution return a Bool (#3306)	commit \| commitdiff \| tree
2019-11-04	Andrew Reynolds	Eliminate deprecated utility function from sygus (...	commit \| commitdiff \| tree
2019-11-01	Andrew Reynolds	Fix non-termination in datatype type enumerator (#3369)	commit \| commitdiff \| tree
2019-11-01	Andrew Reynolds	Eagerly beta reduce during sygus to builtin term conversion...	commit \| commitdiff \| tree
2019-11-01	Andrew Reynolds	Rename datatypes sygus solver (#3417)	commit \| commitdiff \| tree
2019-10-30	Andrew Reynolds	Split some generic utilities from the non-linear extension...	commit \| commitdiff \| tree
2019-10-28	Andrew Reynolds	Fix for non-linear models (#3410)	commit \| commitdiff \| tree
next

RSS Atom