projects / cvc5.git / search
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Use zero slope tangent planes for transcendental functions (#2803)
2019-03-14 Andrew ReynoldsUse zero slope tangent planes for transcendental functions...
commit | commitdiff | tree
2019-03-14 Andrew ReynoldsProperly handle lambdas in relevant domain (#2853)
 commit | commitdiff | tree
2019-03-14 Andrew Reynolds Add getFreeVariables method to node algorithm (#2852)
 commit | commitdiff | tree
2019-03-14 Andrew ReynoldsImplement proper semantics for TPTP predicate is_rat...
commit | commitdiff | tree
2019-03-14 Andrew Reynolds Fix substitution step in ho matching (#2825)
 commit | commitdiff | tree
2019-03-14 Andrew ReynoldsGeneralize sygus-rr-verify for fast enumerator (#2829)
 commit | commitdiff | tree
2019-03-13 Andres NoetzliAdd statistics for proof gen./checking time, size ...
commit | commitdiff | tree
2019-03-13 Andrew ReynoldsRemove spurious data member. (#2857)
 commit | commitdiff | tree
2019-03-13 Mathias PreinerFix public headers for make install. (#2856)
 commit | commitdiff | tree
2019-03-12 Andrew ReynoldsAdd option --sygus-rr-synth-rec for considering all...
commit | commitdiff | tree
2019-03-12 Andrew Reynolds Move tuple/record update elimination from ppRewrite...
commit | commitdiff | tree
2019-03-01 Alex OzdemirErProof class with LFSC output (#2812)
 commit | commitdiff | tree
2019-02-27 Andres NoetzliUse string stream for proofs instead of tmp files ...
https://github.com/CVC4/LFSC/pull/14).
 commit | commitdiff | tree
2019-02-26 Andres NoetzliClangFormat: Disable DerivePointerAlignment (#2842)
 commit | commitdiff | tree
2019-02-13 Aina NiemetzNew C++ API: Remove redundant declareFun function....
commit | commitdiff | tree
2019-02-13 Andres NoetzliRewrite simple regexp pattern to str.contains (#2827)
 commit | commitdiff | tree
2019-02-11 Aina NiemetzNew C++ API: Unit tests for declare* functions. (#2831)
 commit | commitdiff | tree
2019-02-04 Andres NoetzliAdd rewrite for contains + const strings replace (...
commit | commitdiff | tree
2019-02-02 Andres NoetzliFix corner case in stripConstantEndpoints (#2824)
 commit | commitdiff | tree
2019-01-29 Aina NiemetzNew C++ API: Fix checks for mkTerm. (#2820)
 commit | commitdiff | tree
2019-01-29 Andres NoetzliStrings: Remove redundant replace rewrite (#2822)
 commit | commitdiff | tree
2019-01-24 Alex OzdemirExtended DRAT signature to operational DRAT (#2815)
 commit | commitdiff | tree
2019-01-23 Andres NoetzliAvoid using ProofManager in non-proof CMS build (#2814)
 commit | commitdiff | tree
2019-01-23 Andres NoetzliStrings: Strengthen multiset reasoning (#2817)
 commit | commitdiff | tree
2019-01-22 Andrew Reynolds Fix tuple and record CVC printing (#2818)
 commit | commitdiff | tree
2019-01-22 Andrew Reynolds Fix parsing of overloaded parametric datatype selectors...
commit | commitdiff | tree
2019-01-22 Aina NiemetzNew README (markdown). (#2797)
 commit | commitdiff | tree
2019-01-19 Andres NoetzliFix missing-override warning (#2811)
[comment](https://github.com/CVC4/CVC4/pull/2786#discussion_r247...
commit | commitdiff | tree
2019-01-18 Andres Noetzli Fix ABC build (#2808)
 commit | commitdiff | tree
2019-01-17 Andres NoetzliAdd option to print BV constants in binary (#2805)
 commit | commitdiff | tree
2019-01-16 Alex OzdemirBugfix: LFSC clause equality (#2801)
 commit | commitdiff | tree
2019-01-16 Alex OzdemirExtended Resolution Signature (#2788)
 commit | commitdiff | tree
2019-01-16 Andres NoetzliCMake: Fix search for static libraries (#2798)
 commit | commitdiff | tree
2019-01-15 Andres NoetzliStrings: Add option to change loop process mode (#2794)
 commit | commitdiff | tree
2019-01-15 Andrew Reynolds Fix unsound double abs rewrite rule for FP (#2792)
 commit | commitdiff | tree
2019-01-15 Andrew Reynolds Only check disequal terms with sygus-rr-verify (#2793)
 commit | commitdiff | tree
2019-01-14 Alex OzdemirClausalBitvectorProof (#2786)
 commit | commitdiff | tree
2019-01-13 Alex OzdemirLFSC LRAT Output (#2787)
 commit | commitdiff | tree
2019-01-12 Alex OzdemirLratInstruction inheritance (#2784)
 commit | commitdiff | tree
2019-01-11 Alex OzdemirFixed linking against drat2er, and use drat2er (#2785)
 commit | commitdiff | tree
2019-01-11 Aina NiemetzNew C++ API: Add unit tests for setInfo, setLogic,...
commit | commitdiff | tree
2019-01-10 Aina NiemetzNew C++ API: Get rid of mkConst functions (simplify...
commit | commitdiff | tree
2019-01-09 Andrew ReynoldsDo not rewrite 1-constructor sygus testers to true...
commit | commitdiff | tree
2019-01-09 Alex OzdemirClause proof printing (#2779)
 commit | commitdiff | tree
2019-01-09 Alex OzdemirLFSC drat output (#2776)
 commit | commitdiff | tree
2019-01-07 Aina NiemetzNew C++ API: Add missing getType() calls to kick off...
commit | commitdiff | tree
2019-01-06 Alex Ozdemir[DRAT] DRAT data structure (#2767)
 commit | commitdiff | tree
2019-01-04 Alex Ozdemir[LRAT] A C++ data structure for LRAT. (#2737)
 commit | commitdiff | tree
2019-01-04 Aina NiemetzNew C++ API: Add missing catch blocks for std::invalid_argum...
commit | commitdiff | tree
2019-01-03 Alex Ozdemir[LRA proof] Recording & Printing LRA Proofs (#2758)
 commit | commitdiff | tree
2019-01-03 Aina NiemetzNew C++ API: Add tests for mk-functions in solver object...
commit | commitdiff | tree
2018-12-19 Andrew ReynoldsFix issues with REWRITE_DONE in floating point rewriter...
commit | commitdiff | tree
2018-12-18 Aina NiemetzRemove noop. (#2763)
 commit | commitdiff | tree
2018-12-17 Aina NiemetzNew C++ API: Add tests for term object. (#2755)
 commit | commitdiff | tree
2018-12-17 Alex OzdemirDRAT Signature (#2757)
 commit | commitdiff | tree
2018-12-15 Alex Ozdemir [LRA Proof] Storage for LRA proofs (#2747)
 commit | commitdiff | tree
2018-12-14 Aina NiemetzNew C++ API: Add tests for opterm object. (#2756)
 commit | commitdiff | tree
2018-12-13 Aina NiemetzNew C++ API: Add tests for sort functions of solver...
commit | commitdiff | tree
2018-12-13 Andrew ReynoldsRemove spurious map (#2750)
 commit | commitdiff | tree
2018-12-13 Aina NiemetzFix compiler warnings. (#2748)
 commit | commitdiff | tree
2018-12-12 Andres NoetzliAPI: Add simple empty/sigma regexp unit tests (#2746)
 commit | commitdiff | tree
2018-12-12 Alex Ozdemir[LRA proof] More complete LRA example proofs. (#2722)
 commit | commitdiff | tree
2018-12-12 Alex Ozdemir[LRAT] signature robust against duplicate literals...
commit | commitdiff | tree
2018-12-11 Andrew ReynoldsRemove alternate versions of mbqi (#2742)
 commit | commitdiff | tree
2018-12-11 Alex OzdemirLRAT signature (#2731)
 commit | commitdiff | tree
2018-12-07 Alex OzdemirArith Constraint Proof Loggin (#2732)
 commit | commitdiff | tree
2018-12-07 Alex OzdemirEnable BV proofs when using an eager bitblaster (#2733)
 commit | commitdiff | tree
2018-12-06 Andrew Reynolds Take into account minimality and types for cached...
commit | commitdiff | tree
2018-12-04 Andrew ReynoldsApply extended rewriting on PBE static symmetry breaking...
commit | commitdiff | tree
2018-12-03 Alex OzdemirBit vector proof superclass (#2599)
 commit | commitdiff | tree
2018-12-02 Andrew ReynoldsOptimizations for PBE strings (#2728)
 commit | commitdiff | tree
2018-11-29 Andrew Reynolds Infrastructure for sygus side conditions (#2729)
 commit | commitdiff | tree
2018-11-29 Andrew ReynoldsCombine sygus stream with PBE (#2726)
 commit | commitdiff | tree
2018-11-28 Andrew ReynoldsImprove interface for sygus grammar cons (#2727)
 commit | commitdiff | tree
2018-11-28 Andrew ReynoldsInformation gain heuristic for PBE (#2719)
 commit | commitdiff | tree
2018-11-28 Andrew ReynoldsOptimize re-elim for re.allchar components (#2725)
 commit | commitdiff | tree
2018-11-28 Andres NoetzliImprove skolem caching by normalizing skolem args ...
commit | commitdiff | tree
2018-11-28 Andrew ReynoldsGeneralize sygus stream solution filtering to logical...
commit | commitdiff | tree
2018-11-28 Andrew ReynoldsImprove cegqi engine trace. (#2714)
 commit | commitdiff | tree
2018-11-27 Andrew ReynoldsLazy model construction in TheoryEngine (#2633)
 commit | commitdiff | tree
2018-11-27 Alex OzdemirLRA proof signature fixes and a first proof for linear...
commit | commitdiff | tree
2018-11-22 Andres NoetzliMove ss-combine rewrite to extended rewriter (#2703)
 commit | commitdiff | tree
2018-11-22 Andres NoetzliAdd rewrite for (str.substr s x y) --> "" (#2695)
 commit | commitdiff | tree
2018-11-21 Andrew ReynoldsCache evaluations for PBE (#2699)
 commit | commitdiff | tree
2018-11-21 Andrew ReynoldsSupport string replace all (#2704)
 commit | commitdiff | tree
2018-11-21 Andrew Reynolds Fix type enumerator for FP (#2717)
 commit | commitdiff | tree
2018-11-20 Andrew Reynolds Clausify context-dependent simplifications in ext...
commit | commitdiff | tree
2018-11-19 Andrew ReynoldsFix E-matching for case where candidate generator is...
commit | commitdiff | tree
2018-11-15 Andrew Reynolds Expand definitions prior to model core computation...
commit | commitdiff | tree
2018-11-08 Mathias Preinercmake: Add option to explicitely enable/disable static...
commit | commitdiff | tree
2018-11-07 Andrew Reynolds Fix for itos reduction (#2691)
 commit | commitdiff | tree
2018-11-06 Andrew ReynoldsIncorporate static PBE symmetry breaking lemmas into...
commit | commitdiff | tree
2018-11-05 Andrew ReynoldsChange default sygus enumeration mode to auto (#2689)
 commit | commitdiff | tree
2018-11-05 Andrew ReynoldsFix coverity warnings in sygus enumerator (#2687)
 commit | commitdiff | tree
2018-11-05 Aina NiemetzNew C++ API: Split unit tests. (#2688)
 commit | commitdiff | tree
2018-11-05 Andrew ReynoldsAllow partial models with optimized sygus enumeration...
commit | commitdiff | tree
2018-11-02 yoni206fixes to regression docs (#2679)
 commit | commitdiff | tree
2018-10-31 Andrew ReynoldsAdd optimized sygus enumeration (#2677)
 commit | commitdiff | tree
2018-10-24 Andrew ReynoldsMinor improvement to sygus trace (#2675)
 commit | commitdiff | tree
2018-10-24 Andres NoetzliCMake: Set RPATH on installed binary (#2671)
 commit | commitdiff | tree
next