projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Finish the LFSC printer (#7285)
[cvc5.git] / src / smt /
2021-10-07 Andrew ReynoldsUse skolem lemma in prop layer interfaces (#7320) tree | commitdiff
2021-10-07 Andrew ReynoldsMake the cardinality of the alphabet of strings configu... tree | commitdiff
2021-10-07 Andrew ReynoldsEliminate more circular dependencies on solver engine... tree | commitdiff
2021-10-06 Gereon KremerChange semantics of dumpUnsatCoresFull (#7314) tree | commitdiff
2021-10-05 Gereon KremerFinish refactoring on option handlers (#7295) tree | commitdiff
2021-10-04 Andrew ReynoldsMove isFiniteType from theory engine to Env (#7287) tree | commitdiff
2021-10-04 Andrew ReynoldsMake decision engine use env (#7300) tree | commitdiff
2021-10-01 Andrew ReynoldsUpdate theory preprocessor to use Env (#7288) tree | commitdiff
2021-10-01 Andrew ReynoldsAdd the print benchmark utility (#7196) tree | commitdiff
2021-10-01 Andrew ReynoldsUse the proper evaluator for optimized SyGuS datatype... tree | commitdiff
2021-10-01 Aina NiemetzRename SmtEngine to SolverEngine. (#7282) tree | commitdiff
2021-09-30 Aina NiemetzRename files smt_engine.(cpp|h) to solver_engine.(cpp... tree | commitdiff
2021-09-29 Abdalrhman MohamedRemove support for extended `(check-sat <term>)` comman... tree | commitdiff
2021-09-29 Andrew ReynoldsProperly restrict PBE symmetry breaking for abduction... tree | commitdiff
2021-09-23 Gereon KremerEliminate Output macro in favor of simple Env functions... tree | commitdiff
2021-09-23 Lachnitt[proofs] Alethe: Add Alethe Files to be Compiled ... tree | commitdiff
2021-09-23 Andrew ReynoldsMore uses of EnvObj (#7230) tree | commitdiff
2021-09-23 Abdalrhman MohamedUse `|` to print quoted strings in `set-info` command... tree | commitdiff
2021-09-22 Andrew ReynoldsTowards standard usage of evaluator (#7189) tree | commitdiff
2021-09-17 Andres NoetzliUse a single `NodeManager` per thread (#7204) tree | commitdiff
2021-09-14 Andrew ReynoldsAdd get-difficulty to the API (#7194) tree | commitdiff
2021-09-14 Andrew ReynoldsSupport sygus version 2.1 command assume (#7081) tree | commitdiff
2021-09-14 Andrew ReynoldsUtilities in preparation for print benchmark utility... tree | commitdiff
2021-09-14 Andrew ReynoldsAdd proof manager method to translate difficulty map... tree | commitdiff
2021-09-14 Mathias Preinerproofs: Properly track pre- and post-rewrites in bbAtom... tree | commitdiff
2021-09-14 Andrew ReynoldsReimplement `--dump=raw-benchmark` as `-o raw-benchmark... tree | commitdiff
2021-09-13 Andrew ReynoldsConnect difficulty manager to TheoryEngine (#7161) tree | commitdiff
2021-09-11 Gereon KremerUse StatisticsRegistry from Env (#7166) tree | commitdiff
2021-09-11 Aina NiemetzcheckModel: Extend documentation. (#7177) tree | commitdiff
2021-09-10 Mathias Preinerbv: Use EnvObj::rewrite() and EnvObj::options() in... tree | commitdiff
2021-09-10 Andrew ReynoldsMore refactoring of set defaults (#7160) tree | commitdiff
2021-09-09 Andrew ReynoldsAdd difficulty post-processor (#7150) tree | commitdiff
2021-09-09 Andrew ReynoldsDisable shared selectors for quantified logics without... tree | commitdiff
2021-09-08 Andrew ReynoldsImprove pre-skolemization, move quantifiers preprocess... tree | commitdiff
2021-09-08 Gereon KremerA couple of minor cleanups (#7141) tree | commitdiff
2021-09-08 Andrew ReynoldsTowards standard usage of ExtendedRewriter (#7145) tree | commitdiff
2021-09-08 Andrew ReynoldsAdd option for using bound inference for relevant asser... tree | commitdiff
2021-09-08 Andrew ReynoldsUse rewriteViaMethod instead of accessing builtin proof... tree | commitdiff
2021-09-07 Andrew ReynoldsRefactoring of proof manager initialization (#7073) tree | commitdiff
2021-09-07 Andrew ReynoldsRefactoring and fixes of set defaults for quantifiers... tree | commitdiff
2021-09-03 Aina NiemetzEnvObj: Add options(), context(), userContext(). (... tree | commitdiff
2021-09-03 Andrew ReynoldsEliminate backwards ref to SmtEngine from abduction... tree | commitdiff
2021-09-03 Aina Niemetztheory: Have Theory and TheoryArith* derive from EnvObj... tree | commitdiff
2021-09-02 Aina NiemetzEnvObj: Restrict access. (#7121) tree | commitdiff
2021-09-02 Gereon KremerRemove options::getAll() (#7111) tree | commitdiff
2021-09-02 Andrew ReynoldsImplement lazy proof checking modes (#7106) tree | commitdiff
2021-09-02 Aina NiemetzEnable sygus-inst for FP, NIA and NRA. (#7098) tree | commitdiff
2021-09-02 Aina NiemetzAdd class EnvObj. (#7113) tree | commitdiff
2021-09-01 Andrew ReynoldsPrint response to get-model using the API (#7084) tree | commitdiff
2021-09-01 Gereon KremerMake driver::totalTime a TimerStat (#7089) tree | commitdiff
2021-09-01 Andrew ReynoldsLazy proof reconstruction for strings theory solver... tree | commitdiff
2021-08-31 Aina Niemetzbv: Remove dump=bv-rewrites. (#7099) tree | commitdiff
2021-08-30 Andrew ReynoldsFurther refactoring of set defaults for incompatibility... tree | commitdiff
2021-08-30 Gereon KremerRefactor filename handling (#7088) tree | commitdiff
2021-08-27 Andrew ReynoldsExpand definitions in sygus operators at the SMT level... tree | commitdiff
2021-08-27 Andrew ReynoldsAdd missing methods to Solver API for models (#7052) tree | commitdiff
2021-08-26 Andrew ReynoldsEliminate currentSmtEngine for subsolver calls (#7068) tree | commitdiff
2021-08-26 Andrew ReynoldsDump models for isNotEntailed results (#7071) tree | commitdiff
2021-08-26 Gereon KremerConsolidate language types (#7065) tree | commitdiff
2021-08-24 Andrew ReynoldsTop-level structure for set defaults (#7047) tree | commitdiff
2021-08-24 Andrew ReynoldsMiscellaneous changes from proof-new (#7042) tree | commitdiff
2021-08-20 Gereon KremerMake driver use options from the solver (#6930) tree | commitdiff
2021-08-20 Andrew ReynoldsSimplify how user-provided quantifier attributes are... tree | commitdiff
2021-08-20 Andrew ReynoldsMore refactoring of set defaults (#7043) tree | commitdiff
2021-08-20 Andrew ReynoldsEliminate eager model building (#7038) tree | commitdiff
2021-08-19 Andrew ReynoldsCatch cases where recursive functions reference functio... tree | commitdiff
2021-08-19 Andrew ReynoldsSplit proof final callback to its own file (#6984) tree | commitdiff
2021-08-19 Andrew ReynoldsRefactor proof output for TPTP (#7029) tree | commitdiff
2021-08-18 Andrew ReynoldsMake TheoryProxy use Env, simplify initialization of... tree | commitdiff
2021-08-17 Andrew ReynoldsMake SmtEngineState use Env (#7028) tree | commitdiff
2021-08-17 Andrew ReynoldsFix policy for eliminating quantified formulas (#7017) tree | commitdiff
2021-08-17 Andrew ReynoldsInitial refactoring of set defaults (#7021) tree | commitdiff
2021-08-16 Gereon KremerMake Theory class use Env (#7011) tree | commitdiff
2021-08-13 Gereon KremerRefactor setDefaults to use an options object (#6994) tree | commitdiff
2021-08-06 Gereon KremerClear options manager (#6991) tree | commitdiff
2021-08-04 Gereon KremerConsolidate solver resets (#6986) tree | commitdiff
2021-08-04 Andrew ReynoldsAdd optional debug information for dumping instantiatio... tree | commitdiff
2021-08-04 Gereon KremerRefactor managed streams (#6934) tree | commitdiff
2021-08-04 Haniel Barbosa[proof] Add getProof to API and use it in GetProofComma... tree | commitdiff
2021-08-04 Andrew ReynoldsRemove dependencies on smt engine in smt solver (#6965) tree | commitdiff
2021-08-03 Andrew ReynoldsRemove "inUnsatCore" flag throughout (#6964) tree | commitdiff
2021-08-03 Gereon KremerProperly honor --stats-all and --stats-expert when... tree | commitdiff
2021-07-31 Gereon KremerPerform statistics printing via the API (#6952) tree | commitdiff
2021-07-29 Haniel Barbosa[proofs] Set BV solver to better proof-producing one... tree | commitdiff
2021-07-29 Andrew ReynoldsIntegrate central equality engine approach into theory... tree | commitdiff
2021-07-27 Andrew ReynoldsTrack instantiation reasons in proofs (#6935) tree | commitdiff
2021-07-26 Gereon KremerMove public options functions to separate file (#6671) tree | commitdiff
2021-07-26 Andrew ReynoldsMore updates to arithmetic in preparation for central... tree | commitdiff
2021-07-22 Andres NoetzliAdd support for minimal unsat cores (#4605) tree | commitdiff
2021-07-15 Mathias Preinerbv: Disable bv-assert-input if proofs are enabled.... tree | commitdiff
2021-07-14 Andrew ReynoldsFix for context on input proof generator (#6873) tree | commitdiff
2021-07-13 Mathias Preinerbv: Expand bitblast proof steps in the proof post proce... tree | commitdiff
2021-07-09 Andrew ReynoldsImplement stop-only for new justification heuristic... tree | commitdiff
2021-07-06 Andrew ReynoldsIntegrate learned rewrite preprocessing pass (#6840) tree | commitdiff
2021-07-06 OuyanchengAdd some printing functions for OptimizationObjective... tree | commitdiff
2021-07-01 Andrew ReynoldsAdd recursive function definitions to subsolver in... tree | commitdiff
2021-06-30 Andrew ReynoldsDo not apply fmfBound to standard quantifiers when... tree | commitdiff
2021-06-28 Haniel Barbosa[proof] [dot] Make dot printer stateful (#6799) tree | commitdiff
2021-06-23 Haniel Barbosa[hol] Disable bound fmf when HOL (#6792) tree | commitdiff
2021-06-21 Mathias PreinerMove cnfConversionTime statistic to CnfStream. (#6769) tree | commitdiff
next