projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Improve error for check theory assertions with model (#7679)
[cvc5.git] / test /
2021-11-22 Andrew ReynoldsFix const RE test for internal regexp rv kind (#7678) tree | commitdiff
2021-11-20 yoni206bv2int module: translation of more cases (#7653) tree | commitdiff
2021-11-19 Mathias PreinerAllow negative denominator for CLN Rationals constructe... tree | commitdiff
2021-11-18 Aina Niemetzapi: Fix kind documentation for BAG_MAKE. (#7663) tree | commitdiff
2021-11-17 Gereon Kremermake default and modes strings instead of enum values... tree | commitdiff
2021-11-17 Andres NoetzliFix binding of quoted symbols in `define-fun` (#7655) tree | commitdiff
2021-11-16 yoni206Translating API tests to Python — part 1 (#7597) tree | commitdiff
2021-11-16 Haniel Barbosa[proofs] Make sure --proof-check=... is no-op when... tree | commitdiff
2021-11-15 Aina Niemetzapi: Rename BOUND_VAR_LIST to VARIABLE_LIST. (#7632) tree | commitdiff
2021-11-13 Andres NoetzliSkip `str.code` inferences for sequence eqcs (#7644) tree | commitdiff
2021-11-13 mudathirmahgoubFix type error for rewriting bag.map bag.union_disjoint... tree | commitdiff
2021-11-13 mudathirmahgoubAdd operator set.map to theory of sets (#7641) tree | commitdiff
2021-11-12 mudathirmahgoubbags: Rename kinds with a more consistent naming scheme... tree | commitdiff
2021-11-12 Andres NoetzliRemove `ConstantMap<Rational>` (#7635) tree | commitdiff
2021-11-11 Abdalrhman MohamedAdd an API method to get the raw name of a term. (... tree | commitdiff
2021-11-11 Andrew ReynoldsAdd lazy approach for handling lambdas in the HO extens... tree | commitdiff
2021-11-10 Aina Niemetzapi: Add Solver::mkRegexpAll(). (#7614) 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-10 Aina NiemetzReorganize test/unit/api directory. (#7612) tree | commitdiff
2021-11-09 Andrew ReynoldsOnly eliminate lambdas in higher-order elimination... tree | commitdiff
2021-11-09 Aina NiemetzClean up ctest configuration and CI test configuration... tree | commitdiff
2021-11-09 Haniel Barbosa[proofs] Generalize trivial cycle detection in LazyCDPr... tree | commitdiff
2021-11-09 Aina Niemetzregex: Rename REGEXP_EMPTY and REGEXP_SIGMA to match... tree | commitdiff
2021-11-09 Gereon KremerRemove `CVC5Message` (#7610) 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 Gereon KremerIntegrate java unit tests into ctest (#7593) 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 Gereon KremerRemove `Notice()` in favor of new `verbose()` (#7588) 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
2021-11-05 Haniel Barbosa[proofs] Fix open sat proof (#7509) tree | commitdiff
2021-11-05 Andrew ReynoldsEliminate a level of nesting of traversals in theory... tree | commitdiff
2021-11-05 Gereon KremerRemove `Chat()` in favor of new `verbose()` (#7586) tree | commitdiff
2021-11-05 Andres Noetzli[FP] Do not assert that model has shared term (#7585) tree | commitdiff
2021-11-05 Gereon KremerRemove quadratic solving in NlModel (#7542) tree | commitdiff
2021-11-04 Andrew ReynoldsAdd -o sygus-grammar to print auto-generated SyGuS... tree | commitdiff
2021-11-04 Andrew ReynoldsImprove defaults for sygus default grammars (#7553) tree | commitdiff
2021-11-04 Andrew ReynoldsReplace the old dump infrastructure (#7572) tree | commitdiff
2021-11-04 Gereon KremerStart refactoring of `-o` and `-v` (#7449) tree | commitdiff
2021-11-04 Gereon KremerRefactor cmake to build either static or shared (#7534) tree | commitdiff
2021-11-04 Gereon KremerEnable CDCAC solver for selected quantified logics... tree | commitdiff
2021-11-03 Aina Niemetzapi: Rename some separation logic functions for consist... tree | commitdiff
2021-11-03 Aina NiemetzAdd unit test to cover previous failure with second... tree | commitdiff
2021-11-03 mudathirmahgoubEnable CI for Junit tests (#7436) tree | commitdiff
2021-11-03 Andrew ReynoldsRefactor skolem construction (#7561) tree | commitdiff
2021-11-03 Andrew ReynoldsFormalize more string skolems (#7554) tree | commitdiff
2021-11-03 Andrew ReynoldsFix preregistration for floating point theory (#7558) tree | commitdiff
2021-11-02 Andrew ReynoldsImprove syntax for fmf cardinality constraints (#7556) tree | commitdiff
2021-11-02 Andrew ReynoldsMake quant elimination robust to presence of other... tree | commitdiff
2021-11-01 Andrew ReynoldsWeaken assertion in CEGQI (#7548) tree | commitdiff
2021-11-01 Mathias Preinerbv: Remove layered solver. (#7455) tree | commitdiff
2021-11-01 Andrew ReynoldsFix upwards closure for relations (#7515) tree | commitdiff
2021-11-01 Gereon KremerRefactor DidYouMean (#7535) tree | commitdiff
2021-10-31 mudathirmahgoubFix soundess issue for bags with negative multiplicity... tree | commitdiff
2021-10-31 mudathirmahgoubRemove assertSkeleton for bag elements during model... tree | commitdiff
2021-10-29 Gereon KremerFix proof of nl lemma for a corner case (#7530) tree | commitdiff
2021-10-29 Andrew ReynoldsFix model construction for higher order involving irrel... tree | commitdiff
2021-10-29 Andrew ReynoldsAdd PfRule ARITH_POLY_NORM (#7501) tree | commitdiff
2021-10-28 Gereon KremerFix proof for xor in circuit propagator (#7525) tree | commitdiff
2021-10-28 Haniel Barbosa[proofs] Fix assertion in EqProof conversion (#7522) tree | commitdiff
2021-10-28 Andrew V. JonesAdd support for checking if a `-Wno` flag exists before... tree | commitdiff
2021-10-28 Abdalrhman MohamedAdd a `define-fun` command for each `:named` term.... tree | commitdiff
2021-10-28 Abdalrhman MohamedFix `(set-info <sexpr>)` parsing and printing bugs... tree | commitdiff
2021-10-27 Andrew ReynoldsAdd missing API checks to getValue (#7475) tree | commitdiff
2021-10-27 Andres Noetzli[Regression Script] Fix use of undefined variables... tree | commitdiff
2021-10-27 Andres NoetzliRequire ITE branches to be first class types (#7508) tree | commitdiff
2021-10-27 Andrew ReynoldsFix care graph computation for higher-order (#7474) tree | commitdiff
2021-10-27 Andrew ReynoldsFix model unsoundness for relation join (#7511) tree | commitdiff
2021-10-27 Andrew ReynoldsAvoid non-terminating check with assumptions in strings... tree | commitdiff
2021-10-27 Andrew ReynoldsDeterministic variables for RE elim (#7489) tree | commitdiff
2021-10-27 Gereon KremerMake --version exit (#7506) tree | commitdiff
2021-10-26 Haniel Barbosa[proofs] Fix singleton check in MACRO_RES post-processi... tree | commitdiff
2021-10-26 Haniel Barbosa[proofs] Reset local var in SatProofManager since incre... tree | commitdiff
2021-10-26 Andrew ReynoldsDisable automatic symmetry in proofs of theory explanat... tree | commitdiff
2021-10-26 Haniel Barbosa[proofs] Fix and simplify CHAIN_RESOLUTION checker... tree | commitdiff
2021-10-26 Andrew ReynoldsAdd regressions for fixed issues (#7495) tree | commitdiff
2021-10-26 Andrew ReynoldsDisable sygus-inst when incremental (#7485) tree | commitdiff
2021-10-25 Andrew ReynoldsAdd new method for enumerating unsat queries with SyGuS... tree | commitdiff
2021-10-25 Andrew ReynoldsJava and python unit tests for mkCardinalityConstraint... tree | commitdiff
2021-10-25 Andrew ReynoldsFix more missing uses of CDProof::isSame (#7491) tree | commitdiff
2021-10-25 Andrew ReynoldsFix support for global declarations (#7480) tree | commitdiff
2021-10-25 mudathirmahgoubAdd inference for count map (#7264) tree | commitdiff
2021-10-25 Andrew ReynoldsReenable proofs on some regressions (#7483) tree | commitdiff
2021-10-25 Andres Noetzli[Regression Script] Support older Python versions ... tree | commitdiff
2021-10-24 Andrew ReynoldsAdd new eager conflict detection in strings for integer... tree | commitdiff
2021-10-22 Andrew ReynoldsAdd requires libpoly to regression (#7467) tree | commitdiff
2021-10-22 mudathirmahgoubRefactor java package name from cvc5 to io.github.cvc5... tree | commitdiff
2021-10-22 Haniel Barbosa[proof] Fixing CHAIN_RESOLUTION checker (#7465) tree | commitdiff
2021-10-22 Gereon KremerFix out-of-sync pruning in CDCAC proofs (#7470) tree | commitdiff
2021-10-22 Gereon KremerFix another double negation proof issue (#7468) tree | commitdiff
2021-10-22 Andrew ReynoldsAdd more abduction regressions (#7461) tree | commitdiff
2021-10-22 Gereon KremerMake CAD proofs user context dependent (#7466) tree | commitdiff
2021-10-22 yoni206Making `IntBlaster` inherit from `EnvObj` (#7431) tree | commitdiff
2021-10-22 Andrew ReynoldsDo not use global proxy variable attribute for strings... tree | commitdiff
2021-10-22 mudathirmahgoubAdd missing methods to Solver.java (#7299) tree | commitdiff
next