projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2021-10-28 Andrew V. JonesAdd support for checking if a `-Wno` flag exists before... commit | commitdiff | tree
2021-10-28 Abdalrhman... Add a `define-fun` command for each `:named` term.... commit | commitdiff | tree
2021-10-28 Andrew ReynoldsProperly guard proof construction for STRINGS_EXTF_EQ_R... commit | commitdiff | tree
2021-10-28 Andrew ReynoldsLFSC signature for linear arithmetic (#7445) commit | commitdiff | tree
2021-10-28 Andrew ReynoldsLFSC signature for CNF (#7444) commit | commitdiff | tree
2021-10-28 Andrew ReynoldsLFSC signature for Booleans (#7443) commit | commitdiff | tree
2021-10-28 Andrew ReynoldsLFSC signature for equality (#7442) commit | commitdiff | tree
2021-10-28 Abdalrhman... Fix `(set-info <sexpr>)` parsing and printing bugs... commit | commitdiff | tree
2021-10-28 Gereon KremerRemove separate cpp docs for UnknownExplanation (#7516) commit | commitdiff | tree
2021-10-28 Gereon KremerBuild shared and static in CI (#7472) commit | commitdiff | tree
2021-10-27 Andrew ReynoldsAdd missing API checks to getValue (#7475) commit | commitdiff | tree
2021-10-27 Gereon KremerAdd comments for arith type rules. (#7488) commit | commitdiff | tree
2021-10-27 Gereon KremerAdd documentation on output tags (#7499) commit | commitdiff | tree
2021-10-27 Andres Noetzli[Regression Script] Fix use of undefined variables... commit | commitdiff | tree
2021-10-27 Gereon KremerFix patching for poly on windows (#7513) commit | commitdiff | tree
2021-10-27 Andres NoetzliRequire ITE branches to be first class types (#7508) commit | commitdiff | tree
2021-10-27 Andrew ReynoldsFix care graph computation for higher-order (#7474) commit | commitdiff | tree
2021-10-27 Andrew ReynoldsFix model unsoundness for relation join (#7511) commit | commitdiff | tree
2021-10-27 yoni206Python api documentation for sorts (#7440) commit | commitdiff | tree
2021-10-27 Andrew ReynoldsAvoid non-terminating check with assumptions in strings... commit | commitdiff | tree
2021-10-27 Andrew ReynoldsDeterministic variables for RE elim (#7489) commit | commitdiff | tree
2021-10-27 mudathirmahgoubFix mac compile errors in sort.cpp (#7507) commit | commitdiff | tree
2021-10-27 Gereon KremerMake --version exit (#7506) commit | commitdiff | tree
2021-10-27 Gereon KremerFix libpoly build on windows (#7502) commit | commitdiff | tree
2021-10-26 Haniel Barbosa[proofs] Fix singleton check in MACRO_RES post-processi... commit | commitdiff | tree
2021-10-26 Haniel Barbosa[proofs] Modularize check for whether a clause is singl... commit | commitdiff | tree
2021-10-26 Haniel Barbosa[proofs] Reset local var in SatProofManager since incre... commit | commitdiff | tree
2021-10-26 Andrew ReynoldsDisable automatic symmetry in proofs of theory explanat... commit | commitdiff | tree
2021-10-26 Haniel Barbosa[proofs] Fix and simplify CHAIN_RESOLUTION checker... commit | commitdiff | tree
2021-10-26 Andrew ReynoldsAdd regressions for fixed issues (#7495) commit | commitdiff | tree
2021-10-26 Andrew ReynoldsDisable sygus-inst when incremental (#7485) commit | commitdiff | tree
2021-10-26 Lachnitt[proofs] Alethe: Translate Block of clause pattern... commit | commitdiff | tree
2021-10-26 Lachnitt[proofs] Alethe: Translate AND_INTRO rule (#7405) commit | commitdiff | tree
2021-10-26 Lachnitt[proofs] Alethe: Translate AND_ELIM rule (#7404) commit | commitdiff | tree
2021-10-26 Lachnitt[proofs] Alethe: Translate CONTRA rule (#7403) commit | commitdiff | tree
2021-10-26 Gereon KremerUpload docs for tags to docs-releases (#7415) commit | commitdiff | tree
2021-10-26 Gereon KremerFix frequent rebuild of options target (#7450) commit | commitdiff | tree
2021-10-26 Gereon KremerFix Configuration::isStaticBuild (#7456) commit | commitdiff | tree
2021-10-26 Lachnitt[proofs] Alethe: Translate NOT_NOT_ELIM rule (#7402) commit | commitdiff | tree
2021-10-25 Lachnitt[proofs] Alethe: Translate MODUS_PONENS rule (#7401) commit | commitdiff | tree
2021-10-25 Andrew ReynoldsAdd new method for enumerating unsat queries with SyGuS... commit | commitdiff | tree
2021-10-25 Lachnitt[proofs] Alethe: Translate EQ_RESOLVE rule (#7400) commit | commitdiff | tree
2021-10-25 Andrew ReynoldsFix spurious checks to closed proofs (#7484) commit | commitdiff | tree
2021-10-25 Andrew ReynoldsJava and python unit tests for mkCardinalityConstraint... commit | commitdiff | tree
2021-10-25 Andrew ReynoldsFix more missing uses of CDProof::isSame (#7491) commit | commitdiff | tree
2021-10-25 Andrew ReynoldsFix support for global declarations (#7480) commit | commitdiff | tree
2021-10-25 Andrew ReynoldsRemove HOL/fmf bound messages in set defaults (#7487) commit | commitdiff | tree
2021-10-25 mudathirmahgoubAdd inference for count map (#7264) commit | commitdiff | tree
2021-10-25 Andrew ReynoldsReenable proofs on some regressions (#7483) commit | commitdiff | tree
2021-10-25 Lachnitt[proofs] Alethe: Translate SPLIT rule (#7399) commit | commitdiff | tree
2021-10-25 Andres Noetzli[Regression Script] Support older Python versions ... commit | commitdiff | tree
2021-10-24 mudathirmahgoubDelete redundant file option_Info.cpp (#7477) commit | commitdiff | tree
2021-10-24 Andrew ReynoldsAdd new eager conflict detection in strings for integer... commit | commitdiff | tree
2021-10-23 Andrew ReynoldsRemove spurious assertoin (#7458) commit | commitdiff | tree
2021-10-22 Andrew ReynoldsAdd requires libpoly to regression (#7467) commit | commitdiff | tree
2021-10-22 mudathirmahgoubRefactor java package name from cvc5 to io.github.cvc5... commit | commitdiff | tree
2021-10-22 Gereon KremerRemove options::X__name (#7414) commit | commitdiff | tree
2021-10-22 Andrew ReynoldsRemove stale pointer to proof node manager from skolemi... commit | commitdiff | tree
2021-10-22 Haniel Barbosa[proof] Fixing CHAIN_RESOLUTION checker (#7465) commit | commitdiff | tree
2021-10-22 Gereon KremerFix out-of-sync pruning in CDCAC proofs (#7470) commit | commitdiff | tree
2021-10-22 Gereon KremerFix another double negation proof issue (#7468) commit | commitdiff | tree
2021-10-22 Andrew ReynoldsRemove `--uf-ho` option (#7463) commit | commitdiff | tree
2021-10-22 Andrew ReynoldsFix symmetry issue in theory engine conflicts (#7469) commit | commitdiff | tree
2021-10-22 Andrew ReynoldsAdd more abduction regressions (#7461) commit | commitdiff | tree
2021-10-22 Lachnitt[proofs] Alethe: Translate FACTORING rule (#7398) commit | commitdiff | tree
2021-10-22 Lachnitt[proofs] Alethe: Translate CHAIN_RESOLUTION rule (... commit | commitdiff | tree
2021-10-22 Gereon KremerMake CAD proofs user context dependent (#7466) commit | commitdiff | tree
2021-10-22 Andrew ReynoldsRefactor theory inference manager constructor (#7457) commit | commitdiff | tree
2021-10-22 yoni206Making `IntBlaster` inherit from `EnvObj` (#7431) commit | commitdiff | tree
2021-10-22 Andrew ReynoldsDo not use global proxy variable attribute for strings... commit | commitdiff | tree
2021-10-22 Andres NoetzliFix memory management of `ErrorInformation` (#7388) commit | commitdiff | tree
2021-10-22 mudathirmahgoubAdd missing methods to Solver.java (#7299) commit | commitdiff | tree
2021-10-22 Andrew ReynoldsMake expression mining use configurable options and... commit | commitdiff | tree
2021-10-21 Aina Niemetzdocs: Use light gray for background on the right. ... commit | commitdiff | tree
2021-10-21 Gereon KremerAlso fix case of negated ite (#7454) commit | commitdiff | tree
2021-10-21 Gereon KremerFix symmetric proof issue for ITE in circuit propagator... commit | commitdiff | tree
2021-10-21 Andrew ReynoldsSplit utilites from CEGIS core connective module (... commit | commitdiff | tree
2021-10-21 Andres Noetzli[Regression Script] Fix printing of error diff (#7451) commit | commitdiff | tree
2021-10-21 Haniel Barbosa[proofs] Fix open proof in SAT solver due to cycles... commit | commitdiff | tree
2021-10-21 Gereon KremerAdd regression (#7447) commit | commitdiff | tree
2021-10-21 Gereon KremerFix incorrect proof from ITE in circuit propagator... commit | commitdiff | tree
2021-10-21 Andres NoetzliRefactor regressions script (#7249) commit | commitdiff | tree
2021-10-21 Andrew ReynoldsMake cardinality constraint a nullary operator (#7333) commit | commitdiff | tree
2021-10-21 Gereon KremerWorking on windows builds (#7381) commit | commitdiff | tree
2021-10-21 Gereon KremerAdd setup to generate graphs for cmake target dependenc... commit | commitdiff | tree
2021-10-21 Andres NoetzliEnable and fix dump test (#7387) commit | commitdiff | tree
2021-10-21 Gereon KremerFix (#7437) commit | commitdiff | tree
2021-10-20 Andrew ReynoldsEnable some previously failing regressions (#7434) commit | commitdiff | tree
2021-10-20 Gereon KremerFix docs upload (again) (#7435) commit | commitdiff | tree
2021-10-20 Aina Niemetzapi: Add Solver::mkSepEmp(). (#7432) commit | commitdiff | tree
2021-10-20 Aina Niemetzapi: Improve documentation for special cases with nulla... commit | commitdiff | tree
2021-10-20 Andrew ReynoldsMove variadic trie utility to its own file (#7410) commit | commitdiff | tree
2021-10-20 Andrew ReynoldsAdd regressions for fixed issues (#7421) commit | commitdiff | tree
2021-10-20 yoni206Add `isNull` and `isUpdater` to `Sort` class of python... commit | commitdiff | tree
2021-10-20 Andrew ReynoldsThrow exception if checking model with separation logic... commit | commitdiff | tree
2021-10-20 Andrew ReynoldsCheck for higher-order variables in TheoryUF::ppRewrite... commit | commitdiff | tree
2021-10-20 Gereon KremerFix inadvertent failure of workflow step (#7420) commit | commitdiff | tree
2021-10-20 Andrew ReynoldsEliminate last static calls to rewriter from smt layer... commit | commitdiff | tree
2021-10-20 Andrew ReynoldsMake SyGuS solver robust to non-closed enumerable sorts... commit | commitdiff | tree
2021-10-20 Andrew ReynoldsDo not construct instantiation for checking propagating... commit | commitdiff | tree
next