projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Preprare central model building for RANs (#7951)
[cvc5.git] / src / smt /
2022-01-14 Gereon KremerPreprare central model building for RANs (#7951) tree | commitdiff
2022-01-13 Andres NoetzliUnify abstract values and uninterpreted constants ... tree | commitdiff
2022-01-12 Andrew ReynoldsAdd -o learned-lits to output learned literals (#7934) tree | commitdiff
2022-01-12 Andrew ReynoldsEnsure configuration of shared selectors is consistent... tree | commitdiff
2022-01-12 Andrew ReynoldsEliminate use of subtyping from results of quantifier... tree | commitdiff
2022-01-11 Andrew ReynoldsTighten policy for unsat cores in sygus core connective... tree | commitdiff
2022-01-11 Andrew ReynoldsGuard use of unsat core mode pp-only (#7899) tree | commitdiff
2022-01-07 Andrew ReynoldsFix eager string preprocessing in incremental mode... tree | commitdiff
2022-01-06 Andrew ReynoldsMake alpha equivalence user context dependent (#7889) tree | commitdiff
2022-01-06 Andrew ReynoldsDisallow separation logic in incremental mode (#7888) tree | commitdiff
2022-01-06 Andrew ReynoldsMinor cleaning of non-clausal simplification (#7886) tree | commitdiff
2022-01-05 Andrew ReynoldsTrack input list for atoms in difficulty manager (... tree | commitdiff
2022-01-04 Andrew ReynoldsChange default granularity of proofs to macro (#7855) tree | commitdiff
2022-01-04 Andrew ReynoldsRemove spurious call to applySubs (#7871) tree | commitdiff
2022-01-04 Andrew ReynoldsRemove unused shutdown infrastructure (#7872) tree | commitdiff
2021-12-22 Andrew ReynoldsAdd support for incremental + interpolants (#7853) tree | commitdiff
2021-12-21 Andrew ReynoldsSupport get-abduct-next (#7850) tree | commitdiff
2021-12-20 Andrew ReynoldsAllow SyGuS subsolver to be reused in incremental mode... tree | commitdiff
2021-12-17 Andrew ReynoldsRefactoring initialization of proofs (#7834) tree | commitdiff
2021-12-16 Andrew ReynoldsFix get-model when sort constructors are present (... tree | commitdiff
2021-12-16 Andrew ReynoldsMinor fix for print benchmark. (#7821) tree | commitdiff
2021-12-15 Andrew ReynoldsAdd trace to see inferences in final proof (#7813) tree | commitdiff
2021-12-14 Andrew ReynoldsConnecting the core array solver in strings (#7800) tree | commitdiff
2021-12-13 Andrew ReynoldsInitial cut at distinguishing uses of CONST_RATIONAL... tree | commitdiff
2021-12-13 Gereon KremerImprove nonlinear solver (#7787) tree | commitdiff
2021-12-10 Haniel Barbosa[proofs] Add option to prune inputs from final proof... tree | commitdiff
2021-12-09 Andrew ReynoldsRemove a few static access to options in proof code... tree | commitdiff
2021-12-09 Andrew ReynoldsDo not make SyGuS subsolver in unsat state after solvin... tree | commitdiff
2021-12-08 Gereon KremerStatic options acceses again (#7771) tree | commitdiff
2021-12-07 Gereon KremerRemove more static accesses to options (#7764) tree | commitdiff
2021-12-07 Andrew ReynoldsAdd proof annotation option (#7750) tree | commitdiff
2021-12-07 Andrew ReynoldsAllow sygus in incremental mode (#7756) tree | commitdiff
2021-12-07 Andrew ReynoldsMake data structures in relevance manager SAT-context... tree | commitdiff
2021-12-07 Andrew ReynoldsTowards support for incremental sygus (#7736) tree | commitdiff
2021-12-07 Andrew ReynoldsEliminate more static calls to Rewriter::rewrite (... tree | commitdiff
2021-12-01 Andrew ReynoldsImprovements for get-difficulty (#7720) tree | commitdiff
2021-11-24 Andres NoetzliMinor fixes (#7691) tree | commitdiff
2021-11-22 Gereon KremerRefactor IO stream manipulators (#7555) tree | commitdiff
2021-11-17 Andres NoetzliFix binding of quoted symbols in `define-fun` (#7655) tree | commitdiff
2021-11-16 Haniel Barbosa[proofs] Make sure --proof-check=... is no-op when... tree | commitdiff
2021-11-12 Andres NoetzliRemove `ConstantMap<Rational>` (#7635) tree | commitdiff
2021-11-11 Andrew ReynoldsGeneralize front-end checks to check for shadowed varia... tree | commitdiff
2021-11-11 Andrew ReynoldsAdd lazy approach for handling lambdas in the HO extens... tree | commitdiff
2021-11-09 Gereon KremerRemove command-verbosity option (#7581) tree | commitdiff
2021-11-06 Abdalrhman MohamedPrint `unsupported` for unrecognized flags. (#7384) tree | commitdiff
2021-11-06 Gereon KremerRemove `Notice()` in favor of new `verbose()` (#7588) tree | commitdiff
2021-11-05 Andrew ReynoldsEliminate a level of nesting of traversals in theory... tree | commitdiff
2021-11-05 Gereon KremerRemove `Chat()` in favor of new `verbose()` (#7586) tree | commitdiff
2021-11-05 Andrew ReynoldsRemove many static calls to rewrite (#7580) tree | commitdiff
2021-11-05 Gereon KremerEliminate `Warning` macro in favor of `EnvObj::warning... tree | commitdiff
2021-11-04 Andrew ReynoldsReplace the old dump infrastructure (#7572) tree | commitdiff
2021-11-04 Gereon KremerStart refactoring of `-o` and `-v` (#7449) tree | commitdiff
2021-11-04 Gereon KremerEnable CDCAC solver for selected quantified logics... tree | commitdiff
2021-11-04 Gereon KremerMinor cleanup in SolverEngine::setInfo() (#7566) tree | commitdiff
2021-11-03 Aina Niemetzapi: Rename some separation logic functions for consist... tree | commitdiff
2021-11-03 Andrew ReynoldsRefactor skolem construction (#7561) tree | commitdiff
2021-11-02 Abdalrhman MohamedAdd printing methods for some commands. (#7557) tree | commitdiff
2021-11-02 Mathias PreinerFix setDefaults() for proofs with bitblast-internal... tree | commitdiff
2021-11-02 Andrew ReynoldsMake quant elimination robust to presence of other... tree | commitdiff
2021-11-01 Mathias Preinerbv: Remove layered solver. (#7455) tree | commitdiff
2021-11-01 Gereon KremerReplace more static options accesses (#7531) tree | commitdiff
2021-10-28 Abdalrhman MohamedAdd a `define-fun` command for each `:named` term.... tree | commitdiff
2021-10-27 Andrew ReynoldsDeterministic variables for RE elim (#7489) tree | commitdiff
2021-10-26 Haniel Barbosa[proofs] Fix singleton check in MACRO_RES post-processi... tree | commitdiff
2021-10-26 Haniel Barbosa[proofs] Fix and simplify CHAIN_RESOLUTION checker... tree | commitdiff
2021-10-26 Andrew ReynoldsDisable sygus-inst when incremental (#7485) tree | commitdiff
2021-10-25 Andrew ReynoldsAdd new method for enumerating unsat queries with SyGuS... tree | commitdiff
2021-10-25 Andrew ReynoldsFix support for global declarations (#7480) tree | commitdiff
2021-10-25 Andrew ReynoldsRemove HOL/fmf bound messages in set defaults (#7487) tree | commitdiff
2021-10-25 mudathirmahgoubAdd inference for count map (#7264) tree | commitdiff
2021-10-22 Gereon KremerRemove options::X__name (#7414) tree | commitdiff
2021-10-22 Haniel Barbosa[proof] Fixing CHAIN_RESOLUTION checker (#7465) tree | commitdiff
2021-10-22 Andrew ReynoldsRemove `--uf-ho` option (#7463) tree | commitdiff
2021-10-20 Andrew ReynoldsThrow exception if checking model with separation logic... tree | commitdiff
2021-10-20 Andrew ReynoldsEliminate last static calls to rewriter from smt layer... tree | commitdiff
2021-10-20 Abdalrhman MohamedAvoid escaping `double-quotes` twice. (#7409) tree | commitdiff
2021-10-19 Andrew ReynoldsFix expected conclusion for EQ_RESOLVE when expanding... tree | commitdiff
2021-10-14 Gereon KremerFix (get-info :authors) (#7373) tree | commitdiff
2021-10-13 Andrew ReynoldsEliminate uses of rewrite from datatypes theory (#7354) tree | commitdiff
2021-10-12 Andrew ReynoldsEliminate calls to currentResourceManager (#7350) tree | commitdiff
2021-10-12 Aina NiemetzClean up occurrences of SmtEngine in comments. (#7349) tree | commitdiff
2021-10-12 Aina NiemetzGet rid of unused member d_smtStats in ExpandDefs.... tree | commitdiff
2021-10-12 Aina NiemetzRename SmtEngineState to SolverEngineState. (#7344) tree | commitdiff
2021-10-12 Andrew ReynoldsProvide a non-traversal interface to term formula remov... tree | commitdiff
2021-10-11 Aina NiemetzRename SmtEngineStatistics to SolverEngineStatistics... tree | commitdiff
2021-10-11 Aina NiemetzRename SmtScope to SolverEngineScope. (#7284) tree | commitdiff
2021-10-11 Andrew ReynoldsConnect the LFSC printer (#7323) tree | commitdiff
2021-10-09 Gereon KremerRemove static accesses to options where EnvObj is used... tree | commitdiff
2021-10-08 Andrew ReynoldsA few more miscellaneous uses of EnvObj (#7325) tree | commitdiff
2021-10-07 Andrew ReynoldsMove preprocessor to smt solver (#7321) tree | commitdiff
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
next