cvc5.git
2022-03-07 Andrew ReynoldsProper error message for non-first-class sets (#8245)
2022-03-07 Gereon KremerTry harder to show that a RAN is rational (#8230)
2022-03-06 Andres NoetzliDisallow models with `--arrays-weak-equiv` (#8217)
2022-03-05 Andrew ReynoldsUnit tests for fixed projects issues (#8229)
2022-03-05 Andrew ReynoldsMake seq.unit robust wrt subtyping (#8209)
2022-03-05 Andres Noetzli[Docs] Add missing requirement (#8238)
2022-03-05 Gereon KremerAdd regressions for fixed issue (#8237)
2022-03-05 Andrew ReynoldsEnable NL tangent planes by default (#8233)
2022-03-04 mudathirmahgoubFix bag.map upwards inferences (#8232)
2022-03-04 Gereon KremerAdd unit test for fixed issue (#8235)
2022-03-04 Gereon KremerRemove spurious assertion in linear solver (#8231)
2022-03-04 Gereon KremerGuard recursion into terms during substitution in arith...
2022-03-04 Andrew ReynoldsFix rewrite rule synthesis for 0-ary operators (#8221)
2022-03-04 Andrew ReynoldsLogic exception when using solution filtering for non...
2022-03-04 Gereon KremerOnly build wheels nightly and for releases (#8223)
2022-03-04 Andrew ReynoldsAdd regressions for fixed projects issues (#8228)
2022-03-04 Andrew ReynoldsAdd support for get learned literals in the API (#8099)
2022-03-03 Andrew ReynoldsFix datatype declaration printing in LFSC printer ...
2022-03-03 Gereon KremerBuild python wheels in our CI (#8087)
2022-03-03 Andrew ReynoldsGeneralize LFSC string signature to sequences (#8220)
2022-03-03 Lachnitt[proofs] Alethe: Removed Steps that are Double-Printed...
2022-03-03 Andrew ReynoldsThrow logic exception if a transcendental function...
2022-03-03 Andrew ReynoldsAdd regression for fixed issue (#8213)
2022-03-03 Andrew ReynoldsImprove error for higher-order logic (#8207)
2022-03-03 Mathias Preinercmake: Fix murxla setup. (#8215)
2022-03-03 Gereon KremerIntegrate pythonic api (#8131)
2022-03-03 Gereon KremerFix rewriting of mixed-integer atoms (#8214)
2022-03-02 Andrew ReynoldsFix issue with dropping non-reduced sine terms (#8211)
2022-03-02 Andrew ReynoldsFix models involving cardinality of sets of finite...
2022-03-02 Andrew ReynoldsAlways purify universe from set minus (#8201)
2022-03-02 Andrew ReynoldsEliminate CDHashMap::insertAtContextLevelZero (#8173)
2022-03-02 Andrew ReynoldsFix incorrect assertion in prop engine proofs (#8204)
2022-03-02 Andrew ReynoldsClean usage of options in regressions (#8190)
2022-03-02 Andrew ReynoldsImprove error message when not using strings-exp (...
2022-03-02 Gereon KremerMove libpoly <-> CoCoA conversion to new utility (...
2022-03-02 Gereon KremerRefactor rewriting of arithmetic division (#8195)
2022-03-02 Andrew ReynoldsAdd utility to access how to print floating point ...
2022-03-02 Andrew ReynoldsMake blockModelValues robust to non-closed enumerable...
2022-03-02 Andrew ReynoldsAdd regressions for fixed issues (#8202)
2022-03-02 Gereon KremerPrune spurious roots in lazard evaluation of coverings...
2022-03-02 Gereon KremerAdd standard theories to documentation (#8192)
2022-03-01 Andrew ReynoldsFix issue involving dropped purification lemmas for...
2022-03-01 Andrew ReynoldsDo not use sygus evaluation functions in sygus-inst...
2022-03-01 Andrew ReynoldsDisable regression (#8191)
2022-03-01 Andres Noetzli[BV] Fix rewriter policy for `bvneg` (#8196)
2022-03-01 Andrew ReynoldsFix lambda lifting + proofs (#8152)
2022-03-01 Andres NoetzliRemove unused data members from `TheoryArrays` (#8197)
2022-03-01 Gereon KremerRename cad to coverings (#8187)
2022-02-28 Andres Noetzli[Seq/Model] Do not enumerate elements of constants...
2022-02-28 Gereon KremerRefactor rewriting of arithmetic atoms (#8175)
2022-02-28 Andrew ReynoldsFix special casing for PI in model value (#8189)
2022-02-28 Andrew ReynoldsPreserve model values for exact sine points (#8188)
2022-02-28 Andrew ReynoldsTrack names for witness terms in model (#8184)
2022-02-28 Andrew ReynoldsAdd two reduction schemas for sin terms (#8171)
2022-02-28 Andres NoetzliRemove broken/unused `--mmap` option (#8178)
2022-02-28 Gereon KremerAdd scripts to build python wheels (#8132)
2022-02-28 Gereon KremerRefactor rewriting of arithmetic leafs (#8177)
2022-02-28 Gereon KremerRefactor rewriting of arithmetic addition (#8180)
2022-02-25 Andrew ReynoldsConsider PI to be a model value (#8176)
2022-02-25 Andrew ReynoldsSyntax fixes for LFSC signature (#8172)
2022-02-25 Gereon KremerAdd utilities to rewrite atoms for the arithmetic rewri...
2022-02-25 Gereon KremerRefactor rewriting of arithmetic negation and subtracti...
2022-02-25 Gereon KremerSlightly refactor arithmetic rewriting for extended...
2022-02-25 Andrew ReynoldsFix non-termination in quantifiers rewriter (#8165)
2022-02-25 Andrew ReynoldsSimplify and fix how purified terms are managed in...
2022-02-25 Andrew ReynoldsFix dropped bounds on PI (#8164)
2022-02-25 Andrew ReynoldsRemove approximations infrastructure from model (#8166)
2022-02-25 Andrew ReynoldsRemove spurious assertion involving constants for argum...
2022-02-25 Andrew ReynoldsMake quantifiers terminate if it detects a (duplicate...
2022-02-25 Andrew ReynoldsAdd regression for fixed transcendental regression...
2022-02-25 Andrew ReynoldsConsolidate extended rewrite preprocessing modes (...
2022-02-25 Andres Noetzli[Python API] Add support for blocking models (#8134)
2022-02-24 Andrew ReynoldsEnsure variables are constrained in model when equal...
2022-02-24 Andrew ReynoldsMake model builder robust to multiple value-like terms...
2022-02-24 Gereon KremerImprove error message for missing options include ...
2022-02-24 Andrew ReynoldsMake sine solver sound with respect to region boundarie...
2022-02-24 Andrew ReynoldsCheck for free variables in several SolverEngine calls...
2022-02-24 Gereon KremerGet rid of some static objects in arithmetic theory...
2022-02-24 Andrew ReynoldsMake uninterpreted sort owner non-static (#8144)
2022-02-24 Andrew ReynoldsAdd regression for some fixed array issues (#8145)
2022-02-23 Gereon KremerAdd two regressions related to RAN models (#8142)
2022-02-23 Andrew ReynoldsAllow elimination of unevaluated terms by default ...
2022-02-23 Andrew ReynoldsFurther relax what is considered a value in the model...
2022-02-23 Andrew ReynoldsDo not insist that entries for UF are constant in FMF...
2022-02-23 Andrew ReynoldsEliminate match from LFSC proofs (#8090)
2022-02-23 Gereon KremerRemove long obsolete unsafe interrupt exception (#8139)
2022-02-23 Andrew ReynoldsOption exception when incompatible with proofs (#8064)
2022-02-23 Gereon KremerFix creation of RAN from non-dyadic rational (#8138)
2022-02-23 Gereon KremerFix icp candidate parsing (#8137)
2022-02-23 Andrew ReynoldsProperly sanatize user names in LFSC (#8080)
2022-02-23 Andres Noetzli[Rewriter] Do not attempt to rewrite constants (#8061)
2022-02-23 Gereon KremerFix pruning of covering intervals in proofs (#8084)
2022-02-23 Gereon KremerRefactor multiplication in arithmetic rewriter (#7965)
2022-02-23 Andrew ReynoldsFix issue in datatypes care graph computation involving...
2022-02-22 Andrew ReynoldsSupport some cases of isConst for regular expressions...
2022-02-22 Andrew ReynoldsRemove refineConflicts option (#8129)
2022-02-22 Andrew ReynoldsChange inference scheme in transcendentals to rewrite...
2022-02-22 Andrew ReynoldsRelax what is generated in the model from NL (#8113)
2022-02-22 vinciusb[proofs] [dot] Enable DAG and tree printing with dot...
2022-02-21 Andrew ReynoldsFixes and additions for LFSC signatures (#8120)
next