projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Add miscellaneous missing theory definitions for LFSC (#8039)
[cvc5.git] / test / regress /
2022-02-02 Andrew ReynoldsFix invalid rewrite involving iand (#8026) tree | commitdiff
2022-02-02 Andrew ReynoldsFix printing of re.loop as an operator in LFSC (#8029) tree | commitdiff
2022-02-02 Andrew ReynoldsMake LFSC side condition for concat unify robust to... tree | commitdiff
2022-02-02 Andrew ReynoldsAdd missing null terminators for regexp (#8027) tree | commitdiff
2022-02-02 Gereon KremerAdd additional check to avoid cyclic substitution ... tree | commitdiff
2022-02-02 Andrew ReynoldsExtend proof step buffer to optionally ensure unique... tree | commitdiff
2022-02-01 mudathirmahgoubAdd bag.filter operator (#8006) tree | commitdiff
2022-01-31 Andres NoetzliFix memory leak in quantifier info (#8005) tree | commitdiff
2022-01-26 mudathirmahgoubAdd Card solver to bags (#7986) tree | commitdiff
2022-01-25 Andrew ReynoldsAdd output -o post-asserts (#7987) tree | commitdiff
2022-01-25 Andres NoetzliSend `nth(unit(...), ...)` terms to array solver (... tree | commitdiff
2022-01-25 Andres Noetzli[Strings] Avoid trivial explanation (#7982) tree | commitdiff
2022-01-24 Gereon KremerDisable regression if poly is not available (#7981) tree | commitdiff
2022-01-24 Gereon KremerUse proper RAN nodes for nl model (#7939) tree | commitdiff
2022-01-24 Abdalrhman MohamedEnable dump tester. (#7884) tree | commitdiff
2022-01-21 Andrew ReynoldsFix trivial explantions in sequences array solver ... tree | commitdiff
2022-01-20 Andres NoetzliFix `Nth-Update` rule, add `Update-Bound` rule (#7968) tree | commitdiff
2022-01-20 Andrew ReynoldsFix proofs for trivial cases of datatypes tester merge... tree | commitdiff
2022-01-19 Gereon KremerFix a subtle issue with double negations in coverings... tree | commitdiff
2022-01-18 Andres Noetzli[API] Add missing arity check (#7905) tree | commitdiff
2022-01-17 Andrew ReynoldsRefactor options related to rewriting and symmetry... tree | commitdiff
2022-01-17 Andres Noetzli[Strings] Fix rewriter for `re.loop` (#7956) tree | commitdiff
2022-01-15 Andrew ReynoldsAdd inverse inference for update-over-concat (#7954) tree | commitdiff
2022-01-14 Andrew ReynoldsImprove names for sygus enumeration option (#7945) tree | commitdiff
2022-01-14 Andrew ReynoldsClean enumerative instantiation options (#7947) tree | commitdiff
2022-01-14 Andrew ReynoldsImplement -o subs to show learned top-level substitutio... tree | commitdiff
2022-01-14 Andrew ReynoldsFix learned rewrite pass for non-real equalties (#7936) tree | commitdiff
2022-01-14 Andrew ReynoldsWeaken assertion in relevance manager (#7943) tree | commitdiff
2022-01-13 Andres NoetzliUnify abstract values and uninterpreted constants ... tree | commitdiff
2022-01-12 Andrew ReynoldsAdd -o learned-lits to output learned literals (#7934) tree | commitdiff
2022-01-12 Andrew ReynoldsEnsure configuration of shared selectors is consistent... tree | commitdiff
2022-01-12 Andrew ReynoldsAlways use partial function for sqrt (#7926) tree | commitdiff
2022-01-12 Andrew ReynoldsEliminate use of subtyping from results of quantifier... tree | commitdiff
2022-01-11 Abdalrhman MohamedDisable filtering of shapes in sygus-rcons pool. (... tree | commitdiff
2022-01-11 Andrew ReynoldsTighten policy for unsat cores in sygus core connective... tree | commitdiff
2022-01-11 Abdalrhman MohamedCheck the synthesized funs of `check-synth-next`. ... tree | commitdiff
2022-01-10 Aina Niemetzapi: Remove Sort::isComparableTo(). (#7903) tree | commitdiff
2022-01-07 Andrew ReynoldsFix eager string preprocessing in incremental mode... tree | commitdiff
2022-01-07 Andrew ReynoldsAdd regressions for array sequence solver (#7874) tree | commitdiff
2022-01-07 Andres Noetzli[Regressions] Add directive for disabling testers ... tree | commitdiff
2022-01-06 Andrew ReynoldsMake alpha equivalence user context dependent (#7889) tree | commitdiff
2022-01-06 Gereon KremerImprove theory combination in the presence of real... tree | commitdiff
2022-01-06 Andrew ReynoldsFix non-idempotent rewrite in arrays (#7887) tree | commitdiff
2022-01-04 Andrew ReynoldsFix int blaster (#7856) tree | commitdiff
2022-01-04 mudathirmahgoubAdd bag.member operator to theory of bags (#7857) tree | commitdiff
2022-01-04 mudathirmahgoubRefactor bag solver (#7770) tree | commitdiff
2022-01-03 Andres NoetzliExecute `(reset)` command in parse-only mode (#7862) tree | commitdiff
2021-12-23 Andres Noetzli[Regressions] Support more complex scrubbers (#7819) tree | commitdiff
2021-12-22 Andrew ReynoldsAdd support for incremental + interpolants (#7853) tree | commitdiff
2021-12-21 Andrew ReynoldsSupport get-abduct-next (#7850) tree | commitdiff
2021-12-20 Andrew ReynoldsAllow SyGuS subsolver to be reused in incremental mode... tree | commitdiff
2021-12-17 Andres NoetzliFix rewrite for `str.update(str.rev(s), n, t))` (#7838) tree | commitdiff
2021-12-17 Mathias PreinerDisable unsat cores for quaternion_ds1_symm_0428.fof... tree | commitdiff
2021-12-16 Andrew ReynoldsFix get-model when sort constructors are present (... tree | commitdiff
2021-12-16 Andrew ReynoldsMinor fix for print benchmark. (#7821) tree | commitdiff
2021-12-16 yoni206bv-to-int: use pow2 operator (#7812) tree | commitdiff
2021-12-16 yoni206int-to-bv: fail if one of the arguments has type real... tree | commitdiff
2021-12-16 mudathirmahgoubAdd regression bags-of-bags-subtypes.smt2 (#7814) tree | commitdiff
2021-12-14 mudathirmahgoubFix cvc5-projects issue 358 (#7804) tree | commitdiff
2021-12-14 Abdalrhman MohamedAdd a random Sygus enumerator. (#7782) tree | commitdiff
2021-12-13 mudathirmahgoubA more efficient implementation for bag.card operator... tree | commitdiff
2021-12-13 Gereon KremerImprove nonlinear solver (#7787) tree | commitdiff
2021-12-13 yoni206Integrate new int-blaster (#7781) tree | commitdiff
2021-12-13 mudathirmahgoubFix cvc5-projects issues #358 and #375 (#7743) tree | commitdiff
2021-12-10 Abdalrhman MohamedMute `define-fun` command generated for named terms... tree | commitdiff
2021-12-09 Andrew ReynoldsConsider polarity in relevance manager (#7768) tree | commitdiff
2021-12-08 Andrew ReynoldsMake several regressions faster (#7769) tree | commitdiff
2021-12-08 Andrew ReynoldsFix type rule for datatype updater for parametric sorts... tree | commitdiff
2021-12-07 Andrew ReynoldsAllow sygus in incremental mode (#7756) tree | commitdiff
2021-12-07 Andrew ReynoldsMake data structures in relevance manager SAT-context... tree | commitdiff
2021-12-06 Gereon KremerDisable option regression for competition build (#7751) tree | commitdiff
2021-12-06 Andrew ReynoldsAdd regressions for fixed projects issues (#7739) tree | commitdiff
2021-12-02 mudathirmahgoubadd bag.fold operator (#7718) tree | commitdiff
2021-12-02 Gereon KremerAdd unit tests for api::Solver::setOption() (#7708) tree | commitdiff
2021-12-01 Andrew ReynoldsRemove spurious assertion in parser (#7713) tree | commitdiff
2021-11-30 Mathias PreinerChange CVC4 urls to cvc5. (#7706) tree | commitdiff
2021-11-30 Andrew ReynoldsAdd rewrite for is_int pi (#7711) tree | commitdiff
2021-11-30 Andrew ReynoldsProper check for first-class types in datatype subfield... tree | commitdiff
2021-11-30 Gereon KremerRemove now unused dumping infrastructure (#7703) tree | commitdiff
2021-11-25 Mathias PreinerGuard regression tests that require libpoly to pass... tree | commitdiff
2021-11-24 Andrew ReynoldsFix potential for cycles in trust substitutions (#7687) tree | commitdiff
2021-11-23 mudathirmahgoubAdd rewrite rule for bag.card operator using bag.map... tree | commitdiff
2021-11-22 Andrew ReynoldsFix const RE test for internal regexp rv kind (#7678) tree | commitdiff
2021-11-17 Andres NoetzliFix binding of quoted symbols in `define-fun` (#7655) tree | commitdiff
2021-11-16 Haniel Barbosa[proofs] Make sure --proof-check=... is no-op when... tree | commitdiff
2021-11-13 Andres NoetzliSkip `str.code` inferences for sequence eqcs (#7644) tree | commitdiff
2021-11-12 mudathirmahgoubbags: Rename kinds with a more consistent naming scheme... tree | commitdiff
2021-11-11 Andrew ReynoldsAdd lazy approach for handling lambdas in the HO extens... tree | commitdiff
2021-11-10 mudathirmahgoubFix soundness issue of missing premises for count bag... tree | commitdiff
2021-11-10 Andrew ReynoldsFix parsing array constants (#7617) tree | commitdiff
2021-11-10 Aina Niemetzsets: Rename set.intersection to set.inter. (#7622) tree | commitdiff
2021-11-09 Andrew ReynoldsOnly eliminate lambdas in higher-order elimination... tree | commitdiff
2021-11-09 Haniel Barbosa[proofs] Generalize trivial cycle detection in LazyCDPr... tree | commitdiff
2021-11-09 Gereon KremerRemove command-verbosity option (#7581) tree | commitdiff
2021-11-08 mudathirmahgoubexpand bag.choose operator (#7481) tree | commitdiff
2021-11-08 Aina Niemetzsets: Rename kinds with a more consistent naming scheme... tree | commitdiff
2021-11-06 Abdalrhman MohamedPrint `unsupported` for unrecognized flags. (#7384) tree | commitdiff
2021-11-06 Andrew ReynoldsDo not use extended rewrites on recursive function... tree | commitdiff
2021-11-06 Mathias PreinerDisable regress2 test. (#7591) tree | commitdiff
2021-11-05 Andrew ReynoldsFix exclusion criteria for codatatype model values... tree | commitdiff
next