summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2020-12-02Update copyright headers.Aina Niemetz
2020-12-02Rename macro Message to CVC4Message. (#5576)Aina Niemetz
2020-12-02(proof-new) Proofs for expand definitions (#5562)Andrew Reynolds
2020-12-01Fix issues related to model declarations (#5560)Andrew Reynolds
2020-11-30More fixes for quantifier elimination (#5533)Andrew Reynolds
2020-11-30Eliminate uses of SExpr from the parser. (#5496)Abdalrhman Mohamed
2020-11-30Remove includes for old API from internal code (#5536)Andrew Reynolds
2020-11-26Removing infrastructure related to SMT model (#5527)Andrew Reynolds
2020-11-26Move expand definitions to its own file (#5528)Andrew Reynolds
2020-11-25Fully decouple SmtEngine and the Expr layer (#5532)Andrew Reynolds
2020-11-25Use symbol manager for printing responses get-model (#5516)Andrew Reynolds
2020-11-23(proof-new) Miscellaneous changes from proof-new (#5445)Andrew Reynolds
2020-11-23Add declare model symbol methods to SymbolManager and Model (#5480)Andrew Reynolds
2020-11-23Add get-info :time. (#5485)Gereon Kremer
2020-11-20Fix remove term formula policy for terms beneath quantifiers (#5497)Andrew Reynolds
2020-11-20Support nested quantifier elimination for get-qe command (#5490)Andrew Reynolds
2020-11-20(proof-new) Replace LazyCDProofSet by generic CDProofSet (#5487)Gereon Kremer
2020-11-19Enable new implementation of CEGQI based on nested quantifier elimination (#5...Andrew Reynolds
2020-11-19Use symbol manager for unsat cores (#5468)Andrew Reynolds
2020-11-18Minor cleanup of SmtEngine (#5450)Andrew Reynolds
2020-11-18Do not expand definitions of extended arithmetic operators (#5433)Andrew Reynolds
2020-11-18Use symbol manager for get assignment (#5451)Andrew Reynolds
2020-11-12Fix printing of define named function (#5425)Andrew Reynolds
2020-11-12(proof-new) Improve printing and debugging for pedantic checking (#5337)Andrew Reynolds
2020-11-11Move symbol manager to src/expr/ (#5420)Andrew Reynolds
2020-11-11Pass symbol manager to commands (#5410)Andrew Reynolds
2020-11-10Do not mark extended functions as reduced based on decomposing contains (#5407)Andrew Reynolds
2020-11-10Add proper support for the declare-heap command for separation logic (#5405)Andrew Reynolds
2020-11-09Simplify handling of subtypes in smt2 printer (#5401)Andrew Reynolds
2020-11-05Simplify printing with respect to expression types (#5394)Andrew Reynolds
2020-10-29Update api::Sort to use TypeNode instead of Type (#5363)Andrew Reynolds
2020-10-28Remove more uses of Expr (#5357)Andrew Reynolds
2020-10-27Refactor DeclareSygusVarCommand and SynthFunCommand to use the API. (#5334)Abdalrhman Mohamed
2020-10-27Disable --nl-cad option by default (#5350)Gereon Kremer
2020-10-27Enable --nl-cad by default (#5345)Gereon Kremer
2020-10-22Use theoryof-mode=type for QF_NRA (#5326)Gereon Kremer
2020-10-20Add finishInit for getInterpol and getAbduct. (#5316)Abdalrhman Mohamed
2020-10-20(proof-new) Fixes for proofs in rewriter (#5307)Andrew Reynolds
2020-10-20(proof-new) Update add lazy step interface in LazyCDProof (#5299)Andrew Reynolds
2020-10-20Remove some Commands from the API. (#5268)Abdalrhman Mohamed
2020-10-20Fix miscellaneous warnings (#5256)Andrew Reynolds
2020-10-20Split CheckModels utility to its own file (#5303)Andrew Reynolds
2020-10-19(proof-new) Updates to assertions pipeline and preprocess generator (#5300)Andrew Reynolds
2020-10-19(proof-new) Update preprocessing pass context for proofs (#5298)Andrew Reynolds
2020-10-18 (proof-new) Witness axiom reconstruction for purification skolems (#5289)Andrew Reynolds
2020-10-18(proof-new) More features for SMT proof post-processor (#5246)Andrew Reynolds
2020-10-16Refactor SMT-level model object (#5277)Andrew Reynolds
2020-10-13(proof-new) Generalize preprocess proof generator (#5245)Andrew Reynolds
2020-10-12Eliminate uses of Expr in SmtEngine interface (#5240)Andrew Reynolds
2020-10-12Ensure uninterpreted sort owner is UF if uf-ho or finite-model-find is enable...Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback