projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Remove unecessary separation logic options (#8269)
[cvc5.git] / test /
2022-03-15 Andrew ReynoldsFix to consider leafs of theory sets to be variables... tree | commitdiff
2022-03-15 Andrew ReynoldsSimplify reductions for set and bag choose (#8304) tree | commitdiff
2022-03-15 Aina NiemetzRename TO_FP operator kinds. (#8285) tree | commitdiff
2022-03-14 Andrew ReynoldsFixes for skolem definition management (#8301) tree | commitdiff
2022-03-14 Andrew ReynoldsRemove unecessary methods from the API (#8260) tree | commitdiff
2022-03-14 Andrew ReynoldsAdd rewrite for allchar beneath union + star (#8299) tree | commitdiff
2022-03-14 Andrew ReynoldsRun preprocess rewrite on equalities until fixed point... tree | commitdiff
2022-03-12 Andrew ReynoldsIntroduce new splitting inference in sets + cardinality... tree | commitdiff
2022-03-12 Mathias Preinercmake: Do not require googletest if unit tests are... tree | commitdiff
2022-03-12 Andrew ReynoldsAlways ensure literal when requiring phase via inferenc... tree | commitdiff
2022-03-11 Andres Noetzli[API/Python] Add support for `Solver::getModel()` ... tree | commitdiff
2022-03-11 Andrew ReynoldsRemove old decision justification heurstic (#8275) tree | commitdiff
2022-03-11 Andrew ReynoldsUpdate abduction and interpolation API to not use pass... tree | commitdiff
2022-03-11 Andrew ReynoldsConsider APPLY_CONSTRUCTOR applied to values to be... tree | commitdiff
2022-03-11 Andrew ReynoldsFix reduction for arc trig functions (#8289) tree | commitdiff
2022-03-10 Andrew ReynoldsFix theoryOf call in get equality status (#8279) tree | commitdiff
2022-03-10 Andrew ReynoldsEliminate unecessary datatype options (#8280) tree | commitdiff
2022-03-10 mudathirmahgoubFix cvc5-projects issue 475 (#8278) tree | commitdiff
2022-03-10 Andrew ReynoldsAdd output -o pre-asserts (#8270) tree | commitdiff
2022-03-10 Andrew ReynoldsDisable timing out regressions (#8273) tree | commitdiff
2022-03-10 Mathias PreinerFix regression errors for arm64 nightlies. (#8268) tree | commitdiff
2022-03-09 Gereon KremerRename expert statistics to internal, add documentation... tree | commitdiff
2022-03-09 Gereon KremerClear obsolete pending lemmas in arithmetic (#8236) tree | commitdiff
2022-03-09 Andrew ReynoldsAdd regression for fixed issue 6700 (#8265) tree | commitdiff
2022-03-08 Andrew ReynoldsDo not expand APPLY_SELECTOR (#8174) tree | commitdiff
2022-03-08 Andres Noetzli[API/Python] Add support for `Solver::getProof()` ... tree | commitdiff
2022-03-08 Andrew ReynoldsGuard another case of non-termination in quantifiers... tree | commitdiff
2022-03-08 Gereon KremerMake one CI job not use libpoly (#8261) tree | commitdiff
2022-03-08 Andrew ReynoldsEliminate shadowing in the quantifiers rewriter (#8244) tree | commitdiff
2022-03-08 Andrew ReynoldsAdd unit for fixed project issue (#8253) tree | commitdiff
2022-03-07 Andres NoetzliUpdate documentation of `Solver::getUnsatCore()` (... tree | commitdiff
2022-03-07 Gereon KremerTry harder to show that a RAN is rational (#8230) tree | commitdiff
2022-03-06 Andres NoetzliDisallow models with `--arrays-weak-equiv` (#8217) tree | commitdiff
2022-03-05 Andrew ReynoldsUnit tests for fixed projects issues (#8229) tree | commitdiff
2022-03-05 Andrew ReynoldsMake seq.unit robust wrt subtyping (#8209) tree | commitdiff
2022-03-05 Gereon KremerAdd regressions for fixed issue (#8237) tree | commitdiff
2022-03-05 Andrew ReynoldsEnable NL tangent planes by default (#8233) tree | commitdiff
2022-03-04 Gereon KremerAdd unit test for fixed issue (#8235) tree | commitdiff
2022-03-04 Gereon KremerRemove spurious assertion in linear solver (#8231) tree | commitdiff
2022-03-04 Gereon KremerGuard recursion into terms during substitution in arith... tree | commitdiff
2022-03-04 Andrew ReynoldsFix rewrite rule synthesis for 0-ary operators (#8221) tree | commitdiff
2022-03-04 Andrew ReynoldsLogic exception when using solution filtering for non... tree | commitdiff
2022-03-04 Andrew ReynoldsAdd regressions for fixed projects issues (#8228) tree | commitdiff
2022-03-04 Andrew ReynoldsAdd support for get learned literals in the API (#8099) tree | commitdiff
2022-03-03 Andrew ReynoldsThrow logic exception if a transcendental function... tree | commitdiff
2022-03-03 Andrew ReynoldsAdd regression for fixed issue (#8213) tree | commitdiff
2022-03-03 Gereon KremerFix rewriting of mixed-integer atoms (#8214) tree | commitdiff
2022-03-02 Andrew ReynoldsFix issue with dropping non-reduced sine terms (#8211) tree | commitdiff
2022-03-02 Andrew ReynoldsFix models involving cardinality of sets of finite... tree | commitdiff
2022-03-02 Andrew ReynoldsAlways purify universe from set minus (#8201) tree | commitdiff
2022-03-02 Andrew ReynoldsEliminate CDHashMap::insertAtContextLevelZero (#8173) tree | commitdiff
2022-03-02 Andrew ReynoldsFix incorrect assertion in prop engine proofs (#8204) tree | commitdiff
2022-03-02 Andrew ReynoldsClean usage of options in regressions (#8190) tree | commitdiff
2022-03-02 Andrew ReynoldsImprove error message when not using strings-exp (... tree | commitdiff
2022-03-02 Andrew ReynoldsMake blockModelValues robust to non-closed enumerable... tree | commitdiff
2022-03-02 Andrew ReynoldsAdd regressions for fixed issues (#8202) tree | commitdiff
2022-03-02 Gereon KremerPrune spurious roots in lazard evaluation of coverings... tree | commitdiff
2022-03-01 Andrew ReynoldsFix issue involving dropped purification lemmas for... tree | commitdiff
2022-03-01 Andrew ReynoldsDisable regression (#8191) tree | commitdiff
2022-03-01 Andres Noetzli[BV] Fix rewriter policy for `bvneg` (#8196) tree | commitdiff
2022-03-01 Gereon KremerRename cad to coverings (#8187) tree | commitdiff
2022-02-28 Andres Noetzli[Seq/Model] Do not enumerate elements of constants... tree | commitdiff
2022-02-28 Andrew ReynoldsFix special casing for PI in model value (#8189) tree | commitdiff
2022-02-28 Andrew ReynoldsPreserve model values for exact sine points (#8188) tree | commitdiff
2022-02-28 Andrew ReynoldsTrack names for witness terms in model (#8184) tree | commitdiff
2022-02-28 Andrew ReynoldsAdd two reduction schemas for sin terms (#8171) tree | commitdiff
2022-02-28 Andres NoetzliRemove broken/unused `--mmap` option (#8178) tree | commitdiff
2022-02-25 Andrew ReynoldsConsider PI to be a model value (#8176) tree | commitdiff
2022-02-25 Andrew ReynoldsFix non-termination in quantifiers rewriter (#8165) tree | commitdiff
2022-02-25 Andrew ReynoldsSimplify and fix how purified terms are managed in... tree | commitdiff
2022-02-25 Andrew ReynoldsFix dropped bounds on PI (#8164) tree | commitdiff
2022-02-25 Andrew ReynoldsRemove approximations infrastructure from model (#8166) tree | commitdiff
2022-02-25 Andrew ReynoldsRemove spurious assertion involving constants for argum... tree | commitdiff
2022-02-25 Andrew ReynoldsMake quantifiers terminate if it detects a (duplicate... tree | commitdiff
2022-02-25 Andrew ReynoldsAdd regression for fixed transcendental regression... tree | commitdiff
2022-02-25 Andrew ReynoldsConsolidate extended rewrite preprocessing modes (... tree | commitdiff
2022-02-25 Andres Noetzli[Python API] Add support for blocking models (#8134) tree | commitdiff
2022-02-24 Andrew ReynoldsEnsure variables are constrained in model when equal... tree | commitdiff
2022-02-24 Andrew ReynoldsMake model builder robust to multiple value-like terms... tree | commitdiff
2022-02-24 Andrew ReynoldsMake sine solver sound with respect to region boundarie... tree | commitdiff
2022-02-24 Andrew ReynoldsCheck for free variables in several SolverEngine calls... tree | commitdiff
2022-02-24 Andrew ReynoldsMake uninterpreted sort owner non-static (#8144) tree | commitdiff
2022-02-24 Andrew ReynoldsAdd regression for some fixed array issues (#8145) tree | commitdiff
2022-02-23 Gereon KremerAdd two regressions related to RAN models (#8142) tree | commitdiff
2022-02-23 Andrew ReynoldsAllow elimination of unevaluated terms by default ... tree | commitdiff
2022-02-23 Andrew ReynoldsFurther relax what is considered a value in the model... tree | commitdiff
2022-02-23 Andrew ReynoldsDo not insist that entries for UF are constant in FMF... tree | commitdiff
2022-02-23 Gereon KremerRemove long obsolete unsafe interrupt exception (#8139) tree | commitdiff
2022-02-23 Andrew ReynoldsOption exception when incompatible with proofs (#8064) tree | commitdiff
2022-02-23 Gereon KremerFix icp candidate parsing (#8137) tree | commitdiff
2022-02-23 Andrew ReynoldsProperly sanatize user names in LFSC (#8080) tree | commitdiff
2022-02-23 Gereon KremerFix pruning of covering intervals in proofs (#8084) tree | commitdiff
2022-02-23 Andrew ReynoldsFix issue in datatypes care graph computation involving... tree | commitdiff
2022-02-22 Andrew ReynoldsRelax what is generated in the model from NL (#8113) tree | commitdiff
2022-02-18 Andrew ReynoldsAdd unit test for fixed issue with get-difficulty ... tree | commitdiff
2022-02-18 Andrew ReynoldsThrow option exceptions when combining input conversion... tree | commitdiff
2022-02-18 Andrew ReynoldsAdd well formed term check to solver engine (#8056) tree | commitdiff
2022-02-18 Andrew ReynoldsMake spurious assertion into warning (#8051) tree | commitdiff
2022-02-17 Andrew ReynoldsMissing ids for arith conflicts (#8108) tree | commitdiff
2022-02-16 Andrew ReynoldsOnly consider relevant terms in the array-inspired... tree | commitdiff
next