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

2020-04-15	Andrew Reynolds	Fix assertion in enumerative instantiation (#4313)	commit \| commitdiff \| tree
2020-04-15	Andrew Reynolds	Convert more cases of strings to words (#4206)	commit \| commitdiff \| tree
2020-04-15	Andrew Reynolds	Abort if in conflict in enumerative instantiation ...	commit \| commitdiff \| tree
2020-04-15	Andrew Reynolds	Always flush lemmas from downwards closure in sets...	commit \| commitdiff \| tree
2020-04-15	Andrew Reynolds	Do not normalize to representatives for variable equalities...	commit \| commitdiff \| tree
2020-04-15	Andrew Reynolds	Always assign function values in higher order (#4279)	commit \| commitdiff \| tree
2020-04-15	Andrew Reynolds	Fix combinations of cegqi and non-standard triggers...	commit \| commitdiff \| tree
2020-04-15	Andrew Reynolds	Disable preregistration of instantiations for cegqi...	commit \| commitdiff \| tree
2020-04-14	Andrew Reynolds	Disable macros when higher-order (#4266)	commit \| commitdiff \| tree
2020-04-14	Andrew Reynolds	Fix relevant domain computation for nested quantifiers...	commit \| commitdiff \| tree
2020-04-14	Andrew Reynolds	Remove a few options (#4295)	commit \| commitdiff \| tree
2020-04-14	Andrew Reynolds	Remove a few spurious assertions (#4294)	commit \| commitdiff \| tree
2020-04-14	Andrew Reynolds	Remove early type check option (#4234)	commit \| commitdiff \| tree
2020-04-14	Andrew Reynolds	Remove argument extender (#4223)	commit \| commitdiff \| tree
2020-04-14	Andrew Reynolds	Remove mergePredicates from EqualityEngine interface...	commit \| commitdiff \| tree
2020-04-14	Andrew Reynolds	Fix dump-unsat-cores-full (#4303)	commit \| commitdiff \| tree
2020-04-13	Andrew Reynolds	Fix SyGuS define-fun printing from benchmarks coming...	commit \| commitdiff \| tree
2020-04-12	Andrew Reynolds	Fixes for extended rewriter (#4278)	commit \| commitdiff \| tree
2020-04-12	Andrew Reynolds	Move slow nl regression to regress3 (#4276)	commit \| commitdiff \| tree
2020-04-11	Andrew Reynolds	Ensure exported sygus solutions match grammar (#4270)	commit \| commitdiff \| tree
2020-04-11	Andrew Reynolds	Split the non-linear solver (#4219)	commit \| commitdiff \| tree
2020-04-10	Andrew Reynolds	Explain non-emptiness by non-zero length in strings...	commit \| commitdiff \| tree
2020-04-10	Andrew Reynolds	Add a few stats to strings (#4252)	commit \| commitdiff \| tree
2020-04-10	Andrew Reynolds	Towards proper use of resource managers (#4233)	commit \| commitdiff \| tree
2020-04-09	Andrew Reynolds	Disable slow sygus regression (#4232)	commit \| commitdiff \| tree
2020-04-09	Andrew Reynolds	Split ProcessAssertions module from SmtEngine (#4210)	commit \| commitdiff \| tree
2020-04-08	Andrew Reynolds	Fix dump models and dump proofs (#4230)	commit \| commitdiff \| tree
2020-04-08	Andrew Reynolds	Eliminate call to currentNM within NodeManager (#4227)	commit \| commitdiff \| tree
2020-04-07	Andrew Reynolds	Cleanup deprecated quantifiers attribute features ...	commit \| commitdiff \| tree
2020-04-07	Andrew Reynolds	Disable slow regression (#4221)	commit \| commitdiff \| tree
2020-04-07	Andrew Reynolds	Enum for all remaining string inferences (#4220)	commit \| commitdiff \| tree
2020-04-06	Andrew Reynolds	Remove links field in all toml files (#4201)	commit \| commitdiff \| tree
2020-04-05	Andrew Reynolds	Add missing stat for lemmas based on inferences (#4214)	commit \| commitdiff \| tree
2020-04-05	Andrew Reynolds	Type-independent preregistration of empty word (#4205)	commit \| commitdiff \| tree
2020-04-03	Andrew Reynolds	Only rewrite lambdas via array representations when...	commit \| commitdiff \| tree
2020-04-03	Andrew Reynolds	Split sequences rewriter (#4194)	commit \| commitdiff \| tree
2020-04-02	Andrew Reynolds	Introduce enums for all string inferences, excluding...	commit \| commitdiff \| tree
2020-04-01	Andrew Reynolds	Support char smt-lib syntax (#4188)	commit \| commitdiff \| tree
2020-03-31	Andrew Reynolds	Fix fmf benchmark (#4193)	commit \| commitdiff \| tree
2020-03-31	Andrew Reynolds	Remove replay and use-theory options and idl (#4186)	commit \| commitdiff \| tree
2020-03-31	Andrew Reynolds	Fix strange bound regression (#4192)	commit \| commitdiff \| tree
2020-03-31	Andrew Reynolds	Convert more uses of string-specific functions (#4158)	commit \| commitdiff \| tree
2020-03-31	Andrew Reynolds	Fixing regressions (#4189)	commit \| commitdiff \| tree
2020-03-30	Andrew Reynolds	Rewrites for all remaining return statements in strings...	commit \| commitdiff \| tree
2020-03-30	Andrew Reynolds	Support indexed operators re.loop and re.^ (#4167)	commit \| commitdiff \| tree
2020-03-30	Andrew Reynolds	Remove ref skolem datatype option (#4185)	commit \| commitdiff \| tree
2020-03-30	Andrew Reynolds	Fix arguments to print callback (#4171)	commit \| commitdiff \| tree
2020-03-29	Andrew Reynolds	Enumeration for String rewrites (#4173)	commit \| commitdiff \| tree
2020-03-28	Andrew Reynolds	Split transcendental solver to its own file (#4156)	commit \| commitdiff \| tree
2020-03-27	Andrew Reynolds	Fix expected output on arith regression (#4162)	commit \| commitdiff \| tree
2020-03-27	Andrew Reynolds	Move string utility file (#4164)	commit \| commitdiff \| tree
2020-03-27	Andrew Reynolds	Do not require that function sorts are first class...	commit \| commitdiff \| tree
2020-03-27	Andrew Reynolds	Support unicode internal representation and escape...	commit \| commitdiff \| tree
2020-03-27	Andrew Reynolds	Move set defaults function to its own file (#4154)	commit \| commitdiff \| tree
2020-03-26	Andrew Reynolds	Disable slow regression (#4157)	commit \| commitdiff \| tree
2020-03-26	Andrew Reynolds	Add stats for string reductions, lemmas and conflicts...	commit \| commitdiff \| tree
2020-03-26	Andrew Reynolds	Generalize more string-specific functions (#4152)	commit \| commitdiff \| tree
2020-03-26	Andrew Reynolds	Care graphs based on polymorphic operators in strings...	commit \| commitdiff \| tree
2020-03-25	Andrew Reynolds	Generalize more uses of string-specific functions...	commit \| commitdiff \| tree
2020-03-24	Andrew Reynolds	Restrict partial triggers to standard quantified formulas...	commit \| commitdiff \| tree
2020-03-24	Andrew Reynolds	Restrict cases of sygus grammar reduction based on...	commit \| commitdiff \| tree
2020-03-23	Andrew Reynolds	Infer when sygus operators are equivalent to builtin...	commit \| commitdiff \| tree
2020-03-23	Andrew Reynolds	Simplify auxiliary variable handling in CEGQI (#4141)	commit \| commitdiff \| tree
2020-03-23	Andrew Reynolds	Throw exception for non-well-founded unimplemented...	commit \| commitdiff \| tree
2020-03-23	Andrew Reynolds	Change transcendental function app slave list to unordered_s...	commit \| commitdiff \| tree
2020-03-22	Andrew Reynolds	Sort inference does not handle APPLY_UF when higher...	commit \| commitdiff \| tree
2020-03-20	Andrew Reynolds	Generalize mkConcat for types (#4123)	commit \| commitdiff \| tree
2020-03-20	Andrew Reynolds	Fix variable shadowing issue in sygus-inference (#4121)	commit \| commitdiff \| tree
2020-03-20	Andrew Reynolds	Fix sort comparison within assertion in cegis (#4113)	commit \| commitdiff \| tree
2020-03-20	Andrew Reynolds	Guard cases of sort inference in quantifier free logics...	commit \| commitdiff \| tree
2020-03-20	Andrew Reynolds	Split string-specific operators from TheoryStringsRewriter...	commit \| commitdiff \| tree
2020-03-20	Andrew Reynolds	Do not assign higher-order representative if function...	commit \| commitdiff \| tree
2020-03-20	Andrew Reynolds	Handle failures for sygus QE preprocess (#4072)	commit \| commitdiff \| tree
2020-03-20	Andrew Reynolds	Parse error for SyGuS version 1.0 vs 2.0 (#4057)	commit \| commitdiff \| tree
2020-03-20	Andrew Reynolds	Make handling of illegal internal representatives in...	commit \| commitdiff \| tree
2020-03-20	Andrew Reynolds	Refactor enumerator for strings (#4014)	commit \| commitdiff \| tree
2020-03-19	Andrew Reynolds	Fix regression output related to sygus+bv-div-zero...	commit \| commitdiff \| tree
2020-03-19	Andrew Reynolds	SyGuS must use total bitvector division (#4119)	commit \| commitdiff \| tree
2020-03-19	Andrew Reynolds	Remove spurious assertion (#4117)	commit \| commitdiff \| tree
2020-03-19	Andrew Reynolds	Explicitly handle isFinite for rounding modes (#4115)	commit \| commitdiff \| tree
2020-03-19	Andrew Reynolds	Always enable cbqi literal dependency (#4116)	commit \| commitdiff \| tree
2020-03-19	Andrew Reynolds	Fix issue with multiple infinities in CEGQI for LIRA...	commit \| commitdiff \| tree
2020-03-16	Andrew Reynolds	Handle cases in --sygus-rr where evaluation is not...	commit \| commitdiff \| tree
2020-03-13	Andrew Reynolds	Removing a few deprecated options (#4052)	commit \| commitdiff \| tree
2020-03-13	Andrew Reynolds	Remove regress for real to int (#4071)	commit \| commitdiff \| tree
2020-03-13	Andrew Reynolds	Generalize type rules for strings to sequences (#3987)	commit \| commitdiff \| tree
2020-03-13	Andrew Reynolds	Fix case of non-constant value for sygus sampling ...	commit \| commitdiff \| tree
2020-03-12	Andrew Reynolds	Add options for nec regression (#4056)	commit \| commitdiff \| tree
2020-03-12	Andrew Reynolds	Convert most instances of dataypes in parsers to the...	commit \| commitdiff \| tree
2020-03-12	Andrew Reynolds	Do not allow quantifiers over real variables in real...	commit \| commitdiff \| tree
2020-03-12	Andrew Reynolds	Remove local theory extension option (#4048)	commit \| commitdiff \| tree
2020-03-12	Andrew Reynolds	Do not make models for quantified function variables...	commit \| commitdiff \| tree
2020-03-12	Andrew Reynolds	Ensure legal candidate equalities when using relational...	commit \| commitdiff \| tree
2020-03-12	Andrew Reynolds	Fix double notify in equality engine (#4036)	commit \| commitdiff \| tree
2020-03-12	Andrew Reynolds	Simplifications to the Datatypes API (#4040)	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Do not enable some SMT-COMP specific options by default...	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Guard against null relevancy condition in SyGuS (#4033)	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Add missing datatype functions to new API (#3930)	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Switch to Nodes for conjecture generator (#4026)	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Remove experimental symmetry breaker (#4005)	commit \| commitdiff \| tree
next

RSS Atom