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

2017-11-30	Andrew Reynolds	Fixes for issue 1404 (#1409)	commit \| commitdiff \| tree
2017-11-30	Andrew Reynolds	Remove remaining references to QuantArith (#1408)	commit \| commitdiff \| tree
2017-11-30	Andrew Reynolds	Minor improvements and changes to defaults for cbqi...	commit \| commitdiff \| tree
2017-11-29	Andrew Reynolds	Improve caching in term formula removal (#1398)	commit \| commitdiff \| tree
2017-11-29	Andrew Reynolds	Improve the rewriter for SINE. (#1221)	commit \| commitdiff \| tree
2017-11-28	Andrew Reynolds	Improve rewrite for string substr (#1337)	commit \| commitdiff \| tree
2017-11-28	Andrew Reynolds	Improve trigger filter instances (#1402)	commit \| commitdiff \| tree
2017-11-28	Andrew Reynolds	Fix models for --solve-real-as-int. (#1371)	commit \| commitdiff \| tree
2017-11-25	Andrew Reynolds	Fixes for higher-order (#1405)	commit \| commitdiff \| tree
2017-11-25	Andrew Reynolds	(Refactor) Instantiate utility (#1387)	commit \| commitdiff \| tree
2017-11-24	Andrew Reynolds	Implement tangent and secant planes for transcendental...	commit \| commitdiff \| tree
2017-11-24	Andrew Reynolds	Ho parsing and regressions (#1350)	commit \| commitdiff \| tree
2017-11-22	Andrew Reynolds	Sygus Lambda Grammars (#1390)	commit \| commitdiff \| tree
2017-11-22	Andrew Reynolds	Transcendental tangent planes utilities (#1288)	commit \| commitdiff \| tree
2017-11-21	Andrew Reynolds	Cegqi bv remove extract terms preprocess pass (#1376)	commit \| commitdiff \| tree
2017-11-19	Andrew Reynolds	Ho instantiation (#1204)	commit \| commitdiff \| tree
2017-11-17	Andrew Reynolds	(Refactor) Document and clean single invocation partition...	commit \| commitdiff \| tree
2017-11-16	Andrew Reynolds	(Refactor) Arithmetic monomial sum (#1381)	commit \| commitdiff \| tree
2017-11-15	Andrew Reynolds	Sygus print callbacks (#1348)	commit \| commitdiff \| tree
2017-11-15	Andrew Reynolds	Reenable some regressions, minor. (#1369)	commit \| commitdiff \| tree
2017-11-15	Andrew Reynolds	Make QEffort an enum (#1366)	commit \| commitdiff \| tree
2017-11-14	Andrew Reynolds	(Refactor) Split sygus term db (#1335)	commit \| commitdiff \| tree
2017-11-14	Andrew Reynolds	Clean Ceg Instantiators (#1365)	commit \| commitdiff \| tree
2017-11-14	Andrew Reynolds	(Refactor) Decouple rep set iterator and quantifiers...	commit \| commitdiff \| tree
2017-11-13	Andrew Reynolds	Disable sygus qe preprocessing by default (#1353)	commit \| commitdiff \| tree
2017-11-13	Andrew Reynolds	Implement enumerator for functions. (#1243)	commit \| commitdiff \| tree
2017-11-13	Andrew Reynolds	Argument Relevance for Synthesis Conjectures (#1311)	commit \| commitdiff \| tree
2017-11-10	Andrew Reynolds	(Documentation-only) datatype.h (#1346)	commit \| commitdiff \| tree
2017-11-10	Andrew Reynolds	Printing for higher-order (#1347)	commit \| commitdiff \| tree
2017-11-09	Andrew Reynolds	Higher-order prep (#1338)	commit \| commitdiff \| tree
2017-11-09	Andrew Reynolds	Decouple sygus term database and term database. (...	commit \| commitdiff \| tree
2017-11-07	Andrew Reynolds	Guard relevant domain computation properly, minor....	commit \| commitdiff \| tree
2017-11-07	Andrew Reynolds	Allow FORALL in quantifier elimination command (#1322)	commit \| commitdiff \| tree
2017-11-07	Andrew Reynolds	Updates to interface for Sygus grammar construction...	commit \| commitdiff \| tree
2017-11-06	Andrew Reynolds	Unrecurisify rewrite solve assertion for cbqi bv (...	commit \| commitdiff \| tree
2017-11-06	Andrew Reynolds	Improve rewriting for string contains part 2 (#1300)	commit \| commitdiff \| tree
2017-11-05	Andrew Reynolds	Make higher-order a flag in logic info. (#1318)	commit \| commitdiff \| tree
2017-11-04	Andrew Reynolds	Suppport SAT logic (#1310)	commit \| commitdiff \| tree
2017-11-04	Andrew Reynolds	Fix bv help message. (#1315)	commit \| commitdiff \| tree
2017-11-03	Andrew Reynolds	Sygus clean main (#1297)	commit \| commitdiff \| tree
2017-11-02	Andrew Reynolds	(Move-only) Split quant util (#1306)	commit \| commitdiff \| tree
2017-11-01	Andrew Reynolds	(Refactor) Split term util (#1303)	commit \| commitdiff \| tree
2017-11-01	Andrew Reynolds	CBQI BV choice expressions (#1296)	commit \| commitdiff \| tree
2017-11-01	Andrew Reynolds	(Move-only) Refactor and document theory model part...	commit \| commitdiff \| tree
2017-10-31	Andrew Reynolds	Remove include (#1298)	commit \| commitdiff \| tree
2017-10-28	Andrew Reynolds	(Move only) Move enumerative instantiation strategy...	commit \| commitdiff \| tree
2017-10-28	Andrew Reynolds	Sygus process conjecture (#1286)	commit \| commitdiff \| tree
2017-10-28	Andrew Reynolds	Document term db (#1220)	commit \| commitdiff \| tree
2017-10-28	Andrew Reynolds	Improve strings rewriter for contains (#1207)	commit \| commitdiff \| tree
2017-10-28	Andrew Reynolds	Document quant arith (#1271)	commit \| commitdiff \| tree
2017-10-27	Andrew Reynolds	Cbqi multiple instantiation (#1289)	commit \| commitdiff \| tree
2017-10-27	Andrew Reynolds	Refactor theory model (#1236)	commit \| commitdiff \| tree
2017-10-27	Andrew Reynolds	Implement Hilbert choice operator (#1291)	commit \| commitdiff \| tree
2017-10-26	Andrew Reynolds	Op overload no fun variant (#1285)	commit \| commitdiff \| tree
2017-10-25	Andrew Reynolds	Cbqi bv ineq mode (#1273)	commit \| commitdiff \| tree
2017-10-24	Andrew Reynolds	Removing deprecated file. (#1270)	commit \| commitdiff \| tree
2017-10-23	Andrew Reynolds	Document sygus programming-by-examples utility (#1260)	commit \| commitdiff \| tree
2017-10-20	Andrew Reynolds	SyGuS term size limit (#1262)	commit \| commitdiff \| tree
2017-10-20	Andrew Reynolds	Make Sygus conjectures higher-order (#1244)	commit \| commitdiff \| tree
2017-10-18	Andrew Reynolds	Tptp unsat cores (#1228)	commit \| commitdiff \| tree
2017-10-18	Andrew Reynolds	Strings API escape sequences (#1245)	commit \| commitdiff \| tree
2017-10-17	Andrew Reynolds	Sygus enumerators to conjecture (#1237)	commit \| commitdiff \| tree
2017-10-13	Andrew Reynolds	CBQI BV quick heuristics (#1239)	commit \| commitdiff \| tree
2017-10-12	Andrew Reynolds	Initial support for solving bit-vector inequalities...	commit \| commitdiff \| tree
2017-10-12	Andrew Reynolds	Sygus logics (#1226)	commit \| commitdiff \| tree
2017-10-11	Andrew Reynolds	Ho Lambda Lifting (#1116)	commit \| commitdiff \| tree
2017-10-11	Andrew Reynolds	Adds infrastructure for a rewriting pass in BvInstantiator...	commit \| commitdiff \| tree
2017-10-11	Andrew Reynolds	Move unsat core names to smt engine (#1192)	commit \| commitdiff \| tree
2017-10-11	Andrew Reynolds	Ho node manager types (#1203)	commit \| commitdiff \| tree
2017-10-10	Andrew Reynolds	Split term database (#1206)	commit \| commitdiff \| tree
2017-10-05	Andrew Reynolds	Minor change to how SyGus commands are translated to...	commit \| commitdiff \| tree
2017-10-05	Andrew Reynolds	Ho model (#1120)	commit \| commitdiff \| tree
2017-10-04	Andrew Reynolds	Ho quant util (#1119)	commit \| commitdiff \| tree
2017-10-04	Andrew Reynolds	Add regression from #50 regarding "as" parsing in smt2...	commit \| commitdiff \| tree
2017-10-03	Andrew Reynolds	Move sygus grammar utilities to separate file. (#1184)	commit \| commitdiff \| tree
2017-10-03	Andrew Reynolds	Op overload parser (#1162)	commit \| commitdiff \| tree
2017-10-01	Andrew Reynolds	Refactor check function in last call effort of non...	commit \| commitdiff \| tree
2017-09-30	Andrew Reynolds	SyGuS streaming solution mode (#1131)	commit \| commitdiff \| tree
2017-09-29	Andrew Reynolds	Simplify representation of inversion Skolems for bv...	commit \| commitdiff \| tree
2017-09-29	Andrew Reynolds	Initial working version of BV word-level instantiation...	commit \| commitdiff \| tree
2017-09-29	Andrew Reynolds	Update symbol table to support operator overloading...	commit \| commitdiff \| tree
2017-09-28	Andrew Reynolds	Cegqi refactor prep bv (#1155)	commit \| commitdiff \| tree
2017-09-28	Andrew Reynolds	Improve finite model finding for recursive predicates...	commit \| commitdiff \| tree
2017-09-27	Andrew Reynolds	Minor fixes for partial quantifier elimination. (#1147)	commit \| commitdiff \| tree
2017-09-27	Andrew Reynolds	Add quantifiers API example, fixes #879 (#1146)	commit \| commitdiff \| tree
2017-09-26	Andrew Reynolds	Cegqi refactor substitutions (#1129)	commit \| commitdiff \| tree
2017-09-25	Andrew Reynolds	Fix bug related to sort inference + subtypes. (#1125)	commit \| commitdiff \| tree
2017-09-21	Andrew Reynolds	Sygus inv templ refactor (#1110)	commit \| commitdiff \| tree
2017-09-21	Andrew Reynolds	Extend quantifier-free UF solver to higher-order. This...	commit \| commitdiff \| tree
2017-09-19	Andrew Reynolds	Refactor cegqi instantiation infrastructure so that...	commit \| commitdiff \| tree
2017-09-19	Andrew Reynolds	Fix issue #1105 involving string to int (#1112)	commit \| commitdiff \| tree
2017-09-14	Andrew Reynolds	Remove unhandled subtypes (#1098)	commit \| commitdiff \| tree
2017-09-14	Andrew Reynolds	Add new kinds required for higher-order. (#1083)	commit \| commitdiff \| tree
2017-09-14	Andrew Reynolds	Add isConst check for lambda expressions. (#1084)	commit \| commitdiff \| tree
2017-09-13	Andrew Reynolds	Modify equality engine to allow operators to be marked...	commit \| commitdiff \| tree
2017-09-12	Andrew Reynolds	Initial infrastructure for BV instantiation via word...	commit \| commitdiff \| tree
2017-09-10	Andrew Reynolds	Ensure that expand definitions is called on all non...	commit \| commitdiff \| tree
2017-09-07	Andrew Reynolds	Properly handle user cardinality constraints for uf...	commit \| commitdiff \| tree
2017-09-05	Andrew Reynolds	Remove support for conversions between uint32/uint16...	commit \| commitdiff \| tree
2017-08-31	Andrew Reynolds	Answer unknown when uf-ss=no-minimal is combined with...	commit \| commitdiff \| tree
next

RSS Atom