projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Add support for re.all (#2980)
[cvc5.git] / src / smt /
2019-04-30 Andrew ReynoldsEliminate APPLY kind (#2976) tree | commitdiff
2019-04-24 Mathias PreinerDo not use __ prefix for header guards. (#2974) tree | commitdiff
2019-04-17 Andrew ReynoldsMore use of isClosure (#2959) tree | commitdiff
2019-04-11 Andrew Reynolds Eliminate Boolean ITE within terms, fixes 2947 (#2949) tree | commitdiff
2019-03-26 Aina NiemetzUpdate copyright headers. tree | commitdiff
2019-03-22 makaimannUse empty vector instead of false in query with null... tree | commitdiff
2019-03-20 Andrew ReynoldsSygus abduction feature (#2744) tree | commitdiff
2019-03-16 Andres NoetzliLimit --solve-int-as-bv=X to QF_NIA/QF_LIA/QF_IDL ... tree | commitdiff
2019-03-14 makaimanncheck for null assumption in query and replace with... tree | commitdiff
2019-03-13 Andres NoetzliAdd statistics for proof gen./checking time, size ... tree | commitdiff
2019-02-27 Andres NoetzliUse string stream for proofs instead of tmp files ... tree | commitdiff
2019-02-12 Andres NoetzliDelete temporary proof files when aborting CVC4 (#2834) tree | commitdiff
2019-01-18 Andres Noetzli Fix ABC build (#2808) tree | commitdiff
2019-01-15 Andres NoetzliStrings: Add option to change loop process mode (#2794) tree | commitdiff
2019-01-11 Aina NiemetzNew C++ API: Add unit tests for setInfo, setLogic,... tree | commitdiff
2018-12-11 Andrew ReynoldsRemove alternate versions of mbqi (#2742) tree | commitdiff
2018-12-10 makaimannBoolToBV modes (off, ite, all) (#2530) tree | commitdiff
2018-12-06 Andres NoetzliFix use-after-free due to destruction order (#2739) tree | commitdiff
2018-11-29 Andrew ReynoldsCombine sygus stream with PBE (#2726) tree | commitdiff
2018-11-27 Andrew ReynoldsLazy model construction in TheoryEngine (#2633) tree | commitdiff
2018-11-21 Andrew ReynoldsQuickly recognize when PBE conjectures are infeasible... tree | commitdiff
2018-11-15 Andrew Reynolds Expand definitions prior to model core computation... tree | commitdiff
2018-10-31 Andres NoetzliRecord assumption info in AssertionPipeline (#2678) tree | commitdiff
2018-10-22 Andres NoetzliRecover from wrong use of get-info :reason-unknown... tree | commitdiff
2018-10-20 Andrew ReynoldsSygus streaming non-implied predicates (#2660) tree | commitdiff
2018-10-19 Andres NoetzliAdd OptionException handling during initialization... tree | commitdiff
2018-10-19 Andrew ReynoldsNon-implied mode for model cores (#2653) tree | commitdiff
2018-10-18 Haniel BarbosaIntroducing internal commands for SyGuS commands (... tree | commitdiff
2018-10-18 Andrew ReynoldsSygus query generator (#2465) tree | commitdiff
2018-10-15 Andrew ReynoldsDelay initialization of theory engine (#2621) tree | commitdiff
2018-10-13 Andres NoetzliReset input language for ExprMiner subsolver (#2624) tree | commitdiff
2018-10-11 Haniel BarbosaFix default setting of CegisUnif options (#2605) tree | commitdiff
2018-10-11 Andrew ReynoldsSynthesize rewrite rules from inputs (#2608) tree | commitdiff
2018-10-09 Aina NiemetzFix compiler warnings. (#2601) tree | commitdiff
2018-10-05 Andrew ReynoldsUpdate default options for sygus (#2586) tree | commitdiff
2018-10-01 Andres Noetzli Fix dumping pre/post preprocessing passes (#2469) tree | commitdiff
2018-10-01 Andres NoetzliRefactor preprocessing pass registration (#2468) tree | commitdiff
2018-09-22 Mathias Preinercmake: Remove unused CMakeLists.txt tree | commitdiff
2018-09-22 Aina Niemetzcmake: Added initial build infrastructure. tree | commitdiff
2018-09-18 Andrew ReynoldsMove and rename sygus solver classes (#2488) tree | commitdiff
2018-09-18 Haniel Barbosafix assertion error (#2487) tree | commitdiff
2018-09-17 Andres NoetzliRemove broken dumping support from portfolio build... tree | commitdiff
2018-09-17 Andres NoetzliRemove unnecessary tracing from preprocessing (#2472) tree | commitdiff
2018-09-15 Andres NoetzliRefactor how assertions are added to decision engine... tree | commitdiff
2018-09-11 Andrew ReynoldsSupport model cores via option --produce-model-cores... tree | commitdiff
2018-09-11 Aina NiemetzRefactor non-clausal simplify preprocessing pass. ... tree | commitdiff
2018-09-05 Andrew ReynoldsFiner-grained inference of substitutions in incremental... tree | commitdiff
2018-09-04 Aina NiemetzTransfer ownership of learned literals from SMT engine... tree | commitdiff
2018-09-04 Aina NiemetzFix merge mishap of #2359. tree | commitdiff
2018-08-30 Mathias PreinerRefactor theory preprocess into preprocessing pass... tree | commitdiff
2018-08-29 Mathias PreinerRefactor MipLibTrick preprocessing pass. (#2359) tree | commitdiff
2018-08-28 Aina NiemetzMove flag needsFinish from SMT engine to circuit propag... tree | commitdiff
2018-08-26 Andres NoetzliRefactor unconstrained simplification pass (#2374) tree | commitdiff
2018-08-25 yoni206Refactor quantifier macros preprocessing pass (#1840) tree | commitdiff
2018-08-25 Haniel BarbosaRefactor nlExtPurify preprocessing pass (#1963) tree | commitdiff
2018-08-24 Andrew Reynolds Remove spurious disabling of cbqi-all (#2368) tree | commitdiff
2018-08-24 Andrew Reynolds Do not print internally generated datatypes in externa... tree | commitdiff
2018-08-23 Haniel BarbosaMakes the filename be set in the SMT engine by default... tree | commitdiff
2018-08-23 Aina NiemetzRefactor ITE simplification preprocessing pass. (#2360) tree | commitdiff
2018-08-23 Andres NoetzliUse "filename" instead of "name" in SmtEngine::setInfo... tree | commitdiff
2018-08-23 yoni206global-negate preprocessing pass (#2317) tree | commitdiff
2018-08-21 Tim KingRemoving unused bool members in command.cpp. Also initi... tree | commitdiff
2018-08-21 Mathias PreinerMove d_realAssertionsEnd from SmtEnginePrivate to Asser... tree | commitdiff
2018-08-21 Andrew ReynoldsUse cbqi-full for sygus (#2346) tree | commitdiff
2018-08-20 Andrew Reynolds Make sygus inference a preprocessing pass (#2334) tree | commitdiff
2018-08-17 Andrew Reynolds Eliminate partial operators in sygus grammar normaliza... tree | commitdiff
2018-08-17 Mathias PreinerRefactor eager atoms preprocessing pass. (#2318) tree | commitdiff
2018-08-17 Haniel Barbosacleaning unnecessary timers/dumps (#2327) tree | commitdiff
2018-08-17 Caleb DonovickMake quantifiers-preprocess preprocessing pass (#2322) tree | commitdiff
2018-08-17 Andres NoetzliRefactor IteRemoval preprocessing pass (#1793) tree | commitdiff
2018-08-16 Andres NoetzliMove node algorithms to separate file (#2311) tree | commitdiff
2018-08-16 Haniel BarbosaRefactor extended rewriter preprocessing pass (#2324) tree | commitdiff
2018-08-16 Haniel BarbosaRefactor apply2const (#2316) tree | commitdiff
2018-08-15 Andres NoetzliRemove unused tuple classes (#2313) tree | commitdiff
2018-08-15 Andrew ReynoldsMake sort inference a preprocessing pass (#2309) tree | commitdiff
2018-08-15 Andres NoetzliFix dumping of get-unsat-assumptions (#2302) tree | commitdiff
2018-08-14 Andres NoetzliFix get-unsat-assumptions output (#2301) tree | commitdiff
2018-08-08 Andrew ReynoldsDo beta-reduction in expandDefinitions (#2286) tree | commitdiff
2018-08-08 Andres NoetzliRequire Swig 3 (#2283) tree | commitdiff
2018-08-08 Andres NoetzliDelete functions instead of using CVC4_UNDEFINED (... tree | commitdiff
2018-08-07 Andrew Reynolds Move sygus quantifier elimination step for non-ground... tree | commitdiff
2018-08-06 Andrew ReynoldsFixes for sygus inference (#2238) tree | commitdiff
2018-08-02 Andres NoetzliRemove outdated references to TLS (#2245) tree | commitdiff
2018-08-02 Andrew ReynoldsFix issues with printing parametric datatypes in smt2... tree | commitdiff
2018-08-01 ayveejayImprovements and tests for the API around separation... tree | commitdiff
2018-07-31 Mathias PreinerFix option handler for lazy/bv-sat-solver combinations... tree | commitdiff
2018-07-30 Mathias PreinerAdd support for incremental eager bit-blasting. (#1838) tree | commitdiff
2018-07-27 Andrew Reynolds Make check-synth robust for assertions that are not... tree | commitdiff
2018-07-26 yoni206Disabling bvLazyRewriteExtf in the right place (#2214) tree | commitdiff
2018-07-25 ayveejayPerforming clang-format on the original change-set... tree | commitdiff
2018-07-24 ayveejayAdding API access methods to get heap/nil expressions... tree | commitdiff
2018-07-23 Andrew ReynoldsGeneralize symmetry detection for 1 symmetry variable... tree | commitdiff
2018-07-17 yoni206Refactor sep-pre-skolem-emp preprocessing pass tree | commitdiff
2018-07-17 Andrew ReynoldsDo extended rewrite on results of quantifier eliminatio... tree | commitdiff
2018-07-11 Caleb DonovickMove rewrite to pass (#2128) tree | commitdiff
2018-07-03 Andrew ReynoldssygusComp2018: update sygus-related options setting... tree | commitdiff
2018-07-03 Andrew ReynoldsRemove miscellaneous dead and unused code from quantifi... tree | commitdiff
2018-07-02 Aina NiemetzRefactor ApplySubsts preprocessing pass. (#2120) tree | commitdiff
2018-07-02 Caleb DonovickAdd missing include (#2127) tree | commitdiff
2018-06-27 Andrew ReynoldsSynthesize candidate-rewrites from standard inputs... tree | commitdiff
next