projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Decision strategy: incorporate cegis unif (#2482)
2018-09-17
Andrew Reynolds
Decision strategy: incorporate cegis unif (#2482)
commit
|
commitdiff
|
tree
2018-09-17
Andrew Reynolds
Decision strategy: incorporate bounded integers (...
commit
|
commitdiff
|
tree
2018-09-17
Andrew Reynolds
Decision strategy: incorporate datatypes sygus solver...
commit
|
commitdiff
|
tree
2018-09-17
Andrew Reynolds
More aggressive skolem caching for strings, document...
commit
|
commitdiff
|
tree
2018-09-17
Andres Noetzli
Follow redirects with cURL in contrib/get* scripts...
commit
|
commitdiff
|
tree
2018-09-17
Andres Noetzli
Remove broken dumping support from portfolio build...
commit
|
commitdiff
|
tree
2018-09-17
Andrew Reynolds
Decision strategy: incorporate sygus feasible and sygus...
commit
|
commitdiff
|
tree
2018-09-15
Andres Noetzli
Refactor how assertions are added to decision engine...
commit
|
commitdiff
|
tree
2018-09-14
Andrew Reynolds
Generalize CandidateRewriteDatabase to ExprMiner (...
commit
|
commitdiff
|
tree
2018-09-13
Mathias Preiner
Fix #include for minisat headers in bvminisat. (#2463)
commit
|
commitdiff
|
tree
2018-09-13
Haniel Barbosa
Uses information gain heuristic for building better...
commit
|
commitdiff
|
tree
2018-09-13
Andrew Reynolds
Simplify storing of transcendental function applications...
commit
|
commitdiff
|
tree
2018-09-13
Andrew Reynolds
Decision strategy: incorporate CEGQI (#2460)
commit
|
commitdiff
|
tree
2018-09-12
Aina Niemetz
New C++ API: Try to fix (false positive) Coverity warnings...
commit
|
commitdiff
|
tree
2018-09-12
Aina Niemetz
Examples: Remove obsolete flag CVC4_MAKE_EXAMPLES....
commit
|
commitdiff
|
tree
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
Andres Noetzli
Set NodeManager to nullptr when exporting vars (#2445)
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 instantiation...
commit
|
commitdiff
|
tree
2018-09-07
Mathias Preiner
Replace boost::integer_traits with std::numeric_limits...
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
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
Andrew Reynolds
Extended rewriter for string equalities (#2427)
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
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
Andrew Reynolds
Add regular expression elimination module (#2400)
commit
|
commitdiff
|
tree
2018-08-28
Andrew Reynolds
Split term canonize utility to own file and document...
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 dead code in fp_converter (#2388)
commit
|
commitdiff
|
tree
2018-08-28
Andrew Reynolds
Fix sort inference for quantified variables of interpreted...
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-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-26
Andrew Reynolds
Fix unsigned integer type issues in strings (#2380)
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
Andrew Reynolds
Do not print internally generated datatypes in external...
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
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
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
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
Andrew Reynolds
Warn and enable quantifiers when using sygus + logics...
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
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
2018-08-20
Andrew Reynolds
Minor improvements to the interface for sygus sampler...
commit
|
commitdiff
|
tree
2018-08-20
Andrew Reynolds
Make sygus inference a preprocessing pass (#2334)
commit
|
commitdiff
|
tree
2018-08-17
Andrew Reynolds
Remove support for flipDecision (#2319)
commit
|
commitdiff
|
tree
2018-08-17
Andrew Reynolds
Remove miscellaneous unused code (#2333)
commit
|
commitdiff
|
tree
2018-08-17
Andrew Reynolds
Split sygus grammar to its own ANTLR grammar (#2307)
commit
|
commitdiff
|
tree
2018-08-17
Andrew Reynolds
Fix spurious warning in sort inference (#2331)
commit
|
commitdiff
|
tree
2018-08-17
Haniel Barbosa
cleaning unnecessary timers/dumps (#2327)
commit
|
commitdiff
|
tree
2018-08-17
Haniel Barbosa
Adding support for bitvector SyGuS problems without...
commit
|
commitdiff
|
tree
2018-08-17
Andres Noetzli
Refactor IteRemoval preprocessing pass (#1793)
commit
|
commitdiff
|
tree
2018-08-16
Andrew Reynolds
Minor fixes and improvement for sygus to builtin. ...
commit
|
commitdiff
|
tree
2018-08-16
Haniel Barbosa
Refactor apply2const (#2316)
commit
|
commitdiff
|
tree
2018-08-15
Tim King
Removing attribute cleanups. (#2300)
commit
|
commitdiff
|
tree
2018-08-15
Andres Noetzli
Remove unused tuple classes (#2313)
commit
|
commitdiff
|
tree
2018-08-15
Andres Noetzli
Remove unused class DynamicArray (#2312)
commit
|
commitdiff
|
tree
2018-08-15
Andrew Reynolds
Make sort inference a preprocessing pass (#2309)
commit
|
commitdiff
|
tree
2018-08-15
Andres Noetzli
Remove unused declaration (#2310)
commit
|
commitdiff
|
tree
2018-08-14
Aina Niemetz
autotools: Remove personal builds, rename build 'default...
commit
|
commitdiff
|
tree
2018-08-14
Andres Noetzli
Fix get-unsat-assumptions output (#2301)
commit
|
commitdiff
|
tree
2018-08-13
Tim King
Removing support for T* and const T* attributes. (...
commit
|
commitdiff
|
tree
2018-08-11
Andres Noetzli
Make attributes robust to static init orderings (#2295)
commit
|
commitdiff
|
tree
2018-08-10
Aina Niemetz
Fix portfolio command executor for changes from #2240...
commit
|
commitdiff
|
tree
2018-08-10
Andres Noetzli
Do not use static initialization in CxxTest runner...
commit
|
commitdiff
|
tree
2018-08-09
Andres Noetzli
Fix documentation of regression tests (#2290)
commit
|
commitdiff
|
tree
2018-08-09
Aina Niemetz
Plug solver API object into parser. (#2240)
commit
|
commitdiff
|
tree
2018-08-09
Tim King
Fixing documentation nit from PR#2232. (#2289)
commit
|
commitdiff
|
tree
2018-08-08
Tim King
Proposal for adding map utility functions to CVC4...
commit
|
commitdiff
|
tree
2018-08-08
Andrew Reynolds
Disable argument relevance for sygus by default (#2288)
commit
|
commitdiff
|
tree
2018-08-08
Andrew Reynolds
Move uf model code from uf to quantifiers (#2095)
commit
|
commitdiff
|
tree
2018-08-08
Andres Noetzli
Require Swig 3 (#2283)
commit
|
commitdiff
|
tree
next