projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Removing infrastructure related to SMT model (#5527)
[cvc5.git]
/
src
/
smt
/
2020-11-26
Andrew Reynolds
Removing infrastructure related to SMT model (#5527)
tree
|
commitdiff
2020-11-26
Andrew Reynolds
Move expand definitions to its own file (#5528)
tree
|
commitdiff
2020-11-26
Andrew Reynolds
Fully decouple SmtEngine and the Expr layer (#5532)
tree
|
commitdiff
2020-11-25
Andrew Reynolds
Use symbol manager for printing responses get-model...
tree
|
commitdiff
2020-11-23
Andrew Reynolds
(proof-new) Miscellaneous changes from proof-new (...
tree
|
commitdiff
2020-11-23
Andrew Reynolds
Add declare model symbol methods to SymbolManager and...
tree
|
commitdiff
2020-11-23
Gereon Kremer
Add get-info :time. (#5485)
tree
|
commitdiff
2020-11-20
Andrew Reynolds
Fix remove term formula policy for terms beneath quanti...
tree
|
commitdiff
2020-11-20
Andrew Reynolds
Support nested quantifier elimination for get-qe comman...
tree
|
commitdiff
2020-11-20
Gereon Kremer
(proof-new) Replace LazyCDProofSet by generic CDProofSe...
tree
|
commitdiff
2020-11-19
Andrew Reynolds
Enable new implementation of CEGQI based on nested...
tree
|
commitdiff
2020-11-19
Andrew Reynolds
Use symbol manager for unsat cores (#5468)
tree
|
commitdiff
2020-11-18
Andrew Reynolds
Minor cleanup of SmtEngine (#5450)
tree
|
commitdiff
2020-11-18
Andrew Reynolds
Do not expand definitions of extended arithmetic operat...
tree
|
commitdiff
2020-11-18
Andrew Reynolds
Use symbol manager for get assignment (#5451)
tree
|
commitdiff
2020-11-12
Andrew Reynolds
Fix printing of define named function (#5425)
tree
|
commitdiff
2020-11-12
Andrew Reynolds
(proof-new) Improve printing and debugging for pedantic...
tree
|
commitdiff
2020-11-11
Andrew Reynolds
Move symbol manager to src/expr/ (#5420)
tree
|
commitdiff
2020-11-11
Andrew Reynolds
Pass symbol manager to commands (#5410)
tree
|
commitdiff
2020-11-10
Andrew Reynolds
Do not mark extended functions as reduced based on...
tree
|
commitdiff
2020-11-10
Andrew Reynolds
Add proper support for the declare-heap command for...
tree
|
commitdiff
2020-11-09
Andrew Reynolds
Simplify handling of subtypes in smt2 printer (#5401)
tree
|
commitdiff
2020-11-06
Andrew Reynolds
Simplify printing with respect to expression types...
tree
|
commitdiff
2020-10-30
Andrew Reynolds
Update api::Sort to use TypeNode instead of Type (...
tree
|
commitdiff
2020-10-28
Andrew Reynolds
Remove more uses of Expr (#5357)
tree
|
commitdiff
2020-10-27
Abdalrhman Mohamed
Refactor DeclareSygusVarCommand and SynthFunCommand...
tree
|
commitdiff
2020-10-27
Gereon Kremer
Disable --nl-cad option by default (#5350)
tree
|
commitdiff
2020-10-27
Gereon Kremer
Enable --nl-cad by default (#5345)
tree
|
commitdiff
2020-10-22
Gereon Kremer
Use theoryof-mode=type for QF_NRA (#5326)
tree
|
commitdiff
2020-10-21
Abdalrhman Mohamed
Add finishInit for getInterpol and getAbduct. (#5316)
tree
|
commitdiff
2020-10-21
Andrew Reynolds
(proof-new) Fixes for proofs in rewriter (#5307)
tree
|
commitdiff
2020-10-20
Andrew Reynolds
(proof-new) Update add lazy step interface in LazyCDPro...
tree
|
commitdiff
2020-10-20
Abdalrhman Mohamed
Remove some Commands from the API. (#5268)
tree
|
commitdiff
2020-10-20
Andrew Reynolds
Fix miscellaneous warnings (#5256)
tree
|
commitdiff
2020-10-20
Andrew Reynolds
Split CheckModels utility to its own file (#5303)
tree
|
commitdiff
2020-10-19
Andrew Reynolds
(proof-new) Updates to assertions pipeline and preproce...
tree
|
commitdiff
2020-10-19
Andrew Reynolds
(proof-new) Update preprocessing pass context for proof...
tree
|
commitdiff
2020-10-18
Andrew Reynolds
(proof-new) Witness axiom reconstruction for purificat...
tree
|
commitdiff
2020-10-18
Andrew Reynolds
(proof-new) More features for SMT proof post-processor...
tree
|
commitdiff
2020-10-16
Andrew Reynolds
Refactor SMT-level model object (#5277)
tree
|
commitdiff
2020-10-14
Andrew Reynolds
(proof-new) Generalize preprocess proof generator ...
tree
|
commitdiff
2020-10-12
Andrew Reynolds
Eliminate uses of Expr in SmtEngine interface (#5240)
tree
|
commitdiff
2020-10-12
Andrew Reynolds
Ensure uninterpreted sort owner is UF if uf-ho or finit...
tree
|
commitdiff
2020-10-10
Abdalrhman Mohamed
Provide API version of some SMT Commands. (#5222)
tree
|
commitdiff
2020-10-09
Andrew Reynolds
(proof-new) Theory engine proof producing (#5195)
tree
|
commitdiff
2020-10-08
Andrew Reynolds
(proof-new) Fixes and improvements for smt proof postpr...
tree
|
commitdiff
2020-10-06
yoni206
bv-to-int: change order of passes (#5208)
tree
|
commitdiff
2020-10-06
Abdalrhman Mohamed
Recover from some exceptions. (#5203)
tree
|
commitdiff
2020-10-05
Andrew Reynolds
Make sygus more robust to unknown responses in solution...
tree
|
commitdiff
2020-10-02
Andrew Reynolds
(proof-new) Fixes for theory preprocessing proofs ...
tree
|
commitdiff
2020-10-02
Gereon Kremer
Allow for theory combination of strings with nonlinear...
tree
|
commitdiff
2020-10-01
Andrew Reynolds
(proof-new) Preprocessing passes use proper interfaces...
tree
|
commitdiff
2020-10-01
Andrew Reynolds
Make SygusSolver use sygus attributes directly (#5172)
tree
|
commitdiff
2020-09-30
Gereon Kremer
Remove too strict assertion to allow for approximate...
tree
|
commitdiff
2020-09-29
Andrew Reynolds
(proof-new) Fixes for preprocess proof generator and...
tree
|
commitdiff
2020-09-29
Haniel Barbosa
[proof-new] Updates to proof node updater (#5156)
tree
|
commitdiff
2020-09-29
Andrew Reynolds
Reset assertions on resetAssertions (#5153)
tree
|
commitdiff
2020-09-24
Andrew Reynolds
Function definition fmf preprocessing pass (#5064)
tree
|
commitdiff
2020-09-23
Andrew Reynolds
Disable cegqi-bv when using sygus (#5124)
tree
|
commitdiff
2020-09-23
Andrew Reynolds
Allow E-matching by default when strings are enabled...
tree
|
commitdiff
2020-09-23
Abdalrhman Mohamed
Refactor Commands to use the Public API. (#5105)
tree
|
commitdiff
2020-09-23
Andrew Reynolds
Fix type issue with term formula removal (#5107)
tree
|
commitdiff
2020-09-22
Mathias Preiner
Add simple BV solver (#5065)
tree
|
commitdiff
2020-09-22
mudathirmahgoub
Add skeleton for theory of bags (multisets) (#5100)
tree
|
commitdiff
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
tree
|
commitdiff
2020-09-18
Andrew Reynolds
Fix assertion list for globally defined recursive funct...
tree
|
commitdiff
2020-09-18
Andres Noetzli
Fix muzzled builds (#5093)
tree
|
commitdiff
2020-09-18
Andrew Reynolds
(proof-new) Updates to proof node updater algorithm...
tree
|
commitdiff
2020-09-18
Andrew Reynolds
(proof-new) Rewrites involving operators in term conver...
tree
|
commitdiff
2020-09-17
Andrew Reynolds
Reduce recursion in term formula removal (#5052)
tree
|
commitdiff
2020-09-17
yoni206
Dumping internal define-funs with no arguments (#5077)
tree
|
commitdiff
2020-09-16
Abdalrhman Mohamed
Dump commands in internal code using command printing...
tree
|
commitdiff
2020-09-15
Ying Sheng
Interpolation: Add implementation for SyGuS interpolati...
tree
|
commitdiff
2020-09-12
Andrew Reynolds
(proof-new) Add SMT proof manager (#5054)
tree
|
commitdiff
2020-09-09
Andrew Reynolds
(proof-new) Minor changes to proof node updater (#5011)
tree
|
commitdiff
2020-09-09
Andrew Reynolds
(proof-new) Make proofs in term formula removal term...
tree
|
commitdiff
2020-09-08
Andres Noetzli
Make CVC/API BV div/mod semantics match SMT-LIB (#4997)
tree
|
commitdiff
2020-09-08
Andrew Reynolds
Eliminate a custom use of TheorySep in quantifiers...
tree
|
commitdiff
2020-09-04
Abdalrhman Mohamed
Use Result::Sat instead of BenchmarkStatus in printers...
tree
|
commitdiff
2020-09-02
Abdalrhman Mohamed
Introduce an internal version of Commands. (#4988)
tree
|
commitdiff
2020-09-01
Haniel Barbosa
Removes old proof code (#4964)
tree
|
commitdiff
2020-09-01
FabianWolff
Fix spelling errors (#4977)
tree
|
commitdiff
2020-08-28
yoni206
Incremental support for bv_to_int (#4967)
tree
|
commitdiff
2020-08-28
Andrew Reynolds
(proof-new) Add the SMT proof post processor (#4913)
tree
|
commitdiff
2020-08-26
Andrew Reynolds
Replace Expr-level datatype with Node-level DType ...
tree
|
commitdiff
2020-08-25
Haniel Barbosa
Eliminating spurious replay of commands for define...
tree
|
commitdiff
2020-08-22
Andrew Reynolds
Remove unecessary theory model builder base class ...
tree
|
commitdiff
2020-08-21
Andrew Reynolds
Connect the relevance manager to TheoryEngine and use...
tree
|
commitdiff
2020-08-21
Andrew Reynolds
Remove BV equality slicer (#4928)
tree
|
commitdiff
2020-08-20
Andrew Reynolds
Split QuantElimSolver from SmtEngine (#4919)
tree
|
commitdiff
2020-08-19
Gereon Kremer
Fix SmtEngine::reset() (#4917)
tree
|
commitdiff
2020-08-18
Abdalrhman Mohamed
Refactor functions that print commands (Part 2) (#4905)
tree
|
commitdiff
2020-08-18
Andrew Reynolds
(proof-new) SMT proof postprocess callback (#4883)
tree
|
commitdiff
2020-08-18
Andrew Reynolds
Split SygusSolver from SmtEngine (#4891)
tree
|
commitdiff
2020-08-15
Andrew Reynolds
Add finishInit method to PropEngine (#4895)
tree
|
commitdiff
2020-08-13
Andrew Reynolds
Split SmtSolver from SmtEngine (#4880)
tree
|
commitdiff
2020-08-13
Andrew Reynolds
More basic fix for dumping synth-fun (#4886)
tree
|
commitdiff
2020-08-12
Abdalrhman Mohamed
Refactor functions that print commands (Part 1) (#4869)
tree
|
commitdiff
2020-08-12
Andrew Reynolds
(proof-new) Improve interfaces to proof generators...
tree
|
commitdiff
2020-08-12
Andrew Reynolds
(proof-new) Witness form proof generator (#4782)
tree
|
commitdiff
next