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

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
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... ...underlying datatype. (See https://github.com/abdoo8080/CVC4/tree/sygus...	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	Aina Niemetz	New C++ API: Remove support for (reset). (#4037)	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	Aina Niemetz	Hide options for and related to the BV abstraction...	commit \| commitdiff \| tree
2020-03-12	Andrew Reynolds	Simplifications to the Datatypes API (#4040)	commit \| commitdiff \| tree
2020-03-12	makaimann	Add automatic Cython binding installation (#3933)	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	Andres Noetzli	reset-assertions: Update TheoryEngine's PropEngine...	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Remove experimental symmetry breaker (#4005)	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Fix non-parametrized operators in subgoal generation...	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Remove partial instantiation for local theory extensions...	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Fix (#4017)	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Fix duplicate variable issue in sygus-qe-preproc (...	commit \| commitdiff \| tree
2020-03-11	Andres Noetzli	Introduce tables in the rewriter (#3742)	commit \| commitdiff \| tree
2020-03-11	Andres Noetzli	Set assertion in `CnfStream::ensureLiteral()` (#3927) (https://github.com/CVC4/CVC4/blob/ba6ade0fc3f4cd339885...	commit \| commitdiff \| tree
2020-03-11	Aina Niemetz	bv-gauss-elim: Fix handling of inconsistent case. ...	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Fix real to int for parameterized kinds (#4016)	commit \| commitdiff \| tree
2020-03-10	Andrew Reynolds	Fix options for regression: --sort-inference is incompatible...	commit \| commitdiff \| tree
2020-03-10	Andrew Reynolds	Fix sort inference for top-level Boolean variables...	commit \| commitdiff \| tree
2020-03-10	Aina Niemetz	Fix issue with reset-assertions. (#3988)	commit \| commitdiff \| tree
next

RSS Atom