projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Add the symmetry breaker module (#1847)
[cvc5.git]
/
src
/
smt
/
smt_engine.cpp
2018-05-09
PaulMeng
Add the symmetry breaker module (#1847)
blob
|
commitdiff
|
raw
2018-05-08
Mathias Preiner
Refactor bv-abstraction preprocessing pass. (#1860)
blob
|
commitdiff
|
raw
|
diff to current
2018-05-08
Andrew Reynolds
Infrastructure for approximations in model output ...
blob
|
commitdiff
|
raw
|
diff to current
2018-05-08
Aina Niemetz
Fix order of preprocessing pass registration. (#1887)
blob
|
commitdiff
|
raw
|
diff to current
2018-05-04
Mathias Preiner
Refactor bv-intro-pow2 preprocessing pass. (#1851)
blob
|
commitdiff
|
raw
|
diff to current
2018-05-03
Mathias Preiner
Fix redundant internalPush calls. (#1865)
blob
|
commitdiff
|
raw
|
diff to current
2018-05-03
Andrew Reynolds
Option to interleave tangent plane inferences (#1833)
blob
|
commitdiff
|
raw
|
diff to current
2018-05-03
Andrew Reynolds
Initial support for string standard in smt lib 2.6...
blob
|
commitdiff
|
raw
|
diff to current
2018-04-30
Haniel Barbosa
Refactor real2int (#1813)
blob
|
commitdiff
|
raw
|
diff to current
2018-04-30
Andrew Reynolds
Remove subsort symmetry breaking (#1807)
blob
|
commitdiff
|
raw
|
diff to current
2018-04-25
yoni206
Refactor bv-to-bool and bool-to-bv preprocessing passes...
blob
|
commitdiff
|
raw
|
diff to current
2018-04-25
Andrew Reynolds
Add benchmark requiring subgoal generation with inducti...
blob
|
commitdiff
|
raw
|
diff to current
2018-04-20
yoni206
Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv...
blob
|
commitdiff
|
raw
|
diff to current
2018-04-20
PaulMeng
Symmetry detection module (#1749)
blob
|
commitdiff
|
raw
|
diff to current
2018-04-19
Andres Noetzli
Refactor pbRewrites preprocessing pass (#1767)
blob
|
commitdiff
|
raw
|
diff to current
2018-04-14
yoni206
allowing --bool-to-bv without quantifiers (#1771)
blob
|
commitdiff
|
raw
|
diff to current
2018-04-11
Aina Niemetz
Refactored BVGauss preprocessing pass. (#1766)
blob
|
commitdiff
|
raw
|
diff to current
2018-04-10
Andrew Reynolds
Improve accuracy of stats for sygus sampler (#1755)
blob
|
commitdiff
|
raw
|
diff to current
2018-04-10
Aina Niemetz
Fix dumping of benchmark in SmtEngine::checkSatisfiabil...
blob
|
commitdiff
|
raw
|
diff to current
2018-04-05
Mathias Preiner
Add more general SignExtendUltConst rewriting. (#1385)
blob
|
commitdiff
|
raw
|
diff to current
2018-04-04
Andres Noetzli
Refactor IntToBV preprocessing pass (#1716)
blob
|
commitdiff
|
raw
|
diff to current
2018-04-04
Andrew Reynolds
Option to turn arbitrary input into sygus (#1704)
blob
|
commitdiff
|
raw
|
diff to current
2018-04-02
Clark Barrett
Remove references to nyu (#1721)
blob
|
commitdiff
|
raw
|
diff to current
2018-03-26
Andrew Reynolds
Check model only when sat (#1694)
blob
|
commitdiff
|
raw
|
diff to current
2018-03-09
Aina Niemetz
Add support for SMT-LIB v2.5 command get-unsat-assumpti...
blob
|
commitdiff
|
raw
|
diff to current
2018-03-07
Mathias Preiner
Make statistics output consistent. (#1647)
blob
|
commitdiff
|
raw
|
diff to current
2018-03-05
Mathias Preiner
Enable -Wsuggest-override by default. (#1643)
blob
|
commitdiff
|
raw
|
diff to current
2018-03-05
Aina Niemetz
Add support for check-sat-assuming. (#1637)
blob
|
commitdiff
|
raw
|
diff to current
2018-02-28
Aina Niemetz
SmtEngine::getAssignment now returns a vector of assign...
blob
|
commitdiff
|
raw
|
diff to current
2018-02-14
Andrew Reynolds
Quantifiers subdirectories (#1608)
blob
|
commitdiff
|
raw
|
diff to current
2018-02-13
Andrew Reynolds
Option to use extended rewriter as a preprocessing...
blob
|
commitdiff
|
raw
|
diff to current
2018-02-08
Andrew Reynolds
Minor improvements to sygus sampling. (#1577)
blob
|
commitdiff
|
raw
|
diff to current
2018-02-02
Haniel Barbosa
Option to check solutions produced by SyGuS solver...
blob
|
commitdiff
|
raw
|
diff to current
2018-02-01
Andrew Reynolds
Use sygus to synthesize/verify rewrite rules (#1547)
blob
|
commitdiff
|
raw
|
diff to current
2018-01-25
Tim King
Commenting out throw specifiers on SmtEngine. These...
blob
|
commitdiff
|
raw
|
diff to current
2018-01-22
Andrew Reynolds
Only push/pop around check-sat if it is associated...
blob
|
commitdiff
|
raw
|
diff to current
2018-01-09
Aina Niemetz
Reorganized bitvector.h. (#1505)
blob
|
commitdiff
|
raw
|
diff to current
2018-01-03
Andrew Reynolds
Global negate (#1466)
blob
|
commitdiff
|
raw
|
diff to current
2017-12-27
Andrew Reynolds
Disable sygus PBE when sygus stream is enabled (#1451)
blob
|
commitdiff
|
raw
|
diff to current
2017-12-21
Andrew Reynolds
Fixes for cbqi-bv (#1449)
blob
|
commitdiff
|
raw
|
diff to current
2017-12-11
justinxu421
Add new infrastructure for preprocessing passes (#1053)
blob
|
commitdiff
|
raw
|
diff to current
2017-12-07
Andrew Reynolds
Fixes related to SyGuS + real arithmetic (#1432)
blob
|
commitdiff
|
raw
|
diff to current
2017-12-07
Andrew Reynolds
Add command for define-fun-rec and add to API (#1412)
blob
|
commitdiff
|
raw
|
diff to current
2017-12-01
Andres Noetzli
Fix reset-assertions (#1413)
blob
|
commitdiff
|
raw
|
diff to current
2017-11-30
Aina Niemetz
Add Gaussian Elimination as a preprocessing pass for...
blob
|
commitdiff
|
raw
|
diff to current
2017-11-30
Andrew Reynolds
Minor improvements and changes to defaults for cbqi...
blob
|
commitdiff
|
raw
|
diff to current
2017-11-28
Andrew Reynolds
Fix models for --solve-real-as-int. (#1371)
blob
|
commitdiff
|
raw
|
diff to current
2017-11-17
Andrew Reynolds
(Refactor) Document and clean single invocation partiti...
blob
|
commitdiff
|
raw
|
diff to current
2017-11-17
Aina Niemetz
Add random number generator. (#1370)
blob
|
commitdiff
|
raw
|
diff to current
2017-11-16
Andrew Reynolds
(Refactor) Arithmetic monomial sum (#1381)
blob
|
commitdiff
|
raw
|
diff to current
2017-11-15
Tim King
Adding garbage collection for Proof objects. (#1294)
blob
|
commitdiff
|
raw
|
diff to current
2017-11-13
Andrew Reynolds
Disable sygus qe preprocessing by default (#1353)
blob
|
commitdiff
|
raw
|
diff to current
2017-11-09
Andrew Reynolds
Higher-order prep (#1338)
blob
|
commitdiff
|
raw
|
diff to current
2017-11-07
Andrew Reynolds
Allow FORALL in quantifier elimination command (#1322)
blob
|
commitdiff
|
raw
|
diff to current
2017-11-03
Andrew Reynolds
Sygus clean main (#1297)
blob
|
commitdiff
|
raw
|
diff to current
2017-10-28
Andres Noetzli
Change bvudiv semantics based on input language (#1292)
blob
|
commitdiff
|
raw
|
diff to current
2017-10-24
Aina Niemetz
CBQI BV: Add ULT/SLT inverse handling. (#1268)
blob
|
commitdiff
|
raw
|
diff to current
2017-10-20
Andrew Reynolds
Make Sygus conjectures higher-order (#1244)
blob
|
commitdiff
|
raw
|
diff to current
2017-10-17
Clark Barrett
Fix for issue 1247 (#1257)
blob
|
commitdiff
|
raw
|
diff to current
2017-10-11
Andrew Reynolds
Ho Lambda Lifting (#1116)
blob
|
commitdiff
|
raw
|
diff to current
2017-10-11
Andrew Reynolds
Move unsat core names to smt engine (#1192)
blob
|
commitdiff
|
raw
|
diff to current
2017-10-10
Andrew Reynolds
Split term database (#1206)
blob
|
commitdiff
|
raw
|
diff to current
2017-09-19
Andres Noetzli
Fix issue #1074, improve non-fatal error handling ...
blob
|
commitdiff
|
raw
|
diff to current
2017-09-14
Tim King
Simplifying the throw specifier of SmtEngine::checkSat...
blob
|
commitdiff
|
raw
|
diff to current
2017-09-14
Martin
Floating point symfpu support (#1093)
blob
|
commitdiff
|
raw
|
diff to current
2017-09-10
Andrew Reynolds
Ensure that expand definitions is called on all non...
blob
|
commitdiff
|
raw
|
diff to current
2017-08-24
Andrew Reynolds
Merge pull request #191 from timothy-king/cleanup-regexp
blob
|
commitdiff
|
raw
|
diff to current
2017-08-24
Andres Noetzli
Fix typos
blob
|
commitdiff
|
raw
|
diff to current
2017-08-07
ajreynol
Make quantifier elimination more robust to preprocessing.
blob
|
commitdiff
|
raw
|
diff to current
2017-07-21
Tim King
Merge branch 'master' into cleanup-regexp
blob
|
commitdiff
|
raw
|
diff to current
2017-07-21
Tim King
Moving from the gnu extensions for hash maps to the...
blob
|
commitdiff
|
raw
|
diff to current
2017-07-20
Tim King
Removing the unused CDAttribute. This makes CDHashMap...
blob
|
commitdiff
|
raw
|
diff to current
2017-07-13
Aina Niemetz
Merge pull request #188 from aniemetz/cx11
blob
|
commitdiff
|
raw
|
diff to current
2017-07-12
ajreynol
Make type rules more strict for operators whose type...
blob
|
commitdiff
|
raw
|
diff to current
2017-07-10
ajreynol
Do not exit when value/model/unsat-core/proof is reques...
blob
|
commitdiff
|
raw
|
diff to current
2017-07-10
ajreynol
Merge datatype shared selectors/sygus comp 2017 branch...
blob
|
commitdiff
|
raw
|
diff to current
2017-07-07
Mathias Preiner
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2017-05-31
ajreynol
Fix model construction for BV with cbqi. Minor change...
blob
|
commitdiff
|
raw
|
diff to current
2017-05-31
ajreynol
Minor change to defaults, update smt comp script, minor...
blob
|
commitdiff
|
raw
|
diff to current
2017-05-12
Andres Notzli
Make signal handlers safer
blob
|
commitdiff
|
raw
|
diff to current
2017-05-05
ajreynol
Do not eliminate extended arithmetic symbols when finit...
blob
|
commitdiff
|
raw
|
diff to current
2017-05-04
guykatzz
fixing bug 790: track dependencies when the unsatCores...
blob
|
commitdiff
|
raw
|
diff to current
2017-04-22
Clark Barrett
Merge pull request #151 from 4tXJ7f/fix_debug
blob
|
commitdiff
|
raw
|
diff to current
2017-04-21
Andres Noetzli
Move assertion out of loop for better performance
blob
|
commitdiff
|
raw
|
diff to current
2017-04-20
Andrew Reynolds
Merge pull request #149 from PaulMeng/master
blob
|
commitdiff
|
raw
|
diff to current
2017-04-20
ajreynol
Minor fixes.
blob
|
commitdiff
|
raw
|
diff to current
2017-04-14
ajreynol
Fix for fmf-fun when the option is set by user command.
blob
|
commitdiff
|
raw
|
diff to current
2017-04-12
ajreynol
Add nullary operator metakind.
blob
|
commitdiff
|
raw
|
diff to current
2017-04-07
ajreynol
Change option names for nl.
blob
|
commitdiff
|
raw
|
diff to current
2017-04-04
Clark Barrett
Merge pull request #141 from 4tXJ7f/remove_def
blob
|
commitdiff
|
raw
|
diff to current
2017-04-03
Andrew Reynolds
Merge pull request #142 from timothy-king/nlAlgMerge
blob
|
commitdiff
|
raw
|
diff to current
2017-04-03
Tim King
Adding a model based axiom instantiation scheme for...
blob
|
commitdiff
|
raw
|
diff to current
2017-03-30
Clark Barrett
Merge pull request #139 from 4tXJ7f/remove_throw
blob
|
commitdiff
|
raw
|
diff to current
2017-03-30
Andres Notzli
[Coverity] Remove throw qualifiers in src/smt
blob
|
commitdiff
|
raw
|
diff to current
2017-03-24
ajreynol
Refactor model building for quantifiers to be a single...
blob
|
commitdiff
|
raw
|
diff to current
2017-03-23
Clark Barrett
Fixing warning message.
blob
|
commitdiff
|
raw
|
diff to current
2017-03-23
guykatzz
support incremental unsat cores
blob
|
commitdiff
|
raw
|
diff to current
2017-03-16
ajreynol
Minor fixes, always expand applications of lambdas...
blob
|
commitdiff
|
raw
|
diff to current
2017-03-16
ajreynol
Parsing support for SMT LIB 2.6. Minor fixes for printi...
blob
|
commitdiff
|
raw
|
diff to current
2017-03-06
Clark Barrett
Adding support for bool-to-bv
blob
|
commitdiff
|
raw
|
diff to current
next