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

2020-05-26	Andrew Reynolds	(proof-new) Updates to strings skolem cache. (#4524)	commit \| commitdiff \| tree
2020-05-26	Mathias Preiner	Update to CaDiCaL version 1.2.1. (#4530)	commit \| commitdiff \| tree
2020-05-24	Andres Noetzli	[SMT-COMP] Redirect non-answers to /dev/null (#4528)	commit \| commitdiff \| tree
2020-05-23	mudathirmahgoub	remove unused field d_emp_exp in TheorySetsPrivate...	commit \| commitdiff \| tree
2020-05-23	Andrew Reynolds	Add the sequence datatype (#4153)	commit \| commitdiff \| tree
2020-05-23	Abdalrhman Mohamed	Fix mistakes in sygus API comments. (#4520)	commit \| commitdiff \| tree
2020-05-23	Andrew Reynolds	Refactor operator elimination in arithmetic (#4519)	commit \| commitdiff \| tree
2020-05-22	Andres Noetzli	[SMT-COMP] Use tear-down-incremental for arithmetic...	commit \| commitdiff \| tree
2020-05-22	Aina Niemetz	CaDiCaL: Clean up initialization on creation. (#4516)	commit \| commitdiff \| tree
2020-05-22	Andrew Reynolds	(proof-new) Add rewrite corresponding to regular expression...	commit \| commitdiff \| tree
2020-05-22	Aina Niemetz	Cryptominisat: Clean up initialization on creation...	commit \| commitdiff \| tree
2020-05-22	Aina Niemetz	Add support for SAT solver Kissat. (#4514)	commit \| commitdiff \| tree
2020-05-22	Andrew Reynolds	(proof-new) Proof node to SExpr utility. (#4512)	commit \| commitdiff \| tree
2020-05-22	Andrew Reynolds	Update string kind names in new API (#4509)	commit \| commitdiff \| tree
2020-05-22	Andrew Reynolds	(proof-new) Minor update to strings solver state (...	commit \| commitdiff \| tree
2020-05-21	Andrew Reynolds	Disable re-elim by default (#4508)	commit \| commitdiff \| tree
2020-05-21	Abdalrhman Mohamed	Make Grammar reusable. (#4506)	commit \| commitdiff \| tree
2020-05-21	Andrew Reynolds	Throw logic exception for equality between regular...	commit \| commitdiff \| tree
2020-05-21	Andrew Reynolds	Fix missing check for cardinality one in unconstrained...	commit \| commitdiff \| tree
2020-05-20	Andrew Reynolds	Normal form equality conflicts and uniqueness check...	commit \| commitdiff \| tree
2020-05-20	Andrew Reynolds	Add proof skolem cache (#4485)	commit \| commitdiff \| tree
2020-05-20	Andrew Reynolds	Fix parametric datatype instantiation (#4493)	commit \| commitdiff \| tree
2020-05-20	Aina Niemetz	CegqiBv: Clean up after renaming options. (#4487)	commit \| commitdiff \| tree
2020-05-20	Andrew Reynolds	Use debug-check-model to enable internal debugging...	commit \| commitdiff \| tree
2020-05-20	Abdalrhman Mohamed	Add a simple script to convert sygus v1 files to v2...	commit \| commitdiff \| tree
2020-05-20	Andrew Reynolds	Do not eliminate variables that are equal to unevaluatable...	commit \| commitdiff \| tree
2020-05-20	Andrew Reynolds	Fix cached free variable identifiers in sygus term...	commit \| commitdiff \| tree
2020-05-19	mudathirmahgoub	Renamed operator CHOICE to WITNESS (#4207)	commit \| commitdiff \| tree
2020-05-19	Andrew Reynolds	Use fresh variables when miniscoping (#4296)	commit \| commitdiff \| tree
2020-05-19	Andrew Reynolds	Update enum and option names for sygus languages (...	commit \| commitdiff \| tree
2020-05-19	Andres Noetzli	Make SolveEq and PlusCombineLikeTerms idempotent (...	commit \| commitdiff \| tree
2020-05-12	Andrew Reynolds	Do not enable unconstrained simplification if arithmetic...	commit \| commitdiff \| tree
2020-05-06	Andres Noetzli	Update run scripts for SMT-COMP 2020 (#4454)	commit \| commitdiff \| tree
2020-05-05	Andrew Reynolds	Always introduce fresh variable for unconstrained APPLY_UF...	commit \| commitdiff \| tree
2020-05-05	Aina Niemetz	Update copyright year and AUTHORS/THANKS files. (#4468)	commit \| commitdiff \| tree
2020-05-02	Aina Niemetz	SMT-COMP 2020: Enable --fp-exp for new FP logics. ...	commit \| commitdiff \| tree
2020-05-02	Andrew Reynolds	Move slow regression to regress3 (#4430)	commit \| commitdiff \| tree
2020-05-01	Andrew Reynolds	Fix regression (#4424)	commit \| commitdiff \| tree
2020-04-30	Andrew Reynolds	Remove skolem share involving pre_first_ctn. (#4423)	commit \| commitdiff \| tree
2020-04-30	Andrew Reynolds	Do not mark congruent terms are reduced (#4419)	commit \| commitdiff \| tree
2020-04-29	Aina Niemetz	SMT-COMP 2020: Fix scripts to use --no-type-checking...	commit \| commitdiff \| tree
2020-04-29	Andrew Reynolds	Avoid circular dependencies for justifying reductions...	commit \| commitdiff \| tree
2020-04-29	Andrew Reynolds	Fix strings 2.6 regression (#4413)	commit \| commitdiff \| tree
2020-04-28	Andres Noetzli	Register lower bound for str.to_int (#4408)	commit \| commitdiff \| tree
2020-04-28	Andrew Reynolds	Updates to SMT COMP script for 20 minute timeout (...	commit \| commitdiff \| tree
2020-04-28	Haniel Barbosa	update Haniel's affiliation (#4404)	commit \| commitdiff \| tree
2020-04-28	Aina Niemetz	contrib/get-gmp: Rename and update install instructions...	commit \| commitdiff \| tree
2020-04-28	Andrew Reynolds	Support the SMT-LIB Unicode string standard by default...	commit \| commitdiff \| tree
2020-04-28	Andrew Reynolds	Update cardinality in strings to unicode standard ...	commit \| commitdiff \| tree
2020-04-27	Andrew Reynolds	Fix sygus unit (#4371)	commit \| commitdiff \| tree
2020-04-27	Mathias Preiner	Fix examples instructions in INSTALL.md. (#4397)	commit \| commitdiff \| tree
2020-04-26	Andrew Reynolds	Fix sets cardinality cycle rule (#4392) https://github.com/CVC4/CVC4/blob/master/src...	commit \| commitdiff \| tree
2020-04-23	Andres Noetzli	Introduce best content heuristic for strings (#4382)	commit \| commitdiff \| tree
2020-04-23	Andres Noetzli	Strings: Register skolems before sending lemma (#4381)	commit \| commitdiff \| tree
2020-04-22	Andrew Reynolds	Ensure disequality splits are processed as lemmas ...	commit \| commitdiff \| tree
2020-04-22	Andrew Reynolds	Allow eager bitblasting with solve bv as int in QF_NIA...	commit \| commitdiff \| tree
2020-04-22	Abdalrhman Mohamed	Convert V2.5 SMT regressions to V2.6. (#4319)	commit \| commitdiff \| tree
2020-04-22	Andres Noetzli	Reinstantiate support for conjunctions in facts (#4377)	commit \| commitdiff \| tree
2020-04-21	Andrew Reynolds	Update to sygus version 2 (#4372)	commit \| commitdiff \| tree
2020-04-21	Andrew Reynolds	Fix for parse options related to binary name (#4368) https://github.com/CVC4/CVC4/blob/master/test...	commit \| commitdiff \| tree
2020-04-21	Abdalrhman Mohamed	Introduce a public interface for Sygus commands. (...	commit \| commitdiff \| tree
2020-04-21	Andrew Reynolds	Make option names related to CEGQI consistent (#4316)	commit \| commitdiff \| tree
2020-04-20	Andrew Reynolds	Refactor inference manager in strings to be amenable...	commit \| commitdiff \| tree
2020-04-20	Andrew Reynolds	Add SCOPE proof rule (#4332)	commit \| commitdiff \| tree
2020-04-19	Andrew Reynolds	Disable unsat cores on nec regression (#4330)	commit \| commitdiff \| tree
2020-04-18	Andrew Reynolds	Track inference id for pending facts in strings (#4331)	commit \| commitdiff \| tree
2020-04-18	Haniel Barbosa	Improving EqProof printing (#4329)	commit \| commitdiff \| tree
2020-04-17	Andrew Reynolds	Add (context-dependent) Proof (#4323)	commit \| commitdiff \| tree
2020-04-17	Mathias Preiner	antlr: Use relative path in ANTLR script. (#4324)	commit \| commitdiff \| tree
2020-04-17	Mathias Preiner	SyGuS instantiation quantifiers module (#3910)	commit \| commitdiff \| tree
2020-04-16	Andrew Reynolds	Add ProofNodeManager and ProofChecker (#4317)	commit \| commitdiff \| tree
2020-04-16	Andrew Reynolds	Eliminate remaining references to parent TheoryStrings...	commit \| commitdiff \| tree
2020-04-15	Andrew Reynolds	Add ProofNode data structure (#4311)	commit \| commitdiff \| tree
2020-04-15	Andrew Reynolds	Move regular expression inclusion test to RegExpEntail...	commit \| commitdiff \| tree
2020-04-15	Andrew Reynolds	Change option names --default-dag-thresh and --default...	commit \| commitdiff \| tree
2020-04-15	Andrew Reynolds	Split TermRegistry object from TheoryStrings (#4312)	commit \| commitdiff \| tree
2020-04-15	Andrew Reynolds	Do not mark string extended functions as eliminated...	commit \| commitdiff \| tree
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	Alex Ozdemir	Add skip predicate to node traversal. (#4222)	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
next

RSS Atom