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

2018-08-17	Mathias Preiner	Refactor eager atoms preprocessing pass. (#2318)	commit \| commitdiff \| tree
2018-08-17	Caleb Donovick	Make quantifiers-preprocess preprocessing pass (#2322)	commit \| commitdiff \| tree
2018-08-16	Tim King	Switching an Assert to a CVC4_CHECK to test if it resolves...	commit \| commitdiff \| tree
2018-08-15	Mathias Preiner	Add contrib/get-gmp script. (#2292)	commit \| commitdiff \| tree
2018-08-08	Andrew Reynolds	Simplify and improve the sygus parser (#2266)	commit \| commitdiff \| tree
2018-08-07	Andrew Reynolds	Remove support for Enum sygus syntax. (#2264)	commit \| commitdiff \| tree
2018-08-06	Andrew Reynolds	Fixes for sygus inference (#2238)	commit \| commitdiff \| tree
2018-08-02	Andrew Reynolds	Make strings robust to regular expression variables...	commit \| commitdiff \| tree
2018-08-02	Andrew Reynolds	Improvements and fixes in cegqi arithmetic (#2247)	commit \| commitdiff \| tree
2018-08-01	Andrew Reynolds	Fix issues with bv2nat (#2219)	commit \| commitdiff \| tree
2018-08-01	Andrew Reynolds	Fix assertion in conjecture generator (#2246)	commit \| commitdiff \| tree
2018-08-01	Andrew Reynolds	Make conjecture generator's uf term enumeration safer...	commit \| commitdiff \| tree
2018-08-01	Andrew Reynolds	Make candidate rewrite match filtering handle polymorphic...	commit \| commitdiff \| tree
2018-07-27	Mathias Preiner	Make Python a required CVC4 dependency. (#2227)	commit \| commitdiff \| tree
2018-07-27	Andrew Reynolds	Fix for candidate rewrite rule filtering. (#2220)	commit \| commitdiff \| tree
2018-07-27	Andrew Reynolds	Make check-synth robust for assertions that are not...	commit \| commitdiff \| tree
2018-07-27	Andrew Reynolds	Fix Node::hasFreeVar for function variables (#2216)	commit \| commitdiff \| tree
2018-07-26	Aina Niemetz	New C++ API: Enable examples. (#2222)	commit \| commitdiff \| tree
2018-07-26	Andrew Reynolds	Fix rewriter for lambda (#2211)	commit \| commitdiff \| tree
2018-07-26	ayveejay	Avoid explicit dependency on Python 3 (#2195)	commit \| commitdiff \| tree
2018-07-25	Tim King	Changing ArithIteUtils to use CDInsertHashMap. (#2206)	commit \| commitdiff \| tree
2018-07-25	Tim King	Removing support for CDHashMap::iterator's postfix...	commit \| commitdiff \| tree
2018-07-22	Andrew Reynolds	sygusComp2018: Improvements to CEGIS loop (#2187)	commit \| commitdiff \| tree
2018-07-11	Caleb Donovick	Move rewrite to pass (#2128)	commit \| commitdiff \| tree
2018-07-07	Andrew Reynolds	sygusComp2018: improve extended rewriter for Bool...	commit \| commitdiff \| tree
2018-07-06	Martin	Feature/fp rewrite improvement (#2154)	commit \| commitdiff \| tree
2018-07-06	Aina Niemetz	New C++ API: Implementation of Solver class: Term handling...	commit \| commitdiff \| tree
2018-07-06	Andrew Reynolds	sygusComp2018: simplify beta reduction in uf rewriter...	commit \| commitdiff \| tree
2018-07-05	Andrew Reynolds	Make string length lemmas more robust to rewriting...	commit \| commitdiff \| tree
2018-07-05	Andrew Reynolds	Minor changes to sygus-rr utilities to support floating...	commit \| commitdiff \| tree
2018-07-04	Andrew Reynolds	Fix fmf-fun for non-equality function definitions ...	commit \| commitdiff \| tree
2018-07-02	Caleb Donovick	Add missing include (#2127)	commit \| commitdiff \| tree
2018-06-28	Andrew Reynolds	Remove comment about model value hack (#2118)	commit \| commitdiff \| tree
2018-06-26	Andrew Reynolds	sygusComp2018: add scripts. (#2103)	commit \| commitdiff \| tree
2018-06-26	Andrew Reynolds	Disable uf symmetry breaker in incremental mode (...	commit \| commitdiff \| tree
2018-06-12	Andrew Reynolds	Fix strip constant endpoint for ITOS in strings rewriter...	commit \| commitdiff \| tree
2018-06-11	Andrew Reynolds	Fix equality conflicts reported by FP (#2064)	commit \| commitdiff \| tree
2018-06-04	Andrew Reynolds	Enable cegqi (with model values) for floating point...	commit \| commitdiff \| tree
2018-06-02	Andrew Reynolds	Fix assertion involving unassigned Boolean eqc in...	commit \| commitdiff \| tree
2018-06-02	Mathias Preiner	Fix BV-abstraction check to consider SKOLEM. (#2042)	commit \| commitdiff \| tree
2018-06-02	Andrew Reynolds	Fix preinitialization pass for finite model finding...	commit \| commitdiff \| tree
2018-06-01	Andrew Reynolds	Use monomial sum utility to solve for quantifiers...	commit \| commitdiff \| tree
2018-06-01	Andrew Reynolds	Reduce before preregister. (#2025)	commit \| commitdiff \| tree
2018-05-31	Mathias Preiner	Fix bv-abstraction check for AND with non bit-vector...	commit \| commitdiff \| tree
2018-05-30	Aina Niemetz	Ignore license key in set-info command. (#2021)	commit \| commitdiff \| tree
2018-05-30	Andrew Reynolds	Fixes for quantifiers + incremental (#2009)	commit \| commitdiff \| tree
2018-05-30	Mathias Preiner	Normalize negated bit-vector terms over equalities...	commit \| commitdiff \| tree
2018-05-30	Andrew Reynolds	Draft run script for strings smt comp 2018. (#2016)	commit \| commitdiff \| tree
2018-05-29	Andrew Reynolds	Disable minisat elimination when nonlinear is enabled...	commit \| commitdiff \| tree
2018-05-27	Andrew Reynolds	Fix cegqi assertions for quantified non-linear cases...	commit \| commitdiff \| tree
2018-05-25	Mathias Preiner	Add QF_BV configuration for SMTCOMP'18. (#1981)	commit \| commitdiff \| tree
2018-05-24	Andrew Reynolds	Fix nl regression for unsat cores. (#1973)	commit \| commitdiff \| tree
2018-05-21	Andrew Reynolds	Improvements in parsing and printing related to mixed...	commit \| commitdiff \| tree
2018-05-21	makaimann	Handle IMPLIES in bool-to-bv and test it in regress0...	commit \| commitdiff \| tree
2018-05-21	Andrew Reynolds	Refactor sygus eval unfold (#1946)	commit \| commitdiff \| tree
2018-05-21	Caleb Donovick	Fix file extension (#1919)	commit \| commitdiff \| tree
2018-05-05	Andrew Reynolds	Fix handling of TO_REAL in cvc printer (#1876)	commit \| commitdiff \| tree
2018-05-04	Andrew Reynolds	Do not print tuples. (#1874)	commit \| commitdiff \| tree
2018-05-04	Mathias Preiner	Refactor bv-intro-pow2 preprocessing pass. (#1851)	commit \| commitdiff \| tree
2018-05-04	Andrew Reynolds	Sets subtypes (#1095)	commit \| commitdiff \| tree
2018-05-03	Mathias Preiner	Fix redundant internalPush calls. (#1865)	commit \| commitdiff \| tree
2018-05-03	Andrew Reynolds	Fix cvc printer for nullary constructors (#1856)	commit \| commitdiff \| tree
2018-05-03	Andrew Reynolds	Initial support for string standard in smt lib 2.6...	commit \| commitdiff \| tree
2018-04-30	Andrew Reynolds	Remove subsort symmetry breaking (#1807)	commit \| commitdiff \| tree
2018-04-20	yoni206	Allow metadata lines in test files to have leading...	commit \| commitdiff \| tree
2018-04-15	Andrew Reynolds	Fix mk type const (#1776)	commit \| commitdiff \| tree
2018-04-04	Andrew Reynolds	Proper initialization and destruction of sygus unif...	commit \| commitdiff \| tree
2018-04-04	Andrew Reynolds	Option to turn arbitrary input into sygus (#1704)	commit \| commitdiff \| tree
2018-03-26	Andrew Reynolds	Check model only when sat (#1694)	commit \| commitdiff \| tree
2018-03-25	Andrew Reynolds	Cleanup various exit calls (#1692)	commit \| commitdiff \| tree
2018-03-25	Mathias Preiner	Remove doc/libcvc4.3 from options/Makefile.am. (#1696)	commit \| commitdiff \| tree
2018-03-20	Andrew Reynolds	Fix datatype dump regression. (#1672)	commit \| commitdiff \| tree
2018-02-10	Aina Niemetz	Remove mkNode from bv::utils (#1587)	commit \| commitdiff \| tree
2018-01-27	Tim King	Removing an unused variable. Resolves CID 1172257....	commit \| commitdiff \| tree
2018-01-27	Tim King	Removing structurally dead code. (#1540)	commit \| commitdiff \| tree
2018-01-14	Tim King	Removing throw specifiers from OptionsHandler. (#1510)	commit \| commitdiff \| tree
2018-01-10	Tim King	Cleaning up throw specifiers on Exception and subclasses...	commit \| commitdiff \| tree
2017-12-11	justinxu421	Add new infrastructure for preprocessing passes (#1053)	commit \| commitdiff \| tree
2017-12-01	Andres Noetzli	Fix build when Valgrind instrumentation enabled	commit \| commitdiff \| tree
2017-11-15	Tim King	Adding garbage collection for Proof objects. (#1294)	commit \| commitdiff \| tree
2017-11-04	Andrew Reynolds	Fix bv help message. (#1315)	commit \| commitdiff \| tree
2017-10-27	Tim King	Adds a macro to SWIG to ignore the override and final...	commit \| commitdiff \| tree
2017-10-26	Tim King	Removing throw specifiers from OutputChannel and subclasses...	commit \| commitdiff \| tree
2017-10-10	Martin	Add skeleton of the FP theory solver (#1130)	commit \| commitdiff \| tree
2017-10-05	Martin	Allow CDHashMaps for objects without default constructors...	commit \| commitdiff \| tree
2017-10-03	Martin	Add 5 FP kinds for partial to total fn conversion ...	commit \| commitdiff \| tree
2017-10-02	Tim King	Removing throw specifiers from SymbolTable::Implementation...	commit \| commitdiff \| tree
2017-10-02	Tim King	CID 1457268: Initializing CegConjecture::d_syntax_guided...	commit \| commitdiff \| tree
2017-09-29	Andres Noetzli	Add license information for GMP	commit \| commitdiff \| tree
2017-09-29	Andrew Reynolds	Update symbol table to support operator overloading...	commit \| commitdiff \| tree
2017-09-29	Mathias Preiner	Fix output of --show-config for readline. (#1159)	commit \| commitdiff \| tree
2017-09-27	Andrew Reynolds	Minor fixes for partial quantifier elimination. (#1147)	commit \| commitdiff \| tree
2017-09-27	Martin Brain	Fix type checking of to_real (#1127)	commit \| commitdiff \| tree
2017-09-27	Martin Brain	Improve FP rewriter: const folding, other (#1126)	commit \| commitdiff \| tree
2017-09-26	Tim King	Fixing CIDs 1172014 and 1172013: Initializing members...	commit \| commitdiff \| tree
2017-09-26	Tim King	Fixing Cid 1172009 (#1141)	commit \| commitdiff \| tree
2017-09-26	Tim King	Fixing CID 1172020: Initializing CDHashMap::iterator...	commit \| commitdiff \| tree
2017-09-26	Tim King	Fixing CID 1362903: Initializing d_bvp to nullptr....	commit \| commitdiff \| tree
2017-09-26	Tim King	CID 1362904: Initializing GetInstantiationsCommand...	commit \| commitdiff \| tree
2017-09-26	Tim King	Fixing CIDs 1172012 and 1172011: Initiallzing d_exprManager...	commit \| commitdiff \| tree
next

RSS Atom