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

2020-04-10	Andrew Reynolds	Towards proper use of resource managers (#4233)	commit \| commitdiff \| tree
2020-04-09	Mathias Preiner	CI: Add a step to list dependencies. (#4255)	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	mudathirmahgoub	Added CHOOSE operator for sets (#4211)	commit \| commitdiff \| tree
2020-04-08	Andres Noetzli	Perform theory widening eagerly (#4044)	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-06	Andres Noetzli	Refactor disequality processing in string solver (...	commit \| commitdiff \| tree
2020-04-06	Aina Niemetz	New C++ API: Rename Solver::mkTermInternal. (#4217)	commit \| commitdiff \| tree
2020-04-05	Andrew Reynolds	Add missing stat for lemmas based on inferences (#4214)	commit \| commitdiff \| tree
2020-04-05	Andres Noetzli	Add safe_print() support for Kind enum (#4213)	commit \| commitdiff \| tree
2020-04-05	Andrew Reynolds	Type-independent preregistration of empty word (#4205)	commit \| commitdiff \| tree
2020-04-04	Aina Niemetz	New C++ API: Remove Op::getSort(). (#4208)	commit \| commitdiff \| tree
2020-04-03	Andres Noetzli	Update theory rewriter ownership, add stats to strings...	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	Andres Noetzli	Remove undocumented/uncommon aliases (#4177)	commit \| commitdiff \| tree
2020-04-02	Andrew Reynolds	Introduce enums for all string inferences, excluding...	commit \| commitdiff \| tree
2020-04-02	Andres Noetzli	Initialize theory rewriters in theories (#4197)	commit \| commitdiff \| tree
2020-04-01	Andrew Reynolds	Support char smt-lib syntax (#4188)	commit \| commitdiff \| tree
2020-04-01	Mathias Preiner	Fix install for ANTLR contrib script and CI dependency...	commit \| commitdiff \| tree
2020-04-01	Aina Niemetz	Rename checkValid/query to checkEntailed. (#4191)	commit \| commitdiff \| tree
2020-03-31	Mathias Preiner	Switch to GitHub actions for CI (#4190) Switch to GitHub actions for CI (#4190) Enable CI with GitHub actions, add macOS builds and...	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	Mathias Preiner	Add coverage badge. (#4187)	commit \| commitdiff \| tree
2020-03-30	Andrew Reynolds	Fix arguments to print callback (#4171)	commit \| commitdiff \| tree
2020-03-30	mudathirmahgoub	Frontend support for the choice operator (#4175)	commit \| commitdiff \| tree
2020-03-29	Andrew Reynolds	Enumeration for String rewrites (#4173)	commit \| commitdiff \| tree
2020-03-28	Abdalrhman Mohamed	Change is-cons to (_ is cons) in Sygus benchmarks....	commit \| commitdiff \| tree
2020-03-28	Abdalrhman Mohamed	Convert the last few Sygus benchmarks to V2. (#4172)	commit \| commitdiff \| tree
2020-03-28	Abdalrhman Mohamed	Stop printing datatype declaration for Sygus V1 grammar...	commit \| commitdiff \| tree
2020-03-28	Alex Ozdemir	Node traversal iterator (#3845)	commit \| commitdiff \| tree
2020-03-28	Andrew Reynolds	Split transcendental solver to its own file (#4156) ...43099566+ahmed-irfan@users.noreply.github.com>	commit \| commitdiff \| tree
2020-03-27	Andres Noetzli	Fix issues with unsat cores and reset-assertions (...	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... ...check (as it should): https://github.com/CVC4/CVC4/blob/master/src... ...update the regression https://github.com/CVC4/CVC4/blob/master/test...	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	Amalee	Added unit-cube-like test for branch and bound (#3922) ...43099566+ahmed-irfan@users.noreply.github.com>	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	Andres Noetzli	Support async-signal-safe printing of inferences (...	commit \| commitdiff \| tree
2020-03-25	Ahmed Irfan	bv2int : linear mult opt (#4142)	commit \| commitdiff \| tree
2020-03-25	Andrew Reynolds	Generalize more uses of string-specific functions...	commit \| commitdiff \| tree
2020-03-24	yoni206	Int2BV fail on demand (#4079)	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-23	Andres Noetzli	Collect statistics about normal form inferences (#4127)	commit \| commitdiff \| tree
2020-03-22	Andrew Reynolds	Sort inference does not handle APPLY_UF when higher...	commit \| commitdiff \| tree
2020-03-22	Abdalrhman Mohamed	Convert V1 Sygus files to V2. (#4136)	commit \| commitdiff \| tree
2020-03-21	Andres Noetzli	Simplify heuristic in `processNEqc` (#4129)	commit \| commitdiff \| tree
2020-03-21	Andres Noetzli	Don't run bv_nat parse test with competition build...	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	yoni206	Bv2int fail on demand	commit \| commitdiff \| tree
2020-03-19	Andres Noetzli	Only apply testConstStringInRegExp to const regexp...	commit \| commitdiff \| tree
2020-03-19	Andrew Reynolds	SyGuS must use total bitvector division (#4119)	commit \| commitdiff \| tree
2020-03-19	Andres Noetzli	Only allow bv2nat/int2bv with BV and integer logic...	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-18	Alex Ozdemir	Move node visitor class from smt_util/ to expr/ (#4110)	commit \| commitdiff \| tree
2020-03-17	Aina Niemetz	SmtEngine: Convert members owned by SmtEngine to unique...	commit \| commitdiff \| tree
2020-03-16	Aina Niemetz	DecisionEngine: Use single unique pointer for ITE strategy...	commit \| commitdiff \| tree
2020-03-16	Aina Niemetz	Issue 4077: Add unit test to reproduce issue. (#4107)	commit \| commitdiff \| tree
2020-03-16	Andres Noetzli	Create master equality engine at context level 0 (...	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
next

RSS Atom