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

2020-03-06	Andrew Reynolds	Support default sygus grammar construction for sets...	commit \| commitdiff \| tree
2020-03-05	Andrew Reynolds	Migrate a majority of the functionality in parsers...	commit \| commitdiff \| tree
2020-03-05	Andrew Reynolds	Move ownership of DecisionEngine into PropEngine. ...	commit \| commitdiff \| tree
2020-03-05	Andrew Reynolds	Fix issues with real to int (#3918)	commit \| commitdiff \| tree
2020-03-03	Andrew Reynolds	Standardize the interface for SMT engine subsolvers...	commit \| commitdiff \| tree
2020-03-02	Andrew Reynolds	Split collect model info by types in strings (#3847)	commit \| commitdiff \| tree
2020-02-29	Andrew Reynolds	Convert more uses of string to word (#3834)	commit \| commitdiff \| tree
2020-02-29	Andrew Reynolds	Throw warning instead of error for non-constant values...	commit \| commitdiff \| tree
2020-02-29	Andrew Reynolds	Fix assertion related to assignability in the model...	commit \| commitdiff \| tree
2020-02-29	Andrew Reynolds	Replace conditional rewrite pass in quantifiers with...	commit \| commitdiff \| tree
2020-02-28	Andrew Reynolds	Use enum for quantifiers rewrite steps (#3840)	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Refactor operator applications in the parser (#3831)	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Update purifySygusGTerm to the new API (#3830)	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Fix large models for strings (#3835)	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Add support for is_digit and regular expression difference...	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Disable regression that times out on debug (#3833)	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Move fix for vacuous sygus types out of the parser...	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Initial work towards -Wshadow (#3817)	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Some initial work on using words (#3819)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Infrastructure for tautological literals in nonlinear...	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Use side effect utility for non-linear lemmas (#3780)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Fix regression (#3827)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	More fixes for printing sygus commands (#3812)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Basic support for regular expression complement (#3437)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Refactor type ascriptions in the parser (#3825)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Minor improvement to ParseOp (#3808)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Use default consts when not using any const during...	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Fix node arity issue in reduction of int2bv (#3777)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Move equivalence class info to its own file in strings...	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Support for witnessing choice in models (#3781)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Minor cleaning of smt2 parser (#3823)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Embed mkAssociative utilities within the API. (#3801)	commit \| commitdiff \| tree
2020-02-24	Andrew Reynolds	Fixes for quantifiers documentation (#3811)	commit \| commitdiff \| tree
2020-02-24	Andrew Reynolds	Utilities for words (#3797)	commit \| commitdiff \| tree
2020-02-24	Andrew Reynolds	Convert parser input interface to api::Term (#3809)	commit \| commitdiff \| tree
2020-02-24	Andrew Reynolds	Add missing functions to new C++ API (#3769)	commit \| commitdiff \| tree
2020-02-23	Andrew Reynolds	Minor refactoring of equality notifications (#3798)	commit \| commitdiff \| tree
2020-02-22	Andrew Reynolds	Move check memberships to reg exp solver (#3793)	commit \| commitdiff \| tree
2020-02-22	Andrew Reynolds	Move cardinality inference scheme to base solver in...	commit \| commitdiff \| tree
2020-02-21	Andrew Reynolds	Simple changes towards unicode string standard (#3791)	commit \| commitdiff \| tree
2020-02-21	Andrew Reynolds	Split extended functions solver in strings (#3768)	commit \| commitdiff \| tree
2020-02-20	Andrew Reynolds	Remove front-end support for Chain (#3767)	commit \| commitdiff \| tree
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
next

RSS Atom