projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Add HAVE_CLOCK_GETTIME guard to clock_gettime.c (#2428)
2018-09-05
Mathias Preiner
Add HAVE_CLOCK_GETTIME guard to clock_gettime.c (#2428)
commit
|
commitdiff
|
tree
2018-09-04
Andrew Reynolds
Remove redundant strings rewrite. (#2422)
commit
|
commitdiff
|
tree
2018-08-28
Andrew Reynolds
Address more coverity warnings (#2394)
commit
|
commitdiff
|
tree
2018-08-28
Andrew Reynolds
Refactor extended rewriter, move rewrites to aggressive...
commit
|
commitdiff
|
tree
2018-08-28
Aina Niemetz
New C++ API: Fix isDefinedKind() to not be ambigious...
commit
|
commitdiff
|
tree
2018-08-27
Mathias Preiner
Use std:unique_ptr instead of raw pointers in theory...
commit
|
commitdiff
|
tree
2018-08-25
yoni206
Refactor quantifier macros preprocessing pass (#1840)
commit
|
commitdiff
|
tree
2018-08-24
Aina Niemetz
New C++ API: Add checks for kind arguments. (#2369)
commit
|
commitdiff
|
tree
2018-08-23
Tim King
Replacing allocatedInCMM and d_noTrash with false everywhere...
commit
|
commitdiff
|
tree
2018-08-23
Andrew Reynolds
Fixing some coverity warnings (#2357)
commit
|
commitdiff
|
tree
2018-08-21
Aina Niemetz
Remove disabled system test cvc3_george. (#2342)
commit
|
commitdiff
|
tree
2018-08-18
Aina Niemetz
run-regress script: Exit with exit code > 0 on failure...
commit
|
commitdiff
|
tree
2018-08-17
Andrew Reynolds
Add sygus stream regressions (#2330)
commit
|
commitdiff
|
tree
2018-08-17
Andrew Reynolds
Eliminate partial operators in sygus grammar normalization...
commit
|
commitdiff
|
tree
2018-08-17
Tim King
Initialize inputAssertions only when proofRecipe is...
commit
|
commitdiff
|
tree
2018-08-17
Mathias Preiner
Refactor eager atoms preprocessing pass. (#2318)
commit
|
commitdiff
|
tree
2018-08-17
Caleb Donovick
Make quantifiers-preprocess preprocessing pass (#2322)
commit
|
commitdiff
|
tree
2018-08-16
Tim King
Switching an Assert to a CVC4_CHECK to test if it resolves...
commit
|
commitdiff
|
tree
2018-08-15
Mathias Preiner
Add contrib/get-gmp script. (#2292)
commit
|
commitdiff
|
tree
2018-08-08
Andrew Reynolds
Simplify and improve the sygus parser (#2266)
commit
|
commitdiff
|
tree
2018-08-07
Andrew Reynolds
Remove support for Enum sygus syntax. (#2264)
commit
|
commitdiff
|
tree
2018-08-06
Andrew Reynolds
Fixes for sygus inference (#2238)
commit
|
commitdiff
|
tree
2018-08-02
Andrew Reynolds
Make strings robust to regular expression variables...
commit
|
commitdiff
|
tree
2018-08-02
Andrew Reynolds
Improvements and fixes in cegqi arithmetic (#2247)
commit
|
commitdiff
|
tree
2018-08-01
Andrew Reynolds
Fix issues with bv2nat (#2219)
commit
|
commitdiff
|
tree
2018-08-01
Andrew Reynolds
Fix assertion in conjecture generator (#2246)
commit
|
commitdiff
|
tree
2018-08-01
Andrew Reynolds
Make conjecture generator's uf term enumeration safer...
commit
|
commitdiff
|
tree
2018-08-01
Andrew Reynolds
Make candidate rewrite match filtering handle polymorphic...
commit
|
commitdiff
|
tree
2018-07-27
Mathias Preiner
Make Python a required CVC4 dependency. (#2227)
commit
|
commitdiff
|
tree
2018-07-27
Andrew Reynolds
Fix for candidate rewrite rule filtering. (#2220)
commit
|
commitdiff
|
tree
2018-07-27
Andrew Reynolds
Make check-synth robust for assertions that are not...
commit
|
commitdiff
|
tree
2018-07-27
Andrew Reynolds
Fix Node::hasFreeVar for function variables (#2216)
commit
|
commitdiff
|
tree
2018-07-26
Aina Niemetz
New C++ API: Enable examples. (#2222)
commit
|
commitdiff
|
tree
2018-07-26
Andrew Reynolds
Fix rewriter for lambda (#2211)
commit
|
commitdiff
|
tree
2018-07-26
ayveejay
Avoid explicit dependency on Python 3 (#2195)
commit
|
commitdiff
|
tree
2018-07-25
Tim King
Changing ArithIteUtils to use CDInsertHashMap. (#2206)
commit
|
commitdiff
|
tree
2018-07-25
Tim King
Removing support for CDHashMap::iterator's postfix...
commit
|
commitdiff
|
tree
2018-07-22
Andrew Reynolds
sygusComp2018: Improvements to CEGIS loop (#2187)
commit
|
commitdiff
|
tree
2018-07-11
Caleb Donovick
Move rewrite to pass (#2128)
commit
|
commitdiff
|
tree
2018-07-07
Andrew Reynolds
sygusComp2018: improve extended rewriter for Bool...
commit
|
commitdiff
|
tree
2018-07-06
Martin
Feature/fp rewrite improvement (#2154)
commit
|
commitdiff
|
tree
2018-07-06
Aina Niemetz
New C++ API: Implementation of Solver class: Term handling...
commit
|
commitdiff
|
tree
2018-07-06
Andrew Reynolds
sygusComp2018: simplify beta reduction in uf rewriter...
commit
|
commitdiff
|
tree
2018-07-05
Andrew Reynolds
Make string length lemmas more robust to rewriting...
commit
|
commitdiff
|
tree
2018-07-05
Andrew Reynolds
Minor changes to sygus-rr utilities to support floating...
commit
|
commitdiff
|
tree
2018-07-04
Andrew Reynolds
Fix fmf-fun for non-equality function definitions ...
commit
|
commitdiff
|
tree
2018-07-02
Caleb Donovick
Add missing include (#2127)
commit
|
commitdiff
|
tree
2018-06-28
Andrew Reynolds
Remove comment about model value hack (#2118)
commit
|
commitdiff
|
tree
2018-06-26
Andrew Reynolds
sygusComp2018: add scripts. (#2103)
commit
|
commitdiff
|
tree
2018-06-26
Andrew Reynolds
Disable uf symmetry breaker in incremental mode (...
commit
|
commitdiff
|
tree
2018-06-12
Andrew Reynolds
Fix strip constant endpoint for ITOS in strings rewriter...
commit
|
commitdiff
|
tree
2018-06-11
Andrew Reynolds
Fix equality conflicts reported by FP (#2064)
commit
|
commitdiff
|
tree
2018-06-04
Andrew Reynolds
Enable cegqi (with model values) for floating point...
commit
|
commitdiff
|
tree
2018-06-02
Andrew Reynolds
Fix assertion involving unassigned Boolean eqc in...
commit
|
commitdiff
|
tree
2018-06-02
Mathias Preiner
Fix BV-abstraction check to consider SKOLEM. (#2042)
commit
|
commitdiff
|
tree
2018-06-02
Andrew Reynolds
Fix preinitialization pass for finite model finding...
commit
|
commitdiff
|
tree
2018-06-01
Andrew Reynolds
Use monomial sum utility to solve for quantifiers...
commit
|
commitdiff
|
tree
2018-06-01
Andrew Reynolds
Reduce before preregister. (#2025)
commit
|
commitdiff
|
tree
2018-05-31
Mathias Preiner
Fix bv-abstraction check for AND with non bit-vector...
commit
|
commitdiff
|
tree
2018-05-30
Aina Niemetz
Ignore license key in set-info command. (#2021)
commit
|
commitdiff
|
tree
2018-05-30
Andrew Reynolds
Fixes for quantifiers + incremental (#2009)
commit
|
commitdiff
|
tree
2018-05-30
Mathias Preiner
Normalize negated bit-vector terms over equalities...
commit
|
commitdiff
|
tree
2018-05-30
Andrew Reynolds
Draft run script for strings smt comp 2018. (#2016)
commit
|
commitdiff
|
tree
2018-05-29
Andrew Reynolds
Disable minisat elimination when nonlinear is enabled...
commit
|
commitdiff
|
tree
2018-05-27
Andrew Reynolds
Fix cegqi assertions for quantified non-linear cases...
commit
|
commitdiff
|
tree
2018-05-25
Mathias Preiner
Add QF_BV configuration for SMTCOMP'18. (#1981)
commit
|
commitdiff
|
tree
2018-05-24
Andrew Reynolds
Fix nl regression for unsat cores. (#1973)
commit
|
commitdiff
|
tree
2018-05-21
Andrew Reynolds
Improvements in parsing and printing related to mixed...
commit
|
commitdiff
|
tree
2018-05-21
makaimann
Handle IMPLIES in bool-to-bv and test it in regress0...
commit
|
commitdiff
|
tree
2018-05-21
Andrew Reynolds
Refactor sygus eval unfold (#1946)
commit
|
commitdiff
|
tree
2018-05-21
Caleb Donovick
Fix file extension (#1919)
commit
|
commitdiff
|
tree
2018-05-05
Andrew Reynolds
Fix handling of TO_REAL in cvc printer (#1876)
commit
|
commitdiff
|
tree
2018-05-04
Andrew Reynolds
Do not print tuples. (#1874)
commit
|
commitdiff
|
tree
2018-05-04
Mathias Preiner
Refactor bv-intro-pow2 preprocessing pass. (#1851)
commit
|
commitdiff
|
tree
2018-05-04
Andrew Reynolds
Sets subtypes (#1095)
commit
|
commitdiff
|
tree
2018-05-03
Mathias Preiner
Fix redundant internalPush calls. (#1865)
commit
|
commitdiff
|
tree
2018-05-03
Andrew Reynolds
Fix cvc printer for nullary constructors (#1856)
commit
|
commitdiff
|
tree
2018-05-03
Andrew Reynolds
Initial support for string standard in smt lib 2.6...
commit
|
commitdiff
|
tree
2018-04-30
Andrew Reynolds
Remove subsort symmetry breaking (#1807)
commit
|
commitdiff
|
tree
2018-04-20
yoni206
Allow metadata lines in test files to have leading...
commit
|
commitdiff
|
tree
2018-04-15
Andrew Reynolds
Fix mk type const (#1776)
commit
|
commitdiff
|
tree
2018-04-04
Andrew Reynolds
Proper initialization and destruction of sygus unif...
commit
|
commitdiff
|
tree
2018-04-04
Andrew Reynolds
Option to turn arbitrary input into sygus (#1704)
commit
|
commitdiff
|
tree
2018-03-26
Andrew Reynolds
Check model only when sat (#1694)
commit
|
commitdiff
|
tree
2018-03-25
Andrew Reynolds
Cleanup various exit calls (#1692)
commit
|
commitdiff
|
tree
2018-03-25
Mathias Preiner
Remove doc/libcvc4.3 from options/Makefile.am. (#1696)
commit
|
commitdiff
|
tree
2018-03-20
Andrew Reynolds
Fix datatype dump regression. (#1672)
commit
|
commitdiff
|
tree
2018-02-10
Aina Niemetz
Remove mkNode from bv::utils (#1587)
commit
|
commitdiff
|
tree
2018-01-27
Tim King
Removing an unused variable. Resolves CID 1172257....
commit
|
commitdiff
|
tree
2018-01-27
Tim King
Removing structurally dead code. (#1540)
commit
|
commitdiff
|
tree
2018-01-14
Tim King
Removing throw specifiers from OptionsHandler. (#1510)
commit
|
commitdiff
|
tree
2018-01-10
Tim King
Cleaning up throw specifiers on Exception and subclasses...
commit
|
commitdiff
|
tree
2017-12-11
justinxu421
Add new infrastructure for preprocessing passes (#1053)
commit
|
commitdiff
|
tree
2017-11-15
Tim King
Adding garbage collection for Proof objects. (#1294)
commit
|
commitdiff
|
tree
2017-11-04
Andrew Reynolds
Fix bv help message. (#1315)
commit
|
commitdiff
|
tree
2017-10-27
Tim King
Adds a macro to SWIG to ignore the override and final...
commit
|
commitdiff
|
tree
2017-10-26
Tim King
Removing throw specifiers from OutputChannel and subclasses...
commit
|
commitdiff
|
tree
2017-10-10
Martin
Add skeleton of the FP theory solver (#1130)
commit
|
commitdiff
|
tree
2017-10-05
Martin
Allow CDHashMaps for objects without default constructors...
commit
|
commitdiff
|
tree
2017-10-03
Martin
Add 5 FP kinds for partial to total fn conversion ...
commit
|
commitdiff
|
tree
next