projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2020-11-11 Andrew ReynoldsFix preregistration in TheorySep before declare-heap... commit | commitdiff | tree
2020-11-10 Andrew ReynoldsDo not mark extended functions as reduced based on... commit | commitdiff | tree
2020-11-10 Alex OzdemirPin LFSC version (#5412) commit | commitdiff | tree
2020-11-10 Andrew ReynoldsMake mkGroundTerm deterministic (#5347) commit | commitdiff | tree
2020-11-10 Andrew ReynoldsAdd getSubtermKinds to node algorithm (#5398) commit | commitdiff | tree
2020-11-10 Andrew ReynoldsAdd proper support for the declare-heap command for... commit | commitdiff | tree
2020-11-10 Andrew ReynoldsMigrate some documentation about attributes (#5390) commit | commitdiff | tree
2020-11-09 Andrew ReynoldsAdd symbol manager (#5380) commit | commitdiff | tree
2020-11-09 Andrew ReynoldsSimplify handling of subtypes in smt2 printer (#5401) commit | commitdiff | tree
2020-11-09 Gereon KremerProperly clear interrupt for solve() as well. (#5403) commit | commitdiff | tree
2020-11-09 Andrew ReynoldsDo not regress explanations of datatype lemmas (#5376) commit | commitdiff | tree
2020-11-06 mudathirmahgoubFix issue #5342 (#5349) commit | commitdiff | tree
2020-11-06 Andrew Reynolds(proof-new) Miscellaneous changes to strings for proofs... commit | commitdiff | tree
2020-11-06 Andrew ReynoldsSplit sygus template inference to its own file (#5388) commit | commitdiff | tree
2020-11-06 Andrew ReynoldsSimplify printing with respect to expression types... commit | commitdiff | tree
2020-11-05 mudathirmahgoubRemove mkSingleton from the API (#5366) commit | commitdiff | tree
2020-11-04 Andres NoetzliAdd constants from equality engine evaluation to model... commit | commitdiff | tree
2020-11-03 Andrew ReynoldsAdd scope methods constructing types in API (#5393) commit | commitdiff | tree
2020-11-03 Andres NoetzliAdd support for printing `re.loop` and `re.^` (#5392) commit | commitdiff | tree
2020-11-03 Andrew ReynoldsReset built model flag at presolve in nonlinear (#5386) commit | commitdiff | tree
2020-11-03 Andrew ReynoldsMove sygus qe preproc to its own file (#5375) commit | commitdiff | tree
2020-11-03 makaimannRun python tests during make check (#5226) commit | commitdiff | tree
2020-11-02 Aina Niemetzcontrib: Remove dependency directories. (#5367) commit | commitdiff | tree
2020-11-02 Andrew ReynoldsUpdate strings proxy variable map to be context indepen... commit | commitdiff | tree
2020-11-02 Andrew ReynoldsMiscellaneous cleaning of parser (#5369) commit | commitdiff | tree
2020-11-02 Andrew ReynoldsAvoid dynamic allocation in symbol table implementation... commit | commitdiff | tree
2020-10-30 Gereon KremerUse BoundInference in nonlinear extension (#5359) commit | commitdiff | tree
2020-10-30 Andrew ReynoldsUpdate api::Sort to use TypeNode instead of Type (... commit | commitdiff | tree
2020-10-29 Andrew ReynoldsSet strings pending conflict flag (#5364) commit | commitdiff | tree
2020-10-29 mudathirmahgoubAdd mkInteger to the API (#5274) commit | commitdiff | tree
2020-10-29 Andrew Reynolds(proof-new) Update the strings inference manager for... commit | commitdiff | tree
2020-10-29 Gereon KremerAdd NodeManager::mkOr() (#5360) commit | commitdiff | tree
2020-10-28 yoni206run_regression.py to fail on invalid requirements ... commit | commitdiff | tree
2020-10-28 Andrew ReynoldsRemove more uses of Expr (#5357) commit | commitdiff | tree
2020-10-28 Andrew ReynoldsFixes for unconstrained variables in nonlinear model... commit | commitdiff | tree
2020-10-28 Andrew ReynoldsConvert symbol table from Expr-level to Term-level... commit | commitdiff | tree
2020-10-28 Gereon KremerSplit NlSolver in multiple subsolvers (#5315) commit | commitdiff | tree
2020-10-28 Andrew ReynoldsAdd rewrites for div/mod in the arithmetic rewriter... commit | commitdiff | tree
2020-10-27 Mathias Preinerrun_regression: Add --skip-timeout option, lower timeou... commit | commitdiff | tree
2020-10-27 Abdalrhman... Refactor DeclareSygusVarCommand and SynthFunCommand... commit | commitdiff | tree
2020-10-27 Andrew ReynoldsAdd missing methods involving datatype sorts to the... commit | commitdiff | tree
2020-10-27 Gereon KremerDisable --nl-cad option by default (#5350) commit | commitdiff | tree
2020-10-27 Gereon KremerEnable --nl-cad by default (#5345) commit | commitdiff | tree
2020-10-27 mudathirmahgoubAdd DUPICATE_REMOVAL operator to bags (#5336) commit | commitdiff | tree
2020-10-26 Andrew Reynolds(proof-new) Add datatypes proof checker (#5340) commit | commitdiff | tree
2020-10-26 Andrew ReynoldsSend external equalities from collapse selector as... commit | commitdiff | tree
2020-10-24 mudathirmahgoubFix issue 5271 (#5335) commit | commitdiff | tree
2020-10-24 Haniel Barbosa[proof-new] Fix n-ary kind handling in EqEngine explana... commit | commitdiff | tree
2020-10-23 Andrew ReynoldsApply alpha equivalence to annotated quantified formula... commit | commitdiff | tree
2020-10-23 Andrew ReynoldsChange datatypes lemma policy for equalities not coming... commit | commitdiff | tree
2020-10-23 Andrew ReynoldsFix related to preregistering boolean term variables... commit | commitdiff | tree
2020-10-22 Gereon KremerUse theoryof-mode=type for QF_NRA (#5326) commit | commitdiff | tree
2020-10-22 Andrew ReynoldsRemove unused equality engine types (#5319) commit | commitdiff | tree
2020-10-22 mudathirmahgoubFix issue 5309 (#5327) commit | commitdiff | tree
2020-10-22 Andrew Reynolds(proof-new) Make theory preprocessor user-context depen... commit | commitdiff | tree
2020-10-21 Gereon Kremer(proof-new) Make circuit propagator proof producing... commit | commitdiff | tree
2020-10-21 mudathirmahgoubImplement bags evaluator (#5322) commit | commitdiff | tree
2020-10-21 Alex Ozdemir(proof-new) Add arith proof macros file to CMake (... commit | commitdiff | tree
2020-10-21 Alex Ozdemir(proof-new) arith: dedup literals in flattenImpl (... commit | commitdiff | tree
2020-10-21 Andrew Reynolds(proof-new) Updates to lazy proof chain (#5317) commit | commitdiff | tree
2020-10-21 mudathirmahgoubAdd operator MakeBagOp for constructing bags (#5209) commit | commitdiff | tree
2020-10-21 Abdalrhman... Add finishInit for getInterpol and getAbduct. (#5316) commit | commitdiff | tree
2020-10-21 Andrew Reynolds(proof-new) Fixes for proofs in rewriter (#5307) commit | commitdiff | tree
2020-10-20 Aina NiemetzFix compiler warnings. (#5305) commit | commitdiff | tree
2020-10-20 Gereon Kremer(proof-new) Add proofs for circuit propagator (#5301) commit | commitdiff | tree
2020-10-20 Andrew Reynolds(proof-new) Fix for CDProof::isSame (#5297) commit | commitdiff | tree
2020-10-20 Andrew Reynolds(proof-new) Update add lazy step interface in LazyCDPro... commit | commitdiff | tree
2020-10-20 Abdalrhman... Remove some Commands from the API. (#5268) commit | commitdiff | tree
2020-10-20 Andrew ReynoldsFix miscellaneous warnings (#5256) commit | commitdiff | tree
2020-10-20 Andrew ReynoldsMake seq.nth a trigger kind (#5314) commit | commitdiff | tree
2020-10-20 Gereon KremerHandle rewrite to bool in BoundInference (#5311) commit | commitdiff | tree
2020-10-20 Andrew ReynoldsSplit CheckModels utility to its own file (#5303) commit | commitdiff | tree
2020-10-20 Aina NiemetzInteger (CLN): Minor improvements. (#5306) commit | commitdiff | tree
2020-10-20 yoni206Expand `seq.nth` lazily (#5287) commit | commitdiff | tree
2020-10-19 Aina NiemetzInteger: CLN: Move implementation of member functions... commit | commitdiff | tree
2020-10-19 Haniel Barbosa[proof-new] Fixing resolution proof checker (#5262) commit | commitdiff | tree
2020-10-19 Andrew Reynolds(proof-new) Updates to assertions pipeline and preproce... commit | commitdiff | tree
2020-10-19 Andrew Reynolds(proof-new) Update preprocessing pass context for proof... commit | commitdiff | tree
2020-10-19 Haniel Barbosa[proof-new] Improving cycle checking in lazycdproofchai... commit | commitdiff | tree
2020-10-19 Andrew ReynoldsSafer version of pending lemma processing in inference... commit | commitdiff | tree
2020-10-19 Andrew Reynolds(proof-new) Refactoring cyclic checks (#5291) commit | commitdiff | tree
2020-10-18 Andrew Reynolds (proof-new) Witness axiom reconstruction for purificat... commit | commitdiff | tree
2020-10-18 Andrew Reynolds(proof-new) Implementation of trust substitution (... commit | commitdiff | tree
2020-10-18 Andrew Reynolds(proof-new) More features for SMT proof post-processor... commit | commitdiff | tree
2020-10-18 Andrew Reynolds(proof-new) Improvements for theory engine (#5292) commit | commitdiff | tree
2020-10-16 Andrew ReynoldsRefactor SMT-level model object (#5277) commit | commitdiff | tree
2020-10-16 Andrew ReynoldsCatch more cases of nested recursion in datatypes ... commit | commitdiff | tree
2020-10-16 yoni206bv2int: caching introduced terms (#5283) commit | commitdiff | tree
2020-10-16 Andrew ReynoldsAdd inference enumeration to datatypes (#5275) commit | commitdiff | tree
2020-10-15 Alex Ozdemir(proof-new) TheoryArithPrivate: farkas lemma proof... commit | commitdiff | tree
2020-10-14 mudathirmahgoubFix issue #5269 (#5270) commit | commitdiff | tree
2020-10-14 yoni206bv2int: implementing the iand-sum mode (#5265) commit | commitdiff | tree
2020-10-14 Alex Ozdemir(proof-new) debug statements & docs for INT_TRUST ... commit | commitdiff | tree
2020-10-14 Alex Ozdemir(proof-new) pfs in TheoryArith(Private) explainations... commit | commitdiff | tree
2020-10-14 Andrew ReynoldsGuard uses of printing approximations for constants... commit | commitdiff | tree
2020-10-14 Alex Ozdemir(proof-new) pfs for conflicts in TheoryArithPrivate... commit | commitdiff | tree
2020-10-14 yoni206bv2int: rewritings and unsat cores (#5263) commit | commitdiff | tree
2020-10-14 Haniel Barbosausing NOT_NOT_ELIM rather than macros to do double... commit | commitdiff | tree
2020-10-14 Alex Ozdemir(proof-new) Prove lemmas in Constraint (#5254) commit | commitdiff | tree
2020-10-14 Andrew Reynolds(proof-new) Generalize preprocess proof generator ... commit | commitdiff | tree
next