projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Remove unnecessary tracing from preprocessing (#2472)
[cvc5.git]
/
src
/
smt
/
smt_engine.cpp
2018-09-17
Andres Noetzli
Remove unnecessary tracing from preprocessing (#2472)
blob
|
commitdiff
|
raw
2018-09-15
Andres Noetzli
Refactor how assertions are added to decision engine...
blob
|
commitdiff
|
raw
|
diff to current
2018-09-11
Andrew Reynolds
Support model cores via option --produce-model-cores...
blob
|
commitdiff
|
raw
|
diff to current
2018-09-11
Aina Niemetz
Refactor non-clausal simplify preprocessing pass. ...
blob
|
commitdiff
|
raw
|
diff to current
2018-09-05
Andrew Reynolds
Finer-grained inference of substitutions in incremental...
blob
|
commitdiff
|
raw
|
diff to current
2018-09-04
Aina Niemetz
Transfer ownership of learned literals from SMT engine...
blob
|
commitdiff
|
raw
|
diff to current
2018-09-04
Aina Niemetz
Fix merge mishap of #2359.
blob
|
commitdiff
|
raw
|
diff to current
2018-08-30
Mathias Preiner
Refactor theory preprocess into preprocessing pass...
blob
|
commitdiff
|
raw
|
diff to current
2018-08-29
Mathias Preiner
Refactor MipLibTrick preprocessing pass. (#2359)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-28
Aina Niemetz
Move flag needsFinish from SMT engine to circuit propag...
blob
|
commitdiff
|
raw
|
diff to current
2018-08-26
Andres Noetzli
Refactor unconstrained simplification pass (#2374)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-25
yoni206
Refactor quantifier macros preprocessing pass (#1840)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-25
Haniel Barbosa
Refactor nlExtPurify preprocessing pass (#1963)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-24
Andrew Reynolds
Remove spurious disabling of cbqi-all (#2368)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-24
Andrew Reynolds
Do not print internally generated datatypes in externa...
blob
|
commitdiff
|
raw
|
diff to current
2018-08-23
Haniel Barbosa
Makes the filename be set in the SMT engine by default...
blob
|
commitdiff
|
raw
|
diff to current
2018-08-23
Aina Niemetz
Refactor ITE simplification preprocessing pass. (#2360)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-23
Andres Noetzli
Use "filename" instead of "name" in SmtEngine::setInfo...
blob
|
commitdiff
|
raw
|
diff to current
2018-08-23
yoni206
global-negate preprocessing pass (#2317)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-21
Tim King
Removing unused bool members in command.cpp. Also initi...
blob
|
commitdiff
|
raw
|
diff to current
2018-08-21
Mathias Preiner
Move d_realAssertionsEnd from SmtEnginePrivate to Asser...
blob
|
commitdiff
|
raw
|
diff to current
2018-08-21
Andrew Reynolds
Use cbqi-full for sygus (#2346)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-20
Andrew Reynolds
Make sygus inference a preprocessing pass (#2334)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-17
Andrew Reynolds
Eliminate partial operators in sygus grammar normaliza...
blob
|
commitdiff
|
raw
|
diff to current
2018-08-17
Mathias Preiner
Refactor eager atoms preprocessing pass. (#2318)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-17
Haniel Barbosa
cleaning unnecessary timers/dumps (#2327)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-17
Caleb Donovick
Make quantifiers-preprocess preprocessing pass (#2322)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-17
Andres Noetzli
Refactor IteRemoval preprocessing pass (#1793)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-16
Haniel Barbosa
Refactor extended rewriter preprocessing pass (#2324)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-16
Haniel Barbosa
Refactor apply2const (#2316)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-15
Andres Noetzli
Remove unused tuple classes (#2313)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-15
Andrew Reynolds
Make sort inference a preprocessing pass (#2309)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-15
Andres Noetzli
Fix dumping of get-unsat-assumptions (#2302)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-08
Andrew Reynolds
Do beta-reduction in expandDefinitions (#2286)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-07
Andrew Reynolds
Move sygus quantifier elimination step for non-ground...
blob
|
commitdiff
|
raw
|
diff to current
2018-08-06
Andrew Reynolds
Fixes for sygus inference (#2238)
blob
|
commitdiff
|
raw
|
diff to current
2018-08-02
Andrew Reynolds
Fix issues with printing parametric datatypes in smt2...
blob
|
commitdiff
|
raw
|
diff to current
2018-08-01
ayveejay
Improvements and tests for the API around separation...
blob
|
commitdiff
|
raw
|
diff to current
2018-07-31
Mathias Preiner
Fix option handler for lazy/bv-sat-solver combinations...
blob
|
commitdiff
|
raw
|
diff to current
2018-07-30
Mathias Preiner
Add support for incremental eager bit-blasting. (#1838)
blob
|
commitdiff
|
raw
|
diff to current
2018-07-27
Andrew Reynolds
Make check-synth robust for assertions that are not...
blob
|
commitdiff
|
raw
|
diff to current
2018-07-26
yoni206
Disabling bvLazyRewriteExtf in the right place (#2214)
blob
|
commitdiff
|
raw
|
diff to current
2018-07-25
ayveejay
Performing clang-format on the original change-set...
blob
|
commitdiff
|
raw
|
diff to current
2018-07-24
ayveejay
Adding API access methods to get heap/nil expressions...
blob
|
commitdiff
|
raw
|
diff to current
2018-07-23
Andrew Reynolds
Generalize symmetry detection for 1 symmetry variable...
blob
|
commitdiff
|
raw
|
diff to current
2018-07-17
yoni206
Refactor sep-pre-skolem-emp preprocessing pass
blob
|
commitdiff
|
raw
|
diff to current
2018-07-17
Andrew Reynolds
Do extended rewrite on results of quantifier eliminatio...
blob
|
commitdiff
|
raw
|
diff to current
2018-07-11
Caleb Donovick
Move rewrite to pass (#2128)
blob
|
commitdiff
|
raw
|
diff to current
2018-07-03
Andrew Reynolds
sygusComp2018: update sygus-related options setting...
blob
|
commitdiff
|
raw
|
diff to current
2018-07-03
Andrew Reynolds
Remove miscellaneous dead and unused code from quantifi...
blob
|
commitdiff
|
raw
|
diff to current
2018-07-02
Aina Niemetz
Refactor ApplySubsts preprocessing pass. (#2120)
blob
|
commitdiff
|
raw
|
diff to current
2018-07-02
Caleb Donovick
Add missing include (#2127)
blob
|
commitdiff
|
raw
|
diff to current
2018-06-27
Andrew Reynolds
Synthesize candidate-rewrites from standard inputs...
blob
|
commitdiff
|
raw
|
diff to current
2018-06-26
Andrew Reynolds
Disable uf symmetry breaker in incremental mode (...
blob
|
commitdiff
|
raw
|
diff to current
2018-06-13
Andres Noetzli
Disable unconstrainedSimp pass when proofs enabled...
blob
|
commitdiff
|
raw
|
diff to current
2018-06-09
Andres Noetzli
Reset decisions at SAT level after solving (#2059)
blob
|
commitdiff
|
raw
|
diff to current
2018-06-04
Andrew Reynolds
Enable cegqi (with model values) for floating point...
blob
|
commitdiff
|
raw
|
diff to current
2018-05-30
Aina Niemetz
Ignore license key in set-info command. (#2021)
blob
|
commitdiff
|
raw
|
diff to current
2018-05-30
Andrew Reynolds
Fixes for quantifiers + incremental (#2009)
blob
|
commitdiff
|
raw
|
diff to current
2018-05-29
Andres Noetzli
Make user's SMT2 version override file version (#2004)
blob
|
commitdiff
|
raw
|
diff to current
2018-05-29
Andrew Reynolds
Disable minisat elimination when nonlinear is enabled...
blob
|
commitdiff
|
raw
|
diff to current
2018-05-23
Andrew Reynolds
Add notions of evaluated kinds in TheoryModel (#1947)
blob
|
commitdiff
|
raw
|
diff to current
2018-05-23
Andres Noetzli
Set same options for proofs as for unsat cores (#1957)
blob
|
commitdiff
|
raw
|
diff to current
2018-05-22
Andres Noetzli
Disable symmetry breaker for unsat cores (#1958)
blob
|
commitdiff
|
raw
|
diff to current
2018-05-22
Andrew Reynolds
Make sygus infer find function definitions (#1951)
blob
|
commitdiff
|
raw
|
diff to current
2018-05-16
yoni206
Refactor static learning preprocessing pass (#1857)
blob
|
commitdiff
|
raw
|
diff to current
2018-05-15
Andrew Reynolds
Minor improvements to --nl-ext-purify (#1896)
blob
|
commitdiff
|
raw
|
diff to current
2018-05-11
Aina Niemetz
Fix ackermannize preprocessing pass. (#1904)
blob
|
commitdiff
|
raw
|
diff to current
2018-05-10
Andrew Reynolds
Sygus repair constants (#1812)
blob
|
commitdiff
|
raw
|
diff to current
2018-05-10
Aina Niemetz
Refactored BVAckermann preprocessing pass. (#1889)
blob
|
commitdiff
|
raw
|
diff to current
2018-05-09
Andrew Reynolds
Better option names for PBE (#1891)
blob
|
commitdiff
|
raw
|
diff to current
2018-05-09
Andrew Reynolds
Make symmetry-breaker-exp into a preprocessing pass...
blob
|
commitdiff
|
raw
|
diff to current
2018-05-09
PaulMeng
Add the symmetry breaker module (#1847)
blob
|
commitdiff
|
raw
|
diff to current
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
next