summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2020-12-09Fixed a bunch of clang warnings. (#5637)Gereon Kremer
2020-12-09Make decision engine independent of AssertionsPipeline (#5626)Andrew Reynolds
2020-12-08Fix a bug with synth-fun printer (#5512)Abdalrhman Mohamed
2020-12-07Fix issue with free variables introduced by quantifier rewriter (#5602)Andrew Reynolds
2020-12-07Do not expand theory definitions at the beginning of preprocessing (#5544)Andrew Reynolds
2020-12-03(proof-new) Updates to SMT proof manager and SmtEngine (#5446)Andrew Reynolds
2020-12-03Refactor handling of global declarations (#5577)Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback