projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2020-10-13 yoni206bv2int: improving bvand tables (#5235) commit | commitdiff | tree
2020-10-12 Andrew ReynoldsRemove uf-ss-totality option (#5251) commit | commitdiff | tree
2020-10-12 Andrew ReynoldsEliminate uses of Expr in SmtEngine interface (#5240) commit | commitdiff | tree
2020-10-12 Andrew ReynoldsEnsure uninterpreted sort owner is UF if uf-ho or finit... commit | commitdiff | tree
2020-10-11 Mathias PreinerSyGuS instantiation modes (#5228) commit | commitdiff | tree
2020-10-11 Gereon KremerAdd conversion of poly polynomial to cvc node. (#5218) commit | commitdiff | tree
2020-10-10 Abdalrhman... Provide API version of some SMT Commands. (#5222) commit | commitdiff | tree
2020-10-10 yoni206bv2int: bvand translation code move (#5227) commit | commitdiff | tree
2020-10-09 Mathias PreinerRemove deprecated add-path commands and use $GITHUB_PAT... commit | commitdiff | tree
2020-10-09 Alex Ozdemiruse right arith explanation fn to fix regressions ... commit | commitdiff | tree
2020-10-09 Alex Ozdemir(proof-new) proofs for arith-constraint explanations... commit | commitdiff | tree
2020-10-09 Andres Noetzlireset-assertions: Remove all non-global symbols in... commit | commitdiff | tree
2020-10-09 Andrew ReynoldsSimplify approach for collapsed selectors over non... commit | commitdiff | tree
2020-10-09 Andrew Reynolds(proof-new) Add lazy proof set utility (#5221) commit | commitdiff | tree
2020-10-09 Andrew Reynolds(proof-new) Theory engine proof producing (#5195) commit | commitdiff | tree
2020-10-08 Andrew Reynolds(proof-new) Fixes and improvements for smt proof postpr... commit | commitdiff | tree
2020-10-08 makaimannGet correct NodeManagerScope for toStrings in API ... commit | commitdiff | tree
2020-10-08 yoni206fix unit failures on debug without symfpu (#5212) commit | commitdiff | tree
2020-10-07 Alex Ozdemir(proof-new) proofs in ee -> arith pipeline (#5215) commit | commitdiff | tree
2020-10-07 Aina NiemetzNew C++ API: Rename Term::isConst() to Term::isValue... commit | commitdiff | tree
2020-10-07 Gereon KremerMake sure conflicts are not rewritten (in arithmetic... commit | commitdiff | tree
2020-10-07 Andrew Reynolds(proof-new) Add the strings proof constructor (#4903) commit | commitdiff | tree
2020-10-07 Malte MuesImprove OSX support by adding os detection and adapting... commit | commitdiff | tree
2020-10-07 Andrew ReynoldsProcess pending inferences at the beginning of datatype... commit | commitdiff | tree
2020-10-06 yoni206bv-to-int: change order of passes (#5208) commit | commitdiff | tree
2020-10-06 Alex Ozdemir(proof-new) proofs for ArithCongMan -> ee facts (#5207) commit | commitdiff | tree
2020-10-06 Andrew Reynolds(proof-new) Add interface for trusted substitution... commit | commitdiff | tree
2020-10-06 Andrew Reynolds(proof-new) Allow null proofs from generators in LazyCD... commit | commitdiff | tree
2020-10-06 mudathirmahgoubAdd operators bag.from_set, bag.to_set to the theory... commit | commitdiff | tree
2020-10-06 Andrew ReynoldsAdd arithmetic preprocess module (#5188) commit | commitdiff | tree
2020-10-06 Abdalrhman... Recover from some exceptions. (#5203) commit | commitdiff | tree
2020-10-06 mudathirmahgoubRemove subtyping for sets (#5205) commit | commitdiff | tree
2020-10-05 Aina Niemetzcmake: Add warning when unit testing is disabled due... commit | commitdiff | tree
2020-10-05 Aina NiemetzSyGuS: Add fp.sub to default FP grammar. (#5206) commit | commitdiff | tree
2020-10-05 Aina NiemetzInteger: GMP: Move implementation of member functions... commit | commitdiff | tree
2020-10-05 Andrew ReynoldsMake sygus more robust to unknown responses in solution... commit | commitdiff | tree
2020-10-04 mudathirmahgoubRemove subtyping for sets theory (#5179) commit | commitdiff | tree
2020-10-03 Aina Niemetzsygus-inst: Add more special BV values. (#5191) commit | commitdiff | tree
2020-10-03 Mathias PreinerFix CI builds and add cancel workflow. commit | commitdiff | tree
2020-10-03 Andrew ReynoldsFix theory white unit test (#5194) commit | commitdiff | tree
2020-10-03 Andrew ReynoldsStandardization of Theory (#5181) commit | commitdiff | tree
2020-10-02 Andrew ReynoldsMinor simplifications to substitution map class (#5180) commit | commitdiff | tree
2020-10-02 Andrew Reynolds(proof-new) Fixes for theory preprocessing proofs ... commit | commitdiff | tree
2020-10-02 Andrew Reynolds(proof-new) Make shared solver proof producing (#5169) commit | commitdiff | tree
2020-10-02 Gereon KremerAllow for theory combination of strings with nonlinear... commit | commitdiff | tree
2020-10-02 Andrew ReynoldsDecouple modules from TheoryArithPrivate (#5184) commit | commitdiff | tree
2020-10-02 Alex Ozdemir(proof-new) New proofs in arith::Constraint::externalEx... commit | commitdiff | tree
2020-10-02 Alex OzdemirRemove duplicate declarations in th_bv.plf (#5183) commit | commitdiff | tree
2020-10-02 Aina NiemetzSyGuS: Add min/max (sub)normal constants to FP default... commit | commitdiff | tree
2020-10-01 Andrew Reynolds(proof-new) Make arrays proof producing (#5112) commit | commitdiff | tree
2020-10-01 Mathias PreinerAdd additional ground terms to SyGuS instantiation... commit | commitdiff | tree
2020-10-01 Andrew ReynoldsUpdate theory of arithmetic to standard check (#5178) commit | commitdiff | tree
2020-10-01 Aina NiemetzFloatingPoint: Add utility functions for largest and... commit | commitdiff | tree
2020-10-01 Gereon KremerAllow to use the initial assignment for CAD (#5177) commit | commitdiff | tree
2020-10-01 Andrew Reynolds(proof-new) Preprocessing passes use proper interfaces... commit | commitdiff | tree
2020-10-01 Andrew ReynoldsMake SygusSolver use sygus attributes directly (#5172) commit | commitdiff | tree
2020-10-01 Mathias PreinerAdd GH action to cancel previous pending/running CI... commit | commitdiff | tree
2020-10-01 Aina NiemetzBitVector: Extend interface of setBit to set it to... commit | commitdiff | tree
2020-09-30 Aina NiemetzFloatingPoint: Add utility functions for largest and... commit | commitdiff | tree
2020-09-30 Gereon KremerRemove too strict assertion to allow for approximate... commit | commitdiff | tree
2020-09-30 Gereon KremerAdd missing includes. (#5170) commit | commitdiff | tree
2020-09-30 Gereon KremerAdd strategy for nonlinear extension (#5160) commit | commitdiff | tree
2020-09-30 Andrew ReynoldsDynamic allocation of equality engine for shared solver... commit | commitdiff | tree
2020-09-30 Andrew Reynolds(proof-new) Add the term conversion sequence generator... commit | commitdiff | tree
2020-09-29 Haniel Barbosa[proof-new] Adds a proof manager for prop engine (... commit | commitdiff | tree
2020-09-29 mudathirmahgoubFix bags headers (#5165) commit | commitdiff | tree
2020-09-29 Alex Ozdemir(proof-new) Add proof managers and eager gens to arith... commit | commitdiff | tree
2020-09-29 Andrew Reynolds(proof-new) Fixes for preprocess proof generator and... commit | commitdiff | tree
2020-09-29 Haniel Barbosa[proof-new] Adds a proof post processor for the Prop... commit | commitdiff | tree
2020-09-29 Haniel Barbosa[proof-new] Updates to proof node updater (#5156) commit | commitdiff | tree
2020-09-29 Haniel Barbosa[proof-new] Adds a proof-producing CNF converter (... commit | commitdiff | tree
2020-09-29 Gereon KremerClean up nonlinear extension (#5149) commit | commitdiff | tree
2020-09-29 Andrew ReynoldsReset assertions on resetAssertions (#5153) commit | commitdiff | tree
2020-09-29 Alex OzdemirAdd utilities for arith/proof_checker and build it... commit | commitdiff | tree
2020-09-29 Haniel Barbosa[proof-new] Removing spurious forward declaration in... commit | commitdiff | tree
2020-09-29 Haniel Barbosa[proof-new] Adds a proof node hash function (#5154) commit | commitdiff | tree
2020-09-29 Andrew ReynoldsDisable regression that is timing out (#5142) commit | commitdiff | tree
2020-09-28 Andrew ReynoldsMinor fixes to quantifiers proofs (#5151) commit | commitdiff | tree
2020-09-28 Haniel Barbosa[proof-new] Adds a proof manager for the SAT solver... commit | commitdiff | tree
2020-09-28 mudathirmahgoubImplement bags rewriter (#5132) commit | commitdiff | tree
2020-09-28 Gereon KremerAdd new arithmetic BoundInference class (#5148) commit | commitdiff | tree
2020-09-27 Andrew ReynoldsFix sygus quantifier elimination preprocess for multipl... commit | commitdiff | tree
2020-09-26 Gereon KremerUse inference manager for nl_solver (#5125) commit | commitdiff | tree
2020-09-26 Andrew ReynoldsConnect the shared solver to theory engine (#5103) commit | commitdiff | tree
2020-09-26 Andrew ReynoldsUse original quantified formula for single invocation... commit | commitdiff | tree
2020-09-26 Aina NiemetzRestrict bvxnor to only allow two operands (was n-ary... commit | commitdiff | tree
2020-09-25 Andrew ReynoldsMake sygus refinement step more robust to unevaluatable... commit | commitdiff | tree
2020-09-25 Haniel BarbosaCleaning and documenting cnf stream (#5134) commit | commitdiff | tree
2020-09-24 Aina NiemetzSyGuS: Add default grammar for FP. (#5133) commit | commitdiff | tree
2020-09-24 Andrew Reynolds Function definition fmf preprocessing pass (#5064) commit | commitdiff | tree
2020-09-24 Andrew ReynoldsModify lemma vs fact policy for datatype equalities... commit | commitdiff | tree
2020-09-23 Andrew ReynoldsDisable cegqi-bv when using sygus (#5124) commit | commitdiff | tree
2020-09-23 Gereon KremerMake IAND solver use inference manager. (#5126) commit | commitdiff | tree
2020-09-23 Aina NiemetzMissing format from #5112. commit | commitdiff | tree
2020-09-23 yoni206bv2int: new options for bvand translation (#5096) commit | commitdiff | tree
2020-09-23 Andrew ReynoldsAllow E-matching by default when strings are enabled... commit | commitdiff | tree
2020-09-23 Aina NiemetzNew C++ API: Catch and throw recoverable exception... commit | commitdiff | tree
2020-09-23 Aina NiemetzFP: Use Assert instead of AlwaysAssert in traits::... commit | commitdiff | tree
2020-09-23 Abdalrhman... Refactor Commands to use the Public API. (#5105) commit | commitdiff | tree
2020-09-23 Andrew ReynoldsFix type issue with term formula removal (#5107) commit | commitdiff | tree
next