projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
New C++ API: Fix isDefinedKind() to not be ambigious with respect to … (#2384)
[cvc5.git]
/
src
/
2018-08-28
Aina Niemetz
New C++ API: Fix isDefinedKind() to not be ambigious...
tree
|
commitdiff
2018-08-27
Mathias Preiner
Use std:unique_ptr instead of raw pointers in theory...
tree
|
commitdiff
2018-08-27
Andres Noetzli
Resolution proof: separate printing from proof (#1964)
tree
|
commitdiff
2018-08-27
Andrew Reynolds
Make division chainable in the smt2 parser (#2367)
tree
|
commitdiff
2018-08-26
Andres Noetzli
Use uniform length limit for String constants (#2381)
tree
|
commitdiff
2018-08-26
Andrew Reynolds
Fix unsigned integer type issues in strings (#2380)
tree
|
commitdiff
2018-08-26
Andres Noetzli
Refactor unconstrained simplification pass (#2374)
tree
|
commitdiff
2018-08-25
yoni206
Refactor quantifier macros preprocessing pass (#1840)
tree
|
commitdiff
2018-08-25
Haniel Barbosa
Refactor nlExtPurify preprocessing pass (#1963)
tree
|
commitdiff
2018-08-25
Andrew Reynolds
Clean up quantifiers engine initialization. (#2371)
tree
|
commitdiff
2018-08-24
Andrew Reynolds
Fix more simple coverity warnings (#2372)
tree
|
commitdiff
2018-08-24
Andrew Reynolds
Remove spurious disabling of cbqi-all (#2368)
tree
|
commitdiff
2018-08-24
Andres Noetzli
Add tests that enumerate and verify rewrite rules ...
tree
|
commitdiff
2018-08-24
Andrew Reynolds
Do not print internally generated datatypes in externa...
tree
|
commitdiff
2018-08-24
Aina Niemetz
New C++ API: Add checks for kind arguments. (#2369)
tree
|
commitdiff
2018-08-23
Tim King
Replacing allocatedInCMM and d_noTrash with false every...
tree
|
commitdiff
2018-08-23
Haniel Barbosa
Makes the filename be set in the SMT engine by default...
tree
|
commitdiff
2018-08-23
Andrew Reynolds
Fixing some coverity warnings (#2357)
tree
|
commitdiff
2018-08-23
Aina Niemetz
Refactor ITE simplification preprocessing pass. (#2360)
tree
|
commitdiff
2018-08-23
Andres Noetzli
Use "filename" instead of "name" in SmtEngine::setInfo...
tree
|
commitdiff
2018-08-23
yoni206
global-negate preprocessing pass (#2317)
tree
|
commitdiff
2018-08-22
Andrew Reynolds
More unused code elimination (#2358)
tree
|
commitdiff
2018-08-22
yoni206
Generating less consistency lemmas in bv-ackermann...
tree
|
commitdiff
2018-08-22
Tim King
Wrapping TheorySetsPrivate in a unique_ptr. (#2356)
tree
|
commitdiff
2018-08-22
Andrew Reynolds
Fix invalid iterator comparisons (#2349)
tree
|
commitdiff
2018-08-22
Andrew Reynolds
Fix processing of nested Variable construct in sygus...
tree
|
commitdiff
2018-08-21
Tim King
Removing unused bool members in command.cpp. Also initi...
tree
|
commitdiff
2018-08-21
Andrew Reynolds
Warn and enable quantifiers when using sygus + logics...
tree
|
commitdiff
2018-08-21
Haniel Barbosa
Makes the new row propagation system default (#2335)
tree
|
commitdiff
2018-08-21
Mathias Preiner
Move d_realAssertionsEnd from SmtEnginePrivate to Asser...
tree
|
commitdiff
2018-08-21
Tim King
Add constexpr annotations to help coverity understand...
tree
|
commitdiff
2018-08-21
Andrew Reynolds
Use cbqi-full for sygus (#2346)
tree
|
commitdiff
2018-08-21
Aina Niemetz
Fix initialization of d_smt in ValidityChecker for...
tree
|
commitdiff
2018-08-21
Andrew Reynolds
More unused code elimination (#2339)
tree
|
commitdiff
2018-08-20
Andrew Reynolds
Remove support for prototype (non-sygus) synthesis...
tree
|
commitdiff
2018-08-20
Andrew Reynolds
Minor improvements to the interface for sygus sampler...
tree
|
commitdiff
2018-08-20
Andrew Reynolds
Make sygus inference a preprocessing pass (#2334)
tree
|
commitdiff
2018-08-17
Andrew Reynolds
Remove support for flipDecision (#2319)
tree
|
commitdiff
2018-08-17
Andrew Reynolds
Remove miscellaneous unused code (#2333)
tree
|
commitdiff
2018-08-17
Andrew Reynolds
Split sygus grammar to its own ANTLR grammar (#2307)
tree
|
commitdiff
2018-08-17
Andrew Reynolds
Fix spurious warning in sort inference (#2331)
tree
|
commitdiff
2018-08-17
Andrew Reynolds
Fix arithmetic division by zero in sygus repair consta...
tree
|
commitdiff
2018-08-17
Andrew Reynolds
Eliminate partial operators in sygus grammar normaliza...
tree
|
commitdiff
2018-08-17
Tim King
Initialize inputAssertions only when proofRecipe is...
tree
|
commitdiff
2018-08-17
Mathias Preiner
Refactor eager atoms preprocessing pass. (#2318)
tree
|
commitdiff
2018-08-17
Haniel Barbosa
cleaning unnecessary timers/dumps (#2327)
tree
|
commitdiff
2018-08-17
Haniel Barbosa
Adding support for bitvector SyGuS problems without...
tree
|
commitdiff
2018-08-17
Caleb Donovick
Make quantifiers-preprocess preprocessing pass (#2322)
tree
|
commitdiff
2018-08-17
Tim King
Removing coverity warnings from theory_sep.cpp (#2320)
tree
|
commitdiff
2018-08-17
Andres Noetzli
Refactor IteRemoval preprocessing pass (#1793)
tree
|
commitdiff
2018-08-16
Andres Noetzli
Move node algorithms to separate file (#2311)
tree
|
commitdiff
2018-08-16
Andrew Reynolds
Minor fixes and improvement for sygus to builtin. ...
tree
|
commitdiff
2018-08-16
Haniel Barbosa
Refactor extended rewriter preprocessing pass (#2324)
tree
|
commitdiff
2018-08-16
Haniel Barbosa
Refactor apply2const (#2316)
tree
|
commitdiff
2018-08-16
Tim King
Switching an Assert to a CVC4_CHECK to test if it resol...
tree
|
commitdiff
2018-08-15
Tim King
Removing attribute cleanups. (#2300)
tree
|
commitdiff
2018-08-15
Andres Noetzli
Remove unused tuple classes (#2313)
tree
|
commitdiff
2018-08-15
Andres Noetzli
Remove unused class DynamicArray (#2312)
tree
|
commitdiff
2018-08-15
Andrew Reynolds
Make sort inference a preprocessing pass (#2309)
tree
|
commitdiff
2018-08-15
Andres Noetzli
Fix dumping of get-unsat-assumptions (#2302)
tree
|
commitdiff
2018-08-15
Andres Noetzli
Remove unused declaration (#2310)
tree
|
commitdiff
2018-08-14
Andres Noetzli
Fix get-unsat-assumptions output (#2301)
tree
|
commitdiff
2018-08-13
Tim King
Removing support for T* and const T* attributes. (...
tree
|
commitdiff
2018-08-11
Andres Noetzli
Make attributes robust to static init orderings (#2295)
tree
|
commitdiff
2018-08-10
Aina Niemetz
Fix portfolio command executor for changes from #2240...
tree
|
commitdiff
2018-08-09
Andrew Reynolds
Fix char overflow issues in regular expression solver...
tree
|
commitdiff
2018-08-09
Aina Niemetz
Plug solver API object into parser. (#2240)
tree
|
commitdiff
2018-08-09
Tim King
Fixing documentation nit from PR#2232. (#2289)
tree
|
commitdiff
2018-08-08
Tim King
Proposal for adding map utility functions to CVC4...
tree
|
commitdiff
2018-08-08
Andrew Reynolds
Disable argument relevance for sygus by default (#2288)
tree
|
commitdiff
2018-08-08
Andrew Reynolds
Add debug test for sygus subcall verify calls. (#2287)
tree
|
commitdiff
2018-08-08
Andrew Reynolds
Move uf model code from uf to quantifiers (#2095)
tree
|
commitdiff
2018-08-08
Andrew Reynolds
Do beta-reduction in expandDefinitions (#2286)
tree
|
commitdiff
2018-08-08
Andres Noetzli
Require Swig 3 (#2283)
tree
|
commitdiff
2018-08-08
Andrew Reynolds
Simplify and improve the sygus parser (#2266)
tree
|
commitdiff
2018-08-08
Andrew Reynolds
Document/refactor datatypes sygus simple symmetry break...
tree
|
commitdiff
2018-08-08
Andrew Reynolds
Fix simple reg exp consume rewrite (#2281)
tree
|
commitdiff
2018-08-08
Andres Noetzli
Delete functions instead of using CVC4_UNDEFINED (...
tree
|
commitdiff
2018-08-07
Andrew Reynolds
Wait to do sygus qe preprocess until full effort check...
tree
|
commitdiff
2018-08-07
Andrew Reynolds
Fix inference of pre and post conditions for non variab...
tree
|
commitdiff
2018-08-07
Mathias Preiner
Make output of flushInformation and safeFlushInformatio...
tree
|
commitdiff
2018-08-07
Aina Niemetz
Add rewrite for nested BITVECTOR_ITE that can be merged...
tree
|
commitdiff
2018-08-07
Andrew Reynolds
Make flat form inferences optional in strings (#2277)
tree
|
commitdiff
2018-08-07
Andrew Reynolds
Add RegLan to smt2/sygus parsers. (#2276)
tree
|
commitdiff
2018-08-07
Andrew Reynolds
Move sygus quantifier elimination step for non-ground...
tree
|
commitdiff
2018-08-07
Andrew Reynolds
Remove support for Enum sygus syntax. (#2264)
tree
|
commitdiff
2018-08-06
Andrew Reynolds
Fixes for sygus inference (#2238)
tree
|
commitdiff
2018-08-06
Andrew Reynolds
Fixes and improvements for single invocation inference...
tree
|
commitdiff
2018-08-06
Andrew Reynolds
Fix degenerate case of sygus grammar construction for...
tree
|
commitdiff
2018-08-04
Aina Niemetz
Add rewrite for nested BITVECTOR_ITE with cond_outer...
tree
|
commitdiff
2018-08-04
Aina Niemetz
Add rewrite for BITVECTOR_ITE with const children....
tree
|
commitdiff
2018-08-03
Aina Niemetz
Add rewrite for BITVECTOR_ITE with term_then == term_el...
tree
|
commitdiff
2018-08-03
Andrew Reynolds
Eliminate option for sygus UF evaluation functions...
tree
|
commitdiff
2018-08-03
Mathias Preiner
Fix printing statistics in case of signals. (#2267)
tree
|
commitdiff
2018-08-03
Aina Niemetz
Add timer for BV inequality solver. (#2265)
tree
|
commitdiff
2018-08-02
Andrew Reynolds
Parse standard separation logic inputs (#2257)
tree
|
commitdiff
2018-08-02
Andrew Reynolds
Improve CEGQI heuristics involving equality and multipl...
tree
|
commitdiff
2018-08-02
Andrew Reynolds
Fix candidate rewrite utilities for non-first-class...
tree
|
commitdiff
2018-08-02
Andrew Reynolds
Make strings robust to regular expression variables...
tree
|
commitdiff
2018-08-02
Aina Niemetz
Add rewrites for BITVECTOR_ITE and BITVECTOR_COMP with...
tree
|
commitdiff
next