projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Expand definitions in sygus operators at the SMT level (#7077)
[cvc5.git]
/
src
/
smt
/
smt_engine.cpp
2021-08-27
Andrew Reynolds
Expand definitions in sygus operators at the SMT level...
blob
|
commitdiff
|
raw
2021-08-27
Andrew Reynolds
Add missing methods to Solver API for models (#7052)
blob
|
commitdiff
|
raw
|
diff to current
2021-08-26
Andrew Reynolds
Eliminate currentSmtEngine for subsolver calls (#7068)
blob
|
commitdiff
|
raw
|
diff to current
2021-08-26
Gereon Kremer
Consolidate language types (#7065)
blob
|
commitdiff
|
raw
|
diff to current
2021-08-20
Andrew Reynolds
Simplify how user-provided quantifier attributes are...
blob
|
commitdiff
|
raw
|
diff to current
2021-08-20
Andrew Reynolds
Eliminate eager model building (#7038)
blob
|
commitdiff
|
raw
|
diff to current
2021-08-19
Andrew Reynolds
Refactor proof output for TPTP (#7029)
blob
|
commitdiff
|
raw
|
diff to current
2021-08-18
Andrew Reynolds
Make TheoryProxy use Env, simplify initialization of...
blob
|
commitdiff
|
raw
|
diff to current
2021-08-17
Andrew Reynolds
Make SmtEngineState use Env (#7028)
blob
|
commitdiff
|
raw
|
diff to current
2021-08-17
Andrew Reynolds
Initial refactoring of set defaults (#7021)
blob
|
commitdiff
|
raw
|
diff to current
2021-08-04
Andrew Reynolds
Add optional debug information for dumping instantiatio...
blob
|
commitdiff
|
raw
|
diff to current
2021-08-04
Andrew Reynolds
Remove dependencies on smt engine in smt solver (#6965)
blob
|
commitdiff
|
raw
|
diff to current
2021-08-03
Andrew Reynolds
Remove "inUnsatCore" flag throughout (#6964)
blob
|
commitdiff
|
raw
|
diff to current
2021-08-03
Gereon Kremer
Properly honor --stats-all and --stats-expert when...
blob
|
commitdiff
|
raw
|
diff to current
2021-07-31
Gereon Kremer
Perform statistics printing via the API (#6952)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-26
Gereon Kremer
Move public options functions to separate file (#6671)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-22
Andres Noetzli
Add support for minimal unsat cores (#4605)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-15
Gereon Kremer
Remove public option wrappers (#6716)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-07
Gereon Kremer
Remove `Options::wasSetByUser()` (#6682)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-02
Gereon Kremer
Remove `Options::operator[]` (#6649)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-29
Gereon Kremer
Remove `Options::set()` method (#6556)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-26
Andres Noetzli
More precise includes of `Node` constants (#6617)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-21
Andrew Reynolds
Update to sygus standard output for check-synth respons...
blob
|
commitdiff
|
raw
|
diff to current
2021-05-20
Haniel Barbosa
Remove old unsat cores (#6581)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-19
Haniel Barbosa
Change the default unsat cores (#6571)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-13
Mathias Preiner
Add std::hash overloads for Node, TNode and TypeNode...
blob
|
commitdiff
|
raw
|
diff to current
2021-05-07
Andrew Reynolds
Simplifications to expand definitions (#6487)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-04
Andrew Reynolds
Move env into smt solver, theory engine, prop engine...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-30
Andrew Reynolds
Use substitutions for implementing defined functions...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-28
Gereon Kremer
Refactor resource manager options (#6446)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-28
Gereon Kremer
Remove exception headers from options.h (#6456)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-26
Gereon Kremer
First part of options refactoring (#6428)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-24
Mathias Preiner
Add assumption-based unsat cores. (#6427)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-22
Haniel Barbosa
Reconciling proofs and unsat cores (#6405)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-20
Gereon Kremer
Add InferenceId as resources (#6339)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-16
Gereon Kremer
Replace SExpr class by simpler conversion routines...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-15
Gereon Kremer
Avoid options listener for resource manager. (#6366)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-15
Aina Niemetz
Rename occurrences of CVC4 to CVC5. (#6351)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-14
Gereon Kremer
Refactor / reimplement statistics (#6162)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-14
Haniel Barbosa
[unsat-cores] Improving new unsat cores (#6356)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-14
Andrew Reynolds
Add internal API methods for pool-based instantiation...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-13
Abdalrhman Mohamed
Fix sexpr bug with AST output language. (#6329)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-12
Gereon Kremer
Refactor resource manager (#6322)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-12
Aina Niemetz
Refactor and update copyright headers. (#6316)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-07
Andrew Reynolds
Fixes for abducts (#6279)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-06
Andres Noetzli
Remove template argument from `NodeBuilder` (#6290)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-02
Gereon Kremer
Minor refactoring (#6273)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-01
Aina Niemetz
Rename namespace CVC5 to cvc5. (#6258)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-01
Gereon Kremer
Make ResetCommand go through APISolver (#6172)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-31
Aina Niemetz
Rename namespace CVC4 to CVC5. (#6249)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-23
Haniel Barbosa
Removing unused build options and deprecated proof...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-23
Aina Niemetz
Remove internal includes of Api header. (#6193)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-22
Gereon Kremer
Move statistics from the driver into the SmtEngine...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-18
Haniel Barbosa
When giving an SMT-LIB version, defaulting to SMT-LIB...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-18
Gereon Kremer
Move stats registry to env. (#6173)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-18
Abdalrhman Mohamed
Eliminate more uses of SExpr. (#6149)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-16
Haniel Barbosa
[proof-new] Renaming proof option to be in sync with...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-12
Andrew Reynolds
(proof-new) Miscellaneous sync to master (#6129)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-11
Aina Niemetz
Delete Expr layer. (#6117)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-10
Andrew Reynolds
Add Env class (#6093)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-09
Gereon Kremer
Some more cleanup of includes (#6083)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-09
Aina Niemetz
Update copyright headers to 2021. (#6081)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-06
Mathias Preiner
Remove SMT-LIB 2.5 and 2.0 support. (#6068)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-03
Gereon Kremer
More cleanup of includes to reduce compilation times...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-03
Abdalrhman Mohamed
Remove uses of SExpr class. (#6035)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-02
Gereon Kremer
Clean up includes to reduce compile times (#6031)
blob
|
commitdiff
|
raw
|
diff to current
2021-02-22
Andrew Reynolds
(proof-new) Change proof-new option to proof (#5955)
blob
|
commitdiff
|
raw
|
diff to current
2021-01-29
Haniel Barbosa
[proof-new] Connecting new unsat cores (#5834)
blob
|
commitdiff
|
raw
|
diff to current
2021-01-28
Andrew Reynolds
Reorganize calls to quantifiers engine from SmtEngine...
blob
|
commitdiff
|
raw
|
diff to current
2021-01-27
Andrew Reynolds
(proof-new) Improvements to quantifiers engine and...
blob
|
commitdiff
|
raw
|
diff to current
2021-01-11
Andrew Reynolds
Further simplifications in preparation for removing...
blob
|
commitdiff
|
raw
|
diff to current
2021-01-08
Haniel Barbosa
[proof-new] Implementing getProof in the API and SMT...
blob
|
commitdiff
|
raw
|
diff to current
2020-12-18
Andrew Reynolds
Simplify internal API for sygus (#5687)
blob
|
commitdiff
|
raw
|
diff to current
2020-12-16
Andrew Reynolds
Simplify synth-fun printer (#5682)
blob
|
commitdiff
|
raw
|
diff to current
2020-12-14
Andrew Reynolds
Properly implement datatype selector triggers (#5624)
blob
|
commitdiff
|
raw
|
diff to current
2020-12-12
Andrew Reynolds
Flush statistics through NodeManager in SmtEngine ...
blob
|
commitdiff
|
raw
|
diff to current
2020-12-03
Andrew Reynolds
(proof-new) Updates to SMT proof manager and SmtEngine...
blob
|
commitdiff
|
raw
|
diff to current
2020-12-02
Andrew Reynolds
Fix issues related to model declarations (#5560)
blob
|
commitdiff
|
raw
|
diff to current
2020-12-01
Andrew Reynolds
More fixes for quantifier elimination (#5533)
blob
|
commitdiff
|
raw
|
diff to current
2020-11-30
Abdalrhman Mohamed
Eliminate uses of SExpr from the parser. (#5496)
blob
|
commitdiff
|
raw
|
diff to current
2020-11-26
Andrew Reynolds
Removing infrastructure related to SMT model (#5527)
blob
|
commitdiff
|
raw
|
diff to current
2020-11-26
Andrew Reynolds
Fully decouple SmtEngine and the Expr layer (#5532)
blob
|
commitdiff
|
raw
|
diff to current
2020-11-23
Gereon Kremer
Add get-info :time. (#5485)
blob
|
commitdiff
|
raw
|
diff to current
2020-11-19
Andrew Reynolds
Enable new implementation of CEGQI based on nested...
blob
|
commitdiff
|
raw
|
diff to current
2020-11-19
Andrew Reynolds
Use symbol manager for unsat cores (#5468)
blob
|
commitdiff
|
raw
|
diff to current
2020-11-18
Andrew Reynolds
Minor cleanup of SmtEngine (#5450)
blob
|
commitdiff
|
raw
|
diff to current
2020-11-18
Andrew Reynolds
Use symbol manager for get assignment (#5451)
blob
|
commitdiff
|
raw
|
diff to current
2020-11-10
Andrew Reynolds
Add proper support for the declare-heap command for...
blob
|
commitdiff
|
raw
|
diff to current
2020-10-28
Andrew Reynolds
Remove more uses of Expr (#5357)
blob
|
commitdiff
|
raw
|
diff to current
2020-10-27
Abdalrhman Mohamed
Refactor DeclareSygusVarCommand and SynthFunCommand...
blob
|
commitdiff
|
raw
|
diff to current
2020-10-21
Abdalrhman Mohamed
Add finishInit for getInterpol and getAbduct. (#5316)
blob
|
commitdiff
|
raw
|
diff to current
2020-10-20
Andrew Reynolds
Split CheckModels utility to its own file (#5303)
blob
|
commitdiff
|
raw
|
diff to current
2020-10-19
Andrew Reynolds
(proof-new) Update preprocessing pass context for proof...
blob
|
commitdiff
|
raw
|
diff to current
2020-10-16
Andrew Reynolds
Refactor SMT-level model object (#5277)
blob
|
commitdiff
|
raw
|
diff to current
2020-10-12
Andrew Reynolds
Eliminate uses of Expr in SmtEngine interface (#5240)
blob
|
commitdiff
|
raw
|
diff to current
2020-10-10
Abdalrhman Mohamed
Provide API version of some SMT Commands. (#5222)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-30
Gereon Kremer
Remove too strict assertion to allow for approximate...
blob
|
commitdiff
|
raw
|
diff to current
2020-09-29
Andrew Reynolds
(proof-new) Fixes for preprocess proof generator and...
blob
|
commitdiff
|
raw
|
diff to current
2020-09-29
Andrew Reynolds
Reset assertions on resetAssertions (#5153)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
blob
|
commitdiff
|
raw
|
diff to current
next