cvc5.git
2019-01-15 Andrew Reynolds Only check disequal terms with sygus-rr-verify (#2793)
2019-01-14 Alex OzdemirClausalBitvectorProof (#2786)
2019-01-13 Alex OzdemirLFSC LRAT Output (#2787)
2019-01-12 Alex OzdemirLratInstruction inheritance (#2784)
2019-01-11 Alex OzdemirFixed linking against drat2er, and use drat2er (#2785)
2019-01-11 Aina NiemetzNew C++ API: Add unit tests for setInfo, setLogic,...
2019-01-10 Aina NiemetzNew C++ API: Get rid of mkConst functions (simplify...
2019-01-09 Andrew ReynoldsDo not rewrite 1-constructor sygus testers to true...
2019-01-09 Alex Ozdemir[BV Proofs] Option for proof format (#2777)
2019-01-09 Alex OzdemirClause proof printing (#2779)
2019-01-09 Alex OzdemirLFSC drat output (#2776)
2019-01-07 Aina NiemetzNew C++ API: Add missing getType() calls to kick off...
2019-01-06 Alex Ozdemir[DRAT] DRAT data structure (#2767)
2019-01-05 Mathias Preinercmake: Disable unit tests for static builds. (#2775)
2019-01-04 Andres NoetzliC++ API: Fix OOB read in unit test (#2774)
2019-01-04 Alex Ozdemir[LRAT] A C++ data structure for LRAT. (#2737)
2019-01-04 Aina NiemetzNew C++ API: Add missing catch blocks for std::invalid_...
2019-01-03 Andres NoetzliAPI/Smt2 parser: refactor termAtomic (#2674)
2019-01-03 Andres NoetzliC++ API: Reintroduce zero-value mkBitVector method...
2019-01-03 Alex Ozdemir[LRA proof] Recording & Printing LRA Proofs (#2758)
2019-01-03 Aina NiemetzNew C++ API: Add tests for mk-functions in solver objec...
2018-12-20 Aina NiemetzClean up BV kinds and type rules. (#2766)
2018-12-20 Aina NiemetzAdd missing type rules for parameterized operator kinds...
2018-12-19 Andrew ReynoldsFix issues with REWRITE_DONE in floating point rewriter...
2018-12-18 Aina NiemetzRemove noop. (#2763)
2018-12-17 Alex Ozdemir Configured for linking against drat2er (#2754)
2018-12-17 Aina NiemetzNew C++ API: Add tests for term object. (#2755)
2018-12-17 Alex OzdemirDRAT Signature (#2757)
2018-12-15 Andres NoetzliRevert "Move ss-combine rewrite to extended rewriter...
2018-12-15 Alex Ozdemir [LRA Proof] Storage for LRA proofs (#2747)
2018-12-14 Aina NiemetzFixed typos.
2018-12-14 Aina NiemetzNew C++ API: Add tests for opterm object. (#2756)
2018-12-14 Andrew Reynolds Fix extended rewriter for binary associative operators...
2018-12-14 Andrew ReynoldsMake single invocation and invariant pre/post condition...
2018-12-13 Aina NiemetzNew C++ API: Add tests for sort functions of solver...
2018-12-13 Andrew ReynoldsRemove spurious map (#2750)
2018-12-13 Aina NiemetzFix compiler warnings. (#2748)
2018-12-12 Andres NoetzliAPI: Add simple empty/sigma regexp unit tests (#2746)
2018-12-12 Alex Ozdemir[LRA proof] More complete LRA example proofs. (#2722)
2018-12-12 Alex Ozdemir[LRAT] signature robust against duplicate literals...
2018-12-11 Andrew ReynoldsRemove alternate versions of mbqi (#2742)
2018-12-11 Alex OzdemirLRAT signature (#2731)
2018-12-10 makaimannBoolToBV modes (off, ite, all) (#2530)
2018-12-07 Andres NoetzliStrings: Make EXTF_d inference more conservative (...
2018-12-07 Alex OzdemirArith Constraint Proof Loggin (#2732)
2018-12-07 Alex OzdemirEnable BV proofs when using an eager bitblaster (#2733)
2018-12-06 Andres NoetzliFix use-after-free due to destruction order (#2739)
2018-12-06 Andrew Reynolds Take into account minimality and types for cached...
2018-12-04 Andrew ReynoldsApply extended rewriting on PBE static symmetry breakin...
2018-12-04 Andrew ReynoldsEnable regular expression elimination by default. ...
2018-12-03 Andrew Reynolds Skip non-cardinality types in sets min card inference...
2018-12-03 Alex OzdemirBit vector proof superclass (#2599)
2018-12-02 Andrew ReynoldsOptimizations for PBE strings (#2728)
2018-11-29 Andrew Reynolds Infrastructure for sygus side conditions (#2729)
2018-11-29 Andrew ReynoldsCombine sygus stream with PBE (#2726)
2018-11-28 Andrew ReynoldsImprove interface for sygus grammar cons (#2727)
2018-11-28 Andrew ReynoldsInformation gain heuristic for PBE (#2719)
2018-11-28 Andrew ReynoldsOptimize re-elim for re.allchar components (#2725)
2018-11-28 Andres NoetzliImprove skolem caching by normalizing skolem args ...
2018-11-28 Andrew ReynoldsGeneralize sygus stream solution filtering to logical...
2018-11-28 Andrew ReynoldsImprove cegqi engine trace. (#2714)
2018-11-27 Andrew ReynoldsMake (T)NodeTrie a general utility (#2489)
2018-11-27 Andrew ReynoldsFix coverity warnings in datatypes (#2553)
2018-11-27 Andrew ReynoldsLazy model construction in TheoryEngine (#2633)
2018-11-27 Andres NoetzliReduce lookahead when parsing string literals (#2721)
2018-11-27 Alex OzdemirLRA proof signature fixes and a first proof for linear...
2018-11-23 Tom SmedingUse https for antlr3.org downloads (#2701)
2018-11-22 Andres NoetzliMove ss-combine rewrite to extended rewriter (#2703)
2018-11-22 Andres NoetzliAdd rewrite for (str.substr s x y) --> "" (#2695)
2018-11-21 Andrew ReynoldsCache evaluations for PBE (#2699)
2018-11-21 Andrew ReynoldsQuickly recognize when PBE conjectures are infeasible...
2018-11-21 MartinObvious rewrites to floating-point < and <=. (#2706)
2018-11-21 Andrew ReynoldsSupport string replace all (#2704)
2018-11-21 Andrew Reynolds Fix type enumerator for FP (#2717)
2018-11-20 Andrew ReynoldsFix real2int regression. (#2716)
2018-11-20 Alex OzdemirChange lemma proof step storage & iterators (#2712)
2018-11-20 Andrew Reynolds Clausify context-dependent simplifications in ext...
2018-11-19 Andrew ReynoldsFix E-matching for case where candidate generator is...
2018-11-15 Andrew Reynolds Expand definitions prior to model core computation...
2018-11-14 Mathias Preinercmake: Require boost 1.50.0 for examples. (#2710)
2018-11-08 Mathias Preinercmake: Add option to explicitely enable/disable static...
2018-11-08 Andres NoetzliEvaluator: add support for str.code (#2696)
2018-11-07 Haniel BarbosaAdding default SyGuS grammar construction for arrays...
2018-11-07 Andres NoetzliFix collectEmptyEqs in string rewriter (#2692)
2018-11-07 Andrew Reynolds Fix for itos reduction (#2691)
2018-11-06 Andrew ReynoldsIncorporate static PBE symmetry breaking lemmas into...
2018-11-05 Andrew ReynoldsChange default sygus enumeration mode to auto (#2689)
2018-11-05 Andrew ReynoldsFix coverity warnings in sygus enumerator (#2687)
2018-11-05 Aina NiemetzNew C++ API: Split unit tests. (#2688)
2018-11-05 yoni206Increasing coverage (#2683)
2018-11-05 Andres NoetzliAPI: Fix assignment operators (#2680)
2018-11-05 Andres Noetzliconfigure.sh: Fix option parsing to match --help (...
2018-11-05 Andrew ReynoldsAllow partial models with optimized sygus enumeration...
2018-11-05 Andrew Reynolds Implement option to turn off symmetry breaking for...
2018-11-03 Haniel BarbosaRefactor default grammars construction (#2681)
2018-11-02 yoni206fixes to regression docs (#2679)
2018-10-31 Andrew ReynoldsAdd optimized sygus enumeration (#2677)
2018-10-31 Andres NoetzliRecord assumption info in AssertionPipeline (#2678)
2018-10-24 Andrew ReynoldsMinor improvement to sygus trace (#2675)
2018-10-24 Andres NoetzliCMake: Set RPATH on installed binary (#2671)
next