cvc5.git
2020-10-18 Andrew Reynolds (proof-new) Witness axiom reconstruction for purificat...
2020-10-18 Andrew Reynolds(proof-new) Implementation of trust substitution (...
2020-10-18 Andrew Reynolds(proof-new) More features for SMT proof post-processor...
2020-10-18 Andrew Reynolds(proof-new) Improvements for theory engine (#5292)
2020-10-16 Andrew ReynoldsRefactor SMT-level model object (#5277)
2020-10-16 Andrew ReynoldsCatch more cases of nested recursion in datatypes ...
2020-10-16 yoni206bv2int: caching introduced terms (#5283)
2020-10-16 Andrew ReynoldsAdd inference enumeration to datatypes (#5275)
2020-10-15 Alex Ozdemir(proof-new) TheoryArithPrivate: farkas lemma proof...
2020-10-14 mudathirmahgoubFix issue #5269 (#5270)
2020-10-14 yoni206bv2int: implementing the iand-sum mode (#5265)
2020-10-14 Alex Ozdemir(proof-new) debug statements & docs for INT_TRUST ...
2020-10-14 Alex Ozdemir(proof-new) pfs in TheoryArith(Private) explainations...
2020-10-14 Andrew ReynoldsGuard uses of printing approximations for constants...
2020-10-14 Alex Ozdemir(proof-new) pfs for conflicts in TheoryArithPrivate...
2020-10-14 yoni206bv2int: rewritings and unsat cores (#5263)
2020-10-14 Haniel Barbosausing NOT_NOT_ELIM rather than macros to do double...
2020-10-14 Alex Ozdemir(proof-new) Prove lemmas in Constraint (#5254)
2020-10-14 Andrew Reynolds(proof-new) Generalize preprocess proof generator ...
2020-10-14 Andrew Reynolds(proof-new) Simplifications for proof rule checker...
2020-10-14 Andrew Reynolds (proof-new) Miscellaneous minor improvements and fixes...
2020-10-13 Andrew Reynolds(proof-new) New rules for Booleans (#5243)
2020-10-13 Andrew Reynolds(proof-new) Change merge policy for proof node updater...
2020-10-13 yoni206bv2int: improving bvand tables (#5235)
2020-10-12 Andrew ReynoldsRemove uf-ss-totality option (#5251)
2020-10-12 Andrew ReynoldsEliminate uses of Expr in SmtEngine interface (#5240)
2020-10-12 Andrew ReynoldsEnsure uninterpreted sort owner is UF if uf-ho or finit...
2020-10-11 Mathias PreinerSyGuS instantiation modes (#5228)
2020-10-11 Gereon KremerAdd conversion of poly polynomial to cvc node. (#5218)
2020-10-10 Abdalrhman... Provide API version of some SMT Commands. (#5222)
2020-10-10 yoni206bv2int: bvand translation code move (#5227)
2020-10-09 Mathias PreinerRemove deprecated add-path commands and use $GITHUB_PAT...
2020-10-09 Alex Ozdemiruse right arith explanation fn to fix regressions ...
2020-10-09 Alex Ozdemir(proof-new) proofs for arith-constraint explanations...
2020-10-09 Andres Noetzlireset-assertions: Remove all non-global symbols in...
2020-10-09 Andrew ReynoldsSimplify approach for collapsed selectors over non...
2020-10-09 Andrew Reynolds(proof-new) Add lazy proof set utility (#5221)
2020-10-09 Andrew Reynolds(proof-new) Theory engine proof producing (#5195)
2020-10-08 Andrew Reynolds(proof-new) Fixes and improvements for smt proof postpr...
2020-10-08 makaimannGet correct NodeManagerScope for toStrings in API ...
2020-10-08 yoni206fix unit failures on debug without symfpu (#5212)
2020-10-07 Alex Ozdemir(proof-new) proofs in ee -> arith pipeline (#5215)
2020-10-07 Aina NiemetzNew C++ API: Rename Term::isConst() to Term::isValue...
2020-10-07 Gereon KremerMake sure conflicts are not rewritten (in arithmetic...
2020-10-07 Andrew Reynolds(proof-new) Add the strings proof constructor (#4903)
2020-10-07 Malte MuesImprove OSX support by adding os detection and adapting...
2020-10-07 Andrew ReynoldsProcess pending inferences at the beginning of datatype...
2020-10-06 yoni206bv-to-int: change order of passes (#5208)
2020-10-06 Alex Ozdemir(proof-new) proofs for ArithCongMan -> ee facts (#5207)
2020-10-06 Andrew Reynolds(proof-new) Add interface for trusted substitution...
2020-10-06 Andrew Reynolds(proof-new) Allow null proofs from generators in LazyCD...
2020-10-06 mudathirmahgoubAdd operators bag.from_set, bag.to_set to the theory...
2020-10-06 Andrew ReynoldsAdd arithmetic preprocess module (#5188)
2020-10-06 Abdalrhman... Recover from some exceptions. (#5203)
2020-10-06 mudathirmahgoubRemove subtyping for sets (#5205)
2020-10-05 Aina Niemetzcmake: Add warning when unit testing is disabled due...
2020-10-05 Aina NiemetzSyGuS: Add fp.sub to default FP grammar. (#5206)
2020-10-05 Aina NiemetzInteger: GMP: Move implementation of member functions...
2020-10-05 Andrew ReynoldsMake sygus more robust to unknown responses in solution...
2020-10-04 mudathirmahgoubRemove subtyping for sets theory (#5179)
2020-10-03 Aina Niemetzsygus-inst: Add more special BV values. (#5191)
2020-10-03 Mathias PreinerFix CI builds and add cancel workflow.
2020-10-03 Andrew ReynoldsFix theory white unit test (#5194)
2020-10-03 Andrew ReynoldsStandardization of Theory (#5181)
2020-10-02 Andrew ReynoldsMinor simplifications to substitution map class (#5180)
2020-10-02 Andrew Reynolds(proof-new) Fixes for theory preprocessing proofs ...
2020-10-02 Andrew Reynolds(proof-new) Make shared solver proof producing (#5169)
2020-10-02 Gereon KremerAllow for theory combination of strings with nonlinear...
2020-10-02 Andrew ReynoldsDecouple modules from TheoryArithPrivate (#5184)
2020-10-02 Alex Ozdemir(proof-new) New proofs in arith::Constraint::externalEx...
2020-10-02 Alex OzdemirRemove duplicate declarations in th_bv.plf (#5183)
2020-10-02 Aina NiemetzSyGuS: Add min/max (sub)normal constants to FP default...
2020-10-01 Andrew Reynolds(proof-new) Make arrays proof producing (#5112)
2020-10-01 Mathias PreinerAdd additional ground terms to SyGuS instantiation...
2020-10-01 Andrew ReynoldsUpdate theory of arithmetic to standard check (#5178)
2020-10-01 Aina NiemetzFloatingPoint: Add utility functions for largest and...
2020-10-01 Gereon KremerAllow to use the initial assignment for CAD (#5177)
2020-10-01 Andrew Reynolds(proof-new) Preprocessing passes use proper interfaces...
2020-10-01 Andrew ReynoldsMake SygusSolver use sygus attributes directly (#5172)
2020-10-01 Mathias PreinerAdd GH action to cancel previous pending/running CI...
2020-10-01 Aina NiemetzBitVector: Extend interface of setBit to set it to...
2020-09-30 Aina NiemetzFloatingPoint: Add utility functions for largest and...
2020-09-30 Gereon KremerRemove too strict assertion to allow for approximate...
2020-09-30 Gereon KremerAdd missing includes. (#5170)
2020-09-30 Gereon KremerAdd strategy for nonlinear extension (#5160)
2020-09-30 Andrew ReynoldsDynamic allocation of equality engine for shared solver...
2020-09-30 Andrew Reynolds(proof-new) Add the term conversion sequence generator...
2020-09-29 Haniel Barbosa[proof-new] Adds a proof manager for prop engine (...
2020-09-29 mudathirmahgoubFix bags headers (#5165)
2020-09-29 Alex Ozdemir(proof-new) Add proof managers and eager gens to arith...
2020-09-29 Andrew Reynolds(proof-new) Fixes for preprocess proof generator and...
2020-09-29 Haniel Barbosa[proof-new] Adds a proof post processor for the Prop...
2020-09-29 Haniel Barbosa[proof-new] Updates to proof node updater (#5156)
2020-09-29 Haniel Barbosa[proof-new] Adds a proof-producing CNF converter (...
2020-09-29 Gereon KremerClean up nonlinear extension (#5149)
2020-09-29 Andrew ReynoldsReset assertions on resetAssertions (#5153)
2020-09-29 Alex OzdemirAdd utilities for arith/proof_checker and build it...
2020-09-29 Haniel Barbosa[proof-new] Removing spurious forward declaration in...
2020-09-29 Haniel Barbosa[proof-new] Adds a proof node hash function (#5154)
2020-09-29 Andrew ReynoldsDisable regression that is timing out (#5142)
next