projects / cvc5.git / search
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Track instantiation reasons in proofs (#6935)
2021-07-27 Andrew ReynoldsTrack instantiation reasons in proofs (#6935)
 commit | commitdiff | tree
2021-07-27 Andrew ReynoldsAdd basic LFSC utilities (#6879)
 commit | commitdiff | tree
2021-07-27 Andrew ReynoldsMove enum value generator to own file (#6941)
 commit | commitdiff | tree
2021-07-27 Andrew ReynoldsMinor fix for term database + central equality engine...
commit | commitdiff | tree
2021-07-27 Andrew ReynoldsRevert change to regression (#6940)
 commit | commitdiff | tree
2021-07-27 Andrew ReynoldsMake all dependencies in the fast enumerator optional...
commit | commitdiff | tree
2021-07-27 Andrew ReynoldsAdd print expression utility (#6880)
 commit | commitdiff | tree
2021-07-27 Andrew ReynoldsMinor changes from proof-new (#6937)
 commit | commitdiff | tree
2021-07-27 Andrew ReynoldsMiscellaneous fixes from proof-new (#6914)
 commit | commitdiff | tree
2021-07-27 Andrew ReynoldsAdd proof letify utility (#6881)
 commit | commitdiff | tree
2021-07-27 Andrew ReynoldsFix eq proof conversion for constant merged parameterized...
commit | commitdiff | tree
2021-07-27 Andrew ReynoldsDefault equality proofs for bags and separation logic...
commit | commitdiff | tree
2021-07-27 Andrew ReynoldsAdd sygus enumerator callback (#6923)
 commit | commitdiff | tree
2021-07-26 Andrew ReynoldsEnable default equality proofs for sets (#6931)
 commit | commitdiff | tree
2021-07-26 Andrew ReynoldsMore updates to arithmetic in preparation for central...
commit | commitdiff | tree
2021-07-25 Andrew ReynoldsChanges to datatypes in preparation for central equality...
commit | commitdiff | tree
2021-07-25 Andrew ReynoldsRefactor equality engine setup for arithmetic congruence...
commit | commitdiff | tree
2021-07-22 Andrew ReynoldsSimplify computation of relevant terms in datatypes...
commit | commitdiff | tree
2021-07-22 Andrew ReynoldsAdd the central equality engine manager (#6893)
 commit | commitdiff | tree
2021-07-22 Andrew ReynoldsMiscellaneous changes in preparation for central equality...
commit | commitdiff | tree
2021-07-22 Andrew ReynoldsPreparation for carry the rewrite rule database in...
commit | commitdiff | tree
2021-07-18 Andrew ReynoldsAdd n-ary term utilities (#6896)
 commit | commitdiff | tree
2021-07-16 Andrew ReynoldsDo not exhaustive instantiation when FMF is disabled...
commit | commitdiff | tree
2021-07-15 Andrew ReynoldsFix context for proofs of instantiations (#6890)
 commit | commitdiff | tree
2021-07-15 Andrew ReynoldsDistinguish quantifiers preprocess as its own proof...
commit | commitdiff | tree
2021-07-15 Andrew ReynoldsConnect the equality solver to theory arith (#6894)
 commit | commitdiff | tree
2021-07-15 Andrew ReynoldsArithmetic equality solver (#6876)
 commit | commitdiff | tree
2021-07-15 Andrew ReynoldsMove master equality engine notification to own file...
commit | commitdiff | tree
2021-07-15 Andrew ReynoldsAdd node converter utility (#6878)
 commit | commitdiff | tree
2021-07-14 Andrew ReynoldsFix for context on input proof generator (#6873)
 commit | commitdiff | tree
2021-07-14 Andrew ReynoldsMove synthesis verification check to own file (#6882)
 commit | commitdiff | tree
2021-07-14 Andrew ReynoldsRefactor setup of proof equality engine for central...
commit | commitdiff | tree
2021-07-14 Andrew ReynoldsFix models for sequences of infinite element type ...
commit | commitdiff | tree
2021-07-13 Andrew ReynoldsAdd branch and bound lemma if linear arithmetic generates...
commit | commitdiff | tree
2021-07-12 Andrew ReynoldsAdd branch and bound (#6865)
 commit | commitdiff | tree
2021-07-12 Andrew ReynoldsFix for learned rewrite pass, add regression (#6850)
 commit | commitdiff | tree
2021-07-12 Andrew ReynoldsAdd arithmetic preprocess rewrite equality module ...
commit | commitdiff | tree
2021-07-12 Andrew ReynoldsAdd trace for combination splits (#6862)
 commit | commitdiff | tree
2021-07-12 Andrew ReynoldsImprovements to debug check model (#6861)
 commit | commitdiff | tree
2021-07-09 Andrew ReynoldsFix sets cardinality inference involving equivalent...
commit | commitdiff | tree
2021-07-09 Andrew ReynoldsImplement stop-only for new justification heuristic...
commit | commitdiff | tree
2021-07-08 Andrew ReynoldsDisable ordering heuristic for justification by default...
commit | commitdiff | tree
2021-07-07 Andrew ReynoldsFix regressions for competition build (#6846)
 commit | commitdiff | tree
2021-07-07 Andrew ReynoldsStandard output for trigger selection (#6841)
 commit | commitdiff | tree
2021-07-06 Andrew ReynoldsIntegrate learned rewrite preprocessing pass (#6840)
 commit | commitdiff | tree
2021-07-06 Andrew ReynoldsAdd implementation of learned rewrite pass (#6843)
 commit | commitdiff | tree
2021-07-06 Andrew ReynoldsAdd learned rewrite preprocessing pass (#6842)
 commit | commitdiff | tree
2021-07-05 Andrew ReynoldsMake buffered inference manager more robust to backtracking...
commit | commitdiff | tree
2021-07-02 Andrew ReynoldsFix rewriter for negative constant seq.nth (#6827)
 commit | commitdiff | tree
2021-07-01 Andrew ReynoldsAdd recursive function definitions to subsolver in...
commit | commitdiff | tree
2021-07-01 Andrew ReynoldsAdd option to limit the number of instantiation rounds...
commit | commitdiff | tree
2021-06-30 Andrew ReynoldsDo not notify during equality engine initialization...
commit | commitdiff | tree
2021-06-30 Andrew ReynoldsDo not apply fmfBound to standard quantifiers when...
commit | commitdiff | tree
2021-06-30 Andrew ReynoldsFix pre vs. post-rewrite in proofs for theory preprocessor...
commit | commitdiff | tree
2021-06-28 Andrew ReynoldsRename internal string kinds to match API (#6797)
 commit | commitdiff | tree
2021-06-24 Andrew ReynoldsFix linear arithmetic for duplicate lemmas in incremental...
commit | commitdiff | tree
2021-06-22 Andrew ReynoldsAvoid full normalization of lambdas in getValue (#6787)
 commit | commitdiff | tree
2021-06-22 Andrew ReynoldsMinor simplification to equality engine notifications...
commit | commitdiff | tree
2021-06-22 Andrew ReynoldsAlways check legal eliminations in quantified logics...
commit | commitdiff | tree
2021-06-22 Andrew ReynoldsFix type enumeration for non first-class sorts in FMF...
commit | commitdiff | tree
2021-06-22 Andrew ReynoldsFix cases of ITE within regular expressions (#6783)
 commit | commitdiff | tree
2021-06-22 Andrew ReynoldsSet up fine grained equality notifications (#6734)
 commit | commitdiff | tree
2021-06-13 Andrew ReynoldsMinor simplifications to LogicInfo (#6737)
 commit | commitdiff | tree
2021-06-11 Andrew ReynoldsRemove support for lazy BV extended function reductions...
commit | commitdiff | tree
2021-06-10 Andrew ReynoldsEnsure bv2nat and int2bv are not rewritten when using...
commit | commitdiff | tree
2021-06-09 Andrew ReynoldsIntegrate learned literal manager into preprocessing...
commit | commitdiff | tree
2021-06-09 Andrew ReynoldsFixes related to printing tuples, define-fun commands...
commit | commitdiff | tree
2021-06-08 Andrew ReynoldsFix for 2 dimensional dependent bounded quantifiers...
commit | commitdiff | tree
2021-06-08 Andrew ReynoldsAdd learned literal manager utility (#6709)
 commit | commitdiff | tree
2021-06-08 Andrew ReynoldsMake TheoryUF compatible with central equality engine...
commit | commitdiff | tree
2021-06-08 Andrew ReynoldsFix str.update reduction (#6696)
 commit | commitdiff | tree
2021-06-07 Andrew Reynolds(proof-new) Fix missing connection in trust substitution...
commit | commitdiff | tree
2021-06-07 Andrew Reynolds(proof-new) Lazy proof chain debug names (#6680)
 commit | commitdiff | tree
2021-06-04 Andrew ReynoldsMiscellaneous changes from central ee branch (#6687)
 commit | commitdiff | tree
2021-06-03 Andrew ReynoldsSimplify automatic set-logic in smt2 parser (#6678)
 commit | commitdiff | tree
2021-06-02 Andrew ReynoldsFixes for printing define-fun-rec (#6673)
 commit | commitdiff | tree
2021-06-02 Andrew ReynoldsFix unsat core proofs (#6655)
 commit | commitdiff | tree
2021-06-01 Andrew ReynoldsUse top-level substitutions in ITE simp (#6651)
 commit | commitdiff | tree
2021-06-01 Andrew ReynoldsDisable timeout regressions (#6650)
 commit | commitdiff | tree
2021-05-27 Andrew ReynoldsFix regular expression aggressive elim (#6627)
 commit | commitdiff | tree
2021-05-27 Andrew ReynoldsUpdate proof namespaces (#6614)
 commit | commitdiff | tree
2021-05-27 Andrew ReynoldsFix CEGQI for datatypes with Boolean subfields (#6630)
 commit | commitdiff | tree
2021-05-27 Andrew ReynoldsFix spurious assertion for trivial abduction (#6629)
 commit | commitdiff | tree
2021-05-27 Andrew ReynoldsEnable new justification heuristic by default (#6613)
 commit | commitdiff | tree
2021-05-24 Andrew ReynoldsFix non-fixed length case in re-elim (#6612)
 commit | commitdiff | tree
2021-05-24 Andrew ReynoldsImplementation of the new justification heuristic ...
commit | commitdiff | tree
2021-05-24 Andrew ReynoldsMove proof utilities to src/proof/ (#6611)
 commit | commitdiff | tree
2021-05-24 Andrew ReynoldsFix re-elim length requirement for symbolic RE memberships...
commit | commitdiff | tree
2021-05-24 Andrew ReynoldsFix instance of no rewrite in extended rewriter (#6610)
 commit | commitdiff | tree
2021-05-24 Andrew ReynoldsBetter formalization of regular expression unfolding...
commit | commitdiff | tree
2021-05-21 Andrew ReynoldsFix tests of unsat cores (#6593)
 commit | commitdiff | tree
2021-05-21 Andrew ReynoldsFix and refactor relevant domain (#6528)
 commit | commitdiff | tree
2021-05-21 Andrew ReynoldsFormalize shared selectors as skolem functions (#6591)
 commit | commitdiff | tree
2021-05-21 Andrew ReynoldsMinor simplification to boolean proof checker (#6590)
 commit | commitdiff | tree
2021-05-21 Andrew Reynolds(proof-new) Minor documentation sync (#6592)
 commit | commitdiff | tree
2021-05-21 Andrew ReynoldsAdd utility to get all types occurring in a term (...
commit | commitdiff | tree
2021-05-21 Andrew ReynoldsUpdate to sygus standard output for check-synth responses...
commit | commitdiff | tree
2021-05-19 Andrew ReynoldsPass empty vector when constructing re empty, fixes...
commit | commitdiff | tree
2021-05-19 Andrew ReynoldsMake strings emp inference an unhandled inference for...
commit | commitdiff | tree
2021-05-19 Andrew ReynoldsFix strings rewriter for non-standard re range (#6570)
 commit | commitdiff | tree
next