projects / cvc5.git / history
? search:
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 ReynoldsExpand definitions in sygus operators at the SMT level... blob | commitdiff | raw
2021-08-27 Andrew ReynoldsAdd missing methods to Solver API for models (#7052) blob | commitdiff | raw | diff to current
2021-08-26 Andrew ReynoldsEliminate currentSmtEngine for subsolver calls (#7068) blob | commitdiff | raw | diff to current
2021-08-26 Gereon KremerConsolidate language types (#7065) blob | commitdiff | raw | diff to current
2021-08-20 Andrew ReynoldsSimplify how user-provided quantifier attributes are... blob | commitdiff | raw | diff to current
2021-08-20 Andrew ReynoldsEliminate eager model building (#7038) blob | commitdiff | raw | diff to current
2021-08-19 Andrew ReynoldsRefactor proof output for TPTP (#7029) blob | commitdiff | raw | diff to current
2021-08-18 Andrew ReynoldsMake TheoryProxy use Env, simplify initialization of... blob | commitdiff | raw | diff to current
2021-08-17 Andrew ReynoldsMake SmtEngineState use Env (#7028) blob | commitdiff | raw | diff to current
2021-08-17 Andrew ReynoldsInitial refactoring of set defaults (#7021) blob | commitdiff | raw | diff to current
2021-08-04 Andrew ReynoldsAdd optional debug information for dumping instantiatio... blob | commitdiff | raw | diff to current
2021-08-04 Andrew ReynoldsRemove dependencies on smt engine in smt solver (#6965) blob | commitdiff | raw | diff to current
2021-08-03 Andrew ReynoldsRemove "inUnsatCore" flag throughout (#6964) blob | commitdiff | raw | diff to current
2021-08-03 Gereon KremerProperly honor --stats-all and --stats-expert when... blob | commitdiff | raw | diff to current
2021-07-31 Gereon KremerPerform statistics printing via the API (#6952) blob | commitdiff | raw | diff to current
2021-07-26 Gereon KremerMove public options functions to separate file (#6671) blob | commitdiff | raw | diff to current
2021-07-22 Andres NoetzliAdd support for minimal unsat cores (#4605) blob | commitdiff | raw | diff to current
2021-06-15 Gereon KremerRemove public option wrappers (#6716) blob | commitdiff | raw | diff to current
2021-06-07 Gereon KremerRemove `Options::wasSetByUser()` (#6682) blob | commitdiff | raw | diff to current
2021-06-02 Gereon KremerRemove `Options::operator[]` (#6649) blob | commitdiff | raw | diff to current
2021-05-29 Gereon KremerRemove `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 ReynoldsUpdate to sygus standard output for check-synth respons... blob | commitdiff | raw | diff to current
2021-05-20 Haniel BarbosaRemove old unsat cores (#6581) blob | commitdiff | raw | diff to current
2021-05-19 Haniel BarbosaChange the default unsat cores (#6571) blob | commitdiff | raw | diff to current
2021-05-13 Mathias PreinerAdd std::hash overloads for Node, TNode and TypeNode... blob | commitdiff | raw | diff to current
2021-05-07 Andrew ReynoldsSimplifications to expand definitions (#6487) blob | commitdiff | raw | diff to current
2021-05-04 Andrew ReynoldsMove env into smt solver, theory engine, prop engine... blob | commitdiff | raw | diff to current
2021-04-30 Andrew ReynoldsUse substitutions for implementing defined functions... blob | commitdiff | raw | diff to current
2021-04-28 Gereon KremerRefactor resource manager options (#6446) blob | commitdiff | raw | diff to current
2021-04-28 Gereon KremerRemove exception headers from options.h (#6456) blob | commitdiff | raw | diff to current
2021-04-26 Gereon KremerFirst part of options refactoring (#6428) blob | commitdiff | raw | diff to current
2021-04-24 Mathias PreinerAdd assumption-based unsat cores. (#6427) blob | commitdiff | raw | diff to current
2021-04-22 Haniel BarbosaReconciling proofs and unsat cores (#6405) blob | commitdiff | raw | diff to current
2021-04-20 Gereon KremerAdd InferenceId as resources (#6339) blob | commitdiff | raw | diff to current
2021-04-16 Gereon KremerReplace SExpr class by simpler conversion routines... blob | commitdiff | raw | diff to current
2021-04-15 Gereon KremerAvoid options listener for resource manager. (#6366) blob | commitdiff | raw | diff to current
2021-04-15 Aina NiemetzRename occurrences of CVC4 to CVC5. (#6351) blob | commitdiff | raw | diff to current
2021-04-14 Gereon KremerRefactor / 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 ReynoldsAdd internal API methods for pool-based instantiation... blob | commitdiff | raw | diff to current
2021-04-13 Abdalrhman MohamedFix sexpr bug with AST output language. (#6329) blob | commitdiff | raw | diff to current
2021-04-12 Gereon KremerRefactor resource manager (#6322) blob | commitdiff | raw | diff to current
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316) blob | commitdiff | raw | diff to current
2021-04-07 Andrew ReynoldsFixes for abducts (#6279) blob | commitdiff | raw | diff to current
2021-04-06 Andres NoetzliRemove template argument from `NodeBuilder` (#6290) blob | commitdiff | raw | diff to current
2021-04-02 Gereon KremerMinor refactoring (#6273) blob | commitdiff | raw | diff to current
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) blob | commitdiff | raw | diff to current
2021-04-01 Gereon KremerMake ResetCommand go through APISolver (#6172) blob | commitdiff | raw | diff to current
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) blob | commitdiff | raw | diff to current
2021-03-23 Haniel BarbosaRemoving unused build options and deprecated proof... blob | commitdiff | raw | diff to current
2021-03-23 Aina NiemetzRemove internal includes of Api header. (#6193) blob | commitdiff | raw | diff to current
2021-03-22 Gereon KremerMove statistics from the driver into the SmtEngine... blob | commitdiff | raw | diff to current
2021-03-18 Haniel BarbosaWhen giving an SMT-LIB version, defaulting to SMT-LIB... blob | commitdiff | raw | diff to current
2021-03-18 Gereon KremerMove stats registry to env. (#6173) blob | commitdiff | raw | diff to current
2021-03-18 Abdalrhman MohamedEliminate 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 NiemetzDelete Expr layer. (#6117) blob | commitdiff | raw | diff to current
2021-03-10 Andrew ReynoldsAdd Env class (#6093) blob | commitdiff | raw | diff to current
2021-03-09 Gereon KremerSome more cleanup of includes (#6083) blob | commitdiff | raw | diff to current
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) blob | commitdiff | raw | diff to current
2021-03-06 Mathias PreinerRemove SMT-LIB 2.5 and 2.0 support. (#6068) blob | commitdiff | raw | diff to current
2021-03-03 Gereon KremerMore cleanup of includes to reduce compilation times... blob | commitdiff | raw | diff to current
2021-03-03 Abdalrhman MohamedRemove uses of SExpr class. (#6035) blob | commitdiff | raw | diff to current
2021-03-02 Gereon KremerClean 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 ReynoldsReorganize 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 ReynoldsFurther 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 ReynoldsSimplify internal API for sygus (#5687) blob | commitdiff | raw | diff to current
2020-12-16 Andrew ReynoldsSimplify synth-fun printer (#5682) blob | commitdiff | raw | diff to current
2020-12-14 Andrew ReynoldsProperly implement datatype selector triggers (#5624) blob | commitdiff | raw | diff to current
2020-12-12 Andrew ReynoldsFlush 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 ReynoldsFix issues related to model declarations (#5560) blob | commitdiff | raw | diff to current
2020-12-01 Andrew ReynoldsMore fixes for quantifier elimination (#5533) blob | commitdiff | raw | diff to current
2020-11-30 Abdalrhman MohamedEliminate uses of SExpr from the parser. (#5496) blob | commitdiff | raw | diff to current
2020-11-26 Andrew ReynoldsRemoving infrastructure related to SMT model (#5527) blob | commitdiff | raw | diff to current
2020-11-26 Andrew ReynoldsFully decouple SmtEngine and the Expr layer (#5532) blob | commitdiff | raw | diff to current
2020-11-23 Gereon KremerAdd get-info :time. (#5485) blob | commitdiff | raw | diff to current
2020-11-19 Andrew ReynoldsEnable new implementation of CEGQI based on nested... blob | commitdiff | raw | diff to current
2020-11-19 Andrew ReynoldsUse symbol manager for unsat cores (#5468) blob | commitdiff | raw | diff to current
2020-11-18 Andrew ReynoldsMinor cleanup of SmtEngine (#5450) blob | commitdiff | raw | diff to current
2020-11-18 Andrew ReynoldsUse symbol manager for get assignment (#5451) blob | commitdiff | raw | diff to current
2020-11-10 Andrew ReynoldsAdd proper support for the declare-heap command for... blob | commitdiff | raw | diff to current
2020-10-28 Andrew ReynoldsRemove more uses of Expr (#5357) blob | commitdiff | raw | diff to current
2020-10-27 Abdalrhman MohamedRefactor DeclareSygusVarCommand and SynthFunCommand... blob | commitdiff | raw | diff to current
2020-10-21 Abdalrhman MohamedAdd finishInit for getInterpol and getAbduct. (#5316) blob | commitdiff | raw | diff to current
2020-10-20 Andrew ReynoldsSplit 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 ReynoldsRefactor SMT-level model object (#5277) blob | commitdiff | raw | diff to current
2020-10-12 Andrew ReynoldsEliminate uses of Expr in SmtEngine interface (#5240) blob | commitdiff | raw | diff to current
2020-10-10 Abdalrhman MohamedProvide API version of some SMT Commands. (#5222) blob | commitdiff | raw | diff to current
2020-09-30 Gereon KremerRemove 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 ReynoldsReset assertions on resetAssertions (#5153) blob | commitdiff | raw | diff to current
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... blob | commitdiff | raw | diff to current
next