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

2020-02-20	Andrew Reynolds	Minor removals (#3786)	commit \| commitdiff \| tree
2020-02-19	Andrew Reynolds	Fix symmetry breaking for multiple sygus types (#3775)	commit \| commitdiff \| tree
2020-02-19	Andrew Reynolds	Delay enumerative instantiation if theory engine does...	commit \| commitdiff \| tree
2020-02-19	Andrew Reynolds	Change Record to shared_ptr (#3778)	commit \| commitdiff \| tree
2020-02-19	Andrew Reynolds	Fix approximate bounds for transcendental functions...	commit \| commitdiff \| tree
2020-02-18	Andrew Reynolds	Add missing kinds for the new API (#3757)	commit \| commitdiff \| tree
2020-02-17	Andrew Reynolds	Option to limit the number of rounds of enumerative...	commit \| commitdiff \| tree
2020-02-17	Andrew Reynolds	Fix soundness bug in reduction of integer div/mod...	commit \| commitdiff \| tree
2020-02-16	Andrew Reynolds	Fix simple issue with cache (#3762)	commit \| commitdiff \| tree
2020-02-16	Andrew Reynolds	Add temporary global API conversion utilities. (#3759)	commit \| commitdiff \| tree
2020-02-16	Andrew Reynolds	Disable regression (#3761)	commit \| commitdiff \| tree
2020-02-15	Andrew Reynolds	Move proxy variables to InferenceManager in strings...	commit \| commitdiff \| tree
2020-02-14	Andrew Reynolds	Remove quantifiers rewrite rules infrastructure (#3754)	commit \| commitdiff \| tree
2020-02-14	Andrew Reynolds	Update sygus v1 parser to use ParseOp utility (#3756)	commit \| commitdiff \| tree
2020-02-13	Andrew Reynolds	Const input for sygus print callback (#3755)	commit \| commitdiff \| tree
2020-02-12	Andrew Reynolds	Ensure ext rewrites for associative ops dont throw...	commit \| commitdiff \| tree
2020-02-12	Andrew Reynolds	Fix non-linear equality solving that involves mixed...	commit \| commitdiff \| tree
2020-02-11	Andrew Reynolds	Fix term simplification based on entailment in quantifiers...	commit \| commitdiff \| tree
2020-02-11	Andrew Reynolds	Use example evaluation cache instead of sygus PBE ...	commit \| commitdiff \| tree
2020-02-08	Andrew Reynolds	Fix rewrite rules sat regressions (#3734)	commit \| commitdiff \| tree
2020-02-08	Andrew Reynolds	Split strings finite model finding strategy (#3727)	commit \| commitdiff \| tree
2020-02-08	Andrew Reynolds	Split core solver from the theory of strings (#3713)	commit \| commitdiff \| tree
2020-02-08	Andrew Reynolds	Interface for example evaluation cache utilities (...	commit \| commitdiff \| tree
2020-02-07	Andrew Reynolds	Refactor check-model handling in SmtEngine (#3723)	commit \| commitdiff \| tree
2020-02-07	Andrew Reynolds	Statistics for fast enumerator (#3699)	commit \| commitdiff \| tree
2020-02-07	Andrew Reynolds	Example evaluation cache utility (#3698)	commit \| commitdiff \| tree
2020-02-07	Andrew Reynolds	Fix exact sqrt (#3721)	commit \| commitdiff \| tree
2020-02-06	Andrew Reynolds	Generalize containsQuantifiers to hasClosure (#3722)	commit \| commitdiff \| tree
2020-02-05	Andrew Reynolds	Fix QF_NIA smt comp script (#3715)	commit \| commitdiff \| tree
2020-02-04	Andrew Reynolds	Split base solver from the theory of strings (#3680)	commit \| commitdiff \| tree
2020-02-03	Andrew Reynolds	Utility function for getting component types (#3703)	commit \| commitdiff \| tree
2020-02-03	Andrew Reynolds	Minor fixes to regressions (#3702)	commit \| commitdiff \| tree
2020-02-03	Andrew Reynolds	Split on model values when repaired model from non...	commit \| commitdiff \| tree
2020-02-03	Andrew Reynolds	Fix invariant template inference for trivially infeasible...	commit \| commitdiff \| tree
2020-02-03	Andrew Reynolds	Fix corner case of empty domains in bounded fmf (#3690)	commit \| commitdiff \| tree
2020-02-03	Andrew Reynolds	Example inference utility (#3670)	commit \| commitdiff \| tree
2020-01-31	Andrew Reynolds	Allow PBE symmetry breaking with sygus stream (#3686)	commit \| commitdiff \| tree
2020-01-31	Andrew Reynolds	Refactor relevance vectors for asserted quantifiers...	commit \| commitdiff \| tree
2020-01-31	Andrew Reynolds	Update sygus grammar normalization to use node-level...	commit \| commitdiff \| tree
2020-01-31	Andrew Reynolds	Refactor sygus stats (#3684)	commit \| commitdiff \| tree
2020-01-31	Andrew Reynolds	Minor refactoring of constructor classes in fast enumerator...	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	Fix rep set increment for empty domains (#3682)	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	Make eq chain an aggressive rewrite in extended rewriter...	commit \| commitdiff \| tree
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
next

RSS Atom