projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Make flat form inferences optional in strings (#2277)
2018-08-07
Andrew Reynolds
Make flat form inferences optional in strings (#2277)
commit
|
commitdiff
|
tree
2018-08-07
Andrew Reynolds
Add RegLan to smt2/sygus parsers. (#2276)
commit
|
commitdiff
|
tree
2018-08-07
Andrew Reynolds
Move sygus quantifier elimination step for non-ground...
commit
|
commitdiff
|
tree
2018-08-06
Andrew Reynolds
Fixes and improvements for single invocation inference...
commit
|
commitdiff
|
tree
2018-08-06
Andrew Reynolds
Fix degenerate case of sygus grammar construction for...
commit
|
commitdiff
|
tree
2018-08-04
Aina Niemetz
Add rewrite for nested BITVECTOR_ITE with cond_outer...
commit
|
commitdiff
|
tree
2018-08-04
Aina Niemetz
Add rewrite for BITVECTOR_ITE with const children....
commit
|
commitdiff
|
tree
2018-08-03
Aina Niemetz
Add rewrite for BITVECTOR_ITE with term_then == term_else...
commit
|
commitdiff
|
tree
2018-08-03
Andrew Reynolds
Eliminate option for sygus UF evaluation functions...
commit
|
commitdiff
|
tree
2018-08-03
Aina Niemetz
Add timer for BV inequality solver. (#2265)
commit
|
commitdiff
|
tree
2018-08-02
Andrew Reynolds
Parse standard separation logic inputs (#2257)
commit
|
commitdiff
|
tree
2018-08-02
Andrew Reynolds
Improve CEGQI heuristics involving equality and multiple...
commit
|
commitdiff
|
tree
2018-08-02
Andrew Reynolds
Fix candidate rewrite utilities for non-first-class...
commit
|
commitdiff
|
tree
2018-08-02
Aina Niemetz
Add rewrites for BITVECTOR_ITE and BITVECTOR_COMP with...
commit
|
commitdiff
|
tree
2018-08-02
Andrew Reynolds
Remove references to deprecated propagate as decision...
commit
|
commitdiff
|
tree
2018-08-02
Andrew Reynolds
Fix API call for reg exp. (#2248)
commit
|
commitdiff
|
tree
2018-08-02
Andrew Reynolds
Fix issues with printing parametric datatypes in smt2...
commit
|
commitdiff
|
tree
2018-08-01
Mathias Preiner
Fix bool-to-bv preprocessing pass for non-{bv,bool...
commit
|
commitdiff
|
tree
2018-08-01
Aina Niemetz
InteractiveShell: Remove redundant options argument...
commit
|
commitdiff
|
tree
2018-08-01
Aina Niemetz
New C++ API: Fixed ownership of options object. (#2243)
commit
|
commitdiff
|
tree
2018-08-01
Mathias Preiner
Remove hasAssertions() method from eager BV solver...
commit
|
commitdiff
|
tree
2018-07-31
Mathias Preiner
Fix option handler for lazy/bv-sat-solver combinations...
commit
|
commitdiff
|
tree
2018-07-30
Mathias Preiner
Add support for incremental eager bit-blasting. (#1838)
commit
|
commitdiff
|
tree
2018-07-27
Mathias Preiner
Require argument description for non-{bool,void} options...
commit
|
commitdiff
|
tree
2018-07-27
Andres Noetzli
Fix issues related to cxxtest in configure.ac (#2226)
commit
|
commitdiff
|
tree
2018-07-27
Mathias Preiner
Fix CryptoMiniSat config to allow system versions....
commit
|
commitdiff
|
tree
2018-07-26
yoni206
Disabling bvLazyRewriteExtf in the right place (#2214)
commit
|
commitdiff
|
tree
2018-07-26
Andrew Reynolds
Fix a few issues in the sygus sampler related to evaluation...
commit
|
commitdiff
|
tree
2018-07-26
Aina Niemetz
New C++ API: Third batch of commands (SMT-LIB). (#2212)
commit
|
commitdiff
|
tree
2018-07-26
Aina Niemetz
New C++ API: Second batch of commands (SMT-LIB). (...
commit
|
commitdiff
|
tree
2018-07-25
Andrew Reynolds
Move reg exp rewrites from prerewrite to postrewrite...
commit
|
commitdiff
|
tree
2018-07-25
Mathias Preiner
Use CryptoMiniSat 5.6.3. (#2205)
commit
|
commitdiff
|
tree
2018-07-24
Andrew Reynolds
Improvements to sets + cardinality + quantifiers (...
commit
|
commitdiff
|
tree
2018-07-24
Aina Niemetz
New C++ API: First batch of commands (SMT-LIB and...
commit
|
commitdiff
|
tree
2018-07-23
Andrew Reynolds
Improve rewriter for regular expression concatenation...
commit
|
commitdiff
|
tree
2018-07-23
Andrew Reynolds
Generalize symmetry detection for 1 symmetry variable...
commit
|
commitdiff
|
tree
2018-07-23
Aina Niemetz
New C++ API: Implementation of Solver class: OpTerm...
commit
|
commitdiff
|
tree
2018-07-23
Aina Niemetz
New C++ API: declare-datatype. (#2166)
commit
|
commitdiff
|
tree
2018-07-23
Andrew Reynolds
sygusComp2018: add regressions (#2191)
commit
|
commitdiff
|
tree
2018-07-23
Andrew Reynolds
Fix warning in sygus PBE (#2190)
commit
|
commitdiff
|
tree
2018-07-21
Andrew Reynolds
Optimizations and fixes for computing whether a type...
commit
|
commitdiff
|
tree
2018-07-21
Andrew Reynolds
sygusComp2018: refactor and improve sygus io utility...
commit
|
commitdiff
|
tree
2018-07-20
Andrew Reynolds
Cleanup and additions for candidate generator (#2173)
commit
|
commitdiff
|
tree
2018-07-20
Andrew Reynolds
sygusComp2018: minor changes to repair constant utility...
commit
|
commitdiff
|
tree
2018-07-17
Andrew Reynolds
sygusComp2018: pbe multi-enumerator fairness option...
commit
|
commitdiff
|
tree
2018-07-17
yoni206
Refactor sep-pre-skolem-emp preprocessing pass
commit
|
commitdiff
|
tree
2018-07-17
Andrew Reynolds
Minor cleanup and fixes for conflict-based instantiation...
commit
|
commitdiff
|
tree
2018-07-17
Andrew Reynolds
Do extended rewrite on results of quantifier elimination...
commit
|
commitdiff
|
tree
2018-07-17
Andrew Reynolds
Purify applications of exp to transcendental arguments...
commit
|
commitdiff
|
tree
2018-07-17
Andrew Reynolds
sygusComp2018: update policies for solution reconstruction...
commit
|
commitdiff
|
tree
2018-07-17
Andrew Reynolds
sygusComp2018: Improvements to datatypes sygus solver...
commit
|
commitdiff
|
tree
2018-07-17
Andrew Reynolds
sygusComp 2018: updates to sygus term database (#2170)
commit
|
commitdiff
|
tree
2018-07-14
Andrew Reynolds
sygusComp2018: update semantics for declare-fun in...
commit
|
commitdiff
|
tree
2018-07-13
Andrew Reynolds
Fix and improve grammar normalization for any constant...
commit
|
commitdiff
|
tree
2018-07-13
Andres Noetzli
Properly clean up assertion stack in CnfProof (#2147)
commit
|
commitdiff
|
tree
2018-07-13
Andrew Reynolds
sygusComp2018: optimization for collect model info...
commit
|
commitdiff
|
tree
2018-07-13
Aina Niemetz
New C++ API: Minor reorder. (#2163)
commit
|
commitdiff
|
tree
2018-07-13
Aina Niemetz
New C++ API: Implementation of datatype classes. (...
commit
|
commitdiff
|
tree
2018-07-13
Aina Niemetz
New C++ API: Implementation of Solver class: Consts...
commit
|
commitdiff
|
tree
2018-07-08
Andres Noetzli
Add more sophisticated floating-point sampler (#2155)
commit
|
commitdiff
|
tree
2018-07-06
Andrew Reynolds
Split ext theory to own file and document (#1809)
commit
|
commitdiff
|
tree
2018-07-06
Aina Niemetz
New C++ API: Implementation of Solver class: Sort handling...
commit
|
commitdiff
|
tree
2018-07-04
Andrew Reynolds
More cleanup in strings (#2138)
commit
|
commitdiff
|
tree
2018-07-04
Aina Niemetz
New C++ API: Implementation of datatype declaration...
commit
|
commitdiff
|
tree
2018-07-04
Aina Niemetz
New C++ API: Implementation of OpTerm. (#2132)
commit
|
commitdiff
|
tree
2018-07-03
Aina Niemetz
New C++ API: Implementation of Term. (#2131)
commit
|
commitdiff
|
tree
2018-07-03
Aina Niemetz
New C++ API: Implementation of Kind maps. (#2130)
commit
|
commitdiff
|
tree
2018-07-03
Aina Niemetz
Fix datatypes example: nil constructor was missing...
commit
|
commitdiff
|
tree
2018-07-03
Andrew Reynolds
sygusComp2018: update sygus-related options setting...
commit
|
commitdiff
|
tree
2018-07-03
Andrew Reynolds
Remove miscellaneous dead and unused code from quantifiers...
commit
|
commitdiff
|
tree
2018-07-03
Andres Noetzli
Add regression test for issue #1986 (#2114)
commit
|
commitdiff
|
tree
2018-07-02
Aina Niemetz
Refactor ApplySubsts preprocessing pass. (#2120)
commit
|
commitdiff
|
tree
2018-07-02
Aina Niemetz
New C++ API: Implementation of Sort. (#2122)
commit
|
commitdiff
|
tree
2018-07-02
Andrew Reynolds
Remove some dead code from theory strings (#2125)
commit
|
commitdiff
|
tree
2018-07-02
Andrew Reynolds
Modify cegqi heuristic for finite datatypes (#2126)
commit
|
commitdiff
|
tree
2018-07-02
Andrew Reynolds
Improve error message. (#2124)
commit
|
commitdiff
|
tree
2018-06-29
Andrew Reynolds
Use evaluator in sygus sampler. (#2117)
commit
|
commitdiff
|
tree
2018-06-29
Aina Niemetz
New C++ API: Implementation of Result. (#2112)
commit
|
commitdiff
|
tree
2018-06-28
Andrew Reynolds
sygusComp2018: optimization for invariance test (...
commit
|
commitdiff
|
tree
2018-06-28
Andres Noetzli
Fix stale reference in MiniSat when generating UC ...
commit
|
commitdiff
|
tree
2018-06-28
Andrew Reynolds
Do not rename uninterpreted constants (#2098)
commit
|
commitdiff
|
tree
2018-06-28
Andrew Reynolds
Split and document ceg theory instantiators (#2094)
commit
|
commitdiff
|
tree
2018-06-27
Aina Niemetz
Header for new C++ API. (#1697)
commit
|
commitdiff
|
tree
2018-06-27
Andrew Reynolds
Synthesize candidate-rewrites from standard inputs...
commit
|
commitdiff
|
tree
2018-06-26
Andres Noetzli
sygusComp2018: Add evaluator (#2090)
commit
|
commitdiff
|
tree
2018-06-26
Andrew Reynolds
Add casc j9 tfn script (#2100)
commit
|
commitdiff
|
tree
2018-06-26
Andrew Reynolds
Fix assertion for relational triggers (#2096)
commit
|
commitdiff
|
tree
2018-06-26
Andrew Reynolds
Do not dagify printing over binders (#2093)
commit
|
commitdiff
|
tree
2018-06-26
Andrew Reynolds
Remove unnecessary code in register quantifier internal...
commit
|
commitdiff
|
tree
2018-06-26
Andres Noetzli
Minor improvements in SMT2 and CVC printers (#2089)
commit
|
commitdiff
|
tree
2018-06-25
Andres Noetzli
Remove parentheses for prefix ops without args (#2082)
commit
|
commitdiff
|
tree
2018-06-21
Andres Noetzli
Fix warnings and enable -Wnon-virtual-dtor warning...
commit
|
commitdiff
|
tree
2018-06-21
Andres Noetzli
Check unsat cores in regressions also without LFSC...
commit
|
commitdiff
|
tree
2018-06-20
Andres Noetzli
Resolve CVC4_USE_SYMFPU in headers at config-time ...
commit
|
commitdiff
|
tree
2018-06-15
Andrew Reynolds
Disable solving non-linear BV literals by default ...
commit
|
commitdiff
|
tree
2018-06-13
Andres Noetzli
Workaround for incremental unsat cores (#1962)
commit
|
commitdiff
|
tree
2018-06-13
Andrew Reynolds
Fix simple regexp consume (#2066)
commit
|
commitdiff
|
tree
2018-06-13
Andres Noetzli
Disable unconstrainedSimp pass when proofs enabled...
commit
|
commitdiff
|
tree
2018-06-10
Andres Noetzli
Disable test that fails in competition mode (#2063)
commit
|
commitdiff
|
tree
2018-06-09
Andres Noetzli
Add flag to skip regression if feature enabled (#2062)
commit
|
commitdiff
|
tree
next