projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2018-09-12
Andrew Reynolds
Initial infrastructure for theory decision manager...
commit
|
commitdiff
|
tree
2018-09-12
Andrew Reynolds
Fix for when strings process loop is disabled. (#2456)
commit
|
commitdiff
|
tree
2018-09-11
Aina Niemetz
Fixe compiler warning in line_buffer.cpp. (#2453)
commit
|
commitdiff
|
tree
2018-09-11
Andrew Reynolds
Support model cores via option --produce-model-cores...
commit
|
commitdiff
|
tree
2018-09-11
yoni206
Avoid calling size() every iteration (#2450)
commit
|
commitdiff
|
tree
2018-09-11
Andrew Reynolds
Fix global negate (#2449)
commit
|
commitdiff
|
tree
2018-09-11
Haniel Barbosa
fix (#2446)
commit
|
commitdiff
|
tree
2018-09-11
Andres Noetzli
Set NodeManager to nullptr when exporting vars (#2445)
commit
|
commitdiff
|
tree
2018-09-11
Haniel Barbosa
Using a single condition enumerator in sygus-unif ...
commit
|
commitdiff
|
tree
2018-09-11
Aina Niemetz
Refactor non-clausal simplify preprocessing pass. ...
commit
|
commitdiff
|
tree
2018-09-10
Andrew Reynolds
Squash implementation of counterexample-guided instanti...
commit
|
commitdiff
|
tree
2018-09-10
Andres Noetzli
Add (str.replace (str.replace y w y) y z) rewrite ...
commit
|
commitdiff
|
tree
2018-09-07
Mathias Preiner
Replace boost::integer_traits with std::numeric_limits...
commit
|
commitdiff
|
tree
2018-09-07
Mathias Preiner
Remove clock_gettime() replacement for macOS. (#2436)
commit
|
commitdiff
|
tree
2018-09-07
Andrew Reynolds
Make isClosedEnumerable a member of TypeNode (#2434)
commit
|
commitdiff
|
tree
2018-09-06
Andrew Reynolds
Further simplify and fix initialization of ce guided...
commit
|
commitdiff
|
tree
2018-09-06
Andrew Reynolds
Refactor and document quantifiers variable elimination...
commit
|
commitdiff
|
tree
2018-09-06
Andrew Reynolds
Minor improvements to interface for rep set. (#2435)
commit
|
commitdiff
|
tree
2018-09-05
Andrew Reynolds
More extended rewrites for strings equality (#2431)
commit
|
commitdiff
|
tree
2018-09-05
Andrew Reynolds
Eliminate select over store in quantifier bodies ...
commit
|
commitdiff
|
tree
2018-09-05
Mathias Preiner
Use std::uniqe_ptr for d_eq_infer to make Coverity...
commit
|
commitdiff
|
tree
2018-09-05
Andrew Reynolds
Remove printing support for sygus enumeration types...
commit
|
commitdiff
|
tree
2018-09-05
Andrew Reynolds
Finer-grained inference of substitutions in incremental...
commit
|
commitdiff
|
tree
2018-09-05
Andres Noetzli
Add regex grammar to rewriter verification tests (...
commit
|
commitdiff
|
tree
2018-09-05
Andrew Reynolds
Extended rewriter for string equalities (#2427)
commit
|
commitdiff
|
tree
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-09-04
Andres Noetzli
Update INSTALL instructions (#2420)
commit
|
commitdiff
|
tree
2018-09-04
Andres Noetzli
Remove CVC3 compatibility layer (#2418)
commit
|
commitdiff
|
tree
2018-09-04
Andres Noetzli
Remove unused options file (#2413)
commit
|
commitdiff
|
tree
2018-09-04
Andrew Reynolds
Minor improvements to theory model builder interface...
commit
|
commitdiff
|
tree
2018-09-04
Andrew Reynolds
Make quantifiers strategies exit immediately when in...
commit
|
commitdiff
|
tree
2018-09-04
Aina Niemetz
Transfer ownership of learned literals from SMT engine...
commit
|
commitdiff
|
tree
2018-09-04
Aina Niemetz
Fix merge mishap of #2359.
commit
|
commitdiff
|
tree
2018-09-04
Andrew Reynolds
Refactor ceg conjecture initialization (#2411)
commit
|
commitdiff
|
tree
2018-08-31
Haniel Barbosa
Allows SAT checks of repair const to have different...
commit
|
commitdiff
|
tree
2018-08-31
Andrew Reynolds
Refactor and document alpha equivalence. (#2402)
commit
|
commitdiff
|
tree
2018-08-31
Haniel Barbosa
Fix export of bound variables (#2409)
commit
|
commitdiff
|
tree
2018-08-30
Mathias Preiner
Refactor theory preprocess into preprocessing pass...
commit
|
commitdiff
|
tree
2018-08-30
Andres Noetzli
Use useBland option in FCSimplexDecisionProcedure ...
commit
|
commitdiff
|
tree
2018-08-30
Andrew Reynolds
Add regular expression elimination module (#2400)
commit
|
commitdiff
|
tree
2018-08-29
Mathias Preiner
Refactor MipLibTrick preprocessing pass. (#2359)
commit
|
commitdiff
|
tree
2018-08-29
Tim King
Forcing attribute_internals.h to use uint64_t's for...
commit
|
commitdiff
|
tree
2018-08-29
Haniel Barbosa
fix bv total ops printing (#2365)
commit
|
commitdiff
|
tree
2018-08-28
Andrew Reynolds
Split term canonize utility to own file and document...
commit
|
commitdiff
|
tree
2018-08-28
Aina Niemetz
Reorder circuit propagator class.
commit
|
commitdiff
|
tree
2018-08-28
Aina Niemetz
Move flag needsFinish from SMT engine to circuit propag...
commit
|
commitdiff
|
tree
2018-08-28
Andrew Reynolds
Fix for get constraints method in fmf-fun (#2399)
commit
|
commitdiff
|
tree
2018-08-28
Andrew Reynolds
Solve equalities between Boolean variables in presolve...
commit
|
commitdiff
|
tree
2018-08-28
Andres Noetzli
Remove throw specifiers in FP type checker (#2392)
commit
|
commitdiff
|
tree
2018-08-28
Andres Noetzli
Remove dead code in fp_converter (#2388)
commit
|
commitdiff
|
tree
2018-08-28
Andrew Reynolds
Fix sort inference for quantified variables of interpre...
commit
|
commitdiff
|
tree
2018-08-28
Andrew Reynolds
Address more coverity warnings (#2394)
commit
|
commitdiff
|
tree
2018-08-28
Andrew Reynolds
Fix warning in sygus io. (#2391)
commit
|
commitdiff
|
tree
2018-08-28
Andres Noetzli
Remove dead code in evaluator (#2389)
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-27
Andres Noetzli
Resolution proof: separate printing from proof (#1964)
commit
|
commitdiff
|
tree
2018-08-27
Andrew Reynolds
Make division chainable in the smt2 parser (#2367)
commit
|
commitdiff
|
tree
2018-08-27
Andres Noetzli
Remove Coverity build from Travis (#2373)
commit
|
commitdiff
|
tree
2018-08-26
Andres Noetzli
Use uniform length limit for String constants (#2381)
commit
|
commitdiff
|
tree
2018-08-26
Andrew Reynolds
Fix unsigned integer type issues in strings (#2380)
commit
|
commitdiff
|
tree
2018-08-26
Andres Noetzli
Refactor unconstrained simplification pass (#2374)
commit
|
commitdiff
|
tree
2018-08-25
yoni206
Refactor quantifier macros preprocessing pass (#1840)
commit
|
commitdiff
|
tree
2018-08-25
Haniel Barbosa
Refactor nlExtPurify preprocessing pass (#1963)
commit
|
commitdiff
|
tree
2018-08-25
Andrew Reynolds
Clean up quantifiers engine initialization. (#2371)
commit
|
commitdiff
|
tree
2018-08-24
Andrew Reynolds
Fix more simple coverity warnings (#2372)
commit
|
commitdiff
|
tree
2018-08-24
Andrew Reynolds
Remove spurious disabling of cbqi-all (#2368)
commit
|
commitdiff
|
tree
2018-08-24
Andres Noetzli
Add tests that enumerate and verify rewrite rules ...
commit
|
commitdiff
|
tree
2018-08-24
Andrew Reynolds
Do not print internally generated datatypes in externa...
commit
|
commitdiff
|
tree
2018-08-24
Aina Niemetz
New C++ API: Add checks for kind arguments. (#2369)
commit
|
commitdiff
|
tree
2018-08-23
Andres Noetzli
Add missing overrides in unit tests (#2362)
commit
|
commitdiff
|
tree
2018-08-23
Tim King
Replacing allocatedInCMM and d_noTrash with false every...
commit
|
commitdiff
|
tree
2018-08-23
Haniel Barbosa
Makes the filename be set in the SMT engine by default...
commit
|
commitdiff
|
tree
2018-08-23
Andrew Reynolds
Fixing some coverity warnings (#2357)
commit
|
commitdiff
|
tree
2018-08-23
Andrew Reynolds
Fix regression requiring proof build. (#2364)
commit
|
commitdiff
|
tree
2018-08-23
Aina Niemetz
Refactor ITE simplification preprocessing pass. (#2360)
commit
|
commitdiff
|
tree
2018-08-23
Andres Noetzli
Use "filename" instead of "name" in SmtEngine::setInfo...
commit
|
commitdiff
|
tree
2018-08-23
yoni206
global-negate preprocessing pass (#2317)
commit
|
commitdiff
|
tree
2018-08-23
Andrew Reynolds
More regressions that increase coverage (#2354)
commit
|
commitdiff
|
tree
2018-08-22
Andrew Reynolds
More unused code elimination (#2358)
commit
|
commitdiff
|
tree
2018-08-22
yoni206
Generating less consistency lemmas in bv-ackermann...
commit
|
commitdiff
|
tree
2018-08-22
Tim King
Wrapping TheorySetsPrivate in a unique_ptr. (#2356)
commit
|
commitdiff
|
tree
2018-08-22
Andrew Reynolds
Fix option for real2int regression. (#2353)
commit
|
commitdiff
|
tree
2018-08-22
Haniel Barbosa
Adds regression test for automatic generation of SyGuS...
commit
|
commitdiff
|
tree
2018-08-22
Andrew Reynolds
Fix invalid iterator comparisons (#2349)
commit
|
commitdiff
|
tree
2018-08-22
Andrew Reynolds
Fix processing of nested Variable construct in sygus...
commit
|
commitdiff
|
tree
2018-08-21
Tim King
Removing unused bool members in command.cpp. Also initi...
commit
|
commitdiff
|
tree
2018-08-21
Andrew Reynolds
Warn and enable quantifiers when using sygus + logics...
commit
|
commitdiff
|
tree
2018-08-21
Haniel Barbosa
Makes the new row propagation system default (#2335)
commit
|
commitdiff
|
tree
2018-08-21
Mathias Preiner
Move d_realAssertionsEnd from SmtEnginePrivate to Asser...
commit
|
commitdiff
|
tree
2018-08-21
Tim King
Add constexpr annotations to help coverity understand...
commit
|
commitdiff
|
tree
2018-08-21
Andrew Reynolds
Use cbqi-full for sygus (#2346)
commit
|
commitdiff
|
tree
2018-08-21
Andres Noetzli
Remove support for *.expect files in regressions (...
commit
|
commitdiff
|
tree
2018-08-21
Aina Niemetz
Fix initialization of d_smt in ValidityChecker for...
commit
|
commitdiff
|
tree
2018-08-21
Aina Niemetz
Remove disabled system test cvc3_george. (#2342)
commit
|
commitdiff
|
tree
2018-08-21
Andrew Reynolds
More unused code elimination (#2339)
commit
|
commitdiff
|
tree
2018-08-20
Andrew Reynolds
Remove support for prototype (non-sygus) synthesis...
commit
|
commitdiff
|
tree
2018-08-20
Andrew Reynolds
Add regressions that increase coverage (#2337)
commit
|
commitdiff
|
tree
next