cvc5.git
2021-10-25 Andres Noetzli[Regression Script] Support older Python versions ...
2021-10-24 mudathirmahgoubDelete redundant file option_Info.cpp (#7477)
2021-10-24 Andrew ReynoldsAdd new eager conflict detection in strings for integer...
2021-10-23 Andrew ReynoldsRemove spurious assertoin (#7458)
2021-10-22 Andrew ReynoldsAdd requires libpoly to regression (#7467)
2021-10-22 mudathirmahgoubRefactor java package name from cvc5 to io.github.cvc5...
2021-10-22 Gereon KremerRemove options::X__name (#7414)
2021-10-22 Andrew ReynoldsRemove stale pointer to proof node manager from skolemi...
2021-10-22 Haniel Barbosa[proof] Fixing CHAIN_RESOLUTION checker (#7465)
2021-10-22 Gereon KremerFix out-of-sync pruning in CDCAC proofs (#7470)
2021-10-22 Gereon KremerFix another double negation proof issue (#7468)
2021-10-22 Andrew ReynoldsRemove `--uf-ho` option (#7463)
2021-10-22 Andrew ReynoldsFix symmetry issue in theory engine conflicts (#7469)
2021-10-22 Andrew ReynoldsAdd more abduction regressions (#7461)
2021-10-22 Lachnitt[proofs] Alethe: Translate FACTORING rule (#7398)
2021-10-22 Lachnitt[proofs] Alethe: Translate CHAIN_RESOLUTION rule (...
2021-10-22 Gereon KremerMake CAD proofs user context dependent (#7466)
2021-10-22 Andrew ReynoldsRefactor theory inference manager constructor (#7457)
2021-10-22 yoni206Making `IntBlaster` inherit from `EnvObj` (#7431)
2021-10-22 Andrew ReynoldsDo not use global proxy variable attribute for strings...
2021-10-22 Andres NoetzliFix memory management of `ErrorInformation` (#7388)
2021-10-22 mudathirmahgoubAdd missing methods to Solver.java (#7299)
2021-10-22 Andrew ReynoldsMake expression mining use configurable options and...
2021-10-21 Aina Niemetzdocs: Use light gray for background on the right. ...
2021-10-21 Gereon KremerAlso fix case of negated ite (#7454)
2021-10-21 Gereon KremerFix symmetric proof issue for ITE in circuit propagator...
2021-10-21 Andrew ReynoldsSplit utilites from CEGIS core connective module (...
2021-10-21 Andres Noetzli[Regression Script] Fix printing of error diff (#7451)
2021-10-21 Haniel Barbosa[proofs] Fix open proof in SAT solver due to cycles...
2021-10-21 Gereon KremerAdd regression (#7447)
2021-10-21 Gereon KremerFix incorrect proof from ITE in circuit propagator...
2021-10-21 Andres NoetzliRefactor regressions script (#7249)
2021-10-21 Andrew ReynoldsMake cardinality constraint a nullary operator (#7333)
2021-10-21 Gereon KremerWorking on windows builds (#7381)
2021-10-21 Gereon KremerAdd setup to generate graphs for cmake target dependenc...
2021-10-21 Andres NoetzliEnable and fix dump test (#7387)
2021-10-21 Gereon KremerFix (#7437)
2021-10-20 Andrew ReynoldsEnable some previously failing regressions (#7434)
2021-10-20 Gereon KremerFix docs upload (again) (#7435)
2021-10-20 Aina Niemetzapi: Add Solver::mkSepEmp(). (#7432)
2021-10-20 Aina Niemetzapi: Improve documentation for special cases with nulla...
2021-10-20 Andrew ReynoldsMove variadic trie utility to its own file (#7410)
2021-10-20 Andrew ReynoldsAdd regressions for fixed issues (#7421)
2021-10-20 yoni206Add `isNull` and `isUpdater` to `Sort` class of python...
2021-10-20 Andrew ReynoldsThrow exception if checking model with separation logic...
2021-10-20 Andrew ReynoldsCheck for higher-order variables in TheoryUF::ppRewrite...
2021-10-20 Gereon KremerFix inadvertent failure of workflow step (#7420)
2021-10-20 Andrew ReynoldsEliminate last static calls to rewriter from smt layer...
2021-10-20 Andrew ReynoldsMake SyGuS solver robust to non-closed enumerable sorts...
2021-10-20 Andrew ReynoldsDo not construct instantiation for checking propagating...
2021-10-20 Andrew ReynoldsCheck whether abduct option is enabled (#7418)
2021-10-20 Aina Niemetzapi: Rename get(BV|FP)*Size functions for consistency...
2021-10-20 Lachnitt[proofs] Alethe: Documentation on Translation (#7394)
2021-10-20 Andrew ReynoldsAdd LFSC signature for n-ary programs (#7360)
2021-10-20 Andrew ReynoldsUse codatatype bound variables for codatatype values...
2021-10-20 Andrew ReynoldsReimplement support for relational triggers (#7063)
2021-10-20 Andrew ReynoldsDo not make assumption about model for Boolean variable...
2021-10-20 Andrew ReynoldsCorrectly parse uninterpreted constant values in get...
2021-10-20 Abdalrhman... Avoid escaping `double-quotes` twice. (#7409)
2021-10-20 Andrew ReynoldsMake proofs of rewrites robust to use in internal subso...
2021-10-20 Andrew ReynoldsAdd basic regular expression type enumerator (#7416)
2021-10-19 Andrew ReynoldsFix expected conclusion for EQ_RESOLVE when expanding...
2021-10-19 Andrew ReynoldsSupport sequences of fixed finite cardinality (#7371)
2021-10-19 Andrew ReynoldsFix issue related to sanity checking integer models...
2021-10-19 Gereon KremerRemove setDefaults methods (#7413)
2021-10-18 Andrew ReynoldsAdd regression for fixed issue (#7395)
2021-10-18 Abdalrhman... Move check for experimental arrays features to `theory_...
2021-10-18 Andres NoetzliUpdate SMT-COMP script (#7389)
2021-10-15 yoni206Python api documentation: Op, Grammar, Result, Enums...
2021-10-15 Andrew ReynoldsAdd more regressions for fixed issues (#7382)
2021-10-15 Gereon KremerHave docs_upload properly upload tags. (#7352)
2021-10-15 Alex OzdemirFix bad cast in the python API (#7359)
2021-10-15 Andrew ReynoldsFix issues related to proofs of lemmas with duplicate...
2021-10-14 Andrew ReynoldsAdd regressions for fixed issues (#7369)
2021-10-14 Gereon KremerFix (get-info :authors) (#7373)
2021-10-14 Gereon KremerImprove ManagedStreams (#7367)
2021-10-14 Andrew ReynoldsAdd regression for fixed issue (#7365)
2021-10-14 Andrew ReynoldsImprove parser for tuple select (#7364)
2021-10-14 Andrew ReynoldsSplit entailment check from term database (#7342)
2021-10-14 Gereon KremerAlso test older cmake versions (#7347)
2021-10-14 Andrew ReynoldsFix quantifiers variable elimination for parametric...
2021-10-14 Gereon KremerFix GLPK linking (#7357)
2021-10-14 Andrew ReynoldsAdd core LFSC signatures (#7289)
2021-10-13 Andrew ReynoldsEliminate uses of rewrite from datatypes theory (#7354)
2021-10-13 Andrew ReynoldsMake (proof) equality engine use Env (#7336)
2021-10-12 Andrew ReynoldsSimplify refinement in sygus solver (#7343)
2021-10-12 Andrew ReynoldsEliminate calls to currentResourceManager (#7350)
2021-10-12 Mathias Preinercmake: Fix git info if build directory is outside of...
2021-10-12 Aina NiemetzClean up occurrences of SmtEngine in comments. (#7349)
2021-10-12 Aina NiemetzGet rid of unused member d_smtStats in ExpandDefs....
2021-10-12 Aina NiemetzRename SmtEngineState to SolverEngineState. (#7344)
2021-10-12 Gereon KremerFix glpk, add antlr.so (#7341)
2021-10-12 Andrew ReynoldsProvide a non-traversal interface to term formula remov...
2021-10-12 Andrew ReynoldsMinor cleaning of instantiation utilities (#7334)
2021-10-12 Andrew ReynoldsSimplify skolemization in sygus solver (#7331)
2021-10-12 Ouyanchengfix deprecation of std::iterator (#7332)
2021-10-11 Mathias PreinerStart post-release for 0.0.2
2021-10-11 Mathias PreinerBump version to 0.0.2
2021-10-11 Mathias PreinerFix release action.
2021-10-11 Aina NiemetzRename SmtEngineStatistics to SolverEngineStatistics...
next