projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Ignore isInConflict when adding conflicts (#5995)
[cvc5.git] / src / smt /
2021-03-04 Aina NiemetzNew C++ API: Clean up usage of internal Type/TypeNodes... tree | commitdiff
2021-03-04 Aina NiemetzNew C++ API: Clean up usage of internal Result. (#6043) tree | commitdiff
2021-03-03 Gereon KremerMore cleanup of includes to reduce compilation times... tree | commitdiff
2021-03-03 Abdalrhman MohamedRemove uses of SExpr class. (#6035) tree | commitdiff
2021-03-02 Gereon KremerClean up includes to reduce compile times (#6031) tree | commitdiff
2021-02-22 Andrew Reynolds(proof-new) Change proof-new option to proof (#5955) tree | commitdiff
2021-02-17 Mathias PreinerAdd bit-level propagation support to BV bitblast solver... tree | commitdiff
2021-02-12 Andrew ReynoldsSimplify and fix decision engine's handling of skolem... tree | commitdiff
2021-02-11 Andrew ReynoldsSimplify interface for preprocessor (#5890) tree | commitdiff
2021-02-10 Andrew ReynoldsRemove track instantiations infrastructure (#5883) tree | commitdiff
2021-02-10 Andrew ReynoldsOptimize get skolems method (#5876) tree | commitdiff
2021-02-10 Andrew ReynoldsDo not traverse quantifiers in term formula removal... tree | commitdiff
2021-02-08 Haniel BarbosaFix dumping of assertions for monolithic preprocessing... tree | commitdiff
2021-02-03 Mathias PreinerAdd BV solver bitblast. (#5851) tree | commitdiff
2021-02-03 Haniel Barbosa[proof-new] Fix MACRO_RESOLUTION expansion for singleto... tree | commitdiff
2021-02-02 Andrew ReynoldsCleanup some includes (#5847) tree | commitdiff
2021-02-02 Haniel Barbosa[proof-new] Fix bug in expansion of MACRO_RESOLUTION... tree | commitdiff
2021-02-01 Abdalrhman MohamedAvoid calling the printers while converting sexpr to... tree | commitdiff
2021-01-29 Haniel Barbosa[proof-new] Connecting new unsat cores (#5834) tree | commitdiff
2021-01-29 Andrew Reynolds(proof-new) Distinguish pre vs post rewrites in term... tree | commitdiff
2021-01-28 Andrew ReynoldsReorganize calls to quantifiers engine from SmtEngine... tree | commitdiff
2021-01-28 Andrew ReynoldsSimplify lemma interface (#5819) tree | commitdiff
2021-01-27 Andrew Reynolds(proof-new) Improvements to quantifiers engine and... tree | commitdiff
2021-01-22 Haniel Barbosa[proof-new] Expanding MACRO_RESOLUTION in post-processi... tree | commitdiff
2021-01-20 Andrew ReynoldsDo not track processed in remove term formulas loop... tree | commitdiff
2021-01-15 Andrew ReynoldsImplement --no-strings-lazy-pp as a preprocessing pass... tree | commitdiff
2021-01-14 Andrew ReynoldsUpdates to theory preprocess equality (#5776) tree | commitdiff
2021-01-12 yoni206Foreign theory rewrite option (#5763) tree | commitdiff
2021-01-11 Andrew ReynoldsFurther simplifications in preparation for removing... tree | commitdiff
2021-01-08 Haniel Barbosa[proof-new] Implementing getProof in the API and SMT... tree | commitdiff
2021-01-06 Andrew ReynoldsAdd new interfaces to term formula removal and theory... tree | commitdiff
2021-01-05 Andrew ReynoldsRemove a few miscellaneous references to the expr layer... tree | commitdiff
2020-12-24 Haniel Barbosa[proof-new] Only use old proofs for unsat cores if... tree | commitdiff
2020-12-23 Andrew ReynoldsRemove quant EPR option (#5716) tree | commitdiff
2020-12-23 Haniel Barbosa[proof-new] Adding a manager for the new unsat cores... tree | commitdiff
2020-12-22 Andrew ReynoldsMake theory preprocess rewrite equalities a preprocessi... tree | commitdiff
2020-12-22 Andrew ReynoldsRemove preregister instantiation heuristic (#5713) tree | commitdiff
2020-12-21 Andrew ReynoldsMove ownership of theory preprocessor to TheoryProxy... tree | commitdiff
2020-12-21 Andrew ReynoldsEliminate recursion from the internals of term formula... tree | commitdiff
2020-12-18 Andrew ReynoldsSimplify internal API for sygus (#5687) tree | commitdiff
2020-12-17 Andrew ReynoldsSimplify term formula removal interface (#5695) tree | commitdiff
2020-12-17 Andrew ReynoldsSimplify and fix check models (#5685) tree | commitdiff
2020-12-16 Andrew ReynoldsSimplify preprocessing (#5647) tree | commitdiff
2020-12-16 Andrew ReynoldsSimplify synth-fun printer (#5682) tree | commitdiff
2020-12-16 Andrew ReynoldsMove ownership of term formula removal to theory prepro... tree | commitdiff
2020-12-15 Andrew ReynoldsRemove bv divide by zero option (#5672) tree | commitdiff
2020-12-14 Andrew ReynoldsProperly implement datatype selector triggers (#5624) tree | commitdiff
2020-12-14 Haniel Barbosa[proof-new] Updating interfaces between prop engine... tree | commitdiff
2020-12-12 Andrew ReynoldsFlush statistics through NodeManager in SmtEngine ... tree | commitdiff
2020-12-10 Gereon KremerFixed a bunch of clang warnings. (#5637) tree | commitdiff
2020-12-09 Andrew ReynoldsMake decision engine independent of AssertionsPipeline... tree | commitdiff
2020-12-08 Abdalrhman MohamedFix a bug with synth-fun printer (#5512) tree | commitdiff
2020-12-07 Andrew ReynoldsFix issue with free variables introduced by quantifier... tree | commitdiff
2020-12-07 Andrew ReynoldsDo not expand theory definitions at the beginning of... tree | commitdiff
2020-12-03 Andrew Reynolds(proof-new) Updates to SMT proof manager and SmtEngine... tree | commitdiff
2020-12-03 Andrew ReynoldsRefactor handling of global declarations (#5577) tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-12-02 Aina NiemetzRename macro Message to CVC4Message. (#5576) tree | commitdiff
2020-12-02 Andrew Reynolds(proof-new) Proofs for expand definitions (#5562) tree | commitdiff
2020-12-02 Andrew ReynoldsFix issues related to model declarations (#5560) tree | commitdiff
2020-12-01 Andrew ReynoldsMore fixes for quantifier elimination (#5533) tree | commitdiff
2020-11-30 Abdalrhman MohamedEliminate uses of SExpr from the parser. (#5496) tree | commitdiff
2020-11-30 Andrew ReynoldsRemove includes for old API from internal code (#5536) tree | commitdiff
2020-11-26 Andrew ReynoldsRemoving infrastructure related to SMT model (#5527) tree | commitdiff
2020-11-26 Andrew ReynoldsMove expand definitions to its own file (#5528) tree | commitdiff
2020-11-26 Andrew ReynoldsFully decouple SmtEngine and the Expr layer (#5532) tree | commitdiff
2020-11-25 Andrew ReynoldsUse 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 ReynoldsAdd declare model symbol methods to SymbolManager and... tree | commitdiff
2020-11-23 Gereon KremerAdd get-info :time. (#5485) tree | commitdiff
2020-11-20 Andrew ReynoldsFix remove term formula policy for terms beneath quanti... tree | commitdiff
2020-11-20 Andrew ReynoldsSupport 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 ReynoldsEnable new implementation of CEGQI based on nested... tree | commitdiff
2020-11-19 Andrew ReynoldsUse symbol manager for unsat cores (#5468) tree | commitdiff
2020-11-18 Andrew ReynoldsMinor cleanup of SmtEngine (#5450) tree | commitdiff
2020-11-18 Andrew ReynoldsDo not expand definitions of extended arithmetic operat... tree | commitdiff
2020-11-18 Andrew ReynoldsUse symbol manager for get assignment (#5451) tree | commitdiff
2020-11-12 Andrew ReynoldsFix 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 ReynoldsMove symbol manager to src/expr/ (#5420) tree | commitdiff
2020-11-11 Andrew ReynoldsPass symbol manager to commands (#5410) tree | commitdiff
2020-11-10 Andrew ReynoldsDo not mark extended functions as reduced based on... tree | commitdiff
2020-11-10 Andrew ReynoldsAdd proper support for the declare-heap command for... tree | commitdiff
2020-11-09 Andrew ReynoldsSimplify handling of subtypes in smt2 printer (#5401) tree | commitdiff
2020-11-06 Andrew ReynoldsSimplify printing with respect to expression types... tree | commitdiff
2020-10-30 Andrew ReynoldsUpdate api::Sort to use TypeNode instead of Type (... tree | commitdiff
2020-10-28 Andrew ReynoldsRemove more uses of Expr (#5357) tree | commitdiff
2020-10-27 Abdalrhman MohamedRefactor DeclareSygusVarCommand and SynthFunCommand... tree | commitdiff
2020-10-27 Gereon KremerDisable --nl-cad option by default (#5350) tree | commitdiff
2020-10-27 Gereon KremerEnable --nl-cad by default (#5345) tree | commitdiff
2020-10-22 Gereon KremerUse theoryof-mode=type for QF_NRA (#5326) tree | commitdiff
2020-10-21 Abdalrhman MohamedAdd 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 MohamedRemove some Commands from the API. (#5268) tree | commitdiff
2020-10-20 Andrew ReynoldsFix miscellaneous warnings (#5256) tree | commitdiff
2020-10-20 Andrew ReynoldsSplit 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
next